Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
gruhn authored Nov 22, 2024
1 parent e4e055c commit c0974e8
Showing 1 changed file with 11 additions and 11 deletions.
22 changes: 11 additions & 11 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
Not really usable as a fully fledged SMT solver right now.
Mainly just a collection of the various algorithms used in SMT solvers, implemented in Haskell:
Mainly just a collection of various algorithms used in SMT solvers, implemented in Haskell:

* SAT solving
* [x] [Davis–Putnam–Logemann–Loveland (DPLL)](/src/SAT/DPLL.hs)
* [x] [Conflict Driven Clause Learning (CDCL)](/src/SAT/CDCL.hs)
* [Davis–Putnam–Logemann–Loveland (DPLL)](/src/SAT/DPLL.hs)
* [Conflict Driven Clause Learning (CDCL)](/src/SAT/CDCL.hs)
* Uninterpreted Functions
* [x] [Congruence Closure](/src/Theory/UninterpretedFunctions.hs)
* [Congruence Closure](/src/Theory/UninterpretedFunctions.hs)
* Linear Arithmatic
* [x] [Simplex Method](/src/Theory/LinearArithmatic/Simplex.hs)
* [x] [Fourier-Motzkin](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
* [x] [Branch and Bound](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
* [Simplex Method](/src/Theory/LinearArithmatic/Simplex.hs)
* [Fourier-Motzkin](/src/Theory/LinearArithmatic/FourierMotzkin.hs)
* [Branch and Bound](/src/Theory/LinearArithmatic/BranchAndBound.hs)
* Non-Linear Arithmatic
* [ ] [Interval Constraint Propagation](/src/Theory/NonLinearArithmatic/IntervalConstraintPropagation.hs)
* [ ] [Subtropical Satisfiability](/src/Theory/NonLinearArithmatic/Subtropical.hs)
* [ ] [Cylindtrical Algebraic Decomposition](/src/Theory/NonLinearArithmatic/CAD.hs)
* [ ] Virtual Substitution
* [Interval Constraint Propagation](/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs)
* [Subtropical Satisfiability](/src/Theory/NonLinearRealArithmatic/Subtropical.hs)
* [Cylindtrical Algebraic Decomposition](/src/Theory/NonLinearRealArithmatic/CAD.hs)
* Virtual Substitution

0 comments on commit c0974e8

Please sign in to comment.