mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Added is_qfaufbv_probe and is_qfauflia_probe.
Potential performance disruption for some users: Changed default_tactic to call the respective tactics, where previously they would have run the default 'smt' tactic. Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
a8d8e3e9e5
commit
d20c7bc9ee
|
@ -198,11 +198,75 @@ struct is_non_qflira_functor {
|
|||
}
|
||||
};
|
||||
|
||||
struct is_non_qfauflira_functor {
|
||||
struct found {};
|
||||
ast_manager & m;
|
||||
arith_util m_arith_util;
|
||||
array_util m_array_util;
|
||||
bool m_int;
|
||||
bool m_real;
|
||||
|
||||
is_non_qfauflira_functor(ast_manager & _m, bool _int, bool _real) :
|
||||
m(_m), m_arith_util(_m), m_array_util(_m), m_int(_int), m_real(_real) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
void operator()(quantifier *) { throw found(); }
|
||||
|
||||
bool compatible_sort(app * n) const {
|
||||
if (m.is_bool(n))
|
||||
return true;
|
||||
if (m_int && m_arith_util.is_int(n))
|
||||
return true;
|
||||
if (m_real && m_arith_util.is_real(n))
|
||||
return true;
|
||||
if (m_array_util.is_array(n))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
void operator()(app * n) {
|
||||
if (!compatible_sort(n))
|
||||
throw found();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == m_arith_util.get_family_id()) {
|
||||
switch (n->get_decl_kind()) {
|
||||
case OP_LE: case OP_GE: case OP_LT: case OP_GT:
|
||||
case OP_ADD: case OP_NUM:
|
||||
return;
|
||||
case OP_MUL:
|
||||
if (n->get_num_args() != 2)
|
||||
throw found();
|
||||
if (!m_arith_util.is_numeral(n->get_arg(0)))
|
||||
throw found();
|
||||
return;
|
||||
case OP_TO_REAL:
|
||||
if (!m_real)
|
||||
throw found();
|
||||
break;
|
||||
default:
|
||||
throw found();
|
||||
}
|
||||
return;
|
||||
}
|
||||
if (is_uninterp(n))
|
||||
return;
|
||||
throw found();
|
||||
}
|
||||
};
|
||||
|
||||
static bool is_qflia(goal const & g) {
|
||||
is_non_qflira_functor p(g.m(), true, false);
|
||||
return !test(g, p);
|
||||
}
|
||||
|
||||
static bool is_qfauflia(goal const & g) {
|
||||
is_non_qfauflira_functor p(g.m(), true, false);
|
||||
return !test(g, p);
|
||||
}
|
||||
|
||||
class is_qflia_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
|
@ -210,6 +274,13 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
class is_qfauflia_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
return is_qfauflia(g);
|
||||
}
|
||||
};
|
||||
|
||||
static bool is_qflra(goal const & g) {
|
||||
is_non_qflira_functor p(g.m(), false, true);
|
||||
return !test(g, p);
|
||||
|
@ -289,6 +360,10 @@ probe * mk_is_qflia_probe() {
|
|||
return alloc(is_qflia_probe);
|
||||
}
|
||||
|
||||
probe * mk_is_qfauflia_probe() {
|
||||
return alloc(is_qfauflia_probe);
|
||||
}
|
||||
|
||||
probe * mk_is_qflra_probe() {
|
||||
return alloc(is_qflra_probe);
|
||||
}
|
||||
|
|
|
@ -33,6 +33,7 @@ probe * mk_arith_max_degree_probe();
|
|||
*/
|
||||
|
||||
probe * mk_is_qflia_probe();
|
||||
probe * mk_is_qfauflia_probe();
|
||||
probe * mk_is_qflra_probe();
|
||||
probe * mk_is_qflira_probe();
|
||||
probe * mk_is_ilp_probe();
|
||||
|
@ -40,6 +41,7 @@ probe * mk_is_mip_probe();
|
|||
|
||||
/*
|
||||
ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", "mk_is_qflia_probe()")
|
||||
ADD_PROBE("is-qfauflia", "true if the goal is in QF_AUFLIA.", "mk_is_qfauflia_probe()")
|
||||
ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", "mk_is_qflra_probe()")
|
||||
ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", "mk_is_qflira_probe()")
|
||||
ADD_PROBE("is-ilp", "true if the goal is ILP.", "mk_is_ilp_probe()")
|
||||
|
|
|
@ -28,10 +28,14 @@ Notes:
|
|||
#include"probe_arith.h"
|
||||
#include"quant_tactics.h"
|
||||
#include"qffpa_tactic.h"
|
||||
#include"qfaufbv_tactic.h"
|
||||
#include"qfauflia_tactic.h"
|
||||
|
||||
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * st = using_params(and_then(mk_simplify_tactic(m),
|
||||
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
|
||||
cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m),
|
||||
cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m),
|
||||
cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
|
||||
cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
|
||||
cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
|
||||
|
@ -39,7 +43,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
|||
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),
|
||||
mk_smt_tactic()))))))))),
|
||||
mk_smt_tactic()))))))))))),
|
||||
p);
|
||||
return st;
|
||||
}
|
||||
|
|
|
@ -316,6 +316,44 @@ probe * mk_is_qfbv_probe() {
|
|||
return alloc(is_qfbv_probe);
|
||||
}
|
||||
|
||||
struct is_non_qfaufbv_predicate {
|
||||
struct found {};
|
||||
ast_manager & m;
|
||||
bv_util m_bv_util;
|
||||
array_util m_array_util;
|
||||
|
||||
is_non_qfaufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m), m_array_util(_m) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
void operator()(quantifier *) { throw found(); }
|
||||
|
||||
void operator()(app * n) {
|
||||
if (!m.is_bool(n) && !m_bv_util.is_bv(n) && !m_array_util.is_array(n))
|
||||
throw found();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == m_bv_util.get_family_id() || fid == m_array_util.get_family_id())
|
||||
return;
|
||||
if (is_uninterp(n))
|
||||
return;
|
||||
|
||||
throw found();
|
||||
}
|
||||
};
|
||||
|
||||
class is_qfaufbv_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
return !test<is_non_qfaufbv_predicate>(g);
|
||||
}
|
||||
};
|
||||
|
||||
probe * mk_is_qfaufbv_probe() {
|
||||
return alloc(is_qfaufbv_probe);
|
||||
}
|
||||
|
||||
class num_consts_probe : public probe {
|
||||
bool m_bool; // If true, track only boolean constants. Otherwise, track only non boolean constants.
|
||||
char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.
|
||||
|
|
|
@ -111,10 +111,12 @@ probe * mk_div(probe * p1, probe * p2);
|
|||
|
||||
probe * mk_is_propositional_probe();
|
||||
probe * mk_is_qfbv_probe();
|
||||
probe * mk_is_qfaufbv_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()")
|
||||
ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", "mk_is_qfbv_probe()")
|
||||
ADD_PROBE("is-qfaufbv", "true if the goal is in QF_AUFBV.", "mk_is_qfaufbv_probe()")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue