Towards a complete SMT solver

[Robbepop]

For stevia to be a more or less complete SMT solver the following high-level modules will need to be implemented in one form or another:

• AST: Data structures for the expression tree.
• Simplifier: Word-level simplifications on the AST data structure.
• Simple Serializer: Serialize AST data structure into human-readable form.
• SMTLib2 Parser: Parse input given in SMTLib2 compliant form.
  • WIP: https://github.com/Robbepop/stevia/tree/master/stevia_parser
• SAT Driver: Drives the underlying SAT solver with the given CNF formula.
  • FFI Bindings: https://github.com/Robbepop/ipasir-rs

With AIG optimizations:

• SMT -> AIG: Bit Blaster: Transform a given AST expression tree into a pure boolean formula. The resulting boolean formula should be cheaply convertible to an AIG representation.
• AIG Driver: Drives processing AIG input.
• AIG -> CNF: Tseytin Transformation -> Transforms AIG represented data to CNF format.

Additional optimizations:

• Abstraction Refinement: Heuristics and driver for the array-abstraction-refinement. Maybe this could also handle the newly developed copy-abstraction-refinement.
• Linear Bitvector Solver: Optimizer and solver for some specialized bitvector terms. Also involves writing of some word-level transformations to preprocess AST data into normalized form.