From 0181f0f9dfd51fa4a8d3a3293c839d076a570ac2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Mar 2014 18:03:20 -0700 Subject: [PATCH] add bvmax tactic, add proviso for non-0 lower bounds in elim01 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 6 ++ src/cmd_context/cmd_context.h | 1 + src/opt/opt_context.h | 3 +- src/opt/opt_solver.cpp | 1 + src/opt/weighted_maxsat.cpp | 98 +++++++++++++++++++++++++++--- src/sat/sat_solver.cpp | 2 +- src/smt/theory_pb.cpp | 8 +++ src/tactic/arith/elim01_tactic.cpp | 16 ++++- 8 files changed, 121 insertions(+), 14 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 993b8d68f..ca9e90430 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1376,6 +1376,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions throw cmd_exception(ex.msg()); } get_opt()->set_status(r); + if (r != l_false) { + get_opt()->display_assignment(regular_stream()); + } } else if (m_solver) { m_check_sat_result = m_solver.get(); // solver itself stores the result. @@ -1580,6 +1583,9 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) { else if (m_solver) { m_solver->collect_statistics(st); } + else if (m_opt) { + m_opt->collect_statistics(st); + } st.display_smt2(regular_stream()); } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index dc0bf9833..8f7fc3228 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -121,6 +121,7 @@ public: virtual void cancel() = 0; virtual lbool optimize() = 0; virtual void set_hard_constraints(ptr_vector & hard) = 0; + virtual void display_assignment(std::ostream& out) = 0; }; class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 798a67a1c..fe5f91406 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -122,8 +122,7 @@ namespace opt { virtual void get_unsat_core(ptr_vector & r) {} virtual std::string reason_unknown() const { return std::string("unknown"); } - void display_assignment(std::ostream& out); - void display_range_assignment(std::ostream& out); + virtual void display_assignment(std::ostream& out); static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 7b23161d6..434f88a5a 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -44,6 +44,7 @@ namespace opt { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); + m_params.m_relevancy_lvl = 0; } unsigned opt_solver::m_dump_count = 0; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 597bfa6b0..539ba74e9 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -29,6 +29,9 @@ Notes: #include "tactic.h" #include "model_smt2_pp.h" #include "pb_sls.h" +#include "qfbv_tactic.h" +#include "card2bv_tactic.h" +#include "tactic2solver.h" namespace smt { @@ -450,6 +453,7 @@ namespace opt { volatile bool m_cancel; params_ref m_params; opt_solver m_solver; + ref m_sat_solver; scoped_ptr m_imp; smt::pb_sls m_sls; @@ -511,6 +515,9 @@ namespace opt { if (m_engine == symbol("pwmax")) { return pb_solve(); } + if (m_engine == symbol("bvmax")) { + return pb2sat_solve(); + } if (m_engine == symbol("wpm2")) { return wpm2_solve(); } @@ -520,7 +527,11 @@ namespace opt { if (m_engine == symbol("sls")) { return sls_solve(); } - return incremental_solve(); + if (m_engine == symbol::null || m_engine == symbol("wmax")) { + return incremental_solve(); + } + IF_VERBOSE(0, verbose_stream() << "(unknown engine " << m_engine << " using default 'wmax')\n";); + return incremental_solve(); } rational get_lower() const { @@ -535,6 +546,25 @@ namespace opt { mdl = m_model.get(); } + void set_cancel(bool f) { + if (m_sat_solver) { + m_sat_solver->set_cancel(f); + } + m_sls.set_cancel(f); + m_cancel = f; + m_solver.set_cancel(f); + m_imp->m_cancel = f; + m_imp->m_solver.set_cancel(f); + } + + void collect_statistics(statistics& st) const { + m_solver.collect_statistics(st); + if (m_sat_solver) { + m_sat_solver->collect_statistics(st); + } + } + + class scoped_ensure_theory { smt::theory_weighted_maxsat* m_wth; public: @@ -732,7 +762,6 @@ namespace opt { // convert bounds constraint into pseudo-Boolean - lbool pb_solve() { pb_util u(m); expr_ref fml(m), val(m); @@ -778,6 +807,63 @@ namespace opt { return is_sat; } + // + // convert bounds constraint into pseudo-Boolean, + // then treat pseudo-Booleans as bit-vectors and + // sorting circuits. + // + lbool pb2sat_solve() { + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); + tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); + tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); + m_sat_solver = mk_tactic2solver(m, tac.get(), m_params); + unsigned sz = s.get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + m_sat_solver->assert_expr(s.get_assertion(i)); + } + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + b = m.mk_fresh_const("b", m.mk_bool_sort()); + // TODO: s.mc().insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + m_sat_solver->assert_expr(fml); + nsoft.push_back(b); + } + lbool is_sat = l_true; + bool was_sat = false; + while (l_true == is_sat) { + is_sat = m_sat_solver->check_sat(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + m_sat_solver->get_model(m_model); + m_upper = rational::zero(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(nsoft[i].get(), val)); + m_assignment[i] = !m.is_true(val); + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } + } + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); + m_sat_solver->assert_expr(fml); + was_sat = true; + } + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + m_lower = m_upper; + } + return is_sat; + } + expr* mk_not(expr* e) { if (m.is_not(e, e)) { return e; @@ -1285,14 +1371,10 @@ namespace opt { return m_imp->m_assignment[idx]; } void wmaxsmt::set_cancel(bool f) { - m_imp->m_sls.set_cancel(f); - m_imp->m_cancel = f; - m_imp->m_solver.set_cancel(f); - m_imp->m_imp->m_cancel = f; - m_imp->m_imp->m_solver.set_cancel(f); + m_imp->set_cancel(f); } void wmaxsmt::collect_statistics(statistics& st) const { - m_imp->m_solver.collect_statistics(st); + m_imp->collect_statistics(st); } void wmaxsmt::get_model(model_ref& mdl) { m_imp->get_model(mdl); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f57623774..e807915c4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -686,7 +686,7 @@ namespace sat { // // ----------------------- lbool solver::check() { - IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";); + IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";); SASSERT(scope_lvl() == 0); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index aa0bff164..f0ea8f6e6 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1558,6 +1558,8 @@ namespace smt { } } + static unsigned s_min_l_size = UINT_MAX; + // // modeled after sat_solver/smt_context // @@ -1731,6 +1733,12 @@ namespace smt { m_lemma.prune(false); IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma);); + //unsigned l_size = m_ineq_literals.size() + ((is_true==l_false)?0:m_lemma.size()); + //if (s_min_l_size >= l_size) { + // verbose_stream() << "(pb.conflict min size: " << l_size << ")\n"; + // s_min_l_size = l_size; + //} + //IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << "\n";); switch(is_true) { case l_true: UNREACHABLE(); diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index ad6e2c3b0..300291cb2 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -167,6 +167,7 @@ public: expr_ref_vector axioms(m); bounds(*g); + rational zero(0); bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); for (; bit != bend; ++bit) { if (!is_app(*bit)) continue; @@ -174,9 +175,14 @@ public: bool s1, s2; rational lo, hi; if (a.is_int(x) && - bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && - bounds.has_upper(x, hi, s2) && !s2 && hi <= m_max_hi) { - add_variable(b2i, sub, x, hi.get_unsigned(), axioms); + bounds.has_lower(x, lo, s1) && !s1 && zero <= lo && + bounds.has_upper(x, hi, s2) && !s2 && hi <= m_max_hi && lo <= hi) { + add_variable(b2i, sub, x, lo.get_unsigned(), hi.get_unsigned(), axioms); + } + else if (a.is_int(x)) { + TRACE("pb", tout << "Not adding variable " << mk_pp(x, m) << " has lower: " + << bounds.has_lower(x, lo, s1) << " " << lo << " has upper: " + << bounds.has_upper(x, hi, s2) << " " << hi << "\n";); } } @@ -209,6 +215,7 @@ public: void add_variable(bool2int_model_converter* b2i, expr_safe_replace& sub, app* x, + unsigned min_value, unsigned max_value, expr_ref_vector& axioms) { std::string name = x->get_decl()->get_name().str(); @@ -242,6 +249,9 @@ public: if ((max_value & (max_value + 1)) != 0) { axioms.push_back(a.mk_le(sum, a.mk_numeral(rational(max_value), true))); } + if (min_value > 0) { + axioms.push_back(a.mk_ge(sum, a.mk_numeral(rational(min_value), true))); + } } };