mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 15:47:29 +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 06:57:25 -07:00
parent 17eeebe3e7
commit b67ee8cdeb
15 changed files with 123 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/char_decl_plugin.cpp
View file

@ -66,8 +66,8 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
msg << "incorrect number of arguments passed. Expected one character, received " << arity;
else {
arith_util a(m);
// TODO: non-deterministic parameter evaluation
return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr));
sort* int_sort = a.mk_int();
return m.mk_func_decl(symbol("char.to_int"), arity, domain, int_sort, func_decl_info(m_family_id, k, 0, nullptr));
}
m.raise_exception(msg.str());
case OP_CHAR_TO_BV:
@ -80,8 +80,8 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
else {
bv_util b(m);
unsigned sz = num_bits();
// TODO: non-deterministic parameter evaluation
return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr));
sort* bv_sort = b.mk_sort(sz);
return m.mk_func_decl(symbol("char.to_bv"), arity, domain, bv_sort, func_decl_info(m_family_id, k, 0, nullptr));
}
m.raise_exception(msg.str());
case OP_CHAR_FROM_BV: {

8
src/ast/converters/generic_model_converter.cpp
View file

@ -262,8 +262,12 @@ expr_ref generic_model_converter::simplify_def(entry const& e) {
rep.apply_substitution(c, m.mk_true(), result1);
rep.apply_substitution(c, m.mk_false(), result2);
th_rewriter rw(m);
// TODO: non-deterministic parameter evaluation
expr_ref result(m.mk_and(m.mk_implies(result2, c), m.mk_implies(c, result1)), m);
expr_ref impl1(m);
expr_ref impl2(m);
expr_ref result(m);
impl1 = m.mk_implies(result2, c);
impl2 = m.mk_implies(c, result1);
result = m.mk_and(impl1, impl2);
rw(result);
return result;
}

19
src/ast/normal_forms/defined_names.cpp
View file

@ -191,9 +191,21 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var
bound_vars(var_sorts, var_names, MK_OR(n, MK_NOT(e)), n, defs);
}
else if (m.is_term_ite(e)) {
// TODO: non-deterministic parameter evaluation
bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs);
bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0), MK_EQ(n, to_app(e)->get_arg(2))), n, defs);
expr* cond = to_app(e)->get_arg(0);
expr* then_branch = to_app(e)->get_arg(1);
expr* else_branch = to_app(e)->get_arg(2);
expr_ref not_cond(m);
expr_ref eq_then(m);
expr_ref eq_else(m);
expr_ref disj1(m);
expr_ref disj2(m);
not_cond = m.mk_not(cond);
eq_then = m.mk_eq(n, then_branch);
eq_else = m.mk_eq(n, else_branch);
disj1 = m.mk_or(not_cond, eq_then);
disj2 = m.mk_or(cond, eq_else);
bound_vars(var_sorts, var_names, disj1, n, defs);
bound_vars(var_sorts, var_names, disj2, n, defs);
}
else if (is_lambda(e)) {
// n(y) = \x . M[x,y]
@ -373,4 +385,3 @@ func_decl * defined_names::get_name_decl(unsigned i) const {

8
src/ast/normal_forms/pull_quant.cpp
View file

@ -265,9 +265,10 @@ struct pull_quant::imp {
return BR_FAILED;
if (m.proofs_enabled()) {
// TODO: non-deterministic parameter evaluation
result_pr = m.mk_pull_quant(m.mk_app(f, num, args),
to_quantifier(result.get()));
expr_ref f_app(m);
f_app = m.mk_app(f, num, args);
quantifier* q = to_quantifier(result.get());
result_pr = m.mk_pull_quant(f_app, q);
}
return BR_DONE;
}
@ -393,4 +394,3 @@ void pull_nested_quant::reset() {
m_imp->m_rw.reset();
}

7
src/ast/rewriter/factor_equivs.cpp
View file

@ -136,8 +136,11 @@ bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
expr_equiv_class::iterator b(a);
for (++b; b != end; ++b) {
// TODO: non-deterministic parameter evaluation
out.push_back(m.mk_eq(*a, *b));
expr* lhs = *a;
expr* rhs = *b;
expr_ref eq(m);
eq = m.mk_eq(lhs, rhs);
out.push_back(eq);
dirty = true;
}
}

14
src/ast/rewriter/factor_rewriter.cpp
View file

@ -141,10 +141,16 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) {
pos0 = pos;
}
else {
// TODO: non-deterministic parameter evaluation
tmp = m().mk_or(m().mk_and(pos, pos0), m().mk_and(neg, neg0));
// TODO: non-deterministic parameter evaluation
neg0 = m().mk_or(m().mk_and(neg, pos0), m().mk_and(pos, neg0));
expr_ref pos_and_pos0(m());
expr_ref neg_and_neg0(m());
expr_ref neg_and_pos0(m());
expr_ref pos_and_neg0(m());
pos_and_pos0 = m().mk_and(pos, pos0);
neg_and_neg0 = m().mk_and(neg, neg0);
tmp = m().mk_or(pos_and_pos0, neg_and_neg0);
neg_and_pos0 = m().mk_and(neg, pos0);
pos_and_neg0 = m().mk_and(pos, neg0);
neg0 = m().mk_or(neg_and_pos0, pos_and_neg0);
pos0 = tmp;
}
}

12
src/ast/rewriter/maximize_ac_sharing.cpp
View file

@ -58,8 +58,10 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
for (unsigned j = i + 1; j < num_args; j++) {
if (contains(f, _args[i], _args[j])) {
TRACE(ac_sharing_detail, tout << "reusing args: " << i << " " << j << "\n";);
// TODO: non-deterministic parameter evaluation
_args[i] = m.mk_app(f, _args[i], _args[j]);
expr* lhs = _args[i];
expr* rhs = _args[j];
expr* combined = m.mk_app(f, lhs, rhs);
_args[i] = combined;
SASSERT(num_args > 1);
for (unsigned w = j; w + 1 < num_args; w++) {
_args[w] = _args[w+1];
@ -82,8 +84,10 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
}
else {
insert(f, _args[i], _args[i+1]);
// TODO: non-deterministic parameter evaluation
_args[j] = m.mk_app(f, _args[i], _args[i+1]);
expr* lhs = _args[i];
expr* rhs = _args[i+1];
expr* combined = m.mk_app(f, lhs, rhs);
_args[j] = combined;
}
}
num_args = j;

9
src/ast/rewriter/rewriter_def.h
View file

@ -574,8 +574,9 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
num_no_pats = j;
}
if (ProofGen) {
// TODO: non-deterministic parameter evaluation
quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body), m());
quantifier_ref new_q(m());
quantifier* updated_q = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body);
new_q = updated_q;
m_pr = nullptr;
if (q != new_q) {
m_pr = result_pr_stack().get(fr.m_spos);
@ -600,8 +601,8 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
TRACE(reduce_quantifier_bug, tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";);
if (!m_cfg.reduce_quantifier(q, new_body, new_pats.data(), new_no_pats.data(), m_r, m_pr)) {
if (fr.m_new_child) {
// TODO: non-deterministic parameter evaluation
m_r = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body);
quantifier* updated_q = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body);
m_r = updated_q;
}
else {
TRACE(rewriter_reuse, tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";);

7
src/ast/rewriter/seq_eq_solver.cpp
View file

@ -344,8 +344,10 @@ namespace seq {
if (ctx.expr2rep(xs[0]) == ctx.expr2rep(ys[0]))
return false;
// TODO: non-deterministic parameter evaluation
expr_ref eq(m.mk_eq(xs[0], ys[0]), m);
expr* lhs = xs[0];
expr* rhs = ys[0];
expr_ref eq(m);
eq = m.mk_eq(lhs, rhs);
expr* veq = ctx.expr2rep(eq);
if (m.is_true(veq))
return false;
@ -730,4 +732,3 @@ namespace seq {
};

11
src/ast/sls/sls_seq_plugin.cpp
View file

@ -161,8 +161,15 @@ namespace sls {
if (r == 0 || sx.length() == 0)
// create lemma: len(x) = 0 <=> x = ""
// TODO: non-deterministic parameter evaluation
ctx.add_constraint(m.mk_eq(m.mk_eq(e, a.mk_int(0)), m.mk_eq(x, seq.str.mk_string(""))));
{
expr_ref len_zero(m);
expr_ref eq_empty(m);
expr_ref bicond(m);
len_zero = m.mk_eq(e, a.mk_int(0));
eq_empty = m.mk_eq(x, seq.str.mk_string(""));
bicond = m.mk_eq(len_zero, eq_empty);
ctx.add_constraint(bicond);
}
if (ctx.rand(2) == 0 && update(e, rational(sx.length())))
return false;

9
src/smt/seq_regex.cpp
View file

@ -396,8 +396,13 @@ namespace smt {
else if (re().is_empty(r2))
r = r1;
else
// TODO: non-deterministic parameter evaluation
r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1));
{
expr_ref diff12(m);
expr_ref diff21(m);
diff12 = re().mk_diff(r1, r2);
diff21 = re().mk_diff(r2, r1);
r = re().mk_union(diff12, diff21);
}
rewrite(r);
return r;
}

7
src/smt/theory_datatype.cpp
View file

@ -247,8 +247,11 @@ namespace smt {
assert_eq_axiom(arg, acc_own, is_con);
}
// update_field is identity if 'n' is not created by a matching constructor.
// TODO: non-deterministic parameter evaluation
app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_expr(), arg1)), m);
expr_ref not_rec(m);
not_rec = m.mk_not(rec_app);
expr_ref eq_expr(m);
eq_expr = m.mk_eq(n->get_expr(), arg1);
app_ref imp(m.mk_implies(not_rec, eq_expr), m);
assert_eq_axiom(n, arg1, ~is_con);
app_ref n_is_con(m.mk_app(rec, own), m);

6
src/smt/theory_dl.cpp
View file

@ -252,8 +252,10 @@ namespace smt {
get_rep(s, r, v);
app_ref lt(m()), le(m());
lt = u().mk_lt(x,y);
// TODO: non-deterministic parameter evaluation
le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x));
app_ref ry(m()), rx(m());
ry = m().mk_app(r, y);
rx = m().mk_app(r, x);
le = b().mk_ule(ry, rx);
if (m().has_trace_stream()) {
app_ref body(m());
body = m().mk_eq(lt, le);

21
src/tactic/bv/bv1_blaster_tactic.cpp
View file

@ -142,8 +142,10 @@ class bv1_blaster_tactic : public tactic {
unsigned i = bits1.size();
while (i > 0) {
--i;
// TODO: non-deterministic parameter evaluation
new_eqs.push_back(m().mk_eq(bits1[i], bits2[i]));
expr* lhs = bits1[i];
expr* rhs = bits2[i];
expr* eq = m().mk_eq(lhs, rhs);
new_eqs.push_back(eq);
}
result = mk_and(m(), new_eqs.size(), new_eqs.data());
}
@ -157,8 +159,12 @@ class bv1_blaster_tactic : public tactic {
bit_buffer new_ites;
unsigned num = t_bits.size();
for (unsigned i = 0; i < num; i++)
// TODO: non-deterministic parameter evaluation
new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i]));
{
expr* t_bit = t_bits[i];
expr* e_bit = e_bits[i];
expr* ite = t_bit == e_bit ? t_bit : m().mk_ite(c, t_bit, e_bit);
new_ites.push_back(ite);
}
result = butil().mk_concat(new_ites.size(), new_ites.data());
}
@ -218,8 +224,11 @@ class bv1_blaster_tactic : public tactic {
bit_buffer new_bits;
unsigned num = bits1.size();
for (unsigned i = 0; i < num; i++) {
// TODO: non-deterministic parameter evaluation
new_bits.push_back(m().mk_ite(m().mk_eq(bits1[i], bits2[i]), m_bit0, m_bit1));
expr* bit1 = bits1[i];
expr* bit2 = bits2[i];
expr* eq_bits = m().mk_eq(bit1, bit2);
expr* ite = m().mk_ite(eq_bits, m_bit0, m_bit1);
new_bits.push_back(ite);
}
result = butil().mk_concat(new_bits.size(), new_bits.data());
}

32
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -149,8 +149,12 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
expr_ref body(m_manager);
// TODO: non-deterministic parameter evaluation
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
expr* x_arg = x.get();
app_ref ft_app(m_manager);
app_ref fs_app(m_manager);
ft_app = m_manager.mk_app(f_t, x_arg);
fs_app = m_manager.mk_app(f_s, x_arg);
body = m_manager.mk_eq(ft_app, fs_app);
result = m_manager.mk_forall(1, sorts, names, body);
res = BR_DONE;
@ -296,9 +300,12 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
new_args.push_back(m_manager.mk_app(ss[i].get(), x.get()));
expr_ref body(m_manager);
// TODO: non-deterministic parameter evaluation
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
m_manager.mk_app(map_f, num, new_args.data()));
expr* x_arg = x.get();
app_ref ft_app(m_manager);
ft_app = m_manager.mk_app(f_t, x_arg);
app_ref map_app(m_manager);
map_app = m_manager.mk_app(map_f, num, new_args.data());
body = m_manager.mk_eq(ft_app, map_app);
expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
extra_assertions.push_back(frllx);
@ -332,11 +339,16 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
expr_ref body(m_manager);
// TODO: non-deterministic parameter evaluation
body = m_manager.mk_or(m_manager.mk_eq(x, i),
// TODO: non-deterministic parameter evaluation
m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
m_manager.mk_app(f_s, x.get())));
expr_ref eq_x_i(m_manager);
eq_x_i = m_manager.mk_eq(x, i);
expr* x_arg = x.get();
app_ref ft_app(m_manager);
app_ref fs_app(m_manager);
ft_app = m_manager.mk_app(f_t, x_arg);
fs_app = m_manager.mk_app(f_s, x_arg);
expr_ref funcs_eq(m_manager);
funcs_eq = m_manager.mk_eq(ft_app, fs_app);
body = m_manager.mk_or(eq_x_i, funcs_eq);
expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
extra_assertions.push_back(frllx);