add options

3 files changed, 45 insertions, 1 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 3544c37fe..414a9cfa6 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -224,3 +224,30 @@ header = "options/strings_options.h"
   default    = "true"
   read_only  = true
   help       = "do flat form inferences"
+
+[[option]]
+  name       = "stringsCacheSkolems"
+  category   = "expert"
+  long       = "strings-cache-skolems"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "Cache skolems in string reductions"
+
+[[option]]
+  name       = "stringsNormalizeSkolems"
+  category   = "expert"
+  long       = "strings-normalize-skolems"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "Normalize string skolems before looking them up in the cache"
+
+[[option]]
+  name       = "stringsRewriterEntailChecks"
+  category   = "expert"
+  long       = "strings-rewriter-entail-checks"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "Enable the entailment checks in the strings rewriter"
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index b6604d6e0..53ec3c368 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"
@@ -42,6 +43,13 @@ Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
 Node SkolemCache::mkTypedSkolemCached(
     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
 {
+  if (!options::stringsCacheSkolems())
+  {
+    Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
+    d_allSkolems.insert(n);
+    return n;
+  }
+
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
 
@@ -87,6 +95,11 @@ bool SkolemCache::isSkolem(Node n) const
 std::tuple<SkolemCache::SkolemId, Node, Node>
 SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 {
+  if (!options::stringsNormalizeSkolems())
+  {
+    return std::make_tuple(id, a, b);
+  }
+
   Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 0de42f686..23d20c4c7 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -4010,6 +4010,10 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict)
     return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
   }
 
+  if (!options::stringsRewriterEntailChecks()) {
+    return false;
+  }
+
   Node ar =
       strict
           ? NodeManager::currentNM()->mkNode(
@@ -4659,7 +4663,7 @@ Node TheoryStringsRewriter::getConstantArithBound(Node a, bool isLower)
       ret = NodeManager::currentNM()->mkConst(Rational(0));
     }
   }
-  else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
+  else if (options::stringsRewriterEntailChecks() && (a.getKind() == kind::PLUS || a.getKind() == kind::MULT))
   {
     std::vector<Node> children;
     bool success = true;