mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

qffp tactic cleaned up to be in line with the default behavior of other tactics.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-30 15:23:46 +01:00
parent cb2bf48254
commit 1724811e1b
1 changed files with 26 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/tactic/fpa/qffp_tactic.cpp
View file

@ -30,38 +30,50 @@ Notes:
#include"qffp_tactic.h" #include"qffp_tactic.h"
struct has_fp_to_real_predicate { struct is_non_fp_qfnra_predicate {
struct found {}; struct found {};
ast_manager & m; ast_manager & m;
bv_util bu; bv_util bu;
fpa_util fu; fpa_util fu;
arith_util au; arith_util au;
has_fp_to_real_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} is_non_fp_qfnra_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
void operator()(var *) { throw found(); } void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); } void operator()(quantifier *) { throw found(); }
void operator()(app * n) { void operator()(app * n) {
family_id fid = n->get_family_id();
if (fid != null_family_id && fid != fu.get_family_id())
throw found();
sort * s = get_sort(n); sort * s = get_sort(n);
if (au.is_real(s) && n->get_family_id() == fu.get_family_id() && if (fid == fu.get_family_id()) {
is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL) if (!fu.is_float(s) && !fu.is_rm(s) &&
to_app(n)->get_decl_kind() != OP_FPA_TO_REAL)
throw found();
}
else if (fid == null_family_id) {
if (!fu.is_float(s) && !fu.is_rm(s) && !m.is_bool(s))
throw found();
}
else if (fid == m.get_basic_family_id())
return;
else
throw found(); throw found();
} }
}; };
class has_fp_to_real_probe : public probe { class is_fp_qfnra_probe : public probe {
public: public:
virtual result operator()(goal const & g) { virtual result operator()(goal const & g) {
return test<has_fp_to_real_predicate>(g); return !test<is_non_fp_qfnra_predicate>(g);
} }
virtual ~is_fp_qfnra_probe() {}
virtual ~has_fp_to_real_probe() {}
}; };
probe * mk_has_fp_to_real_probe() { probe * mk_is_fp_qfnra_probe() {
return alloc(has_fp_to_real_probe); return alloc(is_fp_qfnra_probe);
} }
@ -82,12 +94,11 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m, p), simp_p), using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(), cond(mk_is_propositional_probe(),
cond(mk_produce_proofs_probe(), cond(mk_produce_proofs_probe(),
mk_smt_tactic(), // `sat' does not support proofs. mk_smt_tactic(p), // `sat' does not support proofs.
mk_sat_tactic(m, p)), mk_sat_tactic(m, p)),
cond(mk_has_fp_to_real_probe(), cond(mk_is_fp_qfnra_probe(),
mk_qfnra_tactic(m, p), mk_qfnra_tactic(m, p),
mk_smt_tactic(p))), mk_smt_tactic(p))));
mk_fail_if_undecided_tactic());
st->updt_params(p); st->updt_params(p);
return st; return st;