mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Bugfix for bv*div0 model construction.
This commit is contained in:
parent
88f007e9da
commit
bb5118acbb
|
@ -354,6 +354,21 @@ public:
|
|||
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 {
|
||||
|
|
|
@ -694,7 +694,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
if (r2.is_zero()) {
|
||||
if (!hi_div0) {
|
||||
result = m().mk_app(get_fid(), OP_BSDIV0, arg1);
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
// The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
|
||||
|
@ -745,7 +745,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
if (r2.is_zero()) {
|
||||
if (!hi_div0) {
|
||||
result = m().mk_app(get_fid(), OP_BUDIV0, arg1);
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
// The "hardware interpretation" for (bvudiv x 0) is #xffff
|
||||
|
@ -808,7 +808,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
if (r2.is_zero()) {
|
||||
if (!hi_div0) {
|
||||
result = m().mk_app(get_fid(), OP_BSREM0, arg1);
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
// The "hardware interpretation" for (bvsrem x 0) is x
|
||||
|
|
|
@ -155,7 +155,7 @@ public:
|
|||
void updt_params(params_ref const & p);
|
||||
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
|
||||
|
||||
void set_mkbv2num(bool f) { m_mkbv2num = f; }
|
||||
|
||||
unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); }
|
||||
|
@ -164,7 +164,7 @@ public:
|
|||
bool is_bv(expr * t) const { return m_util.is_bv(t); }
|
||||
expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); }
|
||||
expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); }
|
||||
|
||||
|
||||
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
|
||||
void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
if (mk_app_core(f, num_args, args, result) == BR_FAILED)
|
||||
|
@ -174,6 +174,8 @@ public:
|
|||
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
|
||||
|
||||
bool hi_div0() const { return m_hi_div0; }
|
||||
|
||||
bv_util & get_util() { return m_util; }
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -181,6 +181,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
}
|
||||
|
||||
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
|
||||
TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
|
||||
|
||||
func_interp * fi = m_model.get_func_interp(f);
|
||||
if (fi != 0) {
|
||||
|
@ -199,7 +200,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
return true;
|
||||
}
|
||||
|
||||
if (f->get_family_id() == null_family_id && m_model_completion) {
|
||||
if (m_model_completion &&
|
||||
(f->get_family_id() == null_family_id ||
|
||||
m_bv_rw.get_util().is_considered_uninterpreted(f)))
|
||||
{
|
||||
sort * s = f->get_range();
|
||||
expr * val = m_model.get_some_value(s);
|
||||
func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
|
||||
|
|
Loading…
Reference in a new issue