summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/cnf_stream.cpp253
-rw-r--r--src/prop/cnf_stream.h17
-rw-r--r--src/prop/prop_engine.cpp4
-rw-r--r--test/unit/prop/cnf_stream_black.h24
4 files changed, 237 insertions, 61 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 350b6f5cf..225f95d54 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -326,66 +326,233 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
}
-SatLiteral TseitinCnfStream::toCNF(TNode node) {
- Debug("cnf") << "toCNF(" << node << ")" << endl;
+SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
+ Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
- // If the node has already been translated, return the previous translation
- if(isCached(node)) {
- return lookupInCache(node);
- }
+ SatLiteral nodeLit;
+ Node negatedNode = node.notNode();
- // Handle each Boolean operator case
- switch(node.getKind()) {
- case NOT:
- return handleNot(node);
- case XOR:
- return handleXor(node);
- case ITE:
- return handleIte(node);
- case IFF:
- return handleIff(node);
- case IMPLIES:
- return handleImplies(node);
- case OR:
- return handleOr(node);
- case AND:
- return handleAnd(node);
- default:
- {
- //TODO make sure this does not contain any boolean substructure
- return handleAtom(node);
- //Unreachable();
- //Node atomic = handleNonAtomicNode(node);
- //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+ // If the non-negated node has already been translated, get the translation
+ if(isCached(node)) {
+ nodeLit = lookupInCache(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 IFF:
+ nodeLit = handleIff(node);
+ break;
+ case IMPLIES:
+ nodeLit = handleImplies(node);
+ break;
+ case OR:
+ nodeLit = handleOr(node);
+ break;
+ case AND:
+ nodeLit = handleAnd(node);
+ break;
+ default:
+ {
+ //TODO make sure this does not contain any boolean substructure
+ nodeLit = handleAtom(node);
+ //Unreachable();
+ //Node atomic = handleNonAtomicNode(node);
+ //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+ }
}
}
+
+ // Return the appropriate (negated) literal
+ if (!negated) return nodeLit;
+ else return ~nodeLit;
}
-void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) {
- Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
- d_assertingLemma = lemma;
- if(node.getKind() == AND) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
+ Assert(node.getKind() == AND);
+ if (!negated) {
// If the node is a conjunction, we handle each conjunct separately
- for( TNode::const_iterator conjunct = node.begin(),
- node_end = node.end();
- conjunct != node_end;
- ++conjunct ) {
- convertAndAssert(*conjunct, lemma);
+ for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
+ conjunct != node_end; ++conjunct ) {
+ convertAndAssert(*conjunct, lemma, false);
+ }
+ } else {
+ // If the node is a disjunction, we construct a clause and assert it
+ int nChildren = node.getNumChildren();
+ SatClause clause(nChildren);
+ TNode::const_iterator disjunct = node.begin();
+ for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
+ Assert( disjunct != node.end() );
+ clause[i] = toCNF(*disjunct, true);
}
- } else if(node.getKind() == OR) {
+ Assert(disjunct == node.end());
+ assertClause(node, clause);
+ }
+}
+
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
+ Assert(node.getKind() == OR);
+ if (!negated) {
// If the node is a disjunction, we construct a clause and assert it
int nChildren = node.getNumChildren();
SatClause clause(nChildren);
TNode::const_iterator disjunct = node.begin();
for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
Assert( disjunct != node.end() );
- clause[i] = toCNF(*disjunct);
+ clause[i] = toCNF(*disjunct, false);
}
- Assert( disjunct == node.end() );
+ Assert(disjunct == node.end());
assertClause(node, clause);
} else {
- // Otherwise, we just convert using the definitional transformation
- assertClause(node, toCNF(node));
+ // If the node is a conjunction, we handle each conjunct separately
+ for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
+ conjunct != node_end; ++conjunct ) {
+ convertAndAssert(*conjunct, lemma, true);
+ }
+ }
+}
+
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
+ if (!negated) {
+ // p XOR q
+ SatLiteral p = toCNF(node[0], false);
+ SatLiteral q = toCNF(node[1], false);
+ // Construct the clauses (p => !q) and (!q => p)
+ SatClause clause1(2);
+ clause1[0] = ~p;
+ clause1[1] = ~q;
+ assertClause(node, clause1);
+ SatClause clause2(2);
+ clause2[0] = p;
+ clause2[1] = q;
+ assertClause(node, clause2);
+ } else {
+ // !(p XOR q) is the same as p <=> q
+ SatLiteral p = toCNF(node[0], false);
+ SatLiteral q = toCNF(node[1], false);
+ // Construct the clauses (p => q) and (q => p)
+ SatClause clause1(2);
+ clause1[0] = ~p;
+ clause1[1] = q;
+ assertClause(node, clause1);
+ SatClause clause2(2);
+ clause2[0] = p;
+ clause2[1] = ~q;
+ assertClause(node, clause2);
+ }
+}
+
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
+ if (!negated) {
+ // p <=> q
+ SatLiteral p = toCNF(node[0], false);
+ SatLiteral q = toCNF(node[1], false);
+ // Construct the clauses (p => q) and (q => p)
+ SatClause clause1(2);
+ clause1[0] = ~p;
+ clause1[1] = q;
+ assertClause(node, clause1);
+ SatClause clause2(2);
+ clause2[0] = p;
+ clause2[1] = ~q;
+ assertClause(node, clause2);
+ } else {
+ // !(p <=> q) is the same as p XOR q
+ SatLiteral p = toCNF(node[0], false);
+ SatLiteral q = toCNF(node[1], false);
+ // Construct the clauses (p => !q) and (!q => p)
+ SatClause clause1(2);
+ clause1[0] = ~p;
+ clause1[1] = ~q;
+ assertClause(node, clause1);
+ SatClause clause2(2);
+ clause2[0] = p;
+ clause2[1] = q;
+ assertClause(node, clause2);
+ }
+}
+
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
+ if (!negated) {
+ // p => q
+ SatLiteral p = toCNF(node[0], false);
+ SatLiteral q = toCNF(node[1], false);
+ // Construct the clause ~p || q
+ SatClause clause(2);
+ clause[0] = ~p;
+ clause[1] = q;
+ assertClause(node, clause);
+ } else {// Construct the
+ // !(p => q) is the same as (p && ~q)
+ convertAndAssert(node[0], lemma, false);
+ convertAndAssert(node[1], lemma, true);
+ }
+}
+
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
+ // 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) and (!q => !p) and (!r => p)
+ SatClause clause1(2);
+ clause1[0] = ~p;
+ clause1[1] = q;
+ assertClause(node, clause1);
+ SatClause clause2(2);
+ clause2[0] = p;
+ clause2[1] = r;
+ assertClause(node, clause2);
+ SatClause clause3(2);
+ clause3[0] = q;
+ clause3[1] = ~p;
+ assertClause(node, clause3);
+ SatClause clause4(2);
+ clause4[0] = r;
+ clause4[1] = p;
+ assertClause(node, clause4);
+}
+
+// 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 lemma, bool negated) {
+ Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+ d_assertingLemma = lemma;
+ switch(node.getKind()) {
+ case AND:
+ convertAndAssertAnd(node, lemma, negated);
+ break;
+ case OR:
+ convertAndAssertOr(node, lemma, negated);
+ break;
+ case IFF:
+ convertAndAssertIff(node, lemma, negated);
+ break;
+ case XOR:
+ convertAndAssertXor(node, lemma, negated);
+ break;
+ case IMPLIES:
+ convertAndAssertImplies(node, lemma, negated);
+ break;
+ case ITE:
+ convertAndAssertIte(node, lemma, negated);
+ break;
+ case NOT:
+ convertAndAssert(node[0], lemma, !negated);
+ break;
+ default:
+ // Atoms
+ assertClause(node, toCNF(node, negated));
+ break;
}
}
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a574adf23..ce6c7eb1e 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -144,9 +144,10 @@ public:
/**
* Converts and asserts a formula.
* @param node node to convert and assert
- * @param whether the sat solver can choose to remove this clause
+ * @param whether the sat solver can choose to remove the clauses
+ * @param negated wheather we are asserting the node negated
*/
- virtual void convertAndAssert(TNode node, bool lemma = false) = 0;
+ virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0;
/**
* Get the node that is represented by the given SatLiteral.
@@ -185,8 +186,9 @@ public:
* Convert a given formula to CNF and assert it to the SAT solver.
* @param node the formula to assert
* @param lemma is this a lemma that is erasable
+ * @param negated true if negated
*/
- void convertAndAssert(TNode node, bool lemma);
+ void convertAndAssert(TNode node, bool lemma, bool negated = false);
/**
* Constructs the stream to use the given sat solver.
@@ -215,13 +217,20 @@ private:
SatLiteral handleAnd(TNode node);
SatLiteral handleOr(TNode node);
+ void convertAndAssertAnd(TNode node, bool lemma, bool negated);
+ void convertAndAssertOr(TNode node, bool lemma, bool negated);
+ void convertAndAssertXor(TNode node, bool lemma, bool negated);
+ void convertAndAssertIff(TNode node, bool lemma, bool negated);
+ void convertAndAssertImplies(TNode node, bool lemma, bool negated);
+ void convertAndAssertIte(TNode node, bool lemma, bool negated);
/**
* Transforms the node into CNF recursively.
* @param node the formula to transform
+ * @param negated wheather the literal is negated
* @return the literal representing the root of the formula
*/
- SatLiteral toCNF(TNode node);
+ SatLiteral toCNF(TNode node, bool negated = false);
}; /* class TseitinCnfStream */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b9fbd3ce6..16881f9e4 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -77,14 +77,14 @@ void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as non-removable
- d_cnfStream->convertAndAssert(node);
+ d_cnfStream->convertAndAssert(node, false, false);
}
void PropEngine::assertLemma(TNode node) {
Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as removable
- d_cnfStream->convertAndAssert(node);
+ d_cnfStream->convertAndAssert(node, false, false);
}
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 9c8560783..bbae46df7 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -104,7 +104,7 @@ void testAnd() {
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::AND, a, b, c) );
+ d_nodeManager->mkNode(kind::AND, a, b, c), false);
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -125,13 +125,13 @@ void testComplexExpr() {
d_nodeManager->mkNode(kind::OR, c, d),
d_nodeManager->mkNode(
kind::NOT,
- d_nodeManager->mkNode(kind::XOR, e, f)))) );
+ d_nodeManager->mkNode(kind::XOR, e, f)))), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
void testFalse() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false) );
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -140,7 +140,7 @@ void testIff() {
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IFF, a, b) );
+ d_nodeManager->mkNode(kind::IFF, a, b), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -149,7 +149,7 @@ void testImplies() {
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IMPLIES, a, b) );
+ d_nodeManager->mkNode(kind::IMPLIES, a, b), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -165,7 +165,7 @@ void testIte() {
d_nodeManager->mkVar(d_nodeManager->integerType())
),
d_nodeManager->mkVar(d_nodeManager->integerType())
- ));
+ ), false);
}
@@ -173,7 +173,7 @@ void testNot() {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::NOT, a) );
+ d_nodeManager->mkNode(kind::NOT, a), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -183,13 +183,13 @@ void testOr() {
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::OR, a, b, c) );
+ d_nodeManager->mkNode(kind::OR, a, b, c), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
void testTrue() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) );
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -197,10 +197,10 @@ void testVar() {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(a);
+ d_cnfStream->convertAndAssert(a, false);
TS_ASSERT( d_satSolver->addClauseCalled() );
d_satSolver->reset();
- d_cnfStream->convertAndAssert(b);
+ d_cnfStream->convertAndAssert(b, false);
TS_ASSERT( d_satSolver->addClauseCalled() );
}
@@ -209,7 +209,7 @@ void testXor() {
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::XOR, a, b) );
+ d_nodeManager->mkNode(kind::XOR, a, b), false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback