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

modify clauses used by not-contains

Browse source 
The literal "emp" can be true in the current assignment, in which case the clause
cnt or emp or ~postf is true and does not contribute to propagation.
This saves, potentially, for generating lemmas for postf.

Add a lemma a = "" or |s| >= idx when a = tail(s, idx)
The lemma ensures that length bounding on s is enforced
(the branch that expands not-contains for long sequences s is closed).
This commit is contained in:
Nikolaj Bjorner 2022-09-11 05:48:17 -07:00
parent 7a55bd5687
commit 53611f47df
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1258,9 +1258,12 @@ namespace seq {
expr_ref emp = mk_eq_empty(a);
expr_ref cnt = expr_ref(e, m);
add_clause(cnt, ~pref);
add_clause(cnt, ~postf);
add_clause(cnt, emp, ~postf);
add_clause(~emp, mk_eq_empty(tail));
add_clause(emp, mk_eq(a, seq.str.mk_concat(head, tail)));
expr* s, *idx;
if (m_sk.is_tail(tail, s, idx))
add_clause(emp, mk_ge_e(mk_len(s), idx));
}
expr_ref axioms::length_limit(expr* s, unsigned k) {