diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
commit | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (patch) | |
tree | 6a3608afa6276e11e1a72504c439a4991e9dea41 /src/proof/theory_proof.h | |
parent | 08c8433e4ab849024930a8c4dbe8756e13d08099 (diff) |
cleaned up proof code
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index b09641fec..773428633 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -28,13 +28,11 @@ namespace CVC4 { - typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; + typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; - + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; class TheoryProof { protected: - ExprSet d_atomSet; - ExprSet d_inputFormulas; ExprSet d_termDeclarations; SortSet d_sortDeclarations; ExprSet d_declarationCache; @@ -42,18 +40,14 @@ namespace CVC4 { void addDeclaration(Expr atom); public: TheoryProof(); - void addAtom(Expr atom); - void assertFormula(Expr formula); - virtual void printFormula(Expr atom, std::ostream& os) = 0; - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; }; class LFSCTheoryProof: public TheoryProof { - void printTerm(Expr term, std::ostream& os); + static void printTerm(Expr term, std::ostream& os); + void printDeclarations(std::ostream& os, std::ostream& paren); public: - virtual void printFormula(Expr atom, std::ostream& os); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + static void printFormula(Expr atom, std::ostream& os); virtual void printAssertions(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ |