From 2b48092541925a0f89f3cf83e3dceffc7486f513 Mon Sep 17 00:00:00 2001 From: unknown Date: Sun, 23 Aug 2015 10:58:12 -0700 Subject: [PATCH 1/9] local sat solver change Signed-off-by: unknown --- src/sat/sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3d6130d5e..8761873bc 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2626,7 +2626,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(); From ee5f1ad6b62269624c961c45f44cab46daf904fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 15:55:40 -0700 Subject: [PATCH 2/9] fix issue #203: domain range was one too large Signed-off-by: unknown --- src/smt/theory_dl.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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) { From ef7915858bca5e759ee0a34df2ae976e7e507bef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 16:27:07 -0700 Subject: [PATCH 3/9] add filter to detect circumventing the default semantics of bit-vector division with the use of the sat-based bit-vector solver. Provides a way to fix issue #190 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.h | 2 ++ src/tactic/bv/bv1_blaster_tactic.cpp | 3 +++ src/tactic/probe.cpp | 3 +++ 3 files changed, 8 insertions(+) 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/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); } }; From b2ebd095cb76eacb9fa4f083b1300e68f0035626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 17:01:46 -0700 Subject: [PATCH 4/9] fix for unintialized variable m_conflict_lvl Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 4 +++- src/sat/sat_solver.cpp | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) 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 db82cbe0e..9d4f5df0f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -964,6 +964,7 @@ namespace sat { set_conflict(justification(), ~lit); flet _min1(m_config.m_minimize_core, false); flet _min2(m_config.m_minimize_core_partial, false); + m_conflict_lvl = 1; resolve_conflict_for_unsat_core(); m_assumptions.pop_back(); weight += weights[i]; From 7639eff29b92b9a7ee3aa2af52af6985f44e18ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Aug 2015 11:09:10 -0700 Subject: [PATCH 5/9] retain default configuration between calls to SMT tactic so that values are not overwritten between calls to smt-setup. Fixes bug #196 Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 1 + src/smt/smt_setup.cpp | 1 + src/smt/tactic/smt_tactic.cpp | 8 +++++--- 3 files changed, 7 insertions(+), 3 deletions(-) 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_setup.cpp b/src/smt/smt_setup.cpp index 98ad5e51a..b72ecbd84 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; 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()) From d00d6a3506d57a2a58d3a62e9e915ce05697f676 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Aug 2015 13:21:33 -0700 Subject: [PATCH 6/9] enable Boolean propagation in AUFBV to fix inefficiency (bit-blasting destroys simplifications that are possible by simple Boolean propagation). Fixes issue #194 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 3 +-- src/smt/smt_setup.cpp | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) 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 b72ecbd84..dba4ef57f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -551,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)); } From af9143b64aea6c90f4068f88448d64d9ef86c733 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Aug 2015 17:15:31 -0700 Subject: [PATCH 7/9] tune initial propagation for pd-maxres Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 68 +++++++++++++++++++++++++++--------------- src/sat/sat_solver.h | 1 + 2 files changed, 45 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9d4f5df0f..6755d1778 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -943,6 +943,14 @@ namespace sat { } } + 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(); + m_assumptions.pop_back(); + } + bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, svector& blocker) { double weight = 0; @@ -952,44 +960,56 @@ namespace sat { SASSERT(is_external(lit.var())); m_assumption_set.insert(lit); TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";); - + SASSERT(m_scope_lvl == 1); switch(value(lit)) { case l_undef: m_assumptions.push_back(lit); assign(lit, justification()); + propagate(false); + if (inconsistent()) { + resolve_weighted(); + pop(1); + push(); + for (unsigned j = 0; j < m_assumptions.size(); ++j) { + assign(m_assumptions[j], justification()); + } + propagate(false); + goto post_process_false; + } break; + case l_false: { 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); - m_conflict_lvl = 1; - resolve_conflict_for_unsat_core(); - m_assumptions.pop_back(); - 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";); - 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";); - // block the current correction set candidate. - return false; - } - break; + resolve_weighted(); + goto post_process_false; } case l_true: break; } - propagate(false); + continue; + + post_process_false: + 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_inconsistent = true; + TRACE("opt", tout << "found 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";); + // block the current correction set candidate. + return false; + } } + TRACE("sat", tout << "initialized\n";); return true; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c656465ed..8c9c613c0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -298,6 +298,7 @@ namespace sat { void init_search(); 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); + void resolve_weighted(); void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; From 7c47809973a2da7efed8fa91b40c3f83ceeae130 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Aug 2015 16:33:53 -0700 Subject: [PATCH 8/9] reworking pd-maxres Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 90 +++++++++++++++++++++++++++--------------- src/sat/sat_solver.h | 3 +- src/sat/sat_types.h | 1 + 3 files changed, 61 insertions(+), 33 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 6755d1778..64eb10148 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -926,7 +926,7 @@ namespace sat { svector blocker; if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) { pop_to_base_level(); - mk_clause(blocker.size(), blocker.c_ptr()); + mk_clause(blocker.size(), blocker.c_ptr()); goto retry_init_assumptions; } } @@ -948,68 +948,93 @@ namespace sat { flet _min2(m_config.m_minimize_core_partial, false); m_conflict_lvl = m_scope_lvl; resolve_conflict_for_unsat_core(); - m_assumptions.pop_back(); } bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, svector& blocker) { double weight = 0; blocker.reset(); + svector 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); 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(); - pop(1); - push(); - for (unsigned j = 0; j < m_assumptions.size(); ++j) { - assign(m_assumptions[j], justification()); + blocker.reset(); + // next time around, the negation of the literal will be implied. + for (unsigned j = 0; j < m_core.size(); ++j) { + blocker.push_back(~m_core[j]); } - propagate(false); - goto post_process_false; + IF_VERBOSE(1, + verbose_stream() << "undef: " << lit << " : " << blocker << "\n"; + verbose_stream() << m_assumptions << "\n";); + // TBD: avoid redoing assignments, bail out for a full assignment. + 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); resolve_weighted(); - goto post_process_false; - } + weight += weights[i]; + TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\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(1, verbose_stream() << "small core: " << m_core << "\n";); + return true; + } + if (weight >= max_weight) { + ++m_stats.m_blocked_corr_sets; + TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); + // block the current correction set candidate. + IF_VERBOSE(1, verbose_stream() << "blocking " << blocker << "\n";); + 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); + } + blocker.push_back(lit); + break; case l_true: break; } - continue; - - post_process_false: - 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_inconsistent = true; - TRACE("opt", tout << "found 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";); - // block the current correction set candidate. - return false; - } } TRACE("sat", tout << "initialized\n";); + IF_VERBOSE(1, verbose_stream() << blocker << " - " << min_core << "\n";); + if (min_core_valid && blocker.size() > min_core.size()) { + pop_to_base_level(); + 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; } @@ -2531,6 +2556,7 @@ namespace sat { // // ----------------------- bool solver::check_invariant() const { + if (m_cancel) return true; integrity_checker checker(*this); SASSERT(checker()); return true; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 8c9c613c0..f8f3cd13b 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -297,7 +297,8 @@ namespace sat { lbool bounded_search(); void init_search(); 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, svector& blocker); void resolve_weighted(); void reinit_assumptions(); bool tracking_assumptions() 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(); } From 8622356375b026cfacbf4ffc0c46594d28e1c04b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Aug 2015 08:09:46 -0700 Subject: [PATCH 9/9] working on pd-maxres Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 61 +++++++++++++++++++++++++++--------------- src/sat/sat_solver.h | 7 +++-- 2 files changed, 45 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 64eb10148..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,7 +935,6 @@ namespace sat { m_assumption_set.insert(lit); m_assumptions.push_back(lit); assign(lit, justification()); - // propagate(false); } } @@ -950,17 +945,36 @@ namespace sat { resolve_conflict_for_unsat_core(); } - bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, - svector& blocker) { + bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { double weight = 0; - blocker.reset(); - svector min_core; + 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())); 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); @@ -969,15 +983,16 @@ namespace sat { propagate(false); if (inconsistent()) { resolve_weighted(); - blocker.reset(); + 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) { - blocker.push_back(~m_core[j]); + m_replay_clause.push_back(~m_core[j]); } - IF_VERBOSE(1, - verbose_stream() << "undef: " << lit << " : " << blocker << "\n"; + pop_to_base_level(); + IF_VERBOSE(11, + verbose_stream() << "undef: " << lit << " : " << m_replay_clause << "\n"; verbose_stream() << m_assumptions << "\n";); - // TBD: avoid redoing assignments, bail out for a full assignment. return false; } blocker.push_back(~lit); @@ -996,14 +1011,16 @@ namespace sat { if (m_core.size() <= 3) { m_inconsistent = true; TRACE("opt", tout << "found small core: " << m_core << "\n";); - IF_VERBOSE(1, verbose_stream() << "small core: " << m_core << "\n";); + IF_VERBOSE(11, verbose_stream() << "small core: " << m_core << "\n";); return true; } if (weight >= max_weight) { ++m_stats.m_blocked_corr_sets; TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); // block the current correction set candidate. - IF_VERBOSE(1, verbose_stream() << "blocking " << blocker << "\n";); + 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()); @@ -1012,6 +1029,7 @@ namespace sat { 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; @@ -1020,9 +1038,10 @@ namespace sat { } } TRACE("sat", tout << "initialized\n";); - IF_VERBOSE(1, verbose_stream() << blocker << " - " << min_core << "\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) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f8f3cd13b..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,9 +297,11 @@ 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;