From 34af1988166d012ad9a03c7274489d9bbec9886c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2013 08:51:01 -0800 Subject: [PATCH 1/4] missing file Signed-off-by: Nikolaj Bjorner --- src/api/api_pb.cpp | 57 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 src/api/api_pb.cpp diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp new file mode 100644 index 000000000..52290d28a --- /dev/null +++ b/src/api/api_pb.cpp @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + api_pb.cpp + +Abstract: + API for pb theory + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-13. + +Revision History: + +--*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" +#include"api_util.h" +#include"card_decl_plugin.h" + +extern "C" { + + Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, + Z3_ast const args[], unsigned k) { + Z3_TRY; + LOG_Z3_mk_atmost(c, num_args, args, k); + RESET_ERROR_CODE(); + parameter param(k); + card_util util(mk_c(c)->m()); + ast* a = util.mk_at_most_k(num_args, to_exprs(args), k); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + + Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, + Z3_ast const args[], int coeffs[], + int k) { + Z3_TRY; + LOG_Z3_mk_pble(c, num_args, args, coeffs, k); + RESET_ERROR_CODE(); + card_util util(mk_c(c)->m()); + ast* a = util.mk_le(num_args, coeffs, to_exprs(args), k); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + +}; From d729e89a7b3d05359ba391f978cb3861c9d382a4 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Thu, 14 Nov 2013 12:36:39 -0800 Subject: [PATCH 2/4] Fix a minor bug on cardinality solver --- src/opt/opt_solver.cpp | 16 ++++++++-------- src/opt/opt_solver.h | 4 ++-- src/smt/theory_card.cpp | 5 +++-- 3 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 02b01912e..fee4a8663 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -109,9 +109,11 @@ namespace opt { lbool r = m_context.check(num_assumptions, assumptions); if (m_is_dump) { - std::stringstream buffer; - buffer << "opt_solver" << ++g_checksat_count << ".smt2"; - to_smt2_benchmark(buffer.str().c_str(), "benchmark", "QF_BV"); + std::stringstream file_name; + file_name << "opt_solver" << ++g_checksat_count << ".smt2"; + std::ofstream buffer(file_name.str().c_str()); + to_smt2_benchmark(buffer, "opt_solver", "QF_BV"); + buffer.close(); } if (r == l_true && m_objective_enabled) { m_objective_values.reset(); @@ -212,9 +214,8 @@ namespace opt { return dynamic_cast(s); } - void opt_solver::to_smt2_benchmark(char const * file_name, char const * name, char const * logic, - char const * status, char const * attributes) { - std::ofstream buffer(file_name); + void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, + char const * status, char const * attributes) { ast_smt_pp pp(m); pp.set_benchmark_name(name); pp.set_logic(logic); @@ -225,8 +226,7 @@ namespace opt { for (unsigned i = 0; i < get_num_assertions(); ++i) { pp.add_assumption(to_expr(get_assertion(i))); } - pp.display_smt2(buffer, to_expr(m.mk_true())); - buffer.close(); + pp.display_smt2(buffer, to_expr(m.mk_true())); } opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 90ebe3251..de7ef0b1d 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -90,8 +90,8 @@ namespace opt { smt::theory_opt& get_optimizer(); - void to_smt2_benchmark(char const * file_name, char const * name = "benchmarks", - char const * logic = "", char const * status = "unknown", char const * attributes = ""); + void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks", + char const * logic = "", char const * status = "unknown", char const * attributes = ""); }; } diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index c32b600c1..3aa72baef 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -133,9 +133,10 @@ namespace smt { } static unsigned gcd(unsigned a, unsigned b) { - if (a == 0) return b; - if (b == 0) return a; while (a != b) { + if (a == 0) return b; + if (b == 0) return a; + SASSERT(a != 0 && b != 0); if (a < b) { b %= a; } From 06ae0db116034afbd00bf206acdf97b703d2c8ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2013 18:04:05 -0800 Subject: [PATCH 3/4] 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(); From 4be11f24e1a68e9f114c949405678712dc9e4f29 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Thu, 14 Nov 2013 19:02:15 -0800 Subject: [PATCH 4/4] Instrument fu_malik to use the new SAT solver (WIP) --- src/opt/core_maxsat.cpp | 4 +- src/opt/fu_malik.cpp | 74 +++++++++++++++++++++++----- src/tactic/smtlogics/qfbv_tactic.cpp | 14 ++++-- 3 files changed, 73 insertions(+), 19 deletions(-) diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp index b4472971e..b386595d3 100644 --- a/src/opt/core_maxsat.cpp +++ b/src/opt/core_maxsat.cpp @@ -65,7 +65,7 @@ namespace opt { for (unsigned i = 0; i < ans.size(); ++i) { tout << mk_pp(ans[i].get(), m) << "\n"; }); - IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat: " << ans.size() << "\n";); + IF_VERBOSE(0, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";); if (ans.size() > m_answer.size()) { m_answer.reset(); m_answer.append(ans); @@ -92,7 +92,7 @@ namespace opt { core_vars.insert(get_not(core[i])); block_vars.remove(core[i]); } - IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";); + IF_VERBOSE(0, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";); if (core.empty()) { m_upper = m_answer.size(); return l_true; diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 6ba3bba39..42f410761 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -18,6 +18,11 @@ Notes: --*/ #include "fu_malik.h" +#include "smtlogics/qfbv_tactic.h" +#include "tactic2solver.h" +#include "goal.h" +#include "probe.h" +#include "smt_context.h" /** \brief Fu & Malik procedure for MaxSAT. This procedure is based on @@ -37,25 +42,29 @@ 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 & m_original_solver; + bool m_use_new_bv_solver; 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), - m_assignment(m) + m_assignment(m), + m_original_solver(s), + m_use_new_bv_solver(false) { m_upper_size = m_soft.size() + 1; } + solver& s() { return *m_s; } /** \brief One step of the Fu&Malik algorithm. @@ -73,18 +82,30 @@ namespace opt { */ lbool step() { - IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";); // add some count, add some information of # of soft constraints still possibly sat. + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";); expr_ref_vector assumptions(m), block_vars(m); 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); + if (m_use_new_bv_solver) { + unsigned i = 0; + while (s().check_sat(core.size(), core.c_ptr()) != l_false) { + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";); + core.push_back(assumptions[i].get()); + ++i; + } + } + else { + s().get_unsat_core(core); + } + + SASSERT(!core.empty()); // Update soft-constraints and aux_vars for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -101,9 +122,11 @@ 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())); } + SASSERT (!block_vars.empty()); assert_at_most_one(block_vars); + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";); return l_false; } @@ -111,7 +134,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 +152,40 @@ namespace opt { has_zero = m.mk_and(has_zero1, has_zero2); } } + + void set_solver() { + solver& current_solver = s(); + goal g(m, true, false); + unsigned num_assertions = current_solver.get_num_assertions(); + for (unsigned i = 0; i < num_assertions; ++i) { + g.assert_expr(current_solver.get_assertion(i)); + } + probe *p = mk_is_qfbv_probe(); + bool all_bv = (*p)(g).is_true(); + if (all_bv) { + opt_solver & os = opt_solver::to_opt(m_original_solver); + smt::context & ctx = os.get_context(); + tactic* t = mk_qfbv_tactic(m, ctx.get_params()); + // The new SAT solver hasn't supported unsat core yet + m_s = mk_tactic2solver(m, t); + SASSERT(m_s != &m_original_solver); + for (unsigned i = 0; i < num_assertions; ++i) { + m_s->assert_expr(current_solver.get_assertion(i)); + } + m_use_new_bv_solver = true; + IF_VERBOSE(0, verbose_stream() << "Force to use the new BV solver." << std::endl;); + } + } // 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 +198,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/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 51b040332..cdbc6927e 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -31,6 +31,15 @@ Notes: #define MEMLIMIT 300 +tactic * mk_new_sat_tactic(ast_manager & m) { + IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;); + tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + and_then(mk_simplify_tactic(m), + mk_smt_tactic()), + mk_sat_tactic(m)); + return new_sat; +} + tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); @@ -85,10 +94,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = and_then(mk_simplify_tactic(m), mk_smt_tactic()); #else - tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - and_then(mk_simplify_tactic(m), - mk_smt_tactic()), - mk_sat_tactic(m)); + tactic * new_sat = mk_new_sat_tactic(m); #endif tactic * st = using_params(and_then(preamble_st,