diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /src/proof | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 16 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 9 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 192 | ||||
-rw-r--r-- | src/proof/array_proof.h | 42 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 568 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 42 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 137 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 43 | ||||
-rw-r--r-- | src/proof/lemma_proof.cpp | 193 | ||||
-rw-r--r-- | src/proof/lemma_proof.h | 79 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 209 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 48 | ||||
-rw-r--r-- | src/proof/proof_output_channel.cpp | 82 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 50 | ||||
-rw-r--r-- | src/proof/proof_utils.cpp | 52 | ||||
-rw-r--r-- | src/proof/proof_utils.h | 105 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 410 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 635 | ||||
-rw-r--r-- | src/proof/skolemization_manager.h | 1 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 748 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 157 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 119 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 10 |
23 files changed, 2909 insertions, 1038 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index a1287b667..4864cbf46 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -69,18 +69,18 @@ inline static bool match(TNode n1, TNode n2) { void ProofArith::toStream(std::ostream& out) { Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl; //AJR : carry this further? - LetMap map; + ProofLetMap map; toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map); } -void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) { +void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) { Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl; pf->debug_print("lfsc-arith"); Debug("lfsc-arith") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); } -Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) { +Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) { Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; pf->debug_print("pf::arith"); Debug("pf::arith") << std::endl; @@ -643,7 +643,7 @@ void ArithProof::registerTerm(Expr term) { } } -void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind() << ". Type: " << term.getType() << ". Number of children: " << term.getNumChildren() << std::endl; @@ -810,14 +810,14 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) { } } -void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { +void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { os << " ;; Arith Theory Lemma \n;;"; for (unsigned i = 0; i < lemma.size(); ++i) { os << lemma[i] <<" "; } os <<"\n"; //os << " (clausify_false trust)"; - ArithProof::printTheoryLemmaProof( lemma, os, paren ); + ArithProof::printTheoryLemmaProof(lemma, os, paren, map); } void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { @@ -830,4 +830,8 @@ void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& p // Nothing to do here at this point. } +void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* CVC4 namespace */ diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 788e4bd86..d980654c4 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -29,13 +29,13 @@ namespace CVC4 { //proof object outputted by TheoryArith class ProofArith : public Proof { private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map); + static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); public: ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {} //it is simply an equality engine proof theory::eq::EqProof * d_proof; void toStream(std::ostream& out); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map); + static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); }; @@ -68,12 +68,13 @@ public: LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) : ArithProof(arith, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 8aba8dce9..484bc70c8 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -81,27 +81,45 @@ inline static bool match(TNode n1, TNode n2) { void ProofArray::setRowMergeTag(unsigned tag) { d_reasonRow = tag; + d_proofPrinter.d_row = tag; } void ProofArray::setRow1MergeTag(unsigned tag) { d_reasonRow1 = tag; + d_proofPrinter.d_row1 = tag; } void ProofArray::setExtMergeTag(unsigned tag) { d_reasonExt = tag; + d_proofPrinter.d_ext = tag; +} + +unsigned ProofArray::getRowMergeTag() const { + return d_reasonRow; +} + +unsigned ProofArray::getRow1MergeTag() const { + return d_reasonRow1; +} + +unsigned ProofArray::getExtMergeTag() const { + return d_reasonExt; } void ProofArray::toStream(std::ostream& out) { + ProofLetMap map; + toStream(out, map); +} + +void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) { Trace("pf::array") << "; Print Array proof..." << std::endl; - //AJR : carry this further? - LetMap map; toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map); Debug("pf::array") << "; Print Array proof done!" << std::endl; } -void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) { +void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map) { Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; @@ -111,10 +129,10 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, unsigned tb, - const LetMap& map) { + const ProofLetMap& map) { Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; if(tb == 0) { @@ -150,7 +168,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf->d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::array"); + pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter); congruenceClosures.push_back(pf->d_children[i+count]); } @@ -220,48 +238,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ++i; } } - Assert(neg >= 0); + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) { + Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + Assert(pf->d_node.getNumChildren() == 2); + Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + } Node n1; std::stringstream ss, ss2; //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + if(!disequalityFound || pf->d_children.size() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - Debug("mgdx") << "\nhave proven: " << n1 << std::endl; - Debug("mgdx") << "n2 is " << n2 << std::endl; - Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; - Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; + out << "(clausify_false (contra _ "; - if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } + if (disequalityFound) { + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("mgdx") << "\nhave proven: " << n1 << std::endl; + Debug("mgdx") << "n2 is " << n2 << std::endl; + Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; + Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; - if (pf->d_children[neg]->d_id == d_reasonExt) { - // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. - - // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6 - - out << "(clausify_false (contra _ "; - out << ss.str(); + if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); - - out << " "; - out << ss2.str(); - out << "))"; - - } else { - // The negative node is, e.g., a pure equality - out << "(clausify_false (contra _ "; - - if(n2[0].getKind() == kind::APPLY_UF) { + if ((pf->d_children[neg]->d_id == d_reasonExt) || + (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) { + // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. + out << ss.str(); + out << " "; + toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + out << ss2.str(); + } else if (n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; out << "(symm _ _ _ "; out << ss.str(); @@ -276,16 +294,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " << ProofManager::getLitName(n2[0]) << std::endl; - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << " " << ProofManager::getLitName(n2[0]); } + } else { + Node n2 = pf->d_node; + Assert(n2.getKind() == kind::EQUAL); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + + out << ss.str(); + out << " "; + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n1[0].toExpr(), + n1[1].toExpr()); } + out << "))" << std::endl; return Node(); } if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); std::stack<const theory::eq::EqProof*> stk; for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { Assert(!pf2->d_node.isNull()); @@ -315,7 +344,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd"); + pf2->debug_print("mgd", 0, &d_proofPrinter); // Temp Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl; Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl; @@ -332,7 +361,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "SIDE IS 1\n"; if(!match(pf2->d_node, n1[1])) { Debug("mgd") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("mgd"); + pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -546,6 +575,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf->d_node; } + else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::NOT); + Node n = pf->d_node[0]; + Assert(n.getKind() == kind::EQUAL); + Assert(n.getNumChildren() == 2); + Assert(n[0].isConst() && n[1].isConst()); + + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n[0].toExpr(), + n[1].toExpr()); + return pf->d_node; + } + else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; @@ -554,7 +597,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf->d_children.size() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); Debug("mgd") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; @@ -772,7 +815,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("mgdx",0); + pf->debug_print("mgdx", 0, &d_proofPrinter); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -931,6 +974,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, t4 = pf->d_children[0]->d_node[0][side][0][2]; ret = pf->d_node; + // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry. + bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; Assert(pf->d_children.size() == 1); @@ -939,28 +985,31 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + if (swap) { + out << "(symm _ _ _ "; + } + out << "(negativerow _ _ "; - tp->printTerm(t1.toExpr(), out, map); + tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); out << " "; - tp->printTerm(t2.toExpr(), out, map); + tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); out << " "; tp->printTerm(t3.toExpr(), out, map); out << " "; tp->printTerm(t4.toExpr(), out, map); out << " "; - - // if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); - // } else { - // Debug("pf::array") << "Need symmetry!" << std::endl; - // out << "(negsymm _ _ _ " << ss.str() << ")"; - // } + if (side != 0) { + out << "(negsymm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } out << ")"; - // Unreachable(); + if (swap) { + out << ") "; + } return ret; } @@ -1071,13 +1120,12 @@ void ArrayProof::registerTerm(Expr term) { } std::string ArrayProof::skolemToLiteral(Expr skolem) { + Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl; Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end()); return d_skolemToLiteral[skolem]; } -void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { - Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl; - +void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY); if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) { @@ -1154,23 +1202,35 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& m void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; Assert (type.isArray() || type.isSort()); - os << type <<" "; + if (type.isArray()){ + ArrayType array_type(type); + + Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: " + << array_type.getIndexType() + << ", element type: " << array_type.getConstituentType() << std::endl; + + os << "(Array "; + printSort(array_type.getIndexType(), os); + os << " "; + printSort(array_type.getConstituentType(), os); + os << ")"; + } else { + os << type <<" "; + } } -void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { +void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { os << " ;; Array Theory Lemma \n;;"; for (unsigned i = 0; i < lemma.size(); ++i) { os << lemma[i] <<" "; } os <<"\n"; //os << " (clausify_false trust)"; - ArrayProof::printTheoryLemmaProof(lemma, os, paren); + ArrayProof::printTheoryLemmaProof(lemma, os, paren, map); } void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { // declaring the sorts - Debug("pf::array") << "Arrays declaring sorts..." << std::endl; - for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { if (!ProofManager::currentPM()->wasPrinted(*it)) { os << "(% " << *it << " sort\n"; @@ -1229,6 +1289,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::array") << "Array: print deferred declarations called" << std::endl; + unsigned count = 1; for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) { Expr term = *it; Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it); @@ -1237,7 +1298,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p << "It is a witness for: " << equality << std::endl; std::ostringstream newSkolemLiteral; - newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); + newSkolemLiteral << ".sl" << count++; std::string skolemLiteral = newSkolemLiteral.str(); d_skolemToLiteral[*it] = skolemLiteral; @@ -1250,14 +1311,13 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p Node array_one = equality[0][0]; Node array_two = equality[0][1]; - LetMap map; - + ProofLetMap map; os << "(ext _ _ "; printTerm(array_one.toExpr(), os, map); os << " "; printTerm(array_two.toExpr(), os, map); os << " (\\ "; - printTerm(*it, os, map); + os << ProofManager::sanitize(*it); os << " (\\ "; os << skolemLiteral.c_str(); os << "\n"; @@ -1266,4 +1326,8 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p } } +void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* CVC4 namespace */ diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index fb25c9433..69e62dbf3 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -30,10 +30,36 @@ namespace CVC4 { //proof object outputted by TheoryARRAY class ProofArray : public Proof { private: + class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter { + public: + ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) { + } + + std::string printTag(unsigned tag) { + if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence"; + if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality"; + if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity"; + if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants"; + if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity"; + + if (tag == d_row) return "Read Over Write"; + if (tag == d_row1) return "Read Over Write (1)"; + if (tag == d_ext) return "Extensionality"; + + std::ostringstream result; + result << tag; + return result.str(); + } + + unsigned d_row; + unsigned d_row1; + unsigned d_ext; + }; + Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, unsigned tb, - const LetMap& map); + const ProofLetMap& map); /** Merge tag for ROW applications */ unsigned d_reasonRow; @@ -41,18 +67,25 @@ private: unsigned d_reasonRow1; /** Merge tag for EXT applications */ unsigned d_reasonExt; + + ArrayProofPrinter d_proofPrinter; public: ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} //it is simply an equality engine proof theory::eq::EqProof *d_proof; void toStream(std::ostream& out); - void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); + void toStream(std::ostream& out, const ProofLetMap& map); + void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map); void registerSkolem(Node equality, Node skolem); void setRowMergeTag(unsigned tag); void setRow1MergeTag(unsigned tag); void setExtMergeTag(unsigned tag); + + unsigned getRowMergeTag() const; + unsigned getRow1MergeTag() const; + unsigned getExtMergeTag() const; }; namespace theory { @@ -85,12 +118,13 @@ public: : ArrayProof(arrays, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index b63782226..f19e45920 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,14 +15,17 @@ **/ -#include "proof/bitvector_proof.h" #include "options/bv_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" #include "proof/clause_id.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_rewrite_rules.h" using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -80,20 +83,40 @@ BVSatProof* BitVectorProof::getSatProof() { } void BitVectorProof::registerTermBB(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl; + if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return; d_seenBBTerms.insert(term); d_bbTerms.push_back(term); + + // If this term gets used in the final proof, we will want to register it. However, + // we don't know this at this point; and when the theory proof engine sees it, if it belongs + // to another theory, it won't register it with this proof. So, we need to tell the + // engine to inform us. + + if (theory::Theory::theoryOf(term) != theory::THEORY_BV) { + Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl; + d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV); + } } void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { + Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl; + Expr def = atom.iffExpr(atom_bb); - d_bbAtoms.insert(std::make_pair(atom, def)); + d_bbAtoms.insert(std::make_pair(atom, def)); registerTerm(atom); + + // Register the atom's terms for bitblasting + registerTermBB(atom[0]); + registerTermBB(atom[1]); } void BitVectorProof::registerTerm(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; + d_usedBB.insert(term); if (Theory::isLeafOf(term, theory::THEORY_BV) && @@ -101,6 +124,11 @@ void BitVectorProof::registerTerm(Expr term) { d_declarations.insert(term); } + Debug("pf::bv") << "Going to register children: " << std::endl; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + Debug("pf::bv") << "\t" << term[i] << std::endl; + } + // don't care about parametric operators for bv? for (unsigned i = 0; i < term.getNumChildren(); ++i) { d_proofEngine->registerTerm(term[i]); @@ -108,6 +136,7 @@ void BitVectorProof::registerTerm(Expr term) { } std::string BitVectorProof::getBBTermName(Expr expr) { + Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl; std::ostringstream os; os << "bt"<< expr.getId(); return os.str(); @@ -122,6 +151,8 @@ void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) { } void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) { + Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl; + std::vector<Expr> expr_confl; for (int i = 0; i < confl.size(); ++i) { prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); @@ -129,6 +160,7 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; expr_confl.push_back(expr_lit); } + Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); Debug("pf::bv") << "Make conflict for " << conflict << std::endl; @@ -144,30 +176,104 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); d_bbConflictMap[conflict] = clause_id; d_resolutionProof->endResChain(clause_id); - Debug("pf::bv") << "BitVectorProof::endBVConflict id"<<clause_id<< " => " << conflict << "\n"; + Debug("pf::bv") << "BitVectorProof::endBVConflict id" <<clause_id<< " => " << conflict << "\n"; d_isAssumptionConflict = false; } void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Debug("pf::bv") << "Construct full proof." << std::endl; d_resolutionProof->constructProof(); return; } - for(unsigned i = 0; i < conflicts.size(); ++i) { + + for (unsigned i = 0; i < conflicts.size(); ++i) { Expr confl = conflicts[i]; - Debug("pf::bv") << "Finalize conflict " << confl << std::endl; - //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); - if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ + Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; + + // Special case: if the conflict has a (true) or a (not false) in it, it is trivial... + bool ignoreConflict = false; + if ((confl.isConst() && confl.getConst<bool>()) || + (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst<bool>())) { + ignoreConflict = true; + } else if (confl.getKind() == kind::OR) { + for (unsigned k = 0; k < confl.getNumChildren(); ++k) { + if ((confl[k].isConst() && confl[k].getConst<bool>()) || + (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst<bool>())) { + ignoreConflict = true; + } + } + } + if (ignoreConflict) { + Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl; + continue; + } + + if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) { ClauseId id = d_bbConflictMap[confl]; d_resolutionProof->collectClauses(id); - }else{ - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; + } else { + // There is no exact match for our conflict, but maybe it is a subset of another conflict + ExprToClauseId::const_iterator it; + bool matchFound = false; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + Expr possibleMatch = it->first; + if (possibleMatch.getKind() != kind::OR) { + // This is a single-node conflict. If this node is in the conflict we're trying to prove, + // we have a match. + for (unsigned k = 0; k < confl.getNumChildren(); ++k) { + if (confl[k] == possibleMatch) { + matchFound = true; + d_resolutionProof->collectClauses(it->second); + break; + } + } + } else { + if (possibleMatch.getNumChildren() > confl.getNumChildren()) + continue; + + unsigned k = 0; + bool matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { + // j is the index in possibleMatch + // k is the index in confl + while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) { + ++k; + } + if (k == confl.getNumChildren()) { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + + if (matching) { + Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl; + d_resolutionProof->collectClauses(it->second); + matchFound = true; + break; + } + } + } + + if (!matchFound) { + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; + } + + Unreachable(); + } } } } -void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: " << Theory::theoryOf(term) << std::endl; @@ -238,17 +344,31 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa printBitOf(term, os, map); return; } - case kind::VARIABLE: + + case kind::VARIABLE: { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + return; + } + case kind::SKOLEM: { - os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; + + // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems, + // like ITE terms. Is there a more elegant way? + + if (ProofManager::getSkolemizationManager()->isSkolem(term)) { + os << ProofManager::sanitize(term); + } else { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + } return; } + default: Unreachable(); } } -void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (term.getKind() == kind::BITVECTOR_BITOF); unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex; Expr var = term[0]; @@ -258,14 +378,7 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m << ", var = " << var << std::endl; os << "(bitof "; - if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) { - // If var is "simple", we can just sanitize and print - os << ProofManager::sanitize(var); - } else { - // If var is "complex", it can belong to another theory. Therefore, dispatch again. - d_proofEngine->printBoundTerm(var, os, map); - } - + os << d_exprToVariableName[var]; os << " " << bit << ")"; } @@ -283,7 +396,7 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { os << paren.str(); } -void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) { std::string op = utils::toLFSCKind(term.getKind()); std::ostringstream paren; std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; @@ -301,7 +414,7 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Le } } -void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; os << " "; @@ -309,7 +422,7 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const L os <<")"; } -void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" "; os << " "; @@ -319,7 +432,7 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMa os <<")"; } -void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; os <<" "; @@ -349,14 +462,16 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl; - Assert (type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec "<<width<<")"; } -void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { +void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { + Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl; Expr conflict = utils::mkSortedExpr(kind::OR, lemma); + Debug("pf::bv") << "\tconflict = " << conflict << std::endl; + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { std::ostringstream lemma_paren; for (unsigned i = 0; i < lemma.size(); ++i) { @@ -377,7 +492,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os // print corresponding literal in bv sat solver prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); os << pm->getAtomName(bb_var, "bb"); - os <<"(\\unit"<<bb_var<<"\n"; + os <<"(\\ unit"<<bb_var<<"\n"; lemma_paren <<")"; } Expr lem = utils::mkOr(lemma); @@ -386,11 +501,134 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); os <<lemma_paren.str(); } else { - Unreachable(); // If we were to reach here, we would crash because BV replay is currently not supported - // in TheoryProof::printTheoryLemmaProof() - Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; - BitVectorProof::printTheoryLemmaProof( lemma, os, paren ); + Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching sub-conflict..." + << std::endl; + + bool matching; + + ExprToClauseId::const_iterator it; + unsigned i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + // Our conflict is sorted, and the records are also sorted. + ++i; + Expr possibleMatch = it->first; + + if (possibleMatch.getKind() != kind::OR) { + // This is a single-node conflict. If this node is in the conflict we're trying to prove, + // we have a match. + matching = false; + + for (unsigned k = 0; k < conflict.getNumChildren(); ++k) { + if (conflict[k] == possibleMatch) { + matching = true; + break; + } + } + } else { + if (possibleMatch.getNumChildren() > conflict.getNumChildren()) + continue; + + unsigned k = 0; + + matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { + // j is the index in possibleMatch + // k is the index in conflict + while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) { + ++k; + } + if (k == conflict.getNumChildren()) { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + } + + if (matching) { + Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl; + // The rest is just a copy of the usual handling, if a precise match is found. + // We only use the literals that appear in the matching conflict, though, and not in the + // original lemma - as these may not have even been bit blasted! + std::ostringstream lemma_paren; + + if (possibleMatch.getKind() == kind::OR) { + for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) { + Expr lit = possibleMatch[i]; + + if (lit.getKind() == kind::NOT) { + os << "(intro_assump_t _ _ _ "; + } else { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren <<")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os <<" "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os <<"(\\ unit"<<bb_var<<"\n"; + lemma_paren <<")"; + } + } else { + // The conflict only consists of one node, either positive or negative. + Expr lit = possibleMatch; + if (lit.getKind() == kind::NOT) { + os << "(intro_assump_t _ _ _ "; + } else { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren <<")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os <<" "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os <<"(\\ unit"<<bb_var<<"\n"; + lemma_paren <<")"; + } + + ClauseId lemma_id = it->second; + d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + os <<lemma_paren.str(); + + return; + } + } + + // We failed to find a matching sub conflict. The last hope is that the + // conflict has a FALSE assertion in it; this can happen in some corner cases, + // where the FALSE is the result of a rewrite. + + for (unsigned i = 0; i < lemma.size(); ++i) { + if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) { + Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; + os << "(clausify_false "; + os << ProofManager::getLitName(lemma[i]); + os << ")"; + return; + } + } + + Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; + } + + Unreachable(); } } @@ -402,7 +640,14 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { - os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n"; + if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) { + d_exprToVariableName[*it] = ProofManager::sanitize(*it); + } else { + std::string newAlias = assignAlias(*it); + d_exprToVariableName[*it] = newAlias; + } + + os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; paren <<")"; } } @@ -411,15 +656,43 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea // Nothing to do here at this point. } +void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Print "trust" statements to bind complex bv variables to their associated terms + + ExprToString::const_iterator it = d_assignedAliases.begin(); + ExprToString::const_iterator end = d_assignedAliases.end(); + + for (; it != end; ++it) { + Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl; + std::stringstream declaration; + declaration << ".fbvd" << d_aliasToBindDeclaration.size(); + d_aliasToBindDeclaration[it->second] = declaration.str(); + + os << "(th_let_pf _ "; + + os << "(trust_f "; + os << "(= (BitVec " << utils::getSize(it->first) << ") "; + os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") "; + ProofLetMap emptyMap; + d_proofEngine->printBoundTerm(it->first, os, emptyMap); + os << ")) "; + os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n"; + paren << "))"; + } + + os << "\n"; +} + void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { // TODO: once we have the operator elimination rules remove those that we // eliminated Assert (term.getType().isBitVector()); Kind kind = term.getKind(); - if (Theory::isLeafOf(term, theory::THEORY_BV) && - !term.isConst()) { - os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )"; + if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) { + // A term is a leaf if it has no children, or if it belongs to another theory + os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term]; + os << " _)"; return; } @@ -448,14 +721,18 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_PLUS : case kind::BITVECTOR_SUB : case kind::BITVECTOR_CONCAT : { - for (unsigned i =0; i < term.getNumChildren() - 1; ++i) { + Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; + + for (int i = term.getNumChildren() - 1; i > 0; --i) { os <<"(bv_bbl_"<< utils::toLFSCKind(kind); + if (kind == kind::BITVECTOR_CONCAT) { - os << " " << utils::getSize(term) <<" _ "; + os << " " << utils::getSize(term) << " _"; } - os <<" _ _ _ _ _ _ "; + os << " _ _ _ _ _ _ "; } - os << getBBTermName(term[0]) <<" "; + + os << getBBTermName(term[0]) << " "; for (unsigned i = 1; i < term.getNumChildren(); ++i) { os << getBBTermName(term[i]); @@ -463,22 +740,25 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } return; } + case kind::BITVECTOR_NEG : case kind::BITVECTOR_NOT : case kind::BITVECTOR_ROTATE_LEFT : case kind::BITVECTOR_ROTATE_RIGHT : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind); - os <<" _ _ _ _ "; + os << "(bv_bbl_"<<utils::toLFSCKind(kind); + os << " _ _ _ _ "; os << getBBTermName(term[0]); - os <<")"; + os << ")"; return; } case kind::BITVECTOR_EXTRACT : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; - os << utils::getSize(term) << " "; + os <<"(bv_bbl_"<<utils::toLFSCKind(kind); + + os << " " << utils::getSize(term) << " "; os << utils::getExtractHigh(term) << " "; os << utils::getExtractLow(term) << " "; os << " _ _ _ _ "; + os << getBBTermName(term[0]); os <<")"; return; @@ -486,8 +766,8 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_REPEAT : case kind::BITVECTOR_ZERO_EXTEND : case kind::BITVECTOR_SIGN_EXTEND : { - os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" "; - os << utils::getSize(term) <<" "; + os << "(bv_bbl_" << utils::toLFSCKind(kind) << " "; + os << utils::getSize(term) << " "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; os << amount; @@ -501,6 +781,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; os << amount; } + os <<" _ _ _ _ "; os << getBBTermName(term[0]); os <<")"; @@ -516,7 +797,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_SHL : case kind::BITVECTOR_LSHR : case kind::BITVECTOR_ASHR : { - // these are terms for which bit-blasting is not supported yet + // these are terms for which bit-blasting is not supported yet std::ostringstream paren; os <<"(trust_bblast_term _ "; paren <<")"; @@ -539,7 +820,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -550,11 +831,19 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { case kind::BITVECTOR_SLE : case kind::BITVECTOR_SGT : case kind::BITVECTOR_SGE : - case kind::EQUAL: - { - os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + case kind::EQUAL: { + Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; + + os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + + if (swap) {os << "_swap";} + os << " _ _ _ _ _ _ "; - os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; + os << getBBTermName(atom[0]); + os << " "; + os << getBBTermName(atom[1]); + os << ")"; + return; } default: @@ -562,19 +851,62 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { } } +void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { + Assert(atom.getKind() == kind::EQUAL); + + os << "(bv_bbl_=_false"; + os << " _ _ _ _ _ _ "; + os << getBBTermName(atom[0]); + + os << " "; + + os << getBBTermName(atom[1]); + + os << ")"; +} void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { // bit-blast terms + { + Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl; + std::vector<Expr>::const_iterator it = d_bbTerms.begin(); + std::vector<Expr>::const_iterator end = d_bbTerms.end(); + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + + for (; it != end; ++it) { + if (d_usedBB.find(*it) == d_usedBB.end()) { + Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; + } else { + Debug("pf::bv") << "\t" << *it << std::endl; + } + } + + Debug("pf::bv") << std::endl; + } + std::vector<Expr>::const_iterator it = d_bbTerms.begin(); std::vector<Expr>::const_iterator end = d_bbTerms.end(); for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end() && options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) continue; - os <<"(decl_bblast _ _ _ "; - printTermBitblasting(*it, os); - os << "(\\ "<< getBBTermName(*it); - paren <<"\n))"; + + // Is this term has an alias, we inject it through the decl_bblast statement + if (hasAlias(*it)) { + os << "(decl_bblast_with_alias _ _ _ _ "; + printTermBitblasting(*it, os); + os << " " << d_aliasToBindDeclaration[d_assignedAliases[*it]] << " "; + os << "(\\ "<< getBBTermName(*it); + os << "\n"; + paren <<"))"; + } else { + os << "(decl_bblast _ _ _ "; + printTermBitblasting(*it, os); + os << "(\\ "<< getBBTermName(*it); + os << "\n"; + paren <<"))"; + } } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -589,7 +921,35 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) bool val = ait->first.getConst<bool>(); os << "(iff_symm " << (val ? "true" : "false" ) << ")"; } else { - printAtomBitblasting(ait->first, os); + Assert(ait->first == ait->second[0]); + + bool swap = false; + if (ait->first.getKind() == kind::EQUAL) { + Expr bitwiseEquivalence = ait->second[1]; + if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst<bool>()) { + printAtomBitblastingToFalse(ait->first, os); + } else { + if (bitwiseEquivalence.getKind() != kind::AND) { + // Just one bit + if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0]); + } + } else { + // Multiple bits + if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0][0]); + } else if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[0] == bitwiseEquivalence[0][1][0]); + } + } + + printAtomBitblasting(ait->first, os, swap); + } + } else { + printAtomBitblasting(ait->first, os, swap); + } } os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; @@ -597,34 +957,102 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) } } -void LFSCBitVectorProof::printResolutionProof(std::ostream& os, - std::ostream& paren) { - // collect the input clauses used +void LFSCBitVectorProof::calculateAtomsInBitblastingProof() { + // Collect the input clauses used IdToSatClause used_lemmas; IdToSatClause used_inputs; - d_resolutionProof->collectClausesUsed(used_inputs, - used_lemmas); - Assert (used_lemmas.empty()); + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); + Assert(used_lemmas.empty()); +} + +const std::set<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() { + return &d_atomsInBitblastingProof; +} +void LFSCBitVectorProof::printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) { // print mapping between theory atoms and internal SAT variables - os << ";; BB atom mapping\n"; + os << std::endl << ";; BB atom mapping\n" << std::endl; - NodeSet atoms; - d_cnfProof->collectAtomsForClauses(used_inputs,atoms); + std::set<Node>::iterator atomIt; + Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; + for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) { + Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; + } + Debug("pf::bv") << std::endl; // first print bit-blasting printBitblasting(os, paren); // print CNF conversion proof for bit-blasted facts - d_cnfProof->printAtomMapping(atoms, os, paren); - os << ";; Bit-blasting definitional clauses \n"; + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + + d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); + os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; for (IdToSatClause::iterator it = used_inputs.begin(); it != used_inputs.end(); ++it) { d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); } - os << ";; Bit-blasting learned clauses \n"; + os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; d_resolutionProof->printResolutions(os, paren); } +std::string LFSCBitVectorProof::assignAlias(Expr expr) { + Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); + + std::stringstream ss; + ss << "fbv" << d_assignedAliases.size(); + Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl; + d_assignedAliases[expr] = ss.str(); + return ss.str(); +} + +bool LFSCBitVectorProof::hasAlias(Expr expr) { + return d_assignedAliases.find(expr) != d_assignedAliases.end(); +} + +void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + Assert (c1.isConst()); + Assert (c2.isConst()); + Assert (utils::getSize(c1) == utils::getSize(c2)); + + os << "(bv_disequal_constants " << utils::getSize(c1) << " "; + + std::ostringstream paren; + + for (int i = utils::getSize(c1) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c1, i) ? "b1" : "b0") << " "; + paren << ")"; + } + os << "bvn"; + os << paren.str(); + + os << " "; + + for (int i = utils::getSize(c2) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c2, i) ? "b1" : "b0") << " "; + + } + os << "bvn"; + os << paren.str(); + + os << ")"; +} + +void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) { + ProofLetMap emptyMap; + os << "(rr_bv_default "; + d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap); + os << ")"; +} + } /* namespace CVC4 */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4a1f4015d..a52292ec9 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,6 +60,7 @@ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId; typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr; +typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString; class BitVectorProof : public TheoryProof { protected: @@ -108,35 +109,52 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0; + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; - virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0; - + virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0; + virtual const std::set<Node>* getAtomsInBitblastingProof() = 0; + virtual void calculateAtomsInBitblastingProof() = 0; }; class LFSCBitVectorProof: public BitVectorProof { void printConstant(Expr term, std::ostream& os); - void printOperatorNary(Expr term, std::ostream& os, const LetMap& map); - void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map); - void printPredicate(Expr term, std::ostream& os, const LetMap& map); - void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map); - void printBitOf(Expr term, std::ostream& os, const LetMap& map); + void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map); + void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map); + void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map); + void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map); + void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map); + + ExprToString d_exprToVariableName; + ExprToString d_assignedAliases; + std::map<std::string, std::string> d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); + + std::set<Node> d_atomsInBitblastingProof; + public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTermBitblasting(Expr term, std::ostream& os); - virtual void printAtomBitblasting(Expr term, std::ostream& os); - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printBitblasting(std::ostream& os, std::ostream& paren); - virtual void printResolutionProof(std::ostream& os, std::ostream& paren); + virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap); + void calculateAtomsInBitblastingProof(); + const std::set<Node>* getAtomsInBitblastingProof(); + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); }; }/* CVC4 namespace */ diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 19e9cbac9..b58ade35e 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,6 +19,7 @@ #include "proof/clause_id.h" #include "proof/proof_manager.h" +#include "proof/proof_utils.h" #include "proof/theory_proof.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" @@ -32,7 +33,6 @@ CnfProof::CnfProof(prop::CnfStream* stream, : d_cnfStream(stream) , d_clauseToAssertion(ctx) , d_assertionToProofRule(ctx) - , d_clauseIdToOwnerTheory(ctx) , d_currentAssertionStack() , d_currentDefinitionStack() , d_clauseToDefinition(ctx) @@ -103,7 +103,6 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); - registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -143,16 +142,15 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -void CnfProof::registerExplanationLemma(ClauseId clauseId) { - d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); +LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) { + Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); + return d_lemmaToProofRecipe[lemma]; } -theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { - Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); - return d_clauseIdToOwnerTheory[clause]; +bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) { + return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); } - void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -183,12 +181,10 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setExplainerTheory(theory::TheoryId theory) { - d_explainerTheory = theory; -} - -theory::TheoryId CnfProof::getExplainerTheory() { - return d_explainerTheory; +void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { + Assert(proofRecipe); + Assert(proofRecipe->getNumSteps() > 0); + d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -212,22 +208,19 @@ Node CnfProof::getCurrentDefinition() { return d_currentDefinitionStack.back(); } - Node CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); Node node = d_cnfStream->getNode(lit); return node; } - void CnfProof::collectAtoms(const prop::SatClause* clause, - NodeSet& atoms) { + std::set<Node>& atoms) { for (unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = clause->operator[](i); prop::SatVariable var = lit.getSatVariable(); TNode atom = getAtom(var); if (atoms.find(atom) == atoms.end()) { - Assert (atoms.find(atom) == atoms.end()); atoms.insert(atom); } } @@ -237,14 +230,75 @@ prop::SatLiteral CnfProof::getLiteral(TNode atom) { return d_cnfStream->getLiteral(atom); } +bool CnfProof::hasLiteral(TNode atom) { + return d_cnfStream->hasLiteral(atom); +} + +void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) { + d_cnfStream->ensureLiteral(atom, noPreregistration); +} + void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atom_map) { + std::set<Node>& atoms) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atom_map); + collectAtoms(clause, atoms); } +} + +void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set<Node>& atoms, + NodePairSet& rewrites) { + IdToSatClause::const_iterator it = lemmaClauses.begin(); + for (; it != lemmaClauses.end(); ++it) { + const prop::SatClause* clause = it->second; + + // TODO: just calculate the map from ID to recipe once, + // instead of redoing this over and over again + std::vector<Expr> clause_expr; + std::set<Node> clause_expr_nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes); + + for (unsigned i = 0; i < recipe.getNumSteps(); ++i) { + const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i); + Node atom = proofStep->getLiteral(); + + if (atom == Node()) { + // The last proof step always has the empty node as its target... + continue; + } + + if (atom.getKind() == kind::NOT) { + atom = atom[0]; + } + + atoms.insert(atom); + } + + LemmaProofRecipe::RewriteIterator rewriteIt; + for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) { + rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second)); + // The unrewritten terms also need to have literals, so insert them into atoms + Node rewritten = rewriteIt->first; + if (rewritten.getKind() == kind::NOT) { + rewritten = rewritten[0]; + } + atoms.insert(rewritten); + } + } } void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, @@ -263,13 +317,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, +void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren) { - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); + std::set<Node>::const_iterator it = atoms.begin(); + std::set<Node>::const_iterator end = atoms.end(); - for (;it != end; ++it) { + for (;it != end; ++it) { os << "(decl_atom "; Node atom = *it; prop::SatVariable var = getLiteral(atom).getSatVariable(); @@ -277,8 +331,30 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name) - << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name); + os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + paren << ")))"; + } +} + +void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap) { + std::set<Node>::const_iterator it = atoms.begin(); + std::set<Node>::const_iterator end = atoms.end(); + + for (;it != end; ++it) { + os << "(decl_atom "; + Node atom = *it; + prop::SatVariable var = getLiteral(atom).getSatVariable(); + //FIXME hideous + LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); + // pe->printLetTerm(atom.toExpr(), os); + pe->printBoundTerm(atom.toExpr(), os, letMap); + + os << " (\\ " << ProofManager::getVarName(var, d_name); + os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -304,6 +380,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { + Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting " + << std::endl; + os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); @@ -336,6 +415,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // and prints the proof of the top-level formula bool is_input = printProofTopLevel(base_assertion, os_base); + if (is_input) { + Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl; + } + //get base assertion with polarity bool base_pol = base_assertion.getKind()!=kind::NOT; base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; @@ -564,6 +647,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, if( !pols[0] || num_nots_1==1 ){ os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; }else{ + Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl; os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } Assert( elimNum!=0 ); @@ -662,6 +746,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + paren << "))"; } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a21cb1c0e..788526b80 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,6 +27,7 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" +#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -43,7 +44,9 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; -typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; +typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe; +typedef std::pair<Node, Node> NodePair; +typedef std::set<NodePair> NodePairSet; class CnfProof { protected: @@ -55,11 +58,8 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; - /** Map from assertion to the theory that added this assertion **/ - ClauseIdToTheory d_clauseIdToOwnerTheory; - - /** The last theory to explain a lemma **/ - theory::TheoryId d_explainerTheory; + /** Map from lemma to the recipe for proving it **/ + LemmaToRecipe d_lemmaToProofRecipe; /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; @@ -91,10 +91,16 @@ public: Node getAtom(prop::SatVariable var); prop::SatLiteral getLiteral(TNode node); + bool hasLiteral(TNode node); + void ensureLiteral(TNode node, bool noPreregistration = false); + void collectAtoms(const prop::SatClause* clause, - NodeSet& atoms); + std::set<Node>& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atoms); + std::set<Node>& atoms); + void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set<Node>& atoms, + NodePairSet& rewrites); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -121,11 +127,9 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setExplainerTheory(theory::TheoryId theory); - theory::TheoryId getExplainerTheory(); - theory::TheoryId getOwnerTheory(ClauseId clause); - - void registerExplanationLemma(ClauseId clauseId); + void setProofRecipe(LemmaProofRecipe* proofRecipe); + LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); + bool haveProofRecipe(const std::set<Node> &lemma); // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); @@ -134,9 +138,13 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const NodeSet& atoms, + virtual void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren) = 0; + virtual void printAtomMapping(const std::set<Node>& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap) = 0; virtual void printClause(const prop::SatClause& clause, std::ostream& os, @@ -161,10 +169,15 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const NodeSet& atoms, + void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren); + void printAtomMapping(const std::set<Node>& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap); + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp new file mode 100644 index 000000000..a12a516cf --- /dev/null +++ b/src/proof/lemma_proof.cpp @@ -0,0 +1,193 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "proof/lemma_proof.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) : + d_theory(theory), d_literalToProve(literalToProve) { +} + +theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const { + return d_theory; +} + +Node LemmaProofRecipe::ProofStep::getLiteral() const { + return d_literalToProve; +} + +void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) { + d_assertions.insert(assertion); +} + +std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const { + return d_assertions; +} + +void LemmaProofRecipe::addStep(ProofStep& proofStep) { + std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin(); + d_proofSteps.push_front(proofStep); +} + +std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::set<Node> existingAssertions = getBaseAssertions(); + + std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); + while (index != 0) { + existingAssertions.insert(step->getLiteral().negate()); + ++step; + --index; + } + + std::set<Node> neededAssertions = step->getAssertions(); + + std::set<Node> result; + std::set_difference(neededAssertions.begin(), neededAssertions.end(), + existingAssertions.begin(), existingAssertions.end(), + std::inserter(result, result.begin())); + return result; +} + +void LemmaProofRecipe::dump(const char *tag) const { + + if (d_proofSteps.size() == 1) { + Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl; + } + + unsigned count = 1; + Debug(tag) << "Base assertions:" << std::endl; + for (std::set<Node>::iterator baseIt = d_baseAssertions.begin(); + baseIt != d_baseAssertions.end(); + ++baseIt) { + Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl; + ++count; + } + + Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl; + + count = 1; + for (std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) { + Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] "; + if (step->getLiteral() == Node()) { + Debug(tag) << "Contradiction"; + } else { + Debug(tag) << step->getLiteral(); + } + + Debug(tag) << std::endl; + + std::set<Node> missingAssertions = getMissingAssertionsForStep(count - 1); + for (std::set<Node>::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) { + Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl; + } + + Debug(tag) << std::endl; + ++count; + } + + if (!d_assertionToExplanation.empty()) { + Debug(tag) << std::endl << "Rewrites used:" << std::endl; + count = 1; + for (std::map<Node, Node>::const_iterator rewrite = d_assertionToExplanation.begin(); + rewrite != d_assertionToExplanation.end(); + ++rewrite) { + Debug(tag) << "\tRewrite #" << count << ":" << std::endl + << "\t\t" << rewrite->first + << std::endl << "\t\trewritten into" << std::endl + << "\t\t" << rewrite->second + << std::endl << std::endl; + ++count; + } + } +} + +void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) { + d_baseAssertions.insert(baseAssertion); +} + +std::set<Node> LemmaProofRecipe::getBaseAssertions() const { + return d_baseAssertions; +} + +theory::TheoryId LemmaProofRecipe::getTheory() const { + Assert(d_proofSteps.size() > 0); + return d_proofSteps.back().getTheory(); +} + +void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) { + if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) { + Assert(d_assertionToExplanation[assertion] == explanation); + } + + d_assertionToExplanation[assertion] = explanation; +} + +bool LemmaProofRecipe::wasRewritten(Node assertion) const { + return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end(); +} + +Node LemmaProofRecipe::getExplanation(Node assertion) const { + Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()); + return d_assertionToExplanation.find(assertion)->second; +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const { + return d_assertionToExplanation.begin(); +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const { + return d_assertionToExplanation.end(); +} + +bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const { + return d_baseAssertions < other.d_baseAssertions; + } + +bool LemmaProofRecipe::simpleLemma() const { + return d_proofSteps.size() == 1; +} + +bool LemmaProofRecipe::compositeLemma() const { + return !simpleLemma(); +} + +const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::list<ProofStep>::const_iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) { + Assert(index < d_proofSteps.size()); + + std::list<ProofStep>::iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +unsigned LemmaProofRecipe::getNumSteps() const { + return d_proofSteps.size(); +} + +} /* namespace CVC4 */ diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h new file mode 100644 index 000000000..e96ff5337 --- /dev/null +++ b/src/proof/lemma_proof.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__LEMMA_PROOF_H +#define __CVC4__LEMMA_PROOF_H + +#include "expr/expr.h" +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" +#include "util/proof.h" +#include "expr/node.h" + +namespace CVC4 { + +class LemmaProofRecipe { +public: + class ProofStep { + public: + ProofStep(theory::TheoryId theory, Node literalToProve); + theory::TheoryId getTheory() const; + Node getLiteral() const; + void addAssertion(const Node& assertion); + std::set<Node> getAssertions() const; + + private: + theory::TheoryId d_theory; + Node d_literalToProve; + std::set<Node> d_assertions; + }; + + //* The lemma assertions and owner */ + void addBaseAssertion(Node baseAssertion); + std::set<Node> getBaseAssertions() const; + theory::TheoryId getTheory() const; + + //* Rewrite rules */ + typedef std::map<Node, Node>::const_iterator RewriteIterator; + RewriteIterator rewriteBegin() const; + RewriteIterator rewriteEnd() const; + + void addRewriteRule(Node assertion, Node explanation); + bool wasRewritten(Node assertion) const; + Node getExplanation(Node assertion) const; + + //* Proof Steps */ + void addStep(ProofStep& proofStep); + const ProofStep* getStep(unsigned index) const; + ProofStep* getStep(unsigned index); + unsigned getNumSteps() const; + std::set<Node> getMissingAssertionsForStep(unsigned index) const; + bool simpleLemma() const; + bool compositeLemma() const; + + void dump(const char *tag) const; + bool operator<(const LemmaProofRecipe& other) const; + +private: + //* The list of assertions for this lemma */ + std::set<Node> d_baseAssertions; + + //* The various steps needed to derive the empty clause */ + std::list<ProofStep> d_proofSteps; + + //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */ + std::map<Node, Node> d_assertionToExplanation; +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a3689d746..d155630e5 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -20,6 +20,7 @@ #include "base/cvc4_assert.h" #include "context/context.h" #include "options/bv_options.h" +#include "options/proof_options.h" #include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" @@ -61,10 +62,10 @@ ProofManager::ProofManager(ProofFormat format): } ProofManager::~ProofManager() { - delete d_satProof; - delete d_cnfProof; - delete d_theoryProof; - delete d_fullProof; + if (d_satProof) delete d_satProof; + if (d_cnfProof) delete d_cnfProof; + if (d_theoryProof) delete d_theoryProof; + if (d_fullProof) delete d_fullProof; } ProofManager* ProofManager::currentPM() { @@ -95,7 +96,6 @@ CnfProof* ProofManager::getCnfProof() { } TheoryProofEngine* ProofManager::getTheoryProofEngine() { - Assert (options::proof()); Assert (currentPM()->d_theoryProof != NULL); return currentPM()->d_theoryProof; } @@ -200,7 +200,6 @@ std::string ProofManager::getLitName(prop::SatLiteral lit, return append(prefix+".l", lit.toInt()); } - std::string ProofManager::getPreprocessedAssertionName(Node node, const std::string& prefix) { node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; @@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom, Assert(!lit.isNegated()); return getAtomName(lit.getSatVariable(), prefix); } + std::string ProofManager::getLitName(TNode lit, const std::string& prefix) { - return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) { + return currentPM()->d_rewriteFilters[litName]; + } + + return litName; } std::string ProofManager::sanitize(TNode node) { @@ -330,7 +335,14 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, , d_smtEngine(smtEngine) {} +void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) { + Unreachable(); +} + void LFSCProof::toStream(std::ostream& out) { + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + d_satProof->constructProof(); // collecting leaf clauses in resolution proof @@ -384,8 +396,37 @@ void LFSCProof::toStream(std::ostream& out) { for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; - NodeSet atoms; + std::set<Node> atoms; + NodePairSet rewrites; // collects the atoms in the clauses + d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites); + + if (!rewrites.empty()) { + Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl; + NodePairSet::const_iterator rewriteIt; + for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) { + Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl; + } + Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl; + } else { + Debug("pf::pm") << "No rewrites in lemmas found" << std::endl; + } + + // The derived/unrewritten atoms may not have CNF literals required later on. + // If they don't, add them. + std::set<Node>::const_iterator it; + for (it = atoms.begin(); it != atoms.end(); ++it) { + Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl; + if (!d_cnfProof->hasLiteral(*it)) { + // For arithmetic: these literals are not normalized, causing an error in Arith. + if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) { + d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver. + } else { + d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration. + } + } + } + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); @@ -393,38 +434,23 @@ void LFSCProof::toStream(std::ostream& out) { for (NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { utils::collectAtoms(*it, atoms); + // utils::collectAtoms(*it, newAtoms); } - NodeSet::iterator atomIt; - Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl; + std::set<Node>::iterator atomIt; + Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " + << std::endl << std::endl; for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) { Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl; - - if (Debug.isOn("proof:pm")) { - // std::cout << NodeManager::currentNM(); - Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; - for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - - Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; - for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - } } - smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; out << " ;; Declarations\n"; // declare the theory atoms - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); - Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl; - for(; it != end; ++it) { + for(it = atoms.begin(); it != atoms.end(); ++it) { Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } @@ -444,15 +470,31 @@ void LFSCProof::toStream(std::ostream& out) { out << "(: (holds cln)\n\n"; // Have the theory proofs print deferred declarations, e.g. for skolem variables. - out << " ;; Printing deferred declarations \n"; + out << " ;; Printing deferred declarations \n\n"; d_theoryProof->printDeferredDeclarations(out, paren); + d_theoryProof->finalizeBvConflicts(used_lemmas, out); + ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof(); + + out << "\n ;; Printing the global let map \n"; + + ProofLetMap globalLetMap; + if (options::lfscLetification()) { + ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren); + } + + out << " ;; Printing aliasing declarations \n\n"; + d_theoryProof->printAliasingDeclarations(out, paren); + + out << " ;; Rewrites for Lemmas \n"; + d_theoryProof->printLemmaRewrites(rewrites, out, paren); + // print trust that input assertions are their preprocessed form - printPreprocessedAssertions(used_assertions, out, paren); + printPreprocessedAssertions(used_assertions, out, paren, globalLetMap); // print mapping between theory atoms and internal SAT variables out << ";; Printing mapping from preprocessed assertions into atoms \n"; - d_cnfProof->printAtomMapping(atoms, out, paren); + d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap); Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl; @@ -464,12 +506,8 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl; - // FIXME: for now assume all theory lemmas are in CNF form so - // distinguish between them and inputs - // print theory lemmas for resolution proof - Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl; - d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); + d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap); Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { @@ -491,22 +529,24 @@ void LFSCProof::toStream(std::ostream& out) { void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, - std::ostream& paren) { + std::ostream& paren, + ProofLetMap& globalLetMap) { os << "\n ;; In the preprocessor we trust \n"; NodeSet::const_iterator it = assertions.begin(); NodeSet::const_iterator end = assertions.end(); + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl; + for (; it != end; ++it) { os << "(th_let_pf _ "; //TODO os << "(trust_f "; - ProofManager::currentPM()->getTheoryProofEngine()->printLetTerm((*it).toExpr(), os); + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); os << ") "; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; - } os << "\n"; @@ -568,6 +608,14 @@ void ProofManager::markPrinted(const Type& type) { d_printedTypes.insert(type); } +void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) { + d_rewriteFilters[original] = substitute; +} + +void ProofManager::clearRewriteFilters() { + d_rewriteFilters.clear(); +} + std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { switch(k) { case RULE_GIVEN: @@ -607,5 +655,88 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { return out; } +void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){ + Assert (currentPM()->d_theoryProof != NULL); + currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result)); +} + +void ProofManager::clearRewriteLog() { + Assert (currentPM()->d_theoryProof != NULL); + currentPM()->d_rewriteLog.clear(); +} + +std::vector<RewriteLogEntry> ProofManager::getRewriteLog() { + return currentPM()->d_rewriteLog; +} + +void ProofManager::dumpRewriteLog() const { + Debug("pf::rr") << "Dumpign rewrite log:" << std::endl; + + for (unsigned i = 0; i < d_rewriteLog.size(); ++i) { + Debug("pf::rr") << "\tRule " << d_rewriteLog[i].getRuleId() + << ": " + << d_rewriteLog[i].getOriginal() + << " --> " + << d_rewriteLog[i].getResult() << std::endl; + } +} + +void bind(Expr term, ProofLetMap& map, Bindings& letOrder) { + ProofLetMap::iterator it = map.find(term); + if (it != map.end()) + return; + + for (unsigned i = 0; i < term.getNumChildren(); ++i) + bind(term[i], map, letOrder); + + // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)). + // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too. + Kind k = term.getKind(); + if (((k == kind::OR) || (k == kind::AND)) && term.getNumChildren() > 2) { + Node currentExpression = term[term.getNumChildren() - 1]; + for (int i = term.getNumChildren() - 2; i >= 0; --i) { + NodeBuilder<> builder(k); + builder << term[i]; + builder << currentExpression.toExpr(); + currentExpression = builder; + bind(currentExpression.toExpr(), map, letOrder); + } + } else { + unsigned newId = ProofLetCount::newId(); + ProofLetCount letCount(newId); + map[term] = letCount; + letOrder.push_back(LetOrderElement(term, newId)); + } +} + +void ProofManager::printGlobalLetMap(std::set<Node>& atoms, + ProofLetMap& letMap, + std::ostream& out, + std::ostringstream& paren) { + Bindings letOrder; + std::set<Node>::const_iterator atom; + for (atom = atoms.begin(); atom != atoms.end(); ++atom) { + bind(atom->toExpr(), letMap, letOrder); + } + + // TODO: give each theory a chance to add atoms. For now, just query BV directly... + const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof(); + for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) { + bind(atom->toExpr(), letMap, letOrder); + } + + for (unsigned i = 0; i < letOrder.size(); ++i) { + Expr currentExpr = letOrder[i].expr; + unsigned letId = letOrder[i].id; + ProofLetMap::iterator it = letMap.find(currentExpr); + Assert(it != letMap.end()); + out << "\n(@ let" << letId << " "; + d_theoryProof->printBoundTerm(currentExpr, out, letMap); + paren << ")"; + it->second.increment(); + } + + out << std::endl << std::endl; +} } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index c74aac237..14793f380 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -22,6 +22,7 @@ #include <iosfwd> #include <map> #include "proof/proof.h" +#include "proof/proof_utils.h" #include "proof/skolemization_manager.h" #include "util/proof.h" #include "expr/node.h" @@ -34,6 +35,8 @@ namespace CVC4 { +class SmtGlobals; + // forward declarations namespace Minisat { class Solver; @@ -113,6 +116,30 @@ enum ProofRule { RULE_ARRAYS_ROW, /* arrays, read-over-write */ };/* enum ProofRules */ +class RewriteLogEntry { +public: + RewriteLogEntry(unsigned ruleId, Node original, Node result) + : d_ruleId(ruleId), d_original(original), d_result(result) { + } + + unsigned getRuleId() const { + return d_ruleId; + } + + Node getOriginal() const { + return d_original; + } + + Node getResult() const { + return d_result; + } + +private: + unsigned d_ruleId; + Node d_original; + Node d_result; +}; + class ProofManager { CoreSatProof* d_satProof; CnfProof* d_cnfProof; @@ -136,6 +163,10 @@ class ProofManager { std::set<Type> d_printedTypes; + std::map<std::string, std::string> d_rewriteFilters; + + std::vector<RewriteLogEntry> d_rewriteLog; + protected: LogicInfo d_logic; @@ -224,6 +255,19 @@ public: void markPrinted(const Type& type); bool wasPrinted(const Type& type) const; + void addRewriteFilter(const std::string &original, const std::string &substitute); + void clearRewriteFilters(); + + static void registerRewrite(unsigned ruleId, Node original, Node result); + static void clearRewriteLog(); + + std::vector<RewriteLogEntry> getRewriteLog(); + void dumpRewriteLog() const; + + void printGlobalLetMap(std::set<Node>& atoms, + ProofLetMap& letMap, + std::ostream& out, + std::ostringstream& paren); };/* class ProofManager */ class LFSCProof : public Proof { @@ -235,13 +279,15 @@ class LFSCProof : public Proof { // FIXME: hack until we get preprocessing void printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, - std::ostream& paren); + std::ostream& paren, + ProofLetMap& globalLetMap); public: LFSCProof(SmtEngine* smtEngine, LFSCCoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory); virtual void toStream(std::ostream& out); + virtual void toStream(std::ostream& out, const ProofLetMap& map); virtual ~LFSCProof() {} };/* class LFSCProof */ diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp new file mode 100644 index 000000000..6d729db1f --- /dev/null +++ b/src/proof/proof_output_channel.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_output_channel.cpp +** \verbatim +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "base/cvc4_assert.h" +#include "proof_output_channel.h" +#include "theory/term_registration_visitor.h" +#include "theory/valuation.h" + +namespace CVC4 { + +ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {} + +void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { + Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; + Assert(d_conflict.isNull()); + Assert(!n.isNull()); + d_conflict = n; + Assert(pf != NULL); + d_proof = pf; +} + +bool ProofOutputChannel::propagate(TNode x) throw() { + Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl; + d_propagations.insert(x); + return true; +} + +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { + Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; + d_lemma = n; + return theory::LemmaStatus(TNode::null(), 0); +} + +theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() { + AlwaysAssert(false); + return theory::LemmaStatus(TNode::null(), 0); +} + +void ProofOutputChannel::requirePhase(TNode n, bool b) throw() { + Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl; + Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl; +} + +bool ProofOutputChannel::flipDecision() throw() { + Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl; + AlwaysAssert(false); + return false; +} + +void ProofOutputChannel::setIncomplete() throw() { + Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl; + AlwaysAssert(false); +} + + +MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory) + : d_theory(theory) + , d_visited() { +} + +bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { + return d_visited.find(current) != d_visited.end(); +} + +void MyPreRegisterVisitor::visit(TNode current, TNode parent) { + d_theory->preRegisterTerm(current); + d_visited.insert(current); +} + +void MyPreRegisterVisitor::start(TNode node) { +} + +void MyPreRegisterVisitor::done(TNode node) { +} + +} /* namespace CVC4 */ diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h new file mode 100644 index 000000000..b85af5fb5 --- /dev/null +++ b/src/proof/proof_output_channel.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file proof_output_channel.h + ** \verbatim + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H +#define __CVC4__PROOF_OUTPUT_CHANNEL_H + +#include "theory/output_channel.h" + +namespace CVC4 { + +class ProofOutputChannel : public theory::OutputChannel { +public: + Node d_conflict; + Proof* d_proof; + Node d_lemma; + std::set<Node> d_propagations; + + ProofOutputChannel(); + + virtual ~ProofOutputChannel() throw() {} + + void conflict(TNode n, Proof* pf) throw(); + bool propagate(TNode x) throw(); + theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw(); + theory::LemmaStatus splitLemma(TNode, bool) throw(); + void requirePhase(TNode n, bool b) throw(); + bool flipDecision() throw(); + void setIncomplete() throw(); +};/* class ProofOutputChannel */ + +class MyPreRegisterVisitor { + theory::Theory* d_theory; + __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited; +public: + typedef void return_type; + MyPreRegisterVisitor(theory::Theory* theory); + bool alreadyVisited(TNode current, TNode parent); + void visit(TNode current, TNode parent); + void start(TNode node); + void done(TNode node); +}; /* class MyPreRegisterVisitor */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */ diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index 5b04c281d..fe0d42242 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -21,14 +21,14 @@ namespace CVC4 { namespace utils { -void collectAtoms(TNode node, CVC4::NodeSet& seen) { +void collectAtoms(TNode node, std::set<Node>& seen) { if (seen.find(node) != seen.end()) return; if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) { seen.insert(node); return; } - + for (unsigned i = 0; i < node.getNumChildren(); ++i) { collectAtoms(node[i], seen); } @@ -47,23 +47,23 @@ std::string toLFSCKind(Kind kind) { // bit-vector kinds case kind::BITVECTOR_AND : - return "bvand"; + return "bvand"; case kind::BITVECTOR_OR : - return "bvor"; + return "bvor"; case kind::BITVECTOR_XOR : - return "bvxor"; + return "bvxor"; case kind::BITVECTOR_NAND : - return "bvnand"; + return "bvnand"; case kind::BITVECTOR_NOR : - return "bvnor"; + return "bvnor"; case kind::BITVECTOR_XNOR : - return "bvxnor"; + return "bvxnor"; case kind::BITVECTOR_COMP : - return "bvcomp"; + return "bvcomp"; case kind::BITVECTOR_MULT : return "bvmul"; case kind::BITVECTOR_PLUS : - return "bvadd"; + return "bvadd"; case kind::BITVECTOR_SUB : return "bvsub"; case kind::BITVECTOR_UDIV : @@ -71,49 +71,49 @@ std::string toLFSCKind(Kind kind) { return "bvudiv"; case kind::BITVECTOR_UREM : case kind::BITVECTOR_UREM_TOTAL : - return "bvurem"; + return "bvurem"; case kind::BITVECTOR_SDIV : - return "bvsdiv"; + return "bvsdiv"; case kind::BITVECTOR_SREM : return "bvsrem"; case kind::BITVECTOR_SMOD : - return "bvsmod"; + return "bvsmod"; case kind::BITVECTOR_SHL : - return "bvshl"; + return "bvshl"; case kind::BITVECTOR_LSHR : return "bvlshr"; case kind::BITVECTOR_ASHR : return "bvashr"; case kind::BITVECTOR_CONCAT : - return "concat"; + return "concat"; case kind::BITVECTOR_NEG : - return "bvneg"; + return "bvneg"; case kind::BITVECTOR_NOT : - return "bvnot"; + return "bvnot"; case kind::BITVECTOR_ROTATE_LEFT : - return "rotate_left"; + return "rotate_left"; case kind::BITVECTOR_ROTATE_RIGHT : return "rotate_right"; case kind::BITVECTOR_ULT : - return "bvult"; + return "bvult"; case kind::BITVECTOR_ULE : - return "bvule"; + return "bvule"; case kind::BITVECTOR_UGT : return "bvugt"; case kind::BITVECTOR_UGE : return "bvuge"; case kind::BITVECTOR_SLT : - return "bvslt"; + return "bvslt"; case kind::BITVECTOR_SLE : - return "bvsle"; + return "bvsle"; case kind::BITVECTOR_SGT : - return "bvsgt"; + return "bvsgt"; case kind::BITVECTOR_SGE : - return "bvsge"; + return "bvsge"; case kind::BITVECTOR_EXTRACT : - return "extract"; + return "extract"; case kind::BITVECTOR_REPEAT : - return "repeat"; + return "repeat"; case kind::BITVECTOR_ZERO_EXTEND : return "zero_extend"; case kind::BITVECTOR_SIGN_EXTEND : diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index da10c33a0..546d419fc 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include <set> #include <vector> @@ -29,6 +29,61 @@ namespace CVC4 { typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::pair<Node, Node> NodePair; +typedef std::set<NodePair> NodePairSet; + + +struct ProofLetCount { + static unsigned counter; + static void resetCounter() { counter = 0; } + static unsigned newId() { return ++counter; } + + unsigned count; + unsigned id; + ProofLetCount() + : count(0) + , id(-1) + {} + + void increment() { ++count; } + ProofLetCount(unsigned i) + : count(1) + , id(i) + {} + + ProofLetCount(const ProofLetCount& other) + : count(other.count) + , id (other.id) + {} + + bool operator==(const ProofLetCount &other) const { + return other.id == id && other.count == count; + } + + ProofLetCount& operator=(const ProofLetCount &rhs) { + if (&rhs == this) return *this; + id = rhs.id; + count = rhs.count; + return *this; + } +}; + +struct LetOrderElement { + Expr expr; + unsigned id; + LetOrderElement(Expr e, unsigned i) + : expr(e) + , id(i) + {} + + LetOrderElement() + : expr() + , id(-1) + {} +}; + +typedef std::vector<LetOrderElement> Bindings; + namespace utils { std::string toLFSCKind(Kind kind); @@ -42,7 +97,7 @@ inline unsigned getExtractLow(Expr node) { } inline unsigned getSize(Type type) { - BitVectorType bv(type); + BitVectorType bv(type); return bv.getSize(); } @@ -60,8 +115,8 @@ inline Expr mkFalse() { return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false); } inline BitVector mkBitVectorOnes(unsigned size) { - Assert(size > 0); - return BitVector(1, Integer(1)).signExtend(size - 1); + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); } inline Expr mkExpr(Kind k , Expr expr) { @@ -73,16 +128,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) { inline Expr mkExpr(Kind k , std::vector<Expr>& children) { return NodeManager::currentNM()->toExprManager()->mkExpr(k, children); } - - + + inline Expr mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); } inline Expr mkConst(unsigned size, unsigned int value) { BitVector val(size, value); - return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); + return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); } inline Expr mkConst(const BitVector& value) { @@ -92,14 +147,14 @@ inline Expr mkConst(const BitVector& value) { inline Expr mkOr(const std::vector<Expr>& nodes) { std::set<Expr> all; all.insert(nodes.begin(), nodes.end()); - Assert(all.size() != 0 ); + Assert(all.size() != 0 ); if (all.size() == 1) { // All the same, or just one return nodes[0]; } - - + + NodeBuilder<> disjunction(kind::OR); std::set<Expr>::const_iterator it = all.begin(); std::set<Expr>::const_iterator it_end = all.end(); @@ -109,23 +164,23 @@ inline Expr mkOr(const std::vector<Expr>& nodes) { } Node res = disjunction; - return res.toExpr(); + return res.toExpr(); }/* mkOr() */ - + inline Expr mkAnd(const std::vector<Expr>& conjunctions) { std::set<Expr> all; all.insert(conjunctions.begin(), conjunctions.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return conjunctions[0]; } - + NodeBuilder<> conjunction(kind::AND); std::set<Expr>::const_iterator it = all.begin(); @@ -135,7 +190,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) { ++ it; } - Node res = conjunction; + Node res = conjunction; return res.toExpr(); }/* mkAnd() */ @@ -144,14 +199,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) { all.insert(children.begin(), children.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return children[0]; } - + NodeBuilder<> res(kind); std::set<Expr>::const_iterator it = all.begin(); @@ -165,13 +220,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) { }/* mkSortedNode() */ inline const bool getBit(Expr expr, unsigned i) { - Assert (i < utils::getSize(expr) && - expr.isConst()); + Assert (i < utils::getSize(expr) && + expr.isConst()); Integer bit = expr.getConst<BitVector>().extract(i, i).getValue(); - return (bit == 1u); + return (bit == 1u); } -void collectAtoms(TNode node, NodeSet& seen); +void collectAtoms(TNode node, std::set<Node>& seen); } diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index d94b61bf3..bda8094be 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -34,175 +34,99 @@ #include "util/proof.h" #include "util/statistics_registry.h" +// Forward declarations. namespace CVC4 { - class CnfProof; +template <class Solver> +class ProofProxy; +} /* namespace CVC4 */ +namespace CVC4 { /** * Helper debugging functions */ -template <class Solver> void printDebug(typename Solver::TLit l); -template <class Solver> void printDebug(typename Solver::TClause& c); +template <class Solver> +void printDebug(typename Solver::TLit l); +template <class Solver> +void printDebug(typename Solver::TClause& c); enum ClauseKind { INPUT, - THEORY_LEMMA, // we need to distinguish because we must reprove deleted theory lemmas + THEORY_LEMMA, // we need to distinguish because we must reprove deleted + // theory lemmas LEARNT -};/* enum ClauseKind */ - +}; /* enum ClauseKind */ template <class Solver> struct ResStep { typename Solver::TLit lit; ClauseId id; bool sign; - ResStep(typename Solver::TLit l, ClauseId i, bool s) : - lit(l), - id(i), - sign(s) - {} -};/* struct ResStep */ + ResStep(typename Solver::TLit l, ClauseId i, bool s) + : lit(l), id(i), sign(s) {} +}; /* struct ResStep */ template <class Solver> class ResChain { -public: - typedef std::vector< ResStep<Solver> > ResSteps; - typedef std::set < typename Solver::TLit> LitSet; - -private: - ClauseId d_start; - ResSteps d_steps; - LitSet* d_redundantLits; -public: + public: + typedef std::vector<ResStep<Solver> > ResSteps; + typedef std::set<typename Solver::TLit> LitSet; + ResChain(ClauseId start); + ~ResChain(); + void addStep(typename Solver::TLit, ClauseId, bool); - bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } + bool redundantRemoved() { + return (d_redundantLits == NULL || d_redundantLits->empty()); + } void addRedundantLit(typename Solver::TLit lit); - ~ResChain(); - // accessor methods - ClauseId getStart() { return d_start; } - ResSteps& getSteps() { return d_steps; } - LitSet* getRedundant() { return d_redundantLits; } -};/* class ResChain */ -template <class Solver> class ProofProxy; + // accessor methods + ClauseId getStart() const { return d_start; } + const ResSteps& getSteps() const { return d_steps; } + LitSet* getRedundant() const { return d_redundantLits; } -class CnfProof; + private: + ClauseId d_start; + ResSteps d_steps; + LitSet* d_redundantLits; +}; /* class ResChain */ -template<class Solver> +template <class Solver> class TSatProof { -protected: - typedef std::set < typename Solver::TLit> LitSet; - typedef std::set < typename Solver::TVar> VarSet; - typedef std::hash_map < ClauseId, typename Solver::TCRef > IdCRefMap; - typedef std::hash_map < typename Solver::TCRef, ClauseId > ClauseIdMap; - typedef std::hash_map < ClauseId, typename Solver::TLit> IdUnitMap; - typedef std::hash_map < int, ClauseId> UnitIdMap; - typedef std::hash_map < ClauseId, ResChain<Solver>* > IdResMap; - typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; - typedef std::vector < ResChain<Solver>* > ResStack; - //typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; - typedef std::set < ClauseId > IdSet; - typedef std::vector < typename Solver::TLit > LitVector; - typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause& > IdToMinisatClause; - typedef __gnu_cxx::hash_map<ClauseId, LitVector* > IdToConflicts; - - typename Solver::Solver* d_solver; - CnfProof* d_cnfProof; - - // clauses - IdCRefMap d_idClause; - ClauseIdMap d_clauseId; - IdUnitMap d_idUnit; - UnitIdMap d_unitId; - IdHashSet d_deleted; - IdToSatClause d_deletedTheoryLemmas; - -protected: - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; - VarSet d_assumptions; // assumption literals for bv solver - IdHashSet d_assumptionConflicts; // assumption conflicts not actually added to SAT solver - IdToConflicts d_assumptionConflictsDebug; - - // resolutions - IdResMap d_resChains; - ResStack d_resStack; - bool d_checkRes; - - const ClauseId d_emptyClauseId; - const ClauseId d_nullId; - // proxy class to break circular dependencies - ProofProxy<Solver>* d_proxy; - - // temporary map for updating CRefs - ClauseIdMap d_temp_clauseId; - IdCRefMap d_temp_idClause; - - // unit conflict - ClauseId d_unitConflictId; - bool d_storedUnitConflict; - - ClauseId d_trueLit; - ClauseId d_falseLit; - - std::string d_name; -public: + protected: + typedef ResChain<Solver> ResolutionChain; + + typedef std::set<typename Solver::TLit> LitSet; + typedef std::set<typename Solver::TVar> VarSet; + typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap; + typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap; + typedef std::hash_map<ClauseId, typename Solver::TLit> IdUnitMap; + typedef std::hash_map<int, ClauseId> UnitIdMap; + typedef std::hash_map<ClauseId, ResolutionChain*> IdResMap; + typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap; + typedef std::vector<ResolutionChain*> ResStack; + typedef std::set<ClauseId> IdSet; + typedef std::vector<typename Solver::TLit> LitVector; + typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&> + IdToMinisatClause; + typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts; + + public: TSatProof(Solver* solver, const std::string& name, bool checkRes = false); virtual ~TSatProof(); void setCnfProof(CnfProof* cnf_proof); -protected: - void print(ClauseId id); - void printRes(ClauseId id); - void printRes(ResChain<Solver>* res); - - bool isInputClause(ClauseId id); - bool isLemmaClause(ClauseId id); - bool isAssumptionConflict(ClauseId id); - bool isUnit(ClauseId id); - bool isUnit(typename Solver::TLit lit); - bool hasResolution(ClauseId id); - void createLitSet(ClauseId id, LitSet& set); - void registerResolution(ClauseId id, ResChain<Solver>* res); - - ClauseId getClauseId(typename Solver::TCRef clause); - ClauseId getClauseId(typename Solver::TLit lit); - typename Solver::TCRef getClauseRef(ClauseId id); - typename Solver::TLit getUnit(ClauseId id); - ClauseId getUnitId(typename Solver::TLit lit); - typename Solver::TClause& getClause(typename Solver::TCRef ref); - void getLitVec(ClauseId id, LitVector& vec); - virtual void toStream(std::ostream& out); - bool checkResolution(ClauseId id); - /** - * Constructs a resolution tree that proves lit - * and returns the ClauseId for the unit clause lit - * @param lit the literal we are proving - * - * @return - */ - ClauseId resolveUnit(typename Solver::TLit lit); - /** - * Does a depth first search on removed literals and adds the literals - * to be removed in the proper order to the stack. - * - * @param lit the literal we are recursing on - * @param removedSet the previously computed set of redundant literals - * @param removeStack the stack of literals in reverse order of resolution - */ - void removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); - void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id); -public: void startResChain(typename Solver::TLit start); void startResChain(typename Solver::TCRef start); - void addResolutionStep(typename Solver::TLit lit, typename Solver::TCRef clause, bool sign); + void addResolutionStep(typename Solver::TLit lit, + typename Solver::TCRef clause, bool sign); /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter * @param clause the clause the resolution is proving */ - //void endResChain(typename Solver::TCRef clause); + // void endResChain(typename Solver::TCRef clause); void endResChain(typename Solver::TLit lit); void endResChain(ClauseId id); @@ -219,7 +143,8 @@ public: void storeLitRedundant(typename Solver::TLit lit); /// update the CRef Id maps when Minisat does memory reallocation x - void updateCRef(typename Solver::TCRef old_ref, typename Solver::TCRef new_ref); + void updateCRef(typename Solver::TCRef old_ref, + typename Solver::TCRef new_ref); void finishUpdateCRef(); /** @@ -231,25 +156,22 @@ public: /// clause registration methods - ClauseId registerClause(const typename Solver::TCRef clause, - ClauseKind kind); - ClauseId registerUnitClause(const typename Solver::TLit lit, - ClauseKind kind); + ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind); + ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind); void registerTrueLit(const typename Solver::TLit lit); void registerFalseLit(const typename Solver::TLit lit); ClauseId getTrueUnit() const; ClauseId getFalseUnit() const; - void registerAssumption(const typename Solver::TVar var); ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); - ClauseId storeUnitConflict(typename Solver::TLit lit, - ClauseKind kind); + ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind); /** - * Marks the deleted clauses as deleted. Note we may still use them in the final + * Marks the deleted clauses as deleted. Note we may still use them in the + * final * resolution. * @param clause */ @@ -268,43 +190,171 @@ public: */ void storeUnitResolution(typename Solver::TLit lit); - ProofProxy<Solver>* getProxy() {return d_proxy; } + ProofProxy<Solver>* getProxy() { return d_proxy; } /** * Constructs the SAT proof for the given clause, * by collecting the needed clauses in the d_seen * data-structures, also notifying the proofmanager. */ void constructProof(ClauseId id); - void constructProof() { - constructProof(d_emptyClauseId); - } + void constructProof() { constructProof(d_emptyClauseId); } void collectClauses(ClauseId id); prop::SatClause* buildClause(ClauseId id); -protected: - IdSet d_seenLearnt; - IdToSatClause d_seenInputs; - IdToSatClause d_seenLemmas; + + virtual void printResolution(ClauseId id, std::ostream& out, + std::ostream& paren) = 0; + virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; + virtual void printResolutionEmptyClause(std::ostream& out, + std::ostream& paren) = 0; + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, + std::ostream& paren) = 0; + + void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); + + void storeClauseGlue(ClauseId clause, int glue); + + protected: + void print(ClauseId id) const; + void printRes(ClauseId id) const; + void printRes(const ResolutionChain& res) const; + + bool isInputClause(ClauseId id) const; + bool isLemmaClause(ClauseId id) const; + bool isAssumptionConflict(ClauseId id) const; + + bool isUnit(ClauseId id) const; + typename Solver::TLit getUnit(ClauseId id) const; + + bool isUnit(typename Solver::TLit lit) const; + ClauseId getUnitId(typename Solver::TLit lit) const; + + + + bool hasResolutionChain(ClauseId id) const; + + /** Returns the resolution chain associated with id. Assert fails if + * hasResolution(id) does not hold. */ + const ResolutionChain& getResolutionChain(ClauseId id) const; + + /** Returns a mutable pointer to the resolution chain associated with id. + * Assert fails if hasResolution(id) does not hold. */ + ResolutionChain* getMutableResolutionChain(ClauseId id); + + void createLitSet(ClauseId id, LitSet& set); + + /** + * Registers a ClauseId with a resolution chain res. + * Takes ownership of the memory associated with res. + */ + void registerResolution(ClauseId id, ResolutionChain* res); + + + bool hasClauseIdForCRef(typename Solver::TCRef clause) const; + ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const; + + bool hasClauseIdForLiteral(typename Solver::TLit lit) const; + ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const; + + bool hasClauseRef(ClauseId id) const; + typename Solver::TCRef getClauseRef(ClauseId id) const; + + + const typename Solver::TClause& getClause(typename Solver::TCRef ref) const; + typename Solver::TClause* getMutableClause(typename Solver::TCRef ref); + + void getLitVec(ClauseId id, LitVector& vec); + virtual void toStream(std::ostream& out); + + bool checkResolution(ClauseId id); + + /** + * Constructs a resolution tree that proves lit + * and returns the ClauseId for the unit clause lit + * @param lit the literal we are proving + * + * @return + */ + ClauseId resolveUnit(typename Solver::TLit lit); + + /** + * Does a depth first search on removed literals and adds the literals + * to be removed in the proper order to the stack. + * + * @param lit the literal we are recursing on + * @param removedSet the previously computed set of redundant literals + * @param removeStack the stack of literals in reverse order of resolution + */ + void removedDfs(typename Solver::TLit lit, LitSet* removedSet, + LitVector& removeStack, LitSet& inClause, LitSet& seen); + void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id); std::string varName(typename Solver::TLit lit); std::string clauseName(ClauseId id); - void addToProofManager(ClauseId id, ClauseKind kind); void addToCnfProof(ClauseId id); -public: - virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; - virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; - virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren) = 0; - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; - void collectClausesUsed(IdToSatClause& inputs, - IdToSatClause& lemmas); + // Internal data. + typename Solver::Solver* d_solver; + CnfProof* d_cnfProof; - void storeClauseGlue(ClauseId clause, int glue); + // clauses + IdCRefMap d_idClause; + ClauseIdMap d_clauseId; + IdUnitMap d_idUnit; + UnitIdMap d_unitId; + IdHashSet d_deleted; + IdToSatClause d_deletedTheoryLemmas; + + IdHashSet d_inputClauses; + IdHashSet d_lemmaClauses; + VarSet d_assumptions; // assumption literals for bv solver + IdHashSet d_assumptionConflicts; // assumption conflicts not actually added + // to SAT solver + IdToConflicts d_assumptionConflictsDebug; + + // Resolutions. + /** + * Map from ClauseId to resolution chain corresponding proving the + * clause corresponding to the ClauseId. d_resolutionChains owns the + * memory of the ResChain* it contains. + */ + IdResMap d_resolutionChains; + + /* + * Stack containting current ResChain* we are working on. d_resStack + * owns the memory for the ResChain* it contains. Invariant: no + * ResChain* pointer can be both in d_resStack and + * d_resolutionChains. Memory ownership is transfered from + * d_resStack to d_resolutionChains via registerResolution. + */ + ResStack d_resStack; + bool d_checkRes; + + const ClauseId d_emptyClauseId; + const ClauseId d_nullId; + // proxy class to break circular dependencies + ProofProxy<Solver>* d_proxy; + // temporary map for updating CRefs + ClauseIdMap d_temp_clauseId; + IdCRefMap d_temp_idClause; -private: + // unit conflict + ClauseId d_unitConflictId; + bool d_storedUnitConflict; + + ClauseId d_trueLit; + ClauseId d_falseLit; + + std::string d_name; + + IdSet d_seenLearnt; + IdToSatClause d_seenInputs; + IdToSatClause d_seenLemmas; + + private: __gnu_cxx::hash_map<ClauseId, int> d_glueMap; struct Statistics { IntStat d_numLearnedClauses; @@ -320,49 +370,47 @@ private: }; Statistics d_statistics; -};/* class TSatProof */ +}; /* class TSatProof */ template <class S> class ProofProxy { -private: + private: TSatProof<S>* d_proof; -public: + + public: ProofProxy(TSatProof<S>* pf); void updateCRef(typename S::TCRef oldref, typename S::TCRef newref); -};/* class ProofProxy */ - +}; /* class ProofProxy */ template <class SatSolver> class LFSCSatProof : public TSatProof<SatSolver> { -private: - -public: - LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false) - : TSatProof<SatSolver>(solver, name, checkRes) - {} - virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); + private: + public: + LFSCSatProof(SatSolver* solver, const std::string& name, + bool checkRes = false) + : TSatProof<SatSolver>(solver, name, checkRes) {} + virtual void printResolution(ClauseId id, std::ostream& out, + std::ostream& paren); virtual void printResolutions(std::ostream& out, std::ostream& paren); - virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren); - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren); -};/* class LFSCSatProof */ - - + virtual void printResolutionEmptyClause(std::ostream& out, + std::ostream& paren); + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, + std::ostream& paren); +}; /* class LFSCSatProof */ -template<class Solver> +template <class Solver> prop::SatLiteral toSatLiteral(typename Solver::TLit lit); - /** * Convert from minisat clause to SatClause * * @param minisat_cl * @param sat_cl */ -template<class Solver> +template <class Solver> void toSatClause(const typename Solver::TClause& minisat_cl, prop::SatClause& sat_cl); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index e773e4b47..1e01e4dce 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -32,29 +32,28 @@ namespace CVC4 { template <class Solver> -void printLit (typename Solver::TLit l) { +void printLit(typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; } template <class Solver> -void printClause (typename Solver::TClause& c) { +void printClause(const typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } template <class Solver> -void printClause (std::vector<typename Solver::TLit>& c) { +void printClause(const std::vector<typename Solver::TLit>& c) { for (unsigned i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } - template <class Solver> void printLitSet(const std::set<typename Solver::TLit>& s) { - typename std::set < typename Solver::TLit>::const_iterator it = s.begin(); - for(; it != s.end(); ++it) { + typename std::set<typename Solver::TLit>::const_iterator it = s.begin(); + for (; it != s.end(); ++it) { printLit<Solver>(*it); Debug("proof:sat") << " "; } @@ -63,18 +62,17 @@ void printLitSet(const std::set<typename Solver::TLit>& s) { // purely debugging functions template <class Solver> -void printDebug (typename Solver::TLit l) { +void printDebug(typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; } template <class Solver> -void printDebug (typename Solver::TClause& c) { +void printDebug(typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } Debug("proof:sat") << std::endl; } - /** * Converts the clause associated to id to a set of literals * @@ -84,11 +82,11 @@ void printDebug (typename Solver::TClause& c) { template <class Solver> void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { Assert(set.empty()); - if(isUnit(id)) { + if (isUnit(id)) { set.insert(getUnit(id)); return; } - if ( id == d_emptyClauseId) { + if (id == d_emptyClauseId) { return; } // if it's an assumption @@ -101,13 +99,12 @@ void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { } typename Solver::TCRef ref = getClauseRef(id); - typename Solver::TClause& c = getClause(ref); + const typename Solver::TClause& c = getClause(ref); for (int i = 0; i < c.size(); i++) { set.insert(c[i]); } } - /** * Resolves clause1 and clause2 on variable var and stores the * result in clause1 @@ -124,8 +121,8 @@ bool resolve(const typename Solver::TLit v, typename Solver::TLit var = sign(v) ? ~v : v; if (s) { // literal appears positive in the first clause - if( !clause2.count(~var)) { - if(Debug.isOn("proof:sat")) { + if (!clause2.count(~var)) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof:resolve: Missing literal "; printLit<Solver>(var); Debug("proof:sat") << std::endl; @@ -135,13 +132,13 @@ bool resolve(const typename Solver::TLit v, clause1.erase(var); clause2.erase(~var); typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); - for (; it!= clause2.end(); ++it) { + for (; it != clause2.end(); ++it) { clause1.insert(*it); } } else { // literal appears negative in the first clause - if( !clause1.count(~var) || !clause2.count(var)) { - if(Debug.isOn("proof:sat")) { + if (!clause1.count(~var) || !clause2.count(var)) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof:resolve: Missing literal "; printLit<Solver>(var); Debug("proof:sat") << std::endl; @@ -151,7 +148,7 @@ bool resolve(const typename Solver::TLit v, clause1.erase(~var); clause2.erase(var); typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); - for (; it!= clause2.end(); ++it) { + for (; it != clause2.end(); ++it) { clause1.insert(*it); } } @@ -160,13 +157,19 @@ bool resolve(const typename Solver::TLit v, /// ResChain template <class Solver> -ResChain<Solver>::ResChain(ClauseId start) : - d_start(start), - d_steps(), - d_redundantLits(NULL) - {} +ResChain<Solver>::ResChain(ClauseId start) + : d_start(start), d_steps(), d_redundantLits(NULL) {} + +template <class Solver> +ResChain<Solver>::~ResChain() { + if (d_redundantLits != NULL) { + delete d_redundantLits; + } +} + template <class Solver> -void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id, bool sign) { +void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id, + bool sign) { ResStep<Solver> step(lit, id, sign); d_steps.push_back(step); } @@ -181,50 +184,47 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) { } } - /// ProxyProof template <class Solver> -ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof): - d_proof(proof) -{} +ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof) : d_proof(proof) {} template <class Solver> -void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { +void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, + typename Solver::TCRef newref) { d_proof->updateCRef(oldref, newref); } - /// SatProof template <class Solver> -TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, bool checkRes) - : d_solver(solver) - , d_cnfProof(NULL) - , d_idClause() - , d_clauseId() - , d_idUnit() - , d_deleted() - , d_inputClauses() - , d_lemmaClauses() - , d_assumptions() - , d_assumptionConflicts() - , d_assumptionConflictsDebug() - , d_resChains() - , d_resStack() - , d_checkRes(checkRes) - , d_emptyClauseId(ClauseIdEmpty) - , d_nullId(-2) - , d_temp_clauseId() - , d_temp_idClause() - , d_unitConflictId() - , d_storedUnitConflict(false) - , d_trueLit(ClauseIdUndef) - , d_falseLit(ClauseIdUndef) - , d_name(name) - , d_seenLearnt() - , d_seenInputs() - , d_seenLemmas() - , d_statistics(name) -{ +TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, + bool checkRes) + : d_solver(solver), + d_cnfProof(NULL), + d_idClause(), + d_clauseId(), + d_idUnit(), + d_deleted(), + d_inputClauses(), + d_lemmaClauses(), + d_assumptions(), + d_assumptionConflicts(), + d_assumptionConflictsDebug(), + d_resolutionChains(), + d_resStack(), + d_checkRes(checkRes), + d_emptyClauseId(ClauseIdEmpty), + d_nullId(-2), + d_temp_clauseId(), + d_temp_idClause(), + d_unitConflictId(), + d_storedUnitConflict(false), + d_trueLit(ClauseIdUndef), + d_falseLit(ClauseIdUndef), + d_name(name), + d_seenLearnt(), + d_seenInputs(), + d_seenLemmas(), + d_statistics(name) { d_proxy = new ProofProxy<Solver>(this); } @@ -233,34 +233,53 @@ TSatProof<Solver>::~TSatProof() { delete d_proxy; // FIXME: double free if deleted clause also appears in d_seenLemmas? - IdToSatClause::iterator it = d_deletedTheoryLemmas.begin(); - IdToSatClause::iterator end = d_deletedTheoryLemmas.end(); + IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin(); + IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end(); for (; it != end; ++it) { ClauseId id = it->first; // otherwise deleted in next loop - if (d_seenLemmas.find(id) == d_seenLemmas.end()) + if (d_seenLemmas.find(id) == d_seenLemmas.end()) { delete it->second; + } } - IdToSatClause::iterator seen_it = d_seenLemmas.begin(); - IdToSatClause::iterator seen_end = d_seenLemmas.end(); + IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin(); + IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end(); - for (; seen_it != seen_end; ++seen_it) { - delete seen_it->second; + for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) { + delete seen_lemma_it->second; } - seen_it = d_seenInputs.begin(); - seen_end = d_seenInputs.end(); + IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin(); + IdToSatClause::const_iterator seen_input_end = d_seenInputs.end(); - for (; seen_it != seen_end; ++seen_it) { - delete seen_it->second; + for (; seen_input_it != seen_input_end; ++seen_input_it) { + delete seen_input_it->second; + } + + typedef typename IdResMap::const_iterator ResolutionChainIterator; + ResolutionChainIterator resolution_it = d_resolutionChains.begin(); + ResolutionChainIterator resolution_it_end = d_resolutionChains.end(); + for (; resolution_it != resolution_it_end; ++resolution_it) { + ResChain<Solver>* current = resolution_it->second; + delete current; + } + + // It could be the case that d_resStack is not empty at destruction time + // (for example in the SAT case). + typename ResStack::const_iterator resolution_stack_it = d_resStack.begin(); + typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end(); + for (; resolution_stack_it != resolution_stack_it_end; + ++resolution_stack_it) { + ResChain<Solver>* current = *resolution_stack_it; + delete current; } } template <class Solver> void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) { - Assert (d_cnfProof == NULL); + Assert(d_cnfProof == NULL); d_cnfProof = cnf_proof; } @@ -273,19 +292,19 @@ void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) { */ template <class Solver> bool TSatProof<Solver>::checkResolution(ClauseId id) { - if(d_checkRes) { + if (d_checkRes) { bool validRes = true; - Assert(d_resChains.find(id) != d_resChains.end()); - ResChain<Solver>* res = d_resChains[id]; + Assert(hasResolutionChain(id)); + const ResolutionChain& res = getResolutionChain(id); LitSet clause1; - createLitSet(res->getStart(), clause1); - typename ResChain<Solver>::ResSteps& steps = res->getSteps(); + createLitSet(res.getStart(), clause1); + const typename ResolutionChain::ResSteps& steps = res.getSteps(); for (unsigned i = 0; i < steps.size(); i++) { - typename Solver::TLit var = steps[i].lit; + typename Solver::TLit var = steps[i].lit; LitSet clause2; - createLitSet (steps[i].id, clause2); - bool res = resolve<Solver> (var, clause1, clause2, steps[i].sign); - if(res == false) { + createLitSet(steps[i].id, clause2); + bool res = resolve<Solver>(var, clause1, clause2, steps[i].sign); + if (res == false) { validRes = false; break; } @@ -307,8 +326,9 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { for (unsigned i = 0; i < c.size(); ++i) { int count = clause1.erase(c[i]); if (count == 0) { - if(Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + if (Debug.isOn("proof:sat")) { + Debug("proof:sat") + << "proof:checkResolution::literal not in computed result "; printLit<Solver>(c[i]); Debug("proof:sat") << "\n"; } @@ -316,9 +336,10 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { } } validRes = clause1.empty(); - if (! validRes) { - if(Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + if (!validRes) { + if (Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, " + "unremoved literals: \n"; printLitSet<Solver>(clause1); Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; printClause<Solver>(c); @@ -331,37 +352,54 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { } } - - - /// helper methods template <class Solver> -ClauseId TSatProof<Solver>::getClauseId(typename Solver::TCRef ref) { - if(d_clauseId.find(ref) == d_clauseId.end()) { +bool TSatProof<Solver>::hasClauseIdForCRef(typename Solver::TCRef ref) const { + return d_clauseId.find(ref) != d_clauseId.end(); +} + +template <class Solver> +ClauseId TSatProof<Solver>::getClauseIdForCRef( + typename Solver::TCRef ref) const { + if (d_clauseId.find(ref) == d_clauseId.end()) { Debug("proof:sat") << "Missing clause \n"; } - Assert(d_clauseId.find(ref) != d_clauseId.end()); - return d_clauseId[ref]; + Assert(hasClauseIdForCRef(ref)); + return d_clauseId.find(ref)->second; +} + +template <class Solver> +bool TSatProof<Solver>::hasClauseIdForLiteral(typename Solver::TLit lit) const { + return d_unitId.find(toInt(lit)) != d_unitId.end(); +} + +template <class Solver> +ClauseId TSatProof<Solver>::getClauseIdForLiteral( + typename Solver::TLit lit) const { + Assert(hasClauseIdForLiteral(lit)); + return d_unitId.find(toInt(lit))->second; } template <class Solver> -ClauseId TSatProof<Solver>::getClauseId(typename Solver::TLit lit) { - Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); - return d_unitId[toInt(lit)]; +bool TSatProof<Solver>::hasClauseRef(ClauseId id) const { + return d_idClause.find(id) != d_idClause.end(); } + template <class Solver> -typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) { - if (d_idClause.find(id) == d_idClause.end()) { - Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" " - << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "") - << (isUnit(id)? "Unit" : "") << std::endl; +typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) const { + if (!hasClauseRef(id)) { + Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " " + << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" + : "") + << (isUnit(id) ? "Unit" : "") << std::endl; } - Assert(d_idClause.find(id) != d_idClause.end()); - return d_idClause[id]; + Assert(hasClauseRef(id)); + return d_idClause.find(id)->second; } template <class Solver> -typename Solver::TClause& TSatProof<Solver>::getClause(typename Solver::TCRef ref) { +const typename Solver::TClause& TSatProof<Solver>::getClause( + typename Solver::TCRef ref) const { Assert(ref != Solver::TCRef_Undef); Assert(ref >= 0 && ref < d_solver->ca.size()); return d_solver->ca[ref]; @@ -379,85 +417,106 @@ void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) { return; } typename Solver::TCRef cref = getClauseRef(id); - typename Solver::TClause& cl = getClause(cref); + const typename Solver::TClause& cl = getClause(cref); for (int i = 0; i < cl.size(); ++i) { vec.push_back(cl[i]); } } - template <class Solver> -typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) { - Assert(d_idUnit.find(id) != d_idUnit.end()); - return d_idUnit[id]; +bool TSatProof<Solver>::isUnit(ClauseId id) const { + return d_idUnit.find(id) != d_idUnit.end(); } + template <class Solver> -bool TSatProof<Solver>::isUnit(ClauseId id) { - return d_idUnit.find(id) != d_idUnit.end(); +typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) const { + Assert(isUnit(id)); + return d_idUnit.find(id)->second; } + template <class Solver> -bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) { +bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) const { return d_unitId.find(toInt(lit)) != d_unitId.end(); } + template <class Solver> -ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) { +ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) const { Assert(isUnit(lit)); - return d_unitId[toInt(lit)]; + return d_unitId.find(toInt(lit))->second; } + template <class Solver> -bool TSatProof<Solver>::hasResolution(ClauseId id) { - return d_resChains.find(id) != d_resChains.end(); +bool TSatProof<Solver>::hasResolutionChain(ClauseId id) const { + return d_resolutionChains.find(id) != d_resolutionChains.end(); } + template <class Solver> -bool TSatProof<Solver>::isInputClause(ClauseId id) { - return (d_inputClauses.find(id) != d_inputClauses.end()); +const typename TSatProof<Solver>::ResolutionChain& +TSatProof<Solver>::getResolutionChain(ClauseId id) const { + Assert(hasResolutionChain(id)); + const ResolutionChain* chain = d_resolutionChains.find(id)->second; + return *chain; } + template <class Solver> -bool TSatProof<Solver>::isLemmaClause(ClauseId id) { - return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); +typename TSatProof<Solver>::ResolutionChain* +TSatProof<Solver>::getMutableResolutionChain(ClauseId id) { + Assert(hasResolutionChain(id)); + ResolutionChain* chain = d_resolutionChains.find(id)->second; + return chain; } template <class Solver> -bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) { - return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +bool TSatProof<Solver>::isInputClause(ClauseId id) const { + return d_inputClauses.find(id) != d_inputClauses.end(); } +template <class Solver> +bool TSatProof<Solver>::isLemmaClause(ClauseId id) const { + return d_lemmaClauses.find(id) != d_lemmaClauses.end(); +} + +template <class Solver> +bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) const { + return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +} template <class Solver> -void TSatProof<Solver>::print(ClauseId id) { +void TSatProof<Solver>::print(ClauseId id) const { if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del"<<id; + Debug("proof:sat") << "del" << id; } else if (isUnit(id)) { printLit<Solver>(getUnit(id)); } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty "<< std::endl; - } - else { + Debug("proof:sat") << "empty " << std::endl; + } else { typename Solver::TCRef ref = getClauseRef(id); printClause<Solver>(getClause(ref)); } } + template <class Solver> -void TSatProof<Solver>::printRes(ClauseId id) { - Assert(hasResolution(id)); - Debug("proof:sat") << "id "<< id <<": "; - printRes(d_resChains[id]); +void TSatProof<Solver>::printRes(ClauseId id) const { + Assert(hasResolutionChain(id)); + Debug("proof:sat") << "id " << id << ": "; + printRes(getResolutionChain(id)); } + template <class Solver> -void TSatProof<Solver>::printRes(ResChain<Solver>* res) { - ClauseId start_id = res->getStart(); +void TSatProof<Solver>::printRes(const ResolutionChain& res) const { + ClauseId start_id = res.getStart(); - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "("; print(start_id); } - typename ResChain<Solver>::ResSteps& steps = res->getSteps(); - for(unsigned i = 0; i < steps.size(); i++ ) { + const typename ResolutionChain::ResSteps& steps = res.getSteps(); + for (unsigned i = 0; i < steps.size(); i++) { typename Solver::TLit v = steps[i].lit; ClauseId id = steps[i].id; - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "["; printLit<Solver>(v); Debug("proof:sat") << "] "; @@ -469,8 +528,8 @@ void TSatProof<Solver>::printRes(ResChain<Solver>* res) { /// registration methods template <class Solver> - ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause, - ClauseKind kind) { +ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause, + ClauseKind kind) { Assert(clause != Solver::TCRef_Undef); typename ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { @@ -485,10 +544,8 @@ template <class Solver> Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); d_lemmaClauses.insert(newId); Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " - << newId << " = " << *buildClause(newId) - << ". Explainer theory: " << d_cnfProof->getExplainerTheory() - << std::endl; - d_cnfProof->registerExplanationLemma(newId); + << newId << " = " << *buildClause(newId) + << std::endl; } } @@ -496,15 +553,16 @@ template <class Solver> Assert(kind != INPUT || d_inputClauses.count(id)); Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); - Debug("proof:sat:detailed") << "registerClause CRef: " << clause << " id: " << d_clauseId[clause] - <<" kind: " << kind << "\n"; - //ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); + Debug("proof:sat:detailed") << "registerClause CRef: " << clause + << " id: " << d_clauseId[clause] + << " kind: " << kind << "\n"; + // ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); return id; } template <class Solver> ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, - ClauseKind kind) { + ClauseKind kind) { Debug("cores") << "registerUnitClause " << kind << std::endl; typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { @@ -519,59 +577,57 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " - << lit - << ". Explainer theory: " << d_cnfProof->getExplainerTheory() - << std::endl; + << lit + << std::endl; d_lemmaClauses.insert(newId); - d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; Assert(kind != INPUT || d_inputClauses.count(id)); Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); Debug("proof:sat:detailed") << "registerUnitClause id: " << id - <<" kind: " << kind << "\n"; + << " kind: " << kind << "\n"; // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); return id; } template <class Solver> void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) { - Assert (d_trueLit == ClauseIdUndef); + Assert(d_trueLit == ClauseIdUndef); d_trueLit = registerUnitClause(lit, INPUT); } template <class Solver> void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) { - Assert (d_falseLit == ClauseIdUndef); + Assert(d_falseLit == ClauseIdUndef); d_falseLit = registerUnitClause(lit, INPUT); } template <class Solver> ClauseId TSatProof<Solver>::getTrueUnit() const { - Assert (d_trueLit != ClauseIdUndef); + Assert(d_trueLit != ClauseIdUndef); return d_trueLit; } template <class Solver> ClauseId TSatProof<Solver>::getFalseUnit() const { - Assert (d_falseLit != ClauseIdUndef); + Assert(d_falseLit != ClauseIdUndef); return d_falseLit; } - template <class Solver> void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) { - Assert (d_assumptions.find(var) == d_assumptions.end()); + Assert(d_assumptions.find(var) == d_assumptions.end()); d_assumptions.insert(var); } template <class Solver> -ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TLitVec& confl) { +ClauseId TSatProof<Solver>::registerAssumptionConflict( + const typename Solver::TLitVec& confl) { Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; // Uniqueness is checked in the bit-vector proof // should be vars for (int i = 0; i < confl.size(); ++i) { - Assert (d_assumptions.find(var(confl[i])) != d_assumptions.end()); + Assert(d_assumptions.find(var(confl[i])) != d_assumptions.end()); } ClauseId new_id = ProofManager::currentPM()->nextId(); d_assumptionConflicts.insert(new_id); @@ -588,9 +644,10 @@ ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TL return new_id; } - template <class Solver> -void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { +void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, + LitSet* removedSet, LitVector& removeStack, + LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { return; @@ -604,20 +661,21 @@ void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, LitSet* removedSet } int size = getClause(reason_ref).size(); - for (int i = 1; i < size; i++ ) { + for (int i = 1; i < size; i++) { typename Solver::TLit v = getClause(reason_ref)[i]; - if(inClause.count(v) == 0 && seen.count(v) == 0) { + if (inClause.count(v) == 0 && seen.count(v) == 0) { removedDfs(v, removedSet, removeStack, inClause, seen); } } - if(seen.count(lit) == 0) { + if (seen.count(lit) == 0) { seen.insert(lit); removeStack.push_back(lit); } } template <class Solver> -void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, ClauseId id) { +void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, + ClauseId id) { LitSet* removed = res->getRedundant(); if (removed == NULL) { return; @@ -628,11 +686,12 @@ void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, ClauseId i LitVector removeStack; LitSet seen; - for (typename LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { + for (typename LitSet::iterator it = removed->begin(); it != removed->end(); + ++it) { removedDfs(*it, removed, removeStack, inClause, seen); } - for (int i = removeStack.size()-1; i >= 0; --i) { + for (int i = removeStack.size() - 1; i >= 0; --i) { typename Solver::TLit lit = removeStack[i]; typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); ClauseId reason_id; @@ -655,41 +714,50 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) { removeRedundantFromRes(res, id); Assert(res->redundantRemoved()); - d_resChains[id] = res; - if(Debug.isOn("proof:sat")) { + // Because the SAT solver can add the same clause multiple times, it + // could be the case that a resolution chain for this clause already + // exists (e.g. when removing units in addClause). + if (hasResolutionChain(id)) { + ResChain<Solver>* current = d_resolutionChains.find(id)->second; + delete current; + d_resolutionChains.erase(id); + } + Assert(!hasResolutionChain(id)); + + d_resolutionChains.insert(std::make_pair(id, res)); + if (Debug.isOn("proof:sat")) { printRes(id); } - if(d_checkRes) { + if (d_checkRes) { Assert(checkResolution(id)); } - PSTATS( - d_statistics.d_resChainLengths << ((uint64_t)res->getSteps().size()); - d_statistics.d_avgChainLength.addEntry((uint64_t)res->getSteps().size()); - ++(d_statistics.d_numLearnedClauses); - ) + PSTATS(uint64_t resolutionSteps = + static_cast<uint64_t>(res.getSteps().size()); + d_statistics.d_resChainLengths << resolutionSteps; + d_statistics.d_avgChainLength.addEntry(resolutionSteps); + ++(d_statistics.d_numLearnedClauses);) } - /// recording resolutions template <class Solver> void TSatProof<Solver>::startResChain(typename Solver::TCRef start) { - ClauseId id = getClauseId(start); - ResChain<Solver>* res = new ResChain<Solver>(id); + ClauseId id = getClauseIdForCRef(start); + ResolutionChain* res = new ResolutionChain(id); d_resStack.push_back(res); } template <class Solver> void TSatProof<Solver>::startResChain(typename Solver::TLit start) { ClauseId id = getUnitId(start); - ResChain<Solver>* res = new ResChain<Solver>(id); + ResolutionChain* res = new ResolutionChain(id); d_resStack.push_back(res); } - template <class Solver> void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit, - typename Solver::TCRef clause, bool sign) { + typename Solver::TCRef clause, + bool sign) { ClauseId id = registerClause(clause, LEARNT); ResChain<Solver>* res = d_resStack.back(); res->addStep(lit, id, sign); @@ -697,14 +765,13 @@ void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit, template <class Solver> void TSatProof<Solver>::endResChain(ClauseId id) { - Debug("proof:sat:detailed") <<"endResChain " << id << "\n"; + Debug("proof:sat:detailed") << "endResChain " << id << "\n"; Assert(d_resStack.size() > 0); ResChain<Solver>* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); } - // template <class Solver> // void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) { // Assert(d_resStack.size() > 0); @@ -718,25 +785,25 @@ template <class Solver> void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); ClauseId id = registerUnitClause(lit, LEARNT); - Debug("proof:sat:detailed") <<"endResChain unit " << id << "\n"; - ResChain<Solver>* res = d_resStack.back(); + Debug("proof:sat:detailed") << "endResChain unit " << id << "\n"; + ResolutionChain* res = d_resStack.back(); d_glueMap[id] = 1; registerResolution(id, res); d_resStack.pop_back(); } - template <class Solver> void TSatProof<Solver>::cancelResChain() { Assert(d_resStack.size() > 0); + ResolutionChain* back = d_resStack.back(); + delete back; d_resStack.pop_back(); } - template <class Solver> void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); - ResChain<Solver>* res = d_resStack.back(); + ResolutionChain* res = d_resStack.back(); res->addRedundantLit(lit); } @@ -755,9 +822,9 @@ void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) { template <class Solver> ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { // first check if we already have a resolution for lit - if(isUnit(lit)) { - ClauseId id = getClauseId(lit); - Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + if (isUnit(lit)) { + ClauseId id = getClauseIdForLiteral(lit); + Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id)); return id; } typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); @@ -768,12 +835,13 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { ResChain<Solver>* res = new ResChain<Solver>(reason_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload reason ptr each time. - typename Solver::TClause* reason = &getClause(reason_ref); - for (int i = 0; - i < reason->size(); - i++, reason = &getClause(reason_ref)) { - typename Solver::TLit l = (*reason)[i]; - if(lit != l) { + const typename Solver::TClause& initial_reason = getClause(reason_ref); + size_t current_reason_size = initial_reason.size(); + for (size_t i = 0; i < current_reason_size; i++) { + const typename Solver::TClause& current_reason = getClause(reason_ref); + current_reason_size = current_reason.size(); + typename Solver::TLit l = current_reason[i]; + if (lit != l) { ClauseId res_id = resolveUnit(~l); res->addStep(l, res_id, !sign(l)); } @@ -787,16 +855,19 @@ void TSatProof<Solver>::toStream(std::ostream& out) { Debug("proof:sat") << "TSatProof<Solver>::printProof\n"; Unimplemented("native proof printing not supported yet"); } + template <class Solver> -ClauseId TSatProof<Solver>::storeUnitConflict(typename Solver::TLit conflict_lit, - ClauseKind kind) { +ClauseId TSatProof<Solver>::storeUnitConflict( + typename Solver::TLit conflict_lit, ClauseKind kind) { Debug("cores") << "STORE UNIT CONFLICT" << std::endl; Assert(!d_storedUnitConflict); d_unitConflictId = registerUnitClause(conflict_lit, kind); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId + << "\n"; return d_unitConflictId; } + template <class Solver> void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { Assert(d_resStack.size() == 0); @@ -816,10 +887,10 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { return; } else { Assert(!d_storedUnitConflict); - conflict_id = registerClause(conflict_ref, LEARNT); //FIXME + conflict_id = registerClause(conflict_ref, LEARNT); // FIXME } - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof::finalizeProof Final Conflict "; print(conflict_id); } @@ -827,13 +898,13 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { ResChain<Solver>* res = new ResChain<Solver>(conflict_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. - typename Solver::TClause* conflict = &getClause(conflict_ref); - for (int i = 0; - i < conflict->size(); - ++i, conflict = &getClause(conflict_ref)) { - typename Solver::TLit lit = (*conflict)[i]; + size_t conflict_size = getClause(conflict_ref).size(); + for (size_t i = 0; i < conflict_size; ++i) { + const typename Solver::TClause& conflict = getClause(conflict_ref); + typename Solver::TLit lit = conflict[i]; ClauseId res_id = resolveUnit(~lit); res->addStep(lit, res_id, !sign(lit)); + conflict_size = conflict.size(); } registerResolution(d_emptyClauseId, res); } @@ -845,12 +916,13 @@ void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref, if (d_clauseId.find(oldref) == d_clauseId.end()) { return; } - ClauseId id = getClauseId(oldref); + ClauseId id = getClauseIdForCRef(oldref); Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); d_temp_clauseId[newref] = id; d_temp_idClause[id] = newref; } + template <class Solver> void TSatProof<Solver>::finishUpdateCRef() { d_clauseId.swap(d_temp_clauseId); @@ -859,10 +931,11 @@ void TSatProof<Solver>::finishUpdateCRef() { d_idClause.swap(d_temp_idClause); d_temp_idClause.clear(); } + template <class Solver> void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { - if (d_clauseId.find(clause) != d_clauseId.end()) { - ClauseId id = getClauseId(clause); + if (hasClauseIdForCRef(clause)) { + ClauseId id = getClauseIdForCRef(clause); Assert(d_deleted.find(id) == d_deleted.end()); d_deleted.insert(id); if (isLemmaClause(id)) { @@ -875,14 +948,13 @@ void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { } // template<> -// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, +// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& +// minisat_cl, // prop::SatClause& sat_cl) { // prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); // } - - template <class Solver> void TSatProof<Solver>::constructProof(ClauseId conflict) { collectClauses(conflict); @@ -894,11 +966,10 @@ std::string TSatProof<Solver>::clauseName(ClauseId id) { if (isInputClause(id)) { os << ProofManager::getInputClauseName(id, d_name); return os.str(); - } else - if (isLemmaClause(id)) { + } else if (isLemmaClause(id)) { os << ProofManager::getLemmaClauseName(id, d_name); return os.str(); - }else { + } else { os << ProofManager::getLearntClauseName(id, d_name); return os.str(); } @@ -944,17 +1015,15 @@ void TSatProof<Solver>::collectClauses(ClauseId id) { d_seenLearnt.insert(id); } - Assert(d_resChains.find(id) != d_resChains.end()); - ResChain<Solver>* res = d_resChains[id]; - PSTATS( - d_statistics.d_usedResChainLengths << ((uint64_t)res->getSteps().size()); - d_statistics.d_usedClauseGlue << ((uint64_t) d_glueMap[id]); - ); - ClauseId start = res->getStart(); + const ResolutionChain& res = getResolutionChain(id); + const typename ResolutionChain::ResSteps& steps = res.getSteps(); + PSTATS(d_statistics.d_usedResChainLengths + << ((uint64_t)steps.size()); + d_statistics.d_usedClauseGlue << ((uint64_t)d_glueMap[id]);); + ClauseId start = res.getStart(); collectClauses(start); - typename ResChain<Solver>::ResSteps steps = res->getSteps(); - for(size_t i = 0; i < steps.size(); i++) { + for (size_t i = 0; i < steps.size(); i++) { collectClauses(steps[i].id); } } @@ -964,28 +1033,27 @@ void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas) { inputs = d_seenInputs; lemmas = d_seenLemmas; - PSTATS ( - d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); - d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size()); - ); + PSTATS(d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); + d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size());); } template <class Solver> void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) { - Assert (d_glueMap.find(clause) == d_glueMap.end()); + Assert(d_glueMap.find(clause) == d_glueMap.end()); d_glueMap.insert(std::make_pair(clause, glue)); } template <class Solver> TSatProof<Solver>::Statistics::Statistics(const std::string& prefix) - : d_numLearnedClauses("satproof::"+prefix+"::NumLearnedClauses", 0) - , d_numLearnedInProof("satproof::"+prefix+"::NumLearnedInProof", 0) - , d_numLemmasInProof("satproof::"+prefix+"::NumLemmasInProof", 0) - , d_avgChainLength("satproof::"+prefix+"::AvgResChainLength") - , d_resChainLengths("satproof::"+prefix+"::ResChainLengthsHist") - , d_usedResChainLengths("satproof::"+prefix+"::UsedResChainLengthsHist") - , d_clauseGlue("satproof::"+prefix+"::ClauseGlueHist") - , d_usedClauseGlue("satproof::"+prefix+"::UsedClauseGlueHist") { + : d_numLearnedClauses("satproof::" + prefix + "::NumLearnedClauses", 0), + d_numLearnedInProof("satproof::" + prefix + "::NumLearnedInProof", 0), + d_numLemmasInProof("satproof::" + prefix + "::NumLemmasInProof", 0), + d_avgChainLength("satproof::" + prefix + "::AvgResChainLength"), + d_resChainLengths("satproof::" + prefix + "::ResChainLengthsHist"), + d_usedResChainLengths("satproof::" + prefix + + "::UsedResChainLengthsHist"), + d_clauseGlue("satproof::" + prefix + "::ClauseGlueHist"), + d_usedClauseGlue("satproof::" + prefix + "::UsedClauseGlueHist") { smtStatisticsRegistry()->registerStat(&d_numLearnedClauses); smtStatisticsRegistry()->registerStat(&d_numLearnedInProof); smtStatisticsRegistry()->registerStat(&d_numLemmasInProof); @@ -1008,73 +1076,78 @@ TSatProof<Solver>::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); } - /// LFSCSatProof class template <class Solver> -void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { +void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, + std::ostream& paren) { out << "(satlem_simplify _ _ _ "; - ResChain<Solver>* res = this->d_resChains[id]; - typename ResChain<Solver>::ResSteps& steps = res->getSteps(); + const ResChain<Solver>& res = this->getResolutionChain(id); + const typename ResChain<Solver>::ResSteps& steps = res.getSteps(); - for (int i = steps.size()-1; i >= 0; i--) { + for (int i = steps.size() - 1; i >= 0; i--) { out << "("; - out << (steps[i].sign? "R" : "Q") << " _ _ "; + out << (steps[i].sign ? "R" : "Q") << " _ _ "; } - ClauseId start_id = res->getStart(); + ClauseId start_id = res.getStart(); out << this->clauseName(start_id) << " "; - for(unsigned i = 0; i < steps.size(); i++) { - prop::SatVariable v = prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); - out << this->clauseName(steps[i].id) << " "<<ProofManager::getVarName(v, this->d_name) <<")"; + for (unsigned i = 0; i < steps.size(); i++) { + prop::SatVariable v = + prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); + out << this->clauseName(steps[i].id) << " " + << ProofManager::getVarName(v, this->d_name) << ")"; } if (id == this->d_emptyClauseId) { - out <<"(\\empty empty)"; + out <<"(\\ empty empty)"; return; } - out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name + out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name paren << "))"; // closing parethesis for lemma binding and satlem } /// LFSCSatProof class template <class Solver> -void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) { - Assert (this->isAssumptionConflict(id)); +void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, + std::ostream& out, + std::ostream& paren) { + Assert(this->isAssumptionConflict(id)); // print the resolution proving the assumption conflict printResolution(id, out, paren); // resolve out assumptions to prove empty clause out << "(satlem_simplify _ _ _ "; - std::vector<typename Solver::TLit>& confl = *(this->d_assumptionConflictsDebug[id]); + std::vector<typename Solver::TLit>& confl = + *(this->d_assumptionConflictsDebug[id]); - Assert (confl.size()); + Assert(confl.size()); for (unsigned i = 0; i < confl.size(); ++i) { prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]); - out <<"("; - out << (lit.isNegated() ? "Q" : "R") <<" _ _ "; + out << "("; + out << (lit.isNegated() ? "Q" : "R") << " _ _ "; } - out << this->clauseName(id)<< " "; + out << this->clauseName(id) << " "; for (int i = confl.size() - 1; i >= 0; --i) { prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]); prop::SatVariable v = lit.getSatVariable(); - out << "unit"<< v <<" "; - out << ProofManager::getVarName(v, this->d_name) <<")"; + out << "unit" << v << " "; + out << ProofManager::getVarName(v, this->d_name) << ")"; } - out <<"(\\ e e)\n"; - paren <<")"; + out << "(\\ e e)\n"; + paren << ")"; } - template <class Solver> -void LFSCSatProof<Solver>::printResolutions(std::ostream& out, std::ostream& paren) { +void LFSCSatProof<Solver>::printResolutions(std::ostream& out, + std::ostream& paren) { Debug("bv-proof") << "; print resolutions" << std::endl; std::set<ClauseId>::iterator it = this->d_seenLearnt.begin(); - for(; it!= this->d_seenLearnt.end(); ++it) { - if(*it != this->d_emptyClauseId) { + for (; it != this->d_seenLearnt.end(); ++it) { + if (*it != this->d_emptyClauseId) { Debug("bv-proof") << "; print resolution for " << *it << std::endl; printResolution(*it, out, paren); } @@ -1083,29 +1156,29 @@ void LFSCSatProof<Solver>::printResolutions(std::ostream& out, std::ostream& par } template <class Solver> -void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out, std::ostream& paren) { +void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out, + std::ostream& paren) { printResolution(this->d_emptyClauseId, out, paren); } - inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { - switch(k) { - case CVC4::INPUT: - out << "INPUT"; - break; - case CVC4::THEORY_LEMMA: - out << "THEORY_LEMMA"; - break; - case CVC4::LEARNT: - out << "LEARNT"; - break; - default: - out << "ClauseKind Unknown! [" << unsigned(k) << "]"; + switch (k) { + case CVC4::INPUT: + out << "INPUT"; + break; + case CVC4::THEORY_LEMMA: + out << "THEORY_LEMMA"; + break; + case CVC4::LEARNT: + out << "LEARNT"; + break; + default: + out << "ClauseKind Unknown! [" << unsigned(k) << "]"; } return out; } -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */ diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h index de510e514..b026e21c2 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -37,7 +37,6 @@ public: Node getSkolem(Node disequality); Node getDisequality(Node skolem); bool isSkolem(Node skolem); - void clear(); std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin(); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 088275b3f..d12b561a6 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -19,12 +19,14 @@ #include "base/cvc4_assert.h" #include "context/context.h" #include "options/bv_options.h" +#include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" #include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof.h" #include "proof/uf_proof.h" @@ -45,77 +47,9 @@ namespace CVC4 { -unsigned CVC4::LetCount::counter = 0; +unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; -//for proof replay -class ProofOutputChannel : public theory::OutputChannel { -public: - Node d_conflict; - Proof* d_proof; - Node d_lemma; - - ProofOutputChannel() : d_conflict(), d_proof(NULL) {} - virtual ~ProofOutputChannel() throw() {} - - void conflict(TNode n, Proof* pf) throw() { - Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl; - Assert(d_conflict.isNull()); - Assert(!n.isNull()); - d_conflict = n; - Assert(pf != NULL); - d_proof = pf; - } - bool propagate(TNode x) throw() { - Trace("theory-proof-debug") << "got a propagation: " << x << std::endl; - return true; - } - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { - Trace("theory-proof-debug") << "new lemma: " << n << std::endl; - d_lemma = n; - return theory::LemmaStatus(TNode::null(), 0); - } - theory::LemmaStatus splitLemma(TNode, bool) throw() { - AlwaysAssert(false); - return theory::LemmaStatus(TNode::null(), 0); - } - void requirePhase(TNode n, bool b) throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl; - Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl; - } - bool flipDecision() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl; - AlwaysAssert(false); - return false; - } - void setIncomplete() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl; - AlwaysAssert(false); - } -};/* class ProofOutputChannel */ - -//for proof replay -class MyPreRegisterVisitor { - theory::Theory* d_theory; - __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited; -public: - typedef void return_type; - MyPreRegisterVisitor(theory::Theory* theory) - : d_theory(theory) - , d_visited() - {} - bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); } - void visit(TNode current, TNode parent) { - if(theory::Theory::theoryOf(current) == d_theory->getId()) { - //Trace("theory-proof-debug") << "preregister " << current << std::endl; - d_theory->preRegisterTerm(current); - d_visited.insert(current); - } - } - void start(TNode node) { } - void done(TNode node) { } -}; /* class MyPreRegisterVisitor */ - TheoryProofEngine::TheoryProofEngine() : d_registrationCache() , d_theoryProofTable() @@ -131,13 +65,12 @@ TheoryProofEngine::~TheoryProofEngine() { } } - void TheoryProofEngine::registerTheory(theory::Theory* th) { - if( th ){ + if (th) { theory::TheoryId id = th->getId(); if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) { - Trace("theory-proof-debug") << "; register theory " << id << std::endl; + Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; if (id == theory::THEORY_UF) { d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); @@ -147,7 +80,6 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { if (id == theory::THEORY_BV) { BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); d_theoryProofTable[id] = bvp; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); return; } @@ -166,20 +98,54 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } } +void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { + if (th) { + theory::TheoryId id = th->getId(); + if (id == theory::THEORY_BV) { + Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); + + BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + return; + } + } +} + TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { + // The UF theory handles queries for the Builtin theory. + if (id == theory::THEORY_BUILTIN) { + Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl; + id = theory::THEORY_UF; + } + Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end()); return d_theoryProofTable[id]; } +void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) { + d_exprToTheoryIds[term].insert(id); +} + +void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + Assert(c1.isConst()); + Assert(c2.isConst()); + + Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2)); + getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2); +} + void TheoryProofEngine::registerTerm(Expr term) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; + if (d_registrationCache.count(term)) { return; } - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl; + + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; + Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -193,58 +159,64 @@ void TheoryProofEngine::registerTerm(Expr term) { if (!supportedTheory(theory_id)) return; + // Register the term with its owner theory getTheoryProof(theory_id)->registerTerm(term); + + // A special case: the array theory needs to know of every skolem, even if + // it belongs to another theory (e.g., a BV skolem) + if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl; + getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term); + } + d_registrationCache.insert(term); } -theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { +theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) { ProofManager* pm = ProofManager::currentPM(); - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" - << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + std::set<Node> nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } - if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) { - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. " - << "Returning THEORY_ARITH" << std::endl; - return theory::THEORY_ARITH; + nodes.insert(lit.isNegated() ? node.notNode() : node); } - return pm->getCnfProof()->getOwnerTheory(id); - - // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; - // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; - // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY; - // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; - - // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl; - - // Unreachable(); + // Ensure that the lemma is in the database. + Assert (pm->getCnfProof()->haveProofRecipe(nodes)); + return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); } -void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { - LetMap::iterator it = map.find(term); +void LFSCTheoryProofEngine::bind(Expr term, ProofLetMap& map, Bindings& let_order) { + ProofLetMap::iterator it = map.find(term); if (it != map.end()) { - LetCount& count = it->second; + ProofLetCount& count = it->second; count.increment(); return; } for (unsigned i = 0; i < term.getNumChildren(); ++i) { bind(term[i], map, let_order); } - unsigned new_id = LetCount::newId(); - map[term] = LetCount(new_id); + unsigned new_id = ProofLetCount::newId(); + map[term] = ProofLetCount(new_id); let_order.push_back(LetOrderElement(term, new_id)); } void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { - LetMap map; + ProofLetMap map; Bindings let_order; bind(term, map, let_order); std::ostringstream paren; for (unsigned i = 0; i < let_order.size(); ++i) { Expr current_expr = let_order[i].expr; unsigned let_id = let_order[i].id; - LetMap::const_iterator it = map.find(current_expr); + ProofLetMap::const_iterator it = map.find(current_expr); Assert (it != map.end()); unsigned let_count = it->second.count; Assert(let_count); @@ -253,7 +225,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { continue; } - os << "(@ let"<<let_id << " "; + os << "(@ let" <<let_id << " "; printTheoryTerm(current_expr, os, map); paren <<")"; } @@ -264,16 +236,13 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { printTheoryTerm(last, os, map); } else { - os << " let"<< last_let_id; + os << " let" << last_let_id; } os << paren.str(); } - -void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) { theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term - << ", theory_id = " << theory_id << std::endl; // boolean terms and ITEs are special because they // are common to all theories @@ -315,6 +284,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) { Unreachable(); } +void LFSCTheoryProofEngine::performExtraRegistrations() { + ExprToTheoryIds::const_iterator it; + for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) { + if (d_registrationCache.count(it->first)) { // Only register if the term appeared + TheoryIdSet::const_iterator theoryIt; + for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) { + Debug("pf::tp") << "\tExtra registration of term " << it->first + << " with theory: " << *theoryIt << std::endl; + Assert(supportedTheory(*theoryIt)); + getTheoryProof(*theoryIt)->registerTerm(it->first); + } + } + } +} + +void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) { + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->treatBoolsAsFormulas(value); + } +} + void LFSCTheoryProofEngine::registerTermsFromAssertions() { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); @@ -322,6 +314,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } + + performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -333,17 +327,51 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - // FIXME: merge this with counter - os << "(% A" << counter++ << " (th_holds "; - printLetTerm(*it, os); + std::ostringstream name; + name << "A" << counter++; + os << "(% " << name.str() << " (th_holds "; + + // Assertions appear before the global let map, so we use a dummpMap to avoid letification here. + ProofLetMap dummyMap; + printBoundTerm(*it, os, dummyMap); + os << ")\n"; paren << ")"; } - //store map between assertion and counter - // ProofManager::currentPM()->setAssertion( *it ); + Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl; } +void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, + std::ostream& os, + std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl; + + NodePairSet::const_iterator it; + + for (it = rewrites.begin(); it != rewrites.end(); ++it) { + Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl; + + Node n1 = it->first; + Node n2 = it->second; + Assert(n1.toExpr() == utils::mkFalse() || + theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + + std::ostringstream rewriteRule; + rewriteRule << ".lrr" << d_assertionToRewrite.size(); + + os << "(th_let_pf _ "; + getTheoryProof(theory::Theory::theoryOf(n1))->printRewriteProof(os, n1, n2); + os << "(\\ " << rewriteRule.str() << "\n"; + + d_assertionToRewrite[it->first] = rewriteRule.str(); + Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl; + paren << "))"; + } + + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl; +} + void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl; @@ -378,55 +406,150 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost } } -void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, - std::ostream& paren) { - os << " ;; Theory Lemmas \n"; - ProofManager* pm = ProofManager::currentPM(); - IdToSatClause::const_iterator it = lemmas.begin(); - IdToSatClause::const_iterator end = lemmas.end(); - - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; +void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl; + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; - ClauseId id = it->first; - Debug("pf::tp") << "\tLemma = " << id - << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + it->second->printAliasingDeclarations(os, paren); } - it = lemmas.begin(); +} - // BitVector theory is special case: must know all - // conflicts needed ahead of time for resolution - // proof lemmas - std::vector<Expr> bv_lemmas; - for (; it != end; ++it) { +void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { + Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl; + + ProofManager* pm = ProofManager::currentPM(); + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; + Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl; const prop::SatClause* clause = it->second; + std::set<Node> nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + if (node.isConst()) { + Assert (node.toExpr() == utils::mkTrue()); + continue; + } + nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); + recipe.dump("pf::dumpLemmas"); + } + + Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl; +} - theory::TheoryId theory_id = getTheoryForLemma(id); - if (theory_id != theory::THEORY_BV) continue; +// TODO: this function should be moved into the BV prover. +void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os) { + // BitVector theory is special case: must know all conflicts needed + // ahead of time for resolution proof lemmas + std::vector<Expr> bv_lemmas; + + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + const prop::SatClause* clause = it->second; std::vector<Expr> conflict; + std::set<Node> conflictNodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + + // The literals (true) and (not false) are omitted from conflicts if (atom.isConst()) { Assert (atom == utils::mkTrue() || (atom == utils::mkFalse() && lit.isNegated())); continue; } + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; conflict.push_back(expr_lit); + conflictNodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes); + + unsigned numberOfSteps = recipe.getNumSteps(); + + prop::SatClause currentClause = *clause; + std::vector<Expr> currentClauseExpr = conflict; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + if (currentStep->getTheory() != theory::THEORY_BV) { + continue; + } + + // If any rewrites took place, we need to update the conflict clause accordingly + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i); + std::map<Node, Node> explanationToMissingAssertion; + std::set<Node>::iterator assertionIt; + for (assertionIt = missingAssertions.begin(); + assertionIt != missingAssertions.end(); + ++assertionIt) { + Node negated = (*assertionIt).negate(); + explanationToMissingAssertion[recipe.getExplanation(negated)] = negated; + } + + currentClause = *clause; + currentClauseExpr = conflict; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + + // If this literal is the result of a rewrite, we need to translate it + if (explanationToMissingAssertion.find(previousLiteralNode) != + explanationToMissingAssertion.end()) { + previousLiteralNode = explanationToMissingAssertion[previousLiteralNode]; + } + + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If we're in the final step, the last literal is Null and should not be added. + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr)); } - bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict)); } - // FIXME: ugly, move into bit-vector proof by adding lemma - // queue inside each theory_proof + BitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); + // bv->printResolutionProof(os, paren, letMap); +} - bv->printResolutionProof(os, paren); +void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren, + ProofLetMap& map) { + os << " ;; Theory Lemmas \n"; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl; + + if (Debug.isOn("pf::dumpLemmas")) { + dumpTheoryLemmas(lemmas); + } + + // finalizeBvConflicts(lemmas, os, paren, map); + ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -434,61 +557,255 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, return; } - it = lemmas.begin(); - + ProofManager* pm = ProofManager::currentPM(); Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; - for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl; - - // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl; + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; - Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl; const prop::SatClause* clause = it->second; - // printing clause as it appears in resolution proof - os << "(satlem _ _ "; - std::ostringstream clause_paren; - Debug("pf::tp") << "CnfProof printing clause..." << std::endl; - pm->getCnfProof()->printClause(*clause, os, clause_paren); - Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = " + << id << std::endl; std::vector<Expr> clause_expr; + std::set<Node> clause_expr_nodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); if (atom.isConst()) { Assert (atom == utils::mkTrue()); continue; } Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; clause_expr.push_back(expr_lit); + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); } - Debug("pf::tp") << "Expression printing done!" << std::endl; - - // query appropriate theory for proof of clause - theory::TheoryId theory_id = getTheoryForLemma(id); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; - Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl; - getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; - // os << " (clausify_false trust)"; - os << clause_paren.str(); - os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; - paren << "))"; + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes); + + if (recipe.simpleLemma()) { + // In a simple lemma, there will be no propositional resolution in the end + + Debug("pf::tp") << "Simple lemma" << std::endl; + // Printing the clause as it appears in resolution proof + os << "(satlem _ _ "; + std::ostringstream clause_paren; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + + // Find and handle missing assertions, due to rewrites + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl; + } + + std::set<Node>::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < clause_expr.size(); ++k) { + if (clause_expr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + AlwaysAssert(found); + Debug("pf::tp") << "Replacing theory assertion " + << clause_expr[k] + << " with " + << *missingAssertion + << std::endl; + + clause_expr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + // Query the appropriate theory for a proof of this clause + theory::TheoryId theory_id = getTheoryForLemma(clause); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren, map); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; + paren << "))"; + } else { // This is a composite lemma + + unsigned numberOfSteps = recipe.getNumSteps(); + prop::SatClause currentClause = *clause; + std::vector<Expr> currentClauseExpr = clause_expr; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + currentClause = *clause; + currentClauseExpr = clause_expr; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If the current literal is NULL, can ignore (final step) + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + os << "(satlem _ _ "; + std::ostringstream clause_paren; + + pm->getCnfProof()->printClause(currentClause, os, clause_paren); + + // query appropriate theory for proof of clause + theory::TheoryId theory_id = currentStep->getTheory(); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this step!" << std::endl; + } + + // Turn rewrite filter ON + std::set<Node>::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < currentClauseExpr.size(); ++k) { + if (currentClauseExpr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + AlwaysAssert(found); + + Debug("pf::tp") << "Replacing theory assertion " + << currentClauseExpr[k] + << " with " + << *missingAssertion + << std::endl; + + currentClauseExpr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren, map); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n"; + paren << "))"; + } + + Assert(numberOfSteps >= 2); + + os << "(satlem_simplify _ _ _ "; + for (unsigned i = 0; i < numberOfSteps - 1; ++i) { + // Resolve step i with step i + 1 + if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) { + os << "(Q _ _ "; + } else { + os << "(R _ _ "; + } + + os << pm->getLemmaClauseName(id) << "s" << i; + os << " "; + } + + os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " "; + + prop::SatLiteral v; + for (int i = numberOfSteps - 2; i >= 0; --i) { + v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral()); + os << ProofManager::getVarName(v.getSatVariable(), "") << ") "; + } + + os << "( \\ " << pm->getLemmaClauseName(id) << "\n"; + paren << "))"; + } } } -void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { - // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; +void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; - LetMap::const_iterator it = map.find(term); + ProofLetMap::const_iterator it = map.find(term); if (it != map.end()) { unsigned id = it->second.id; unsigned count = it->second.count; + if (count > LET_COUNT) { - os <<"let"<<id; + os << "let" << id; return; } } @@ -496,7 +813,7 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Le printTheoryTerm(term, os, map); } -void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) { if (term.isVariable()) { os << ProofManager::sanitize(term); return; @@ -596,20 +913,25 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let } -void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { - //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory - Assert( d_theory!=NULL ); +void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) { + // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory + Assert(d_theory!=NULL); + context::UserContext fakeContext; ProofOutputChannel oc; theory::Valuation v(NULL); //make new copy of theory theory::Theory* th; - Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; - if(d_theory->getId()==theory::THEORY_UF) { + Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; + + if (d_theory->getId()==theory::THEORY_UF) { th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); - } else if(d_theory->getId()==theory::THEORY_ARRAY) { + } else if (d_theory->getId()==theory::THEORY_ARRAY) { th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); @@ -626,11 +948,15 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl; MyPreRegisterVisitor preRegVisitor(th); - for( unsigned i=0; i<lemma.size(); i++ ){ - Node lit = Node::fromExpr( lemma[i] ).negate(); - Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; - NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit); - th->assertFact(lit, false); + for (unsigned i=0; i<lemma.size(); i++) { + Node strippedLit = (lemma[i].getKind() == kind::NOT) ? lemma[i][0] : lemma[i]; + if (strippedLit.getKind() == kind::EQUAL || + d_theory->getId() == theory::Theory::theoryOf(strippedLit)) { + Node lit = Node::fromExpr( lemma[i] ).negate(); + Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; + NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit); + th->assertFact(lit, false); + } } Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl; @@ -679,7 +1005,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& th->check(theory::Theory::EFFORT_FULL); } Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; - oc.d_proof->toStream(os); + oc.d_proof->toStream(os, map); Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl; @@ -711,10 +1037,13 @@ void BooleanProof::registerTerm(Expr term) { } } -void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - os << "(p_app " << ProofManager::sanitize(term) <<")"; + if (d_treatBoolsAsFormulas) + os << "(p_app " << ProofManager::sanitize(term) <<")"; + else + os << ProofManager::sanitize(term); return; } @@ -722,6 +1051,32 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& switch(k) { case kind::OR: case kind::AND: + if (options::lfscLetification() && term.getNumChildren() > 2) { + // If letification is on, the entire term is probably a let expression. + // However, we need to transform it from (and a b c) into (and a (and b c)) form first. + Node currentExpression = term[term.getNumChildren() - 1]; + for (int i = term.getNumChildren() - 2; i >= 0; --i) { + NodeBuilder<> builder(k); + builder << term[i]; + builder << currentExpression.toExpr(); + currentExpression = builder; + } + + // The let map should already have the current expression. + ProofLetMap::const_iterator it = map.find(term); + if (it != map.end()) { + unsigned id = it->second.id; + unsigned count = it->second.count; + + if (count > LET_COUNT) { + os << "let" << id; + break; + } + } + } + + // If letification is off or there were 2 children, same treatment as the other cases. + // (No break is intentional). case kind::XOR: case kind::IFF: case kind::IMPLIES: @@ -753,7 +1108,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& return; case kind::CONST_BOOLEAN: - os << (term.getConst<bool>() ? "true" : "false"); + if (d_treatBoolsAsFormulas) + os << (term.getConst<bool>() ? "true" : "false"); + else + os << (term.getConst<bool>() ? "t_true" : "t_false"); return; default: @@ -786,10 +1144,36 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream& // Nothing to do here at this point. } +void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { Unreachable("No boolean lemmas yet!"); } +void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + // By default, we just print a trust statement. Specific theories can implement + // better proofs. + ProofLetMap emptyMap; + + os << "(trust_f (not (= _ "; + d_proofEngine->printBoundTerm(c1, os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(c2, os, emptyMap); + os << ")))"; +} + +void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) { + // This is the default for a rewrite proof: just a trust statement. + ProofLetMap emptyMap; + os << "(trust_f (iff "; + d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap); + os << "))"; +} + } /* namespace CVC4 */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 54c86f3f3..5907f9bd5 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -27,6 +27,7 @@ #include "proof/clause_id.h" #include "prop/sat_solver_types.h" #include "util/proof.h" +#include "proof/proof_utils.h" namespace CVC4 { @@ -34,66 +35,21 @@ namespace theory { class Theory; } /* namespace CVC4::theory */ -struct LetCount { - static unsigned counter; - static void resetCounter() { counter = 0; } - static unsigned newId() { return ++counter; } - - unsigned count; - unsigned id; - LetCount() - : count(0) - , id(-1) - {} - - void increment() { ++count; } - LetCount(unsigned i) - : count(1) - , id(i) - {} - LetCount(const LetCount& other) - : count(other.count) - , id (other.id) - {} - bool operator==(const LetCount &other) const { - return other.id == id && other.count == count; - } - LetCount& operator=(const LetCount &rhs) { - if (&rhs == this) return *this; - id = rhs.id; - count = rhs.count; - return *this; - } -}; - -struct LetOrderElement { - Expr expr; - unsigned id; - LetOrderElement(Expr e, unsigned i) - : expr(e) - , id(i) - {} - - LetOrderElement() - : expr() - , id(-1) - {} -}; - typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; -typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap; -typedef std::vector<LetOrderElement> Bindings; - class TheoryProof; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable; +typedef std::set<theory::TheoryId> TheoryIdSet; +typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds; + class TheoryProofEngine { protected: ExprSet d_registrationCache; TheoryProofTable d_theoryProofTable; + ExprToTheoryIds d_exprToTheoryIds; /** * Returns whether the theory is currently supported in proof @@ -113,7 +69,7 @@ public: */ virtual void printLetTerm(Expr term, std::ostream& os) = 0; virtual void printBoundTerm(Expr term, std::ostream& os, - const LetMap& map) = 0; + const ProofLetMap& map) = 0; /** * Print the proof representation of the given sort. @@ -148,6 +104,14 @@ public: virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; /** + * Print aliasing declarations. + * + * @param os + * @param paren closing parenthesis + */ + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; + + /** * Print proofs of all the theory lemmas (must prove * actual clause used in resolution proof). * @@ -155,7 +119,7 @@ public: * @param paren */ virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, - std::ostream& paren) = 0; + std::ostream& paren, ProofLetMap& map) = 0; /** * Register theory atom (ensures all terms and atoms are declared). @@ -166,35 +130,67 @@ public: /** * Ensures that a theory proof class for the given theory is created. + * This method can be invoked regardless of whether the "proof" option + * has been set. * * @param theory */ void registerTheory(theory::Theory* theory); + /** + * Additional configuration of the theory proof class for the given theory. + * This method should only be invoked when the "proof" option has been set. + * + * @param theory + */ + void finishRegisterTheory(theory::Theory* theory); - theory::TheoryId getTheoryForLemma(ClauseId id); + theory::TheoryId getTheoryForLemma(const prop::SatClause* clause); TheoryProof* getTheoryProof(theory::TheoryId id); + + void markTermForFutureRegistration(Expr term, theory::TheoryId id); + + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + + virtual void treatBoolsAsFormulas(bool value) {}; + + virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; }; class LFSCTheoryProofEngine : public TheoryProofEngine { - LetMap d_letMap; - void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map); - void bind(Expr term, LetMap& map, Bindings& let_order); + void bind(Expr term, ProofLetMap& map, Bindings& let_order); public: LFSCTheoryProofEngine() : TheoryProofEngine() {} + void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map); + void registerTermsFromAssertions(); void printSortDeclarations(std::ostream& os, std::ostream& paren); void printTermDeclarations(std::ostream& os, std::ostream& paren); - virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printLetTerm(Expr term, std::ostream& os); - virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printAssertions(std::ostream& os, std::ostream& paren); + virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, - std::ostream& paren); + std::ostream& paren, + ProofLetMap& map); virtual void printSort(Type type, std::ostream& os); + + void performExtraRegistrations(); + + void treatBoolsAsFormulas(bool value); + void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os); + +private: + static void dumpTheoryLemmas(const IdToSatClause& lemmas); + + // TODO: this function should be moved into the BV prover. + + std::map<Node, std::string> d_assertionToRewrite; }; class TheoryProof { @@ -214,7 +210,7 @@ public: * @param term expresion representing term * @param os output stream */ - void printTerm(Expr term, std::ostream& os, const LetMap& map) { + void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) { d_proofEngine->printBoundTerm(term, os, map); } /** @@ -223,7 +219,7 @@ public: * @param term expresion representing term * @param os output stream */ - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; /** * Print the proof representation of the given type that belongs to some theory. * @@ -246,7 +242,10 @@ public: * * @param os output stream */ - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map); /** * Print the sorts declarations for this theory. * @@ -270,11 +269,32 @@ public: */ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; /** + * Print any aliasing declarations. + * + * @param os + * @param paren + */ + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** * Register a term of this theory that appears in the proof. * * @param term */ virtual void registerTerm(Expr term) = 0; + /** + * Print a proof for the disequality of two constants that belong to this theory. + * + * @param term + */ + virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + /** + * Print a proof for the equivalence of n1 and n2. + * + * @param term + */ + virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); + + virtual void treatBoolsAsFormulas(bool value) {} }; class BooleanProof : public TheoryProof { @@ -285,26 +305,35 @@ public: virtual void registerTerm(Expr term); - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; virtual void printOwnedSort(Type type, std::ostream& os) = 0; virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0; virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; }; class LFSCBooleanProof : public BooleanProof { public: LFSCBooleanProof(TheoryProofEngine* proofEngine) - : BooleanProof(proofEngine) + : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); + + void treatBoolsAsFormulas(bool value) { + d_treatBoolsAsFormulas = value; + } + +private: + bool d_treatBoolsAsFormulas; }; } /* CVC4 namespace */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 32ca122b0..139ce5ed2 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -67,13 +67,17 @@ inline static bool match(TNode n1, TNode n2) { void ProofUF::toStream(std::ostream& out) { + ProofLetMap map; + toStream(out, map); +} + +void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) { Trace("theory-proof-debug") << "; Print UF proof..." << std::endl; //AJR : carry this further? - LetMap map; toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map); } -void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) { +void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) { Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl; Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl; pf->debug_print("lfsc-uf"); @@ -81,12 +85,21 @@ void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqPr toStreamRecLFSC( out, tp, pf, 0, map ); } -Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) { +Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) { Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; pf->debug_print("pf::uf"); Debug("pf::uf") << std::endl; - if(tb == 0) { + if (tb == 0) { + // Special case: false was an input, so the proof is just "false". + if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY && + pf->d_node == NodeManager::currentNM()->mkConst(false)) { + out << "(clausify_false "; + out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode()); + out << ")" << std::endl; + return Node(); + } + Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); Assert(pf->d_children.size() >= 2); @@ -190,42 +203,71 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ++i; } } - Assert(neg >= 0); + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) { + Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; + Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + Assert(pf->d_node.getNumChildren() == 2); + Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + } Node n1; std::stringstream ss; - //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + + if(!disequalityFound || subTrans.d_children.size() >= 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - out << "(clausify_false (contra _ "; Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; - Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } + out << "(clausify_false (contra _ "; - if(n2[0].getKind() == kind::APPLY_UF) { - out << "(trans _ _ _ _ "; - out << "(symm _ _ _ "; - out << ss.str(); - out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; - } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); - if(n1[1] == n2[0][0]) { - out << "(symm _ _ _ " << ss.str() << ")"; + if (disequalityFound) { + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("pf::uf") << "n2 is " << n2[0] << std::endl; + + if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } + + if(n2[0].getKind() == kind::APPLY_UF) { + out << "(trans _ _ _ _ "; + + if (n1[0] == n2[0]) { + out << "(symm _ _ _ "; + out << ss.str(); + out << ") "; + } else { + Assert(n1[1] == n2[0]); + out << ss.str(); + } + out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; } else { - out << ss.str(); + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + if(n1[1] == n2[0][0]) { + out << "(symm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + } else { + Node n2 = pf->d_node; + Assert(n2.getKind() == kind::EQUAL); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + + out << ss.str(); + out << " "; + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr()); + out << "))" << std::endl; } + return Node(); } @@ -584,10 +626,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { - n1 = n1[1]; + n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0]; + n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); @@ -595,16 +637,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { - n1 = n2[1]; + n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0]; + n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); } } else { - // Both n1 and n2 are prediacates. Don't know what to do... + // Both n1 and n2 are predicates. Don't know what to do... Unreachable(); } @@ -655,7 +697,7 @@ void UFProof::registerTerm(Expr term) { } } -void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF); @@ -667,6 +709,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) } Assert (term.getKind() == kind::APPLY_UF); + d_proofEngine->treatBoolsAsFormulas(false); if(term.getType().isBoolean()) { os << "(p_app "; @@ -683,6 +726,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) if(term.getType().isBoolean()) { os << ")"; } + d_proofEngine->treatBoolsAsFormulas(true); } void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { @@ -692,14 +736,14 @@ void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { os << type <<" "; } -void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { +void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { os << " ;; UF Theory Lemma \n;;"; for (unsigned i = 0; i < lemma.size(); ++i) { os << lemma[i] <<" "; } os <<"\n"; //os << " (clausify_false trust)"; - UFProof::printTheoryLemmaProof( lemma, os, paren ); + UFProof::printTheoryLemmaProof(lemma, os, paren, map); } void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { @@ -714,6 +758,8 @@ void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms + Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl; + for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { Expr term = *it; @@ -729,7 +775,8 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { os << "(arrow"; for (unsigned i = 0; i < args.size(); i++) { Type arg_type = args[i]; - os << " " << arg_type; + os << " "; + d_proofEngine->printSort(arg_type, os); if (i < args.size() - 2) { os << " (arrow"; fparen << ")"; @@ -742,10 +789,16 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { } paren << ")"; } + + Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl; } void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { // Nothing to do here at this point. } +void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* namespace CVC4 */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index e359eaebd..444b602dc 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -28,13 +28,14 @@ namespace CVC4 { //proof object outputted by TheoryUF class ProofUF : public Proof { private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map); + static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); public: ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {} //it is simply an equality engine proof theory::eq::EqProof * d_proof; void toStream(std::ostream& out); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map); + void toStream(std::ostream& out, const ProofLetMap& map); + static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); }; @@ -63,12 +64,13 @@ public: LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) : UFProof(uf, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; |