summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r--src/prop/cnf_stream.cpp59
1 files changed, 29 insertions, 30 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 36df53ca3..629e44e3e 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -46,9 +46,7 @@ CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar)
}
void CnfStream::recordTranslation(TNode node) {
- if (d_assertingLemma) {
- d_lemmas.push_back(stripNot(node));
- } else {
+ if (!d_removable) {
d_translationTrail.push_back(stripNot(node));
}
}
@@ -59,7 +57,7 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registr
void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
- d_satSolver->addClause(c, d_assertingLemma);
+ d_satSolver->addClause(c, d_removable);
}
void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -123,9 +121,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
// If a theory literal, we pre-register it
if (theoryLiteral) {
- bool backup = d_assertingLemma;
+ bool backup = d_removable;
d_registrar.preRegister(node);
- d_assertingLemma = backup;
+ d_removable = backup;
}
// Here, you can have it
@@ -372,10 +370,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
// If the non-negated node has already been translated, get the translation
if(isTranslated(node)) {
nodeLit = getLiteral(node);
- // If we are asserting a lemma, we need to take the whole tree to level 0
- if (d_assertingLemma) {
- moveToBaseLevel(node);
- }
} else {
// Handle each Boolean operator case
switch(node.getKind()) {
@@ -425,13 +419,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
else return ~nodeLit;
}
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, 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, false);
+ convertAndAssert(*conjunct, false);
}
} else {
// If the node is a disjunction, we construct a clause and assert it
@@ -448,7 +442,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated)
}
}
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
Assert(node.getKind() == OR);
if (!negated) {
// If the node is a disjunction, we construct a clause and assert it
@@ -466,12 +460,12 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool 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, true);
+ convertAndAssert(*conjunct, true);
}
}
}
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
if (!negated) {
// p XOR q
SatLiteral p = toCNF(node[0], false);
@@ -503,7 +497,7 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated)
recordTranslation(node[1]);
}
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
if (!negated) {
// p <=> q
SatLiteral p = toCNF(node[0], false);
@@ -535,7 +529,7 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated)
recordTranslation(node[1]);
}
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
if (!negated) {
// p => q
SatLiteral p = toCNF(node[0], false);
@@ -549,12 +543,12 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega
recordTranslation(node[1]);
} else {// Construct the
// !(p => q) is the same as (p && ~q)
- convertAndAssert(node[0], lemma, false);
- convertAndAssert(node[1], lemma, true);
+ convertAndAssert(node[0], false);
+ convertAndAssert(node[1], true);
}
}
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
// ITE(p, q, r)
SatLiteral p = toCNF(node[0], false);
SatLiteral q = toCNF(node[1], negated);
@@ -578,30 +572,35 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, 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 lemma, bool negated) {
- Debug("cnf") << "convertAndAssert(" << node << ", lemma = " << lemma << ", negated = " << (negated ? "true" : "false") << ")" << endl;
- d_assertingLemma = lemma;
+void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+ Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+ d_removable = removable;
+ convertAndAssert(node, negated);
+}
+
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+ Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
switch(node.getKind()) {
case AND:
- convertAndAssertAnd(node, lemma, negated);
+ convertAndAssertAnd(node, negated);
break;
case OR:
- convertAndAssertOr(node, lemma, negated);
+ convertAndAssertOr(node, negated);
break;
case IFF:
- convertAndAssertIff(node, lemma, negated);
+ convertAndAssertIff(node, negated);
break;
case XOR:
- convertAndAssertXor(node, lemma, negated);
+ convertAndAssertXor(node, negated);
break;
case IMPLIES:
- convertAndAssertImplies(node, lemma, negated);
+ convertAndAssertImplies(node, negated);
break;
case ITE:
- convertAndAssertIte(node, lemma, negated);
+ convertAndAssertIte(node, negated);
break;
case NOT:
- convertAndAssert(node[0], lemma, !negated);
+ convertAndAssert(node[0], !negated);
break;
default:
// Atoms
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback