mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
working on incremental sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
03979fd580
commit
6821d61ac4
4 changed files with 221 additions and 80 deletions
|
|
@ -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";
|
||||
|
|
|
|||
|
|
@ -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<expr> & 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<symbol> & 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));
|
||||
|
|
|
|||
|
|
@ -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())));
|
||||
*/
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue