diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-23 18:51:53 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-23 18:51:53 -0800 |
| commit | d3c85276c4e7ae06f0c4f2f299c9eda9924358d9 (patch) | |
| tree | 71cd7c2183ebf3b80e2dbae114e4a2c9f3ccdb56 | |
| parent | c3b24d9aa9d7dc80f870fb578e0a27176341fadc (diff) | |
Make skolem depurification an option
| -rw-r--r-- | src/options/strings_options.toml | 9 | ||||
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 4 |
2 files changed, 11 insertions, 2 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 809f48b6d..471a69d71 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -242,6 +242,15 @@ header = "options/strings_options.h" help = "use skolem sharing" [[option]] + name = "skolemDepurification" + category = "expert" + long = "skolem-depurification" + type = "bool" + default = "false" + read_only = true + help = "perform skolem depurification in skolem normalization" + +[[option]] name = "stringRegExpInterMode" category = "expert" long = "re-inter-mode=MODE" diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 81cbd235d..bdfdeb7cd 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -66,7 +66,7 @@ Node SkolemCache::mkTypedSkolemCached( { NodeManager* nm = NodeManager::currentNM(); Node sk; - if (id == SK_PREFIX) + if (options::skolemDepurification() && id == SK_PREFIX) { Node da = depurify(a); Node db = depurify(b); @@ -76,7 +76,7 @@ Node SkolemCache::mkTypedSkolemCached( SK_PURIFY, name, ls); } - else if (id == SK_SUFFIX_REM) + else if (options::skolemDepurification() && id == SK_SUFFIX_REM) { Node da = depurify(a); Node db = depurify(b); |