From a13c64a5b4164b5a10943c0d5283260252be30d0 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 6 Feb 2007 08:01:00 -0800
Subject: Version abc70206

---
 src/sat/bsat/satSolver.c | 8 +++++++-
 src/sat/bsat/satSolver.h | 2 ++
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'src/sat/bsat')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index c4847be4..5c9294b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -457,6 +457,12 @@ static inline void sat_solver_canceluntil(sat_solver* s, int level) {
     reasons = s->reasons;
     bound   = (veci_begin(&s->trail_lim))[level];
 
+    ////////////////////////////////////////
+    // added to cancel all assignments
+//    if ( level == -1 )
+//        bound = 0;
+    ////////////////////////////////////////
+
     for (c = s->qtail-1; c >= bound; c--) {
         int     x  = lit_var(trail[c]);
         values [x] = l_Undef;
@@ -881,7 +887,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
                 return l_Undef; 
             }
 
-            if (sat_solver_dlevel(s) == 0)
+            if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
                 // Simplify the set of problem clauses:
                 sat_solver_simplify(s);
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8f71370f..986e48d5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -170,6 +170,8 @@ struct sat_solver_t
  
     Sat_MmStep_t * pMem;
 
+    int      fSkipSimplify; // set to one to skip simplification of the clause database
+
     // clause store
     void *   pStore;
 
-- 
cgit v1.2.3