Merge from proof branch

1 files changed, 53 insertions, 2 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 54c86f3f3..c8c776ec9 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -27,6 +27,7 @@
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/proof.h"
+#include "proof/proof_utils.h"
 
 namespace CVC4 {
 
@@ -90,10 +91,14 @@ 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
@@ -148,6 +153,14 @@ 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).
    *
@@ -171,8 +184,14 @@ public:
    */
   void registerTheory(theory::Theory* theory);
 
-  theory::TheoryId getTheoryForLemma(ClauseId id);
+  theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
   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 {
@@ -190,11 +209,25 @@ 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 {
@@ -270,11 +303,20 @@ 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 {
@@ -292,12 +334,13 @@ 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)
+    : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
@@ -305,6 +348,14 @@ 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 */