update from the master

5 files changed, 46 insertions, 41 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b7fb1603d..411b89514 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -18,21 +18,22 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/core/Solver.h"
+
 #include <math.h>
 
 #include <iostream>
 
 #include "base/output.h"
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
-#include "prop/minisat/core/Solver.h"
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
 
-
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -229,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);
@@ -602,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)
 {
@@ -661,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)); )
         }
@@ -694,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++){
@@ -786,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
@@ -865,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;
@@ -921,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;
@@ -963,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.
 |________________________________________________________________________________________________@*/
@@ -1037,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()
 {
@@ -1114,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.
@@ -1146,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'
@@ -1219,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);
             }
 
@@ -1417,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)
@@ -1466,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]];
@@ -1537,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);
 }
@@ -1698,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)
   {
@@ -1739,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);
@@ -1784,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/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 777fb1093..99c47e045 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/output.h"
 #include "context/context.h"
+#include "proof/clause_id.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
 #include "prop/minisat/mtl/Heap.h"
@@ -43,7 +44,6 @@ namespace prop {
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-typedef unsigned ClauseId;
 
 namespace CVC4 {
 namespace Minisat {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 739d9087a..bfbf9da6f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5bdaea950..9b551fa70 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,10 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/simp/SimpSolver.h"
+
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
-#include "prop/minisat/simp/SimpSolver.h"
 #include "prop/minisat/utils/System.h"
 
 using namespace CVC4;
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a19bec1ef..a995c1357 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
+#include "proof/clause_id.h"
 #include "prop/minisat/mtl/Queue.h"
 #include "prop/minisat/core/Solver.h"