Poster

[4tXJ7f]

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

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

[4tXJ7f]

Getting there :)

• "data structures like lists and bit vectors": replace "lists" with "arrays". Lists are not really natively supported
• "An SMT, being a decision problem, can output two results": SMT what?
• "exists a possible assignment" -> "exists an assignment"
• "no combination of variable assignments" -> "no variable assignment"
• "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
• "If-then-else clauses are unreadable" -> "If-then-else terms are not supported internally"
• "before the DPLL solving" -> "before the DPLL(T) solving"
• "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"
• For the graphic: The SMTEngine owns both Context and Registry, no?
• "The new implementation allow for more flexibility in certain test cases." -> "The new implementation allow for more flexibility."
• "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."