mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #5469 documentation bug

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-10 09:22:12 -07:00
parent 22bb4c2db7
commit 4beb29d45e
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1043,12 +1043,19 @@ namespace seq {
} }
/** /**
suffix(s, t):
- the sequence s is a suffix of t.
suffix(s, t) => s = seq.suffix_inv(s, t) + t Positive case is handled by the solver when the atom is asserted
suffix(s, t) => t = seq.suffix_inv(s, t) + s
Negative case is handled by axioms when the negation of the atom is asserted
~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t) ~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t)
~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t) ~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t)
~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t) ~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t)
Symmetric axioms are provided for prefix
*/ */
void axioms::suffix_axiom(expr* e) { void axioms::suffix_axiom(expr* e) {