From 06ae0db116034afbd00bf206acdf97b703d2c8ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2013 18:04:05 -0800 Subject: [PATCH] working on pb solver Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 41 ++++++++------- src/opt/fu_malik.cpp | 38 ++++++++++---- src/smt/theory_card.cpp | 109 +++++++++++++++++++++++++++++++++------- src/smt/theory_card.h | 3 ++ src/util/region.h | 1 + 5 files changed, 144 insertions(+), 48 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index f684879ae..66b56d8d4 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -1054,7 +1054,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { ptr_vector ql; - decl_collector decls(m_manager); + ast_manager& m = m_manager; + decl_collector decls(m); smt_renaming rn; for (unsigned i = 0; i < m_assumptions.size(); ++i) { @@ -1065,7 +1066,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { } decls.visit(n); - if (m_manager.is_proof(n)) { + if (m.is_proof(n)) { strm << "("; } if (m_benchmark_name != symbol::null) { @@ -1074,7 +1075,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { if (m_source_info != symbol::null && m_source_info != symbol("")) { strm << "; :source { " << m_source_info << " }\n"; } - if (m_manager.is_bool(n)) { + if (m.is_bool(n)) { strm << "(set-info :status " << m_status << ")\n"; } if (m_category != symbol::null && m_category != symbol("")) { @@ -1091,7 +1092,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { sort* s = decls.get_sorts()[i]; if (!(*m_is_declared)(s)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p.pp_sort_decl(sort_mark, s); } } @@ -1099,7 +1100,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_decls(); ++i) { func_decl* d = decls.get_func_decls()[i]; if (!(*m_is_declared)(d)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); strm << "\n"; } @@ -1108,34 +1109,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < decls.get_num_preds(); ++i) { func_decl* d = decls.get_pred_decls()[i]; if (!(*m_is_declared)(d)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0); + smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p(d); strm << "\n"; } } for (unsigned i = 0; i < m_assumptions.size(); ++i) { - strm << "(assert\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - p(m_assumptions[i].get()); - strm << ")\n"; + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); + strm << "(assert\n "; + p(m_assumptions[i].get()); + strm << ")\n"; } for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - strm << "(assert\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - p(m_assumptions_star[i].get()); + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); + strm << "(assert\n "; + p(m_assumptions_star[i].get()); strm << ")\n"; } - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0); - if (m_manager.is_bool(n)) { - strm << "(assert\n"; - p(n); - strm << ")\n"; + smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0); + if (m.is_bool(n)) { + if (!m.is_true(n)) { + strm << "(assert\n "; + p(n); + strm << ")\n"; + } strm << "(check-sat)\n"; } - else if (m_manager.is_proof(n)) { + else if (m.is_proof(n)) { strm << "(proof\n"; p(n); strm << "))\n"; diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 6ba3bba39..2d9c25be1 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -18,6 +18,8 @@ Notes: --*/ #include "fu_malik.h" +#include "smtlogics/qfbv_tactic.h" +#include "tactic2solver.h" /** \brief Fu & Malik procedure for MaxSAT. This procedure is based on @@ -37,17 +39,18 @@ namespace opt { struct fu_malik::imp { ast_manager& m; - solver& s; + ref m_s; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; expr_ref_vector m_assignment; unsigned m_upper_size; + solver& s() { return *m_s; } imp(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), - s(s), + m_s(&s), m_soft(soft), m_orig_soft(soft), m_aux(m), @@ -78,13 +81,13 @@ namespace opt { for (unsigned i = 0; i < m_soft.size(); ++i) { assumptions.push_back(m.mk_not(m_aux[i].get())); } - lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr()); + lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_false) { return is_sat; } ptr_vector core; - s.get_unsat_core(core); + s().get_unsat_core(core); // Update soft-constraints and aux_vars for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -101,7 +104,7 @@ namespace opt { m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); m_soft[i] = m.mk_or(m_soft[i].get(), block_var); block_vars.push_back(block_var); - s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); + s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); } assert_at_most_one(block_vars); return l_false; @@ -111,7 +114,7 @@ namespace opt { expr_ref has_one(m), has_zero(m), at_most_one(m); mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero); at_most_one = m.mk_or(has_one, has_zero); - s.assert_expr(at_most_one); + s().assert_expr(at_most_one); } void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) { @@ -129,15 +132,30 @@ namespace opt { has_zero = m.mk_and(has_zero1, has_zero2); } } + + void set_solver() { + solver& original_solver = s(); + bool all_bv = false; + // retrieve goal from s() + // extract mk_qfbv_probe + // run probe on goals + // if result is "yes", then create teh qfbv_tactic. + + if (all_bv) { + tactic* t = mk_qfbv_tactic(m); + m_s = mk_tactic2solver(m, t); + } + } // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef lbool operator()() { - lbool is_sat = s.check_sat(0,0); + set_solver(); + lbool is_sat = s().check_sat(0,0); if (!m_soft.empty() && is_sat == l_true) { - solver::scoped_push _sp(s); + solver::scoped_push _sp(s()); for (unsigned i = 0; i < m_soft.size(); ++i) { m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); - s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); + s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); } lbool is_sat = l_true; @@ -150,7 +168,7 @@ namespace opt { if (is_sat == l_true) { // Get a list of satisfying m_soft model_ref model; - s.get_model(model); + s().get_model(model); m_assignment.reset(); for (unsigned i = 0; i < m_orig_soft.size(); ++i) { diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index c32b600c1..d593e3742 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -136,6 +136,12 @@ namespace smt { if (a == 0) return b; if (b == 0) return a; while (a != b) { + if (a == 0) { + return b; + } + if (b == 0) { + return a; + } if (a < b) { b %= a; } @@ -171,7 +177,7 @@ namespace smt { if (!args.empty()) { unsigned g = abs(args[0].second); for (unsigned i = 1; g > 1 && i < args.size(); ++i) { - g = gcd(g, args[i].second); + g = gcd(g, abs(args[i].second)); } if (g > 1) { int k = c->m_k; @@ -183,7 +189,7 @@ namespace smt { k = abs(k); k += (k % g); k /= g; - k = -k; + c->m_k = -k; } for (unsigned i = 0; i < args.size(); ++i) { args[i].second /= g; @@ -213,6 +219,7 @@ namespace smt { void theory_card::collect_statistics(::statistics& st) const { st.update("pb axioms", m_stats.m_num_axioms); + st.update("pb propagations", m_stats.m_num_propagations); st.update("pb predicates", m_stats.m_num_predicates); st.update("pb compilations", m_stats.m_num_compiles); } @@ -316,6 +323,21 @@ namespace smt { return curr_min; } + int theory_card::get_max_delta(card& c) { + if (m_util.is_at_most_k(c.m_app)) { + return 1; + } + int max = 0; + context& ctx = get_context(); + for (unsigned i = 0; i < c.m_args.size(); ++i) { + if (c.m_args[i].second > max && ctx.get_assignment(c.m_args[i].first) == l_undef) { + max = c.m_args[i].second; + } + } + return max; + } + + int theory_card::accumulate_max(literal_vector& lits, card& c) { context& ctx = get_context(); arg_t const& args = c.m_args; @@ -364,19 +386,17 @@ namespace smt { lbool aval = ctx.get_assignment(abv); if (min > k && aval != l_false) { literal_vector& lits = get_lits(); - lits.push_back(~literal(abv)); int curr_min = accumulate_min(lits, c); SASSERT(curr_min > k); - add_clause(c, lits); + add_assign(c, lits, ~literal(abv)); } else if (max <= k && aval != l_true) { literal_vector& lits = get_lits(); - lits.push_back(literal(abv)); int curr_max = accumulate_max(lits, c); SASSERT(curr_max <= k); - add_clause(c, lits); + add_assign(c, lits, literal(abv)); } - else if (min == k && aval == l_true) { + else if (min <= k && k < min + get_max_delta(c) && aval == l_true) { literal_vector& lits = get_lits(); lits.push_back(~literal(abv)); int curr_min = accumulate_min(lits, c); @@ -384,37 +404,70 @@ namespace smt { add_clause(c, lits); } else { - SASSERT(curr_min == k); for (unsigned i = 0; i < args.size(); ++i) { bool_var bv = args[i].first; int inc = args[i].second; - if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { - literal_vector lits_save(lits); // add_clause has a side-effect on literals. - lits_save.push_back(literal(bv, inc > 0)); // avoid incrementing min. - add_clause(c, lits_save); + if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc > 0)); } } } } - else if (max == k + 1 && aval == l_false) { + else if (max - get_max_delta(c) <= k && k < max && aval == l_false) { literal_vector& lits = get_lits(); lits.push_back(literal(abv)); int curr_max = accumulate_max(lits, c); if (curr_max <= k) { add_clause(c, lits); } - else if (curr_max == k + 1) { + else { for (unsigned i = 0; i < args.size(); ++i) { bool_var bv = args[i].first; int inc = args[i].second; - if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { - literal_vector lits_save(lits); // add_clause has a side-effect on literals. - lits_save.push_back(literal(bv, inc < 0)); // avoid decrementing max. - add_clause(c, lits_save); + if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc < 0)); } } } } +#if 0 + else if (aval == l_true) { + SASSERT(min < k); + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + bool all_inc = curr_min == k; + unsigned num_incs = 0; + for (unsigned i = 0; all_inc && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + all_inc = inc + min > k; + num_incs++; + } + } + if (num_incs > 0) { + std::cout << "missed T propgations " << num_incs << "\n"; + } + } + else if (aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + bool all_dec = curr_max > k; + unsigned num_decs = 0; + for (unsigned i = 0; all_dec && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + all_dec = inc + max <= k; + num_decs++; + } + } + if (num_decs > 0) { + std::cout << "missed F propgations " << num_decs << "\n"; + } + } +#endif } void theory_card::assign_eh(bool_var v, bool is_true) { @@ -608,10 +661,14 @@ namespace smt { } bool theory_card::should_compile(card& c) { +#if 1 + return false; +#else if (!m_util.is_at_most_k(c.m_app)) { return false; } return c.m_num_propagations >= c.m_compilation_threshold; +#endif } void theory_card::compile_at_most(card& c) { @@ -686,6 +743,19 @@ namespace smt { return m_literals; } + void theory_card::add_assign(card& c, literal_vector const& lits, literal l) { + literal_vector ls; + ++c.m_num_propagations; + m_stats.m_num_propagations++; + context& ctx = get_context(); + for (unsigned i = 0; i < lits.size(); ++i) { + ls.push_back(~lits[i]); + } + ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l))); + } + + + void theory_card::add_clause(card& c, literal_vector const& lits) { ++c.m_num_propagations; m_stats.m_num_axioms++; @@ -693,7 +763,8 @@ namespace smt { TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); - IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr()); + IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), + lits.size(), lits.c_ptr()); verbose_stream() << "\n";); // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } diff --git a/src/smt/theory_card.h b/src/smt/theory_card.h index e8eae9232..a432ea5a3 100644 --- a/src/smt/theory_card.h +++ b/src/smt/theory_card.h @@ -32,6 +32,7 @@ namespace smt { struct stats { unsigned m_num_axioms; + unsigned m_num_propagations; unsigned m_num_predicates; unsigned m_num_compiles; void reset() { memset(this, 0, sizeof(*this)); } @@ -75,10 +76,12 @@ namespace smt { void add_card(card* c); void add_clause(card& c, literal_vector const& lits); + void add_assign(card& c, literal_vector const& lits, literal l); literal_vector& get_lits(); int find_inc(bool_var bv, svector >const& vars); void propagate_assignment(card& c); + int get_max_delta(card& c); int accumulate_max(literal_vector& lits, card& c); int accumulate_min(literal_vector& lits, card& c); lbool dec_max(int inc, lbool val); diff --git a/src/util/region.h b/src/util/region.h index 7f6bc787e..5be2ae4d3 100644 --- a/src/util/region.h +++ b/src/util/region.h @@ -53,6 +53,7 @@ public: m_scopes.push_back(m_chuncks.size()); } + void pop_scope() { unsigned old_size = m_scopes.back(); m_scopes.pop_back();