diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index 0ce329046..9bb27430d 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -171,6 +171,8 @@ namespace smt { //update_propagation_scope(); return; } + if (ctx.m_stats.m_num_conflicts < m_conflict_gap) + return; m_after_resolve_decide_gap *= 2; if (!shared_clauses_are_true()) { update_propagation_scope(); @@ -221,7 +223,8 @@ namespace smt { if (m_parallel_mode || !m_smt_plugin) return; - if (ctx.m_stats.m_num_restarts >= m_restart_gap + 5) { + if (ctx.m_stats.m_num_restarts >= m_restart_gap + 5 && + m_conflict_gap <= ctx.m_stats.m_num_conflicts) { m_restart_gap *= 2; m_smt_plugin->smt_units_to_sls(); ++m_stats.m_num_restart_sls; @@ -234,6 +237,7 @@ namespace smt { void theory_sls::bounded_run(unsigned num_steps) { m_smt_plugin->bounded_run(num_steps); + m_conflict_gap = ctx.m_stats.m_num_conflicts + m_conflict_inc; if (m_smt_plugin->result() == l_true) { m_smt_plugin->finalize(m_model, m_st); m_smt_plugin = nullptr; @@ -244,6 +248,8 @@ namespace smt { final_check_status theory_sls::final_check_eh() { if (!m_smt_plugin) return FC_DONE; + if (ctx.m_stats.m_num_conflicts < m_conflict_gap) + return FC_DONE; ++m_after_resolve_decide_count; if (m_after_resolve_decide_gap > m_after_resolve_decide_count) return FC_DONE; diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index b0407cbdb..9f15dcf59 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -61,6 +61,8 @@ namespace smt { bool m_checking = false; bool m_parallel_mode = true; unsigned m_restart_gap = 1; + unsigned m_conflict_gap = 100; + unsigned m_conflict_inc = 200; unsigned m_restart_ls_steps = 100000; unsigned m_restart_ls_steps_inc = 10000; unsigned m_restart_ls_steps_max = 300000; diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 5b1c4831f..2a5332fbc 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -53,6 +53,7 @@ public: void throw_non_pb(expr * n) { TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";); + verbose_stream() << "not pb " << mk_pp(n, m) << "\n"; throw non_pb(n); } @@ -63,6 +64,10 @@ public: void operator()(app * n) { family_id fid = n->get_family_id(); if (fid == m.get_basic_family_id()) { + expr* c = nullptr, * th = nullptr, * el = nullptr; + rational r; + if (m.is_ite(n, c, th, el) && m_util.is_numeral(th) && m_util.is_numeral(el, r) && r.is_zero()) + return; // all basic family ops (but term-ite and distinct) are OK if (m.is_term_ite(n) || m.is_distinct(n)) throw_non_pb(n); @@ -340,7 +345,10 @@ private: if (r != nullptr) return r; - r = m.mk_fresh_const(nullptr, m.mk_bool_sort()); + if (m.is_bool(x)) + r = x; + else + r = m.mk_fresh_const(nullptr, m.mk_bool_sort()); expr * not_r = m.mk_not(r); m_const2bit.insert(fd, r); m_not_const2bit.insert(fd, not_r); @@ -745,11 +753,25 @@ private: unsigned sz = to_app(lhs)->get_num_args(); expr * const * ms = to_app(lhs)->get_args(); expr * a, * x; + + auto is_ite = [&](expr* e, rational& r) { + expr *cnd = nullptr, * th = nullptr, * el = nullptr; + return m.is_ite(e, cnd, th, el) && + m_arith_util.is_numeral(el, r) && + r.is_zero() && + m_arith_util.is_numeral(th, r);; + }; + for (unsigned i = 0; i < sz; i++) { - expr * m = ms[i]; - if (is_uninterp_const(m)) + expr* e = ms[i]; + rational r; + if (is_uninterp_const(e)) continue; - if (m_arith_util.is_mul(m, a, x) && m_arith_util.is_numeral(a) && is_uninterp_const(x)) + if (m_arith_util.is_mul(e, a, x) && m_arith_util.is_numeral(a) && is_uninterp_const(x)) + continue; + if (is_ite(e, r)) + continue; + if (m_arith_util.is_mul(e, a, x) && m_arith_util.is_numeral(a) && is_ite(x, r)) continue; throw_non_pb(t); } @@ -760,12 +782,14 @@ private: numeral m_c; m_c = c; for (unsigned i = 0; i < sz; i++) { - expr * m = ms[i]; - if (is_uninterp_const(m)) { - add_bounds_dependencies(m); - m_p.push_back(monomial(lit(m))); + expr * e = ms[i]; + expr* cnd = nullptr, * th = nullptr, * el = nullptr; + rational r1, r2; + if (is_uninterp_const(e)) { + add_bounds_dependencies(e); + m_p.push_back(monomial(lit(e))); } - else if (m_arith_util.is_mul(m, a, x) && m_arith_util.is_numeral(a, a_val)) { + else if (m_arith_util.is_mul(e, a, x) && m_arith_util.is_numeral(a, a_val) && is_uninterp_const(x)) { add_bounds_dependencies(x); if (a_val.is_neg()) { a_val.neg(); @@ -777,6 +801,25 @@ private: m_p.push_back(monomial(a_val, lit(x))); } } + else if (m_arith_util.is_mul(e, a, x) && m_arith_util.is_numeral(a, a_val) && is_ite(x, r1)) { + a_val *= r1; + if (a_val.is_neg()) { + a_val.neg(); + m_c += a_val; + m_p.push_back(monomial(a_val, lit(x, true))); + } + else + m_p.push_back(monomial(a_val, lit(x))); + } + else if (is_ite(e, r1)) { + if (r1.is_neg()) { + r1.neg(); + m_c += r1; + m_p.push_back(monomial(r1, lit(cnd, true))); + } + else + m_p.push_back(monomial(r1, lit(cnd))); + } else { UNREACHABLE(); } @@ -923,6 +966,7 @@ private: quick_pb_check(g); } catch (non_pb& p) { + verbose_stream() << mk_pp(p.e, m) << "\n"; throw_tactic(p.e); } @@ -954,6 +998,7 @@ private: } } catch (non_pb& p) { + verbose_stream() << mk_pp(p.e, m) << "\n"; throw_tactic(p.e); }