diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index fda90006c..1ad9909ad 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -802,12 +802,12 @@ namespace opt { } void context::display(std::ostream& out) { - + display_assignment(out); } void context::display_assignment(std::ostream& out) { - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; + for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { + objective const& obj = m_scoped_state.m_objectives[i]; display_objective(out, obj); if (get_lower_as_num(i) != get_upper_as_num(i)) { out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n"; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 075b89a76..7f571301d 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -37,9 +37,145 @@ Notes: #include "tactic2solver.h" #include "nnf_tactic.h" #include "opt_sls_solver.h" +#include "sat_solver.h" +#include "goal2sat.h" namespace opt { + // incremental SAT solver. + class inc_sat_solver : public solver { + ast_manager& m; + sat::solver m_solver; + goal2sat m_goal2sat; + params_ref m_params; + expr_ref_vector m_fmls; + atom2bool_var m_map; + model_ref m_model; + tactic_ref m_preprocess; + public: + inc_sat_solver(ast_manager& m, params_ref const& p): + m(m), m_solver(p,0), m_params(p), + m_fmls(m), m_map(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()); + } + + virtual ~inc_sat_solver() {} + + virtual void set_progress_callback(progress_callback * callback) { + } + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + SASSERT(num_assumptions == 0); + + goal_ref_buffer result; + model_converter_ref mc; // TODO make model convertion work between checks + proof_converter_ref pc; + expr_dependency_ref core(m); + + if (!m_fmls.empty()) { + goal_ref g = alloc(goal, m); + for (unsigned i = 0; i < m_fmls.size(); ++i) { + g->assert_expr(m_fmls[i].get()); + } + m_fmls.reset(); + try { + (*m_preprocess)(g, result, mc, pc, core); + } + catch (tactic_exception &) { + IF_VERBOSE(0, verbose_stream() << "exception in tactic\n";); + return l_undef; + } + // TODO: check that result is a singleton. + if (result.size() != 1) { + 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); + } + + lbool r = m_solver.check(); + if (r == l_true) { + model_ref md = alloc(model, m); + sat::model const & ll_m = m_solver.get_model(); + atom2bool_var::iterator it = m_map.begin(); + atom2bool_var::iterator end = m_map.end(); + for (; it != end; ++it) { + expr * n = it->m_key; + sat::bool_var v = it->m_value; + switch (sat::value_at(v, ll_m)) { + case l_true: + md->register_decl(to_app(n)->get_decl(), m.mk_true()); + break; + case l_false: + md->register_decl(to_app(n)->get_decl(), m.mk_false()); + break; + default: + break; + } + } + TRACE("sat_tactic", model_v2_pp(tout, *md);); + m_model = md; + if (mc) { + (*mc)(m_model); + } + } + m_solver.pop(m_solver.scope_lvl()); + return r; + } + virtual void set_cancel(bool f) { + m_goal2sat.set_cancel(f); + m_solver.set_cancel(f); + m_preprocess->set_cancel(f); + } + virtual void push() { + IF_VERBOSE(0, verbose_stream() << "push ignored\n";); + } + virtual void pop(unsigned n) { + IF_VERBOSE(0, verbose_stream() << "pop ignored\n";); + } + virtual unsigned get_scope_level() const { + return 0; + } + virtual void assert_expr(expr * t, expr * a) { + if (a) { + m_fmls.push_back(m.mk_implies(a, t)); + } + else { + m_fmls.push_back(t); + } + } + virtual void assert_expr(expr * t) { + m_fmls.push_back(t); + } + virtual void set_produce_models(bool f) {} + virtual void collect_param_descrs(param_descrs & r) { + goal2sat::collect_param_descrs(r); + sat::solver::collect_param_descrs(r); + } + virtual void updt_params(params_ref const & p) { + m_params = p; + } + + virtual void collect_statistics(statistics & st) const {} + virtual void get_unsat_core(ptr_vector & r) { + UNREACHABLE(); + } + virtual void get_model(model_ref & m) { + m = m_model; + } + virtual proof * get_proof() { + UNREACHABLE(); + return 0; + } + virtual std::string reason_unknown() const { + return "no reason given"; + } + virtual void get_labels(svector & r) { + UNREACHABLE(); + } + + }; // --------------------------------------------- // base class with common utilities used @@ -163,10 +299,14 @@ namespace opt { void enable_bvsat() { if (m_enable_sat && !m_sat_enabled && probe_bv()) { +#if 1 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()); solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); +#else + solver* sat_solver = alloc(inc_sat_solver, m, m_params); +#endif unsigned sz = s().get_num_assertions(); for (unsigned i = 0; i < sz; ++i) { sat_solver->assert_expr(s().get_assertion(i)); diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 38dd631cc..db1c7b762 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -31,13 +31,12 @@ Notes: #define MEMLIMIT 300 -tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - - params_ref main_p; - main_p.set_bool("elim_and", true); - main_p.set_bool("push_ite_bv", true); - main_p.set_bool("blast_distinct", true); +static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { + params_ref solve_eq_p; + // conservative guassian elimination. + solve_eq_p.set_uint("solve_eqs_max_occs", 2); + params_ref simp2_p = p; simp2_p.set_bool("som", true); simp2_p.set_bool("pull_cheap_ite", true); @@ -47,6 +46,38 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som + + params_ref hoist_p; + hoist_p.set_bool("hoist_mul", true); + hoist_p.set_bool("som", false); + + 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)), + // 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)); +} + +static tactic * main_p(tactic* t) { + params_ref p; + p.set_bool("elim_and", true); + p.set_bool("push_ite_bv", true); + p.set_bool("blast_distinct", true); + return using_params(t, p); +} + + +tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { + params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); @@ -60,88 +91,55 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { ctx_simp_p.set_uint("max_depth", 32); ctx_simp_p.set_uint("max_steps", 50000000); - params_ref hoist_p; - hoist_p.set_bool("hoist_mul", true); - hoist_p.set_bool("som", false); - - params_ref solve_eq_p; - // conservative guassian elimination. - solve_eq_p.set_uint("solve_eqs_max_occs", 2); params_ref big_aig_p; big_aig_p.set_bool("aig_per_assertion", false); + + tactic* preamble_st = mk_qfbv_preamble(m, p); + + tactic * st = main_p(and_then(preamble_st, + // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function + // symbols. In this case, we should not use + cond(mk_is_qfbv_probe(), + cond(mk_is_qfbv_eq_probe(), + and_then(mk_bv1_blaster_tactic(m), + using_params(smt, solver_p)), + and_then(mk_bit_blaster_tactic(m), + when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), + and_then(using_params(and_then(mk_simplify_tactic(m), + mk_solve_eqs_tactic(m)), + local_ctx_p), + if_no_proofs(cond(mk_produce_unsat_cores_probe(), + mk_aig_tactic(), + using_params(mk_aig_tactic(), + big_aig_p))))), + sat)), + smt))); + + st->updt_params(p); + return st; + +} + + +tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - tactic * preamble_st = 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)), - // 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)); - -#ifdef USE_OLD_SAT_SOLVER - 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()), + and_then(mk_simplify_tactic(m), mk_smt_tactic()), mk_sat_tactic(m)); -#endif - /* use full sls - tactic * st = using_params(and_then(preamble_st, + return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic()); + +} + +/* use full sls + tactic * st = main_p(and_then(preamble_st, cond(mk_is_qfbv_probe(), cond(mk_is_qfbv_eq_probe(), and_then(mk_bv1_blaster_tactic(m), using_params(mk_smt_tactic(), solver_p)), and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))), - mk_smt_tactic())), - main_p);*/ - - /* use pure dpll - tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_qfbv_probe(), - and_then(mk_bit_blaster_tactic(m), - when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), - and_then(using_params(and_then(mk_simplify_tactic(m), - mk_solve_eqs_tactic(m)), - local_ctx_p), - if_no_proofs(cond(mk_produce_unsat_cores_probe(), - mk_aig_tactic(), - using_params(mk_aig_tactic(), - big_aig_p))))), - new_sat), - mk_smt_tactic())), - main_p);*/ - - tactic * st = using_params(and_then(preamble_st, - // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function - // symbols. In this case, we should not use - cond(mk_is_qfbv_probe(), - cond(mk_is_qfbv_eq_probe(), - and_then(mk_bv1_blaster_tactic(m), - using_params(mk_smt_tactic(), solver_p)), - and_then(mk_bit_blaster_tactic(m), - when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), - and_then(using_params(and_then(mk_simplify_tactic(m), - mk_solve_eqs_tactic(m)), - local_ctx_p), - if_no_proofs(cond(mk_produce_unsat_cores_probe(), - mk_aig_tactic(), - using_params(mk_aig_tactic(), - big_aig_p))))), - new_sat)), - mk_smt_tactic())), - main_p); - - st->updt_params(p); - return st; -} + mk_smt_tactic()))); +*/ diff --git a/src/tactic/smtlogics/qfbv_tactic.h b/src/tactic/smtlogics/qfbv_tactic.h index 7210f6f25..c20a4443a 100644 --- a/src/tactic/smtlogics/qfbv_tactic.h +++ b/src/tactic/smtlogics/qfbv_tactic.h @@ -24,8 +24,11 @@ class ast_manager; class tactic; 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_tactic(ast_manager & m, params_ref const & p, tactic* sat, tactic* smt); + #endif