Remove `--strings-binary-csp` option (#3743)

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 3916c68f32ede6f4aa7094f9368ac091ba76b234..f51c4ce679f7d01b5e07dbe417f4805b995bb6d3 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -189,15 +189,6 @@ header = "options/strings_options.h"
   read_only  = true
   help       = "use model guessing to avoid string extended function reductions"
 
-[[option]]
-  name       = "stringBinaryCsp"
-  category   = "regular"
-  long       = "strings-binary-csp"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "use binary search when splitting strings"
-
 [[option]]
   name       = "stringLenPropCsp"
   category   = "regular"

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index acf127df3d258a471f9c8b1ec6b06b9ab5d3e14f..c27304dc823bf61a8f2585ca3ceb4ce5da817f17 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -116,23 +116,13 @@ void CoreSolver::checkCycles()
   d_eqc.clear();
   // Rebuild strings eqc based on acyclic ordering, first copy the equivalence
   // classes from the base solver.
-  std::vector< Node > eqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& eqc = d_bsolver.getStringEqc();
   d_strings_eqc.clear();
-  if( options::stringBinaryCsp() ){
-    //sort: process smallest constants first (necessary if doing binary splits)
-    sortConstLength scl;
-    for( unsigned i=0; i<eqc.size(); i++ ){
-      Node ci = d_bsolver.getConstantEqc(eqc[i]);
-      if( !ci.isNull() ){
-        scl.d_const_length[eqc[i]] = ci.getConst<String>().size();
-      }
-    }
-    std::sort( eqc.begin(), eqc.end(), scl );
-  }
-  for( unsigned i=0; i<eqc.size(); i++ ){
+  for (const Node& r : eqc)
+  {
     std::vector< Node > curr;
     std::vector< Node > exp;
-    checkCycles( eqc[i], curr, exp );
+    checkCycles(r, curr, exp);
     if (d_im.hasProcessed())
     {
       return;
@@ -1380,47 +1370,13 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           }
         }
 
-        Node const_str = nfcv[index];
-        NormalForm::getExplanationForPrefixEq(
-            nfi, nfj, index, index, info.d_ant);
-        CVC4::String stra = const_str.getConst<String>();
-        if (options::stringBinaryCsp() && stra.size() > 3)
-        {
-          // If binary constant splits are enabled, we essentially perform a
-          // binary search over how much overlap the constant has with `nc`.
-          //
-          // E.g. "abcdef" ++ ... = nc ++ ... ---> (nc = "abc" ++ k) v
-          //      (k != "" ^ "abc" = nc ++ k)
-          Node firstHalf = nm->mkConst(isRev ? stra.substr(stra.size() / 2)
-                                             : stra.substr(0, stra.size() / 2));
-          Node sk =
-              d_skCache.mkSkolemCached(nc,
-                                       firstHalf,
-                                       isRev ? SkolemCache::SK_ID_VC_BIN_SPT_REV
-                                             : SkolemCache::SK_ID_VC_BIN_SPT,
-                                       "cb_spt");
-          Trace("strings-csp")
-              << "Const Split: " << firstHalf << " is removed from "
-              << const_str << " (binary) " << std::endl;
-          info.d_conc = nm->mkNode(
-              OR,
-              nc.eqNode(isRev ? utils::mkNConcat(sk, firstHalf)
-                              : utils::mkNConcat(firstHalf, sk)),
-              nm->mkNode(AND,
-                         sk.eqNode(d_emptyString).negate(),
-                         firstHalf.eqNode(isRev ? utils::mkNConcat(sk, nc)
-                                                : utils::mkNConcat(nc, sk))));
-          info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
-          info.d_id = INFER_SSPLIT_CST_BINARY;
-          pinfer.push_back(info);
-          break;
-        }
-
         // Since non of the other inferences apply, we just infer that `nc` has
         // to start with the first character of the constant.
         //
         // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
-        Node firstChar = stra.size() == 1 ? const_str
+        Node constStr = nfcv[index];
+        CVC4::String stra = constStr.getConst<String>();
+        Node firstChar = stra.size() == 1 ? constStr
                                           : nm->mkConst(isRev ? stra.suffix(1)
                                                               : stra.prefix(1));
         Node sk = d_skCache.mkSkolemCached(
@@ -1428,8 +1384,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
             isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
             "c_spt");
         Trace("strings-csp")
-            << "Const Split: " << firstChar << " is removed from " << const_str
+            << "Const Split: " << firstChar << " is removed from " << constStr
             << " (serial) " << std::endl;
+        NormalForm::getExplanationForPrefixEq(
+            nfi, nfj, index, index, info.d_ant);
         info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
                                       : utils::mkNConcat(firstChar, sk));
         info.d_new_skolem[LENGTH_SPLIT].push_back(sk);

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index b2c88d06871a8dfc254c30dd7926786329b21122..e15ee984d9747e9d01323a58d44834920f2cb061 100644 (file)
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -29,7 +29,6 @@ std::ostream& operator<<(std::ostream& out, Inference i)
     case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
     case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
     case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
-    case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
     case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
     case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
     case INFER_FLOOP: out << "F-Loop"; break;

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 0f0329e61f7f756e1788521db3e497a9f47eec02..b98b4fbf2657058d377dbe7799aebde6a7589c58 100644 (file)
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -57,11 +57,6 @@ enum Inference
   //     z = "" V z != ""
   // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
   INFER_LEN_SPLIT_EMP,
-  // string split constant binary, for example:
-  //     x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
-  // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
-  // This inference is disabled by default and is enabled by stringBinaryCsp().
-  INFER_SSPLIT_CST_BINARY,
   // string split constant
   //    x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
   //      implies y1 = "c" ++ y1'

diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index c1e3c721440225d0a3bd09e4915ff7c372bff2bf..8fcf46c14532c3fd53bab354127bfdf954038b87 100644 (file)
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -59,10 +59,6 @@ class SkolemCache
     //    exists k. a = "c" ++ k
     SK_ID_VC_SPT,
     SK_ID_VC_SPT_REV,
-    // a != "" ^ b = "cccccccc" ^ len(a)!=len(b) a ++ a' = b = b' =>
-    //    exists k. a = "cccc" ++ k OR ( len(k) > 0 ^ "cccc" = a ++ k )
-    SK_ID_VC_BIN_SPT,
-    SK_ID_VC_BIN_SPT_REV,
     // a != "" ^ b != "" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' =>
     //    exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k )
     SK_ID_V_SPT,