Adding the changes to the original copy

16 files changed, 636 insertions, 116 deletions

diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
new file mode 100644
index 000000000..af71779d5
--- /dev/null
+++ b/src/prop/minisat/CVC4-README
@@ -0,0 +1,157 @@
+================ CHANGES TO THE ORIGINAL CODE ==================================
+
+The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and
+the context. The context is obtained from the SmtEngine, and the proxy is an 
+intermediary class that has all-access to the SatSolver so as to simplify the 
+interface to (possible) other sat solvers. These two are passed to minisat at 
+construction time and some additional flags are set. We use the SimpSolver 
+solver with simplifications.
+
+To compare with original minisat code in SVN you can compare to revision 6 on 
+the trunk.
+
+The PropEngine then uses the following
+
+// Create the sat solver (this is the proxy, which will create minisat)
+d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
+// Add some clauses
+d_cnfStream->convertAndAssert(node);
+// Check for satisfiabilty 
+bool result = d_satSolver->solve();
+
+* Adding theory literals:
+
+The newVar method has been changed from 
+  Var Solver::newVar(bool sign, bool dvar)
+to 
+  Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
+in order to mark the variables as theory literals. For that purpose there is a 
+new boolean array called "theory" that is true or false if the variables is for
+a theory literal.
+
+* Backtracking/Pushing
+
+Backtracking in minisat is performed through the cancelUntil() method, which is 
+now modified to pop the context the appropriate number of times.
+
+Minisat pushes the scope in the newDecisionLevel() method where we appropriately 
+also push the CVC4 context.
+
+* Phase caching
+
+In order to implement phase-caching (RSAT paper) we 
+(1) flag minisat to use the user-provided polarities first by setting the 
+minisat::SimpSolver::polarity_user flag when initializing the solver (in sat.h)
+(2) when a variable is set (in uncheckedEnqueue()) we remember the value in the
+"polarity" table.
+
+* Asserting the theory literals
+
+In the uncheckedEnqueue() method, if the literal is a theory literal (looking 
+in the "theory" table), it is passed to the prop engine thorough the proxy. 
+
+* Theory propagation (checking)
+
+The BCP propagation method was changed from propagate to propagateBool and 
+another method propagateTheory is defined to do the theory propagation. The 
+propagate method now looks like
+
+Clause* Solver::propagate()
+{
+    Clause* confl = NULL;
+
+    while(qhead < trail.size()) {
+      confl = propagateBool();
+      if (confl != NULL) break;
+      confl = propagateTheory();
+      if (confl != NULL) break;
+    }
+
+    return confl;
+}
+
+The propagateBool method will perform the BCP on the newly assigned variables 
+in the trail, and if a conflict is found it will break. Otherwise, the theory 
+propagation is given a chance to check for satisfiability and maybe enqueue some
+additional propagated literals. 
+
+* Conflict resolution
+
+If a conflict is detected during theory propagation we can rely on the minisat
+conflict resolution with a twist. Since a theory can return a conflict where
+all literals are assigned at a level lower than the current level, we must 
+backtrack to the highest level of any literal in the conflict. This is done
+already in the propagateTheory().  
+
+* Clause simplification
+
+Minisat performs some simplifications on the clause database:
+(1) variable elimination
+(2) subsumtion
+
+Subsumtion is complete even with theory reasoning, but eliminating theory 
+literals by resolution might be incomplete:
+
+(x = 0 \vee x = 1) \wedge (x != 1 \vee y = 1) \wedge x = y
+            ^^^^^          ^^^^^^
+              v              ~v
+
+would, after eliminating v, simplify to
+(x = 0) wedge (y = 1) wedge (x = y) which is unsatisfiable
+
+while x = 1, y = 1 is a satisfying assignment for the above.
+
+Minisat does not perform variable elimination on the variables that are marked
+as frozen (in the "frozen", SimSolver.h) table. We put all the theory literals 
+in the frozen table, which solves the incompleteness problem. 
+
+================ NOTES =========================================================
+
+* Accessing the internals of the SAT solver
+
+The non-public parts of the SAT solver are accessed via the static methods in 
+the SatSolver class. SatSolverProxy is declared as a friend of the 
+SatSolver and has all-privileges access to the internals -- use with care!!!
+
+* Clause Database and CNF
+
+The clause database consists of two parts:
+
+    vec<Clause*>        clauses;          // List of problem clauses.
+    vec<Clause*>        learnts;          // List of learnt clauses.
+
+Clauses is the original problem clauses, and learnts are the clauses learned 
+during the search. I have disabled removal of satisfied problem clauses by 
+setting the remove_satisfied flag to false.
+
+The learnt clauses get removed every once in a while by removing the half of
+clauses with the low activity (reduceDB())
+
+Since the clause database backtracks with the SMT solver, the CNF cache should
+be context dependent and everything will be in sync. 
+
+* Adding a Clause
+
+The only method in the interface that allows addition of clauses in MiniSAT is
+
+    bool Solver::addClause(vec<Lit>& ps),
+
+but it only adds the problem clauses. 
+
+In order to add the clauses to the removable database the interface is now 
+
+    bool Solver::addClause(vec<Lit>& ps, bool removable).      
+
+Clauses added with removable=true might get removed by the SAT solver when 
+compacting the database.
+
+The question is whether to add the propagation/conflict lemmas as removable or 
+not?
+
+* Literal Activities
+
+We do not backtrack literal activities. This does not semantically change the 
+equivalence of the context, but does change solve times if the same problem is
+run several times.
+
+* Do we need to assign literals that only appear in satisfied clauses?
diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile
new file mode 100644
index 000000000..e8b442ac1
--- /dev/null
+++ b/src/prop/minisat/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/prop/minisat
+
+include $(topdir)/Makefile.subdir
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
new file mode 100644
index 000000000..56f61adad
--- /dev/null
+++ b/src/prop/minisat/Makefile.am
@@ -0,0 +1,29 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG
+
+noinst_LTLIBRARIES = libminisat.la
+libminisat_la_SOURCES = \
+	core/Solver.C \
+	core/Solver.h \
+	core/SolverTypes.h \
+	simp/SimpSolver.C \
+	simp/SimpSolver.h \
+	mtl/Alg.h \
+	mtl/BasicHeap.h \
+	mtl/BoxedVec.h \
+	mtl/Heap.h \
+	mtl/Map.h \
+	mtl/Queue.h \
+	mtl/Sort.h \
+	mtl/Vec.h
+
+EXTRA_DIST = \
+	core/Main.C \
+	core/Makefile \
+	simp/Main.C \
+	simp/Makefile \
+	README \
+	LICENSE \
+	mtl/template.mk
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 404f4da5e..1667af20d 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -19,17 +19,46 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "Solver.h"
 #include "Sort.h"
+#include "prop/sat.h"
 #include <cmath>
 
-
 //=================================================================================================
 // Constructor/Destructor:
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
+Clause* Solver::lazy_reason = reinterpret_cast<Clause*>(1);
+
+Clause* Solver::getReason(Lit l)
+{
+    if (reason[var(l)] != lazy_reason) return reason[var(l)];
+    // Get the explanation from the theory
+    SatClause explanation;
+    if (value(l) == l_True) {
+      proxy->explainPropagation(l, explanation);
+      assert(explanation[0] == l);
+    } else {
+      proxy->explainPropagation(~l, explanation);
+      assert(explanation[0] == ~l);
+    }
+    Clause* real_reason = Clause_new(explanation, true);
+    reason[var(l)] = real_reason;
+    // Add it to the database
+    learnts.push(real_reason);
+    attachClause(*real_reason);
+    return real_reason;
+}
+
+Solver::Solver(SatSolver* proxy, context::Context* context) :
 
-Solver::Solver() :
+    // SMT stuff
+    proxy(proxy)
+  , context(context)
 
     // Parameters: (formerly in 'SearchParams')
-    var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
+  , var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
   , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
 
     // More parameters:
@@ -70,7 +99,7 @@ Solver::~Solver()
 // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
 //
-Var Solver::newVar(bool sign, bool dvar)
+Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
 {
     int v = nVars();
     watches   .push();          // (list for positive literal)
@@ -81,6 +110,8 @@ Var Solver::newVar(bool sign, bool dvar)
     activity  .push(0);
     seen      .push(0);
 
+    theory    .push(theoryAtom);
+
     polarity    .push((char)sign);
     decision_var.push((char)dvar);
 
@@ -89,7 +120,7 @@ Var Solver::newVar(bool sign, bool dvar)
 }
 
 
-bool Solver::addClause(vec<Lit>& ps)
+bool Solver::addClause(vec<Lit>& ps, ClauseType type)
 {
     assert(decisionLevel() == 0);
 
@@ -110,16 +141,19 @@ bool Solver::addClause(vec<Lit>& ps)
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
+        assert(type != CLAUSE_LEMMA);
         assert(value(ps[0]) == l_Undef);
         uncheckedEnqueue(ps[0]);
-        return ok = (propagate() == NULL);
+        return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL);
     }else{
         Clause* c = Clause_new(ps, false);
         clauses.push(c);
+        if (type == CLAUSE_LEMMA) lemmas.push(c);
         attachClause(*c);
     }
 
     return true;
+
 }
 
 
@@ -132,6 +166,7 @@ void Solver::attachClause(Clause& c) {
 
 
 void Solver::detachClause(Clause& c) {
+    Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
     assert(find(watches[toInt(~c[0])], &c));
     assert(find(watches[toInt(~c[1])], &c));
@@ -142,8 +177,10 @@ void Solver::detachClause(Clause& c) {
 
 
 void Solver::removeClause(Clause& c) {
+    Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl;
     detachClause(c);
-    free(&c); }
+    free(&c);
+}
 
 
 bool Solver::satisfied(const Clause& c) const {
@@ -157,14 +194,26 @@ bool Solver::satisfied(const Clause& c) const {
 //
 void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
-        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+        // Pop the SMT context
+        for (int l = trail_lim.size() - level; l > 0; --l)
+          context->pop();
+        // Now the minisat stuff
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--) {
             Var     x  = var(trail[c]);
             assigns[x] = toInt(l_Undef);
-            insertVarOrder(x); }
+            insertVarOrder(x);
+        }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
-    } }
+        // We can erase the lemmas now
+        for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) {
+          // TODO: can_erase[lemma[c]] = true;
+        }
+        lemmas.shrink(lemmas.size() - lemmas_lim[level]);
+        lemmas_lim.shrink(lemmas_lim.size() - level);
+    }
+}
 
 
 //=================================================================================================
@@ -255,7 +304,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
         p     = trail[index+1];
-        confl = reason[var(p)];
+        confl = getReason(p);
         seen[var(p)] = 0;
         pathC--;
 
@@ -272,12 +321,12 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         out_learnt.copyTo(analyze_toclear);
         for (i = j = 1; i < out_learnt.size(); i++)
-            if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level))
+            if (getReason(out_learnt[i]) == NULL || !litRedundant(out_learnt[i], abstract_level))
                 out_learnt[j++] = out_learnt[i];
     }else{
         out_learnt.copyTo(analyze_toclear);
         for (i = j = 1; i < out_learnt.size(); i++){
-            Clause& c = *reason[var(out_learnt[i])];
+            Clause& c = *getReason(out_learnt[i]);
             for (int k = 1; k < c.size(); k++)
                 if (!seen[var(c[k])] && level[var(c[k])] > 0){
                     out_learnt[j++] = out_learnt[i];
@@ -315,13 +364,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     analyze_stack.clear(); analyze_stack.push(p);
     int top = analyze_toclear.size();
     while (analyze_stack.size() > 0){
-        assert(reason[var(analyze_stack.last())] != NULL);
+        assert(getReason(analyze_stack.last()) != NULL);
         Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
 
         for (int i = 1; i < c.size(); i++){
             Lit p  = c[i];
             if (!seen[var(p)] && level[var(p)] > 0){
-                if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
+                if (getReason(p) != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
                     seen[var(p)] = 1;
                     analyze_stack.push(p);
                     analyze_toclear.push(p);
@@ -381,16 +430,110 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 void Solver::uncheckedEnqueue(Lit p, Clause* from)
 {
     assert(value(p) == l_Undef);
-    assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
-    level   [var(p)] = decisionLevel();
-    reason  [var(p)] = from;
+    assigns  [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost efficient
+    level    [var(p)] = decisionLevel();
+    reason   [var(p)] = from;
+    // Added for phase-caching
+    polarity [var(p)] = sign(p);
     trail.push(p);
+
+    if (theory[var(p)] && from != lazy_reason) {
+      // Enqueue to the theory
+      proxy->enqueueTheoryLiteral(p);
+    }
+}
+
+
+Clause* Solver::propagate(TheoryCheckType type)
+{
+    Clause* confl = NULL;
+
+    // If this is the final check, no need for Boolean propagation and
+    // theory propagation
+    if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+      return theoryCheck(theory::Theory::FULL_EFFORT);
+    }
+
+    // The effort we will be using to theory check
+    theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
+        theory::Theory::QUICK_CHECK : theory::Theory::STANDARD;
+
+    // Keep running until we have checked everything, we
+    // have no conflict and no new literals have been asserted
+    bool new_assertions;
+    do {
+        new_assertions = false;
+        while(qhead < trail.size()) {
+            confl = propagateBool();
+            if (confl != NULL) break;
+            confl = theoryCheck(effort);
+            if (confl != NULL) break;
+        }
+
+        if (confl == NULL && type == CHECK_WITH_PROPAGATION_STANDARD) {
+          new_assertions = propagateTheory();
+          if (!new_assertions) break;
+        }
+    } while (new_assertions);
+
+    return confl;
 }
 
+bool Solver::propagateTheory() {
+  std::vector<Lit> propagatedLiterals;
+  proxy->theoryPropagate(propagatedLiterals);
+  const unsigned i_end = propagatedLiterals.size();
+  for (unsigned i = 0; i < i_end; ++ i) {
+    uncheckedEnqueue(propagatedLiterals[i], lazy_reason);
+  }
+  proxy->clearPropagatedLiterals();
+  return propagatedLiterals.size() > 0;
+}
 
 /*_________________________________________________________________________________________________
 |
-|  propagate : [void]  ->  [Clause*]
+|  theoryCheck: [void]  ->  [Clause*]
+|
+|  Description:
+|    Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting
+|    clause is returned, otherwise NULL.
+|
+|    Note: the propagation queue might be NOT empty
+|________________________________________________________________________________________________@*/
+Clause* Solver::theoryCheck(theory::Theory::Effort effort)
+{
+  Clause* c = NULL;
+  SatClause clause;
+  proxy->theoryCheck(effort, clause);
+  int clause_size = clause.size();
+  Assert(clause_size != 1, "Can't handle unit clause explanations");
+  if(clause_size > 0) {
+    // Find the max level of the conflict
+    int max_level = 0;
+    for (int i = 0; i < clause_size; ++i) {
+      int current_level = level[var(clause[i])];
+      Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason[var(clause[i])] << " at level " << current_level << std::endl;
+      Assert(toLbool(assigns[var(clause[i])]) != l_Undef, "Got an unassigned literal in conflict!");
+      if (current_level > max_level) max_level = current_level;
+    }
+    // If smaller than the decision level then pop back so we can analyse
+    Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
+    Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!");
+    if (max_level < decisionLevel()) {
+      Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
+      cancelUntil(max_level);
+    }
+    // Create the new clause and attach all the information
+    c = Clause_new(clause, true);
+    learnts.push(c);
+    attachClause(*c);
+  }
+  return c;
+}
+
+/*_________________________________________________________________________________________________
+|
+|  propagateBool : [void]  ->  [Clause*]
 |  
 |  Description:
 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
@@ -399,7 +542,7 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from)
 |    Post-conditions:
 |      * the propagation queue is empty, even if there was a conflict.
 |________________________________________________________________________________________________@*/
-Clause* Solver::propagate()
+Clause* Solver::propagateBool()
 {
     Clause* confl     = NULL;
     int     num_props = 0;
@@ -509,7 +652,7 @@ bool Solver::simplify()
 {
     assert(decisionLevel() == 0);
 
-    if (!ok || propagate() != NULL)
+    if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL)
         return ok = false;
 
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
@@ -554,9 +697,9 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
     starts++;
 
     bool first = true;
-
+    TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
     for (;;){
-        Clause* confl = propagate();
+        Clause* confl = propagate(check_type);
         if (confl != NULL){
             // CONFLICT
             conflicts++; conflictC++;
@@ -582,9 +725,16 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
             varDecayActivity();
             claDecayActivity();
 
+            // We have a conflict so, we are going back to standard checks
+            check_type = CHECK_WITH_PROPAGATION_STANDARD;
+
         }else{
             // NO CONFLICT
 
+            // If this was a final check, we are satisfiable
+            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
+              return l_True;
+
             if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
@@ -620,9 +770,11 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
                 decisions++;
                 next = pickBranchLit(polarity_mode, random_var_freq);
 
-                if (next == lit_Undef)
-                    // Model found:
-                    return l_True;
+                if (next == lit_Undef) {
+                    // We need to do a full theory check to confirm
+                    check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
+                    continue;
+                }
             }
 
             // Increase decision level and enqueue 'next'
@@ -722,7 +874,8 @@ void Solver::verifyModel()
 
     assert(!failed);
 
-    reportf("Verified %d original clauses.\n", clauses.size());
+    if(verbosity >= 1)
+        reportf("Verified %d original clauses.\n", clauses.size());
 }
 
 
@@ -739,3 +892,8 @@ void Solver::checkLiteralCount()
         assert((int)clauses_literals == cnt);
     }
 }
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 0137b6ff3..2e44803e9 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -17,34 +17,68 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Solver_h
-#define Solver_h
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROP__MINISAT__SOLVER_H
+#define __CVC4__PROP__MINISAT__SOLVER_H
+
+#include "context/context.h"
+#include "theory/theory.h"
 
 #include <cstdio>
+#include <cassert>
 
-#include "Vec.h"
-#include "Heap.h"
-#include "Alg.h"
+#include "../mtl/Vec.h"
+#include "../mtl/Heap.h"
+#include "../mtl/Alg.h"
 
 #include "SolverTypes.h"
 
-
 //=================================================================================================
 // Solver -- the main class:
 
+namespace CVC4 {
+namespace prop {
+
+class SatSolver;
+
+namespace minisat {
 
 class Solver {
+
+  /** The only CVC4 entry point to the private solver data */
+  friend class CVC4::prop::SatSolver;
+
+protected:
+
+  /** The pointer to the proxy that provides interfaces to the SMT engine */
+  SatSolver* proxy;
+
+  /** The context from the SMT solver */
+  context::Context* context;
+
 public:
 
     // Constructor/Destructor:
     //
-    Solver();
-    ~Solver();
+    Solver(SatSolver* proxy, context::Context* context);
+    CVC4_PUBLIC ~Solver();
 
     // Problem specification:
     //
-    Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
-    bool    addClause (vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+    Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
+
+    // Types of clauses
+    enum ClauseType {
+      // Clauses defined by the problem
+      CLAUSE_PROBLEM,
+      // Lemma clauses added by the theories
+      CLAUSE_LEMMA,
+      // Conflict clauses
+      CLAUSE_CONFLICT
+    };
+
+    bool    addClause (vec<Lit>& ps, ClauseType type);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
 
     // Solving:
     //
@@ -54,7 +88,7 @@ public:
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
     // Variable mode:
-    // 
+    //
     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
 
@@ -122,12 +156,20 @@ protected:
     vec<vec<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
     vec<char>           assigns;          // The current assignments (lbool:s stored as char:s).
     vec<char>           polarity;         // The preferred polarity of each variable.
+    vec<bool>           theory;           // Is the variable representing a theory atom
     vec<char>           decision_var;     // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
-    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+    vec<Clause*>        lemmas;           // List of lemmas we added (context dependent)
+    vec<int>            lemmas_lim;       // Separator indices for different decision levels in 'lemmas'.
+    static Clause*      lazy_reason;      // The mark when we need to ask the theory engine for a reason
+    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, lazy_reason if theory propagated, or 'NULL' if none.
+
+    Clause* getReason(Lit l);             // Returns the reason, or asks the theory for an explanation
+
     vec<int>            level;            // 'level[var]' contains the level at which the assignment was made.
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+    int                 lhead;            // Head of the lemma stack (for backtracking)
     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
@@ -144,6 +186,15 @@ protected:
     vec<Lit>            analyze_toclear;
     vec<Lit>            add_tmp;
 
+    enum TheoryCheckType {
+      // Quick check, but don't perform theory propagation
+      CHECK_WITHOUTH_PROPAGATION_QUICK,
+      // Check and perform theory propagation
+      CHECK_WITH_PROPAGATION_STANDARD,
+      // The SAT problem is satisfiable, perform a full theory check
+      CHECK_WITHOUTH_PROPAGATION_FINAL
+    };
+
     // Main internal methods:
     //
     void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
@@ -151,7 +202,10 @@ protected:
     void     newDecisionLevel ();                                                      // Begins a new decision level.
     void     uncheckedEnqueue (Lit p, Clause* from = NULL);                            // Enqueue a literal. Assumes value of literal is undefined.
     bool     enqueue          (Lit p, Clause* from = NULL);                            // Test if fact 'p' contradicts current state, enqueue otherwise.
-    Clause*  propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
+    Clause*  propagate        (TheoryCheckType type);                                  // Perform Boolean and Theory. Returns possibly conflicting clause.
+    Clause*  propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
+    bool     propagateTheory  ();                                                      // Perform Theory propagation. Return true if any literals were asserted.
+    Clause*  theoryCheck      (theory::Theory::Effort effort);                         // Perform a theory satisfiability check. Returns possibly conflicting clause.
     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
     void     analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
@@ -177,7 +231,7 @@ protected:
 
     // Misc:
     //
-    int      decisionLevel    ()      const; // Gives the current decisionlevel.
+    int      decisionLevel    ()      const; // Gives the current decision level.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 
@@ -203,11 +257,9 @@ protected:
         return (int)(drand(seed) * size); }
 };
 
-
 //=================================================================================================
 // Implementation of inline methods:
 
-
 inline void Solver::insertVarOrder(Var x) {
     if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
 
@@ -233,7 +285,7 @@ inline void Solver::claBumpActivity (Clause& c) {
 
 inline bool     Solver::enqueue         (Lit p, Clause* from)   { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
 inline bool     Solver::locked          (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.size()); context->push(); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level[x] & 31); }
@@ -256,6 +308,7 @@ inline bool     Solver::okay          ()      const   { return ok; }
 
 
 #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
+//#define reportf(format, args...) do {} while(0)
 
 static inline void logLit(FILE* f, Lit l)
 {
@@ -297,6 +350,9 @@ inline void Solver::printClause(const C& c)
     }
 }
 
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
 //=================================================================================================
-#endif
+#endif /* __CVC4__PROP__MINISAT__SOLVER_H */
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 47e302390..fd6a78ab0 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -17,13 +17,18 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
 
-#ifndef SolverTypes_h
-#define SolverTypes_h
+#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H
+#define __CVC4__PROP__MINISAT__SOLVERTYPES_H
 
 #include <cassert>
 #include <stdint.h>
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
 
@@ -194,4 +199,8 @@ inline void Clause::strengthen(Lit p)
     calcAbstraction();
 }
 
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 240962dfc..e636f2b87 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -17,8 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Alg_h
-#define Alg_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Alg_h
+#define CVC4_MiniSat_Alg_h
+
+#include <cassert>
+
+namespace CVC4 {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // Useful functions on vectors
@@ -54,4 +62,8 @@ static inline bool find(V& ts, const T& t)
     return j < ts.size();
 }
 
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Alg_h */
diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h
index 556d98f84..cb6a7cbd8 100644
--- a/src/prop/minisat/mtl/BasicHeap.h
+++ b/src/prop/minisat/mtl/BasicHeap.h
@@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef BasicHeap_h
-#define BasicHeap_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_BasicHeap_h
+#define CVC4_MiniSat_BasicHeap_h
 
 #include "Vec.h"
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
 
@@ -95,4 +101,9 @@ class BasicHeap {
 
 
 //=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_BasicHeap_h */
diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h
index bddf41008..7cf5ba14f 100644
--- a/src/prop/minisat/mtl/BoxedVec.h
+++ b/src/prop/minisat/mtl/BoxedVec.h
@@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef BoxedVec_h
-#define BoxedVec_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_BoxedVec_h
+#define CVC4_MiniSat_BoxedVec_h
 
 #include <cstdlib>
 #include <cassert>
 #include <new>
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // Automatically resizable arrays
 //
@@ -50,7 +56,7 @@ class bvec {
             x->cap = size;
             return x;
         }
-        
+
     };
 
     Vec_t* ref;
@@ -76,16 +82,16 @@ class bvec {
     altvec (altvec<T>& other)                  { assert(0); }
 
 public:
-    void     clear  (bool dealloc = false) { 
+    void     clear  (bool dealloc = false) {
         if (ref != NULL){
-            for (int i = 0; i < ref->sz; i++) 
+            for (int i = 0; i < ref->sz; i++)
                 (*ref).data[i].~T();
 
-            if (dealloc) { 
-                free(ref); ref = NULL; 
-            }else 
+            if (dealloc) {
+                free(ref); ref = NULL;
+            }else
                 ref->sz = 0;
-        } 
+        }
     }
 
     // Constructors:
@@ -107,11 +113,11 @@ public:
         int cap  = ref != NULL ? ref->cap : 0;
         if (size == cap){
             cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap); 
+            ref = Vec_t::alloc(ref, cap);
         }
-        //new (&ref->data[size]) T(elem); 
-        ref->data[size] = elem; 
-        ref->sz = size+1; 
+        //new (&ref->data[size]) T(elem);
+        ref->data[size] = elem;
+        ref->sz = size+1;
     }
 
     void     push   () {
@@ -119,10 +125,10 @@ public:
         int cap  = ref != NULL ? ref->cap : 0;
         if (size == cap){
             cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap); 
+            ref = Vec_t::alloc(ref, cap);
         }
-        new (&ref->data[size]) T(); 
-        ref->sz = size+1; 
+        new (&ref->data[size]) T();
+        ref->sz = size+1;
     }
 
     void     shrink (int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
@@ -143,5 +149,8 @@ public:
 
 };
 
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif
+#endif /* CVC4_MiniSat_BoxedVec_h */
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index b07ccd152..20d379b1d 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -17,10 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Heap_h
-#define Heap_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Heap_h
+#define CVC4_MiniSat_Heap_h
 
 #include "Vec.h"
+#include <cassert>
+
+namespace CVC4 {
+namespace prop {
+namespace minisat {
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
@@ -92,7 +99,7 @@ class Heap {
 
         indices[n] = heap.size();
         heap.push(n);
-        percolateUp(indices[n]); 
+        percolateUp(indices[n]);
     }
 
 
@@ -104,19 +111,19 @@ class Heap {
         indices[x]       = -1;
         heap.pop();
         if (heap.size() > 1) percolateDown(0);
-        return x; 
+        return x;
     }
 
 
-    void clear(bool dealloc = false) 
-    { 
+    void clear(bool dealloc = false)
+    {
         for (int i = 0; i < heap.size(); i++)
             indices[heap[i]] = -1;
 #ifdef NDEBUG
         for (int i = 0; i < indices.size(); i++)
             assert(indices[i] == -1);
 #endif
-        heap.clear(dealloc); 
+        heap.clear(dealloc);
     }
 
 
@@ -164,6 +171,9 @@ class Heap {
 
 };
 
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
 //=================================================================================================
-#endif
+#endif /* CVC4_MiniSat_Heap_h */
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index b6d76a31c..715b84da4 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Map_h
-#define Map_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Map_h
+#define CVC4_MiniSat_Map_h
 
 #include <stdint.h>
 
 #include "Vec.h"
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // Default hash/equals functions
 //
@@ -80,7 +86,7 @@ class Map {
         cap = newsize;
     }
 
-    
+
     public:
 
      Map () : table(NULL), cap(0), size(0) {}
@@ -94,7 +100,7 @@ class Map {
         for (int i = 0; i < ps.size(); i++)
             if (equals(ps[i].key, k)){
                 d = ps[i].data;
-                return true; } 
+                return true; }
         return false;
     }
 
@@ -115,4 +121,8 @@ class Map {
     }
 };
 
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Map_h */
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 2cc110ce9..291a1f2e3 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Queue_h
-#define Queue_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Queue_h
+#define CVC4_MiniSat_Queue_h
 
 #include "Vec.h"
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 
 
@@ -79,4 +85,9 @@ public:
 //};
 
 //=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Queue_h */
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 1f301f5c2..19e89803b 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Sort_h
-#define Sort_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Sort_h
+#define CVC4_MiniSat_Sort_h
 
 #include "Vec.h"
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // Some sorting algorithms for vec's
 
@@ -90,4 +96,9 @@ template <class T> void sort(vec<T>& v) {
 
 
 //=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Sort_h */
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index e780aa167..364991aa9 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Vec_h
-#define Vec_h
+#include "cvc4_private.h"
+
+#ifndef CVC4_MiniSat_Vec_h
+#define CVC4_MiniSat_Vec_h
 
 #include <cstdlib>
 #include <cassert>
 #include <new>
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
 //=================================================================================================
 // Automatically resizable arrays
 //
@@ -129,5 +135,8 @@ void vec<T>::clear(bool dealloc) {
         sz = 0;
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif
+#endif /* CVC4_MiniSat_Vec_h */
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 22121c31e..00f93402f 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -24,9 +24,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //=================================================================================================
 // Constructor/Destructor:
 
+namespace CVC4 {
+namespace prop {
+namespace minisat {
 
-SimpSolver::SimpSolver() :
-    grow               (0)
+SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) :
+    Solver(proxy, context)
+  , grow               (0)
   , asymm_mode         (false)
   , redundancy_check   (false)
   , merges             (0)
@@ -54,14 +58,14 @@ SimpSolver::~SimpSolver()
 }
 
 
-Var SimpSolver::newVar(bool sign, bool dvar) {
-    Var v = Solver::newVar(sign, dvar);
+Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) {
+    Var v = Solver::newVar(sign, dvar,theoryAtom);
 
     if (use_simplification){
         n_occ    .push(0);
         n_occ    .push(0);
         occurs   .push();
-        frozen   .push((char)false);
+        frozen   .push((char)theoryAtom);
         touched  .push(0);
         elim_heap.insert(v);
         elimtable.push();
@@ -114,7 +118,7 @@ bool SimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp
 
 
 
-bool SimpSolver::addClause(vec<Lit>& ps)
+bool SimpSolver::addClause(vec<Lit>& ps, ClauseType type)
 {
     for (int i = 0; i < ps.size(); i++)
         if (isEliminated(var(ps[i])))
@@ -125,7 +129,7 @@ bool SimpSolver::addClause(vec<Lit>& ps)
     if (redundancy_check && implied(ps))
         return true;
 
-    if (!Solver::addClause(ps))
+    if (!Solver::addClause(ps, type))
         return false;
 
     if (use_simplification && clauses.size() == nclauses + 1){
@@ -152,6 +156,7 @@ bool SimpSolver::addClause(vec<Lit>& ps)
 
 void SimpSolver::removeClause(Clause& c)
 {
+    Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
     assert(!c.learnt());
 
     if (use_simplification)
@@ -207,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l)
         updateElimHeap(var(l));
     }
 
-    return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true;
+    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true;
 }
 
 
@@ -224,11 +229,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     for (int i = 0; i < qs.size(); i++){
         if (var(qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(ps[j]) == var(qs[i]))
+                if (var(ps[j]) == var(qs[i])) {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+                }
             out_clause.push(qs[i]);
         }
         next:;
@@ -256,11 +262,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
     for (int i = 0; i < qs.size(); i++){
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(__ps[j]) == var(__qs[i]))
+                if (var(__ps[j]) == var(__qs[i])) {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+                }
         }
         next:;
     }
@@ -305,7 +312,7 @@ bool SimpSolver::implied(const vec<Lit>& c)
             uncheckedEnqueue(~c[i]);
         }
 
-    bool result = propagate() != NULL;
+    bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL;
     cancelUntil(0);
     return result;
 }
@@ -387,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c)
         else
             l = c[i];
 
-    if (propagate() != NULL){
+    if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){
         cancelUntil(0);
         asymm_lits++;
         if (!strengthenClause(c, l))
@@ -478,7 +485,7 @@ bool SimpSolver::eliminateVar(Var v, bool fail)
     vec<Lit> resolvent;
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++)
-            if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
+            if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent, CLAUSE_CONFLICT))
                 return false;
 
     // DEBUG: For checking that a clause set is saturated with respect to variable elimination.
@@ -520,7 +527,7 @@ void SimpSolver::remember(Var v)
             clause.push(c[j]);
 
         remembered_clauses++;
-        check(addClause(clause));
+        check(addClause(clause, CLAUSE_PROBLEM));
         free(&c);
     }
 
@@ -698,3 +705,7 @@ void SimpSolver::toDimacs(const char* file)
     }else
         fprintf(stderr, "could not open file %s\n", file);
 }
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index f1bf88240..3da574f6c 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -17,26 +17,35 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef SimpSolver_h
-#define SimpSolver_h
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
+#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
 
 #include <cstdio>
+#include <cassert>
+
+#include "../mtl/Queue.h"
+#include "../core/Solver.h"
 
-#include "Queue.h"
-#include "Solver.h"
+namespace CVC4 {
+namespace prop {
 
+class SatSolver;
+
+namespace minisat {
 
 class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver();
-    ~SimpSolver();
+    SimpSolver(SatSolver* proxy, context::Context* context);
+    CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
     //
-    Var     newVar    (bool polarity = true, bool dvar = true);
-    bool    addClause (vec<Lit>& ps);
+    Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
+    bool    addClause (vec<Lit>& ps, ClauseType type);
 
     // Variable mode:
     // 
@@ -157,5 +166,9 @@ inline bool  SimpSolver::isEliminated (Var v) const { return v < elimtable.size(
 inline void  SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
 inline bool  SimpSolver::solve        (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
 
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
 //=================================================================================================
-#endif
+#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */