mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge pull request #503 from martin-neuhaeusser/ufbv_and_ack

Browse source 
Fix bug in ufbv tactic that enabled ackermannization even if unsat co…
This commit is contained in:
Christoph M. Wintersteiger 2016-03-09 13:29:13 +00:00
commit 7413b3278f
1 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -35,9 +35,9 @@ Notes:
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);
// 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);
@ -61,13 +61,13 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
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.
// 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),
mk_ackermannize_bv_tactic(m,p)
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
);
}
@ -80,14 +80,14 @@ static tactic * main_p(tactic* t) {
}
tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
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);
params_ref solver_p;
solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
params_ref no_flat_p;
no_flat_p.set_bool("flat", false);
@ -98,7 +98,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
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
@ -119,10 +119,10 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
big_aig_p))))),
sat),
smt))));
st->updt_params(p);
return st;
}
@ -131,9 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
mk_sat_tactic(m));
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
}