mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Add basic_recognizers and array_recognizers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
cec328cfdc
commit
3ddb1a85f1
|
@ -542,6 +542,16 @@ bool array_decl_plugin::is_fully_interp(sort const * s) const {
|
|||
return m_manager->is_fully_interp(get_array_range(s));
|
||||
}
|
||||
|
||||
func_decl * array_recognizers::get_as_array_func_decl(app * n) const {
|
||||
SASSERT(is_as_array(n));
|
||||
return to_func_decl(n->get_decl()->get_parameter(0).get_ast());
|
||||
}
|
||||
|
||||
array_util::array_util(ast_manager& m):
|
||||
array_recognizers(m.get_family_id("array")),
|
||||
m_manager(m) {
|
||||
}
|
||||
|
||||
bool array_util::is_as_array_tree(expr * n) {
|
||||
ptr_buffer<expr, 32> todo;
|
||||
todo.push_back(n);
|
||||
|
|
|
@ -129,27 +129,34 @@ class array_decl_plugin : public decl_plugin {
|
|||
virtual bool is_fully_interp(sort const * s) const;
|
||||
};
|
||||
|
||||
class array_util {
|
||||
ast_manager & m_manager;
|
||||
family_id m_fid;
|
||||
class array_recognizers {
|
||||
protected:
|
||||
family_id m_fid;
|
||||
public:
|
||||
array_util(ast_manager& m): m_manager(m), m_fid(m.get_family_id("array")) {}
|
||||
ast_manager & get_manager() const { return m_manager; }
|
||||
array_recognizers(family_id fid):m_fid(fid) {}
|
||||
family_id get_family_id() const { return m_fid; }
|
||||
bool is_array(sort* s) const { return is_sort_of(s, m_fid, ARRAY_SORT);}
|
||||
bool is_array(expr* n) const { return is_array(m_manager.get_sort(n)); }
|
||||
bool is_array(expr* n) const { return is_array(get_sort(n)); }
|
||||
bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); }
|
||||
bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
|
||||
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
|
||||
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
|
||||
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
|
||||
bool is_as_array_tree(expr * n);
|
||||
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
|
||||
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
|
||||
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
|
||||
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
|
||||
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
|
||||
func_decl * get_as_array_func_decl(app * n) const { SASSERT(is_as_array(n)); return to_func_decl(n->get_decl()->get_parameter(0).get_ast()); }
|
||||
func_decl * get_as_array_func_decl(app * n) const;
|
||||
};
|
||||
|
||||
class array_util : public array_recognizers {
|
||||
ast_manager & m_manager;
|
||||
public:
|
||||
array_util(ast_manager& m);
|
||||
ast_manager & get_manager() const { return m_manager; }
|
||||
|
||||
bool is_as_array_tree(expr * n);
|
||||
|
||||
app * mk_store(unsigned num_args, expr * const * args) {
|
||||
return m_manager.mk_app(m_fid, OP_STORE, 0, 0, num_args, args);
|
||||
|
|
|
@ -1073,6 +1073,16 @@ expr * basic_decl_plugin::get_some_value(sort * s) {
|
|||
return 0;
|
||||
}
|
||||
|
||||
bool basic_recognizers::is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const {
|
||||
if (is_ite(n)) {
|
||||
t1 = to_app(n)->get_arg(0);
|
||||
t2 = to_app(n)->get_arg(1);
|
||||
t3 = to_app(n)->get_arg(2);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// label_decl_plugin
|
||||
|
|
|
@ -1289,6 +1289,53 @@ inline bool has_labels(expr const * n) {
|
|||
|
||||
sort * get_sort(expr const * n);
|
||||
|
||||
class basic_recognizers {
|
||||
family_id m_fid;
|
||||
public:
|
||||
basic_recognizers(family_id fid):m_fid(fid) {}
|
||||
bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); }
|
||||
bool is_bool(expr const * n) const { return is_bool(get_sort(n)); }
|
||||
bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); }
|
||||
bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); }
|
||||
bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); }
|
||||
bool is_not(expr const * n) const { return is_app_of(n, m_fid, OP_NOT); }
|
||||
bool is_eq(expr const * n) const { return is_app_of(n, m_fid, OP_EQ); }
|
||||
bool is_oeq(expr const * n) const { return is_app_of(n, m_fid, OP_OEQ); }
|
||||
bool is_distinct(expr const * n) const { return is_app_of(n, m_fid, OP_DISTINCT); }
|
||||
bool is_iff(expr const * n) const { return is_app_of(n, m_fid, OP_IFF); }
|
||||
bool is_xor(expr const * n) const { return is_app_of(n, m_fid, OP_XOR); }
|
||||
bool is_ite(expr const * n) const { return is_app_of(n, m_fid, OP_ITE); }
|
||||
bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); }
|
||||
bool is_true(expr const * n) const { return is_app_of(n, m_fid, OP_TRUE); }
|
||||
bool is_false(expr const * n) const { return is_app_of(n, m_fid, OP_FALSE); }
|
||||
bool is_complement_core(expr const * n1, expr const * n2) const {
|
||||
return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2);
|
||||
}
|
||||
bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); }
|
||||
bool is_or(func_decl const * d) const { return is_decl_of(d, m_fid, OP_OR); }
|
||||
bool is_implies(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IMPLIES); }
|
||||
bool is_and(func_decl const * d) const { return is_decl_of(d, m_fid, OP_AND); }
|
||||
bool is_not(func_decl const * d) const { return is_decl_of(d, m_fid, OP_NOT); }
|
||||
bool is_eq(func_decl const * d) const { return is_decl_of(d, m_fid, OP_EQ); }
|
||||
bool is_iff(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IFF); }
|
||||
bool is_xor(func_decl const * d) const { return is_decl_of(d, m_fid, OP_XOR); }
|
||||
bool is_ite(func_decl const * d) const { return is_decl_of(d, m_fid, OP_ITE); }
|
||||
bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); }
|
||||
bool is_distinct(func_decl const * d) const { return is_decl_of(d, m_fid, OP_DISTINCT); }
|
||||
|
||||
MATCH_UNARY(is_not);
|
||||
MATCH_BINARY(is_eq);
|
||||
MATCH_BINARY(is_iff);
|
||||
MATCH_BINARY(is_implies);
|
||||
MATCH_BINARY(is_and);
|
||||
MATCH_BINARY(is_or);
|
||||
MATCH_BINARY(is_xor);
|
||||
MATCH_TERNARY(is_and);
|
||||
MATCH_TERNARY(is_or);
|
||||
|
||||
bool is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const;
|
||||
};
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// Get Some Value functor
|
||||
|
|
Loading…
Reference in a new issue