mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-07 14:55:06 +00:00
Code Activity

another batch of nond args fixes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-29 07:46:55 -07:00
parent e620c5e689
commit 7dae39c24b
11 changed files with 134 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

109
src/ast/rewriter/arith_rewriter.cpp
View file

@ -622,18 +622,41 @@ br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind
return BR_FAILED;
expr_ref f2 = remove_factor(f, arg1);
expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1));
// TODO: non-deterministic parameter evaluation
result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z));
expr_ref eq_f(m);
expr_ref eq_f2(m);
expr_ref disj(m);
eq_f = m_util.mk_eq(f, z);
eq_f2 = m_util.mk_eq(f2, z);
disj = m.mk_or(eq_f, eq_f2);
switch (kind) {
case EQ:
result = disj;
break;
case GE:
result = m.mk_or(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)), result);
{
expr_ref ge_f(m);
expr_ref ge_f2(m);
expr_ref iff(m);
ge_f = m_util.mk_ge(f, z);
ge_f2 = m_util.mk_ge(f2, z);
iff = m.mk_iff(ge_f, ge_f2);
result = m.mk_or(iff, disj);
break;
}
case LE:
result = m.mk_or(m.mk_not(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z))), result);
{
expr_ref ge_f(m);
expr_ref ge_f2(m);
expr_ref iff(m);
expr_ref not_iff(m);
ge_f = m_util.mk_ge(f, z);
ge_f2 = m_util.mk_ge(f2, z);
iff = m.mk_iff(ge_f, ge_f2);
not_iff = m.mk_not(iff);
result = m.mk_or(not_iff, disj);
break;
}
}
return BR_REWRITE3;
}
return BR_FAILED;
@ -869,9 +892,13 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
rational g = gcd(p, k, a, b);
if (g == 1) {
expr_ref nb(m_util.mk_numeral(b, true), m);
// TODO: non-deterministic parameter evaluation
result = m.mk_eq(m_util.mk_mod(u, y),
m_util.mk_mod(m_util.mk_mul(nb, arg2), y));
expr_ref lhs(m);
expr_ref rhs_mul(m);
expr_ref rhs(m);
lhs = m_util.mk_mod(u, y);
rhs_mul = m_util.mk_mul(nb, arg2);
rhs = m_util.mk_mod(rhs_mul, y);
result = m.mk_eq(lhs, rhs);
return true;
}
}
@ -1204,8 +1231,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
}
br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) {
// TODO: non-deterministic parameter evaluation
result = m.mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0));
expr_ref modulus(m);
expr_ref zero(m);
modulus = m_util.mk_mod(arg, m_util.mk_int(k));
zero = m_util.mk_int(0);
result = m.mk_eq(modulus, zero);
return BR_REWRITE2;
}
@ -1232,8 +1262,13 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
}
if (arg1 == arg2) {
expr_ref zero(m_util.mk_int(0), m);
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
expr_ref condition(m);
expr_ref idiv_zero(m);
expr_ref one(m);
condition = m.mk_eq(arg1, zero);
idiv_zero = m_util.mk_idiv(zero, zero);
one = m_util.mk_int(1);
result = m.mk_ite(condition, idiv_zero, one);
return BR_REWRITE3;
}
if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) {
@ -1331,14 +1366,18 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.data());
expr_ref d(m_util.mk_idiv(num, den), m);
expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m);
// TODO: non-deterministic parameter evaluation
return expr_ref(m.mk_ite(m.mk_eq(zero, arg),
m_util.mk_idiv(zero, zero),
m.mk_ite(m_util.mk_ge(arg, zero),
d,
nd)),
m);
}
expr_ref cond_zero(m);
expr_ref cond_ge(m);
expr_ref zero_div(m);
expr_ref inner(m);
expr_ref outer(m);
cond_zero = m.mk_eq(zero, arg);
cond_ge = m_util.mk_ge(arg, zero);
zero_div = m_util.mk_idiv(zero, zero);
inner = m.mk_ite(cond_ge, d, nd);
outer = m.mk_ite(cond_zero, zero_div, inner);
return expr_ref(outer, m);
}
void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
args.push_back(e);
@ -1432,8 +1471,11 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
expr* x = nullptr, * y = nullptr, * z = nullptr;
if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) {
// TODO: non-deterministic parameter evaluation
result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1)));
expr_ref coeff(m);
expr_ref modulus(m);
coeff = m_util.mk_int(v1);
modulus = m_util.mk_mod(y, m_util.mk_int(v2 / v1));
result = m_util.mk_mul(coeff, modulus);
return BR_REWRITE1;
}
@ -2083,21 +2125,29 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
if (k_prime == rational(1, 3) || k_prime == rational(2, 3)) {
// sin(pi/3) == sin(2/3 pi) == Sqrt(3)/2
// sin(4/3 pi) == sin(5/3 pi) == - Sqrt(3)/2
expr * result = m_util.mk_div(mk_sqrt(rational(3)), m_util.mk_numeral(rational(2), false));
expr_ref numerator(mk_sqrt(rational(3)), m);
expr_ref denom(m_util.mk_numeral(rational(2), false), m);
expr * result = m_util.mk_div(numerator, denom);
return neg ? m_util.mk_uminus(result) : result;
}
if (k_prime == rational(1, 12) || k_prime == rational(11, 12)) {
// sin(1/12 pi) == sin(11/12 pi) == [sqrt(6) - sqrt(2)]/4
// sin(13/12 pi) == sin(23/12 pi) == -[sqrt(6) - sqrt(2)]/4
// TODO: non-deterministic parameter evaluation
expr * result = m_util.mk_div(m_util.mk_sub(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
expr_ref sqrt6(mk_sqrt(rational(6)), m);
expr_ref sqrt2(mk_sqrt(rational(2)), m);
expr_ref diff(m_util.mk_sub(sqrt6, sqrt2), m);
expr_ref denom(m_util.mk_numeral(rational(4), false), m);
expr * result = m_util.mk_div(diff, denom);
return neg ? m_util.mk_uminus(result) : result;
}
if (k_prime == rational(5, 12) || k_prime == rational(7, 12)) {
// sin(5/12 pi) == sin(7/12 pi) == [sqrt(6) + sqrt(2)]/4
// sin(17/12 pi) == sin(19/12 pi) == -[sqrt(6) + sqrt(2)]/4
// TODO: non-deterministic parameter evaluation
expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
expr_ref sqrt6(mk_sqrt(rational(6)), m);
expr_ref sqrt2(mk_sqrt(rational(2)), m);
expr_ref sum(m_util.mk_add(sqrt6, sqrt2), m);
expr_ref denom(m_util.mk_numeral(rational(4), false), m);
expr * result = m_util.mk_div(sum, denom);
return neg ? m_util.mk_uminus(result) : result;
}
return nullptr;
@ -2273,10 +2323,11 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
return BR_REWRITE2;
}
end:
end:
if (m_expand_tan) {
// TODO: non-deterministic parameter evaluation
result = m_util.mk_div(m_util.mk_sin(arg), m_util.mk_cos(arg));
expr* num = m_util.mk_sin(arg);
expr* den = m_util.mk_cos(arg);
result = m_util.mk_div(num, den);
return BR_REWRITE2;
}
return BR_FAILED;

12
src/ast/rewriter/poly_rewriter_def.h
View file

@ -923,9 +923,10 @@ bool poly_rewriter<Config>::hoist_multiplication(expr_ref& som) {
}
if (mul_map.find(e, j) && valid[j] && j != k) {
m_curr_sort = adds[k]->get_sort();
// TODO: non-deterministic parameter evaluation
adds[j] = merge_muls(adds[j], adds[k]);
adds[k] = mk_numeral(rational(0));
expr* merged = merge_muls(adds[j], adds[k]);
expr* zero_expr = mk_numeral(rational(0));
adds[j] = merged;
adds[k] = zero_expr;
valid[j] = false;
valid[k] = false;
change = true;
@ -1066,8 +1067,9 @@ template<typename Config>
expr* poly_rewriter<Config>::apply_hoist(expr* a, numeral const& g, obj_hashtable<expr> const& shared) {
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (M().is_ite(a, c, t, e)) {
// TODO: non-deterministic parameter evaluation
return M().mk_ite(c, apply_hoist(t, g, shared), apply_hoist(e, g, shared));
expr* then_branch = apply_hoist(t, g, shared);
expr* else_branch = apply_hoist(e, g, shared);
return M().mk_ite(c, then_branch, else_branch);
}
rational k;
if (is_nontrivial_gcd(g) && is_int_numeral(a, k)) {

5
src/muz/rel/dl_base.cpp
View file

@ -454,8 +454,9 @@ namespace datalog {
r.get_fact(fact);
conjs.reset();
for (unsigned i = 0; i < fact.size(); ++i) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(util.mk_numeral(fact[i], sig[i]), m);
conjs.push_back(m.mk_eq(lhs, rhs));
}
brw.mk_and(conjs.size(), conjs.data(), fml);
disjs.push_back(fml);

16
src/muz/rel/dl_bound_relation.cpp
View file

@ -658,20 +658,23 @@ namespace datalog {
relation_signature const& sig = get_signature();
for (unsigned i = 0; i < sig.size(); ++i) {
if (i != find(i)) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), m.mk_var(find(i), sig[find(i)])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(m.mk_var(find(i), sig[find(i)]), m);
conjs.push_back(m.mk_eq(lhs, rhs));
continue;
}
uint_set2 const& upper = (*this)[i];
uint_set::iterator it = upper.lt.begin(), end = upper.lt.end();
for (; it != end; ++it) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(arith.mk_lt(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(m.mk_var(*it, sig[*it]), m);
conjs.push_back(arith.mk_lt(lhs, rhs));
}
it = upper.le.begin(), end = upper.le.end();
for (; it != end; ++it) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(arith.mk_le(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(m.mk_var(*it, sig[*it]), m);
conjs.push_back(arith.mk_le(lhs, rhs));
}
}
bsimp.mk_and(conjs.size(), conjs.data(), fml);
@ -707,4 +710,3 @@ namespace datalog {
};

5
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -2363,8 +2363,9 @@ namespace datalog {
unsigned rel_idx = static_cast<unsigned>(fact[fact_sz-1]);
m_others[rel_idx]->to_formula(tmp);
for (unsigned i = 0; i + 1 < fact_sz; ++i) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(util.mk_numeral(fact[i], sig[i]), m);
conjs.push_back(m.mk_eq(lhs, rhs));
}
sh(tmp, fact_sz-1, tmp);
conjs.push_back(tmp);

7
src/muz/rel/dl_interval_relation.cpp
View file

@ -375,9 +375,9 @@ namespace datalog {
relation_signature const& sig = get_signature();
for (unsigned i = 0; i < sig.size(); ++i) {
if (i != find(i)) {
// TODO: non-deterministic parameter evaluation
conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]),
m.mk_var(find(i), sig[find(i)])));
expr_ref lhs(m.mk_var(i, sig[i]), m);
expr_ref rhs(m.mk_var(find(i), sig[find(i)]), m);
conjs.push_back(m.mk_eq(lhs, rhs));
continue;
}
interval const& iv = (*this)[i];
@ -650,4 +650,3 @@ namespace datalog {
}
};

6
src/muz/spacer/spacer_convex_closure.cpp
View file

@ -369,7 +369,6 @@ void convex_closure::cc_1dim(const expr_ref &var, expr_ref_vector &out) {
m_data.get_col(j, data);
std::sort(data.begin(), data.end(), gt_proc);
if (infer_div_pred(data, cr, off)) {
// TODO: non-deterministic parameter evaluation
out.push_back(mk_eq_mod(v, cr, off));
}
}
@ -379,8 +378,9 @@ void convex_closure::cc_1dim(const expr_ref &var, expr_ref_vector &out) {
expr *convex_closure::mk_eq_mod(expr *v, rational d, rational r) {
expr *res = nullptr;
if (m_arith.is_int(v)) {
// TODO: non-deterministic parameter evaluation
res = m.mk_eq(m_arith.mk_mod(v, m_arith.mk_int(d)), m_arith.mk_int(r));
expr* mod_expr = m_arith.mk_mod(v, m_arith.mk_int(d));
expr* rhs = m_arith.mk_int(r);
res = m.mk_eq(mod_expr, rhs);
} else if (m_bv.is_bv(v)) {
res = m.mk_eq(m_bv.mk_bv_urem(v, m_bv.mk_numeral(d, m_bv_sz)),
m_bv.mk_numeral(r, m_bv_sz));

6
src/muz/spacer/spacer_generalizers.cpp
View file

@ -251,9 +251,9 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
expr_ref_vector eqs(m);
for (unsigned i = 0, sz = vsymbs.size(); i < sz; ++i) {
for (unsigned j = i + 1; j < sz; ++j) {
// TODO: non-deterministic parameter evaluation
eqs.push_back(m.mk_eq(m.mk_const(vsymbs.get(i)),
m.mk_const(vsymbs.get(j))));
expr* lhs = m.mk_const(vsymbs.get(i));
expr* rhs = m.mk_const(vsymbs.get(j));
eqs.push_back(m.mk_eq(lhs, rhs));
}
}

28
src/sat/smt/arith_axioms.cpp
View file

@ -261,10 +261,11 @@ namespace arith {
// x mod 2^{i + 1} >= 2^i means the i'th bit is 1.
auto bitof = [&](expr* x, unsigned i) {
expr_ref r(m);
// TODO: non-deterministic parameter evaluation
r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i)));
return mk_literal(r);
expr* pow_hi = a.mk_int(rational::power_of_two(i + 1));
expr* pow_lo = a.mk_int(rational::power_of_two(i));
expr* mod_expr = a.mk_mod(x, pow_hi);
expr* ge_expr = a.mk_ge(mod_expr, pow_lo);
return mk_literal(ge_expr);
};
if (a.is_band(n)) {
@ -390,13 +391,18 @@ namespace arith {
// y >= sz & x < 2^{sz-1} => n = 0
// y >= sz & x >= 2^{sz-1} => n = -1
// y = 0 => n = x
auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
// TODO: non-deterministic parameter evaluation
add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0))));
// TODO: non-deterministic parameter evaluation
add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1))));
// TODO: non-deterministic parameter evaluation
add_clause(~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
expr_ref half(a.mk_int(N/2), m);
expr_ref sign_expr(a.mk_ge(x, half), m);
auto signx = mk_literal(sign_expr);
expr_ref modulus(a.mk_mod(y, a.mk_int(N)), m);
expr_ref ge_sz(a.mk_ge(modulus, a.mk_int(sz)), m);
expr_ref eq_zero(m.mk_eq(n, a.mk_int(0)), m);
expr_ref eq_minus_one(m.mk_eq(n, a.mk_int(N - 1)), m);
expr_ref mod_zero(a.mk_eq(modulus, a.mk_int(0)), m);
expr_ref eq_x(m.mk_eq(n, x), m);
add_clause(~mk_literal(ge_sz), signx, mk_literal(eq_zero));
add_clause(~mk_literal(ge_sz), ~signx, mk_literal(eq_minus_one));
add_clause(~mk_literal(mod_zero), mk_literal(eq_x));
}
else
UNREACHABLE();

5
src/sat/smt/q_solver.cpp
View file

@ -341,8 +341,9 @@ namespace q {
}
if (m.is_not(arg, z) && m.is_iff(z, x, y) && is_literal(x) && is_literal(y)) {
e1 = m.mk_or(x, y);
// TODO: non-deterministic parameter evaluation
e2 = m.mk_or(mk_not(m, x), mk_not(m, y));
expr* nx = mk_not(m, x);
expr* ny = mk_not(m, y);
e2 = m.mk_or(nx, ny);
return true;
}
return false;

5
src/sat/tactic/sat2goal.cpp
View file

@ -253,8 +253,9 @@ struct sat2goal::imp {
s.collect_bin_clauses(bin_clauses, m_learned, false);
for (sat::solver::bin_clause const& bc : bin_clauses) {
checkpoint();
// TODO: non-deterministic parameter evaluation
r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second)));
expr* lhs = lit2expr(mc, bc.first);
expr* rhs = lit2expr(mc, bc.second);
r.assert_expr(m.mk_or(lhs, rhs));
}
// collect clauses
assert_clauses(mc, s, s.clauses(), r, true);