mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

add rewrite for partially interpreted arithmetic functions

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-07-25 14:57:27 -07:00
parent 0f2fe6031a
commit c6aab89662
3 changed files with 34 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/ast/arith_decl_plugin.cpp
View file

@ -801,6 +801,29 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
return result;
}
bool arith_util::is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && !is_numeral(args[1])) {
f_out = mk_div0();
return true;
}
if (is_decl_of(f, arith_family_id, OP_IDIV) && n == 2 && !is_numeral(args[1])) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
return true;
}
if (is_decl_of(f, arith_family_id, OP_MOD) && n == 2 && !is_numeral(args[1])) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
return true;
}
if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && !is_numeral(args[1])) {
sort* rs[2] = { mk_int(), mk_int() };
f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
return true;
}
return false;
}
bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
rational r;
if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {

2
src/ast/arith_decl_plugin.h
View file

@ -517,6 +517,8 @@ public:
bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
bool is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
bool is_underspecified(expr* e) const;
bool is_bounded(expr* e) const;

9
src/model/model_evaluator.cpp
View file

@ -421,6 +421,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_DONE;
}
}
else if (!fi && m_au.is_considered_partially_interpreted(f, num, args, f_ui)) {
fi = m_model.get_func_interp(f_ui);
if (fi) {
var_subst vs(m, false);
result = vs(fi->get_interp(), num, args);
result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args));
return BR_DONE;
}
}
else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) {
result = m.get_some_value(f->get_range());
return BR_DONE;