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