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:

• [x] AST: Data structures for the expression tree.
• [x] Simplifier: Word-level simplifications on the AST data structure.
• [x] 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.