Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 55 insertions, 43 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index a101a0c2d..0ec8981ca 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/simp/SimpSolver.h"
 
 #include "options/prop_options.h"
+#include "options/smt_options.h"
 #include "proof/clause_id.h"
-#include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/minisat/utils/System.h"
 
@@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-
-SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) :
-    Solver(proxy, context, enableIncremental)
-  , grow               (opt_grow)
-  , clause_lim         (opt_clause_lim)
-  , subsumption_lim    (opt_subsumption_lim)
-  , simp_garbage_frac  (opt_simp_garbage_frac)
-  , use_asymm          (opt_use_asymm)
-  , use_rcheck         (opt_use_rcheck)
-  , use_elim           (options::minisatUseElim() && !enableIncremental)
-  , merges             (0)
-  , asymm_lits         (0)
-  , eliminated_vars    (0)
-  , elimorder          (1)
-  , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially
-  , occurs             (ClauseDeleted(ca))
-  , elim_heap          (ElimLt(n_occ))
-  , bwdsub_assigns     (0)
-  , n_touched          (0)
+SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
+                       CVC4::context::Context* context,
+                       bool enableIncremental)
+    : Solver(proxy, context, enableIncremental),
+      grow(opt_grow),
+      clause_lim(opt_clause_lim),
+      subsumption_lim(opt_subsumption_lim),
+      simp_garbage_frac(opt_simp_garbage_frac),
+      use_asymm(opt_use_asymm),
+      use_rcheck(opt_use_rcheck),
+      use_elim(options::minisatUseElim() && !enableIncremental),
+      merges(0),
+      asymm_lits(0),
+      eliminated_vars(0),
+      elimorder(1),
+      use_simplification(
+          !enableIncremental
+          && !options::unsatCores())  // TODO: turn off simplifications if
+                                      // proofs are on initially
+      ,
+      occurs(ClauseDeleted(ca)),
+      elim_heap(ElimLt(n_occ)),
+      bwdsub_assigns(0),
+      n_touched(0)
 {
     if(options::minisatUseElim() &&
        options::minisatUseElim.wasSetByUser() &&
@@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
     if (options::minisatDumpDimacs()) {
-      toDimacs(); 
-      return l_Undef; 
+      toDimacs();
+      return l_Undef;
     }
     assert(decisionLevel() == 0);
 
@@ -525,7 +530,7 @@ bool SimpSolver::eliminateVar(Var v)
     for (int i = 0; i < cls.size(); i++)
         (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
 
-    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+    // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
     // clause must exceed the limit on the maximal clause size (if it is set):
     //
     int cnt         = 0;
@@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v)
 
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++)
-            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
-                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
-                return true;
+          if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+              && (++cnt > cls.size() + grow
+                  || (clause_lim != -1 && clause_size > clause_lim)))
+            return true;
 
     // Delete and store old clauses:
     eliminated[v] = true;
@@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v)
         mkElimClause(elimclauses, ~mkLit(v));
     }
 
-    for (int i = 0; i < cls.size(); i++)
-        removeClause(cls[i]); 
+    for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
 
-    ClauseId id = ClauseIdUndef; 
+    ClauseId id = ClauseIdUndef;
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
     for (int i = 0; i < pos.size(); i++)
@@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v)
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
-    
+
     // Free watchers lists for this variable, if possible:
     if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
     if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x)
     eliminated[v] = true;
     setDecisionVar(v, false);
     const vec<CRef>& cls = occurs.lookup(v);
-    
+
     vec<Lit>& subst_clause = add_tmp;
     for (int i = 0; i < cls.size(); i++){
         Clause& c = ca[cls[i]];
@@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 
         gatherTouchedClauses();
         // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
-        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
-            !backwardSubsumptionCheck(true)){
-            ok = false; goto cleanup; }
+        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+            && !backwardSubsumptionCheck(true))
+        {
+          ok = false;
+          goto cleanup;
+        }
 
         // Empty elim_heap and return immediately on user-interrupt:
         if (asynch_interrupt){
@@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
         for (int cnt = 0; !elim_heap.empty(); cnt++){
             Var elim = elim_heap.removeMin();
-            
+
             if (asynch_interrupt) break;
 
             if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
     }
 
     if (verbosity >= 1 && elimclauses.size() > 0)
-        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
-               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+      printf(
+          "|  Eliminated clauses:     %10.2f Mb                                "
+          "      |\n",
+          double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
 
     return ok;
 }
@@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to)
     //
     for (int i = 0; i < subsumption_queue.size(); i++)
         ca.reloc(subsumption_queue[i], to);
-        // TODO reloc now takes the proof form the core solver 
+    // TODO reloc now takes the proof form the core solver
     // Temporary clause:
     //
     ca.reloc(bwdsub_tmpunit, to);
-    // TODO reloc now takes the proof form the core solver 
+    // TODO reloc now takes the proof form the core solver
 }
 
 
@@ -756,15 +766,17 @@ void SimpSolver::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());
 
     cleanUpClauses();
     to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
     relocAll(to);
     Solver::relocAll(to);
     if (verbosity >= 2)
-        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
-               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+      printf(
+          "|  Garbage collection:   %12d bytes => %12d bytes             |\n",
+          ca.size() * ClauseAllocator::Unit_Size,
+          to.size() * ClauseAllocator::Unit_Size);
     to.moveTo(ca);
-    // TODO: proof.finalizeUpdateId(); 
+    // TODO: proof.finalizeUpdateId();
 }