diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 26c5a33d5..1c9b44b52 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -168,6 +168,8 @@ public: } br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + + bool hi_div0() const { return m_hi_div0; } }; #endif diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 693200f61..f4d8e1b43 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -228,7 +228,6 @@ public: switch (is_sat) { case l_true: get_current_correction_set(cs); - IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs);); if (cs.empty()) { m_found_feasible_optimum = m_model.get() != 0; m_lower = m_upper; @@ -350,9 +349,11 @@ public: is_sat = minimize_core(core); ++m_stats.m_num_cores; if (is_sat != l_true) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); break; } if (core.empty()) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";); cores.reset(); m_lower = m_upper; return l_true; @@ -470,6 +471,7 @@ public: SASSERT(!core.empty()); rational w = split_core(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); + IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a27a1a4d2..0fc246464 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -110,7 +110,7 @@ namespace sat { buffer.reset(); for (unsigned i = 0; i < c.size(); i++) buffer.push_back(c[i]); - mk_clause(buffer.size(), buffer.c_ptr()); + mk_clause(buffer); } } } @@ -892,6 +892,7 @@ namespace sat { if (num_lits == 0 && m_user_scope_literals.empty()) { return; } + m_replay_lit = null_literal; retry_init_assumptions: m_assumptions.reset(); @@ -922,13 +923,8 @@ namespace sat { if (m_config.m_optimize_model) { m_wsls.set_soft(num_lits, lits, weights); } - else { - svector blocker; - if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) { - pop_to_base_level(); - mk_clause(blocker.size(), blocker.c_ptr()); - goto retry_init_assumptions; - } + else if (!init_weighted_assumptions(num_lits, lits, weights, max_weight)) { + goto retry_init_assumptions; } return; } @@ -939,55 +935,124 @@ namespace sat { m_assumption_set.insert(lit); m_assumptions.push_back(lit); assign(lit, justification()); - // propagate(false); } } - bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, - svector& blocker) { + void solver::resolve_weighted() { + flet _min1(m_config.m_minimize_core, false); + flet _min2(m_config.m_minimize_core_partial, false); + m_conflict_lvl = m_scope_lvl; + resolve_conflict_for_unsat_core(); + } + + bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { double weight = 0; - blocker.reset(); + literal_vector blocker; + literal_vector min_core; + bool min_core_valid = false; for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; SASSERT(is_external(lit.var())); - m_assumption_set.insert(lit); TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";); + SASSERT(m_scope_lvl == 1); + if (m_replay_lit == lit && value(lit) == l_undef) { + mk_clause(m_replay_clause); + propagate(false); + SASSERT(inconsistent() || value(lit) == l_false); + if (inconsistent()) { + IF_VERBOSE(1, verbose_stream() << lit << " cannot be false either\n";); + return true; + } + IF_VERBOSE(1, verbose_stream() << lit << " set to false\n";); + SASSERT(value(lit) == l_false); + if (m_replay_clause.size() < min_core.size() || !min_core_valid) { + min_core.reset(); + min_core.append(m_replay_clause); + min_core_valid = true; + } + m_replay_clause.reset(); + m_replay_lit = null_literal; + continue; + } switch(value(lit)) { case l_undef: + m_assumption_set.insert(lit); m_assumptions.push_back(lit); assign(lit, justification()); + propagate(false); + if (inconsistent()) { + resolve_weighted(); + m_replay_clause.reset(); + m_replay_lit = lit; + // next time around, the negation of the literal will be implied. + for (unsigned j = 0; j < m_core.size(); ++j) { + m_replay_clause.push_back(~m_core[j]); + } + pop_to_base_level(); + IF_VERBOSE(11, + verbose_stream() << "undef: " << lit << " : " << m_replay_clause << "\n"; + verbose_stream() << m_assumptions << "\n";); + return false; + } + blocker.push_back(~lit); break; - case l_false: { + + case l_false: + m_assumption_set.insert(lit); m_assumptions.push_back(lit); SASSERT(!inconsistent()); set_conflict(justification(), ~lit); - flet _min1(m_config.m_minimize_core, false); - flet _min2(m_config.m_minimize_core_partial, false); - resolve_conflict_for_unsat_core(); - m_assumptions.pop_back(); + resolve_weighted(); weight += weights[i]; - blocker.push_back(lit); TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";); - SASSERT(m_core.size() <= m_assumptions.size() + 1); - SASSERT(m_assumptions.size() <= i); - if (m_core.size() <= 3 || m_core.size() < blocker.size()) { - TRACE("opt", tout << "found small core: " << m_core.size() << "\n";); + SASSERT(m_core.size() <= m_assumptions.size()); + SASSERT(m_assumptions.size() <= i+1); + if (m_core.size() <= 3) { + m_inconsistent = true; + TRACE("opt", tout << "found small core: " << m_core << "\n";); + IF_VERBOSE(11, verbose_stream() << "small core: " << m_core << "\n";); return true; } - m_inconsistent = false; if (weight >= max_weight) { ++m_stats.m_blocked_corr_sets; - TRACE("opt", tout << "blocking soft correction set: " << blocker.size() << "\n";); + TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); // block the current correction set candidate. + IF_VERBOSE(11, verbose_stream() << "blocking " << blocker << "\n";); + pop_to_base_level(); + mk_clause(blocker); return false; } + VERIFY(m_assumptions.back() == m_assumption_set.pop()); + m_assumptions.pop_back(); + m_inconsistent = false; + if (!min_core_valid || m_core.size() < min_core.size()) { + min_core.reset(); + min_core.append(m_core); + min_core_valid = true; + } + blocker.push_back(lit); break; - } case l_true: break; } - propagate(false); + } + TRACE("sat", tout << "initialized\n";); + IF_VERBOSE(11, verbose_stream() << "Blocker: " << blocker << " - " << min_core << "\n";); + if (min_core_valid && blocker.size() > min_core.size()) { + pop_to_base_level(); + push(); + m_assumption_set.reset(); + m_assumptions.reset(); + for (unsigned i = 0; i < min_core.size(); ++i) { + literal lit = min_core[i]; + SASSERT(is_external(lit.var())); + m_assumption_set.insert(lit); + m_assumptions.push_back(lit); + assign(lit, justification()); + } + propagate(false); + SASSERT(inconsistent()); } return true; } @@ -2510,6 +2575,7 @@ namespace sat { // // ----------------------- bool solver::check_invariant() const { + if (m_cancel) return true; integrity_checker checker(*this); SASSERT(checker()); return true; @@ -2630,7 +2696,7 @@ namespace sat { out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n"; for (unsigned i = 0; i < m_trail.size(); i++) { - out << dimacs_lit(m_trail[i]) << " 0\n"; + out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n"; } vector::const_iterator it = m_watches.begin(); vector::const_iterator end = m_watches.end(); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c656465ed..60b6f46de 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -175,6 +175,7 @@ namespace sat { // // ----------------------- bool_var mk_var(bool ext = false, bool dvar = true); + void mk_clause(literal_vector const& lits) { mk_clause(lits.size(), lits.c_ptr()); } void mk_clause(unsigned num_lits, literal * lits); void mk_clause(literal l1, literal l2); void mk_clause(literal l1, literal l2, literal l3); @@ -296,8 +297,12 @@ namespace sat { bool_var next_var(); lbool bounded_search(); void init_search(); + + literal m_replay_lit; + literal_vector m_replay_clause; void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); - bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, svector& blocker); + bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); + void resolve_weighted(); void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 2def82b80..c0c087e59 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -228,6 +228,7 @@ namespace sat { return result; } void insert(literal l) { m_set.insert(l.index()); } + literal pop() { return to_literal(m_set.erase()); } bool contains(literal l) const { return m_set.contains(l.index()); } bool empty() const { return m_set.empty(); } unsigned size() const { return m_set.size(); } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index c02c6760a..bd5f53922 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -252,6 +252,7 @@ void asserted_formulas::reduce() { TRACE("before_reduce", display(tout);); CASSERT("well_sorted", check_well_sorted()); + #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; } set_eliminate_and(false); // do not eliminate and before nnf. diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index a68d4d820..818e12fd1 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -115,8 +115,7 @@ namespace smt { break; case eq_justification::CONGRUENCE: { TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " congruence\n";); - if (!lhs->is_eq()) - TRACE("dyn_ack_target", tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";); + CTRACE("dyn_ack_target", !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";); m_dyn_ack_manager.used_cg_eh(lhs->get_owner(), rhs->get_owner()); unsigned num_args = lhs->get_num_args(); SASSERT(num_args == rhs->get_num_args()); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 98ad5e51a..dba4ef57f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -52,6 +52,7 @@ namespace smt { // } TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";); m_already_configured = true; + switch (cm) { case CFG_BASIC: setup_unknown(); break; case CFG_LOGIC: setup_default(); break; @@ -550,6 +551,7 @@ namespace smt { m_params.m_bv_cc = false; m_params.m_bb_ext_gates = true; m_params.m_nnf_cnf = false; + m_params.m_propagate_booleans = true; m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params)); m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params)); } diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 725d38ed5..a42f00274 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -161,9 +161,11 @@ public: struct scoped_init_ctx { smt_tactic & m_owner; + smt_params m_params; // smt-setup overwrites parameters depending on the current assertions. scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) { - smt::kernel * new_ctx = alloc(smt::kernel, m, o.fparams()); + m_params = o.fparams(); + smt::kernel * new_ctx = alloc(smt::kernel, m, m_params); TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";); new_ctx->set_logic(o.m_logic); if (o.m_callback) { @@ -199,7 +201,8 @@ public: << " PREPROCESS: " << fparams().m_preprocess << "\n"; tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n"; tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; - tout << "params_ref: " << m_params_ref << "\n";); + tout << "params_ref: " << m_params_ref << "\n"; + tout << "nnf: " << fparams().m_nnf_cnf << "\n";); TRACE("smt_tactic_detail", in->display(tout);); TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); scoped_init_ctx init(*this, m); @@ -239,7 +242,6 @@ public: else r = m_ctx->check(assumptions.size(), assumptions.c_ptr()); m_ctx->collect_statistics(m_stats); - switch (r) { case l_true: { if (m_fail_if_inconclusive && !in->sat_preserved()) diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index fc9138bf6..43ec5682e 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -235,13 +235,14 @@ namespace smt { } app* mk_bv_constant(uint64 val, sort* s) { - return b().mk_numeral(rational(val,rational::ui64()),64); + return b().mk_numeral(rational(val, rational::ui64()), 64); } app* max_value(sort* s) { uint64 sz; VERIFY(u().try_get_size(s, sz)); - return mk_bv_constant(sz, s); + SASSERT(sz > 0); + return mk_bv_constant(sz-1, s); } void mk_lt(app* x, app* y) { diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 5f20015ca..f6a6017de 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include"rewriter_def.h" #include"for_each_expr.h" #include"cooperate.h" +#include"bv_rewriter.h" class bv1_blaster_tactic : public tactic { @@ -491,6 +492,8 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) { class is_qfbv_eq_probe : public probe { public: virtual result operator()(goal const & g) { + bv_rewriter rw(g.m()); + if (!rw.hi_div0()) return false; bv1_blaster_tactic t(g.m()); return t.is_target(g); diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 0fdd49a6b..dd27691d3 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -23,6 +23,7 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"goal_util.h" +#include"bv_rewriter.h" class memory_probe : public probe { public: @@ -303,6 +304,8 @@ public: class is_qfbv_probe : public probe { public: virtual result operator()(goal const & g) { + bv_rewriter rw(g.m()); + if (!rw.hi_div0()) return false; return !test(g); } };