Remove `--strings-unified-vspt` option (#8947)

This option was enabled by default and this commit enables it
permanently. Overall, the results (300s timeout) seem to indicate that
the option does not have a significant impact on performance (and is a
bit worse overall):

```
                                status  total  solved    sat  unsat   best  timeout  memout  error  uniq  disagr  time_cpu   memory
config
2022-07-07-strings-main-no-vspt     ok  69984   69513  42755  26758  65940      468       0      1    12       0  175814.9 456860.9
2022-07-07-strings-main-vspt        ok  69984   69509  42750  26759  65097      472       0      1     8       0  174975.7 456793.6
```

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 7407bcdf1802a4f7efbe434fd9f0f4f28b1ea252..423b4f1531c980524e05964a930e3f4999ad2147 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -160,14 +160,6 @@ name   = "Strings Theory"
   name = "none"
   help = "Do not compute intersections for regular expressions."
 
-[[option]]
-  name       = "stringUnifiedVSpt"
-  category   = "expert"
-  long       = "strings-unified-vspt"
-  type       = "bool"
-  default    = "true"
-  help       = "use a single skolem for the variable splitting rule"
-
 [[option]]
   name       = "stringEagerEval"
   category   = "regular"

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 99aac3815b4e5eeda4746aa1edb90c2a03f46e8d..2531e6f3eb5c622e4ffa81fcaa05fdee69ad8afd 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -706,39 +706,17 @@ Node CoreSolver::getConclusion(Node x,
   Node conc;
   if (rule == PfRule::CONCAT_SPLIT || rule == PfRule::CONCAT_LPROP)
   {
-    Node sk1;
-    Node sk2;
-    if (options::stringUnifiedVSpt())
-    {
-      // must compare so that we are agnostic to order of x/y
-      Node ux = x < y ? x : y;
-      Node uy = x < y ? y : x;
-      Node sk = skc->mkSkolemCached(ux,
-                                    uy,
-                                    isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
-                                          : SkolemCache::SK_ID_V_UNIFIED_SPT,
-                                    "v_spt");
-      newSkolems.push_back(sk);
-      sk1 = sk;
-      sk2 = sk;
-    }
-    else
-    {
-      sk1 = skc->mkSkolemCached(
-          x,
-          y,
-          isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT,
-          "v_spt1");
-      sk2 = skc->mkSkolemCached(
-          y,
-          x,
-          isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT,
-          "v_spt2");
-      newSkolems.push_back(sk1);
-      newSkolems.push_back(sk2);
-    }
-    Node eq1 = x.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk1, y)
-                              : nm->mkNode(STRING_CONCAT, y, sk1));
+    // must compare so that we are agnostic to order of x/y
+    Node ux = x < y ? x : y;
+    Node uy = x < y ? y : x;
+    Node sk = skc->mkSkolemCached(ux,
+                                  uy,
+                                  isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
+                                        : SkolemCache::SK_ID_V_UNIFIED_SPT,
+                                  "v_spt");
+    newSkolems.push_back(sk);
+    Node eq1 = x.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk, y)
+                              : nm->mkNode(STRING_CONCAT, y, sk));
 
     if (rule == PfRule::CONCAT_LPROP)
     {
@@ -746,22 +724,19 @@ Node CoreSolver::getConclusion(Node x,
     }
     else
     {
-      Node eq2 = y.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk2, x)
-                                : nm->mkNode(STRING_CONCAT, x, sk2));
+      Node eq2 = y.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk, x)
+                                : nm->mkNode(STRING_CONCAT, x, sk));
       // make agnostic to x/y
       conc = x < y ? nm->mkNode(OR, eq1, eq2) : nm->mkNode(OR, eq2, eq1);
     }
-    if (options::stringUnifiedVSpt())
-    {
-      // we can assume its length is greater than zero
-      Node emp = Word::mkEmptyWord(sk1.getType());
-      conc = nm->mkNode(
-          AND,
-          conc,
-          sk1.eqNode(emp).negate(),
-          nm->mkNode(
-              GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConstInt(Rational(0))));
-    }
+    // we can assume its length is greater than zero
+    Node emp = Word::mkEmptyWord(sk.getType());
+    conc = nm->mkNode(
+        AND,
+        conc,
+        sk.eqNode(emp).negate(),
+        nm->mkNode(
+            GT, nm->mkNode(STRING_LENGTH, sk), nm->mkConstInt(Rational(0))));
   }
   else if (rule == PfRule::CONCAT_CSPLIT)
   {