mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
fix param evaluation non-determinism
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
fad311a70a
commit
a413783c1c
3 changed files with 144 additions and 78 deletions
|
|
@ -38,17 +38,26 @@ static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) {
|
|||
simp2_p.set_uint("local_ctx_limit", 10000000);
|
||||
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
// sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
using_params(mk_simplify_tactic(m), simp2_p),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p)))
|
||||
);
|
||||
tactic* simplify1 = mk_simplify_tactic(m);
|
||||
tactic* propagate = mk_propagate_values_tactic(m);
|
||||
tactic* solve_eqs = mk_solve_eqs_tactic(m);
|
||||
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
|
||||
tactic* size_reduction = mk_bv_size_reduction_tactic(m);
|
||||
tactic* guarded_size_reduction = if_no_proofs(if_no_unsat_cores(size_reduction));
|
||||
tactic* simplify2 = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_params = using_params(simplify2, simp2_p);
|
||||
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
|
||||
tactic* ackermann = mk_ackermannize_bv_tactic(m, p);
|
||||
tactic* guarded_ackermann = if_no_proofs(if_no_unsat_cores(ackermann));
|
||||
|
||||
return and_then(simplify1,
|
||||
propagate,
|
||||
solve_eqs,
|
||||
elim_unc,
|
||||
guarded_size_reduction,
|
||||
simplify_with_params,
|
||||
max_sharing,
|
||||
guarded_ackermann);
|
||||
}
|
||||
|
||||
tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
|
|
@ -58,10 +67,12 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
|
||||
tactic * preamble_st = mk_qfaufbv_preamble(m, p);
|
||||
|
||||
tactic * st = using_params(
|
||||
and_then(preamble_st,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m, p))), main_p);
|
||||
tactic* qfbv = mk_qfbv_tactic(m);
|
||||
tactic* smt = mk_smt_tactic(m, p);
|
||||
probe* qfbv_probe = mk_is_qfbv_probe();
|
||||
tactic* branch = cond(qfbv_probe, qfbv, smt);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st, branch), main_p);
|
||||
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
|
|
|
|||
|
|
@ -48,13 +48,21 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
|
|||
mem_p.set_uint("max_conflicts", 500);
|
||||
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
tactic * r = using_params(and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
using_params(mk_simplify_tactic(m), simp2_p),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
using_params(mk_bit_blaster_tactic(m), mem_p),
|
||||
mk_sat_tactic(m, mem_p)),
|
||||
tactic* simplify1 = mk_simplify_tactic(m);
|
||||
tactic* propagate = mk_propagate_values_tactic(m);
|
||||
tactic* simplify2 = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_params = using_params(simplify2, simp2_p);
|
||||
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
|
||||
tactic* bit_blaster = mk_bit_blaster_tactic(m);
|
||||
tactic* bit_blaster_with_params = using_params(bit_blaster, mem_p);
|
||||
tactic* sat = mk_sat_tactic(m, mem_p);
|
||||
|
||||
tactic * r = using_params(and_then(simplify1,
|
||||
propagate,
|
||||
simplify_with_params,
|
||||
max_sharing,
|
||||
bit_blaster_with_params,
|
||||
sat),
|
||||
p);
|
||||
return r;
|
||||
}
|
||||
|
|
@ -73,16 +81,26 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
|
|||
params_ref elim_p = p_ref;
|
||||
elim_p.set_uint("max_memory",20);
|
||||
|
||||
return
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
|
||||
using_params(mk_simplify_tactic(m), pull_ite_p),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
mk_lia2card_tactic(m),
|
||||
mk_card2bv_tactic(m, p_ref),
|
||||
skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)));
|
||||
tactic* simplify1 = mk_simplify_tactic(m);
|
||||
tactic* propagate = mk_propagate_values_tactic(m);
|
||||
tactic* ctx_simplify = mk_ctx_simplify_tactic(m);
|
||||
tactic* ctx_simplify_with_params = using_params(ctx_simplify, ctx_simp_p);
|
||||
tactic* simplify2 = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_pull_ite = using_params(simplify2, pull_ite_p);
|
||||
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
|
||||
tactic* lia2card = mk_lia2card_tactic(m);
|
||||
tactic* card2bv = mk_card2bv_tactic(m, p_ref);
|
||||
tactic* cofactor = mk_cofactor_term_ite_tactic(m);
|
||||
tactic* cofactor_with_params = using_params(cofactor, elim_p);
|
||||
|
||||
return and_then(simplify1,
|
||||
propagate,
|
||||
ctx_simplify_with_params,
|
||||
simplify_with_pull_ite,
|
||||
elim_unc,
|
||||
lia2card,
|
||||
card2bv,
|
||||
skip_if_failed(cofactor_with_params));
|
||||
}
|
||||
|
||||
static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
|
||||
|
|
@ -91,11 +109,17 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
|
|||
params_ref simp_p = p;
|
||||
simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(using_params(mk_simplify_tactic(m), simp_p),
|
||||
mk_nla2bv_tactic(m, nia2sat_p),
|
||||
skip_if_failed(mk_qfnia_bv_solver(m, p)),
|
||||
mk_fail_if_undecided_tactic());
|
||||
tactic* simplify = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_params = using_params(simplify, simp_p);
|
||||
tactic* nla2bv = mk_nla2bv_tactic(m, nia2sat_p);
|
||||
tactic* bv_solver = mk_qfnia_bv_solver(m, p);
|
||||
tactic* guarded_bv_solver = skip_if_failed(bv_solver);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
|
||||
return and_then(simplify_with_params,
|
||||
nla2bv,
|
||||
guarded_bv_solver,
|
||||
fail_if_undecided);
|
||||
}
|
||||
|
||||
static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
|
||||
|
|
@ -117,14 +141,20 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
|
|||
}
|
||||
|
||||
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(
|
||||
mk_report_verbose_tactic("(qfnia-tactic)", 10),
|
||||
mk_qfnia_preamble(m, p),
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
or_else(mk_qfnia_sat_solver(m, p),
|
||||
try_for(mk_qfnia_smt_solver(m, p), 2000),
|
||||
mk_qfnia_nlsat_solver(m, p),
|
||||
mk_qfnia_smt_solver(m, p)));
|
||||
}
|
||||
tactic* report = mk_report_verbose_tactic("(qfnia-tactic)", 10);
|
||||
tactic* preamble = mk_qfnia_preamble(m, p);
|
||||
|
||||
tactic* sat_solver = mk_qfnia_sat_solver(m, p);
|
||||
tactic* smt_solver1 = mk_qfnia_smt_solver(m, p);
|
||||
tactic* smt_solver_try = try_for(mk_qfnia_smt_solver(m, p), 2000);
|
||||
tactic* nlsat_solver = mk_qfnia_nlsat_solver(m, p);
|
||||
|
||||
tactic* branch = or_else(sat_solver,
|
||||
smt_solver_try,
|
||||
nlsat_solver,
|
||||
smt_solver1);
|
||||
|
||||
return and_then(report,
|
||||
preamble,
|
||||
branch);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -150,33 +150,56 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
|
|||
ctx_simp_p.set_uint("max_depth", 32);
|
||||
ctx_simp_p.set_uint("max_steps", 5000000);
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
tactic* simplify = mk_simplify_tactic(m);
|
||||
tactic* simplify_flat = using_params(simplify, flat_and_or_p);
|
||||
tactic* propagate = mk_propagate_values_tactic(m);
|
||||
tactic* propagate_flat = using_params(propagate, flat_and_or_p);
|
||||
tactic* bv_bound = mk_bv_bound_chk_tactic(m);
|
||||
tactic* guarded_bv_bound = if_no_proofs(if_no_unsat_cores(bv_bound));
|
||||
tactic* solve_eqs = mk_solve_eqs_tactic(m);
|
||||
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
|
||||
tactic* size_reduction = mk_bv_size_reduction_tactic(m);
|
||||
tactic* guarded_size = if_no_proofs(if_no_unsat_cores(size_reduction));
|
||||
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
|
||||
tactic* simplify2 = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_params = using_params(simplify2, simp2_p);
|
||||
|
||||
return and_then(
|
||||
using_params(mk_simplify_tactic(m), flat_and_or_p),
|
||||
using_params(mk_propagate_values_tactic(m), flat_and_or_p),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))),
|
||||
//using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
using_params(mk_simplify_tactic(m), simp2_p)
|
||||
);
|
||||
simplify_flat,
|
||||
propagate_flat,
|
||||
guarded_bv_bound,
|
||||
solve_eqs,
|
||||
elim_unc,
|
||||
guarded_size,
|
||||
max_sharing,
|
||||
simplify_with_params);
|
||||
}
|
||||
|
||||
static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
|
||||
params_ref simp2_p = p, flat_and_or_p = p;
|
||||
flat_and_or_p.set_bool("flat_and_or", false);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(using_params(mk_simplify_tactic(m), flat_and_or_p),
|
||||
using_params(mk_propagate_values_tactic(m), flat_and_or_p),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
|
||||
);
|
||||
tactic* simplify = mk_simplify_tactic(m);
|
||||
tactic* simplify_flat = using_params(simplify, flat_and_or_p);
|
||||
tactic* propagate = mk_propagate_values_tactic(m);
|
||||
tactic* propagate_flat = using_params(propagate, flat_and_or_p);
|
||||
tactic* solve_eqs = mk_solve_eqs_tactic(m);
|
||||
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
|
||||
tactic* reduce_args = mk_reduce_args_tactic(m);
|
||||
tactic* guarded_reduce_args = if_no_proofs(if_no_unsat_cores(reduce_args));
|
||||
tactic* size_reduction = mk_bv_size_reduction_tactic(m);
|
||||
tactic* guarded_size_reduction = if_no_proofs(if_no_unsat_cores(size_reduction));
|
||||
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
|
||||
tactic* ackermann = mk_ackermannize_bv_tactic(m,p);
|
||||
tactic* guarded_ackermann = if_no_proofs(if_no_unsat_cores(ackermann));
|
||||
|
||||
return and_then(simplify_flat,
|
||||
propagate_flat,
|
||||
solve_eqs,
|
||||
elim_unc,
|
||||
guarded_reduce_args,
|
||||
guarded_size_reduction,
|
||||
max_sharing,
|
||||
guarded_ackermann);
|
||||
}
|
||||
|
||||
tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
|
|
@ -186,13 +209,14 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
|
||||
tactic * const preamble_st = mk_qfufbv_preamble(m, p);
|
||||
|
||||
tactic * st = using_params(
|
||||
and_then(preamble_st,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_is_qfbv_probe(),
|
||||
mk_qfbv_tactic(m),
|
||||
mk_smt_tactic(m, p))),
|
||||
main_p);
|
||||
tactic* qfbv = mk_qfbv_tactic(m);
|
||||
tactic* smt = mk_smt_tactic(m, p);
|
||||
probe* qfbv_probe = mk_is_qfbv_probe();
|
||||
tactic* branch = cond(qfbv_probe,
|
||||
qfbv,
|
||||
smt);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st, branch), main_p);
|
||||
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
|
|
@ -202,7 +226,8 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * const preamble_t = mk_qfufbv_preamble1(m, p);
|
||||
|
||||
tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
|
||||
return and_then(preamble_t,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m, p)));
|
||||
tactic* smt = mk_smt_tactic(m, p);
|
||||
probe* qfufbv_probe = mk_is_qfufbv_probe();
|
||||
tactic* branch = cond(qfufbv_probe, actual_tactic, smt);
|
||||
return and_then(preamble_t, branch);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue