From b1f63ea4ec9dae7ce38df84f79eb2c212f49778c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 8 Jan 2020 23:59:20 -0800 Subject: skolem hack --- src/theory/strings/theory_strings.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1bc104096..ba59b4e4f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3412,6 +3412,21 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, isRev ? utils::mkNConcat(sk, nfiv[index]) : utils::mkNConcat(nfiv[index], sk)); + Node eqs = d_true; + if (!isRev) + { + sk.eqNode(d_sk_cache.mkSkolemCached( + nfiv[index], + nfjv[index], + SkolemCache::SK_FIRST_CTN_POST, + "v_spt1")) + .orNode(sk.eqNode(d_sk_cache.mkSkolemCached( + nfjv[index], + nfiv[index], + SkolemCache::SK_FIRST_CTN_POST, + "v_spt2"))); + } + if( lentTestSuccess!=-1 ){ info.d_antn.push_back( lentTestExp ); info.d_conc = lentTestSuccess==0 ? eq1 : eq2; @@ -3425,7 +3440,10 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, info.d_antn.push_back(ldeq); } //set info - info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + info.d_conc = nm->mkNode( + AND, + eqs, + NodeManager::currentNM()->mkNode(kind::OR, eq1, eq2)); info.d_id = INFER_SSPLIT_VAR; info_valid = true; } -- cgit v1.2.3