mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 13:29:11 +00:00
fix param evaluation non-determinism
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
d628027884
commit
cb7c06ddd6
3 changed files with 147 additions and 80 deletions
|
|
@ -55,18 +55,28 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
|
|||
pull_ite_p.set_bool("local_ctx", true);
|
||||
pull_ite_p.set_uint("local_ctx_limit", 10000000);
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m),
|
||||
mk_fix_dl_var_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m)
|
||||
),
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
and_then(mk_solve_eqs_tactic(m),
|
||||
using_params(mk_simplify_tactic(m), lhs_p),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_normalize_bounds_tactic(m),
|
||||
mk_solve_eqs_tactic(m)));
|
||||
tactic* simplify1 = mk_simplify_tactic(m);
|
||||
tactic* fix_dl = mk_fix_dl_var_tactic(m);
|
||||
tactic* propagate1 = mk_propagate_values_tactic(m);
|
||||
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
|
||||
tactic* phase1 = and_then(simplify1,
|
||||
fix_dl,
|
||||
propagate1,
|
||||
elim_unc);
|
||||
|
||||
tactic* solve_eqs1 = mk_solve_eqs_tactic(m);
|
||||
tactic* simplify2 = mk_simplify_tactic(m);
|
||||
tactic* simplify_with_lhs = using_params(simplify2, lhs_p);
|
||||
tactic* propagate2 = mk_propagate_values_tactic(m);
|
||||
tactic* normalize_bounds = mk_normalize_bounds_tactic(m);
|
||||
tactic* solve_eqs2 = mk_solve_eqs_tactic(m);
|
||||
tactic* phase2 = and_then(solve_eqs1,
|
||||
simplify_with_lhs,
|
||||
propagate2,
|
||||
normalize_bounds,
|
||||
solve_eqs2);
|
||||
|
||||
tactic * preamble_st = and_then(phase1, phase2);
|
||||
|
||||
|
||||
|
||||
|
|
@ -78,15 +88,21 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
|
|||
// dynamic psm seems to work well.
|
||||
bv_solver_p.set_sym("gc", symbol("dyn_psm"));
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
mk_bit_blaster_tactic(m),
|
||||
mk_aig_tactic(),
|
||||
mk_sat_tactic(m)),
|
||||
bv_solver_p);
|
||||
tactic* simplify3 = mk_simplify_tactic(m);
|
||||
tactic* propagate3 = mk_propagate_values_tactic(m);
|
||||
tactic* solve_eqs3 = mk_solve_eqs_tactic(m);
|
||||
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
|
||||
tactic* bit_blaster = mk_bit_blaster_tactic(m);
|
||||
tactic* aig = mk_aig_tactic();
|
||||
tactic* sat = mk_sat_tactic(m);
|
||||
tactic* bv_solver_core = and_then(simplify3,
|
||||
propagate3,
|
||||
solve_eqs3,
|
||||
max_sharing,
|
||||
bit_blaster,
|
||||
aig,
|
||||
sat);
|
||||
tactic * bv_solver = using_params(bv_solver_core, bv_solver_p);
|
||||
|
||||
tactic * try2bv =
|
||||
and_then(using_params(mk_lia2pb_tactic(m), lia2pb_p),
|
||||
|
|
@ -98,19 +114,27 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
|
|||
params_ref diff_neq_p;
|
||||
diff_neq_p.set_uint("diff_neq_max_k", 25);
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
tactic * st = cond(mk_and(mk_lt(mk_num_consts_probe(), mk_const_probe(static_cast<double>(BIG_PROBLEM))),
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
mk_and(mk_not(mk_produce_proofs_probe()),
|
||||
mk_not(mk_produce_unsat_cores_probe()))),
|
||||
using_params(and_then(preamble_st,
|
||||
or_else(using_params(mk_diff_neq_tactic(m), diff_neq_p),
|
||||
try2bv,
|
||||
mk_smt_tactic(m))),
|
||||
main_p),
|
||||
mk_smt_tactic(m));
|
||||
probe* num_consts = mk_num_consts_probe();
|
||||
probe* const_limit = mk_const_probe(static_cast<double>(BIG_PROBLEM));
|
||||
probe* few_consts = mk_lt(num_consts, const_limit);
|
||||
probe* produce_proofs = mk_produce_proofs_probe();
|
||||
probe* produce_unsat = mk_produce_unsat_cores_probe();
|
||||
probe* no_proofs = mk_not(produce_proofs);
|
||||
probe* no_unsat = mk_not(produce_unsat);
|
||||
probe* no_proofs_or_unsat = mk_and(no_proofs, no_unsat);
|
||||
probe* small_problem = mk_and(few_consts, no_proofs_or_unsat);
|
||||
|
||||
tactic* diff_neq = mk_diff_neq_tactic(m);
|
||||
tactic* diff_neq_with_params = using_params(diff_neq, diff_neq_p);
|
||||
tactic* smt_default = mk_smt_tactic(m);
|
||||
tactic* branch_solver = or_else(diff_neq_with_params,
|
||||
try2bv,
|
||||
smt_default);
|
||||
tactic* main_branch = using_params(and_then(preamble_st, branch_solver), main_p);
|
||||
|
||||
tactic * st = cond(small_problem,
|
||||
main_branch,
|
||||
smt_default);
|
||||
|
||||
st->updt_params(p);
|
||||
|
||||
|
|
|
|||
|
|
@ -39,8 +39,11 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) {
|
|||
params_ref p_sc = p;
|
||||
p_sc.set_bool("simple_check", true);
|
||||
// p_sc.set_uint("seed", 997);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 10 * 1000));
|
||||
tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
tactic* seq = and_then(nlsat, fail_if_undecided);
|
||||
tactic* limited = try_for(seq, 10 * 1000);
|
||||
ts.push_back(limited);
|
||||
}
|
||||
{
|
||||
params_ref p_heuristic = p;
|
||||
|
|
@ -74,7 +77,11 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_l = p;
|
||||
p_l.set_bool("arith.greatest_error_pivot", true);
|
||||
ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 300 * 1000), mk_fail_if_undecided_tactic()));
|
||||
tactic* smt = mk_smt_tactic(m);
|
||||
tactic* smt_with_params = using_params(smt, p_l);
|
||||
tactic* smt_limited = try_for(smt_with_params, 300 * 1000);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
ts.push_back(and_then(smt_limited, fail_if_undecided));
|
||||
}
|
||||
for (unsigned i = 0; i < 200; ++i) { // 3s * 200 = 600s
|
||||
params_ref p_i = p;
|
||||
|
|
@ -96,8 +103,11 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) {
|
|||
params_ref p_sc = p;
|
||||
p_sc.set_bool("simple_check", true);
|
||||
// p_sc.set_uint("seed", 997);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 20 * 1000));
|
||||
tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
tactic* seq = and_then(nlsat, fail_if_undecided);
|
||||
tactic* limited = try_for(seq, 20 * 1000);
|
||||
ts.push_back(limited);
|
||||
}
|
||||
{
|
||||
params_ref p_heuristic = p;
|
||||
|
|
@ -133,7 +143,11 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_l = p;
|
||||
p_l.set_bool("arith.greatest_error_pivot", true);
|
||||
ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 350 * 1000), mk_fail_if_undecided_tactic()));
|
||||
tactic* smt = mk_smt_tactic(m);
|
||||
tactic* smt_with_params = using_params(smt, p_l);
|
||||
tactic* smt_limited = try_for(smt_with_params, 350 * 1000);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
ts.push_back(and_then(smt_limited, fail_if_undecided));
|
||||
}
|
||||
for (unsigned i = 0; i < 100; ++i) { // 5s * 100 = 500s
|
||||
params_ref p_i = p;
|
||||
|
|
@ -154,8 +168,11 @@ tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_sc = p;
|
||||
p_sc.set_bool("simple_check", true);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 30 * 1000));
|
||||
tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
tactic* seq = and_then(nlsat, fail_if_undecided);
|
||||
tactic* limited = try_for(seq, 30 * 1000);
|
||||
ts.push_back(limited);
|
||||
}
|
||||
{
|
||||
params_ref p_heuristic = p;
|
||||
|
|
@ -192,7 +209,11 @@ tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_l = p;
|
||||
p_l.set_bool("arith.greatest_error_pivot", true);
|
||||
ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 375 * 1000), mk_fail_if_undecided_tactic()));
|
||||
tactic* smt = mk_smt_tactic(m);
|
||||
tactic* smt_with_params = using_params(smt, p_l);
|
||||
tactic* smt_limited = try_for(smt_with_params, 375 * 1000);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
ts.push_back(and_then(smt_limited, fail_if_undecided));
|
||||
}
|
||||
for (unsigned i = 0; i < 40; ++i) { // 10s * 40 = 400s
|
||||
params_ref p_i = p;
|
||||
|
|
@ -213,8 +234,11 @@ tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_sc = p;
|
||||
p_sc.set_bool("simple_check", true);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 50 * 1000));
|
||||
tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
tactic* seq = and_then(nlsat, fail_if_undecided);
|
||||
tactic* limited = try_for(seq, 50 * 1000);
|
||||
ts.push_back(limited);
|
||||
}
|
||||
{
|
||||
|
||||
|
|
@ -247,7 +271,11 @@ tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_l = p;
|
||||
p_l.set_bool("arith.greatest_error_pivot", true);
|
||||
ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 400 * 1000), mk_fail_if_undecided_tactic()));
|
||||
tactic* smt = mk_smt_tactic(m);
|
||||
tactic* smt_with_params = using_params(smt, p_l);
|
||||
tactic* smt_limited = try_for(smt_with_params, 400 * 1000);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
ts.push_back(and_then(smt_limited, fail_if_undecided));
|
||||
}
|
||||
for (unsigned i = 0; i < 10; ++i) { // 20s * 10 = 200s
|
||||
params_ref p_i = p;
|
||||
|
|
@ -268,8 +296,11 @@ tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_sc = p;
|
||||
p_sc.set_bool("simple_check", true);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 100 * 1000));
|
||||
tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
tactic* seq = and_then(nlsat, fail_if_undecided);
|
||||
tactic* limited = try_for(seq, 100 * 1000);
|
||||
ts.push_back(limited);
|
||||
}
|
||||
{
|
||||
params_ref p_order_1 = p;
|
||||
|
|
@ -292,7 +323,11 @@ tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) {
|
|||
{
|
||||
params_ref p_l = p;
|
||||
p_l.set_bool("arith.greatest_error_pivot", true);
|
||||
ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 425 * 1000), mk_fail_if_undecided_tactic()));
|
||||
tactic* smt = mk_smt_tactic(m);
|
||||
tactic* smt_with_params = using_params(smt, p_l);
|
||||
tactic* smt_limited = try_for(smt_with_params, 425 * 1000);
|
||||
tactic* fail_if_undecided = mk_fail_if_undecided_tactic();
|
||||
ts.push_back(and_then(smt_limited, fail_if_undecided));
|
||||
}
|
||||
{
|
||||
ts.push_back(mk_qfnra_nlsat_tactic(m, p));
|
||||
|
|
@ -307,33 +342,34 @@ const double LARGE_THRESHOLD = 600.0;
|
|||
tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) {
|
||||
auto very_small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_small_solver(m, p); });
|
||||
auto small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_small_solver(m, p); });
|
||||
auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); });
|
||||
auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); });
|
||||
auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); });
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)),
|
||||
very_small_t,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)),
|
||||
small_t,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)),
|
||||
middle_t,
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)),
|
||||
large_t,
|
||||
very_large_t
|
||||
)
|
||||
)
|
||||
)
|
||||
);
|
||||
auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); });
|
||||
auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); });
|
||||
auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); });
|
||||
probe* memory_usage = mk_memory_probe();
|
||||
probe* very_small_limit = mk_const_probe(VERY_SMALL_THRESHOLD);
|
||||
probe* small_limit = mk_const_probe(SMALL_THRESHOLD);
|
||||
probe* middle_limit = mk_const_probe(MIDDLE_THRESHOLD);
|
||||
probe* large_limit = mk_const_probe(LARGE_THRESHOLD);
|
||||
|
||||
probe* very_small_check = mk_lt(memory_usage, very_small_limit);
|
||||
probe* small_check = mk_lt(memory_usage, small_limit);
|
||||
probe* middle_check = mk_lt(memory_usage, middle_limit);
|
||||
probe* large_check = mk_lt(memory_usage, large_limit);
|
||||
|
||||
tactic* large_branch = cond(large_check, large_t, very_large_t);
|
||||
tactic* middle_branch = cond(middle_check, middle_t, large_branch);
|
||||
tactic* small_branch = cond(small_check, small_t, middle_branch);
|
||||
return cond(very_small_check, very_small_t, small_branch);
|
||||
}
|
||||
|
||||
tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
|
||||
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(mk_simplify_tactic(m, p),
|
||||
mk_propagate_values_tactic(m, p),
|
||||
mk_qfnra_mixed_solver(m, p)
|
||||
tactic* simplify = mk_simplify_tactic(m, p);
|
||||
tactic* propagate = mk_propagate_values_tactic(m, p);
|
||||
tactic* mixed_solver = mk_qfnra_mixed_solver(m, p);
|
||||
|
||||
return and_then(simplify,
|
||||
propagate,
|
||||
mixed_solver
|
||||
);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,13 +29,20 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
|
|||
s2_p.set_bool("pull_cheap_ite", true);
|
||||
s2_p.set_bool("local_ctx", true);
|
||||
s2_p.set_uint("local_ctx_limit", 10000000);
|
||||
// TODO: non-deterministic parameter evaluation
|
||||
return and_then(mk_simplify_tactic(m, p),
|
||||
mk_propagate_values_tactic(m, p),
|
||||
mk_solve_eqs_tactic(m, p),
|
||||
using_params(mk_simplify_tactic(m, p), s2_p),
|
||||
if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))),
|
||||
mk_smt_tactic(m, p));
|
||||
tactic* simplify = mk_simplify_tactic(m, p);
|
||||
tactic* propagate = mk_propagate_values_tactic(m, p);
|
||||
tactic* solve_eqs = mk_solve_eqs_tactic(m, p);
|
||||
tactic* simplify2 = mk_simplify_tactic(m, p);
|
||||
tactic* simplify_with_pull = using_params(simplify2, s2_p);
|
||||
tactic* symmetry = mk_symmetry_reduce_tactic(m, p);
|
||||
tactic* guarded_symmetry = if_no_proofs(if_no_unsat_cores(symmetry));
|
||||
tactic* smt = mk_smt_tactic(m, p);
|
||||
return and_then(simplify,
|
||||
propagate,
|
||||
solve_eqs,
|
||||
simplify_with_pull,
|
||||
guarded_symmetry,
|
||||
smt);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue