diff options
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
| -rw-r--r-- | src/theory/strings/skolem_cache.h | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 126ee313d..f0376dbc6 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -107,9 +107,14 @@ class SkolemCache // in_re(a, re.++(_*, b, _*)) => // exists k_pre, k_match, k_post. // a = k_pre ++ k_match ++ k_post ^ - // ~in_re(k_pre ++ substr(k_match, 0, str.len(k_match) - 1), - // re.++(_*, b, _*)) ^ - // in_re(k2, y) + // len(k_pre) = indexof_re(x, y, 0) ^ + // (forall l. 0 < l < len(k_match) => + // ~in_re(substr(k_match, 0, l), r)) ^ + // in_re(k_match, b) + // + // k_pre is the prefix before the first, shortest match of b in a. k_match + // is the substring of a matched by b. It is either empty or there is no + // shorter string that matches b. SK_FIRST_MATCH_PRE, SK_FIRST_MATCH, SK_FIRST_MATCH_POST, @@ -180,6 +185,16 @@ class SkolemCache */ static Node mkIndexVar(Node t); + /** Make length variable + * + * This returns an integer variable of kind BOUND_VARIABLE that is used for + * axiomatizing the behavior of a term or predicate t. It refers to lengths + * of strings in the reduction of t. For example, the length variable for the + * term str.indexof(s, r, n) is used to quantify over the lengths of strings + * that could be matched by r. + */ + static Node mkLengthVar(Node t); + private: /** * Simplifies the arguments for a string skolem used for indexing into the |