From: Guy Date: Wed, 8 Jun 2016 18:52:42 +0000 (-0700) Subject: Support for printing a global let map in LFSC proofs. X-Git-Tag: cvc5-1.0.0~6049^2~10 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b8f92d23f7a75b4148f41e039f7bdc5f165babc;p=cvc5.git Support for printing a global let map in LFSC proofs. Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules. --- diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am index 2b6d16cfd..75d9f3c5a 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,7 +3,7 @@ # add support for more theories, just list them here in the same order # you would to the LFSC proof-checker binary. # -CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf +CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf noinst_LTLIBRARIES = libsignatures.la diff --git a/proofs/signatures/th_bv_rewrites.plf b/proofs/signatures/th_bv_rewrites.plf new file mode 100644 index 000000000..bf5dea9e9 --- /dev/null +++ b/proofs/signatures/th_bv_rewrites.plf @@ -0,0 +1,22 @@ +; +; Equality swap +; + +(declare rr_bv_eq + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2))))))) + +; +; Additional rules... +; + +; +; Default, if nothing else applied +; + +(declare rr_bv_default + (! t1 formula + (! t2 formula + (th_holds (iff t1 t2)))))) diff --git a/src/options/proof_options b/src/options/proof_options index 7feb00b0d..68ce156e9 100644 --- a/src/options/proof_options +++ b/src/options/proof_options @@ -5,4 +5,7 @@ module PROOF "options/proof_options.h" Proof +option lfscLetification --lfsc-letification bool :default false + turns on global letification in LFSC proofs + endmodule diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index b9907aac9..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& lemma, std::ostream& os, std::ostream& paren) { +void LFSCArithProof::printTheoryLemmaProof(std::vector& 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) { diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 810d41155..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,9 +68,9 @@ 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& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector& 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); diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index aee236677..484bc70c8 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -107,14 +107,17 @@ unsigned ProofArray::getExtMergeTag() const { } 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", 0, &d_proofPrinter); Debug("pf::array") << std::endl; @@ -126,7 +129,7 @@ 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", 0, &d_proofPrinter); @@ -1122,7 +1125,7 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) { return d_skolemToLiteral[skolem]; } -void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +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) { @@ -1216,14 +1219,14 @@ void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { } } -void LFSCArrayProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { +void LFSCArrayProof::printTheoryLemmaProof(std::vector& 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) { @@ -1308,7 +1311,7 @@ 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 << " "; diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 076ba7381..69e62dbf3 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -59,7 +59,7 @@ private: 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; @@ -74,7 +74,8 @@ public: //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); @@ -117,9 +118,9 @@ 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& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector& 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); diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index b2d6fdecf..171085d7f 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -25,6 +25,7 @@ #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; @@ -272,7 +273,7 @@ void BitVectorProof::finalizeConflicts(std::vector& conflicts) { } } -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; @@ -367,7 +368,7 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa } } -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().bitIndex; Expr var = term[0]; @@ -395,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 ? "_ _ " : ""; @@ -413,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 << " "; @@ -421,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 << " "; @@ -431,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 <<" "; @@ -466,7 +467,7 @@ void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { os << "(BitVec "<& lemma, std::ostream& os, std::ostream& paren) { +void LFSCBitVectorProof::printTheoryLemmaProof(std::vector& 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; @@ -658,7 +659,7 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea os << "(trust_f "; os << "(= (BitVec " << utils::getSize(it->first) << ") "; os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") "; - LetMap emptyMap; + ProofLetMap emptyMap; d_proofEngine->printBoundTerm(it->first, os, emptyMap); os << ")) "; os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n"; @@ -942,31 +943,28 @@ 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()); - - IdToSatClause::iterator it2; - Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl; - for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) { - Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl; - } - Debug("pf::bv") << std::endl; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); + Assert(used_lemmas.empty()); +} +const std::set* 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 << std::endl << ";; BB atom mapping\n" << std::endl; - std::set atoms; - d_cnfProof->collectAtomsForClauses(used_inputs, atoms); - std::set::iterator atomIt; Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; - for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) { + for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) { Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; } Debug("pf::bv") << std::endl; @@ -975,7 +973,11 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, printBitblasting(os, paren); // print CNF conversion proof for bit-blasted facts - d_cnfProof->printAtomMapping(atoms, os, paren); + 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) { @@ -1030,4 +1032,13 @@ void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1 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 5ea754e08..a52292ec9 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -113,41 +113,48 @@ public: 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* 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 d_aliasToBindDeclaration; std::string assignAlias(Expr expr); bool hasAlias(Expr expr); + + std::set 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, bool swap); virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); - virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector& 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* 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 abe48e3cd..b58ade35e 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -337,6 +337,28 @@ void LFSCCnfProof::printAtomMapping(const std::set& atoms, } } +void LFSCCnfProof::printAtomMapping(const std::set& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap) { + std::set::const_iterator it = atoms.begin(); + std::set::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 << ")))"; + } +} + // maps each expr to the position it had in the clause and the polarity it had Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause, std::map& childIndex, diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 62036ced0..788526b80 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -141,6 +141,10 @@ public: virtual void printAtomMapping(const std::set& atoms, std::ostream& os, std::ostream& paren) = 0; + virtual void printAtomMapping(const std::set& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap) = 0; virtual void printClause(const prop::SatClause& clause, std::ostream& os, @@ -169,6 +173,11 @@ public: std::ostream& os, std::ostream& paren); + void printAtomMapping(const std::set& 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/proof_manager.cpp b/src/proof/proof_manager.cpp index 5ce8b523f..65a6b1950 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" @@ -335,6 +336,10 @@ 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); @@ -469,6 +474,16 @@ void LFSCProof::toStream(std::ostream& out) { 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); @@ -476,11 +491,11 @@ void LFSCProof::toStream(std::ostream& out) { 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; @@ -493,7 +508,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl; 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()) { @@ -515,7 +530,8 @@ 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(); @@ -527,7 +543,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, //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"; @@ -640,5 +656,75 @@ 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 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); + + unsigned newId = ProofLetCount::newId(); + ProofLetCount letCount(newId); + map[term] = letCount; + letOrder.push_back(LetOrderElement(term, newId)); +} + +void ProofManager::printGlobalLetMap(std::set& atoms, + ProofLetMap& letMap, + std::ostream& out, + std::ostringstream& paren) { + Bindings letOrder; + std::set::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* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof(); + for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) { + Debug("gk::temp") << "Binding additional atom: " << *atom << std::endl; + 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 c6454b652..14793f380 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -22,6 +22,7 @@ #include #include #include "proof/proof.h" +#include "proof/proof_utils.h" #include "proof/skolemization_manager.h" #include "util/proof.h" #include "expr/node.h" @@ -115,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; @@ -140,6 +165,8 @@ class ProofManager { std::map d_rewriteFilters; + std::vector d_rewriteLog; + protected: LogicInfo d_logic; @@ -231,6 +258,16 @@ public: 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 getRewriteLog(); + void dumpRewriteLog() const; + + void printGlobalLetMap(std::set& atoms, + ProofLetMap& letMap, + std::ostream& out, + std::ostringstream& paren); };/* class ProofManager */ class LFSCProof : public Proof { @@ -242,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_utils.h b/src/proof/proof_utils.h index 8c734c892..546d419fc 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -32,6 +32,58 @@ typedef __gnu_cxx::hash_set NodeSet; typedef std::pair NodePair; typedef std::set 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 Bindings; + namespace utils { std::string toLFSCKind(Kind kind); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index fe67ec94d..7fa11cc5f 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -46,7 +46,7 @@ namespace CVC4 { -unsigned CVC4::LetCount::counter = 0; +unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; TheoryProofEngine::TheoryProofEngine() @@ -180,30 +180,30 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla 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); @@ -212,7 +212,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { continue; } - os << "(@ let"<first << " --> " << it->second << std::endl; + Node n1 = it->first; + Node n2 = it->second; + Assert(theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + std::ostringstream rewriteRule; rewriteRule << ".lrr" << d_assertionToRewrite.size(); - LetMap emptyMap; - os << "(th_let_pf _ (trust_f (iff "; - printBoundTerm(it->second.toExpr(), os, emptyMap); - os << " "; - printBoundTerm(it->first.toExpr(), os, emptyMap); - os << ")) (\\ " << rewriteRule.str() << "\n"; + 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; @@ -423,7 +429,7 @@ void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { } // TODO: this function should be moved into the BV prover. -void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) { +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 bv_lemmas; @@ -514,12 +520,13 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std BitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); - bv->printResolutionProof(os, paren); + // bv->printResolutionProof(os, paren, letMap); } void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, - std::ostream& paren) { + std::ostream& paren, + ProofLetMap& map) { os << " ;; Theory Lemmas \n"; Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl; @@ -527,7 +534,8 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, dumpTheoryLemmas(lemmas); } - finalizeBvConflicts(lemmas, os, paren); + // finalizeBvConflicts(lemmas, os, paren, map); + ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -627,7 +635,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, // 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); + getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren, map); // Turn rewrite filter OFF pm->clearRewriteFilters(); @@ -734,7 +742,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); } - getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren); + getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren, map); // Turn rewrite filter OFF pm->clearRewriteFilters(); @@ -774,15 +782,15 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } -void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { +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"<& lemma, std::ostream& os, std::ostream& paren) { +void TheoryProof::printTheoryLemmaProof(std::vector& 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); @@ -975,7 +986,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector& 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; @@ -1007,7 +1018,7 @@ 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()) { if (d_treatBoolsAsFormulas) @@ -1101,7 +1112,7 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector& lemma, void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { // By default, we just print a trust statement. Specific theories can implement // better proofs. - LetMap emptyMap; + ProofLetMap emptyMap; os << "(trust_f (not (= _ "; d_proofEngine->printBoundTerm(c1, os, emptyMap); @@ -1110,4 +1121,14 @@ void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr 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 352cc1b53..f6f00fa11 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -35,57 +35,8 @@ 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 LetMap; -typedef std::vector Bindings; - class TheoryProof; typedef __gnu_cxx::hash_set ExprSet; @@ -118,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. @@ -168,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). @@ -192,40 +143,43 @@ public: 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. - void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); std::map d_assertionToRewrite; }; @@ -247,7 +201,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); } /** @@ -256,7 +210,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. * @@ -279,7 +233,10 @@ public: * * @param os output stream */ - virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map); /** * Print the sorts declarations for this theory. * @@ -321,6 +278,12 @@ public: * @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) {} }; @@ -333,7 +296,7 @@ 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& lemma, std::ostream& os, std::ostream& paren) = 0; @@ -348,7 +311,7 @@ public: LFSCBooleanProof(TheoryProofEngine* 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& lemma, std::ostream& os, std::ostream& paren); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index bc409901c..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,7 +85,7 @@ 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; @@ -693,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); @@ -732,14 +736,14 @@ void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { os << type <<" "; } -void LFSCUFProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { +void LFSCUFProof::printTheoryLemmaProof(std::vector& 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) { diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 0a23267d8..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,9 +64,9 @@ 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& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector& 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); diff --git a/src/util/proof.h b/src/util/proof.h index fc5f7f901..b4a8a3d29 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -21,13 +21,21 @@ #define __CVC4__PROOF_H #include +#include namespace CVC4 { +class Expr; +class ProofLetCount; +struct ExprHashFunction; + +typedef __gnu_cxx::hash_map ProofLetMap; + class CVC4_PUBLIC Proof { public: virtual ~Proof() { } virtual void toStream(std::ostream& out) = 0; + virtual void toStream(std::ostream& out, const ProofLetMap& map) = 0; };/* class Proof */ }/* CVC4 namespace */