Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).

Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing. 

Adding 3 more small problems from the library that we can solve now to the regressions.

7 files changed, 52 insertions, 7 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51992a31c..634ba00d4 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -98,10 +98,8 @@ Node CnfStream::getNode(const SatLiteral& literal) {
 
 SatLiteral CnfStream::getLiteral(const TNode& node) {
   TranslationCache::iterator find = d_translationCache.find(node);
-  SatLiteral literal;
-  if(find != d_translationCache.end()) {
-    literal = find->second;
-  }
+  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+  SatLiteral literal = find->second;
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
 }
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index e54884925..0f8622cb8 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -182,6 +182,8 @@ void Solver::cancelUntil(int level) {
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
     }
+    // Now, clear the TheoryEngine queue
+    proxy->clearAssertionQueues();
 }
 
 
@@ -442,7 +444,25 @@ Clause* Solver::propagateTheory()
   Clause* c = NULL;
   SatClause clause;
   proxy->theoryCheck(clause);
-  if (clause.size() > 0) {
+  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);
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 922d596be..f10531080 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -93,6 +93,8 @@ public:
   inline void enqueueTheoryLiteral(const SatLiteral& l);
 
   inline void setCnfStream(CnfStream* cnfStream);
+
+  inline void clearAssertionQueues();
 };
 
 }/* CVC4::prop namespace */
@@ -207,6 +209,10 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) {
 }
 
 
+void SatSolver::clearAssertionQueues() {
+  d_theoryEngine->clearAssertionQueues();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 83082ff5d..c0cf06767 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -174,6 +174,16 @@ public:
   }
 
   /**
+   * Clear the assertion queue.
+   */
+  void clearAssertionQueue() {
+    while (d_facts.size() > 0) {
+      d_facts.pop();
+    }
+  }
+
+
+  /**
    * Check the current assignment's consistency.
    */
   virtual void check(Effort level = FULL_EFFORT) = 0;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 87a78d920..4751a584c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -150,6 +150,13 @@ public:
     return d_theoryOut.d_conflictNode;
   }
 
+  /**
+   * Clears the queues of the theories.
+   */
+  void clearAssertionQueues() {
+    d_uf.clearAssertionQueue();
+  }
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */
diff --git a/test/regress/regress0/let.smt b/test/regress/regress0/let.smt
index 45d0eaecb..8b747c3e1 100644
--- a/test/regress/regress0/let.smt
+++ b/test/regress/regress0/let.smt
@@ -2,4 +2,5 @@
   :logic QF_UF
   :status unsat
   :extrafuns ((a U) (b U) (f U U)) 
-  :formula (let (?x a) (not (= ?x a))))
\ No newline at end of file
+  :formula (let (?x a) (and (= a b) (not (= ?x b))))
+)
\ No newline at end of file
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index fa298f1a5..a4e08ff99 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -2,7 +2,10 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
 TESTS =	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
-	simple.04.cvc
+	simple.04.cvc \
+	dead_dnd002.smt \
+	iso_brn001.smt \
+	SEQ032_size2.smt
 
 # synonyms for "check"
 .PHONY: regress regress0 test