diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /src/prop | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 143 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 24 |
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. |