No behavior changes in this commit for current main.
case kind::STRING_STOI: return "str.to_int";
case kind::STRING_IN_REGEXP: return "str.in_re";
case kind::STRING_TO_REGEXP: return "str.to_re";
+ case kind::STRING_UNIT: return "str.unit";
case kind::REGEXP_NONE: return "re.none";
case kind::REGEXP_ALL: return "re.all";
case kind::REGEXP_ALLCHAR: return "re.allchar";
Integer i = results[currNode[1]].d_rat.getNumerator();
if (i.strictlyNegative() || i >= s_len)
{
- results[currNode] = EvalResult(s);
+ results[currNode] = EvalResult(Rational(-1));
}
else
{
std::vector<Node> extractTerms = d_esolver.getActive(STRING_SUBSTR);
for (const Node& n : extractTerms)
{
- if (d_termReg.isHandledUpdate(n))
+ if (d_termReg.isHandledUpdateOrSubstr(n))
{
- // (seq.extract A i l) ^ (<= 0 i) ^ (< i (str.len A)) --> (seq.unit
- // (seq.nth A i))
+ // (seq.extract A i l) in terms:
+ // IF (<= 0 i) ^ (< i (str.len A))
+ // THEN (seq.extract A i l) = (seq.unit (seq.nth A i))
+ // ELSE (seq.extract A i l) = empty
std::vector<Node> exp;
Node cond1 = nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n[1]);
Node cond2 = nm->mkNode(LT, n[1], nm->mkNode(STRING_LENGTH, n[0]));
Node cond = nm->mkNode(AND, cond1, cond2);
- Node body1 = nm->mkNode(
- EQUAL, n, nm->mkNode(SEQ_UNIT, nm->mkNode(SEQ_NTH, n[0], n[1])));
+ TypeNode tn = n.getType();
+ Node nth = nm->mkNode(SEQ_NTH, n[0], n[1]);
+ Node unit = utils::mkUnit(tn, nth);
+ Node body1 = nm->mkNode(EQUAL, n, unit);
Node body2 = nm->mkNode(EQUAL, n, Word::mkEmptyWord(n.getType()));
Node lem = nm->mkNode(ITE, cond, body1, body2);
sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_EXTRACT);
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"
+#include "util/string.h"
using namespace cvc5::context;
using namespace cvc5::internal::kind;
Trace("seq-array-debug") << "check term " << t << "..." << std::endl;
if (k == STRING_UPDATE)
{
- if (!d_termReg.isHandledUpdate(t))
+ if (!d_termReg.isHandledUpdateOrSubstr(t))
{
// not handled by procedure
Trace("seq-array-debug") << "...unhandled" << std::endl;
Trace("seq-array-debug") << "...norm form size 1" << std::endl;
// NOTE: could split on n=0 if needed, do not introduce ITE
Kind ck = nf.d_nf[0].getKind();
+ bool cIsConst = nf.d_nf[0].isConst();
// Note that (seq.unit c) is rewritten to CONST_SEQUENCE{c}, hence we
// check two cases here. It is important for completeness of this schema
// to handle this differently from STRINGS_ARRAY_UPDATE_CONCAT /
// STRINGS_ARRAY_NTH_CONCAT. Otherwise we would conclude a trivial
// equality when update/nth is applied to a constant of length one.
- if (ck == SEQ_UNIT
- || (ck == CONST_SEQUENCE && Word::getLength(nf.d_nf[0]) == 1))
+ if (ck == SEQ_UNIT || ck == STRING_UNIT
+ || (cIsConst && Word::getLength(nf.d_nf[0]) == 1))
{
Trace("seq-array-debug") << "...unit case" << std::endl;
// do we know whether n = 0 ?
{
Assert(k == SEQ_NTH);
Node val;
- if (ck == CONST_SEQUENCE)
+ if (cIsConst)
{
- const Sequence& seq = nf.d_nf[0].getConst<Sequence>();
- val = seq.getVec()[0];
+ val = Word::getNth(nf.d_nf[0], 0);
}
else
{
}
return;
}
- else if (ck != CONST_SEQUENCE)
+ else if (!cIsConst)
{
if (k == STRING_UPDATE)
{
NormalForm& nfSelf = d_csolver.getNormalForm(rself);
if (nfSelf.d_nf.size() == 1)
{
- // otherwise, if the normal form is not a constant sequence, and we
+ // otherwise, if the normal form is not a constant word, and we
// are an atomic update term, then this term will be given to the
// core array solver.
d_currTerms[k].push_back(t);
}
else
{
- // if the normal form is a constant sequence, it is treated as a
+ // if the normal form is a constant word, it is treated as a
// concatenation. We split per character and case split on whether the
// nth/update falls on each character below, which must have a size
// greater than one.
// an optimization to short cut introducing terms like
// (seq.nth (seq.unit c) i), which by construction is only relevant in
// the context where i = 0, hence we replace by c here.
- else if (c.getKind() == CONST_SEQUENCE)
+ else if (c.isConst())
{
- const Sequence& seq = c.getConst<Sequence>();
- if (seq.size() == 1)
+ if (Word::getLength(c) == 1)
{
if (k == STRING_UPDATE)
{
}
else
{
- cc = seq.getVec()[0];
+ cc = Word::getNth(c, 0);
}
}
}
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"
+#include "util/string.h"
using namespace std;
using namespace cvc5::context;
else
{
// should not have two constants in the same equivalence class
- Assert(cval.getType().isSequence());
std::vector<Node> cchars = Word::getChars(cval);
if (cchars.size() == 1)
{
Node oval = prev.isConst() ? n : prev;
- Assert(oval.getKind() == SEQ_UNIT);
+ Assert(oval.getKind() == SEQ_UNIT
+ || oval.getKind() == STRING_UNIT);
s = oval[0];
- t = cchars[0].getConst<Sequence>().getVec()[0];
+ t = Word::getNth(cchars[0], 0);
// oval is congruent (ignored) in this context
d_congruent.insert(oval);
}
for (size_t i = 0; i < 2; i++)
{
NormalForm& nfc = i == 0 ? nfni : nfnj;
- if (nfc.d_nf.size() == 0 || nfc.d_nf[0].getKind() != SEQ_UNIT)
+ if (nfc.d_nf.size() == 0)
{
// may need to look at the other side
continue;
}
Node u = nfc.d_nf[0];
+ if (u.getKind() != SEQ_UNIT && u.getKind() != STRING_UNIT)
+ {
+ continue;
+ }
// if the other side is constant like
NormalForm& nfo = i == 0 ? nfnj : nfni;
if (nfo.d_nf.size() == 0 || !utils::isConstantLike(nfo.d_nf[0]))
break;
}
// get the element of the character
- vc = vchars[0].getConst<Sequence>().getVec()[0];
+ vc = Word::getNth(vchars[0], 0);
}
else
{
- Assert(v.getKind() == SEQ_UNIT);
+ Assert(v.getKind() == SEQ_UNIT || v.getKind() == STRING_UNIT);
vc = v[0];
}
Assert(u[0].getType() == vc.getType());
Node deq = u.eqNode(v).notNode();
std::vector<Node> premises;
premises.push_back(deq);
+ Assert(u[0].getType()==vc.getType());
Node conc = u[0].eqNode(vc).notNode();
d_im.sendInference(premises, conc, InferenceId::STRINGS_UNIT_INJ_DEQ, false, true);
return;
ss1 = nm->mkNode(SEQ_NTH, n1, k);
ss2 = nm->mkNode(SEQ_NTH, n2, k);
}
+
// disequality between nth/substr
Node conc1 = ss1.eqNode(ss2).negate();
d_extt.addFunctionKind(kind::STRING_TO_LOWER);
d_extt.addFunctionKind(kind::STRING_TO_UPPER);
d_extt.addFunctionKind(kind::STRING_REV);
+ d_extt.addFunctionKind(kind::STRING_UNIT);
d_extt.addFunctionKind(kind::SEQ_UNIT);
d_extt.addFunctionKind(kind::SEQ_NTH);
return false;
}
}
- else if (k == SEQ_UNIT || k == STRING_IN_REGEXP || k == STRING_TO_CODE
- || (k == STRING_CONTAINS && pol == 0))
+ else if (k == SEQ_UNIT || k == STRING_UNIT || k == STRING_IN_REGEXP
+ || k == STRING_TO_CODE || (k == STRING_CONTAINS && pol == 0))
{
// never necessary to reduce seq.unit. str.to_code or str.in_re here.
// also, we do not reduce str.contains that are preregistered but not
return false;
}
else if ((k == STRING_UPDATE || k == STRING_SUBSTR)
- && d_termReg.isHandledUpdate(n))
+ && d_termReg.isHandledUpdateOrSubstr(n))
{
// don't need to reduce certain seq.update
// don't need to reduce certain seq.extract with length 1
Node t[2];
for (size_t i = 0; i < 2; i++)
{
- if (children[0][i].getKind() == SEQ_UNIT)
+ Node c = children[0][i];
+ Kind k = c.getKind();
+ if (k == SEQ_UNIT || k == STRING_UNIT)
{
- t[i] = children[0][i][0];
+ t[i] = c[0];
}
- else if (children[0][i].isConst())
+ else if (c.isConst())
{
// notice that Word::getChars is not the right call here, since it
// gets a vector of sequences of length one. We actually need to
- // extract the character, which is a sequence-specific operation.
- const Sequence& sx = children[0][i].getConst<Sequence>();
- const std::vector<Node>& vec = sx.getVec();
- if (vec.size() == 1)
+ // extract the character.
+ if (Word::getLength(c) == 1)
{
- // the character of the single character sequence
- t[i] = vec[0];
+ t[i] = Word::getNth(c, 0);
}
}
if (t[i].isNull())
case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL";
+ case Rewrite::SEQ_NTH_EVAL_OOB: return "SEQ_NTH_EVAL_OOB";
case Rewrite::SEQ_NTH_EVAL_SYM: return "SEQ_NTH_EVAL_SYM";
default: return "?";
}
CHARAT_ELIM,
SEQ_UNIT_EVAL,
SEQ_NTH_EVAL,
+ SEQ_NTH_EVAL_OOB,
SEQ_NTH_EVAL_SYM
};
Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV);
}
- else if (nk0 == SEQ_UNIT)
+ else if (nk0 == SEQ_UNIT || nk0 == STRING_UNIT)
{
Node retNode = nm->mkConstInt(Rational(1));
return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT);
if (posInt.fitsUnsignedInt() && posInt < Integer(len))
{
size_t pos = posInt.toUnsignedInt();
- std::vector<Node> elements = s.getConst<Sequence>().getVec();
- const Node& ret = elements[pos];
+ Node ret = Word::getNth(s, pos);
return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
}
}
+ if (s.getType().isString())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node ret = nm->mkConstInt(Rational(-1));
+ return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL_OOB);
+ }
}
std::vector<Node> prefix, suffix;
if ((i.isConst() && i.getConst<Rational>().isZero())
|| d_stringsEntail.stripSymbolicLength(suffix, prefix, 1, i, true))
{
- if (suffix.size() > 0 && suffix[0].getKind() == SEQ_UNIT)
+ if (suffix.size() > 0)
{
- // (seq.nth (seq.++ prefix (seq.unit x) suffix) n) ---> x
- // if len(prefix) = n
- Node ret = suffix[0][0];
- return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL_SYM);
+ if (suffix[0].getKind() == SEQ_UNIT)
+ {
+ // (seq.nth (seq.++ prefix (seq.unit x) suffix) n) ---> x
+ // if len(prefix) = n
+ Node ret = suffix[0][0];
+ return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL_SYM);
+ }
+ // TODO: STRING_UNIT?
}
}
Node SequencesRewriter::rewriteSeqUnit(Node node)
{
+ Assert(node.getKind() == SEQ_UNIT);
NodeManager* nm = NodeManager::currentNM();
if (node[0].isConst())
{
{
retNode = rewriteStringFromCode(node);
}
+ else if (nk == STRING_UNIT)
+ {
+ retNode = rewriteStringUnit(node);
+ }
else
{
return SequencesRewriter::postRewrite(node);
return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
}
+Node StringsRewriter::rewriteStringUnit(Node n)
+{
+ Assert(n.getKind() == STRING_UNIT);
+ NodeManager* nm = NodeManager::currentNM();
+ if (n[0].isConst())
+ {
+ Integer i = n[0].getConst<Rational>().getNumerator();
+ Node ret;
+ if (i >= 0 && i < d_alphaCard)
+ {
+ std::vector<unsigned> svec = {i.toUnsignedInt()};
+ ret = nm->mkConst(String(svec));
+ return returnRewrite(n, ret, Rewrite::SEQ_UNIT_EVAL);
+ }
+ }
+ return n;
+}
+
} // namespace strings
} // namespace theory
} // namespace cvc5::internal
*/
Node rewriteStringIsDigit(Node n);
+ /** rewrite string unit
+ *
+ * This is the entry point for post-rewriting terms n of the form
+ * str.unit( t )
+ * Returns the rewritten form of n.
+ */
+ Node rewriteStringUnit(Node n);
+
private:
/** The cardinality of the alphabet */
uint32_t d_alphaCard;
void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
+Node mkCodeRange(Node t, uint32_t alphaCard)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkNode(AND,
+ nm->mkNode(GEQ, t, nm->mkConstInt(Rational(0))),
+ nm->mkNode(LT, t, nm->mkConstInt(Rational(alphaCard))));
+}
+
Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
{
NodeManager* nm = NodeManager::currentNM();
Node len = nm->mkNode(STRING_LENGTH, t[0]);
Node code_len = len.eqNode(nm->mkConstInt(Rational(1)));
Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1)));
- Node code_range =
- nm->mkNode(AND,
- nm->mkNode(GEQ, t, nm->mkConstInt(Rational(0))),
- nm->mkNode(LT, t, nm->mkConstInt(Rational(alphaCard))));
+ Node code_range = mkCodeRange(t, alphaCard);
lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
}
else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
bool TermRegistry::hasSeqUpdate() const { return d_hasSeqUpdate; }
-bool TermRegistry::isHandledUpdate(Node n)
+bool TermRegistry::isHandledUpdateOrSubstr(Node n)
{
Assert(n.getKind() == STRING_UPDATE || n.getKind() == STRING_SUBSTR);
NodeManager* nm = NodeManager::currentNM();
* @return true if any seq.nth or seq.update terms have been preregistered
*/
bool hasSeqUpdate() const;
- /** is handled update */
- bool isHandledUpdate(Node n);
+ /** is handled update or substring */
+ bool isHandledUpdateOrSubstr(Node n);
/** get base */
Node getUpdateBase(Node n);
//---------------------------- end queries
TNode n,
bool check)
{
+ Assert(n.getKind() == kind::SEQ_NTH);
TypeNode t = n[0].getType(check);
- if (check && !t.isSequence())
+ if (check && !t.isStringLike())
{
- throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
+ throw TypeCheckingExceptionPrivate(n,
+ "expecting a string-like term in nth");
}
-
- TypeNode t1 = t.getSequenceElementType();
if (check)
{
TypeNode t2 = n[1].getType(check);
n, "expecting an integer start term in nth");
}
}
- return t1;
+ if (t.isSequence())
+ {
+ return t.getSequenceElementType();
+ }
+ Assert(t.isString());
+ return nodeManager->integerType();
}
Cardinality SequenceProperties::computeCardinality(TypeNode type)
; DISABLE-TESTER: dump
-; EXPECT: expecting a sequence
-; SCRUBBER: grep -o "expecting a sequence"
+; EXPECT: expecting a string-like
+; SCRUBBER: grep -o "expecting a string-like"
; EXIT: 1
(set-logic QF_SLIA)
(declare-const i Int)
projects / cvc5.git / commitdiff