cleaned up proof code

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 */