summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cnf_stream.cpp143
-rw-r--r--src/prop/cnf_stream.h24
2 files changed, 92 insertions, 75 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index fd30cd997..c8d86c73d 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Tim King
** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway
+ ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -61,8 +61,8 @@ TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, c
CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
}
-void CnfStream::assertClause(TNode node, SatClause& c) {
- Debug("cnf") << "Inserting into stream " << c << endl;
+void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
+ Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl;
if(Dump.isOn("clauses")) {
if(c.size() == 1) {
Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
@@ -76,28 +76,31 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
Dump("clauses") << AssertCommand(Expr(n.toExpr()));
}
}
+ //store map between clause and original formula
+ PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); );
d_satSolver->addClause(c, d_removable, d_proofId);
+ PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); );
}
-void CnfStream::assertClause(TNode node, SatLiteral a) {
+void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) {
SatClause clause(1);
clause[0] = a;
- assertClause(node, clause);
+ assertClause(node, clause, proof_id);
}
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id) {
SatClause clause(2);
clause[0] = a;
clause[1] = b;
- assertClause(node, clause);
+ assertClause(node, clause, proof_id);
}
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id) {
SatClause clause(3);
clause[0] = a;
clause[1] = b;
clause[2] = c;
- assertClause(node, clause);
+ assertClause(node, clause, proof_id);
}
bool CnfStream::hasLiteral(TNode n) const {
@@ -260,10 +263,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
SatLiteral xorLit = newLiteral(xorNode);
- assertClause(xorNode, a, b, ~xorLit);
- assertClause(xorNode, ~a, ~b, ~xorLit);
- assertClause(xorNode, a, ~b, xorLit);
- assertClause(xorNode, ~a, b, xorLit);
+ assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN);
+ assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN);
+ assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN);
+ assertClause(xorNode, ~a, b, xorLit, RULE_TSEITIN);
return xorLit;
}
@@ -292,14 +295,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
// lit | ~(a_1 | a_2 | a_3 | ... | a_n)
// (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
for(unsigned i = 0; i < n_children; ++i) {
- assertClause(orNode, orLit, ~clause[i]);
+ assertClause(orNode, orLit, ~clause[i], RULE_TSEITIN);
}
// lit -> (a_1 | a_2 | a_3 | ... | a_n)
// ~lit | a_1 | a_2 | a_3 | ... | a_n
clause[n_children] = ~orLit;
// This needs to go last, as the clause might get modified by the SAT solver
- assertClause(orNode, clause);
+ assertClause(orNode.negate(), clause, RULE_TSEITIN);
// Return the literal
return orLit;
@@ -329,7 +332,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
// ~lit | (a_1 & a_2 & a_3 & ... & a_n)
// (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
for(unsigned i = 0; i < n_children; ++i) {
- assertClause(andNode, ~andLit, ~clause[i]);
+ assertClause(andNode.negate(), ~andLit, ~clause[i], RULE_TSEITIN);
}
// lit <- (a_1 & a_2 & a_3 & ... a_n)
@@ -337,7 +340,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
// lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
clause[n_children] = andLit;
// This needs to go last, as the clause might get modified by the SAT solver
- assertClause(andNode, clause);
+ assertClause(andNode, clause, RULE_TSEITIN);
return andLit;
}
@@ -356,13 +359,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
// lit -> (a->b)
// ~lit | ~ a | b
- assertClause(impliesNode, ~impliesLit, ~a, b);
+ assertClause(impliesNode.negate(), ~impliesLit, ~a, b, RULE_TSEITIN);
// (a->b) -> lit
// ~(~a | b) | lit
// (a | l) & (~b | l)
- assertClause(impliesNode, a, impliesLit);
- assertClause(impliesNode, ~b, impliesLit);
+ assertClause(impliesNode, a, impliesLit, RULE_TSEITIN);
+ assertClause(impliesNode, ~b, impliesLit, RULE_TSEITIN);
return impliesLit;
}
@@ -385,16 +388,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
// lit -> ((a-> b) & (b->a))
// ~lit | ((~a | b) & (~b | a))
// (~a | b | ~lit) & (~b | a | ~lit)
- assertClause(iffNode, ~a, b, ~iffLit);
- assertClause(iffNode, a, ~b, ~iffLit);
+ assertClause(iffNode.negate(), ~a, b, ~iffLit, RULE_TSEITIN);
+ assertClause(iffNode.negate(), a, ~b, ~iffLit, RULE_TSEITIN);
// (a<->b) -> lit
// ~((a & b) | (~a & ~b)) | lit
// (~(a & b)) & (~(~a & ~b)) | lit
// ((~a | ~b) & (a | b)) | lit
// (~a | ~b | lit) & (a | b | lit)
- assertClause(iffNode, ~a, ~b, iffLit);
- assertClause(iffNode, a, b, iffLit);
+ assertClause(iffNode, ~a, ~b, iffLit, RULE_TSEITIN);
+ assertClause(iffNode, a, b, iffLit, RULE_TSEITIN);
return iffLit;
}
@@ -429,9 +432,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
// lit -> (t | e) & (b -> t) & (!b -> e)
// lit -> (t | e) & (!b | t) & (b | e)
// (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
- assertClause(iteNode, ~iteLit, thenLit, elseLit);
- assertClause(iteNode, ~iteLit, ~condLit, thenLit);
- assertClause(iteNode, ~iteLit, condLit, elseLit);
+ assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit, RULE_TSEITIN);
+ assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit, RULE_TSEITIN);
+ assertClause(iteNode.negate(), ~iteLit, condLit, elseLit, RULE_TSEITIN);
// If ITE is false then one of the branches is false and the condition
// implies which one
@@ -439,9 +442,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
// !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
// !lit -> (!t | !e) & (!b | !t) & (b | !e)
// (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
- assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
- assertClause(iteNode, iteLit, ~condLit, ~thenLit);
- assertClause(iteNode, iteLit, condLit, ~elseLit);
+ assertClause(iteNode, iteLit, ~thenLit, ~elseLit, RULE_TSEITIN);
+ assertClause(iteNode, iteLit, ~condLit, ~thenLit, RULE_TSEITIN);
+ assertClause(iteNode, iteLit, condLit, ~elseLit, RULE_TSEITIN);
return iteLit;
}
@@ -506,13 +509,14 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
else return ~nodeLit;
}
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id) {
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, false);
+ PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).toExpr(), node.toExpr() ) );
+ convertAndAssert(*conjunct, false, proof_id);
}
} else {
// If the node is a disjunction, we construct a clause and assert it
@@ -524,11 +528,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
clause[i] = toCNF(*disjunct, true);
}
Assert(disjunct == node.end());
- assertClause(node, clause);
+ assertClause(node.negate(), clause, proof_id);
}
}
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule proof_id) {
Assert(node.getKind() == OR);
if (!negated) {
// If the node is a disjunction, we construct a clause and assert it
@@ -540,17 +544,18 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
clause[i] = toCNF(*disjunct, false);
}
Assert(disjunct == node.end());
- assertClause(node, clause);
+ assertClause(node, clause, proof_id);
} else {
// 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, true);
+ PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).negate().toExpr(), node.negate().toExpr() ) );
+ convertAndAssert(*conjunct, true, proof_id);
}
}
}
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) {
if (!negated) {
// p XOR q
SatLiteral p = toCNF(node[0], false);
@@ -559,11 +564,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
SatClause clause1(2);
clause1[0] = ~p;
clause1[1] = ~q;
- assertClause(node, clause1);
+ assertClause(node, clause1, proof_id);
SatClause clause2(2);
clause2[0] = p;
clause2[1] = q;
- assertClause(node, clause2);
+ assertClause(node, clause2, proof_id);
} else {
// !(p XOR q) is the same as p <=> q
SatLiteral p = toCNF(node[0], false);
@@ -572,15 +577,15 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
SatClause clause1(2);
clause1[0] = ~p;
clause1[1] = q;
- assertClause(node, clause1);
+ assertClause(node.negate(), clause1, proof_id);
SatClause clause2(2);
clause2[0] = p;
clause2[1] = ~q;
- assertClause(node, clause2);
+ assertClause(node.negate(), clause2, proof_id);
}
}
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule proof_id) {
if (!negated) {
// p <=> q
SatLiteral p = toCNF(node[0], false);
@@ -589,11 +594,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
SatClause clause1(2);
clause1[0] = ~p;
clause1[1] = q;
- assertClause(node, clause1);
+ assertClause(node, clause1, proof_id);
SatClause clause2(2);
clause2[0] = p;
clause2[1] = ~q;
- assertClause(node, clause2);
+ assertClause(node, clause2, proof_id);
} else {
// !(p <=> q) is the same as p XOR q
SatLiteral p = toCNF(node[0], false);
@@ -602,15 +607,15 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
SatClause clause1(2);
clause1[0] = ~p;
clause1[1] = ~q;
- assertClause(node, clause1);
+ assertClause(node.negate(), clause1, proof_id);
SatClause clause2(2);
clause2[0] = p;
clause2[1] = q;
- assertClause(node, clause2);
+ assertClause(node.negate(), clause2, proof_id);
}
}
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id) {
if (!negated) {
// p => q
SatLiteral p = toCNF(node[0], false);
@@ -619,29 +624,35 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
SatClause clause(2);
clause[0] = ~p;
clause[1] = q;
- assertClause(node, clause);
+ assertClause(node, clause, proof_id);
} else {// Construct the
+ PROOF(ProofManager::currentPM()->setCnfDep( node[0].toExpr(), node.negate().toExpr() ) );
+ PROOF(ProofManager::currentPM()->setCnfDep( node[1].negate().toExpr(), node.negate().toExpr() ) );
// !(p => q) is the same as (p && ~q)
- convertAndAssert(node[0], false);
- convertAndAssert(node[1], true);
+ convertAndAssert(node[0], false, proof_id);
+ convertAndAssert(node[1], true, proof_id);
}
}
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule proof_id) {
// 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)
+ Node nnode = node;
+ if( negated ){
+ nnode = node.negate();
+ }
SatClause clause1(2);
clause1[0] = ~p;
clause1[1] = q;
- assertClause(node, clause1);
+ assertClause(nnode, clause1, proof_id);
SatClause clause2(2);
clause2[0] = p;
clause2[1] = r;
- assertClause(node, clause2);
+ assertClause(nnode, clause2, proof_id);
}
// At the top level we must ensure that all clauses that are asserted are
@@ -661,10 +672,10 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
// We aren't producing proofs or unsat cores; use an invalid proof id.
d_proofId = uint64_t(-1);
}
- convertAndAssert(node, negated);
+ convertAndAssert(node, negated, proof_id);
}
-void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id) {
Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
@@ -675,29 +686,35 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
switch(node.getKind()) {
case AND:
- convertAndAssertAnd(node, negated);
+ convertAndAssertAnd(node, negated, proof_id);
break;
case OR:
- convertAndAssertOr(node, negated);
+ convertAndAssertOr(node, negated, proof_id);
break;
case IFF:
- convertAndAssertIff(node, negated);
+ convertAndAssertIff(node, negated, proof_id);
break;
case XOR:
- convertAndAssertXor(node, negated);
+ convertAndAssertXor(node, negated, proof_id);
break;
case IMPLIES:
- convertAndAssertImplies(node, negated);
+ convertAndAssertImplies(node, negated, proof_id);
break;
case ITE:
- convertAndAssertIte(node, negated);
+ convertAndAssertIte(node, negated, proof_id);
break;
case NOT:
- convertAndAssert(node[0], !negated);
+ convertAndAssert(node[0], !negated, proof_id);
break;
default:
+ {
+ Node nnode = node;
+ if( negated ){
+ nnode = node.negate();
+ }
// Atoms
- assertClause(node, toCNF(node, negated));
+ assertClause(nnode, toCNF(node, negated), proof_id);
+ }
break;
}
}
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b22290ae4..d5d01d126 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Tim King
** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway
+ ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -133,14 +133,14 @@ protected:
* @param node the node giving rise to this clause
* @param clause the clause to assert
*/
- void assertClause(TNode node, SatClause& clause);
+ void assertClause(TNode node, SatClause& clause, ProofRule proof_id);
/**
* 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
*/
- void assertClause(TNode node, SatLiteral a);
+ void assertClause(TNode node, SatLiteral a, ProofRule proof_id);
/**
* Asserts the binary clause to the sat solver.
@@ -148,7 +148,7 @@ protected:
* @param a the first literal in the clause
* @param b the second literal in the clause
*/
- void assertClause(TNode node, SatLiteral a, SatLiteral b);
+ void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id);
/**
* Asserts the ternary clause to the sat solver.
@@ -157,7 +157,7 @@ protected:
* @param b the second literal in the clause
* @param c the thirs literal in the clause
*/
- void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
+ void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id);
/**
* Acquires a new variable from the SAT solver to represent the node
@@ -298,7 +298,7 @@ private:
/**
* Same as above, except that removable is remembered.
*/
- void convertAndAssert(TNode node, bool negated);
+ void convertAndAssert(TNode node, bool negated, ProofRule proof_id);
// Each of these formulas handles takes care of a Node of each Kind.
//
@@ -318,12 +318,12 @@ private:
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);
+ void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id);
+ void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id);
+ void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id);
+ void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id);
+ void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id);
+ void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id);
/**
* Transforms the node into CNF recursively.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback