fixing lookahead/ba + parallel

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

src/sat/ba_solver.cpp

@@ -300,6 +300,10 @@ namespace sat {
     void ba_solver::set_conflict(constraint& c, literal lit) {
         m_stats.m_num_conflicts++;
         TRACE("ba", display(tout, c, true); );
+        if (!validate_conflict(c)) {
+            display(std::cout, c, true);
+            UNREACHABLE();
+        }
         SASSERT(validate_conflict(c));
         if (c.is_xor() && value(lit) == l_true) lit.neg();
         SASSERT(value(lit) == l_false);
@@ -645,6 +649,7 @@ namespace sat {
                 display(verbose_stream(), p, true);
                 verbose_stream() << "alit: " << alit << "\n";
                 verbose_stream() << "num watch " << num_watch << "\n");
+            UNREACHABLE();
             exit(0);
             return l_undef;
         }

src/sat/sat_lookahead.cpp

@@ -92,7 +92,7 @@ namespace sat {
         // TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n"););
         literal_vector & lits = m_binary[idx];
         SASSERT(!lits.empty());
-        literal l = lits.back();			
+        literal l = lits.back();
         lits.pop_back();            
         SASSERT(!m_binary[(~l).index()].empty());
         IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";);
@@ -641,18 +641,18 @@ namespace sat {
     void lookahead::init_arcs(literal l) {
         literal_vector lits;
         literal_vector const& succ = m_binary[l.index()];
-        for (unsigned i = 0; i < succ.size(); ++i) {
+        for (literal u : succ) {
-            literal u = succ[i];
             SASSERT(u != l);
+            // l => u
             if (u.index() > l.index() && is_stamped(u)) {
                 add_arc(~l, ~u);
                 add_arc( u,  l);
             }
         }
         for (auto w : m_watches[l.index()]) {
-            if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
+            if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { 
                 for (literal u : lits) {
-                    if (u.index() > l.index() && is_stamped(u)) {
+                    if (u.index() > (~l).index() && is_stamped(u)) {
                         add_arc(~l, ~u);
                         add_arc( u,  l);
                     }
@@ -1298,6 +1298,8 @@ namespace sat {
         watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end();
         for (; it != end && !inconsistent(); ++it) {
             SASSERT(it->get_kind() == watched::EXT_CONSTRAINT);
+            VERIFY(is_true(l));
+            VERIFY(!is_undef(l));
             bool keep = m_s.m_ext->propagate(l, it->get_ext_constraint_idx());
             if (m_search_mode == lookahead_mode::lookahead1 && !m_inconsistent) {
                 lookahead_literal_occs_fun literal_occs_fn(*this);
@@ -1704,6 +1706,8 @@ namespace sat {
     }
 
     void lookahead::propagate_clauses(literal l) {
+        VERIFY(is_true(l));
+		VERIFY(value(l) == l_true);
         propagate_ternary(l);
         switch (m_search_mode) {
         case lookahead_mode::searching:
@@ -1713,6 +1717,9 @@ namespace sat {
             propagate_clauses_lookahead(l);
             break;
         }
+        VERIFY(!is_undef(l));
+        VERIFY(is_true(l));
+        VERIFY(value(l) == l_true);
         propagate_external(l);
     }
     
@@ -2179,8 +2186,10 @@ namespace sat {
 
     lbool lookahead::cube() {
         literal_vector lits;
+        bool_var_vector vars;
+        for (bool_var v : m_freevars) vars.push_back(v);
         while (true) {
-            lbool result = cube(lits);
+            lbool result = cube(vars, lits);
             if (lits.empty() || result != l_undef) {
                 return l_undef;
             }
@@ -2189,8 +2198,13 @@ namespace sat {
         return l_undef;
     }
 
-    lbool lookahead::cube(literal_vector& lits) {
+    lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits) {
+        scoped_ext _scoped_ext(*this);
         lits.reset();
+        m_select_lookahead_vars.reset();
+        for (auto v : vars) {
+            m_select_lookahead_vars.insert(v);
+        }
         bool is_first = m_cube_state.m_first;
         if (is_first) {
             init_search();
@@ -2412,6 +2426,7 @@ namespace sat {
        \brief simplify set of clauses by extracting units from a lookahead at base level.
     */
     void lookahead::simplify() {
+		scoped_ext _scoped_ext(*this);
         SASSERT(m_prefix == 0);
         SASSERT(m_watches.empty());
         m_search_mode = lookahead_mode::searching;

src/sat/sat_lookahead.h

@@ -571,9 +571,10 @@ namespace sat {
            If cut-depth != 0, then it is used to control the depth of cuts.
            Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
         */
+
         lbool cube();
 
-        lbool cube(literal_vector& lits);
+        lbool cube(bool_var_vector const& vars, literal_vector& lits);
 
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
         /**

src/sat/sat_solver.cpp

@@ -162,6 +162,7 @@ namespace sat {
         m_user_scope_literals.append(src.m_user_scope_literals);
 
         m_mc = src.m_mc;
+        m_stats.m_units = init_trail_size();
     }
 
     // -----------------------
@@ -837,11 +838,11 @@ namespace sat {
         return lh.select_lookahead(assumptions, vars);
     }
 
-    lbool  solver::cube(literal_vector& lits) {
+    lbool  solver::cube(bool_var_vector const& vars, literal_vector& lits) {
         if (!m_cuber) {
             m_cuber = alloc(lookahead, *this);
         }
-        lbool result = m_cuber->cube(lits);
+        lbool result = m_cuber->cube(vars, lits);
         if (result == l_false) {
             dealloc(m_cuber);
             m_cuber = nullptr;
@@ -858,6 +859,7 @@ namespace sat {
     lbool solver::check(unsigned num_lits, literal const* lits) {
         init_reason_unknown();
         pop_to_base_level();
+        m_stats.m_units = init_trail_size();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
         if (m_config.m_dimacs_display) {
@@ -4039,7 +4041,7 @@ namespace sat {
     }
 
     void stats::reset() {
-        memset(this, sizeof(*this), 0);
+        memset(this, 0, sizeof(*this));
     }
 
     void mk_stat::display(std::ostream & out) const {

src/sat/sat_solver.h

@@ -365,7 +365,7 @@ namespace sat {
         char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
 
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
-        lbool  cube(literal_vector& lits);
+        lbool  cube(bool_var_vector const& vars, literal_vector& lits);
 
     protected:
         unsigned m_conflicts_since_init;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -353,8 +353,12 @@ public:
             m_internalized = true;
         }
         convert_internalized();
+        sat::bool_var_vector vars;
+        for (auto& kv : m_map) {
+            vars.push_back(kv.m_value);
+        }
         sat::literal_vector lits;
-        lbool result = m_solver.cube(lits);
+        lbool result = m_solver.cube(vars, lits);
         if (result == l_false || lits.empty()) {
             return expr_ref(m.mk_false(), m);
         }

src/sat/tactic/goal2sat.cpp

@@ -94,12 +94,6 @@ struct goal2sat::imp {
         std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
         throw tactic_exception(s0.c_str());
     }
-
-    sat::bool_var mk_var(expr* t, bool ext) {
-        sat::bool_var v = m_solver.mk_var(ext);
-        m_map.insert(t, v);
-        return v;
-    }
     
     void mk_clause(sat::literal l) {
         TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
@@ -126,7 +120,7 @@ struct goal2sat::imp {
     sat::bool_var mk_true() {
         if (m_true == sat::null_bool_var) {
             // create fake variable to represent true;
-            m_true = mk_var(m.mk_true(), false);
+            m_true = m_solver.mk_var(false);
             mk_clause(sat::literal(m_true, false)); // v is true
         }
         return m_true;
@@ -145,7 +139,8 @@ struct goal2sat::imp {
             }
             else {
                 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
-                sat::bool_var v = mk_var(t, ext);
+                sat::bool_var v = m_solver.mk_var(ext);
+                m_map.insert(t, v);
                 l = sat::literal(v, sign);
                 TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
                 if (ext && !is_uninterp_const(t)) {
@@ -252,7 +247,7 @@ struct goal2sat::imp {
         }
         else {
             SASSERT(num <= m_result_stack.size());
-            sat::bool_var k = mk_var(t, false);
+            sat::bool_var k = m_solver.mk_var();
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             sat::literal * lits = m_result_stack.end() - num;
@@ -291,7 +286,7 @@ struct goal2sat::imp {
         }
         else {
             SASSERT(num <= m_result_stack.size());
-            sat::bool_var k = mk_var(t, false);
+            sat::bool_var k = m_solver.mk_var();
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             // l => /\ lits
@@ -335,7 +330,7 @@ struct goal2sat::imp {
             m_result_stack.reset();
         }
         else {
-            sat::bool_var k = mk_var(n, false);
+            sat::bool_var k = m_solver.mk_var();
             sat::literal  l(k, false);
             m_cache.insert(n, l);
             mk_clause(~l, ~c, t);
@@ -372,7 +367,7 @@ struct goal2sat::imp {
             m_result_stack.reset();
         }
         else {
-            sat::bool_var k = mk_var(t, false);
+            sat::bool_var k = m_solver.mk_var();
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             mk_clause(~l, l1, ~l2);
@@ -397,7 +392,7 @@ struct goal2sat::imp {
         }
         sat::literal_vector lits;
         convert_pb_args(num, lits);
-        sat::bool_var v = mk_var(t, true);
+        sat::bool_var v = m_solver.mk_var(true);
         ensure_extension();
         if (lits.size() % 2 == 0) lits[0].neg();
         m_ext->add_xor(v, lits);
@@ -456,7 +451,7 @@ struct goal2sat::imp {
             m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned());
         }
         else {
-            sat::bool_var v = mk_var(t, true);
+            sat::bool_var v = m_solver.mk_var(true);
             sat::literal lit(v, sign);
             m_ext->add_pb_ge(v, wlits, k.get_unsigned());
             TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@@ -481,7 +476,7 @@ struct goal2sat::imp {
             m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned());
         }
         else {
-            sat::bool_var v = mk_var(t, true);
+            sat::bool_var v = m_solver.mk_var(true);
             sat::literal lit(v, sign);
             m_ext->add_pb_ge(v, wlits, k.get_unsigned());
             TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@@ -530,7 +525,7 @@ struct goal2sat::imp {
             m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned());
         }
         else {
-            sat::bool_var v = mk_var(t, true);
+            sat::bool_var v = m_solver.mk_var(true);
             sat::literal lit(v, sign);
             m_ext->add_at_least(v, lits, k.get_unsigned());
             TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@@ -552,7 +547,7 @@ struct goal2sat::imp {
             m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned());
         }
         else {
-            sat::bool_var v = mk_var(t, true);
+            sat::bool_var v = m_solver.mk_var(true);
             sat::literal lit(v, sign);
             m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
             m_result_stack.shrink(sz - t->get_num_args());

src/tactic/portfolio/parallel_tactic.cpp

@@ -398,7 +398,6 @@ public:
                 mc = concat(fmc.get(), mc.get());
             }
             g->reset();
-            result.push_back(g.get());
             break;
         case l_false:
             SASSERT(!g->proofs_enabled());
@@ -409,9 +408,9 @@ public:
             if (m.canceled()) {
                 throw tactic_exception(Z3_CANCELED_MSG);
             }
-            result.push_back(g.get());
             break;
         }
+        result.push_back(g.get());
     }
 
     void cleanup() {