summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/array_core_solver.cpp1
-rw-r--r--src/theory/strings/base_solver.cpp11
-rw-r--r--src/theory/strings/base_solver.h4
-rw-r--r--src/theory/strings/core_solver.cpp32
-rw-r--r--src/theory/strings/regexp_elim.cpp9
-rw-r--r--src/theory/strings/regexp_entail.cpp19
-rw-r--r--src/theory/strings/regexp_entail.h2
-rw-r--r--src/theory/strings/regexp_solver.cpp2
-rw-r--r--src/theory/strings/sequences_rewriter.cpp26
-rw-r--r--src/theory/strings/sequences_rewriter.h7
-rw-r--r--src/theory/strings/solver_state.cpp6
-rw-r--r--src/theory/strings/term_registry.cpp20
-rw-r--r--src/theory/strings/term_registry.h16
-rw-r--r--src/theory/strings/theory_strings.cpp25
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/strings/theory_strings_utils.cpp22
-rw-r--r--src/theory/strings/theory_strings_utils.h21
17 files changed, 112 insertions, 113 deletions
diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index 3b8fdeff4..9e3921e29 100644
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -116,7 +116,6 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& updateTerms)
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);
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 2d25a0d1e..f5864bdd3 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -32,8 +32,11 @@ namespace cvc5 {
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;
@@ -344,7 +347,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
Node c;
if (isConst)
{
- c = utils::mkNConcat(vecc, n.getType());
+ c = d_termReg.mkNConcat(vecc, n.getType());
}
if (!isConst || !d_state.areEqual(n, c))
{
@@ -421,7 +424,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
{
// 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;
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 96d275cd5..d4b0ebe0d 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -44,7 +44,7 @@ class BaseSolver : protected EnvObj
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
@@ -217,6 +217,8 @@ class BaseSolver : protected EnvObj
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;
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index ab214c9ce..868e855ab 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -562,7 +562,7 @@ void CoreSolver::checkNormalFormsEq()
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())
{
@@ -690,7 +690,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp)
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")
@@ -708,7 +708,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp)
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;
@@ -1090,7 +1090,7 @@ void CoreSolver::processNEqc(Node eqc,
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
@@ -1369,7 +1369,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
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;
@@ -1805,15 +1805,15 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
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);
@@ -1907,12 +1907,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
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)
{
@@ -1955,13 +1955,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
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,
@@ -2653,7 +2653,7 @@ void CoreSolver::checkLengthsEqc() {
// 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")
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 477533bee..a638d6009 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -21,6 +21,7 @@
#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"
@@ -173,7 +174,6 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
conc.push_back(currMem);
}
currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]);
- currEnd = Rewriter::rewrite(currEnd);
}
}
Node res = nm->mkNode(AND, conc);
@@ -560,7 +560,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
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)
{
@@ -588,8 +587,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
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);
}
}
@@ -617,9 +614,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
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.
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index aa69f9ecf..c2ee079db 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -28,7 +28,7 @@ namespace cvc5 {
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));
@@ -659,11 +659,9 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
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)
@@ -690,7 +688,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
}
else if (k == REGEXP_CONCAT)
{
- NodeBuilder nb(PLUS);
+ Rational sum(0);
for (const Node& nc : n)
{
Node flc = getFixedLengthForRegexp(nc);
@@ -698,11 +696,10 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
{
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();
}
@@ -785,8 +782,6 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const
bool RegExpEntail::regExpIncludes(Node r1, Node r2)
{
- Assert(Rewriter::rewrite(r1) == r1);
- Assert(Rewriter::rewrite(r2) == r2);
if (r1 == r2)
{
return true;
diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h
index b0511bd53..62cb5a725 100644
--- a/src/theory/strings/regexp_entail.h
+++ b/src/theory/strings/regexp_entail.h
@@ -146,8 +146,6 @@ class RegExpEntail
* 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 */
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 24ce64842..9a13aeab3 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -115,7 +115,7 @@ bool RegExpSolver::checkInclInter(
std::vector<Node> mems2 = mr.second;
Trace("regexp-process")
<< "Memberships(" << mr.first << ") = " << mr.second << std::endl;
- if (!checkEqcInclusion(mems2))
+ if (options().strings.stringRegexpInclusion && !checkEqcInclusion(mems2))
{
// conflict discovered, return
return true;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 634f27294..aadca9904 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -40,6 +40,7 @@ namespace strings {
SequencesRewriter::SequencesRewriter(Rewriter* r,
HistogramStat<Rewrite>* statistics)
: d_statistics(statistics),
+ d_rr(r),
d_arithEntail(r),
d_stringsEntail(r, d_arithEntail, *this)
{
@@ -135,7 +136,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
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);
@@ -406,7 +407,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
// (= 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]));
@@ -614,9 +615,9 @@ Node SequencesRewriter::rewriteLength(Node node)
}
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]);
@@ -2555,7 +2556,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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]);
@@ -2801,8 +2802,8 @@ Node SequencesRewriter::rewriteReplace(Node node)
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;
@@ -2827,7 +2828,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
// 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>())
@@ -3033,8 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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),
@@ -3346,7 +3346,7 @@ Node SequencesRewriter::rewriteReplaceReAll(Node node)
// "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>();
@@ -3524,7 +3524,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
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;
}
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 854e3fb81..850acfb2a 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -284,7 +284,7 @@ class SequencesRewriter : public TheoryRewriter
* 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)
@@ -305,6 +305,11 @@ class SequencesRewriter : public TheoryRewriter
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. */
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 6b7fc699b..96e143244 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -77,7 +77,8 @@ TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
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
@@ -116,7 +117,8 @@ Node SolverState::explainNonEmpty(Node s)
{
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();
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index d2d723276..85ec680ac 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -81,7 +81,8 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
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,
@@ -115,7 +116,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
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;
@@ -669,6 +670,21 @@ void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
}
}
+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
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 1de5def9e..338e528fe 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -213,6 +213,22 @@ class TermRegistry : protected EnvObj
*/
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;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8b496b725..ee068fe16 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -59,13 +59,15 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
d_rewriter(env.getRewriter(),
&d_statistics.d_rewrites,
d_termReg.getAlphabetCardinality()),
- d_eagerSolver(env, d_state, d_termReg),
+ d_eagerSolver(options().strings.stringEagerSolver
+ ? new EagerSolver(env, d_state, d_termReg)
+ : nullptr),
d_extTheoryCb(),
d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
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,
@@ -588,7 +590,7 @@ bool TheoryStrings::collectModelInfoType(
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;
@@ -651,7 +653,10 @@ void TheoryStrings::notifyFact(TNode atom,
TNode fact,
bool isInternal)
{
- d_eagerSolver.notifyFact(atom, polarity, fact, isInternal);
+ if (d_eagerSolver)
+ {
+ d_eagerSolver->notifyFact(atom, polarity, fact, isInternal);
+ }
// process pending conflicts due to reasoning about endpoints
if (!d_state.isInConflict() && d_state.hasPendingConflict())
{
@@ -769,7 +774,10 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
ei->d_codeTerm = t[0];
}
}
- d_eagerSolver.eqNotifyNewClass(t);
+ if (d_eagerSolver)
+ {
+ d_eagerSolver->eqNotifyNewClass(t);
+ }
}
void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2)
@@ -782,7 +790,10 @@ void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2)
// always create it if e2 was non-null
EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
- d_eagerSolver.eqNotifyMerge(e1, t1, e2, t2);
+ if (d_eagerSolver)
+ {
+ d_eagerSolver->eqNotifyMerge(e1, t1, e2, t2);
+ }
// add information from e2 to e1
if (!e2->d_lengthTerm.get().isNull())
@@ -1046,7 +1057,7 @@ void TheoryStrings::checkRegisterTermsNormalForms()
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);
}
}
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 21db7da0c..dd15e08ec 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -259,7 +259,7 @@ class TheoryStrings : public Theory {
/** The theory rewriter for this theory. */
StringsRewriter d_rewriter;
/** The eager solver */
- EagerSolver d_eagerSolver;
+ std::unique_ptr<EagerSolver> d_eagerSolver;
/** The extended theory callback */
StringsExtfCallback d_extTheoryCb;
/** The (custom) output channel of the theory of strings */
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 0ee2e906d..abac46d37 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -140,28 +140,6 @@ Node mkConcat(const std::vector<Node>& c, TypeNode tn)
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();
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 0cfcd64d0..f97391df8 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -61,27 +61,6 @@ void getConcat(Node n, std::vector<Node>& c);
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).
*/
Node mkPrefix(Node t, Node n);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback