mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Adding parameters to Ackermannization in qfbv_tactic.

Browse source
This commit is contained in:
mikolas 2016-01-29 17:18:21 +00:00
parent 470b5c20fe
commit c9799b143d
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -30,11 +30,10 @@ Notes:
#include"sat_tactic.h" #include"sat_tactic.h"
#include"ackermannize_tactic.h" #include"ackermannize_tactic.h"
#include"ackr_bound_probe.h" #include"ackr_bound_probe.h"
#include"qfbv_tactic_params.hpp"
#define MEMLIMIT 300 #define MEMLIMIT 300
#define ACKRLIMIT 1000
tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
params_ref solve_eq_p; params_ref solve_eq_p;
@ -51,10 +50,20 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
simp2_p.set_bool("hoist_mul", false); // required by som simp2_p.set_bool("hoist_mul", false); // required by som
qfbv_tactic_params my_params(p);
params_ref hoist_p; params_ref hoist_p;
hoist_p.set_bool("hoist_mul", true); hoist_p.set_bool("hoist_mul", true);
hoist_p.set_bool("som", false); hoist_p.set_bool("som", false);
const double should_ackermannize = static_cast<double>(my_params.div0ackermann());
const double ackermannize_limit = static_cast<double>(my_params.div0_ackermann_limit());
probe * const should_ackermann_p = mk_and(
mk_const_probe(should_ackermannize),
mk_lt(mk_ackr_bound_probe(), mk_const_probe(ackermannize_limit))
);
return return
and_then( and_then(
mk_simplify_tactic(m), mk_simplify_tactic(m),
@ -71,7 +80,7 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
// //
using_params(mk_simplify_tactic(m), hoist_p), using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m), mk_max_bv_sharing_tactic(m),
when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(ACKRLIMIT))), mk_ackermannize_tactic(m,p)) when(should_ackermann_p, mk_ackermannize_tactic(m,p))
); );
} }