File tree 1 file changed +17
-0
lines changed
1 file changed +17
-0
lines changed Original file line number Diff line number Diff line change
1
+ Not really usable as a fully fledged SMT solver right now.
2
+ Mainly just a collection of the various algorithms used in SMT solvers, implemented in Haskell:
3
+
4
+ * SAT solving
5
+ * [x] [ Davis–Putnam–Logemann–Loveland (DPLL)] ( /src/SAT/DPLL.hs )
6
+ * [x] [ Conflict Driven Clause Learning (CDCL)] ( /src/SAT/CDCL.hs )
7
+ * Uninterpreted Functions
8
+ * [x] [ Congruence Closure] ( /src/Theory/UninterpretedFunctions.hs )
9
+ * Linear Arithmatic
10
+ * [x] [ Simplex Method] ( /src/Theory/LinearArithmatic/Simplex.hs )
11
+ * [x] [ Fourier-Motzkin] ( /src/Theory/LinearArithmatic/FourierMotzkin.hs )
12
+ * [x] [ Branch and Bound] ( /src/Theory/LinearArithmatic/FourierMotzkin.hs )
13
+ * Non-Linear Arithmatic
14
+ * [ ] [ Interval Constraint Propagation] ( /src/Theory/NonLinearArithmatic/IntervalConstraintPropagation.hs )
15
+ * [ ] [ Subtropical Satisfiability] ( /src/Theory/NonLinearArithmatic/Subtropical.hs )
16
+ * [ ] [ Cylindtrical Algebraic Decomposition] ( /src/Theory/NonLinearArithmatic/CAD.hs )
17
+ * [ ] Virtual Substitution
1
18
You can’t perform that action at this time.
0 commit comments