From 36f4f6b75bd13b7770e6113ed5c2f9b2b895e0ba Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 11 Feb 2020 06:27:29 -0800 Subject: [PATCH] Remove `--strings-binary-csp` option (#3743) --- src/options/strings_options.toml | 9 ----- src/theory/strings/core_solver.cpp | 62 +++++------------------------- src/theory/strings/infer_info.cpp | 1 - src/theory/strings/infer_info.h | 5 --- src/theory/strings/skolem_cache.h | 4 -- 5 files changed, 10 insertions(+), 71 deletions(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3916c68f3..f51c4ce67 100644 --- 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 acf127df3..c27304dc8 100644 --- 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& 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().size(); - } - } - std::sort( eqc.begin(), eqc.end(), scl ); - } - for( unsigned i=0; i 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(); - 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(); + 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 b2c88d068..e15ee984d 100644 --- 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 0f0329e61..b98b4fbf2 100644 --- 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 c1e3c7214..8fcf46c14 100644 --- 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, -- 2.30.2