diff options
author | Guy <katz911@gmail.com> | 2016-04-09 13:05:14 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-04-09 13:05:14 -0700 |
commit | 846a2bbb482412a076120717977833dfd096d41e (patch) | |
tree | c9b530309960b038ecb14909949710f6bedc258a /src/proof/array_proof.h | |
parent | 208a9989b53c61f7f1f0053e97600dd7e12f8aa5 (diff) |
Made ProofArray's printing functions non-static, and consequently the data members non-static as well
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 af980bc43..5792bd272 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 { |