From 53611f47df768c6018fbd1e357ba9d5d473c221b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Sep 2022 05:48:17 -0700 Subject: [PATCH] modify clauses used by not-contains 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). --- src/ast/rewriter/seq_axioms.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 930abe4e6..de0030fc9 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -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) {