adding support for unit conflicts in minisat...

3 files changed, 26 insertions, 5 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 10cd02f94..02eecf858 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -103,7 +103,8 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
-{}
+{
+}
 
 
 Solver::~Solver()
@@ -709,19 +710,30 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
   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
+    // Do some normalization
+    sort(clause);
+    // Find the max level of the conflict and normalize the clause
     int max_level = 0;
     int max_intro_level = 0;
-    for (int i = 0; i < clause_size; ++i) {
+    int i, j = 0;
+    Lit p;
+    for (i = 0; i < clause_size; ++i) {
+      if (clause[i] == p) continue;
       Var v = var(clause[i]);
       int current_level = level(v);
       int current_intro_level = intro_level(v);
       Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(v) << " at level " << current_level << std::endl;
-      Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!");
+      Assert(value(clause[i]) == l_False, "Got an non-true literal in conflict!");
       if (current_level > max_level) max_level = current_level;
       if (current_intro_level > max_intro_level) max_intro_level = current_intro_level;
+      p = clause[j ++] = clause[i];
+    }
+    clause.shrink(i - j);
+    // If there is only one literal add an extra false literal
+    if (clause.size() == 1) {
+      Debug("unit-conflicts") << "Unit conflict!" << proxy->getNode(clause[0]) << std::endl;
+      clause.push(false_literal);
     }
     // 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;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 1eb407c62..65fcf32a0 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -82,6 +82,9 @@ protected:
   /** True if we are currently solving. */
   bool in_solve;
 
+  /** The variable representing Boolean true value */
+  Lit false_literal;
+
 public:
 
     // Constructor/Destructor:
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8bcd9fe76..27ccaacfd 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -67,6 +67,12 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(0, dummy);
     remove_satisfied      = false;
+
+    // Add the true literal immediately
+    Var true_variable = newVar(false, false, false);
+    setFrozen(true_variable, true);
+    false_literal = mkLit(true_variable, true);
+    uncheckedEnqueue(~false_literal, CRef_Undef);
 }