From 4beb29d45e76145caf8f67255ab442e50ec5c01d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 09:22:12 -0700 Subject: [PATCH] fix #5469 documentation bug --- src/ast/rewriter/seq_axioms.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index edc91e21f..6458e36af 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -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 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) + Symmetric axioms are provided for prefix + */ void axioms::suffix_axiom(expr* e) {