From 9a4fb4ff7641b9585605567e11a6f7e683aa63bf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Nov 2017 14:08:55 -0800
Subject: [PATCH] remove ad-hoc parameters, deprecating dimacs cube mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_config.cpp                   |  1 -
 src/sat/sat_config.h                     |  1 -
 src/sat/sat_params.pyg                   |  1 -
 src/sat/sat_solver.cpp                   |  4 +++
 src/tactic/portfolio/parallel_tactic.cpp | 31 +++++++++++++++---------
 5 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index d0618d265..31304bab5 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -89,7 +89,6 @@ namespace sat {
         m_local_search    = p.local_search();
         m_local_search_threads = p.local_search_threads();
         m_lookahead_simplify = p.lookahead_simplify();
-        m_lookahead_cube = p.lookahead_cube();
         m_lookahead_search = p.lookahead_search();
         if (p.lookahead_reward() == symbol("heule_schur")) {
             m_lookahead_reward = heule_schur_reward;
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 17ce7a569..2e1d8a145 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -84,7 +84,6 @@ namespace sat {
         bool               m_local_search;
         bool               m_lookahead_search;
         bool               m_lookahead_simplify;
-        bool               m_lookahead_cube;
         unsigned           m_lookahead_cube_cutoff;
         double             m_lookahead_cube_fraction;
         reward_t           m_lookahead_reward;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 5880f8bfc..229bd8a4b 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -36,7 +36,6 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
-                          ('lookahead_cube', BOOL, False, 'use lookahead solver to create cubes'),
                           ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
                           ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d6ec47f36..f5b04e646 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -871,9 +871,13 @@ namespace sat {
         if (m_config.m_lookahead_search && num_lits == 0) {
             return lookahead_search();
         }
+#if 0
+        // deprecated
         if (m_config.m_lookahead_cube && num_lits == 0) {
             return lookahead_cube();
         }
+#endif
+
         if (m_config.m_local_search) {
             return do_local_search(num_lits, lits);
         }
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index e3d2ee8b3..82fc0fb39 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/src/tactic/portfolio/parallel_tactic.cpp
@@ -111,7 +111,6 @@ class parallel_tactic : public tactic {
                 solver_state* st = try_get_task();
                 if (st) return st;
                 inc_wait();
-
                 std::unique_lock<std::mutex> lock(m_mutex);
                 m_cond.wait(lock, [this] { --m_num_waiters; return true; });                
             }
@@ -289,14 +288,11 @@ class parallel_tactic : public tactic {
         }
 
         void set_simplify_params(bool pb_simp, bool retain_blocked) {
-            m_params.set_bool("bca", true);
             m_params.set_bool("cardinality.solver", pb_simp);
-            m_params.set_bool("cce", true);
-//          m_params.set_bool("elim_blocked_clauses", true);
+            m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
             if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) 
                 m_params.set_uint("inprocess.max", 2);
             m_params.set_bool("lookahead_simplify", true);
-            m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
             m_params.set_uint("restart.max", UINT_MAX);
             m_params.set_bool("retain_blocked_clauses", retain_blocked);
             get_solver().updt_params(m_params);
@@ -344,7 +340,7 @@ private:
         IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
                    if (status == l_true)  verbose_stream() << ":status sat ";
                    if (status == l_undef) verbose_stream() << ":status unknown ";
-                   verbose_stream() <<o ":unsat " << m_num_unsat << ")\n";);
+                   verbose_stream() << ":unsat " << m_num_unsat << ")\n";);
     }
 
     void report_sat(solver_state& s) {
@@ -387,13 +383,13 @@ private:
     cube:
         SASSERT(s.type() == cube_task);
 
-        s.inc_depth(1);
         // extract up to one cube and add it.
         cube.reset();
         cube.append(s.split_cubes(1));
         SASSERT(cube.size() <= 1);
         if (!s.cubes().empty()) m_queue.add_task(s.clone());
         if (!cube.empty()) s.assert_cube(cube.get(0));
+        s.inc_depth(1);
 
         // simplify
         switch (s.simplify()) {
@@ -401,7 +397,7 @@ private:
         case l_true:  report_sat(s); return;
         case l_false: report_unsat(s); return;                
         }
-        if (s.canceled()) return;
+        if (canceled(s)) return;
         
         // extract cubes.
         cubes.reset();
@@ -419,7 +415,8 @@ private:
             cubes.push_back(c);            
         }
 
-        IF_VERBOSE(1, verbose_stream() << "cubes: " << cubes << "\n";);
+        IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";);
+        IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";);
 
         if (cubes.empty()) {
             report_unsat(s);
@@ -448,7 +445,7 @@ private:
             case l_true:  report_sat(s); break;
             case l_false: report_unsat(s); break;                
             }
-            if (s.canceled()) return;
+            if (canceled(s)) return;
         }
         IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";);
         if (hard_cubes.empty()) return;
@@ -458,6 +455,16 @@ private:
         goto cube;        
     }
 
+    bool canceled(solver_state& s) {
+        if (s.canceled()) {
+            m_has_undef = true;
+            return true;
+        }
+        else {
+            return false;
+        }        
+    }
+
     void run_solver() {
         try {
             while (solver_state* st = m_queue.get_task()) {
@@ -490,10 +497,12 @@ private:
         }
         if (!m_models.empty()) {
             mdl = m_models.back();            
+            m_manager.limit().reset_cancel();
             return l_true;
         }
-        if (m_has_undef || m_manager.canceled()) 
+        if (m_has_undef) 
             return l_undef;
+        m_manager.limit().reset_cancel();
         return l_false;
     }