diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-27 15:42:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-27 22:42:10 +0000 |
commit | 29f0b8f378377ed836bddaaf88883d0b2eeb545d (patch) | |
tree | 5d9edb57c60ab8c8a07dab52f18b72dd441d4fdf /src/theory/strings/skolem_cache.cpp | |
parent | 631032b15327c28c44b51490dceb434a38f3419a (diff) |
Fix `str.replace_re` and `str.replace_re_all` (#6615)
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 9b23301f3..913518bc8 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -40,6 +40,16 @@ struct IndexVarAttributeId }; typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute; +/** + * A bound variable corresponding to the universally quantified integer + * variable used to range over the valid lengths of a string, used for + * axiomatizing the behavior of some term. + */ +struct LengthVarAttributeId +{ +}; +typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute; + SkolemCache::SkolemCache(bool useOpts) : d_useOpts(useOpts) { NodeManager* nm = NodeManager::currentNM(); @@ -300,6 +310,14 @@ Node SkolemCache::mkIndexVar(Node t) return bvm->mkBoundVar<IndexVarAttribute>(t, intType); } +Node SkolemCache::mkLengthVar(Node t) +{ + NodeManager* nm = NodeManager::currentNM(); + TypeNode intType = nm->integerType(); + BoundVarManager* bvm = nm->getBoundVarManager(); + return bvm->mkBoundVar<LengthVarAttribute>(t, intType); +} + } // namespace strings } // namespace theory } // namespace cvc5 |