README.md

Not really usable as a fully fledged SMT solver right now. Mainly just a collection of various algorithms used in SMT solvers, implemented in Haskell:

• SAT solving
  • Davis–Putnam–Logemann–Loveland (DPLL)
  • Conflict Driven Clause Learning (CDCL)
• Uninterpreted Functions
  • Congruence Closure
• Linear Arithmatic
  • Simplex Method
  • Fourier-Motzkin
  • Branch and Bound
• Non-Linear Arithmatic
  • Interval Constraint Propagation
  • Subtropical Satisfiability
  • Cylindtrical Algebraic Decomposition
  • Virtual Substitution