|
1 | 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: |
| 2 | +Mainly just a collection of various algorithms used in SMT solvers, implemented in Haskell: |
3 | 3 |
|
4 | 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) |
| 5 | + * [Davis–Putnam–Logemann–Loveland (DPLL)](/src/SAT/DPLL.hs) |
| 6 | + * [Conflict Driven Clause Learning (CDCL)](/src/SAT/CDCL.hs) |
7 | 7 | * Uninterpreted Functions
|
8 |
| - * [x] [Congruence Closure](/src/Theory/UninterpretedFunctions.hs) |
| 8 | + * [Congruence Closure](/src/Theory/UninterpretedFunctions.hs) |
9 | 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) |
| 10 | + * [Simplex Method](/src/Theory/LinearArithmatic/Simplex.hs) |
| 11 | + * [Fourier-Motzkin](/src/Theory/LinearArithmatic/FourierMotzkin.hs) |
| 12 | + * [Branch and Bound](/src/Theory/LinearArithmatic/BranchAndBound.hs) |
13 | 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 |
| 14 | + * [Interval Constraint Propagation](/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs) |
| 15 | + * [Subtropical Satisfiability](/src/Theory/NonLinearRealArithmatic/Subtropical.hs) |
| 16 | + * [Cylindtrical Algebraic Decomposition](/src/Theory/NonLinearRealArithmatic/CAD.hs) |
| 17 | + * Virtual Substitution |
18 | 18 |
|
0 commit comments