diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-07 18:16:54 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-21 02:25:18 -0800 |
| commit | 25fb40b39d7edc66681fb22156597ac070162b1b (patch) | |
| tree | 3b0737f24beabcc750aaab21751c57a1d37c1f80 | |
| parent | c3bc4ac99c36029b78d866ffb89bd0d322821f34 (diff) | |
Add option to toggle skolem sharing
| -rw-r--r-- | src/options/strings_options.toml | 9 | ||||
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 3 |
2 files changed, 11 insertions, 1 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3916c68f3..809f48b6d 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -233,6 +233,15 @@ header = "options/strings_options.h" help = "do flat form inferences" [[option]] + name = "skolemSharing" + category = "expert" + long = "skolem-sharing" + type = "bool" + default = "true" + read_only = true + help = "use skolem sharing" + +[[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 b4e1c74ea..98ceeadc2 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -14,6 +14,7 @@ #include "theory/strings/skolem_cache.h" +#include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "util/rational.h" @@ -53,7 +54,7 @@ Node SkolemCache::mkTypedSkolemCached( } std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); - if (it == d_skolemCache[a][b].end()) + if (!options::skolemSharing() || it == d_skolemCache[a][b].end()) { Node sk = mkTypedSkolem(tn, c); d_skolemCache[a][b][id] = sk; |