mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Added is_considered_uninterpreted() to decl_plugins.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-05 15:22:37 +00:00
parent 3d37c25bcc
commit 7ddd2856c8
4 changed files with 38 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/arith_decl_plugin.h
View file

@ -211,6 +211,25 @@ public:
virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind())
{
case OP_0_PW_0_INT:
case OP_0_PW_0_REAL:
case OP_NEG_ROOT:
case OP_DIV_0:
case OP_IDIV_0:
case OP_MOD_0:
case OP_U_ASIN:
case OP_U_ACOS:
return true;
default:
return false;
}
return false;
}
};
/**

2
src/ast/ast.h
View file

@ -992,6 +992,8 @@ public:
// Event handlers for deleting/translating PARAM_EXTERNAL
virtual void del(parameter const & p) {}
virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
};
// -----------------------------------

32
src/ast/bv_decl_plugin.h
View file

@ -266,6 +266,22 @@ public:
virtual bool are_distinct(app* a, app* b) const;
virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind()) {
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
return true;
default:
return false;
}
return false;
}
};
class bv_recognizers {
@ -353,22 +369,6 @@ public:
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
bool has_sign_bit(rational const & n, unsigned bv_size) const;
bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind()) {
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
return true;
default:
return false;
}
return false;
}
};
class bv_util : public bv_recognizers {