Node left = nm->mkNode(SEQ_NTH, termProxy, n[1]);
Node right =
nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(Rational(0))); // n[2][0]
- right = Rewriter::rewrite(right);
Node lem = nm->mkNode(EQUAL, left, right);
Trace("seq-array-debug") << "enter" << std::endl;
sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE);
namespace theory {
namespace strings {
-BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im)
- : EnvObj(env), d_state(s), d_im(im), d_congruent(context())
+BaseSolver::BaseSolver(Env& env,
+ SolverState& s,
+ InferenceManager& im,
+ TermRegistry& tr)
+ : EnvObj(env), d_state(s), d_im(im), d_termReg(tr), d_congruent(context())
{
d_false = NodeManager::currentNM()->mkConst(false);
d_cardSize = options().strings.stringsAlphaCard;
Node c;
if (isConst)
{
- c = utils::mkNConcat(vecc, n.getType());
+ c = d_termReg.mkNConcat(vecc, n.getType());
}
if (!isConst || !d_state.areEqual(n, c))
{
{
// The equivalence class is not entailed to be equal to a constant
// and we found a better concatenation
- Node nct = utils::mkNConcat(vecnc, n.getType());
+ Node nct = d_termReg.mkNConcat(vecnc, n.getType());
Assert(!nct.isConst());
bei.d_bestContent = nct;
bei.d_bestScore = contentSize;
using NodeSet = context::CDHashSet<Node>;
public:
- BaseSolver(Env& env, SolverState& s, InferenceManager& im);
+ BaseSolver(Env& env, SolverState& s, InferenceManager& im, TermRegistry& tr);
~BaseSolver();
//-----------------------inference steps
SolverState& d_state;
/** The (custom) output channel of the theory of strings */
InferenceManager& d_im;
+ /** Reference to the term registry of theory of strings */
+ TermRegistry& d_termReg;
/** Commonly used constants */
Node d_emptyString;
Node d_false;
return;
}
NormalForm& nfe = getNormalForm(eqc);
- Node nf_term = utils::mkNConcat(nfe.d_nf, stype);
+ Node nf_term = d_termReg.mkNConcat(nfe.d_nf, stype);
std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term);
if (itn != nf_to_eqc.end())
{
if (it != d_normal_form.end())
{
NormalForm& nf = it->second;
- Node ret = utils::mkNConcat(nf.d_nf, stype);
+ Node ret = d_termReg.mkNConcat(nf.d_nf, stype);
nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end());
d_im.addToExplanation(x, nf.d_base, nf_exp);
Trace("strings-debug")
Node nc = getNormalString(x[i], nf_exp);
vec_nodes.push_back(nc);
}
- return utils::mkNConcat(vec_nodes, stype);
+ return d_termReg.mkNConcat(vec_nodes, stype);
}
}
return x;
for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
{
NormalForm& nfi = normal_forms[i];
- Node ni = utils::mkNConcat(nfi.d_nf, stype);
+ Node ni = d_termReg.mkNConcat(nfi.d_nf, stype);
if (nfCache.find(ni) == nfCache.end())
{
// If the equivalence class is entailed to be constant, check
eqnc.push_back(nfkv[i]);
}
}
- eqn[r] = utils::mkNConcat(eqnc, stype);
+ eqn[r] = d_termReg.mkNConcat(eqnc, stype);
}
Trace("strings-solve-debug")
<< "Endpoint eq check: " << eqn[0] << " " << eqn[1] << std::endl;
Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;
Trace("strings-loop") << " ... T(Y.Z)= ";
std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index);
- Node t_yz = utils::mkNConcat(vec_t, stype);
+ Node t_yz = d_termReg.mkNConcat(vec_t, stype);
Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
Trace("strings-loop") << " ... S(Z.Y)= ";
std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end());
- Node s_zy = utils::mkNConcat(vec_s, stype);
+ Node s_zy = d_termReg.mkNConcat(vec_s, stype);
Trace("strings-loop") << s_zy << std::endl;
Trace("strings-loop") << " ... R= ";
std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end());
- Node r = utils::mkNConcat(vec_r, stype);
+ Node r = d_termReg.mkNConcat(vec_r, stype);
Trace("strings-loop") << r << std::endl;
Node emp = Word::mkEmptyWord(stype);
std::vector<Node> v2(vec_r);
v2.insert(v2.begin(), y);
v2.insert(v2.begin(), z);
- restr = utils::mkNConcat(z, y);
- cc = rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype)));
+ restr = d_termReg.mkNConcat(z, y);
+ cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(v2, stype)));
}
else
{
- cc = rewrite(s_zy.eqNode(utils::mkNConcat(z, y)));
+ cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(z, y)));
}
if (cc == d_false)
{
iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y);
Node sk_z = skc->mkSkolem("z_loop");
// t1 * ... * tn = y * z
- Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
+ Node conc1 = t_yz.eqNode(d_termReg.mkNConcat(sk_y, sk_z));
// s1 * ... * sk = z * y * r
vec_r.insert(vec_r.begin(), sk_y);
vec_r.insert(vec_r.begin(), sk_z);
- Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype));
- Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w));
- Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y);
+ Node conc2 = s_zy.eqNode(d_termReg.mkNConcat(vec_r, stype));
+ Node conc3 = vecoi[index].eqNode(d_termReg.mkNConcat(sk_y, sk_w));
+ Node restr = r == emp ? s_zy : d_termReg.mkNConcat(sk_z, sk_y);
str_in_re =
nm->mkNode(kind::STRING_IN_REGEXP,
sk_w,
// now, check if length normalization has occurred
if (ei->d_normalizedLength.get().isNull())
{
- Node nf = utils::mkNConcat(nfi.d_nf, stype);
+ Node nf = d_termReg.mkNConcat(nfi.d_nf, stype);
if (Trace.isOn("strings-process-debug"))
{
Trace("strings-process-debug")
#include "theory/rewriter.h"
#include "theory/strings/regexp_entail.h"
#include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
#include "util/rational.h"
#include "util/string.h"
conc.push_back(currMem);
}
currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]);
- currEnd = Rewriter::rewrite(currEnd);
}
}
Node res = nm->mkNode(AND, conc);
Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType);
Node substr_ch =
nm->mkNode(STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1)));
- substr_ch = Rewriter::rewrite(substr_ch);
// handle the case where it is purely characters
for (const Node& r : disj)
{
else
{
Node regexp_ch = nm->mkNode(STRING_IN_REGEXP, substr_ch, r);
- regexp_ch = Rewriter::rewrite(regexp_ch);
- Assert(regexp_ch.getKind() != STRING_IN_REGEXP);
char_constraints.push_back(regexp_ch);
}
}
Node s = r[0];
if (s.isConst())
{
- Node lens = nm->mkNode(STRING_LENGTH, s);
- lens = Rewriter::rewrite(lens);
- Assert(lens.isConst());
+ Node lens = nm->mkConstInt(Word::getLength(s));
Assert(lens.getConst<Rational>().sgn() > 0);
std::vector<Node> conj;
// lens is a positive constant, so it is safe to use total div/mod here.
namespace theory {
namespace strings {
-RegExpEntail::RegExpEntail(Rewriter* r) : d_rewriter(r), d_aent(r)
+RegExpEntail::RegExpEntail(Rewriter* r) : d_aent(r)
{
d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
Kind k = n.getKind();
if (k == STRING_TO_REGEXP)
{
- Node ret = nm->mkNode(STRING_LENGTH, n[0]);
- ret = Rewriter::rewrite(ret);
- if (ret.isConst())
+ if (n[0].isConst())
{
- return ret;
+ return nm->mkConstInt(Rational(Word::getLength(n[0])));
}
}
else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE)
}
else if (k == REGEXP_CONCAT)
{
- NodeBuilder nb(PLUS);
+ Rational sum(0);
for (const Node& nc : n)
{
Node flc = getFixedLengthForRegexp(nc);
{
return flc;
}
- nb << flc;
+ Assert(flc.isConst() && flc.getType().isInteger());
+ sum += flc.getConst<Rational>();
}
- Node ret = nb.constructNode();
- ret = Rewriter::rewrite(ret);
- return ret;
+ return nm->mkConstInt(sum);
}
return Node::null();
}
bool RegExpEntail::regExpIncludes(Node r1, Node r2)
{
- Assert(Rewriter::rewrite(r1) == r1);
- Assert(Rewriter::rewrite(r2) == r2);
if (r1 == r2)
{
return true;
* computed. Used for getConstantBoundLengthForRegexp.
*/
static bool getConstantBoundCache(TNode n, bool isLower, Node& c);
- /** The underlying rewriter */
- Rewriter* d_rewriter;
/** Arithmetic entailment module */
ArithEntail d_aent;
/** Common constants */
SequencesRewriter::SequencesRewriter(Rewriter* r,
HistogramStat<Rewrite>* statistics)
: d_statistics(statistics),
+ d_rr(r),
d_arithEntail(r),
d_stringsEntail(r, d_arithEntail, *this)
{
Node len0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
Node len_eq = len0.eqNode(len1);
- len_eq = Rewriter::rewrite(len_eq);
+ len_eq = d_rr->rewrite(len_eq);
if (len_eq.isConst() && !len_eq.getConst<bool>())
{
return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ);
// (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
if (x == repl[0])
{
- Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2]));
+ Node eq = rewriteEquality(nm->mkNode(EQUAL, repl[1], repl[2]));
if (eq.isConst() && !eq.getConst<bool>())
{
Node ret = nm->mkNode(NOT, nm->mkNode(STRING_CONTAINS, x, repl[1]));
}
else if (nk0 == STRING_REPLACE || nk0 == STRING_REPLACE_ALL)
{
- Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
- Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
- if (len1 == len2)
+ Node len1 = nm->mkNode(STRING_LENGTH, node[0][1]);
+ Node len2 = nm->mkNode(STRING_LENGTH, node[0][2]);
+ if (d_arithEntail.checkEq(len1, len2))
{
// len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
if (!node[2].isConst() || node[2].getConst<Rational>().sgn() != 0)
{
fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0);
- fstr = Rewriter::rewrite(fstr);
+ fstr = d_rr->rewrite(fstr);
}
Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]);
if (d_stringsEntail.checkLengthOne(node[0]))
{
Node empty = Word::mkEmptyWord(stype);
- Node rn1 = Rewriter::rewrite(
- rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty)));
+ Node rn1 =
+ d_rr->rewrite(rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty)));
if (rn1 != node[1])
{
std::vector<Node> emptyNodes;
// check if contains definitely does (or does not) hold
Node cmp_con = nm->mkNode(kind::STRING_CONTAINS, node[0], node[1]);
- Node cmp_conr = Rewriter::rewrite(cmp_con);
+ Node cmp_conr = d_rr->rewrite(cmp_con);
if (cmp_conr.isConst())
{
if (cmp_conr.getConst<bool>())
if (d_arithEntail.check(wlen, zlen))
{
// w != z
- Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z));
- if (wEqZ.isConst() && !wEqZ.getConst<bool>())
+ if (w != z && w.isConst() && z.isConst())
{
Node ret = nm->mkNode(kind::STRING_REPLACE,
nm->mkNode(kind::STRING_REPLACE, y, w, z),
// "Z" ++ y ++ "Z" ++ y
TypeNode t = x.getType();
Node emp = Word::mkEmptyWord(t);
- Node yp = Rewriter::rewrite(
+ Node yp = d_rr->rewrite(
nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp)));
std::vector<Node> res;
String rem = x.getConst<String>();
Node SequencesRewriter::lengthPreserveRewrite(Node n)
{
NodeManager* nm = NodeManager::currentNM();
- Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n));
+ Node len = d_rr->rewrite(nm->mkNode(kind::STRING_LENGTH, n));
Node res = canonicalStrForSymbolicLength(len, n.getType());
return res.isNull() ? n : res;
}
* We apply certain normalizations to n', such as replacing all constants
* that are not relevant to length by "A".
*/
- static Node lengthPreserveRewrite(Node n);
+ Node lengthPreserveRewrite(Node n);
/**
* Given a symbolic length n, returns the canonical string (of type stype)
Node postProcessRewrite(Node node, Node ret);
/** Reference to the rewriter statistics. */
HistogramStat<Rewrite>* d_statistics;
+ /**
+ * Pointer to the rewriter. NOTE this is a cyclic dependency, and should
+ * be removed.
+ */
+ Rewriter* d_rr;
/** The arithmetic entailment module */
ArithEntail d_arithEntail;
/** Instance of the entailment checker for strings. */
Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
{
Assert(areEqual(t, te));
- Node lt = utils::mkNLength(te);
+ Node lt = NodeManager::currentNM()->mkNode(STRING_LENGTH, t);
+ lt = rewrite(lt);
if (hasTerm(lt))
{
// use own length if it exists, leads to shorter explanation
{
return s.eqNode(emp).negate();
}
- Node sLen = utils::mkNLength(s);
+ Node sLen = NodeManager::currentNM()->mkNode(STRING_LENGTH, s);
+ sLen = rewrite(sLen);
if (areDisequal(sLen, d_zero))
{
return sLen.eqNode(d_zero).negate();
if (tk == STRING_TO_CODE)
{
// ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
- Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConstInt(Rational(1)));
+ 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,
sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
Node sk2 =
sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
- lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
+ lemma = t[0].eqNode(nm->mkNode(STRING_CONCAT, sk1, t[1], sk2));
lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
}
return lemma;
}
}
+Node TermRegistry::mkNConcat(Node n1, Node n2) const
+{
+ return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2));
+}
+
+Node TermRegistry::mkNConcat(Node n1, Node n2, Node n3) const
+{
+ return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3));
+}
+
+Node TermRegistry::mkNConcat(const std::vector<Node>& c, TypeNode tn) const
+{
+ return rewrite(utils::mkConcat(c, tn));
+}
+
} // namespace strings
} // namespace theory
} // namespace cvc5
*/
void removeProxyEqs(Node n, std::vector<Node>& unproc) const;
//---------------------------- end proxy variables
+ /**
+ * Returns the rewritten form of the string concatenation of n1 and n2.
+ */
+ Node mkNConcat(Node n1, Node n2) const;
+
+ /**
+ * Returns the rewritten form of the string concatenation of n1, n2 and n3.
+ */
+ Node mkNConcat(Node n1, Node n2, Node n3) const;
+
+ /**
+ * Returns the rewritten form of the concatentation from vector c of
+ * (string-like) type tn.
+ */
+ Node mkNConcat(const std::vector<Node>& c, TypeNode tn) const;
+
private:
/** Common constants */
Node d_zero;
d_extTheory(env, d_extTheoryCb, d_im),
// the checker depends on the cardinality of the alphabet
d_checker(d_termReg.getAlphabetCardinality()),
- d_bsolver(env, d_state, d_im),
+ d_bsolver(env, d_state, d_im, d_termReg),
d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
d_esolver(env,
d_state,
Assert(r.isConst() || processed.find(r) != processed.end());
nc.push_back(r.isConst() ? r : processed[r]);
}
- Node cc = utils::mkNConcat(nc, tn);
+ Node cc = d_termReg.mkNConcat(nc, tn);
Trace("strings-model")
<< "*** Determined constant " << cc << " for " << rn << std::endl;
processed[rn] = cc;
Node lt = ei ? ei->d_lengthTerm : Node::null();
if (lt.isNull())
{
- Node c = utils::mkNConcat(nfi.d_nf, eqc.getType());
+ Node c = d_termReg.mkNConcat(nfi.d_nf, eqc.getType());
d_termReg.registerTerm(c, 3);
}
}
return NodeManager::currentNM()->mkNode(k, c);
}
-Node mkNConcat(Node n1, Node n2)
-{
- return Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2));
-}
-
-Node mkNConcat(Node n1, Node n2, Node n3)
-{
- return Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3));
-}
-
-Node mkNConcat(const std::vector<Node>& c, TypeNode tn)
-{
- return Rewriter::rewrite(mkConcat(c, tn));
-}
-
-Node mkNLength(Node t)
-{
- return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t));
-}
-
Node mkPrefix(Node t, Node n)
{
NodeManager* nm = NodeManager::currentNM();
*/
Node mkConcat(const std::vector<Node>& c, TypeNode tn);
-/**
- * Returns the rewritten form of the string concatenation of n1 and n2.
- */
-Node mkNConcat(Node n1, Node n2);
-
-/**
- * Returns the rewritten form of the string concatenation of n1, n2 and n3.
- */
-Node mkNConcat(Node n1, Node n2, Node n3);
-
-/**
- * Returns the rewritten form of the concatentation from vector c of
- * (string-like) type tn.
- */
-Node mkNConcat(const std::vector<Node>& c, TypeNode tn);
-
-/**
- * Returns the rewritten form of the length of string term t.
- */
-Node mkNLength(Node t);
-
/**
* Returns (pre t n), which is (str.substr t 0 n).
*/
TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite)
{
+ StringsRewriter sr(d_rewriter, nullptr);
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
Node concat2 = d_nodeManager->mkNode(
kind::STRING_CONCAT,
{gh, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, gh, ij), ij});
- Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1);
- Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2);
+ Node res_concat1 = sr.lengthPreserveRewrite(concat1);
+ Node res_concat2 = sr.lengthPreserveRewrite(concat2);
ASSERT_EQ(res_concat1, res_concat2);
}
projects / cvc5.git / commitdiff