Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theor...

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.

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51992a31c3bc63a0b3a1cd51baa52d3dc923e0ab..634ba00d45452c2a6d35c61fe8c71e3dee98ff6d 100644 (file)
--- 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 e54884925e163eab03d57750f4268a882981d262..0f8622cb8895691848d07b19d6c872532b024336 100644 (file)
--- 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 922d596beb15816ab382108ecb50bce9e38649fc..f105310803e703f18ef78195a0b820bd37274a18 100644 (file)
--- 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 83082ff5d0f3a4c6a9a2abe46619c7376af8fe97..c0cf06767638fd0d30bd68d108ad2921545dea1b 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -173,6 +173,16 @@ public:
     d_facts.push(n);
   }
 
+  /**
+   * Clear the assertion queue.
+   */
+  void clearAssertionQueue() {
+    while (d_facts.size() > 0) {
+      d_facts.pop();
+    }
+  }
+
+
   /**
    * Check the current assignment's consistency.
    */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 87a78d9209a93a8bfadc8906b812bc5acbd3f01d..4751a584cb7aca2427aed0681a1716730f26206f 100644 (file)
--- 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 45d0eaecbcee63a80e6e092ca7a856dd88778b8c..8b747c3e1b1dbaa8ffb99cbaf1df94479ec0f8ba 100644 (file)
--- 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 fa298f1a5efb272aecfe30907d0dc782e5110ce0..a4e08ff994639c2a7c274797b4aebdd6874c79ba 100644 (file)
--- 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