diff options
Diffstat (limited to 'src/proof/uf_proof.h')
| -rw-r--r-- | src/proof/uf_proof.h | 10 |
1 files changed, 6 insertions, 4 deletions
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); }; |