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

precalc parameters to define the eval order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-06 21:11:47 -07:00 • committed by Lev Nachmanson
parent eeb1c18aa4
commit 3eda3867d3
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_seq.cpp
View file

@ -440,7 +440,10 @@ final_check_status theory_seq::final_check_eh() {
bool theory_seq::set_empty(expr* x) {
add_axiom(~mk_eq(m_autil.mk_int(0), mk_len(x), false), mk_eq_empty(x));
// pre-calculate literals to enforce evaluation order
literal zero_len_lit = mk_eq(m_autil.mk_int(0), mk_len(x), false);
literal empty_lit = mk_eq_empty(x);
add_axiom(~zero_len_lit, empty_lit);
return true;
}
@ -3106,7 +3109,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
propagate_non_empty(lit, se2);
dependency* dep = m_dm.mk_leaf(assumption(lit));
// |e1| - |e2| <= -1
literal len_gt = m_ax.mk_le(mk_sub(mk_len(se1), mk_len(se2)), -1);
auto e1e = mk_len(se1);
literal len_gt = m_ax.mk_le(mk_sub(e1e, mk_len(se2)), -1);
ctx.force_phase(len_gt);
m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
}