From 81c2560854a504481d0c6a3da836c02245b97d3e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 May 2014 15:13:26 -0700 Subject: [PATCH] experimenting with inc-sat Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 37 +++++++++++++++++++++------- src/tactic/smtlogics/qfbv_tactic.cpp | 16 ++++++------ src/tactic/smtlogics/qfbv_tactic.h | 2 ++ 3 files changed, 39 insertions(+), 16 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 484159719..18707bf67 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -27,6 +27,7 @@ Notes: #include "pb_decl_plugin.h" #include "uint_set.h" #include "pb_preprocess_tactic.h" +#include "aig_tactic.h" #include "simplify_tactic.h" #include "tactical.h" #include "tactic.h" @@ -34,6 +35,7 @@ Notes: #include "pb_sls.h" #include "qfbv_tactic.h" #include "card2bv_tactic.h" +#include "bit_blaster_tactic.h" #include "tactic2solver.h" #include "nnf_tactic.h" #include "opt_sls_solver.h" @@ -54,13 +56,19 @@ namespace opt { model_converter_ref m_mc; tactic_ref m_preprocess; statistics m_stats; + app_ref m_soft; public: - inc_sat_solver(ast_manager& m, params_ref const& p): + inc_sat_solver(ast_manager& m, params_ref const& p, expr_ref_vector const& soft): m(m), m_solver(p,0), m_params(p), - m_fmls(m), m_map(m) { + m_fmls(m), m_map(m), m_soft(m) { tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); - tactic_ref bv2sat = mk_qfbv_tactic(m, p, mk_skip_tactic(), mk_fail_tactic()); - m_preprocess = and_then(pb2bv.get(), bv2sat.get()); + tactic_ref preamble_st = mk_qfbv_preamble(m, m_params); + m_preprocess = and_then(pb2bv.get(), preamble_st.get(), mk_bit_blaster_tactic(m), mk_aig_tactic()); + + ptr_vector sorts; + sorts.resize(soft.size(), m.mk_bool_sort()); + func_decl_ref fn(m.mk_func_decl(symbol("Soft"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort()), m); + m_soft = m.mk_app(fn, soft.size(), soft.c_ptr()); } virtual ~inc_sat_solver() {} @@ -81,12 +89,15 @@ namespace opt { for (unsigned i = 0; i < m_fmls.size(); ++i) { g->assert_expr(m_fmls[i].get()); } + g->assert_expr(m_soft); + TRACE("opt", g->display(tout);); m_fmls.reset(); - try { + try { (*m_preprocess)(g, result, mc, pc, core); + TRACE("opt", result[0]->display(tout);); } - catch (tactic_exception &) { - IF_VERBOSE(0, verbose_stream() << "exception in tactic\n";); + catch (tactic_exception & ex) { + IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); m_preprocess->collect_statistics(m_stats); return l_undef; } @@ -96,7 +107,15 @@ namespace opt { IF_VERBOSE(0, verbose_stream() << "size of result is not 1, it is: " << result.size() << "\n";); return l_undef; } - m_goal2sat(*result[0], m_params, m_solver, m_map); + g = result[0]; + for (unsigned i = 0; i < g->size(); ++i) { + expr* f = g->form(i); + if (is_app_of(f, m_soft->get_decl())) { + g->update(i, m.mk_true()); + } + } + TRACE("opt", g->display(tout);); + m_goal2sat(*g, m_params, m_solver, m_map); } lbool r = m_solver.check(); @@ -312,7 +331,7 @@ namespace opt { tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); #else - solver* sat_solver = alloc(inc_sat_solver, m, m_params); + solver* sat_solver = alloc(inc_sat_solver, m, m_params, m_soft); #endif unsigned sz = s().get_num_assertions(); for (unsigned i = 0; i < sz; ++i) { diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index db1c7b762..3b5c352bb 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -31,7 +31,7 @@ Notes: #define MEMLIMIT 300 -static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { +tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { params_ref solve_eq_p; // conservative guassian elimination. @@ -53,16 +53,18 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { return and_then( - and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - using_params(mk_solve_eqs_tactic(m), solve_eq_p), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - using_params(mk_simplify_tactic(m), simp2_p)), + mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + using_params(mk_solve_eqs_tactic(m), solve_eq_p), + mk_elim_uncnstr_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), + using_params(mk_simplify_tactic(m), simp2_p), + // // Z3 can solve a couple of extra benchmarks by using hoist_mul // but the timeout in SMT-COMP is too small. // Moreover, it impacted negatively some easy benchmarks. // We should decide later, if we keep it or not. + // using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m)); } diff --git a/src/tactic/smtlogics/qfbv_tactic.h b/src/tactic/smtlogics/qfbv_tactic.h index c20a4443a..98b3e2289 100644 --- a/src/tactic/smtlogics/qfbv_tactic.h +++ b/src/tactic/smtlogics/qfbv_tactic.h @@ -29,6 +29,8 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p = params_ref()); ADD_TACTIC("qfbv", "builtin strategy for solving QF_BV problems.", "mk_qfbv_tactic(m, p)") */ +tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p); + tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p, tactic* sat, tactic* smt); #endif