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.h | |
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.h')
-rw-r--r-- | src/proof/uf_proof.h | 9 |
1 files changed, 5 insertions, 4 deletions
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<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); |