Add option for stripping constant endpoints, fixing entail contains checks

2 files changed, 19 insertions, 0 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index f30790469..ab32ddbec 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -261,3 +261,12 @@ header = "options/strings_options.h"
   default    = "true"
   read_only  = true
   help       = "Enable multiset reasoning in the strings rewriter"
+
+[[option]]
+  name       = "stringsRewriterStripConstantEndpoints"
+  category   = "expert"
+  long       = "strings-rewriter-strip-constant-endpoints"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "Enable stripping of constant endpoints"
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index ac43a2185..b5ef65f40 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3318,6 +3318,11 @@ int TheoryStringsRewriter::componentContains(std::vector<Node>& n1,
                                              bool computeRemainder,
                                              int remainderDir)
 {
+  if (!options::stringsRewriterEntailContainsChecks())
+  {
+    return -1;
+  }
+
   Assert(nb.empty());
   Assert(ne.empty());
   // if n2 is a singleton, we can do optimized version here
@@ -3584,6 +3589,11 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
                                                    std::vector<Node>& ne,
                                                    int dir)
 {
+  if (options::stringsRewriterStripConstantEndpoints())
+  {
+    return false;
+  }
+
   Assert(nb.empty());
   Assert(ne.empty());
   bool changed = false;