SequencesStatistics& stats)
: d_sc(sc), d_statistics(stats)
{
- //Constants
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
}
StringsPreprocess::~StringsPreprocess(){
}
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
- unsigned prev_new_nodes = new_nodes.size();
- Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl;
+Node StringsPreprocess::reduce(Node t,
+ std::vector<Node>& asserts,
+ SkolemCache* sc)
+{
+ Trace("strings-preprocess-debug")
+ << "StringsPreprocess::reduce: " << t << std::endl;
Node retNode = t;
- NodeManager *nm = NodeManager::currentNM();
+ NodeManager* nm = NodeManager::currentNM();
+ Node zero = nm->mkConst(Rational(0));
+ Node one = nm->mkConst(Rational(1));
+ Node negOne = nm->mkConst(Rational(-1));
if( t.getKind() == kind::STRING_SUBSTR ) {
// processing term: substr( s, n, m )
Node s = t[0];
Node n = t[1];
Node m = t[2];
- Node skt = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
+ Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
Node t12 = nm->mkNode(PLUS, n, m);
t12 = Rewriter::rewrite(t12);
Node lt0 = nm->mkNode(STRING_LENGTH, s);
//start point is greater than or equal zero
- Node c1 = nm->mkNode(GEQ, n, d_zero);
+ Node c1 = nm->mkNode(GEQ, n, zero);
//start point is less than end of string
Node c2 = nm->mkNode(GT, lt0, n);
//length is positive
- Node c3 = nm->mkNode(GT, m, d_zero);
+ Node c3 = nm->mkNode(GT, m, zero);
Node cond = nm->mkNode(AND, c1, c2, c3);
Node emp = Word::mkEmptyWord(t.getType());
- Node sk1 = n == d_zero ? emp
- : d_sc->mkSkolemCached(
- s, n, SkolemCache::SK_PREFIX, "sspre");
- Node sk2 = ArithEntail::check(t12, lt0)
- ? emp
- : d_sc->mkSkolemCached(
- s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
+ Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
+ Node sk2 = 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);
Node b13 = nm->mkNode(
OR,
nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
- nm->mkNode(EQUAL, lsk2, d_zero));
+ nm->mkNode(EQUAL, lsk2, zero));
// Length of the result is at most m
Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
// satisfied. If n + m is less than the length of s, then len(sk2) = 0
// cannot be satisfied because we have the constraint that len(skt) <= m,
// so sk2 must be greater than 0.
- new_nodes.push_back( lemma );
+ asserts.push_back(lemma);
// Thus, substr( s, n, m ) = skt
retNode = skt;
Node x = t[0];
Node y = t[1];
Node n = t[2];
- Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof");
+ Node skk = sc->mkTypedSkolemCached(
+ nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
Node negone = nm->mkConst(Rational(-1));
Node krange = nm->mkNode(GEQ, skk, negone);
// assert: indexof( x, y, n ) >= -1
- new_nodes.push_back( krange );
+ asserts.push_back(krange);
krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk);
// assert: len( x ) >= indexof( x, y, z )
- new_nodes.push_back( krange );
+ asserts.push_back(krange);
// substr( x, n, len( x ) - n )
Node st = nm->mkNode(STRING_SUBSTR,
n,
nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
Node io2 =
- d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
+ sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
Node io4 =
- d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
+ sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
// ~contains( substr( x, n, len( x ) - n ), y )
Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
// n > len( x )
Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x));
// 0 > n
- Node c13 = nm->mkNode(GT, d_zero, n);
+ Node c13 = nm->mkNode(GT, zero, n);
Node cond1 = nm->mkNode(OR, c11, c12, c13);
// skk = -1
Node cc1 = skk.eqNode(negone);
nm->mkNode(
STRING_SUBSTR,
y,
- d_zero,
- nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))),
+ zero,
+ nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))),
y)
.negate();
// skk = n + len( io2 )
// skk = n + len( io2 )
// for fresh io2, io4.
Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3));
- new_nodes.push_back( rr );
+ asserts.push_back(rr);
// Thus, indexof( x, y, n ) = skk.
retNode = skk;
{
// processing term: int.to.str( n )
Node n = t[0];
- Node itost = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
+ Node itost = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
Node leni = nm->mkNode(STRING_LENGTH, itost);
std::vector<Node> conc;
argTypes.push_back(nm->integerType());
Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
- Node lem = nm->mkNode(GEQ, leni, d_one);
+ Node lem = nm->mkNode(GEQ, leni, one);
conc.push_back(lem);
lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
conc.push_back(lem);
- lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
+ lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
conc.push_back(lem);
- Node x = nm->mkBoundVar(nm->integerType());
- Node xPlusOne = nm->mkNode(PLUS, x, d_one);
+ Node x = SkolemCache::mkIndexVar(t);
+ Node xPlusOne = nm->mkNode(PLUS, x, one);
Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
- Node g =
- nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, leni));
- Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one);
+ Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni));
+ Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one);
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
Node ten = nm->mkConst(Rational(10));
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
Node leadingZeroPos =
- nm->mkNode(AND, x.eqNode(d_zero), nm->mkNode(GT, leni, d_one));
+ nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
Node cb = nm->mkNode(
AND,
- nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)),
+ nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, one, zero)),
nm->mkNode(LT, c, ten));
Node ux1lem = nm->mkNode(GEQ, n, ux1);
lem = nm->mkNode(FORALL, xbv, lem);
conc.push_back(lem);
- Node nonneg = nm->mkNode(GEQ, n, d_zero);
+ Node nonneg = nm->mkNode(GEQ, n, zero);
Node emp = Word::mkEmptyWord(t.getType());
lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp));
- new_nodes.push_back(lem);
+ asserts.push_back(lem);
// assert:
// IF n>=0
// THEN:
retNode = itost;
} else if( t.getKind() == kind::STRING_STOI ) {
Node s = t[0];
- Node stoit = nm->mkSkolem("stoit", nm->integerType(), "created for stoi");
+ Node stoit = sc->mkTypedSkolemCached(
+ nm->integerType(), t, SkolemCache::SK_PURIFY, "stoit");
Node lens = nm->mkNode(STRING_LENGTH, s);
std::vector<Node> conc1;
- Node lem = stoit.eqNode(d_neg_one);
+ Node lem = stoit.eqNode(negOne);
conc1.push_back(lem);
Node emp = Word::mkEmptyWord(s.getType());
Node sEmpty = s.eqNode(emp);
Node k = nm->mkSkolem("k", nm->integerType());
- Node kc1 = nm->mkNode(GEQ, k, d_zero);
+ Node kc1 = nm->mkNode(GEQ, k, zero);
Node kc2 = nm->mkNode(LT, k, lens);
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
Node codeSk = nm->mkNode(
MINUS,
- nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)),
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
c0);
Node ten = nm->mkConst(Rational(10));
Node kc3 = nm->mkNode(
- OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten));
+ OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten));
conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
std::vector<Node> conc2;
lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
conc2.push_back(lem);
- lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
+ lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
conc2.push_back(lem);
- lem = nm->mkNode(GT, lens, d_zero);
+ lem = nm->mkNode(GT, lens, zero);
conc2.push_back(lem);
- Node x = nm->mkBoundVar(nm->integerType());
+ Node x = SkolemCache::mkIndexVar(t);
Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
- Node g =
- nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, lens));
- Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one);
+ Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens));
+ Node sx = nm->mkNode(STRING_SUBSTR, s, x, one);
Node ux = nm->mkNode(APPLY_UF, u, x);
- Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one));
+ Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one));
Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
- Node cb =
- nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten));
+ Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
lem = nm->mkNode(FORALL, xbv, lem);
conc2.push_back(lem);
- Node sneg = nm->mkNode(LT, stoit, d_zero);
+ Node sneg = nm->mkNode(LT, stoit, zero);
lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2));
- new_nodes.push_back(lem);
+ asserts.push_back(lem);
// assert:
// IF stoit < 0
Node z = t[2];
TypeNode tn = t[0].getType();
Node rp1 =
- d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
+ sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
Node rp2 =
- d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
- Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
+ sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
+ Node rpw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
// y = ""
Node emp = Word::mkEmptyWord(tn);
rp1,
nm->mkNode(kind::STRING_SUBSTR,
y,
- d_zero,
+ zero,
nm->mkNode(kind::MINUS,
nm->mkNode(kind::STRING_LENGTH, y),
- d_one))),
+ one))),
y)
.negate();
cond2,
nm->mkNode(kind::AND, c21, c22, c23),
rpw.eqNode(x)));
- new_nodes.push_back( rr );
+ asserts.push_back(rr);
// Thus, replace( x, y, z ) = rpw.
retNode = rpw;
Node x = t[0];
Node y = t[1];
Node z = t[2];
- Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
+ Node rpaw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
- Node numOcc = d_sc->mkTypedSkolemCached(
+ Node numOcc = sc->mkTypedSkolemCached(
nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
std::vector<TypeNode> argTypes;
argTypes.push_back(nm->integerType());
Node us =
nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
- Node uf = d_sc->mkTypedSkolemCached(
+ Node uf = sc->mkTypedSkolemCached(
ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x));
std::vector<Node> lem;
- lem.push_back(nm->mkNode(GEQ, numOcc, d_zero));
- lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, d_zero)));
+ lem.push_back(nm->mkNode(GEQ, numOcc, zero));
+ lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero)));
lem.push_back(usno.eqNode(rem));
- lem.push_back(nm->mkNode(APPLY_UF, uf, d_zero).eqNode(d_zero));
- lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(d_neg_one));
+ lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero));
+ lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne));
- Node i = nm->mkBoundVar(nm->integerType());
+ Node i = SkolemCache::mkIndexVar(t);
Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
Node bound =
- nm->mkNode(AND, nm->mkNode(GEQ, i, d_zero), nm->mkNode(LT, i, numOcc));
+ nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
Node ufi = nm->mkNode(APPLY_UF, uf, i);
- Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, d_one));
+ Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi);
Node cc = nm->mkNode(
STRING_CONCAT,
nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
z,
- nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, d_one)));
+ nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
std::vector<Node> flem;
- flem.push_back(ii.eqNode(d_neg_one).negate());
+ flem.push_back(ii.eqNode(negOne).negate());
flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc));
flem.push_back(
ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
Node emp = Word::mkEmptyWord(t.getType());
Node assert =
nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem));
- new_nodes.push_back(assert);
+ asserts.push_back(assert);
// Thus, replaceall( x, y, z ) = rpaw
retNode = rpaw;
else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER)
{
Node x = t[0];
- Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
+ Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
Node lenx = nm->mkNode(STRING_LENGTH, x);
Node lenr = nm->mkNode(STRING_LENGTH, r);
Node eqLenA = lenx.eqNode(lenr);
- Node i = nm->mkBoundVar(nm->integerType());
+ Node i = SkolemCache::mkIndexVar(t);
Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
- Node ci =
- nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one));
- Node ri =
- nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one));
+ Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one));
+ Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one));
Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
ci);
Node bound =
- nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr));
+ nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
Node rangeA =
nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res)));
// str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci)
// where ci = str.code( str.substr(x,i,1) )
Node assert = nm->mkNode(AND, eqLenA, rangeA);
- new_nodes.push_back(assert);
+ asserts.push_back(assert);
// Thus, toLower( x ) = r
retNode = r;
else if (t.getKind() == STRING_REV)
{
Node x = t[0];
- Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
+ Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
Node lenx = nm->mkNode(STRING_LENGTH, x);
Node lenr = nm->mkNode(STRING_LENGTH, r);
Node eqLenA = lenx.eqNode(lenr);
- Node i = nm->mkBoundVar(nm->integerType());
+ Node i = SkolemCache::mkIndexVar(t);
Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
Node revi = nm->mkNode(
- MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, d_one));
- Node ssr = nm->mkNode(STRING_SUBSTR, r, i, d_one);
- Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, d_one);
+ MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
+ Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
+ Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
Node bound =
- nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr));
+ nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
Node rangeA = nm->mkNode(
FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx)));
// assert:
// forall i. 0 <= i < len(r) =>
// substr(r,i,1) = substr(x,len(x)-(i+1),1)
Node assert = nm->mkNode(AND, eqLenA, rangeA);
- new_nodes.push_back(assert);
+ asserts.push_back(assert);
// Thus, (str.rev x) = r
retNode = r;
//negative contains reduces to existential
Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
- Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ Node b1 = SkolemCache::mkIndexVar(t);
Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
- Node body = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ),
- NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ),
- NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s )
- );
+ Node body = NodeManager::currentNM()->mkNode(
+ kind::AND,
+ NodeManager::currentNM()->mkNode(kind::LEQ, zero, b1),
+ NodeManager::currentNM()->mkNode(
+ kind::LEQ,
+ b1,
+ NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)),
+ NodeManager::currentNM()->mkNode(
+ kind::EQUAL,
+ NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
+ s));
retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
}
else if (t.getKind() == kind::STRING_LEQ)
{
- Node ltp = nm->mkSkolem("ltp", nm->booleanType());
+ Node ltp = sc->mkTypedSkolemCached(
+ nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp");
Node k = nm->mkSkolem("k", nm->integerType());
std::vector<Node> conj;
- conj.push_back(nm->mkNode(GEQ, k, d_zero));
+ conj.push_back(nm->mkNode(GEQ, k, zero));
Node substr[2];
Node code[2];
for (unsigned r = 0; r < 2; r++)
{
Node ta = t[r];
Node tb = t[1 - r];
- substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k);
+ substr[r] = nm->mkNode(STRING_SUBSTR, ta, zero, k);
code[r] =
- nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one));
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, one));
conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta)));
}
conj.push_back(substr[0].eqNode(substr[1]));
// ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
Node assert =
nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
- new_nodes.push_back(assert);
+ asserts.push_back(assert);
// Thus, str.<=( x, y ) = ltp
retNode = ltp;
}
+ return retNode;
+}
+Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
+{
+ size_t prev_asserts = asserts.size();
+ // call the static reduce routine
+ Node retNode = reduce(t, asserts, d_sc);
if( t!=retNode ){
Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
- if(!new_nodes.empty()) {
- Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl;
- for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) {
- Trace("strings-preprocess") << " " << new_nodes[i] << std::endl;
+ if (!asserts.empty())
+ {
+ Trace("strings-preprocess")
+ << " ... new nodes (" << (asserts.size() - prev_asserts)
+ << "):" << std::endl;
+ for (size_t i = prev_asserts; i < asserts.size(); ++i)
+ {
+ Trace("strings-preprocess") << " " << asserts[i] << std::endl;
}
}
d_statistics.d_reductions << t.getKind();
return retNode;
}
-Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){
+Node StringsPreprocess::simplifyRec(Node t,
+ std::vector<Node>& asserts,
+ std::map<Node, Node>& visited)
+{
std::map< Node, Node >::iterator it = visited.find(t);
if( it!=visited.end() ){
return it->second;
}else{
Node retNode = t;
if( t.getNumChildren()==0 ){
- retNode = simplify( t, new_nodes );
+ retNode = simplify(t, asserts);
}else if( t.getKind()!=kind::FORALL ){
bool changed = false;
std::vector< Node > cc;
cc.push_back( t.getOperator() );
}
for(unsigned i=0; i<t.getNumChildren(); i++) {
- Node s = simplifyRec( t[i], new_nodes, visited );
+ Node s = simplifyRec(t[i], asserts, visited);
cc.push_back( s );
if( s!=t[i] ) {
changed = true;
if( changed ){
tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
}
- retNode = simplify( tmp, new_nodes );
+ retNode = simplify(tmp, asserts);
}
visited[t] = retNode;
return retNode;
}
}
-Node StringsPreprocess::processAssertion( Node n, std::vector< Node > &new_nodes ) {
+Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
+{
std::map< Node, Node > visited;
- std::vector< Node > new_nodes_curr;
- Node ret = simplifyRec( n, new_nodes_curr, visited );
- while( !new_nodes_curr.empty() ){
- Node curr = new_nodes_curr.back();
- new_nodes_curr.pop_back();
- std::vector< Node > new_nodes_tmp;
- curr = simplifyRec( curr, new_nodes_tmp, visited );
- new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() );
- new_nodes.push_back( curr );
+ std::vector<Node> asserts_curr;
+ Node ret = simplifyRec(n, asserts_curr, visited);
+ while (!asserts_curr.empty())
+ {
+ Node curr = asserts_curr.back();
+ asserts_curr.pop_back();
+ std::vector<Node> asserts_tmp;
+ curr = simplifyRec(curr, asserts_tmp, visited);
+ asserts_curr.insert(
+ asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
+ asserts.push_back(curr);
}
return ret;
}
for( unsigned i=0; i<vec_node.size(); i++ ){
Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl;
//preprocess until fixed point
- std::vector< Node > new_nodes;
- std::vector< Node > new_nodes_curr;
- new_nodes_curr.push_back( vec_node[i] );
- while( !new_nodes_curr.empty() ){
- Node curr = new_nodes_curr.back();
- new_nodes_curr.pop_back();
- std::vector< Node > new_nodes_tmp;
- curr = simplifyRec( curr, new_nodes_tmp, visited );
- new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() );
- new_nodes.push_back( curr );
+ std::vector<Node> asserts;
+ std::vector<Node> asserts_curr;
+ asserts_curr.push_back(vec_node[i]);
+ while (!asserts_curr.empty())
+ {
+ Node curr = asserts_curr.back();
+ asserts_curr.pop_back();
+ std::vector<Node> asserts_tmp;
+ curr = simplifyRec(curr, asserts_tmp, visited);
+ asserts_curr.insert(
+ asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
+ asserts.push_back(curr);
}
- Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+ Node res = asserts.size() == 1
+ ? asserts[0]
+ : NodeManager::currentNM()->mkNode(kind::AND, asserts);
if( res!=vec_node[i] ){
res = Rewriter::rewrite( res );
PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); );
projects / cvc5.git / commitdiff