#include "theory/theory.h"
#include "theory/theory_engine.h"
-using namespace std;
-using namespace CVC4::kind;
-
namespace CVC4 {
namespace prop {
Registrar* registrar,
context::Context* context,
OutputManager* outMgr,
+ ResourceManager* rm,
bool fullLitToNodeMap,
std::string name)
: d_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();
}
}
- 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 {
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)){
}
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);
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) {
}
SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
- Debug("cnf") << "convertAtom(" << node << ")" << endl;
+ Trace("cnf") << "convertAtom(" << node << ")\n";
Assert(!hasLiteral(node)) << "atom already mapped!";
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;
<< "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]);
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();
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();
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]);
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]);
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]);
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();
}
}
-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();
}
}
-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);
}
}
-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);
}
}
-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);
}
}
-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();
// 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)
}
}
-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);
++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;
}
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:
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;
/** 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
* 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.
* @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
*/
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 */
projects / cvc5.git / commitdiff