diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-18 10:04:08 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-18 10:04:08 -0700 |
commit | 073335156ff7644364d12a91d4d41af776cfb91b (patch) | |
tree | 3c541683c11b132f168198b0f5c95ccd52df74da /src/theory/strings/theory_strings.cpp | |
parent | f6a2704f9e35f72c7e682fa71a3f64e79dd4e9e3 (diff) |
Strings: More aggressive skolem normalization (#2761)
This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d37d4f904..cea3c3515 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3289,7 +3289,6 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, Node firstChar = stra.size() == 1 ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( 1 ) : stra.prefix( 1 ) ); Node sk = d_sk_cache.mkSkolemCached( other_str, - firstChar, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, "c_spt"); @@ -3687,11 +3686,10 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = d_sk_cache.mkSkolemCached( - nconst_k, firstChar, SkolemCache::SK_ID_DC_SPT, "dc_spt"); + nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); registerLength(sk, LENGTH_ONE); Node skr = d_sk_cache.mkSkolemCached(nconst_k, - firstChar, SkolemCache::SK_ID_DC_SPT_REM, "dc_spt_rem"); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); |