1 files changed, 2 insertions, 53 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index c8c776ec9..54c86f3f3 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -27,7 +27,6 @@
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/proof.h"
-#include "proof/proof_utils.h"
 
 namespace CVC4 {
 
@@ -91,14 +90,10 @@ class TheoryProof;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
 
-typedef std::set<theory::TheoryId> TheoryIdSet;
-typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds;
-
 class TheoryProofEngine {
 protected:
   ExprSet d_registrationCache;
   TheoryProofTable d_theoryProofTable;
-  ExprToTheoryIds d_exprToTheoryIds;
 
   /**
    * Returns whether the theory is currently supported in proof
@@ -153,14 +148,6 @@ public:
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
 
   /**
-   * Print aliasing declarations.
-   *
-   * @param os
-   * @param paren closing parenthesis
-   */
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
-
-  /**
    * Print proofs of all the theory lemmas (must prove
    * actual clause used in resolution proof).
    *
@@ -184,14 +171,8 @@ public:
    */
   void registerTheory(theory::Theory* theory);
 
-  theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
+  theory::TheoryId getTheoryForLemma(ClauseId id);
   TheoryProof* getTheoryProof(theory::TheoryId id);
-
-  void markTermForFutureRegistration(Expr term, theory::TheoryId id);
-
-  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
-
-  virtual void treatBoolsAsFormulas(bool value) {};
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -209,25 +190,11 @@ public:
   virtual void printLetTerm(Expr term, std::ostream& os);
   virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printAssertions(std::ostream& os, std::ostream& paren);
-  virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
                                  std::ostream& paren);
   virtual void printSort(Type type, std::ostream& os);
-
-  void performExtraRegistrations();
-
-  void treatBoolsAsFormulas(bool value);
-
-private:
-  static void dumpTheoryLemmas(const IdToSatClause& lemmas);
-
-  // TODO: this function should be moved into the BV prover.
-  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
-
-  std::map<Node, std::string> d_assertionToRewrite;
 };
 
 class TheoryProof {
@@ -303,20 +270,11 @@ public:
    */
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
   /**
-   * Print any aliasing declarations.
-   *
-   * @param os
-   * @param paren
-   */
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
-  /**
    * Register a term of this theory that appears in the proof.
    *
    * @param term
    */
   virtual void registerTerm(Expr term) = 0;
-
-  virtual void treatBoolsAsFormulas(bool value) {}
 };
 
 class BooleanProof : public TheoryProof {
@@ -334,13 +292,12 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
 };
 
 class LFSCBooleanProof : public BooleanProof {
 public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
-    : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
+    : BooleanProof(proofEngine)
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
@@ -348,14 +305,6 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
-
-  void treatBoolsAsFormulas(bool value) {
-    d_treatBoolsAsFormulas = value;
-  }
-
-private:
-  bool d_treatBoolsAsFormulas;
 };
 
 } /* CVC4 namespace */