diff options
-rw-r--r-- | src/prop/cnf_stream.cpp | 334 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 322 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 14 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 24 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 10 |
6 files changed, 331 insertions, 375 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 62e4eee29..8936fb584 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -38,9 +38,6 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -using namespace std; -using namespace CVC4::kind; - namespace CVC4 { namespace prop { @@ -48,6 +45,7 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, OutputManager* outMgr, + ResourceManager* rm, bool fullLitToNodeMap, std::string name) : d_satSolver(satSolver), @@ -59,24 +57,15 @@ CnfStream::CnfStream(SatSolver* satSolver, d_convertAndAssertCounter(0), d_registrar(registrar), d_name(name), - d_cnfProof(NULL), - d_removable(false) + d_cnfProof(nullptr), + d_removable(false), + d_resourceManager(rm) { } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, - Registrar* registrar, - context::Context* context, - OutputManager* outMgr, - ResourceManager* rm, - bool fullLitToNodeMap, - std::string name) - : CnfStream(satSolver, registrar, context, outMgr, fullLitToNodeMap, name), - d_resourceManager(rm) -{} - -void CnfStream::assertClause(TNode node, SatClause& c) { - Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl; +bool CnfStream::assertClause(TNode node, SatClause& c) +{ + Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n"; if (Dump.isOn("clauses") && d_outMgr != nullptr) { const Printer& printer = d_outMgr->getPrinter(); @@ -98,34 +87,40 @@ void CnfStream::assertClause(TNode node, SatClause& c) { } } - ClauseId clause_id = d_satSolver->addClause(c, d_removable); - if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added) + ClauseId clauseId = d_satSolver->addClause(c, d_removable); - if (d_cnfProof && clause_id != ClauseIdError) + if (d_cnfProof && clauseId != ClauseIdUndef) { - d_cnfProof->registerConvertedClause(clause_id); + d_cnfProof->registerConvertedClause(clauseId); } + return clauseId != ClauseIdUndef; } -void CnfStream::assertClause(TNode node, SatLiteral a) { +bool CnfStream::assertClause(TNode node, SatLiteral a) +{ SatClause clause(1); clause[0] = a; - assertClause(node, clause); + return assertClause(node, clause); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) { +bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) +{ SatClause clause(2); clause[0] = a; clause[1] = b; - assertClause(node, clause); + return assertClause(node, clause); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) { +bool CnfStream::assertClause(TNode node, + SatLiteral a, + SatLiteral b, + SatLiteral c) +{ SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; - assertClause(node, clause); + return assertClause(node, clause); } bool CnfStream::hasLiteral(TNode n) const { @@ -133,11 +128,12 @@ bool CnfStream::hasLiteral(TNode n) const { return find != d_nodeToLiteralMap.end(); } -void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { +void CnfStream::ensureLiteral(TNode n, bool noPreregistration) +{ // These are not removable and have no proof ID d_removable = false; - Debug("cnf") << "ensureLiteral(" << n << ")" << endl; + Trace("cnf") << "ensureLiteral(" << n << ")\n"; if(hasLiteral(n)) { SatLiteral lit = getLiteral(n); if(!d_literalToNodeMap.contains(lit)){ @@ -203,20 +199,25 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { } SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) { - Debug("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom << ")" << endl; + Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom + << ")\n" + << push; Assert(node.getKind() != kind::NOT); // Get the literal for this node SatLiteral lit; if (!hasLiteral(node)) { + Trace("cnf") << d_name << "::newLiteral: node already registered\n"; // If no literal, we'll make one if (node.getKind() == kind::CONST_BOOLEAN) { + Trace("cnf") << d_name << "::newLiteral: boolean const\n"; if (node.getConst<bool>()) { lit = SatLiteral(d_satSolver->trueVar()); } else { lit = SatLiteral(d_satSolver->falseVar()); } } else { + Trace("cnf") << d_name << "::newLiteral: new var\n"; lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate)); } d_nodeToLiteralMap.insert(node, lit); @@ -239,19 +240,28 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister d_registrar->preRegister(node); d_removable = backupRemovable; } - // Here, you can have it - Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; - + Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop; return lit; } TNode CnfStream::getNode(const SatLiteral& literal) { - Debug("cnf") << "getNode(" << literal << ")" << endl; - Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl; + Trace("cnf") << "getNode(" << literal << ")\n"; + Trace("cnf") << "getNode(" << literal << ") => " + << d_literalToNodeMap[literal] << "\n"; return d_literalToNodeMap[literal]; } +const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const +{ + return d_nodeToLiteralMap; +} + +const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const +{ + return d_literalToNodeMap; +} + void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { context::CDList<TNode>::const_iterator it, it_end; for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) { @@ -265,7 +275,7 @@ void CnfStream::setProof(CnfProof* proof) { } SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { - Debug("cnf") << "convertAtom(" << node << ")" << endl; + Trace("cnf") << "convertAtom(" << node << ")\n"; Assert(!hasLiteral(node)) << "atom already mapped!"; @@ -274,9 +284,12 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { bool preRegister = false; // Is this a variable add it to the list - if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) { + if (node.isVar() && node.getKind() != kind::BOOLEAN_TERM_VARIABLE) + { d_booleanVariables.push_back(node); - } else { + } + else + { theoryLiteral = true; canEliminate = false; preRegister = !noPreregistration; @@ -295,15 +308,18 @@ SatLiteral CnfStream::getLiteral(TNode node) { << "Literal not in the CNF Cache: " << node << "\n"; SatLiteral literal = d_nodeToLiteralMap[node]; - Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; + Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal + << "\n"; return literal; } -SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { +SatLiteral CnfStream::handleXor(TNode xorNode) +{ Assert(!hasLiteral(xorNode)) << "Atom already mapped!"; - Assert(xorNode.getKind() == XOR) << "Expecting an XOR expression!"; + Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!"; Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; + Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n"; SatLiteral a = toCNF(xorNode[0]); SatLiteral b = toCNF(xorNode[1]); @@ -318,11 +334,13 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { return xorLit; } -SatLiteral TseitinCnfStream::handleOr(TNode orNode) { +SatLiteral CnfStream::handleOr(TNode orNode) +{ Assert(!hasLiteral(orNode)) << "Atom already mapped!"; - Assert(orNode.getKind() == OR) << "Expecting an OR expression!"; + Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!"; Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!"; Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; + Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n"; // Number of children unsigned n_children = orNode.getNumChildren(); @@ -355,11 +373,13 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { return orLit; } -SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { +SatLiteral CnfStream::handleAnd(TNode andNode) +{ Assert(!hasLiteral(andNode)) << "Atom already mapped!"; - Assert(andNode.getKind() == AND) << "Expecting an AND expression!"; + Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!"; Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!"; Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; + Trace("cnf") << "handleAnd(" << andNode << ")\n"; // Number of children unsigned n_children = andNode.getNumChildren(); @@ -392,12 +412,14 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { return andLit; } -SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { +SatLiteral CnfStream::handleImplies(TNode impliesNode) +{ Assert(!hasLiteral(impliesNode)) << "Atom already mapped!"; - Assert(impliesNode.getKind() == IMPLIES) + Assert(impliesNode.getKind() == kind::IMPLIES) << "Expecting an IMPLIES expression!"; Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; + Trace("cnf") << "handleImplies(" << impliesNode << ")\n"; // Convert the children to cnf SatLiteral a = toCNF(impliesNode[0]); @@ -418,13 +440,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { return impliesLit; } - -SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { +SatLiteral CnfStream::handleIff(TNode iffNode) +{ Assert(!hasLiteral(iffNode)) << "Atom already mapped!"; - Assert(iffNode.getKind() == EQUAL) << "Expecting an EQUAL expression!"; + Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!"; Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; - - Debug("cnf") << "handleIff(" << iffNode << ")" << endl; + Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; + Trace("cnf") << "handleIff(" << iffNode << ")\n"; // Convert the children to CNF SatLiteral a = toCNF(iffNode[0]); @@ -450,23 +472,14 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { return iffLit; } - -SatLiteral TseitinCnfStream::handleNot(TNode notNode) { - Assert(!hasLiteral(notNode)) << "Atom already mapped!"; - Assert(notNode.getKind() == NOT) << "Expecting a NOT expression!"; - Assert(notNode.getNumChildren() == 1) << "Expecting exactly 1 child!"; - - SatLiteral notLit = ~toCNF(notNode[0]); - - return notLit; -} - -SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { - Assert(iteNode.getKind() == ITE); +SatLiteral CnfStream::handleIte(TNode iteNode) +{ + Assert(!hasLiteral(iteNode)) << "Atom already mapped!"; + Assert(iteNode.getKind() == kind::ITE); Assert(iteNode.getNumChildren() == 3); Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; - - Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; + Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " + << iteNode[2] << ")\n"; SatLiteral condLit = toCNF(iteNode[0]); SatLiteral thenLit = toCNF(iteNode[1]); @@ -497,64 +510,48 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { return iteLit; } - -SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { - Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; - +SatLiteral CnfStream::toCNF(TNode node, bool negated) +{ + Trace("cnf") << "toCNF(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; SatLiteral nodeLit; Node negatedNode = node.notNode(); // If the non-negated node has already been translated, get the translation if(hasLiteral(node)) { - Debug("cnf") << "toCNF(): already translated" << endl; + Trace("cnf") << "toCNF(): already translated\n"; nodeLit = getLiteral(node); - } else { - // Handle each Boolean operator case - switch(node.getKind()) { - case NOT: - nodeLit = handleNot(node); - break; - case XOR: - nodeLit = handleXor(node); - break; - case ITE: - nodeLit = handleIte(node); - break; - case IMPLIES: - nodeLit = handleImplies(node); - break; - case OR: - nodeLit = handleOr(node); - break; - case AND: - nodeLit = handleAnd(node); - break; - case EQUAL: - if(node[0].getType().isBoolean()) { - nodeLit = handleIff(node); - } else { - nodeLit = convertAtom(node); - } + // Return the (maybe negated) literal + return !negated ? nodeLit : ~nodeLit; + } + // Handle each Boolean operator case + switch (node.getKind()) + { + case kind::NOT: nodeLit = ~toCNF(node[0]); break; + case kind::XOR: nodeLit = handleXor(node); break; + case kind::ITE: nodeLit = handleIte(node); break; + case kind::IMPLIES: nodeLit = handleImplies(node); break; + case kind::OR: nodeLit = handleOr(node); break; + case kind::AND: nodeLit = handleAnd(node); break; + case kind::EQUAL: + nodeLit = + node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node); break; default: - { - //TODO make sure this does not contain any boolean substructure - nodeLit = convertAtom(node); - //Unreachable(); - //Node atomic = handleNonAtomicNode(node); - //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic); - } - break; + { + nodeLit = convertAtom(node); } + break; } - - // Return the appropriate (negated) literal - if (!negated) return nodeLit; - else return ~nodeLit; + // Return the (maybe negated) literal + return !negated ? nodeLit : ~nodeLit; } -void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { - Assert(node.getKind() == AND); +void CnfStream::convertAndAssertAnd(TNode node, bool negated) +{ + Assert(node.getKind() == kind::AND); + Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (!negated) { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); @@ -575,8 +572,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { } } -void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { - Assert(node.getKind() == OR); +void CnfStream::convertAndAssertOr(TNode node, bool negated) +{ + Assert(node.getKind() == kind::OR); + Trace("cnf") << "CnfStream::convertAndAssertOr(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (!negated) { // If the node is a disjunction, we construct a clause and assert it int nChildren = node.getNumChildren(); @@ -597,7 +597,11 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { } } -void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { +void CnfStream::convertAndAssertXor(TNode node, bool negated) +{ + Assert(node.getKind() == kind::XOR); + Trace("cnf") << "CnfStream::convertAndAssertXor(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (!negated) { // p XOR q SatLiteral p = toCNF(node[0], false); @@ -627,7 +631,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { } } -void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { +void CnfStream::convertAndAssertIff(TNode node, bool negated) +{ + Assert(node.getKind() == kind::EQUAL); + Trace("cnf") << "CnfStream::convertAndAssertIff(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (!negated) { // p <=> q SatLiteral p = toCNF(node[0], false); @@ -657,7 +665,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { } } -void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { +void CnfStream::convertAndAssertImplies(TNode node, bool negated) +{ + Assert(node.getKind() == kind::IMPLIES); + Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (!negated) { // p => q SatLiteral p = toCNF(node[0], false); @@ -674,13 +686,20 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { } } -void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { +void CnfStream::convertAndAssertIte(TNode node, bool negated) +{ + Assert(node.getKind() == kind::ITE); + Trace("cnf") << "CnfStream::convertAndAssertIte(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; // ITE(p, q, r) SatLiteral p = toCNF(node[0], false); SatLiteral q = toCNF(node[1], negated); SatLiteral r = toCNF(node[2], negated); // Construct the clauses: // (p => q) and (!p => r) + // + // Note that below q and r can be used directly because whether they are + // negated has been push to the literal definitions above Node nnode = node; if( negated ){ nnode = node.negate(); @@ -698,14 +717,14 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, - bool removable, - bool negated, - bool input) +void CnfStream::convertAndAssert(TNode node, + bool removable, + bool negated, + bool input) { - Debug("cnf") << "convertAndAssert(" << node - << ", removable = " << (removable ? "true" : "false") - << ", negated = " << (negated ? "true" : "false") << ")" << endl; + Trace("cnf") << "convertAndAssert(" << node + << ", negated = " << (negated ? "true" : "false") + << ", removable = " << (removable ? "true" : "false") << ")\n"; d_removable = removable; if (d_cnfProof) @@ -720,9 +739,10 @@ void TseitinCnfStream::convertAndAssert(TNode node, } } -void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { - Debug("cnf") << "convertAndAssert(" << node - << ", negated = " << (negated ? "true" : "false") << ")" << endl; +void CnfStream::convertAndAssert(TNode node, bool negated) +{ + Trace("cnf") << "convertAndAssert(" << node + << ", negated = " << (negated ? "true" : "false") << ")\n"; if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { d_resourceManager->spendResource(ResourceManager::Resource::CnfStep); @@ -731,38 +751,28 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { ++d_convertAndAssertCounter; switch(node.getKind()) { - case AND: - convertAndAssertAnd(node, negated); - break; - case OR: - convertAndAssertOr(node, negated); - break; - case XOR: - convertAndAssertXor(node, negated); - break; - case IMPLIES: - convertAndAssertImplies(node, negated); - break; - case ITE: - convertAndAssertIte(node, negated); - break; - case NOT: - convertAndAssert(node[0], !negated); - break; - case EQUAL: - if( node[0].getType().isBoolean() ){ - convertAndAssertIff(node, negated); - break; - } - CVC4_FALLTHROUGH; - default: - { - Node nnode = node; - if( negated ){ - nnode = node.negate(); - } - // Atoms - assertClause(nnode, toCNF(node, negated)); + case kind::AND: convertAndAssertAnd(node, negated); break; + case kind::OR: convertAndAssertOr(node, negated); break; + case kind::XOR: convertAndAssertXor(node, negated); break; + case kind::IMPLIES: convertAndAssertImplies(node, negated); break; + case kind::ITE: convertAndAssertIte(node, negated); break; + case kind::NOT: convertAndAssert(node[0], !negated); break; + case kind::EQUAL: + if (node[0].getType().isBoolean()) + { + convertAndAssertIff(node, negated); + break; + } + CVC4_FALLTHROUGH; + default: + { + Node nnode = node; + if (negated) + { + nnode = node.negate(); + } + // Atoms + assertClause(nnode, toCNF(node, negated)); } break; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ea64ccf13..3f40bfbbd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -41,8 +41,13 @@ namespace prop { class PropEngine; /** - * Comments for the behavior of the whole class... [??? -Chris] - * @author Tim King <taking@cs.nyu.edu> + * Implements the following recursive algorithm + * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf + * in a single pass. + * + * The general idea is to introduce a new literal that will be equivalent to + * each subexpression in the constructed equi-satisfiable formula, then + * substitute the new literal for the formula, and so on, recursively. */ class CnfStream { public: @@ -54,7 +59,123 @@ class CnfStream { typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap; + /** + * Constructs a CnfStream that performs equisatisfiable CNF transformations + * and sends the generated clauses and to the given SAT solver. This does not + * take ownership of satSolver, registrar, or context. + * + * @param satSolver the sat solver to use. + * @param registrar the entity that takes care of preregistration of Nodes. + * @param context the context that the CNF should respect. + * @param outMgr Reference to the output manager of the smt engine. Assertions + * will not be dumped if outMgr == nullptr. + * @param rm the resource manager of the CNF stream + * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping. + * @param name string identifier to distinguish between different instances + * even for non-theory literals. + */ + CnfStream(SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + OutputManager* outMgr, + ResourceManager* rm, + bool fullLitToNodeMap = false, + std::string name = ""); + /** + * Convert a given formula to CNF and assert it to the SAT solver. + * + * @param node node to convert and assert + * @param removable whether the sat solver can choose to remove the clauses + * @param negated whether we are asserting the node negated + * @param input whether it is an input assertion (rather than a lemma). This + * information is only relevant for unsat core tracking. + */ + void convertAndAssert(TNode node, + bool removable, + bool negated, + bool input = false); + /** + * Get the node that is represented by the given SatLiteral. + * @param literal the literal from the sat solver + * @return the actual node + */ + TNode getNode(const SatLiteral& literal); + + /** + * Returns true iff the node has an assigned literal (it might not be + * translated). + * @param node the node + */ + bool hasLiteral(TNode node) const; + + /** + * Ensure that the given node will have a designated SAT literal that is + * definitionally equal to it. The result of this function is that the Node + * can be queried via getSatValue(). Essentially, this is like a "convert-but- + * don't-assert" version of convertAndAssert(). + */ + void ensureLiteral(TNode n, bool noPreregistration = false); + + /** + * Returns the literal that represents the given node in the SAT CNF + * representation. + * @param node [Presumably there are some constraints on the kind of + * node? E.g., it needs to be a boolean? -Chris] + */ + SatLiteral getLiteral(TNode node); + + /** + * Returns the Boolean variables from the input problem. + */ + void getBooleanVariables(std::vector<TNode>& outputVariables) const; + + /** Retrieves map from nodes to literals. */ + const CnfStream::NodeToLiteralMap& getTranslationCache() const; + + /** Retrieves map from literals to nodes. */ + const CnfStream::LiteralToNodeMap& getNodeCache() const; + + void setProof(CnfProof* proof); + protected: + /** + * Same as above, except that uses the saved d_removable flag. It calls the + * dedicated converter for the possible formula kinds. + */ + void convertAndAssert(TNode node, bool negated); + /** Specific converters for each formula kind. */ + void convertAndAssertAnd(TNode node, bool negated); + void convertAndAssertOr(TNode node, bool negated); + void convertAndAssertXor(TNode node, bool negated); + void convertAndAssertIff(TNode node, bool negated); + void convertAndAssertImplies(TNode node, bool negated); + void convertAndAssertIte(TNode node, bool negated); + + /** + * Transforms the node into CNF recursively and yields a literal + * definitionally equal to it. + * + * This method also populates caches, kept in d_cnfStream, between formulas + * and literals to avoid redundant work and to retrieve formulas from literals + * and vice-versa. + * + * @param node the formula to transform + * @param negated whether the literal is negated + * @return the literal representing the root of the formula + */ + SatLiteral toCNF(TNode node, bool negated = false); + + /** Specific clausifiers, based on the formula kinds, that clausify a formula, + * by calling toCNF into each of the formula's children under the respective + * kind, and introduce a literal definitionally equal to it. */ + SatLiteral handleNot(TNode node); + SatLiteral handleXor(TNode node); + SatLiteral handleImplies(TNode node); + SatLiteral handleIff(TNode node); + SatLiteral handleIte(TNode node); + SatLiteral handleAnd(TNode node); + SatLiteral handleOr(TNode node); + /** The SAT solver we will be using */ SatSolver* d_satSolver; @@ -92,14 +213,6 @@ class CnfStream { /** Pointer to the proof corresponding to this CnfStream */ CnfProof* d_cnfProof; - /** Remove nots from the node */ - TNode stripNot(TNode node) { - while (node.getKind() == kind::NOT) { - node = node[0]; - } - return node; - } - /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't @@ -112,23 +225,26 @@ class CnfStream { * Asserts the given clause to the sat solver. * @param node the node giving rise to this clause * @param clause the clause to assert + * @return whether the clause was asserted in the SAT solver. */ - void assertClause(TNode node, SatClause& clause); + bool assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. * @param node the node giving rise to this clause * @param a the unit literal of the clause + * @return whether the clause was asserted in the SAT solver. */ - void assertClause(TNode node, SatLiteral a); + bool assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. * @param node the node giving rise to this clause * @param a the first literal in the clause * @param b the second literal in the clause + * @return whether the clause was asserted in the SAT solver. */ - void assertClause(TNode node, SatLiteral a, SatLiteral b); + bool assertClause(TNode node, SatLiteral a, SatLiteral b); /** * Asserts the ternary clause to the sat solver. @@ -136,8 +252,9 @@ class CnfStream { * @param a the first literal in the clause * @param b the second literal in the clause * @param c the thirs literal in the clause + * @return whether the clause was asserted in the SAT solver. */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); + bool assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** * Acquires a new variable from the SAT solver to represent the node @@ -163,182 +280,11 @@ class CnfStream { */ SatLiteral convertAtom(TNode node, bool noPreprocessing = false); - public: - /** - * Constructs a CnfStream that sends constructs an equi-satisfiable - * set of clauses and sends them to the given sat solver. This does not take - * ownership of satSolver, registrar, or context. - * @param satSolver the sat solver to use. - * @param registrar the entity that takes care of preregistration of Nodes. - * @param context the context that the CNF should respect. - * @param outMgr Reference to the output manager of the smt engine. Assertions - * will not be dumped if outMgr == nullptr. - * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping. - * @param name string identifier to distinguish between different instances - * even for non-theory literals. - */ - CnfStream(SatSolver* satSolver, - Registrar* registrar, - context::Context* context, - OutputManager* outMgr = nullptr, - bool fullLitToNodeMap = false, - std::string name = ""); - - /** - * Destructs a CnfStream. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. - */ - virtual ~CnfStream() {} - - /** - * Converts and asserts a formula. - * @param node node to convert and assert - * @param removable whether the sat solver can choose to remove the clauses - * @param negated whether we are asserting the node negated - * @param input whether it is an input assertion (rather than a lemma). This - * information is only relevant for unsat core tracking. - */ - virtual void convertAndAssert(TNode node, - bool removable, - bool negated, - bool input = false) = 0; - - /** - * Get the node that is represented by the given SatLiteral. - * @param literal the literal from the sat solver - * @return the actual node - */ - TNode getNode(const SatLiteral& literal); - - /** - * Returns true iff the node has an assigned literal (it might not be - * translated). - * @param node the node - */ - bool hasLiteral(TNode node) const; - - /** - * Ensure that the given node will have a designated SAT literal that is - * definitionally equal to it. The result of this function is that the Node - * can be queried via getSatValue(). Essentially, this is like a "convert-but- - * don't-assert" version of convertAndAssert(). - */ - virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; - - /** - * Returns the literal that represents the given node in the SAT CNF - * representation. - * @param node [Presumably there are some constraints on the kind of - * node? E.g., it needs to be a boolean? -Chris] - */ - SatLiteral getLiteral(TNode node); - - /** - * Returns the Boolean variables from the input problem. - */ - void getBooleanVariables(std::vector<TNode>& outputVariables) const; - - const NodeToLiteralMap& getTranslationCache() const { - return d_nodeToLiteralMap; - } - - const LiteralToNodeMap& getNodeCache() const { return d_literalToNodeMap; } - - void setProof(CnfProof* proof); -}; /* class CnfStream */ - -/** - * TseitinCnfStream is based on the following recursive algorithm - * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf - * The general idea is to introduce a new literal that - * will be equivalent to each subexpression in the constructed equi-satisfiable - * formula, then substitute the new literal for the formula, and so on, - * recursively. - * - * This implementation does this in a single recursive pass. [??? -Chris] - */ -class TseitinCnfStream : public CnfStream { - public: - /** - * Constructs the stream to use the given sat solver. This does not take - * ownership of satSolver, registrar, or context. - * @param satSolver the sat solver to use - * @param registrar the entity that takes care of pre-registration of Nodes - * @param context the context that the CNF should respect. - * @param outMgr reference to the output manager of the smt engine. Assertions - * will not be dumped if outMgr == nullptr. - * @param rm the resource manager of the CNF stream - * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, - * even for non-theory literals - */ - TseitinCnfStream(SatSolver* satSolver, - Registrar* registrar, - context::Context* context, - OutputManager* outMgr, - ResourceManager* rm, - bool fullLitToNodeMap = false, - std::string name = ""); - - /** - * Convert a given formula to CNF and assert it to the SAT solver. - * @param node the formula to assert - * @param removable is this something that can be erased - * @param negated true if negated - * @param input whether it is an input assertion (rather than a lemma). This - * information is only relevant for unsat core tracking. - */ - void convertAndAssert(TNode node, - bool removable, - bool negated, - bool input = false) override; - - private: - /** - * Same as above, except that removable is remembered. - */ - void convertAndAssert(TNode node, bool negated); - - // Each of these formulas handles takes care of a Node of each Kind. - // - // Each handleX(Node &n) is responsible for: - // - constructing a new literal, l (if necessary) - // - calling registerNode(n,l) - // - adding clauses assure that l is equivalent to the Node - // - calling toCNF on its children (if necessary) - // - returning l - // - // handleX( n ) can assume that n is not in d_translationCache - SatLiteral handleNot(TNode node); - SatLiteral handleXor(TNode node); - SatLiteral handleImplies(TNode node); - SatLiteral handleIff(TNode node); - SatLiteral handleIte(TNode node); - SatLiteral handleAnd(TNode node); - SatLiteral handleOr(TNode node); - - void convertAndAssertAnd(TNode node, bool negated); - void convertAndAssertOr(TNode node, bool negated); - void convertAndAssertXor(TNode node, bool negated); - void convertAndAssertIff(TNode node, bool negated); - void convertAndAssertImplies(TNode node, bool negated); - void convertAndAssertIte(TNode node, bool negated); - - /** - * Transforms the node into CNF recursively. - * @param node the formula to transform - * @param negated whether the literal is negated - * @return the literal representing the root of the formula - */ - SatLiteral toCNF(TNode node, bool negated = false); - - void ensureLiteral(TNode n, bool noPreregistration = false) override; - /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; -}; /* class TseitinCnfStream */ +}; /* class CnfStream */ -} /* CVC4::prop namespace */ -} /* CVC4 namespace */ +} // namespace prop +} // namespace CVC4 #endif /* CVC4__PROP__CNF_STREAM_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e3f00d489..4596972e9 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -91,7 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream( + d_cnfStream = new CVC4::prop::CnfStream( d_satSolver, d_registrar, userContext, &d_outMgr, rm, true); d_theoryProxy = new TheoryProxy( diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index c48e20224..046ad4b1b 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -69,13 +69,13 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) } d_satSolver.reset(solver); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_bitblastingRegistrar.get(), - d_nullContext.get(), - nullptr, - rm, - false, - "EagerBitblaster")); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + nullptr, + rm, + false, + "EagerBitblaster")); } EagerBitblaster::~EagerBitblaster() {} diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index c6590db81..95d78c69b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -80,13 +80,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - nullptr, - rm, - false, - "LazyBitblaster")); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + nullptr, + rm, + false, + "LazyBitblaster")); d_satSolverNotify.reset( d_emptyNotify @@ -575,11 +575,11 @@ void TLazyBitblaster::clearSolver() { d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); ResourceManager* rm = smt::currentResourceManager(); - d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - nullptr, - rm)); + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + nullptr, + rm)); d_satSolverNotify.reset( d_emptyNotify ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index d64749d6b..ae79e1517 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -146,11 +146,11 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_cnfContext = new context::Context(); d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine); ResourceManager* rm = d_smt->getResourceManager(); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, - d_cnfRegistrar, - d_cnfContext, - &d_smt->getOutputManager(), - rm); + d_cnfStream = new CVC4::prop::CnfStream(d_satSolver, + d_cnfRegistrar, + d_cnfContext, + &d_smt->getOutputManager(), + rm); } void tearDown() override |