mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

add filter for avoiding creating redundant disequality axioms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-19 23:15:23 -07:00
parent 1d928663de
commit 0f4126f665
4 changed files with 20 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_axioms.cpp
View file

@ -1357,8 +1357,14 @@ namespace seq {
expr_ref vp = m_sk.mk("diseq.v'", u, v);
expr_ref up_len(mk_len(up), m);
expr_ref vp_len(mk_len(vp), m);
expr_ref u_eq(mk_eq(u, mk_concat(w, seq.str.mk_unit(a), up)), m);
expr_ref v_eq(mk_eq(v, mk_concat(w, seq.str.mk_unit(b), vp)), m);
expr_ref wau(mk_concat(w, seq.str.mk_unit(a), up), m);
expr_ref wbv(mk_concat(w, seq.str.mk_unit(b), vp), m);
expr_ref u_eq(mk_eq(u, wau), m);
expr_ref v_eq(mk_eq(v, wbv), m);
if (m_mark_no_diseq) {
m_mark_no_diseq(wau);
m_mark_no_diseq(wbv);
}
add_clause(eq_uv, ~len_eq, u_eq);
add_clause(eq_uv, ~len_eq, v_eq);
add_clause(eq_uv, ~len_eq, ~mk_eq(a, b));

4
src/ast/rewriter/seq_axioms.h
View file

@ -38,6 +38,7 @@ namespace seq {
std::function<void(expr_ref_vector const&)> m_add_clause;
std::function<void(expr*)> m_set_phase;
std::function<void(void)> m_ensure_digits;
std::function<void(expr *)> m_mark_no_diseq;
expr_ref mk_len(expr* s);
expr_ref mk_sub(expr* x, expr* y);
@ -81,6 +82,9 @@ namespace seq {
void set_add_clause(std::function<void(expr_ref_vector const&)>& ac) { m_add_clause = ac; }
void set_phase(std::function<void(expr*)>& sp) { m_set_phase = sp; }
void set_ensure_digits(std::function<void(void)>& ed) { m_ensure_digits = ed; }
void set_mark_no_diseq(std::function<void(expr *)> &f) {
m_mark_no_diseq = f;
}
void suffix_axiom(expr* n);
void prefix_axiom(expr* n);

8
src/smt/theory_nseq.cpp
View file

@ -63,9 +63,14 @@ namespace smt {
std::function < void(void)> ensure_digit_axiom = [&]() {
throw default_exception("digit axioms should be added lazily via seq_axioms::ensure_digit_axiom");
};
std::function<void(expr *)> mark_no_diseq = [&](expr *e) {
m_no_diseq_set.insert(e);
ctx.push_trail(insert_obj_trail(m_no_diseq_set, e));
};
m_axioms.set_add_clause(add_clause);
m_axioms.set_phase(set_phase);
m_axioms.set_ensure_digits(ensure_digit_axiom);
m_axioms.set_mark_no_diseq(mark_no_diseq);
}
// -----------------------------------------------------------------------
@ -177,10 +182,11 @@ namespace smt {
void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) {
expr* e1 = get_enode(v1)->get_expr();
expr* e2 = get_enode(v2)->get_expr();
TRACE(seq, tout << mk_pp(e1, m) << " != " << mk_pp(e2, m) << "\n");
if (m_seq.is_re(e1))
// regex disequality: nseq cannot verify language non-equivalence
push_unhandled_pred();
else if (m_seq.is_seq(e1))
else if (m_seq.is_seq(e1) && !m_no_diseq_set.contains(e1) && !m_no_diseq_set.contains(e2))
m_axioms.diseq_axiom(e1, e2);
else
;

1
src/smt/theory_nseq.h
View file

@ -62,6 +62,7 @@ namespace smt {
unsigned m_prop_qhead = 0;
unsigned m_next_mem_id = 0; // monotone counter for tracked_str_mem ids
obj_hashtable<expr> m_axiom_set; // dedup guard for axiom_item enqueues
obj_hashtable<expr> m_no_diseq_set; // track expressions that should not trigger new disequality axioms
// statistics
unsigned m_num_conflicts = 0;