mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add pre-processing to default tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f411b3b201
commit
483a973b37
|
@ -48,7 +48,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
|||
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
|
||||
cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p),
|
||||
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
|
||||
mk_smt_tactic(m)))))))))))))),
|
||||
and_then(mk_preamble_tactic(m), mk_smt_tactic(m))))))))))))))),
|
||||
p);
|
||||
return st;
|
||||
}
|
||||
|
|
|
@ -177,20 +177,15 @@ static tactic * mk_bounded_tactic(ast_manager & m) {
|
|||
mk_fail_if_undecided_tactic()));
|
||||
}
|
||||
|
||||
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("som", true);
|
||||
main_p.set_bool("blast_distinct", true);
|
||||
main_p.set_uint("blast_distinct_threshold", 128);
|
||||
// main_p.set_bool("push_ite_arith", true);
|
||||
|
||||
tactic * mk_preamble_tactic(ast_manager& m) {
|
||||
|
||||
params_ref pull_ite_p;
|
||||
pull_ite_p.set_bool("pull_cheap_ite", true);
|
||||
pull_ite_p.set_bool("push_ite_arith", false);
|
||||
pull_ite_p.set_bool("local_ctx", true);
|
||||
pull_ite_p.set_uint("local_ctx_limit", 10000000);
|
||||
|
||||
|
||||
params_ref ctx_simp_p;
|
||||
ctx_simp_p.set_uint("max_depth", 30);
|
||||
ctx_simp_p.set_uint("max_steps", 5000000);
|
||||
|
@ -198,18 +193,35 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
|||
params_ref lhs_p;
|
||||
lhs_p.set_bool("arith_lhs", true);
|
||||
|
||||
tactic * preamble_st = and_then(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_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
using_params(mk_simplify_tactic(m), lhs_p)
|
||||
tactic * preamble_st = 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)
|
||||
);
|
||||
|
||||
preamble_st = and_then(preamble_st,
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
using_params(mk_simplify_tactic(m), lhs_p)
|
||||
);
|
||||
|
||||
return preamble_st;
|
||||
}
|
||||
|
||||
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("som", true);
|
||||
main_p.set_bool("blast_distinct", true);
|
||||
main_p.set_uint("blast_distinct_threshold", 128);
|
||||
// main_p.set_bool("push_ite_arith", true);
|
||||
|
||||
|
||||
|
||||
params_ref quasi_pb_p;
|
||||
quasi_pb_p.set_uint("lia2pb_max_bits", 64);
|
||||
|
||||
tactic * preamble_st = mk_preamble_tactic(m);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
or_else(mk_ilp_model_finder_tactic(m),
|
||||
|
|
|
@ -23,6 +23,8 @@ Notes:
|
|||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_preamble_tactic(ast_manager& m);
|
||||
|
||||
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("qflia", "builtin strategy for solving QF_LIA problems.", "mk_qflia_tactic(m, p)")
|
||||
|
|
Loading…
Reference in a new issue