Navigation Menu

Skip to content

Commit

Permalink
adding div0
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 6, 2019
1 parent 1048abf commit 6cf7d8e
Show file tree
Hide file tree
Showing 6 changed files with 86 additions and 14 deletions.
20 changes: 19 additions & 1 deletion src/ast/arith_decl_plugin.cpp
View file
Expand Up @@ -362,6 +362,11 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
case OP_IDIVIDES: UNREACHABLE();
case OP_REM: return m_i_rem_decl;
case OP_MOD: return m_i_mod_decl;
case OP_DIV0: return m_manager->mk_func_decl(symbol("div0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_DIV0));
case OP_IDIV0: return m_manager->mk_func_decl(symbol("idiv0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_IDIV0));
case OP_REM0: return m_manager->mk_func_decl(symbol("rem0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_REM0));
case OP_MOD0: return m_manager->mk_func_decl(symbol("mod0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_MOD0));
case OP_POWER0: return m_manager->mk_func_decl(symbol("power0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0));
case OP_TO_REAL: return m_to_real_decl;
case OP_TO_INT: return m_to_int_decl;
case OP_IS_INT: return m_is_int_decl;
Expand Down Expand Up @@ -780,18 +785,31 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
return result;
}

bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args) {
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, m_afid, OP_DIV) && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real());
return true;
}
if (is_decl_of(f, m_afid, OP_IDIV) && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_real());
return true;
}
if (is_decl_of(f, m_afid, OP_MOD) && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_real());
return true;
}
if (is_decl_of(f, m_afid, OP_REM) && is_numeral(args[1], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_real());
return true;
}
if (is_decl_of(f, m_afid, OP_POWER) && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) {
sort* rs[2] = { mk_real(), mk_real() };
f_out = m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, mk_real());
return true;
}
return plugin().is_considered_uninterpreted(f);
Expand Down
23 changes: 20 additions & 3 deletions src/ast/arith_decl_plugin.h
View file
Expand Up @@ -46,14 +46,19 @@ enum arith_op_kind {
OP_MUL,
OP_DIV,
OP_IDIV,
OP_DIV0,
OP_IDIV0,
OP_IDIVIDES,
OP_REM,
OP_MOD,
OP_REM0,
OP_MOD0,
OP_TO_REAL,
OP_TO_INT,
OP_IS_INT,
OP_ABS,
OP_POWER,
OP_POWER0,
// hyperbolic and trigonometric functions
OP_SIN,
OP_COS,
Expand Down Expand Up @@ -260,14 +265,21 @@ class arith_recognizers {
bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); }
bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); }
bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); }

bool is_div0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_DIV0); }
bool is_idiv0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_IDIV0); }
bool is_rem0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_REM0); }
bool is_mod0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_MOD0); }
bool is_power0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_POWER0); }

bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); }
bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); }
bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
//bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV0); }
bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
//bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV0); }
bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
Expand Down Expand Up @@ -395,10 +407,15 @@ class arith_util : public arith_recognizers {
app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }
app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); }
app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD, arg1, arg2); }
app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV0, arg1, arg2); }
app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV0, arg1, arg2); }
app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM0, arg1, arg2); }
app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD0, arg1, arg2); }
app * mk_to_real(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_REAL, arg1); }
app * mk_to_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_INT, arg1); }
app * mk_is_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_IS_INT, arg1); }
app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER, arg1, arg2); }
app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER0, arg1, arg2); }

app * mk_sin(expr * arg) { return m_manager.mk_app(m_afid, OP_SIN, arg); }
app * mk_cos(expr * arg) { return m_manager.mk_app(m_afid, OP_COS, arg); }
Expand Down Expand Up @@ -444,7 +461,7 @@ class arith_util : public arith_recognizers {
expr_ref mk_add_simplify(expr_ref_vector const& args);
expr_ref mk_add_simplify(unsigned sz, expr* const* args);

bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args);
bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);

};

Expand Down
23 changes: 15 additions & 8 deletions src/model/model_evaluator.cpp
View file
Expand Up @@ -334,6 +334,21 @@ struct evaluator_cfg : public default_rewriter_cfg {

func_interp * fi = m_model.get_func_interp(f);


func_decl_ref f_ui(m);
if (!fi && m_au.is_considered_uninterpreted(f, num, args, f_ui)) {
if (f_ui) {
fi = m_model.get_func_interp(f);
}
if (!fi) {
result = m_au.mk_numeral(rational(0), f->get_range());
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;
}
if (fi) {
if (fi->is_partial())
fi->set_else(m.get_some_value(f->get_range()));
Expand All @@ -343,14 +358,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_REWRITE_FULL;
}

if (m_au.is_considered_uninterpreted(f, num, args)) {
result = m_au.mk_numeral(rational(0), f->get_range());
return BR_DONE;
}
else if (m_fpau.is_considered_uninterpreted(f, num, args)) {
result = m.get_some_value(f->get_range());
return BR_DONE;
}
return BR_FAILED;
}

Expand Down
1 change: 0 additions & 1 deletion src/muz/rel/dl_base.h
View file
Expand Up @@ -435,7 +435,6 @@ namespace datalog {
Since the destructor is protected, we cannot use the \c dealloc macro.
*/
void destroy() {
SASSERT(this != nullptr);
this->~base_ancestor();
memory::deallocate(this);
}
Expand Down
2 changes: 2 additions & 0 deletions src/smt/theory_arith.h
View file
Expand Up @@ -440,6 +440,7 @@ namespace smt {
arith_eq_solver m_arith_eq_solver;
bool m_found_unsupported_op;
bool m_found_underspecified_op;
ptr_vector<app> m_underspecified_ops;
arith_eq_adapter m_arith_eq_adapter;
vector<row> m_rows;
svector<unsigned> m_dead_rows;
Expand Down Expand Up @@ -1077,6 +1078,7 @@ namespace smt {
//
// -----------------------------------
bool get_value(enode * n, expr_ref & r) override;
bool include_func_interp(func_decl* f) override;

bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
Expand Down
31 changes: 30 additions & 1 deletion src/smt/theory_arith_core.h
View file
Expand Up @@ -39,6 +39,8 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) {
m_underspecified_ops.push_back(n);
get_context().push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
if (!m_found_underspecified_op) {
TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
Expand Down Expand Up @@ -388,7 +390,6 @@ namespace smt {
theory_var theory_arith<Ext>::internalize_div(app * n) {
rational r(1);
if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy())
Expand Down Expand Up @@ -3271,8 +3272,36 @@ namespace smt {
if (!m_model_depends_on_computed_epsilon) {
refine_epsilon();
}
for (app* n : m_underspecified_ops) {
if (m_util.is_div(n)) {
mk_enode(m_util.mk_div0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_idiv(n)) {
mk_enode(m_util.mk_idiv0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_rem(n)) {
mk_enode(m_util.mk_rem0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_mod(n)) {
mk_enode(m_util.mk_mod0(n->get_arg(0), n->get_arg(1)));
}
else if (m_util.is_power(n)) {
mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1)));
}
}
}

template<typename Ext>
bool theory_arith<Ext>::include_func_interp(func_decl* f) {
return
m_util.is_div0(f) ||
m_util.is_idiv0(f) ||
m_util.is_power0(f) ||
m_util.is_rem0(f) ||
m_util.is_mod0(f);
}


template<typename Ext>
model_value_proc * theory_arith<Ext>::mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id());
Expand Down

0 comments on commit 6cf7d8e

Please sign in to comment.