squash-merge from proof branch

1 files changed, 20 insertions, 10 deletions

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index e5a80b428..b4df850f7 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,7 +21,7 @@
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
-#include <ext/hash_map> 
+#include <ext/hash_map>
 #include <ext/hash_set>
 #include <iosfwd>
 
@@ -43,6 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
 
 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
+typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory;
 
 class CnfProof {
 protected:
@@ -54,28 +55,33 @@ protected:
   /** Map from assertion to reason for adding assertion  **/
   NodeToProofRule d_assertionToProofRule;
 
+  /** Map from assertion to the theory that added this assertion  **/
+  ClauseIdToTheory d_clauseIdToOwnerTheory;
+
+  /** The last theory to explain a lemma **/
+  theory::TheoryId d_explainerTheory;
+
   /** Top of stack is assertion currently being converted to CNF **/
   std::vector<Node> d_currentAssertionStack;
 
   /** Top of stack is top-level fact currently being converted to CNF **/
   std::vector<Node> d_currentDefinitionStack;
 
-  
   /** Map from ClauseId to the top-level fact that lead to adding this clause **/
   ClauseIdToNode d_clauseToDefinition;
 
   /** Top-level facts that follow from assertions during convertAndAssert **/
   NodeSet d_definitions;
-  
+
   /** Map from top-level fact to facts/assertion that it follows from **/
   NodeToNode d_cnfDeps;
 
   ClauseIdSet d_explanations;
-  
+
   bool isDefinition(Node node);
 
   Node getDefinitionForClause(ClauseId clause);
-  
+
   std::string d_name;
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream,
@@ -103,10 +109,10 @@ public:
 
   /** Clause is one of the clauses defining top-level assertion node*/
   void setClauseAssertion(ClauseId clause, Node node);
-  
+
   void registerAssertion(Node assertion, ProofRule reason);
   void setCnfDependence(Node from, Node to);
-  
+
   void pushCurrentAssertion(Node assertion); // the current assertion being converted
   void popCurrentAssertion();
   Node getCurrentAssertion();
@@ -115,14 +121,18 @@ public:
   void popCurrentDefinition();
   Node getCurrentDefinition();
 
-  
+  void setExplainerTheory(theory::TheoryId theory);
+  theory::TheoryId getExplainerTheory();
+  theory::TheoryId getOwnerTheory(ClauseId clause);
+
+  void registerExplanationLemma(ClauseId clauseId);
+
   // accessors for the leaf assertions that are being converted to CNF
   bool isAssertion(Node node);
   ProofRule getProofRule(Node assertion);
   ProofRule getProofRule(ClauseId clause);
   Node getAssertionForClause(ClauseId clause);
 
-  
   /** Virtual methods for printing things **/
   virtual void printAtomMapping(const NodeSet& atoms,
                                 std::ostream& os,
@@ -154,7 +164,7 @@ public:
   void printAtomMapping(const NodeSet& atoms,
                         std::ostream& os,
                         std::ostream& paren);
-  
+
   void printClause(const prop::SatClause& clause,
                    std::ostream& os,
                    std::ostream& paren);