diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-12 08:30:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-12 13:30:42 +0000 |
| commit | 111f98a41b488b8124fbecd28dba17465ea30786 (patch) | |
| tree | aaec0192960bdb3e47efc39917c4e2db23ea1f5d /src/theory/strings/skolem_cache.cpp | |
| parent | f41d71cbf1946a5ee5a63c062a23c7426ec5e87d (diff) | |
Ensure sequences of Booleans generate Boolean term variable skolems when applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index eb2df1285..9b23301f3 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -96,8 +96,14 @@ Node SkolemCache::mkTypedSkolemCached( { // exists k. k = a case SK_PURIFY: - sk = sm->mkPurifySkolem(a, c, "string purify skolem"); - break; + { + // for sequences of Booleans, we may purify Boolean terms, in which case + // they must be Boolean term variables. + int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR + : NodeManager::SKOLEM_DEFAULT; + sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags); + } + break; // these are eliminated by normalizeStringSkolem case SK_ID_V_SPT: case SK_ID_V_SPT_REV: |