diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 22:53:55 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 22:53:55 -0800 |
| commit | 52b67c2ce7bfeeedb3ca2d1934e19140c9fe5f97 (patch) | |
| tree | e4b51eb87d81eb8068e1505f7b7d720c5d019024 | |
| parent | 29badd153b7ece62ff18d5545ed8054389e79a77 (diff) | |
SK_ID_DC_SPT_REM > 0
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index becf66ada..5015207f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3770,6 +3770,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { d_sk_cache.mkSkolemCached(nconst_k, SkolemCache::SK_ID_DC_SPT_REM, "dc_spt_rem"); + d_im.registerLength(skr, LENGTH_GEQ_ONE); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); eq1 = Rewriter::rewrite( eq1 ); Node eq2 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, skr ) ); @@ -3779,14 +3780,10 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { antec.insert( antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); antec.push_back( nconst_k.eqNode( d_emptyString ).negate() ); - d_im.sendInference( - antec, - nm->mkNode( - OR, - nm->mkNode(AND, eq1, sk.eqNode(firstChar).negate()), - eq2), - "D-DISL-CSplit"); - d_im.sendPhaseRequirement(eq1, true); + d_im.sendInference(antec, + nm->mkNode(OR, nconst_k.eqNode(sk), eq1), + "D-DISL-CSplit"); + d_im.sendSplit(firstChar, sk, "S-Split(DEQL-Const)", false); return; } } |