From 5610cb498499683950fea4280a51ca060f1429c3 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 29 Oct 2014 14:40:13 +0100
Subject: [PATCH] update TODO

---
 TODO.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/TODO.md b/TODO.md
index 0662d4e8..1b746684 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,12 +1,19 @@
 # Goals
 
+## 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
 - Add proof output as resolution
     * Each theory brings its own proof output (tautologies), somehow
     * pure resolution proofs between boolean clauses and theory tautologies
+- Add model extraction (at least for SAT)
 - 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)?
 
+## Long term goals
+
+- unsat-core (easy from resolution proofs)
+- max-sat/max-smt