mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Renamed the default tactics form QF_FPA and QF_FPABV to QF_FP and QF_FPBV, in anticipation of the logic name QF_FPA to mean floats+arrays.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
01d78b7274
commit
208994e2dc
|
@ -24,7 +24,7 @@ Notes:
|
|||
|
||||
#include"qffpa_tactic.h"
|
||||
|
||||
tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref sat_simp_p = p;
|
||||
sat_simp_p .set_bool("elim_and", true);
|
||||
|
||||
|
@ -37,40 +37,14 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
|
|||
mk_fail_if_undecided_tactic());
|
||||
}
|
||||
|
||||
struct is_non_qffpa_predicate {
|
||||
struct found {};
|
||||
ast_manager & m;
|
||||
float_util u;
|
||||
|
||||
is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
void operator()(quantifier *) { throw found(); }
|
||||
|
||||
void operator()(app * n) {
|
||||
sort * s = get_sort(n);
|
||||
if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s))
|
||||
throw found();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == u.get_family_id())
|
||||
return;
|
||||
if (is_uninterp_const(n))
|
||||
return;
|
||||
|
||||
throw found();
|
||||
}
|
||||
};
|
||||
|
||||
struct is_non_qffpabv_predicate {
|
||||
struct is_non_qffp_predicate {
|
||||
struct found {};
|
||||
ast_manager & m;
|
||||
bv_util bu;
|
||||
float_util fu;
|
||||
arith_util au;
|
||||
|
||||
is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {}
|
||||
is_non_qffp_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
|
@ -78,7 +52,7 @@ struct is_non_qffpabv_predicate {
|
|||
|
||||
void operator()(app * n) {
|
||||
sort * s = get_sort(n);
|
||||
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s))
|
||||
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
|
||||
throw found();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
|
@ -92,25 +66,14 @@ struct is_non_qffpabv_predicate {
|
|||
}
|
||||
};
|
||||
|
||||
class is_qffpa_probe : public probe {
|
||||
class is_qffp_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
return !test<is_non_qffpa_predicate>(g);
|
||||
}
|
||||
};
|
||||
|
||||
class is_qffpabv_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
return !test<is_non_qffpabv_predicate>(g);
|
||||
return !test<is_non_qffp_predicate>(g);
|
||||
}
|
||||
};
|
||||
|
||||
probe * mk_is_qffpa_probe() {
|
||||
return alloc(is_qffpa_probe);
|
||||
}
|
||||
|
||||
probe * mk_is_qffpabv_probe() {
|
||||
return alloc(is_qffpabv_probe);
|
||||
return alloc(is_qffp_probe);
|
||||
}
|
||||
|
|
@ -24,17 +24,17 @@ Notes:
|
|||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("qffpa", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffpa_tactic(m, p)")
|
||||
ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)")
|
||||
ADD_TACTIC("qffp", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffp_tactic(m, p)")
|
||||
ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffp_tactic(m, p)")
|
||||
*/
|
||||
|
||||
probe * mk_is_qffpa_probe();
|
||||
probe * mk_is_qffpabv_probe();
|
||||
probe * mk_is_qffp_probe();
|
||||
probe * mk_is_qffpbv_probe();
|
||||
/*
|
||||
ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()")
|
||||
ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()")
|
||||
ADD_PROBE("is-qffp", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffp_probe()")
|
||||
ADD_PROBE("is-qffpbv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffp_probe()")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
@ -38,7 +38,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
|||
cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
|
||||
cond(mk_is_nra_probe(), mk_nra_tactic(m),
|
||||
cond(mk_is_lira_probe(), mk_lira_tactic(m, p),
|
||||
cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p),
|
||||
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
|
||||
mk_smt_tactic()))))))))),
|
||||
p);
|
||||
return st;
|
||||
|
|
|
@ -78,10 +78,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
|
|||
return mk_ufbv_tactic(m, p);
|
||||
else if (logic=="BV")
|
||||
return mk_ufbv_tactic(m, p);
|
||||
else if (logic=="QF_FPA")
|
||||
return mk_qffpa_tactic(m, p);
|
||||
else if (logic=="QF_FPABV")
|
||||
return mk_qffpa_tactic(m, p);
|
||||
else if (logic=="QF_FP" || logic=="QF_FPBV")
|
||||
return mk_qffp_tactic(m, p);
|
||||
else if (logic=="HORN")
|
||||
return mk_horn_tactic(m, p);
|
||||
else
|
||||
|
|
Loading…
Reference in a new issue