Poster

[4tXJ7f]

Random comments on the poster (will add more to the issue as time goes by):

• [x] Mention how many different preprocessing passes there are
• [x] Maybe include two or so examples of preprocessing passes
• [x] API -> Context
• [x] Maybe have a list of classes that you implemented (PreprocessingPass, PreprocessingPassContext, PreprocessingPassRegistry) with a 1-2 sentence description of their purpose.
• [x] Drawing is missing PreprocessingPassRegistry

[4tXJ7f]

Getting there :)

• [x] "data structures like lists and bit vectors": replace "lists" with "arrays". Lists are not really natively supported
• [x] "An SMT, being a decision problem, can output two results": SMT what?
• [x] "exists a possible assignment" -> "exists an assignment"
• [x] "no combination of variable assignments" -> "no variable assignment"
• [x] "Prior to solving, the underbelly of CVC4 includes a preprocessing step is necessary to make equations readable to the solver or easier to solve": does not quite parse
• [x] "If-then-else clauses are unreadable" -> "If-then-else terms are not supported internally"
• [x] "before the DPLL solving" -> "before the DPLL(T) solving"
• [x] "Preprocessing Context – a class that receives variables from SmtEngine and passes them to the preprocessing passes": maybe something like: "Preprocessing Context – a restricted interface for preprocessing passes to interact with solver internals"
• [x] For the graphic: The SMTEngine owns both Context and Registry, no?
• [x] "The new implementation allow for more flexibility in certain test cases." -> "The new implementation allow for more flexibility."
• [x] "Ideally, the flexibility will allow for multiple ways of processing certain problems. In some circumstances, an ideal method of preprocessing will be found and can be used for similar SMT problems." -> "The flexibility can be used to automatically find better configurations by systematically trying different configurations on a fixed set of benchmarks."