Fixing failures in minisat

6 files changed, 27 insertions, 45 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 5d88a9240..5f8eb12b9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -94,12 +94,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 }
 
 Node CnfStream::getNode(const SatLiteral& literal) {
-  Node node;
   NodeCache::iterator find = d_nodeCache.find(literal);
-  if(find != d_nodeCache.end()) {
-    node = find->second;
-  }
-  return node;
+  Assert(find != d_nodeCache.end());
+  return find->second;
 }
 
 SatLiteral CnfStream::convertAtom(TNode node) {
@@ -121,20 +118,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
   return lit;
 }
 
-SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) {
+SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
-  SatLiteral literal;
-  if(create) {
-    if(find == d_translationCache.end()) {
-      literal = convertAtom(node);
-    } else {
-      literal = find->second;
-    }
-  } else {
-    Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
-    literal = find->second;
-  }
-  Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl;
+  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/cnf_stream.h b/src/prop/cnf_stream.h
index c88b1e265..2ff107068 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -174,14 +174,8 @@ public:
    * representation.
    * @param node [Presumably there are some constraints on the kind of
    * node? E.g., it needs to be a boolean? -Chris]
-   * @param create Controls whether or not to create a new SAT literal
-   * mapping for Node if it does not exist.  This exists to break
-   * circular dependencies, where an atom is converted and asserted to
-   * the SAT solver, which propagates it immediately since it's a
-   * unit, which can theory-propagate additional literals that don't
-   * yet have a SAT literal mapping.
    */
-  SatLiteral getLiteral(TNode node, bool create = false);
+  SatLiteral getLiteral(TNode node);
 
   const TranslationCache& getTranslationCache() const {
     return d_translationCache;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 0da9fc249..39978ab5e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -134,7 +134,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
 
 
 CRef Solver::reason(Var x) const {
-    // If we already have a reaspon, just return it
+    // If we already have a reason, just return it
     if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
 
     // What's the literal we are trying to explain
@@ -143,7 +143,7 @@ CRef Solver::reason(Var x) const {
     // Get the explanation from the theory
     SatClause explanation;
     proxy->explainPropagation(l, explanation);
-    assert(explanation[0] == l);
+    Assert(explanation[0] == l);
 
     // We're actually changing the state, so we hack it into non-const
     Solver* nonconst_this = const_cast<Solver*>(this);
@@ -191,7 +191,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
 
 void Solver::attachClause(CRef cr) {
     const Clause& c = ca[cr];
-    assert(c.size() > 1);
+    Assert(c.size() > 1);
     watches[~c[0]].push(Watcher(cr, c[1]));
     watches[~c[1]].push(Watcher(cr, c[0]));
     if (c.learnt()) learnts_literals += c.size();
@@ -493,7 +493,7 @@ CRef Solver::propagate(TheoryCheckType type)
 
     // The effort we will be using to theory check
     CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
-        CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD;
+    CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD;
 
     // Keep running until we have checked everything, we
     // have no conflict and no new literals have been asserted
@@ -521,6 +521,7 @@ bool Solver::propagateTheory() {
   proxy->theoryPropagate(propagatedLiterals);
   const unsigned i_end = propagatedLiterals.size();
   for (unsigned i = 0; i < i_end; ++ i) {
+    Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
     uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy);
   }
   proxy->clearPropagatedLiterals();
@@ -550,7 +551,7 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
     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(assigns[var(clause[i])] != l_Undef, "Got an unassigned literal in conflict!");
+      Assert(value(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
@@ -613,6 +614,7 @@ CRef Solver::propagateBool()
                 *j++ = w; continue; }
 
             // Look for new watch:
+            Assert(c.size() >= 2);
             for (int k = 2; k < c.size(); k++)
                 if (value(c[k]) != l_False){
                     c[1] = c[k]; c[k] = false_lit;
@@ -789,12 +791,12 @@ lbool Solver::search(int nof_conflicts)
                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
             }
 
-			// We have a conflict so, we are going back to standard checks
+	    // 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 this was a final check, we are satisfiable
             if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
               return l_True;
 
@@ -1036,7 +1038,7 @@ void Solver::relocAll(ClauseAllocator& to)
     for (int i = 0; i < trail.size(); i++){
         Var v = var(trail[i]);
 
-        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
+        if (hasReason(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
             ca.reloc(vardata[v].reason, to);
     }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index a47e865a1..bb8a81f16 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -300,6 +300,7 @@ protected:
     int      decisionLevel    ()      const; // Gives the current decisionlevel.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
     CRef     reason           (Var x) const;
+    bool     hasReason        (Var x) const; // Does the variable have a reason
     int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
     bool     withinBudget     ()      const;
@@ -323,6 +324,8 @@ protected:
 //=================================================================================================
 // Implementation of inline methods:
 
+inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+
 inline int  Solver::level (Var x) const { return vardata[x].level; }
 
 inline void Solver::insertVarOrder(Var x) {
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 57ec29259..2197cb23e 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -56,12 +56,7 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
   const unsigned i_end = outputNodes.size();
   for (unsigned i = 0; i < i_end; ++ i) {
     Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
-    // The second argument ("true") instructs the CNF stream to create
-    // a new literal mapping if it doesn't exist.  This can happen due
-    // to a circular dependence, if a SAT literal "a" is asserted as a
-    // unit to the SAT solver, a round of theory propagation can occur
-    // before all Nodes have SAT variable mappings.
-    SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true);
+    SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]);
     output.push_back(l);
   }
 }
@@ -91,11 +86,8 @@ void SatSolver::clearPropagatedLiterals() {
 void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   Node literalNode = d_cnfStream->getNode(l);
   Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
-  // We can get null from the prop engine if the literal is useless (i.e.)
-  // the expression is not in context anyomore
-  if(!literalNode.isNull()) {
-    d_theoryEngine->assertFact(literalNode);
-  }
+  Assert(!literalNode.isNull());
+  d_theoryEngine->assertFact(literalNode);
 }
 
 void SatSolver::setCnfStream(CnfStream* cnfStream) {
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 7d6f6ff50..f25862b54 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -49,8 +49,11 @@ if HAVE_CXXTESTGEN
 AM_CPPFLAGS = \
 	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" \
 	"-I@top_srcdir@/src" "-I@top_builddir@/src" \
+	"-I@top_srcdir@/src/prop/minisat" \
+	-D __STDC_LIMIT_MACROS \
+	-D __STDC_FORMAT_MACROS \	        
 	$(ANTLR_INCLUDES) $(TEST_CPPFLAGS)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(TEST_CXXFLAGS)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
 AM_LDFLAGS = $(TEST_LDFLAGS)
 
 AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST