squash-merge from proof branch

6 files changed, 75 insertions, 52 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9bc352f9b..7409c7222 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -674,7 +674,8 @@ void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool removable,
                                         bool negated,
                                         ProofRule proof_id,
-                                        TNode from) {
+                                        TNode from,
+                                        theory::TheoryId ownerTheory) {
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -684,6 +685,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
       Node assertion = negated ? node.notNode() : (Node)node;
       Node from_assertion = negated? from.notNode() : (Node) from;
 
+      d_cnfProof->setExplainerTheory(ownerTheory);
       if (proof_id != RULE_INVALID) {
         d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
         d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
@@ -695,7 +697,10 @@ void TseitinCnfStream::convertAndAssert(TNode node,
     });
 
   convertAndAssert(node, negated);
-  PROOF(if (d_cnfProof) d_cnfProof->popCurrentAssertion(); );
+  PROOF
+    (if (d_cnfProof) {
+      d_cnfProof->popCurrentAssertion();
+    });
 }
 
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a6b6781ca..32e2205a1 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -207,9 +207,14 @@ public:
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
+   * @param ownerTheory indicates the theory that should invoked to prove the formula.
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
-
+  virtual void convertAndAssert(TNode node,
+                                bool removable,
+                                bool negated,
+                                ProofRule proof_id,
+                                TNode from = TNode::null(),
+                                theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
   /**
    * Get the node that is represented by the given SatLiteral.
    * @param literal the literal from the sat solver
@@ -278,7 +283,8 @@ public:
    * @param negated true if negated
    */
   void convertAndAssert(TNode node, bool removable,
-                        bool negated, ProofRule rule, TNode from = TNode::null());
+                        bool negated, ProofRule rule, TNode from = TNode::null(),
+                        theory::TheoryId ownerTheory = theory::THEORY_LAST);
 
   /**
    * Constructs the stream to use the given sat solver.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b13448bb2..411b89514 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -230,7 +230,7 @@ CRef Solver::reason(Var x) {
     proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
                               explanation_cl);
     vec<Lit> explanation;
-    MinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
+    MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
     // Sort the literals by trail index level
     lemma_lt lt(*this);
@@ -603,20 +603,20 @@ Lit Solver::pickBranchLit()
 /*_________________________________________________________________________________________________
 |
 |  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
-|  
+|
 |  Description:
 |    Analyze conflict and produce a reason clause.
-|  
+|
 |    Pre-conditions:
 |      * 'out_learnt' is assumed to be cleared.
 |      * Current decision level must be greater than root level.
-|  
+|
 |    Post-conditions:
 |      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
-|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the 
+|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
 |        rest of literals. There may be others from the same level though.
 |      * returns the maximal level of the resolved clauses
-|  
+|
 |________________________________________________________________________________________________@*/
 int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 {
@@ -662,14 +662,14 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
               }
             }
         }
-        
+
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
         p     = trail[index+1];
         confl = reason(var(p));
         seen[var(p)] = 0;
         pathC--;
-        
+
         if ( pathC > 0 && confl != CRef_Undef ) {
           PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
         }
@@ -695,13 +695,13 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 out_learnt[j++] = out_learnt[i];
               } else {
                 PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
-                // Literal is redundant, to be safe, mark the level as current assertion level 
+                // Literal is redundant, to be safe, mark the level as current assertion level
                 // TODO: maybe optimize
                 max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
               }
             }
         }
-        
+
     }else if (ccmin_mode == 1){
         Unreachable();
         for (i = j = 1; i < out_learnt.size(); i++){
@@ -787,7 +787,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
 /*_________________________________________________________________________________________________
 |
 |  analyzeFinal : (p : Lit)  ->  [void]
-|  
+|
 |  Description:
 |    Specialized analysis procedure to express the final conflict in terms of assumptions.
 |    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
@@ -866,7 +866,7 @@ CRef Solver::propagate(TheoryCheckType type)
       if (lemmas.size() > 0) {
         recheck = true;
         confl = updateLemmas();
-        return confl; 
+        return confl;
       } else {
         recheck = proxy->theoryNeedCheck();
         return confl;
@@ -922,7 +922,7 @@ void Solver::propagateTheory() {
   proxy->theoryPropagate(propagatedLiteralsClause);
 
   vec<Lit> propagatedLiterals;
-  MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); 
+  MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
 
   int oldTrailSize = trail.size();
   Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
@@ -964,11 +964,11 @@ void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
 /*_________________________________________________________________________________________________
 |
 |  propagateBool : [void]  ->  [Clause*]
-|  
+|
 |  Description:
 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
 |    otherwise CRef_Undef.
-|  
+|
 |    Post-conditions:
 |      * the propagation queue is empty, even if there was a conflict.
 |________________________________________________________________________________________________@*/
@@ -1038,16 +1038,16 @@ CRef Solver::propagateBool()
 /*_________________________________________________________________________________________________
 |
 |  reduceDB : ()  ->  [void]
-|  
+|
 |  Description:
 |    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
 |    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
 |________________________________________________________________________________________________@*/
-struct reduceDB_lt { 
+struct reduceDB_lt {
     ClauseAllocator& ca;
     reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
-    bool operator () (CRef x, CRef y) { 
-        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
+    bool operator () (CRef x, CRef y) {
+        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
 };
 void Solver::reduceDB()
 {
@@ -1115,7 +1115,7 @@ void Solver::rebuildOrderHeap()
 /*_________________________________________________________________________________________________
 |
 |  simplify : [void]  ->  [bool]
-|  
+|
 |  Description:
 |    Simplify the clause database according to the current top-level assigment. Currently, the only
 |    thing done here is the removal of satisfied clauses, but more things can be put here.
@@ -1147,11 +1147,11 @@ bool Solver::simplify()
 /*_________________________________________________________________________________________________
 |
 |  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
-|  
+|
 |  Description:
-|    Search for a model the specified number of conflicts. 
+|    Search for a model the specified number of conflicts.
 |    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
-|  
+|
 |  Output:
 |    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
 |    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
@@ -1220,9 +1220,9 @@ lbool Solver::search(int nof_conflicts)
                 max_learnts             *= learntsize_inc;
 
                 if (verbosity >= 1)
-                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
-                           (int)conflicts, 
-                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
+                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+                           (int)conflicts,
+                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
             }
 
@@ -1418,7 +1418,7 @@ lbool Solver::solve_()
 
 //=================================================================================================
 // Writing CNF to DIMACS:
-// 
+//
 // FIXME: this needs to be rewritten completely.
 
 static Var mapVar(Var x, vec<Var>& map, Var& max)
@@ -1467,7 +1467,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
     for (int i = 0; i < clauses_persistent.size(); i++)
         if (!satisfied(ca[clauses_persistent[i]]))
             cnt++;
-        
+
     for (int i = 0; i < clauses_persistent.size(); i++)
         if (!satisfied(ca[clauses_persistent[i]])){
             Clause& c = ca[clauses_persistent[i]];
@@ -1538,11 +1538,11 @@ void Solver::garbageCollect()
 {
     // Initialize the next region to a size corresponding to the estimated utilization degree. This
     // is not precise but should avoid some unnecessary reallocations for the new region:
-    ClauseAllocator to(ca.size() - ca.wasted()); 
+    ClauseAllocator to(ca.size() - ca.wasted());
 
     relocAll(to);
     if (verbosity >= 2)
-        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n",
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
@@ -1699,7 +1699,7 @@ CRef Solver::updateLemmas() {
   int backtrack_index = trail.size();
 
   PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
-  
+
   // Attach all the clauses and enqueue all the propagations
   for (int i = 0; i < lemmas.size(); ++ i)
   {
@@ -1740,7 +1740,7 @@ CRef Solver::updateLemmas() {
         (
          Node cnf_assertion = lemmas_cnf_assertion[i].first;
          Node cnf_def = lemmas_cnf_assertion[i].second;
-         
+
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1785,20 +1785,20 @@ CRef Solver::updateLemmas() {
 
 void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy)
 {
- 
+
   // FIXME what is this CRef_lazy
   if (cr == CRef_Lazy) return;
-  
+
   CRef old = cr;  // save the old reference
   Clause& c = operator[](cr);
   if (c.reloced()) { cr = c.relocation(); return; }
-  
+
   cr = to.alloc(c.level(), c, c.removable());
   c.relocate(cr);
   if (proxy) {
-    proxy->updateCRef(old, cr); 
+    proxy->updateCRef(old, cr);
   }
-  // Copy extra data-fields: 
+  // Copy extra data-fields:
   // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
   to[cr].mark(c.mark());
   if (to[cr].removable())         to[cr].activity() = c.activity();
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 583e9da18..ab9ee6588 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -132,12 +132,13 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertLemma(TNode node, bool negated,
                              bool removable,
                              ProofRule rule,
+                             theory::TheoryId ownerTheory,
                              TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a71d4832d..c1c433b05 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -134,7 +134,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 63a09169f..268a90cf6 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -98,19 +98,30 @@ void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
 void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
-  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
-  PROOF(ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); );
-  Debug("prop-explain") << "explainPropagation() => " <<  theoryExplanation << std::endl;
-  if (theoryExplanation.getKind() == kind::AND) {
-    Node::const_iterator it = theoryExplanation.begin();
-    Node::const_iterator it_end = theoryExplanation.end();
+
+  NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
+  Node explanationNode = theoryExplanation.node;
+  theory::TheoryId explainerTheory = theoryExplanation.theory;
+
+  PROOF({
+      ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
+      ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+
+      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
+                        << explainerTheory << std::endl;
+    });
+
+  Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
+  if (explanationNode.getKind() == kind::AND) {
+    Node::const_iterator it = explanationNode.begin();
+    Node::const_iterator it_end = explanationNode.end();
     explanation.push_back(l);
     for (; it != it_end; ++ it) {
       explanation.push_back(~d_cnfStream->getLiteral(*it));
     }
   } else {
     explanation.push_back(l);
-    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
+    explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
   }
 }
 
@@ -164,7 +175,7 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }