From 709ea9740eb99ef599763e5cee46dbad4f09f46c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 1 Nov 2014 20:20:53 +0100 Subject: [PATCH] TODO update. --- TODO.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/TODO.md b/TODO.md index 1b746684..807e66a7 100644 --- a/TODO.md +++ b/TODO.md @@ -2,9 +2,13 @@ ## Main goals -- Functorise `solver.ml` with term module and theory module - * SAT solver depends on actual boolean literals - * Move terms and theories (SMT part) to another directory +- Include cnf conversion in 'sat' library +- 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 as resolution * Each theory brings its own proof output (tautologies), somehow * pure resolution proofs between boolean clauses and theory tautologies @@ -12,6 +16,8 @@ - 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 ## Long term goals