mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

#5753

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-15 10:03:03 -08:00
parent 74824ac901
commit 17cfc1d034
2 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/sat/smt/arith_internalize.cpp
View file

@ -269,17 +269,16 @@ namespace arith {
}
else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
found_unsupported(n);
ensure_arg_vars(to_app(n));
}
else {
// no-op
ensure_arg_vars(to_app(n));
}
}
else {
if (is_app(n)) {
internalize_args(to_app(n));
for (expr* arg : *to_app(n))
if (a.is_real(arg) || a.is_int(arg))
internalize_term(arg);
ensure_arg_vars(to_app(n));
}
theory_var v = mk_evar(n);
coeffs[vars.size()] = coeffs[index];
@ -426,6 +425,12 @@ namespace arith {
e_internalize(arg);
}
void solver::ensure_arg_vars(app* n) {
for (expr* arg : *to_app(n))
if (a.is_real(arg) || a.is_int(arg))
internalize_term(arg);
}
theory_var solver::internalize_power(app* t, app* n, unsigned p) {
internalize_args(t, true);
bool _has_var = has_var(t);

1
src/sat/smt/arith_solver.h
View file

@ -239,6 +239,7 @@ namespace arith {
void add_def_constraint(lp::constraint_index index, theory_var v);
void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, const rational& bound);
void internalize_args(app* t, bool force = false);
void ensure_arg_vars(app* t);
theory_var internalize_power(app* t, app* n, unsigned p);
theory_var internalize_mul(app* t);
theory_var internalize_def(expr* term);