diff options
Diffstat (limited to 'src/proof/array_proof.h')
| -rw-r--r-- | src/proof/array_proof.h | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index df8cb58a2..99ad956a5 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -38,15 +38,20 @@ class ProofArray : public Proof { void registerSkolem(Node equality, Node skolem); - void toStream(std::ostream& out); - void toStream(std::ostream& out, const ProofLetMap& map); - private: - void toStreamLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, const ProofLetMap& map); + void toStream(std::ostream& out) const override; + void toStream(std::ostream& out, const ProofLetMap& map) const override; - Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - const theory::eq::EqProof& pf, unsigned tb, - const ProofLetMap& map); + private: + void toStreamLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map) const; + + Node toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, + const ProofLetMap& map) const; // It is simply an equality engine proof. std::shared_ptr<theory::eq::EqProof> d_proof; |