diff options
author | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
commit | 4b8f92d23f7a75b4148f41e039f7bdc5f165babc (patch) | |
tree | e2d8abdff6f2d6befa652a09188fff991caf1cf4 /src/proof/uf_proof.cpp | |
parent | 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 (diff) |
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.
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
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<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) { |