mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 13:38:43 -05:00

Guillaume Bury 6338f682df Added unsat-core option in sat_solve

Cleaned up a bit soler_types and added some doc

2014-11-11 12:25:16 +01:00

Goals

Main goals

Modify theories to allow passing bulk of assumed literals
- Create shared "vector" (formulas/atoms ?)
- Allow theory propagation
Cleanup code
- Simplify Solver.Make functor
- Clean Solver_types interface
Add proof output for smt/theories
- Each theory brings its own proof output (tautologies), somehow
Allow to plug one's code into boolean propagation
- react upon propagation (possibly by propagating more, or side-effect)
- more advanced/specific propagation (2-clauses)?
- implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf )
Adapt old code for theories, inorder to plug it into new Solver Functor