mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

not-contains placeholder

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-22 18:40:08 -07:00
parent 7b27866310
commit d1d050f69f
2 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1336,6 +1336,22 @@ namespace seq {
add_clause(emp, mk_ge_e(mk_len(s), idx));
}
/**
* Consider the recursive definition of negated contains:
~contains(a, b) =
if |b| > |a| then true
else if |b| = |a| then a != b
else ~prefix(b, a) and ~contains(a[1:], b)
Create the recursive function not_contains that implements this recursive definition.
Add the axiom
contains(a, b) or not_contains(a, b)
*/
void axioms::not_contains_axiom(expr *e) {
throw default_exception("not implemented");
}
expr_ref axioms::length_limit(expr* s, unsigned k) {
expr_ref bound_tracker = m_sk.mk_length_limit(s, k);
expr* s0 = nullptr;

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

@ -113,6 +113,7 @@ namespace seq {
void unit_axiom(expr* n);
void length_axiom(expr* n);
void unroll_not_contains(expr* e);
void not_contains_axiom(expr *e);
void replace_re_axiom(expr* e);
void replace_all_axiom(expr* e);
void replace_re_all_axiom(expr* e);