diff options
| -rw-r--r-- | src/options/strings_options.toml | 9 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 17d68b3b7..f30790469 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -252,3 +252,12 @@ header = "options/strings_options.h" default = "true" read_only = true help = "Enable the contains entailment checks in the strings rewriter" + +[[option]] + name = "stringsRewriterMultisetReasoning" + category = "expert" + long = "strings-rewriter-multiset-reasoning" + type = "bool" + default = "true" + read_only = true + help = "Enable multiset reasoning in the strings rewriter" diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f6854b1b4..ac43a2185 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -4413,6 +4413,11 @@ void TheoryStringsRewriter::getArithApproximations(Node a, bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) { + if (!options::stringsRewriterMultisetReasoning()) + { + return false; + } + NodeManager* nm = NodeManager::currentNM(); std::vector<Node> avec; @@ -4499,6 +4504,11 @@ bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a) { + if (!options::stringsRewriterMultisetReasoning()) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); std::vector<Node> avec; |