From: Dejan Jovanović Date: Mon, 16 Aug 2010 21:49:42 +0000 (+0000) Subject: Fixing failures in minisat X-Git-Tag: cvc5-1.0.0~8890 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c5ed2290cff5247df673b87d9401993d3ca0fc3;p=cvc5.git Fixing failures in minisat --- 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(this); @@ -191,7 +191,7 @@ bool Solver::addClause_(vec& 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& 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