diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-14 17:02:43 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-14 17:02:43 -0800 |
commit | 2771dce1fe1933537f80d68966642ecf3bf95f77 (patch) | |
tree | c3b4c27aa49657b9ae6b7d115927a2bd81b2bb84 /src/theory/strings/theory_strings.cpp | |
parent | 843ca884a8a6e66b06b1682a60277374ed6d3db4 (diff) | |
parent | a2f04c7859932f03537688eda0e816d8b9b4edc3 (diff) |
Merge remote-tracking branch 'fork/betterSkolems' into cav2019strings
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6905b1c06..c52069a31 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1663,8 +1663,8 @@ void TheoryStrings::checkExtfEval( int effort ) { for (const Node& nrcc : nrc) { sendInternalInference(einfo.d_exp, - einfo.d_const == d_false ? nrcc.negate() : nrcc, - effort == 0 ? "EXTF_d" : "EXTF_d-N"); + einfo.d_const == d_false ? nrcc.negate() : nrcc, + effort == 0 ? "EXTF_d" : "EXTF_d-N"); } }else{ to_reduce = nrc; @@ -3195,7 +3195,6 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal 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"); @@ -3570,11 +3569,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 ) ); @@ -3893,6 +3891,23 @@ void TheoryStrings::registerTerm( Node n, int effort ) { Trace("strings-assert") << "(assert " << lem << ")" << std::endl; d_out->lemma(lem); } + else if (n.getKind() == STRING_STRIDOF) + { + Node lower = n[2]; + if (!TheoryStringsRewriter::checkEntailArith(lower)) { + lower = d_zero; + } + Node neg = Rewriter::rewrite(nm->mkNode(EQUAL, n, d_neg_one)); + Node geq = Rewriter::rewrite(nm->mkNode(GEQ, n, lower)); + Node lem = nm->mkNode(OR, neg, geq); + Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl; + Trace("strings-assert") << "(assert " << lem << ")" << std::endl; + //d_out->lemma(lem); + //d_out->requirePhase(neg, true); + + lem = Rewriter::rewrite(nm->mkNode(GT, nm->mkNode(STRING_LENGTH, n[0]), n)); + d_out->lemma(lem); + } } void TheoryStrings::sendInternalInference(std::vector<Node>& exp, |