updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/ba_solver.cpp

@@ -1288,7 +1288,6 @@ namespace sat {
         if (!create_asserting_lemma()) {
             goto bail_out;
         }
-        active2card();
 
         DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A)););
         
@@ -1347,6 +1346,7 @@ namespace sat {
     }
 
     bool ba_solver::create_asserting_lemma() {
+        bool adjusted = false;
 
     adjust_conflict_level:
         int64 bound64 = m_bound;
@@ -1354,7 +1354,6 @@ namespace sat {
         for (bool_var v : m_active_vars) {
             slack += get_abs_coeff(v);
         }
-
         m_lemma.reset();        
         m_lemma.push_back(null_literal);
         unsigned num_skipped = 0;
@@ -1389,26 +1388,32 @@ namespace sat {
                 }
             }
         }
-
         if (slack >= 0) {
             IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
             return false;
         }
-        
+        if (m_overflow) {
+            return false;
+        }        
         if (m_lemma[0] == null_literal) {
             if (m_lemma.size() == 1) {
                 s().set_conflict(justification());
                 return false;
             }
+            return false;
             unsigned old_level = m_conflict_lvl;
             m_conflict_lvl = 0;
             for (unsigned i = 1; i < m_lemma.size(); ++i) {
                 m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i]));
             }
-            IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
+            adjusted = true;
             goto adjust_conflict_level;
         }
-        return !m_overflow;
+        if (!adjusted) {
+            active2card();
+        }
+        return true;
     }
 
     /*

src/sat/tactic/goal2sat.cpp

@@ -1153,6 +1153,8 @@ struct sat2goal::imp {
                 }
             }
         }
+        //s.display(std::cout);
+        //r.display(std::cout);
     }
 
     void add_clause(sat::literal_vector const& lits, expr_ref_vector& lemmas) {

src/tactic/portfolio/parallel_tactic.cpp

@@ -63,12 +63,16 @@ class parallel_tactic : public tactic {
 
         unsigned num_units() const { return m_units; }
 
+        unsigned cube_size() const { return m_cube.size(); }
+
         solver& get_solver() { return *m_solver; }
 
         solver const& get_solver() const { return *m_solver; }
 
         params_ref const& params() const { return m_params; }
 
+        params_ref& params() { return m_params; }
+
         solver_state* clone(params_ref const& p, expr* cube) {
             ast_manager& m = m_solver->get_manager();
             ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode());
@@ -114,7 +118,7 @@ private:
         m_conflicts_decay_rate = 75;
         m_max_conflicts = m_conflicts_lower_bound;
         m_progress = 0;
-        m_num_threads = omp_get_num_procs();  // TBD adjust by possible threads used inside each solver.
+        m_num_threads = 2 * omp_get_num_procs();  // TBD adjust by possible threads used inside each solver.
     }
 
     unsigned get_max_conflicts() { 
@@ -175,16 +179,14 @@ private:
         }
     }
 
-    lbool simplify(solver& s) {
+    lbool simplify(solver_state& s) {
-        params_ref p;
+        s.params().set_uint("max_conflicts", 10);
-        p.copy(m_params);
+        s.params().set_bool("lookahead_simplify", true);
-        p.set_uint("max_conflicts", 10);
+        s.get_solver().updt_params(s.params());
-        p.set_bool("lookahead_simplify", true);
+        lbool is_sat = s.get_solver().check_sat(0,0);
-        s.updt_params(p);
+        s.params().set_uint("max_conflicts", get_max_conflicts());
-        lbool is_sat = s.check_sat(0,0);
+        s.params().set_bool("lookahead_simplify", false);
-        p.set_uint("max_conflicts", get_max_conflicts());
+        s.get_solver().updt_params(s.params());
-        p.set_bool("lookahead_simplify", false);
-        s.updt_params(p);
         return is_sat;
     }
 
@@ -228,12 +230,10 @@ private:
         return l_undef;
     }
 
-    lbool solve(solver& s) {
+    lbool solve(solver_state& s) {
-        params_ref p;
+        s.params().set_uint("max_conflicts", get_max_conflicts());
-        p.copy(m_params);
+        s.get_solver().updt_params(s.params());
-        p.set_uint("max_conflicts", get_max_conflicts());
+        return s.get_solver().check_sat(0, 0);
-        s.updt_params(p);
-        return s.check_sat(0, 0);
     }
 
     void remove_unsat(svector<int>& unsat) {
@@ -260,6 +260,25 @@ private:
     }
 
     lbool solve(model_ref& mdl) {        
+
+        {
+            solver_state& st = *m_solvers[0];
+            st.params().set_uint("restart.max", 200);
+            st.get_solver().updt_params(st.params());
+            lbool is_sat = st.get_solver().check_sat(0, 0);
+            st.params().set_uint("restart.max", UINT_MAX);
+            st.get_solver().updt_params(st.params());
+            switch (is_sat) {
+            case l_true: 
+                get_model(mdl, 0);
+                return l_true;
+            case l_false:
+                return l_false;
+            default:
+                break;
+            }
+        }
+            
         while (true) {
             int sz = pick_solvers();
 
@@ -276,7 +295,7 @@ private:
 
             #pragma omp parallel for
             for (int i = 0; i < sz; ++i) {
-                lbool is_sat = simplify(m_solvers[i]->get_solver());
+                lbool is_sat = simplify(*m_solvers[i]);
                 switch (is_sat) {
                 case l_false: 
                     #pragma omp critical (parallel_tactic)
@@ -305,7 +324,7 @@ private:
 
             #pragma omp parallel for
             for (int i = 0; i < sz; ++i) {
-                lbool is_sat = solve(m_solvers[i]->get_solver());
+                lbool is_sat = solve(*m_solvers[i]);
                 switch (is_sat) {
                 case l_false: 
                     #pragma omp critical (parallel_tactic)
@@ -328,6 +347,7 @@ private:
             remove_unsat(unsat);
 
             sz = std::min(max_num_splits(), sz);
+            sz = std::min(static_cast<int>(m_num_threads/2), sz);
             if (sz == 0) continue;
             
 
@@ -360,9 +380,9 @@ private:
     }
 
     std::ostream& display(std::ostream& out) {
+        out << "branches: " << m_solvers.size() << "\n";
         for (solver_state* s : m_solvers) {
-            out << "solver units " << s->num_units() << "\n";
+            out << "cube " << s->cube_size() << " units " << s->num_units() << "\n";
-            out << "cube " << s->cube() << "\n";
         }
         m_stats.display(out);
         return out;