From: Christopher L. Conway Date: Fri, 14 May 2010 22:50:17 +0000 (+0000) Subject: Adding debugging code in PropEngine/CnfStream X-Git-Tag: cvc5-1.0.0~9057 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07e1a1668a27e90563f23bcf5abb5cb7fe30da86;p=cvc5.git Adding debugging code in PropEngine/CnfStream --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 233032706..eb77b0d54 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -47,12 +47,14 @@ void CnfStream::assertClause(SatLiteral a) { clause[0] = a; assertClause(clause); } + void CnfStream::assertClause(SatLiteral a, SatLiteral b) { SatClause clause(2); clause[0] = a; clause[1] = b; assertClause(clause); } + void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { SatClause clause(3); clause[0] = a; @@ -104,6 +106,14 @@ SatLiteral CnfStream::getLiteral(TNode node) { return literal; } +const CnfStream::NodeCache& CnfStream::getNodeCache() const { + return d_nodeCache; +} + +const CnfStream::TranslationCache& CnfStream::getTranslationCache() const { + return d_translationCache; +} + SatLiteral TseitinCnfStream::handleAtom(TNode node) { Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); @@ -285,6 +295,8 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); + Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; + SatLiteral condLit = toCNF(iteNode[0]); SatLiteral thenLit = toCNF(iteNode[1]); SatLiteral elseLit = toCNF(iteNode[2]); @@ -293,20 +305,30 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // If ITE is true then one of the branches is true and the condition // implies which one + // lit -> (ite b t e) + // lit -> (t | e) & (b -> t) & (!b -> e) + // lit -> (t | e) & (!b | t) & (b | e) + // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) + assertClause(~iteLit, thenLit, elseLit); assertClause(~iteLit, ~condLit, thenLit); assertClause(~iteLit, condLit, elseLit); - assertClause(~iteLit, elseLit, thenLit); // If ITE is false then one of the branches is false and the condition // implies which one + // !lit -> !(ite b t e) + // !lit -> (!t | !e) & (b -> !t) & (!b -> !e) + // !lit -> (!t | !e) & (!b | !t) & (b | !e) + // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) + assertClause(iteLit, ~thenLit, ~elseLit); assertClause(iteLit, ~condLit, ~thenLit); assertClause(iteLit, condLit, ~elseLit); - assertClause(iteLit, ~thenLit, ~elseLit); return iteLit; } Node TseitinCnfStream::handleNonAtomicNode(TNode node) { + Debug("cnf") << "handleNonAtomicNode(" << node << ")" << endl; + /* Our main goal here is to tease out any ITE's sitting under a theory operator. */ Node rewrite; NodeManager *nodeManager = NodeManager::currentNM(); @@ -347,6 +369,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { } SatLiteral TseitinCnfStream::toCNF(TNode node) { + Debug("cnf") << "toCNF(" << node << ")" << endl; // If the node has already been translated, return the previous translation if(isCached(node)) { diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ae4582d6f..7546a8880 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -39,18 +39,19 @@ class PropEngine; * @author Tim King */ class CnfStream { +public: + /** Cache of what nodes have been registered to a literal. */ + typedef __gnu_cxx::hash_map NodeCache; + + /** Cache of what literals have been registered to a node. */ + typedef __gnu_cxx::hash_map TranslationCache; private: /** The SAT solver we will be using */ SatInputInterface *d_satSolver; - /** Cache of what literals have been registered to a node. */ - typedef __gnu_cxx::hash_map TranslationCache; TranslationCache d_translationCache; - - /** Cache of what nodes have been registered to a literal. */ - typedef __gnu_cxx::hash_map NodeCache; NodeCache d_nodeCache; protected: @@ -153,6 +154,8 @@ public: */ SatLiteral getLiteral(TNode node); + const TranslationCache& getTranslationCache() const; + const NodeCache& getNodeCache() const; }; /* class CnfStream */ /** diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 6b28e6f99..ec0e2dfbc 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,6 +25,7 @@ #include #include +#include using namespace std; using namespace CVC4::context; @@ -65,6 +66,26 @@ void PropEngine::assertLemma(TNode node) { d_cnfStream->convertAndAssert(node); } + +void PropEngine::printSatisfyingAssignment(){ + const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache(); + Debug("prop-value") << "Literal | Value | Expr" << endl + << "---------------------------------------------------------" << endl; + for(CnfStream::TranslationCache::const_iterator i = transCache.begin(), + end = transCache.end(); + i != end; + ++i) { + pair curr = *i; + SatLiteral l = curr.second; + if(!sign(l)) { + Node n = curr.first; + SatLiteralValue value = d_satSolver->value(l); + Debug("prop-value") << /*setw(4) << */ "'" << l << "' " /*<< setw(4)*/ << value << " " << n + << endl; + } + } +} + Result PropEngine::checkSat() { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "PropEngine::checkSat()" << endl; @@ -74,6 +95,11 @@ Result PropEngine::checkSat() { bool result = d_satSolver->solve(); // Not in checkSat any more d_inCheckSat = false; + + if( result && debugTagIsOn("prop") ) { + printSatisfyingAssignment(); + } + Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl; return Result(result ? Result::SAT : Result::UNSAT); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 36f6cb0cb..4d25e9bc0 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -63,6 +63,8 @@ class PropEngine { /** The CNF converter in use */ CnfStream* d_cnfStream; + void printSatisfyingAssignment(); + public: /** diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index c578cf361..46d2182a9 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -28,6 +28,7 @@ void SatSolver::theoryCheck(SatClause& conflict) { 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()) { diff --git a/src/prop/sat.h b/src/prop/sat.h index 33ab674c9..42f454820 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -54,6 +54,8 @@ typedef minisat::Lit SatLiteral; /** Type of the SAT clauses */ typedef minisat::vec SatClause; +typedef minisat::lbool SatLiteralValue; + /** * Returns the variable of the literal. * @param lit the literal @@ -71,6 +73,15 @@ hashSatLiteral(const SatLiteral& literal) { return (size_t) minisat::toInt(literal); } +inline std::string stringOfLiteralValue(SatLiteralValue val) { + if( val == minisat::l_False ) { + return "0"; + } else if (val == minisat::l_True ) { + return "1"; + } else { // unknown + return "_"; + } +} #endif /* __CVC4_USE_MINISAT */ /** Interface encapsulating the "input" to the solver, e.g., from the @@ -146,6 +157,8 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); void setCnfStream(CnfStream* cnfStream); + + SatLiteralValue value(SatLiteral l); }; /* Functions that delegate to the concrete SAT solver. */ @@ -185,6 +198,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } +inline SatLiteralValue SatSolver::value(SatLiteral l) { + return d_minisat->modelValue(l); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t @@ -207,6 +224,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { return out; } +inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) { + out << stringOfLiteralValue(val); + return out; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */