mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

#5641

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-02 19:36:17 -08:00
parent 9cbec3b0ca
commit a71aa113e0
2 changed files with 35 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/arith_decl_plugin.h
View file

@ -273,6 +273,17 @@ public:
bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); }
bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); }
bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); }
bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); }
bool is_add(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_ADD); }
bool is_mul(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MUL); }
bool is_sub(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_SUB); }
bool is_uminus(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_UMINUS); }
bool is_div(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_DIV); }
bool is_rem(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_REM); }
bool is_mod(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MOD); }
bool is_to_real(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_REAL); }
bool is_to_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_INT); }
bool is_is_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_IS_INT); }
bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); }
bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); }

35
src/sat/smt/arith_solver.cpp
View file

@ -1447,21 +1447,19 @@ namespace arith {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
if (!m_nla) {
TRACE("arith", tout << "no nla\n";);
CTRACE("arith", !m_nla, tout << "no nla\n";);
if (!m_nla)
return l_true;
}
if (!m_nla->need_check())
return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_lemma_vector);
switch (r) {
case l_false: {
case l_false:
for (const nla::lemma& l : m_nla_lemma_vector)
false_case_of_check_nla(l);
break;
}
case l_true:
if (assume_eqs())
return l_false;
@ -1478,11 +1476,26 @@ namespace arith {
}
bool solver::include_func_interp(func_decl* f) const {
return
a.is_div0(f) ||
a.is_idiv0(f) ||
a.is_power0(f) ||
a.is_rem0(f) ||
a.is_mod0(f);
SASSERT(f->get_family_id() == get_id());
switch (f->get_decl_kind()) {
case OP_ADD:
case OP_SUB:
case OP_UMINUS:
case OP_MUL:
case OP_LE:
case OP_LT:
case OP_GE:
case OP_GT:
case OP_MOD:
case OP_REM:
case OP_DIV:
case OP_POWER:
case OP_IS_INT:
case OP_TO_INT:
case OP_TO_REAL:
return false;
default:
return true;
}
}
}