diff options
Diffstat (limited to 'src/proof/array_proof.h')
| -rw-r--r-- | src/proof/array_proof.h | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 306eb10eb..fb25c9433 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -30,29 +30,29 @@ namespace CVC4 { //proof object outputted by TheoryARRAY class ProofArray : public Proof { private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - theory::eq::EqProof* pf, - unsigned tb, - const LetMap& map); + Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + theory::eq::EqProof* pf, + unsigned tb, + const LetMap& map); /** Merge tag for ROW applications */ - static unsigned s_reasonRow; + unsigned d_reasonRow; /** Merge tag for ROW1 applications */ - static unsigned s_reasonRow1; + unsigned d_reasonRow1; /** Merge tag for EXT applications */ - static unsigned s_reasonExt; + unsigned d_reasonExt; public: ProofArray(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 toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); void registerSkolem(Node equality, Node skolem); - static void setRowMergeTag(unsigned tag); - static void setRow1MergeTag(unsigned tag); - static void setExtMergeTag(unsigned tag); + void setRowMergeTag(unsigned tag); + void setRow1MergeTag(unsigned tag); + void setExtMergeTag(unsigned tag); }; namespace theory { |