From 81ad69214c15831076beaa6839546ebbe099e698 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Oct 2017 17:06:28 -0700 Subject: [PATCH] fixing lookahead/ba + parallel Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 5 ++++ src/sat/sat_lookahead.cpp | 29 ++++++++++++++++++------ src/sat/sat_lookahead.h | 3 ++- src/sat/sat_solver.cpp | 8 ++++--- src/sat/sat_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 6 ++++- src/sat/tactic/goal2sat.cpp | 29 ++++++++++-------------- src/tactic/portfolio/parallel_tactic.cpp | 3 +-- 8 files changed, 53 insertions(+), 32 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 6a68c30c9..a2058512b 100644 --- a/src/sat/ba_solver.cpp +++ b/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; } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 0374aca9c..d0f4bc7f6 100644 --- a/src/sat/sat_lookahead.cpp +++ b/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) { - literal u = succ[i]; + for (literal u : succ) { 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; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 38f9b0481..6ff228427 100644 --- a/src/sat/sat_lookahead.h +++ b/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); /** diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3812eff56..8004c9635 100644 --- a/src/sat/sat_solver.cpp +++ b/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 { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index fa095623f..020c1dc42 100644 --- a/src/sat/sat_solver.h +++ b/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; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 908e56da8..53383a7c2 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/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); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 81302764a..3db2908ed 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/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()); diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 524754613..9bacbe6a0 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/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() {