return "TRANSCENDENTAL_PURIFY_ARG";
case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
- case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
case SkolemFunId::STRINGS_NUM_OCCUR: return "STRINGS_NUM_OCCUR";
case SkolemFunId::STRINGS_OCCUR_INDEX: return "STRINGS_OCCUR_INDEX";
case SkolemFunId::STRINGS_OCCUR_LEN: return "STRINGS_OCCUR_LEN";
SELECTOR_WRONG,
/** a shared selector */
SHARED_SELECTOR,
- /** an application of seq.nth that is out of bounds */
- SEQ_NTH_OOB,
//----- string skolems are cached based on two strings (a, b)
/** exists k. ( b occurs k times in a ) */
STRINGS_NUM_OCCUR,
for (Node j : indexes)
{
// nth(x, m)
- // y = update(s, n, t), m)
+ // y = update(s, n, t)
// x = y or x = s
// ------------------------
// nth(update(s, n, t)) =
// ite(0 <= m < len(s),
// ite(n = m, nth(t, 0), nth(s, m)),
- // Uf(update(s, n, t), m))
+ // nth(update(s, n, t), m))
Node nth = nm->mkNode(SEQ_NTH, termProxy, j);
Node nthInBounds =
nm->mkNode(AND,
Node updateVal = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(0));
Node iteNthInBounds = nm->mkNode(
ITE, i.eqNode(j), updateVal, nm->mkNode(SEQ_NTH, n[0], j));
- Node uf = SkolemCache::mkSkolemSeqNth(n[0].getType(), "Uf");
- Node ufj = nm->mkNode(APPLY_UF, uf, n, j);
- Node rhs = nm->mkNode(ITE, nthInBounds, iteNthInBounds, ufj);
+ Node rhs = nm->mkNode(ITE, nthInBounds, iteNthInBounds, nth);
Node lem = nth.eqNode(rhs);
std::vector<Node> exp;
Trace("seq-array-debug") << "...unit case" << std::endl;
// do we know whether n = 0 ?
// x = (seq.unit m) => (seq.update x n z) = ite(n=0, z, (seq.unit m))
- // x = (seq.unit m) => (seq.nth x n) = ite(n=0, m, Uf(x, n))
- Node thenBranch;
- Node elseBranch;
+ // x = (seq.unit m) ^ n=0 => (seq.nth x n) = m
InferenceId iid;
+ Node eq;
+ std::vector<Node> exp;
+ std::vector<Node> nexp;
+ d_im.addToExplanation(t[0], nf.d_nf[0], exp);
+ d_im.addToExplanation(r, t[0], exp);
if (k == STRING_UPDATE)
{
- thenBranch = t[2];
- elseBranch = nf.d_nf[0];
iid = InferenceId::STRINGS_ARRAY_UPDATE_UNIT;
+ eq = nm->mkNode(
+ ITE, t[1].eqNode(d_zero), t.eqNode(t[2]), t.eqNode(nf.d_nf[0]));
}
else
{
Assert(k == SEQ_NTH);
+ Node val;
if (ck == CONST_SEQUENCE)
{
const Sequence& seq = nf.d_nf[0].getConst<Sequence>();
- thenBranch = seq.getVec()[0];
+ val = seq.getVec()[0];
}
else
{
- thenBranch = nf.d_nf[0][0];
+ val = nf.d_nf[0][0];
}
- Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf");
- elseBranch = nm->mkNode(APPLY_UF, uf, t[0], t[1]);
iid = InferenceId::STRINGS_ARRAY_NTH_UNIT;
+ eq = t.eqNode(val);
+ if (t[1] != d_zero)
+ {
+ exp.push_back(t[1].eqNode(d_zero));
+ nexp.push_back(t[1].eqNode(d_zero));
+ }
}
- std::vector<Node> exp;
- d_im.addToExplanation(t[0], nf.d_nf[0], exp);
- d_im.addToExplanation(r, t[0], exp);
- Node eq = nm->mkNode(ITE,
- t[1].eqNode(d_zero),
- t.eqNode(thenBranch),
- t.eqNode(elseBranch));
if (d_eqProc.find(eq) == d_eqProc.end())
{
d_eqProc.insert(eq);
- d_im.sendInference(exp, eq, iid);
+ d_im.sendInference(exp, nexp, eq, iid);
}
return;
}
// z = (seq.++ x y) =>
// (seq.update z n l) =
// (seq.++ (seq.update x n 1) (seq.update y (- n len(x)) 1))
- // z = (seq.++ x y) =>
+ // z = (seq.++ x y) ^ (>= n 0) ^ (< n (+ (str.len x) (str.len y)))) =>
// (seq.nth z n) =
- // (ite (or (< n 0) (>= n (+ (str.len x) (str.len y)))) (Uf z n)
// (ite (< n (str.len x)) (seq.nth x n)
- // (seq.nth y (- n (str.len x)))))
+ // (seq.nth y (- n (str.len x))))
InferenceId iid;
+ std::vector<Node> exp;
+ std::vector<Node> nexp;
Node eq;
if (k == STRING_UPDATE)
{
{
std::reverse(cchildren.begin(), cchildren.end());
std::reverse(cond.begin(), cond.end());
- Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf");
eq = t.eqNode(cchildren[0]);
for (size_t i = 1, ncond = cond.size(); i < ncond; i++)
{
eq = nm->mkNode(ITE, cond[i], t.eqNode(cchildren[i]), eq);
}
- Node ufa = nm->mkNode(APPLY_UF, uf, t[0], t[1]);
- Node oobCond =
- nm->mkNode(OR, nm->mkNode(LT, t[1], d_zero), cond[0].notNode());
- eq = nm->mkNode(ITE, oobCond, t.eqNode(ufa), eq);
+ Node inBoundsCond = nm->mkNode(AND, nm->mkNode(GEQ, t[1], d_zero), cond[0]);
+ exp.push_back(inBoundsCond);
+ nexp.push_back(inBoundsCond);
iid = InferenceId::STRINGS_ARRAY_NTH_CONCAT;
}
- std::vector<Node> exp;
if (checkInv)
{
NormalForm& nfSelf = d_csolver.getNormalForm(rself);
{
d_eqProc.insert(eq);
Trace("seq-array") << "- send lemma - " << eq << std::endl;
- d_im.sendInference(exp, eq, iid);
+ d_im.sendInference(exp, nexp, eq, iid);
}
}
return mkTypedSkolemCached(tn, a, Node::null(), id, c);
}
-Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
-{
- // Note this method is static and does not rely on any local caching.
- // It is used by expand definitions and by (dynamic) reductions, thus
- // it is centrally located here.
- Assert(seqType.isSequence());
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- std::vector<TypeNode> argTypes;
- argTypes.push_back(seqType);
- argTypes.push_back(nm->integerType());
- TypeNode elemType = seqType.getSequenceElementType();
- TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
- return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
-}
-
Node SkolemCache::mkSkolem(const char* c)
{
// TODO: eliminate this
TypeNode tn, Node a, Node b, SkolemId id, const char* c);
/** Same as mkTypedSkolemCached above for (a,[null],id) */
Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
- /**
- * Specific version for seq.nth, used for cases where the index is out of
- * range for sequence type seqType.
- */
- static Node mkSkolemSeqNth(TypeNode seqType, const char* c);
/** Returns a (uncached) skolem of type string with name c */
Node mkSkolem(const char* c);
/** Returns true if n is a skolem allocated by this class */
Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12));
Node b1 = nm->mkNode(AND, b11, b12, b13);
- // nodes for the case where `seq.nth` is undefined.
- Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
- Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
-
- // the full ite, split on definedness of `seq.nth`
- Node lemma = nm->mkNode(ITE, cond, b1, b2);
+ // the lemma for `seq.nth`
+ Node lemma = nm->mkNode(IMPLIES, cond, b1);
// assert:
- // IF n >=0 AND n < len( s )
- // THEN: s = sk1 ++ unit(skt) ++ sk2 AND
- // len( sk1 ) = n AND
- // ( len( sk2 ) = len( s )- (n+1)
- // ELSE: skt = Uf(s, n), where Uf is a cached skolem function.
+ // n >=0 AND n < len( s )
+ // IMPLIES: s = sk1 ++ unit(skt) ++ sk2 AND
+ // len( sk1 ) = n AND
+ // ( len( sk2 ) = len( s )- (n+1)
asserts.push_back(lemma);
retNode = skt;
}
projects / cvc5.git / commitdiff