From 79db74b6976354141e2cee776d07a47f5c2af423 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 8 Jul 2022 22:27:40 -0700 Subject: [PATCH] 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 ``` --- src/options/strings_options.toml | 8 ---- src/theory/strings/core_solver.cpp | 67 ++++++++++-------------------- 2 files changed, 21 insertions(+), 54 deletions(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 7407bcdf1..423b4f153 100644 --- 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 99aac3815..2531e6f3e 100644 --- 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) { -- 2.30.2