From: Andrew Reynolds Date: Tue, 18 Sep 2018 20:38:44 +0000 (-0500) Subject: More aggressive caching of string skolems. (#2491) X-Git-Tag: cvc5-1.0.0~4632 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e574c859c7f741fc0f4608471afaa5aaac892089;p=cvc5.git More aggressive caching of string skolems. (#2491) --- diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 2d5bef519..ba6caaf79 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -22,6 +22,7 @@ #include "options/strings_options.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" +#include "theory/strings/theory_strings_rewriter.h" using namespace CVC4; using namespace CVC4::kind; @@ -66,9 +67,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node c3 = nm->mkNode(GT, m, d_zero); Node cond = nm->mkNode(AND, c1, c2, c3); - Node sk1 = d_sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); - Node sk2 = - d_sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); + Node sk1 = n == d_zero ? d_empty_str + : d_sc->mkSkolemCached( + s, n, SkolemCache::SK_PREFIX, "sspre"); + Node sk2 = TheoryStringsRewriter::checkEntailArith(t12, lt0) + ? d_empty_str + : d_sc->mkSkolemCached( + s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2)); //length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); @@ -97,62 +102,63 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { else if (t.getKind() == kind::STRING_STRIDOF) { // processing term: indexof( x, y, n ) + Node x = t[0]; + Node y = t[1]; + Node n = t[2]; Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof"); - Node negone = nm->mkConst(::CVC4::Rational(-1)); - Node krange = nm->mkNode(kind::GEQ, skk, negone); + Node negone = nm->mkConst(Rational(-1)); + Node krange = nm->mkNode(GEQ, skk, negone); // assert: indexof( x, y, n ) >= -1 new_nodes.push_back( krange ); - krange = nm->mkNode(kind::GEQ, nm->mkNode(kind::STRING_LENGTH, t[0]), skk); + krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk); // assert: len( x ) >= indexof( x, y, z ) new_nodes.push_back( krange ); // substr( x, n, len( x ) - n ) - Node st = nm->mkNode( - kind::STRING_SUBSTR, - t[0], - t[2], - nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, t[0]), t[2])); - Node io2 = nm->mkSkolem("io2", nm->stringType(), "created for indexof"); - Node io4 = nm->mkSkolem("io4", nm->stringType(), "created for indexof"); + Node st = nm->mkNode(STRING_SUBSTR, + x, + n, + nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n)); + Node io2 = + d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); + Node io4 = + d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); // ~contains( substr( x, n, len( x ) - n ), y ) - Node c11 = nm->mkNode(kind::STRING_STRCTN, st, t[1]).negate(); + Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate(); // n > len( x ) - Node c12 = - nm->mkNode(kind::GT, t[2], nm->mkNode(kind::STRING_LENGTH, t[0])); + Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x)); // 0 > n - Node c13 = nm->mkNode(kind::GT, d_zero, t[2]); - Node cond1 = nm->mkNode(kind::OR, c11, c12, c13); + Node c13 = nm->mkNode(GT, d_zero, n); + Node cond1 = nm->mkNode(OR, c11, c12, c13); // skk = -1 Node cc1 = skk.eqNode(negone); // y = "" - Node cond2 = t[1].eqNode(nm->mkConst(CVC4::String(""))); + Node cond2 = y.eqNode(d_empty_str); // skk = n Node cc2 = skk.eqNode(t[2]); // substr( x, n, len( x ) - n ) = str.++( io2, y, io4 ) - Node c31 = st.eqNode(nm->mkNode(kind::STRING_CONCAT, io2, t[1], io4)); + Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4)); // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) Node c32 = nm->mkNode( - kind::STRING_STRCTN, + STRING_STRCTN, nm->mkNode( - kind::STRING_CONCAT, + STRING_CONCAT, io2, - nm->mkNode(kind::STRING_SUBSTR, - t[1], - d_zero, - nm->mkNode(kind::MINUS, - nm->mkNode(kind::STRING_LENGTH, t[1]), - d_one))), - t[1]) + nm->mkNode( + STRING_SUBSTR, + y, + d_zero, + nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))), + y) .negate(); // skk = n + len( io2 ) - Node c33 = skk.eqNode( - nm->mkNode(kind::PLUS, t[2], nm->mkNode(kind::STRING_LENGTH, io2))); - Node cc3 = nm->mkNode(kind::AND, c31, c32, c33); + Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2))); + Node cc3 = nm->mkNode(AND, c31, c32, c33); // assert: // IF: ~contains( substr( x, n, len( x ) - n ), y ) OR n > len(x) OR 0 > n @@ -163,8 +169,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^ // skk = n + len( io2 ) // for fresh io2, io4. - Node rr = nm->mkNode( - kind::ITE, cond1, cc1, nm->mkNode(kind::ITE, cond2, cc2, cc3)); + Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3)); new_nodes.push_back( rr ); // Thus, indexof( x, y, n ) = skk. @@ -174,7 +179,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0]))); Node num = t[0]; - Node pret = nm->mkSkolem("itost", nm->stringType(), "created for itos"); + Node pret = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost"); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);