added currying for uf proofs; still needs debugging

1 files changed, 11 insertions, 6 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index ac8f9f7b8..b09641fec 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -28,28 +28,33 @@
 
 namespace CVC4 {
 
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > AtomSet;
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > TermSet; 
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
   typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
   
   class TheoryProof {
   protected:
-    AtomSet d_atomSet;
-    TermSet d_termDeclarations;
+    ExprSet d_atomSet;
+    ExprSet d_inputFormulas;
+    ExprSet d_termDeclarations;
     SortSet d_sortDeclarations; 
+    ExprSet d_declarationCache;
+    
     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 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); 
   public:
     virtual void printFormula(Expr atom, std::ostream& os);
-    virtual void printDeclarations(std::ostream& os, std::ostream& paren); 
+    virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+    virtual void printAssertions(std::ostream& os, std::ostream& paren);
   }; 
 } /* CVC4 namespace */
 #endif /* __CVC4__THEORY_PROOF_H */