There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.
#include "expr/node_traversal.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/env.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
namespace passes {
using namespace cvc5::theory;
-ForeignTheoryRewrite::ForeignTheoryRewrite(
- PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
- d_cache(userContext()){};
-Node ForeignTheoryRewrite::simplify(Node n)
+ForeignTheoryRewriter::ForeignTheoryRewriter(Env& env)
+ : EnvObj(env), d_cache(userContext())
+{
+}
+
+Node ForeignTheoryRewriter::simplify(Node n)
{
std::vector<Node> toVisit;
n = rewrite(n);
return d_cache[n];
}
-Node ForeignTheoryRewrite::foreignRewrite(Node n)
+Node ForeignTheoryRewriter::foreignRewrite(Node n)
{
// n is a rewritten node, and so GT, LT, LEQ
// should have been eliminated
return n;
}
-Node ForeignTheoryRewrite::rewriteStringsGeq(Node n)
+Node ForeignTheoryRewriter::rewriteStringsGeq(Node n)
{
+ theory::strings::ArithEntail ae(d_env.getRewriter());
// check if the node can be simplified to true
- if (theory::strings::ArithEntail::check(n[0], n[1], false))
+ if (ae.check(n[0], n[1], false))
{
return NodeManager::currentNM()->mkConst(true);
}
return n;
}
-Node ForeignTheoryRewrite::reconstructNode(Node originalNode,
- std::vector<Node> newChildren)
+Node ForeignTheoryRewriter::reconstructNode(Node originalNode,
+ std::vector<Node> newChildren)
{
// Nodes with no children are reconstructed to themselves
if (originalNode.getNumChildren() == 0)
return builder.constructNode();
}
+ForeignTheoryRewrite::ForeignTheoryRewrite(
+ PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
+ d_ftr(preprocContext->getEnv())
+{
+}
+
PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+ for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
+ ++i)
{
assertionsToPreprocess->replace(
- i, rewrite(simplify((*assertionsToPreprocess)[i])));
+ i, rewrite(d_ftr.simplify((*assertionsToPreprocess)[i])));
}
-
return PreprocessingPassResult::NO_CONFLICT;
}
#include "context/cdhashmap.h"
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace preprocessing {
using CDNodeMap = context::CDHashMap<Node, Node>;
-class ForeignTheoryRewrite : public PreprocessingPass
+class ForeignTheoryRewriter : protected EnvObj
{
public:
- ForeignTheoryRewrite(PreprocessingPassContext* preprocContext);
-
- protected:
- PreprocessingPassResult applyInternal(
- AssertionPipeline* assertionsToPreprocess) override;
+ ForeignTheoryRewriter(Env& env);
/** the main function that simplifies n.
* does a traversal on n and call rewriting fucntions.
*/
/** A specific simplification function specific for GEQ
* constraints in strings.
*/
- static Node rewriteStringsGeq(Node n);
+ Node rewriteStringsGeq(Node n);
/** invoke rewrite functions for n.
* based on the structure of n (typically its kind)
* we invoke rewrites from other theories.
* For example: when encountering a `>=` node,
* we invoke rewrites from the theory of strings.
*/
- static Node foreignRewrite(Node n);
+ Node foreignRewrite(Node n);
/** construct a node with the same operator as originalNode whose children are
* processedChildren
*/
CDNodeMap d_cache;
};
+class ForeignTheoryRewrite : public PreprocessingPass
+{
+ public:
+ ForeignTheoryRewrite(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+ /** Foreign theory rewriter */
+ ForeignTheoryRewriter d_ftr;
+};
+
} // namespace passes
} // namespace preprocessing
} // namespace cvc5
if (ret.getKind() == EQUAL)
{
- new_ret = strings::SequencesRewriter(nullptr).rewriteEqualityExt(ret);
+ strings::SequencesRewriter sr(&d_rew, nullptr);
+ new_ret = sr.rewriteEqualityExt(ret);
}
return new_ret;
namespace theory {
namespace strings {
+ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) {}
+
bool ArithEntail::checkEq(Node a, Node b)
{
if (a == b)
{
return true;
}
- Node ar = Rewriter::rewrite(a);
- Node br = Rewriter::rewrite(b);
+ Node ar = d_rr->rewrite(a);
+ Node br = d_rr->rewrite(b);
return ar == br;
}
Node ar = strict ? NodeManager::currentNM()->mkNode(
kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1)))
: a;
- ar = Rewriter::rewrite(ar);
+ ar = d_rr->rewrite(ar);
if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
{
bool ArithEntail::checkApprox(Node ar)
{
- Assert(Rewriter::rewrite(ar) == ar);
+ Assert(d_rr->rewrite(ar) == ar);
NodeManager* nm = NodeManager::currentNM();
std::map<Node, Node> msum;
Trace("strings-ent-approx-debug")
{
Node curr = toProcess.back();
Trace("strings-ent-approx-debug") << " process " << curr << std::endl;
- curr = Rewriter::rewrite(curr);
+ curr = d_rr->rewrite(curr);
toProcess.pop_back();
if (visited.find(curr) == visited.end())
{
Node aar = aarSum.empty()
? nm->mkConst(Rational(0))
: (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum));
- aar = Rewriter::rewrite(aar);
+ aar = d_rr->rewrite(aar);
Trace("strings-ent-approx-debug")
<< "...processed fixed sum " << aar << " with " << mApprox.size()
<< " approximated monomials." << std::endl;
Node ci = aam.second;
if (!cr.isNull())
{
- ci = ci.isNull() ? cr
- : Rewriter::rewrite(nm->mkNode(MULT, ci, cr));
+ ci = ci.isNull() ? cr : d_rr->rewrite(nm->mkNode(MULT, ci, cr));
}
Trace("strings-ent-approx-debug") << ci << "*" << ti << " ";
int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn();
Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
aar = nm->mkNode(PLUS, aar, mn);
// update the msumAar map
- aar = Rewriter::rewrite(aar);
+ aar = d_rr->rewrite(aar);
msumAar.clear();
if (!ArithMSum::getMonomialSum(aar, msumAar))
{
bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
{
Assert(assumption.getKind() == kind::EQUAL);
- Assert(Rewriter::rewrite(assumption) == assumption);
+ Assert(d_rr->rewrite(assumption) == assumption);
Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
<< ", strict=" << strict << std::endl;
Node b,
bool strict)
{
- Assert(Rewriter::rewrite(assumption) == assumption);
+ Assert(d_rr->rewrite(assumption) == assumption);
NodeManager* nm = NodeManager::currentNM();
Node s = nm->mkBoundVar("slackVal", nm->stringType());
Node slen = nm->mkNode(kind::STRING_LENGTH, s);
- assumption = Rewriter::rewrite(
+ assumption = d_rr->rewrite(
nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
}
bool res = false;
for (const auto& assumption : assumptions)
{
- Assert(Rewriter::rewrite(assumption) == assumption);
+ Assert(d_rr->rewrite(assumption) == assumption);
if (checkWithAssumption(assumption, a, b, strict))
{
Node ArithEntail::getConstantBound(Node a, bool isLower)
{
- Assert(Rewriter::rewrite(a) == a);
+ Assert(d_rr->rewrite(a) == a);
Node ret;
if (a.isConst())
{
else
{
ret = NodeManager::currentNM()->mkNode(a.getKind(), children);
- ret = Rewriter::rewrite(ret);
+ ret = d_rr->rewrite(ret);
}
}
}
bool ArithEntail::checkInternal(Node a)
{
- Assert(Rewriter::rewrite(a) == a);
+ Assert(d_rr->rewrite(a) == a);
// check whether a >= 0
if (a.isConst())
{
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace strings {
/**
class ArithEntail
{
public:
+ ArithEntail(Rewriter* r);
/** check arithmetic entailment equal
* Returns true if it is always the case that a = b.
*/
- static bool checkEq(Node a, Node b);
+ bool checkEq(Node a, Node b);
/** check arithmetic entailment
* Returns true if it is always the case that a >= b,
* and a>b if strict is true.
*/
- static bool check(Node a, Node b, bool strict = false);
+ bool check(Node a, Node b, bool strict = false);
/** check arithmetic entailment
* Returns true if it is always the case that a >= 0.
*/
- static bool check(Node a, bool strict = false);
+ bool check(Node a, bool strict = false);
/** check arithmetic entailment with approximations
*
* Returns true if it is always the case that a >= 0. We expect that a is in
* and thus the entailment len( x ) - len( substr( y, 0, len( x ) ) ) >= 0
* holds.
*/
- static bool checkApprox(Node a);
+ bool checkApprox(Node a);
/**
* Checks whether assumption |= a >= 0 (if strict is false) or
*
* Because: x = -(str.len y), so -x >= 0 --> (str.len y) >= 0 --> true
*/
- static bool checkWithEqAssumption(Node assumption,
- Node a,
- bool strict = false);
+ bool checkWithEqAssumption(Node assumption, Node a, bool strict = false);
/**
* Checks whether assumption |= a >= b (if strict is false) or
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
*/
- static bool checkWithAssumption(Node assumption,
- Node a,
- Node b,
- bool strict = false);
+ bool checkWithAssumption(Node assumption,
+ Node a,
+ Node b,
+ bool strict = false);
/**
* Checks whether assumptions |= a >= b (if strict is false) or
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
*/
- static bool checkWithAssumptions(std::vector<Node> assumptions,
- Node a,
- Node b,
- bool strict = false);
+ bool checkWithAssumptions(std::vector<Node> assumptions,
+ Node a,
+ Node b,
+ bool strict = false);
/** get arithmetic lower bound
* If this function returns a non-null Node ret,
* if and only if
* check( a, strict ) = true.
*/
- static Node getConstantBound(Node a, bool isLower = true);
+ Node getConstantBound(Node a, bool isLower = true);
/**
* Given an inequality y1 + ... + yn >= x, removes operands yi s.t. the
* --> returns false because it is not possible to show
* str.len(y) >= str.len(x)
*/
- static bool inferZerosInSumGeq(Node x,
- std::vector<Node>& ys,
- std::vector<Node>& zeroYs);
+ bool inferZerosInSumGeq(Node x,
+ std::vector<Node>& ys,
+ std::vector<Node>& zeroYs);
private:
/** check entail arithmetic internal
* Returns true if we can show a >= 0 always.
* a is in rewritten form.
*/
- static bool checkInternal(Node a);
+ bool checkInternal(Node a);
/** Get arithmetic approximations
*
* This gets the (set of) arithmetic approximations for term a and stores
* function might be len( substr( x, 0, n ) ) - len( y ), where we don't
* consider (recursively) the approximations for len( substr( x, 0, n ) ).
*/
- static void getArithApproximations(Node a,
- std::vector<Node>& approx,
- bool isOverApprox = false);
+ void getArithApproximations(Node a,
+ std::vector<Node>& approx,
+ bool isOverApprox = false);
+ /** The underlying rewriter */
+ Rewriter* d_rr;
};
} // namespace strings
namespace theory {
namespace strings {
-SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics)
- : d_statistics(statistics), d_stringsEntail(*this)
+SequencesRewriter::SequencesRewriter(Rewriter* r,
+ HistogramStat<Rewrite>* statistics)
+ : d_statistics(statistics),
+ d_arithEntail(r),
+ d_stringsEntail(r, d_arithEntail, *this)
{
}
+ArithEntail& SequencesRewriter::getArithEntail() { return d_arithEntail; }
+
+StringsEntail& SequencesRewriter::getStringsEntail() { return d_stringsEntail; }
+
Node SequencesRewriter::rewriteEquality(Node node)
{
Assert(node.getKind() == kind::EQUAL);
// ------- homogeneous constants
for (unsigned i = 0; i < 2; i++)
{
- Node cn = StringsEntail::checkHomogeneousString(node[i]);
+ Node cn = d_stringsEntail.checkHomogeneousString(node[i]);
if (!cn.isNull() && !Word::isEmpty(cn))
{
Assert(cn.isConst());
}
// (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
- if (StringsEntail::checkNonEmpty(ne[2]))
+ if (d_stringsEntail.checkNonEmpty(ne[2]))
{
Node ret =
nm->mkNode(AND,
}
// (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
- if (StringsEntail::checkLengthOne(ne[1], true) && ne[2] == empty)
+ if (d_stringsEntail.checkLengthOne(ne[1], true) && ne[2] == empty)
{
Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
{
Node zero = nm->mkConst(Rational(0));
- if (ArithEntail::check(ne[1], false) && ArithEntail::check(ne[2], true))
+ if (d_arithEntail.check(ne[1], false)
+ && d_arithEntail.check(ne[2], true))
{
// (= "" (str.substr x 0 m)) ---> (= "" x) if m > 0
if (ne[1] == zero)
}
// (= "" (str.substr "A" 0 z)) ---> (<= z 0)
- if (StringsEntail::checkNonEmpty(ne[0]) && ne[1] == zero)
+ if (d_stringsEntail.checkNonEmpty(ne[0]) && ne[1] == zero)
{
Node ret = nm->mkNode(LEQ, ne[2], zero);
return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_Z);
Node x = node[1 - i];
// (= "A" (str.replace "" x y)) ---> (= "" (str.replace "A" y x))
- if (StringsEntail::checkNonEmpty(x) && repl[0] == empty)
+ if (d_stringsEntail.checkNonEmpty(x) && repl[0] == empty)
{
Node ret = nm->mkNode(
EQUAL, empty, nm->mkNode(STRING_REPLACE, x, repl[2], repl[1]));
{
Node lenY = nm->mkNode(STRING_LENGTH, repl[1]);
Node lenZ = nm->mkNode(STRING_LENGTH, repl[2]);
- if (ArithEntail::checkEq(lenY, lenZ))
+ if (d_arithEntail.checkEq(lenY, lenZ))
{
Node ret = nm->mkNode(OR,
nm->mkNode(EQUAL, repl[0], repl[1]),
{
if (node[1 - i].getKind() == STRING_CONCAT)
{
- new_ret = StringsEntail::inferEqsFromContains(node[i], node[1 - i]);
+ new_ret = d_stringsEntail.inferEqsFromContains(node[i], node[1 - i]);
if (!new_ret.isNull())
{
return returnRewrite(node, new_ret, Rewrite::STR_EQ_CONJ_LEN_ENTAIL);
Node lenPfx0 = nm->mkNode(STRING_LENGTH, pfx0);
Node lenPfx1 = nm->mkNode(STRING_LENGTH, pfx1);
- if (ArithEntail::checkEq(lenPfx0, lenPfx1))
+ if (d_arithEntail.checkEq(lenPfx0, lenPfx1))
{
std::vector<Node> sfxv0(v0.begin() + i, v0.end());
std::vector<Node> sfxv1(v1.begin() + j, v1.end());
.eqNode(utils::mkConcat(sfxv1, stype)));
return returnRewrite(node, ret, Rewrite::SPLIT_EQ);
}
- else if (ArithEntail::check(lenPfx1, lenPfx0, true))
+ else if (d_arithEntail.check(lenPfx1, lenPfx0, true))
{
// The prefix on the right-hand side is strictly longer than the
// prefix on the left-hand side, so we try to strip the right-hand
// (= (str.++ "A" x y) (str.++ x "AB" z)) --->
// (and (= (str.++ "A" x) (str.++ x "A")) (= y (str.++ "B" z)))
std::vector<Node> rpfxv1;
- if (StringsEntail::stripSymbolicLength(
+ if (d_stringsEntail.stripSymbolicLength(
pfxv1, rpfxv1, 1, lenPfx0, true))
{
// The rewrite requires the full left-hand prefix length to be
// in the inner loop)
break;
}
- else if (ArithEntail::check(lenPfx0, lenPfx1, true))
+ else if (d_arithEntail.check(lenPfx0, lenPfx1, true))
{
// The prefix on the left-hand side is strictly longer than the
// prefix on the right-hand side, so we try to strip the left-hand
// (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))
std::vector<Node> sfxv0 = pfxv0;
std::vector<Node> rpfxv0;
- if (StringsEntail::stripSymbolicLength(
+ if (d_stringsEntail.stripSymbolicLength(
sfxv0, rpfxv0, 1, lenPfx1, true))
{
// The rewrite requires the full right-hand prefix length to be
Node lastX;
for (size_t i = 0, nsize = node_vec.size(); i < nsize; i++)
{
- Node s = StringsEntail::getStringOrEmpty(node_vec[i]);
+ Node s = d_stringsEntail.getStringOrEmpty(node_vec[i]);
bool nextX = false;
if (s != lastX)
{
Node zero = nm->mkConst(cvc5::Rational(0));
// if entailed non-positive length or negative start point
- if (ArithEntail::check(zero, node[1], true))
+ if (d_arithEntail.check(zero, node[1], true))
{
Node ret = Word::mkEmptyWord(node.getType());
return returnRewrite(node, ret, Rewrite::SS_START_NEG);
}
- else if (ArithEntail::check(zero, node[2]))
+ else if (d_arithEntail.check(zero, node[2]))
{
Node ret = Word::mkEmptyWord(node.getType());
return returnRewrite(node, ret, Rewrite::SS_LEN_NON_POS);
// over-approximation of the length of (str.substr x a a), which
// then allows us to reason that the result of the whole term must
// be empty.
- if (ArithEntail::check(node[1], node[0][2]))
+ if (d_arithEntail.check(node[1], node[0][2]))
{
Node ret = Word::mkEmptyWord(node.getType());
return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
// if (str.len y) = 1 and (str.len z) = 1
if (node[1] == zero)
{
- if (StringsEntail::checkLengthOne(node[0][1], true)
- && StringsEntail::checkLengthOne(node[0][2], true))
+ if (d_stringsEntail.checkLengthOne(node[0][1], true)
+ && d_stringsEntail.checkLengthOne(node[0][2], true))
{
Node ret = nm->mkNode(
kind::STRING_REPLACE,
{
Node curr = node[2];
std::vector<Node> childrenr;
- if (StringsEntail::stripSymbolicLength(n1, childrenr, 1, curr))
+ if (d_stringsEntail.stripSymbolicLength(n1, childrenr, 1, curr))
{
if (curr != zero && !n1.empty())
{
Node end_pt = Rewriter::rewrite(nm->mkNode(kind::PLUS, node[1], node[2]));
if (node[2] != tot_len)
{
- if (ArithEntail::check(node[2], tot_len))
+ if (d_arithEntail.check(node[2], tot_len))
{
// end point beyond end point of string, map to tot_len
Node ret = nm->mkNode(kind::STRING_SUBSTR, node[0], node[1], tot_len);
// (str.substr s x y) --> "" if x < len(s) |= 0 >= y
Node n1_lt_tot_len =
Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len));
- if (ArithEntail::checkWithAssumption(n1_lt_tot_len, zero, node[2], false))
+ if (d_arithEntail.checkWithAssumption(
+ n1_lt_tot_len, zero, node[2], false))
{
Node ret = Word::mkEmptyWord(node.getType());
return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
// (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
Node non_zero_len =
Rewriter::rewrite(nm->mkNode(kind::LT, zero, node[2]));
- if (ArithEntail::checkWithAssumption(
+ if (d_arithEntail.checkWithAssumption(
non_zero_len, node[1], tot_len, false))
{
Node ret = Word::mkEmptyWord(node.getType());
// (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
Node geq_zero_start =
Rewriter::rewrite(nm->mkNode(kind::GEQ, node[1], zero));
- if (ArithEntail::checkWithAssumption(
+ if (d_arithEntail.checkWithAssumption(
geq_zero_start, zero, tot_len, false))
{
Node ret = Word::mkEmptyWord(node.getType());
}
// (str.substr s x x) ---> "" if (str.len s) <= 1
- if (node[1] == node[2] && StringsEntail::checkLengthOne(node[0]))
+ if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
{
Node ret = Word::mkEmptyWord(node.getType());
return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
// strip off components while quantity is entailed positive
int dir = r == 0 ? 1 : -1;
std::vector<Node> childrenr;
- if (StringsEntail::stripSymbolicLength(n1, childrenr, dir, curr))
+ if (d_stringsEntail.stripSymbolicLength(n1, childrenr, dir, curr))
{
if (r == 0)
{
{
Node start_inner = node[0][1];
Node start_outer = node[1];
- if (ArithEntail::check(start_outer) && ArithEntail::check(start_inner))
+ if (d_arithEntail.check(start_outer) && d_arithEntail.check(start_inner))
{
// both are positive
// thus, start point is definitely start_inner+start_outer.
{
new_len = len_from_inner;
}
- else if (ArithEntail::check(len_from_inner, len_from_outer))
+ else if (d_arithEntail.check(len_from_inner, len_from_outer))
{
new_len = len_from_outer;
}
- else if (ArithEntail::check(len_from_outer, len_from_inner))
+ else if (d_arithEntail.check(len_from_outer, len_from_inner))
{
new_len = len_from_inner;
}
{
Node len1 =
NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
- if (ArithEntail::check(len1, true))
+ if (d_arithEntail.check(len1, true))
{
// we handle the false case here since the rewrite for equality
// uses this function, hence we want to conclude false if possible.
return returnRewrite(node, ret, Rewrite::CTN_LHS_EMPTYSTR);
}
}
- else if (StringsEntail::checkLengthOne(t))
+ else if (d_stringsEntail.checkLengthOne(t))
{
std::vector<Node> vec = Word::getChars(node[0]);
Node emp = Word::mkEmptyWord(t.getType());
else if (node[1].getKind() == kind::STRING_CONCAT)
{
int firstc, lastc;
- if (!StringsEntail::canConstantContainConcat(
+ if (!d_stringsEntail.canConstantContainConcat(
node[0], node[1], firstc, lastc))
{
Node ret = NodeManager::currentNM()->mkConst(false);
// strip endpoints
std::vector<Node> nb;
std::vector<Node> ne;
- if (StringsEntail::stripConstantEndpoints(nc1, nc2, nb, ne))
+ if (d_stringsEntail.stripConstantEndpoints(nc1, nc2, nb, ne))
{
Node ret = NodeManager::currentNM()->mkNode(
kind::STRING_CONTAINS, utils::mkConcat(nc1, stype), node[1]);
// length entailment
Node len_n1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
Node len_n2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
- if (ArithEntail::check(len_n2, len_n1, true))
+ if (d_arithEntail.check(len_n2, len_n1, true))
{
// len( n2 ) > len( n1 ) => contains( n1, n2 ) ---> false
Node ret = NodeManager::currentNM()->mkConst(false);
// For example, contains( str.++( x, "b" ), str.++( "a", x ) ) ---> false
// since the number of a's in the second argument is greater than the number
// of a's in the first argument
- if (StringsEntail::checkMultisetSubset(node[0], node[1]))
+ if (d_stringsEntail.checkMultisetSubset(node[0], node[1]))
{
Node ret = nm->mkConst(false);
return returnRewrite(node, ret, Rewrite::CTN_MSET_NSS);
}
- if (ArithEntail::check(len_n2, len_n1, false))
+ if (d_arithEntail.check(len_n2, len_n1, false))
{
// len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
Node ret = node[0].eqNode(node[1]);
// (str.contains (str.replace x y x) z) ---> (str.contains x z)
// if (str.len z) <= 1
- if (StringsEntail::checkLengthOne(node[1]))
+ if (d_stringsEntail.checkLengthOne(node[1]))
{
Node ret = nm->mkNode(kind::STRING_CONTAINS, node[0][0], node[1]);
return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
// (str.contains (str.replace x y z) w) --->
// (str.contains (str.replace x y "") w)
// if (str.contains z w) ---> false and (str.len w) = 1
- if (StringsEntail::checkLengthOne(node[1]))
+ if (d_stringsEntail.checkLengthOne(node[1]))
{
Node ctn = d_stringsEntail.checkContains(node[0][2], node[1]);
if (!ctn.isNull() && !ctn.getConst<bool>())
return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
}
}
- if (ArithEntail::check(node[2], true))
+ if (d_arithEntail.check(node[2], true))
{
// y>0 implies indexof( x, x, y ) --> -1
Node negone = nm->mkConst(Rational(-1));
{
if (Word::isEmpty(node[1]))
{
- if (ArithEntail::check(len0, node[2]) && ArithEntail::check(node[2]))
+ if (d_arithEntail.check(len0, node[2]) && d_arithEntail.check(node[2]))
{
// len(x)>=z ^ z >=0 implies indexof( x, "", z ) ---> z
return returnRewrite(node, node[2], Rewrite::IDOF_EMP_IDOF);
}
}
- if (ArithEntail::check(len1, len0m2, true))
+ if (d_arithEntail.check(len1, len0m2, true))
{
// len(x)-z < len(y) implies indexof( x, y, z ) ----> -1
Node negone = nm->mkConst(Rational(-1));
}
// Strip components from the beginning that are guaranteed not to match
- if (StringsEntail::stripConstantEndpoints(
+ if (d_stringsEntail.stripConstantEndpoints(
children0, children1, nb, ne, 1))
{
// str.indexof(str.++("AB", x, "C"), "C", 0) --->
// (str.indexof t "" n) is not rewritten to something other than -1 when n
// is beyond the length of t. This is not required for the above rewrites,
// which only apply when n=0.
- if (ArithEntail::check(node[2]) && ArithEntail::check(len0, node[2]))
+ if (d_arithEntail.check(node[2]) && d_arithEntail.check(len0, node[2]))
{
// strip symbolic length
Node new_len = node[2];
std::vector<Node> nr;
- if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
+ if (d_stringsEntail.stripSymbolicLength(children0, nr, 1, new_len))
{
// For example:
// z>=0 and z>str.len( x1 ) and str.contains( x2, y )-->true
{
Node new_len = node[2];
std::vector<Node> nr;
- if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
+ if (d_stringsEntail.stripSymbolicLength(children0, nr, 1, new_len))
{
// Normalize the string before the start index.
//
{
std::vector<Node> cb;
std::vector<Node> ce;
- if (StringsEntail::stripConstantEndpoints(children0, children1, cb, ce, -1))
+ if (d_stringsEntail.stripConstantEndpoints(
+ children0, children1, cb, ce, -1))
{
Node ret = utils::mkConcat(children0, stype);
ret = nm->mkNode(STRING_INDEXOF, ret, node[1], node[2]);
Node zero = nm->mkConst(Rational(0));
Node slen = nm->mkNode(STRING_LENGTH, s);
- if (ArithEntail::check(zero, n, true) || ArithEntail::check(n, slen, true))
+ if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true))
{
Node ret = nm->mkConst(Rational(-1));
return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX);
return returnRewrite(node, ret, Rewrite::INDEXOF_RE_EVAL);
}
- if (ArithEntail::check(n, zero) && ArithEntail::check(slen, n))
+ if (d_arithEntail.check(n, zero) && d_arithEntail.check(slen, n))
{
String emptyStr("");
if (RegExpEntail::testConstStringInRegExp(emptyStr, 0, r))
// ( len( y )>=len(x) ) => str.replace( x, y, x ) ---> x
Node l0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
- if (ArithEntail::check(l1, l0))
+ if (d_arithEntail.check(l1, l0))
{
return returnRewrite(node, node[0], Rewrite::RPL_RPL_LEN_ID);
}
// (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
// if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
- if (StringsEntail::checkLengthOne(node[0]))
+ if (d_stringsEntail.checkLengthOne(node[0]))
{
Node empty = Word::mkEmptyWord(stype);
Node rn1 = Rewriter::rewrite(
if (cmp_conr != cmp_con)
{
- if (StringsEntail::checkNonEmpty(node[1]))
+ if (d_stringsEntail.checkNonEmpty(node[1]))
{
// pull endpoints that can be stripped
// for example,
// str.++( "b", str.replace( x, "a", y ), "b" )
std::vector<Node> cb;
std::vector<Node> ce;
- if (StringsEntail::stripConstantEndpoints(children0, children1, cb, ce))
+ if (d_stringsEntail.stripConstantEndpoints(children0, children1, cb, ce))
{
std::vector<Node> cc;
cc.insert(cc.end(), cb.begin(), cb.end());
Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
// Check len(t) + j > len(x) + 1
- if (ArithEntail::check(maxLen1, len0_1, true))
+ if (d_arithEntail.check(maxLen1, len0_1, true))
{
children1.push_back(nm->mkNode(
kind::STRING_SUBSTR,
// (str.len w) >= (str.len z)
Node wlen = nm->mkNode(kind::STRING_LENGTH, w);
Node zlen = nm->mkNode(kind::STRING_LENGTH, z);
- if (ArithEntail::check(wlen, zlen))
+ if (d_arithEntail.check(wlen, zlen))
{
// w != z
Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z));
// str.replace( x ++ y ++ x ++ y, "A", z ) -->
// str.replace( x ++ y, "A", z ) ++ x ++ y
// since if "A" occurs in x ++ y ++ x ++ y, then it must occur in x ++ y.
- if (StringsEntail::checkLengthOne(node[1]))
+ if (d_stringsEntail.checkLengthOne(node[1]))
{
Node lastLhs;
unsigned lastCheckIndex = 0;
if (node[0] == node[1])
{
// only holds for replaceall if non-empty
- if (nk == STRING_REPLACE || StringsEntail::checkNonEmpty(node[1]))
+ if (nk == STRING_REPLACE || d_stringsEntail.checkNonEmpty(node[1]))
{
return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
}
// Check if we can turn the prefix/suffix into equalities by showing that the
// prefix/suffix is at least as long as the string
- Node eqs = StringsEntail::inferEqsFromContains(n[1], n[0]);
+ Node eqs = d_stringsEntail.inferEqsFromContains(n[1], n[0]);
if (!eqs.isNull())
{
return returnRewrite(n, eqs, Rewrite::SUF_PREFIX_TO_EQS);
#include <vector>
#include "expr/node.h"
+#include "theory/strings/arith_entail.h"
#include "theory/strings/rewrites.h"
#include "theory/strings/sequences_stats.h"
#include "theory/strings/strings_entail.h"
class SequencesRewriter : public TheoryRewriter
{
public:
- SequencesRewriter(HistogramStat<Rewrite>* statistics);
+ SequencesRewriter(Rewriter* r, HistogramStat<Rewrite>* statistics);
+ /** The underlying entailment utilities */
+ ArithEntail& getArithEntail();
+ StringsEntail& getStringsEntail();
protected:
/** rewrite regular expression concatenation
Node postProcessRewrite(Node node, Node ret);
/** Reference to the rewriter statistics. */
HistogramStat<Rewrite>* d_statistics;
-
+ /** The arithmetic entailment module */
+ ArithEntail d_arithEntail;
/** Instance of the entailment checker for strings. */
StringsEntail d_stringsEntail;
}; /* class SequencesRewriter */
namespace theory {
namespace strings {
-StringsEntail::StringsEntail(SequencesRewriter& rewriter) : d_rewriter(rewriter)
+StringsEntail::StringsEntail(Rewriter* r,
+ ArithEntail& aent,
+ SequencesRewriter& rewriter)
+ : d_rr(r), d_arithEntail(aent), d_rewriter(rewriter)
{
}
pos = new_pos + Word::getLength(n[i]);
}
}
- else if (n[i].getKind() == STRING_ITOS && ArithEntail::check(n[i][0]))
+ else if (n[i].getKind() == STRING_ITOS && d_arithEntail.check(n[i][0]))
{
Assert(c.getType().isString()); // string-only
const std::vector<unsigned>& tvec = c.getConst<String>().getVec();
if (n1[sindex_use].isConst())
{
// could strip part of a constant
- Node lowerBound = ArithEntail::getConstantBound(Rewriter::rewrite(curr));
+ Node lowerBound = d_arithEntail.getConstantBound(d_rr->rewrite(curr));
if (!lowerBound.isNull())
{
Assert(lowerBound.isConst());
Rational lbr = lowerBound.getConst<Rational>();
if (lbr.sgn() > 0)
{
- Assert(ArithEntail::check(curr, true));
+ Assert(d_arithEntail.check(curr, true));
Node s = n1[sindex_use];
size_t slen = Word::getLength(s);
Node ncl = nm->mkConst(cvc5::Rational(slen));
Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
- next_s = Rewriter::rewrite(next_s);
+ next_s = d_rr->rewrite(next_s);
Assert(next_s.isConst());
// we can remove the entire constant
if (next_s.getConst<Rational>().sgn() >= 0)
{
- curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, ncl));
+ curr = d_rr->rewrite(nm->mkNode(MINUS, curr, ncl));
success = true;
sindex++;
}
// lower bound minus the length of a concrete string is negative,
// hence lowerBound cannot be larger than long max
Assert(lbr < Rational(String::maxSize()));
- curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, lowerBound));
+ curr = d_rr->rewrite(nm->mkNode(MINUS, curr, lowerBound));
uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
Assert(lbsize < slen);
if (dir == 1)
}
ret = true;
}
- Assert(ArithEntail::check(curr));
+ Assert(d_arithEntail.check(curr));
}
else
{
MINUS,
curr,
NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use]));
- next_s = Rewriter::rewrite(next_s);
- if (ArithEntail::check(next_s))
+ next_s = d_rr->rewrite(next_s);
+ if (d_arithEntail.check(next_s))
{
success = true;
curr = next_s;
}
else if (!n1re.isNull())
{
- n1[i] = Rewriter::rewrite(
+ n1[i] = d_rr->rewrite(
NodeManager::currentNM()->mkNode(STRING_CONCAT, n1[i], n1re));
}
if (remainderDir != 1)
}
else if (!n1rb.isNull())
{
- n1[i] = Rewriter::rewrite(
+ n1[i] = d_rr->rewrite(
NodeManager::currentNM()->mkNode(STRING_CONCAT, n1rb, n1[i]));
}
}
{
// To be a suffix, start + length must be greater than
// or equal to the length of the string.
- success = ArithEntail::check(end_pos, len_n2s);
+ success = d_arithEntail.check(end_pos, len_n2s);
}
else if (dir == -1)
{
{
// we can only compute the remainder if start_pos and end_pos
// are known to be non-negative.
- if (!ArithEntail::check(start_pos)
- || !ArithEntail::check(end_pos))
+ if (!d_arithEntail.check(start_pos)
+ || !d_arithEntail.check(end_pos))
{
return false;
}
if (fullRewriter)
{
- ctn = Rewriter::rewrite(ctn);
+ ctn = d_rr->rewrite(ctn);
}
else
{
bool StringsEntail::checkNonEmpty(Node a)
{
Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a);
- len = Rewriter::rewrite(len);
- return ArithEntail::check(len, true);
+ len = d_rr->rewrite(len);
+ return d_arithEntail.check(len, true);
}
bool StringsEntail::checkLengthOne(Node s, bool strict)
NodeManager* nm = NodeManager::currentNM();
Node one = nm->mkConst(Rational(1));
Node len = nm->mkNode(STRING_LENGTH, s);
- len = Rewriter::rewrite(len);
- return ArithEntail::check(one, len)
- && (!strict || ArithEntail::check(len, true));
+ len = d_rr->rewrite(len);
+ return d_arithEntail.check(one, len)
+ && (!strict || d_arithEntail.check(len, true));
}
bool StringsEntail::checkMultisetSubset(Node a, Node b)
n = n[2];
break;
}
-
if (checkLengthOne(n[0]) && Word::isEmpty(n[2]))
{
// (str.replace "A" x "") --> "A"
// str.len(yn) (where y = y1 ++ ... ++ yn) while keeping the inequality
// true. The terms that can have length zero without making the inequality
// false must be all be empty if (str.contains x y) is true.
- if (!ArithEntail::inferZerosInSumGeq(xLen, yLens, zeroLens))
+ if (!d_arithEntail.inferZerosInSumGeq(xLen, yLens, zeroLens))
{
// We could not prove that the inequality holds
return Node::null();
#include <vector>
#include "expr/node.h"
+#include "theory/strings/arith_entail.h"
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace strings {
class SequencesRewriter;
class StringsEntail
{
public:
- StringsEntail(SequencesRewriter& rewriter);
+ StringsEntail(Rewriter* r, ArithEntail& aent, SequencesRewriter& rewriter);
/** can constant contain list
* return true if constant c can contain the list l in order
/** can constant contain concat
* same as above but with n = str.++( l ) instead of l
*/
- static bool canConstantContainConcat(Node c, Node n, int& firstc, int& lastc);
+ bool canConstantContainConcat(Node c, Node n, int& firstc, int& lastc);
/** strip symbolic length
*
* nr is updated to { "abc", y }
* curr is updated to str.len(y)+1
*/
- static bool stripSymbolicLength(std::vector<Node>& n1,
- std::vector<Node>& nr,
- int dir,
- Node& curr,
- bool strict = false);
+ bool stripSymbolicLength(std::vector<Node>& n1,
+ std::vector<Node>& nr,
+ int dir,
+ Node& curr,
+ bool strict = false);
/** component contains
* This function is used when rewriting str.contains( t1, t2 ), where
* n1 is the vector form of t1
* Checks whether string a is entailed to be non-empty. Is equivalent to
* the call checkArithEntail( len( a ), true ).
*/
- static bool checkNonEmpty(Node a);
+ bool checkNonEmpty(Node a);
/**
* Checks whether string has at most/exactly length one. Length one strings
* at most length one
* @return True if the string has at most/exactly length one, false otherwise
*/
- static bool checkLengthOne(Node s, bool strict = false);
+ bool checkLengthOne(Node s, bool strict = false);
/**
* Checks whether it is always true that `a` is a strict subset of `b` in the
* getStringOrEmpty( (str.substr "ABC" x y) ) --> (str.substr "ABC" x y)
* because the function could not compute a simpler
*/
- static Node getStringOrEmpty(Node n);
+ Node getStringOrEmpty(Node n);
/**
* Infers a conjunction of equalities that correspond to (str.contains x y)
* y) if the function can infer that str.len(y) >= str.len(x) but cannot
* infer that any of the yi must be empty.
*/
- static Node inferEqsFromContains(Node x, Node y);
+ Node inferEqsFromContains(Node x, Node y);
private:
/** component contains base
static Node getMultisetApproximation(Node a);
private:
+ /** Pointer to the full rewriter */
+ Rewriter* d_rr;
+ /** The arithmetic entailment module */
+ ArithEntail& d_arithEntail;
/**
* Reference to the sequences rewriter that owns this `StringsEntail`
* instance.
namespace theory {
namespace strings {
-StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
- : SequencesRewriter(statistics)
+StringsRewriter::StringsRewriter(Rewriter* r,
+ HistogramStat<Rewrite>* statistics)
+ : SequencesRewriter(r, statistics)
{
}
class StringsRewriter : public SequencesRewriter
{
public:
- StringsRewriter(HistogramStat<Rewrite>* statistics);
+ StringsRewriter(Rewriter* r, HistogramStat<Rewrite>* statistics);
RewriteResponse postRewrite(TNode node) override;
d_extTheoryCb(),
d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
- d_rewriter(&d_statistics.d_rewrites),
+ d_rewriter(env.getRewriter(), &d_statistics.d_rewrites),
d_bsolver(env, d_state, d_im),
d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
d_esolver(env,
TEST_F(TestPPWhiteForeignTheoryRewrite, simplify)
{
+ ForeignTheoryRewriter ftr(d_smtEngine->getEnv());
std::cout << "len(x) >= 0 is simplified to true" << std::endl;
Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType());
Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x);
Node zero = d_nodeManager->mkConst<Rational>(0);
Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero);
Node tt = d_nodeManager->mkConst<bool>(true);
- Node simplified1 = ForeignTheoryRewrite::foreignRewrite(geq1);
+ Node simplified1 = ftr.foreignRewrite(geq1);
ASSERT_EQ(simplified1, tt);
std::cout << "len(x) >= n is not simplified to true" << std::endl;
Node n = d_nodeManager->mkVar("n", d_nodeManager->integerType());
Node geq2 = d_nodeManager->mkNode(kind::GEQ, len_x, n);
- Node simplified2 = ForeignTheoryRewrite::foreignRewrite(geq2);
+ Node simplified2 = ftr.foreignRewrite(geq2);
ASSERT_NE(simplified2, tt);
}
TestSmt::SetUp();
Options opts;
d_rewriter = d_smtEngine->getRewriter();
+ d_seqRewriter.reset(new SequencesRewriter(d_rewriter, nullptr));
}
Rewriter* d_rewriter;
+ std::unique_ptr<SequencesRewriter> d_seqRewriter;
void inNormalForm(Node t)
{
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one)
{
+ StringsEntail& se = d_seqRewriter->getStringsEntail();
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
Node three = d_nodeManager->mkConst(Rational(3));
Node i = d_nodeManager->mkVar("i", intType);
- ASSERT_TRUE(StringsEntail::checkLengthOne(a));
- ASSERT_TRUE(StringsEntail::checkLengthOne(a, true));
+ ASSERT_TRUE(se.checkLengthOne(a));
+ ASSERT_TRUE(se.checkLengthOne(a, true));
Node substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one);
- ASSERT_TRUE(StringsEntail::checkLengthOne(substr));
- ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true));
+ ASSERT_TRUE(se.checkLengthOne(substr));
+ ASSERT_FALSE(se.checkLengthOne(substr, true));
substr =
d_nodeManager->mkNode(kind::STRING_SUBSTR,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x),
zero,
one);
- ASSERT_TRUE(StringsEntail::checkLengthOne(substr));
- ASSERT_TRUE(StringsEntail::checkLengthOne(substr, true));
+ ASSERT_TRUE(se.checkLengthOne(substr));
+ ASSERT_TRUE(se.checkLengthOne(substr, true));
substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, two);
- ASSERT_FALSE(StringsEntail::checkLengthOne(substr));
- ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true));
+ ASSERT_FALSE(se.checkLengthOne(substr));
+ ASSERT_FALSE(se.checkLengthOne(substr, true));
}
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith)
{
+ ArithEntail& ae = d_seqRewriter->getArithEntail();
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
Node substr_z = d_nodeManager->mkNode(
kind::STRING_LENGTH,
d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one));
- ASSERT_TRUE(ArithEntail::check(one, substr_z));
+ ASSERT_TRUE(ae.check(one, substr_z));
// (str.len (str.substr z n 1)) >= 1 ---> false
- ASSERT_FALSE(ArithEntail::check(substr_z, one));
+ ASSERT_FALSE(ae.check(substr_z, one));
}
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
{
+ ArithEntail& ae = d_seqRewriter->getArithEntail();
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero));
// x + (str.len y) = 0 |= 0 >= x --> true
- ASSERT_TRUE(
- ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, false));
+ ASSERT_TRUE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, false));
// x + (str.len y) = 0 |= 0 > x --> false
- ASSERT_FALSE(
- ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true));
+ ASSERT_FALSE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true));
Node x_plus_slen_y_plus_z_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode(
kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
// x + (str.len y) + z = 0 |= 0 > x --> false
- ASSERT_FALSE(ArithEntail::checkWithAssumption(
- x_plus_slen_y_plus_z_eq_zero, zero, x, true));
+ ASSERT_FALSE(
+ ae.checkWithAssumption(x_plus_slen_y_plus_z_eq_zero, zero, x, true));
Node x_plus_slen_y_plus_slen_y_eq_zero =
d_rewriter->rewrite(d_nodeManager->mkNode(
zero));
// x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true
- ASSERT_TRUE(ArithEntail::checkWithAssumption(
+ ASSERT_TRUE(ae.checkWithAssumption(
x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
Node five = d_nodeManager->mkConst(Rational(5));
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
// x + 5 < 6 |= 0 >= x --> true
- ASSERT_TRUE(
- ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, false));
+ ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_six, zero, x, false));
// x + 5 < 6 |= 0 > x --> false
- ASSERT_TRUE(
- !ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, true));
+ ASSERT_TRUE(!ae.checkWithAssumption(x_plus_five_lt_six, zero, x, true));
Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x);
Node x_plus_five_lt_five =
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
// x + 5 < 5 |= -x >= 0 --> true
- ASSERT_TRUE(ArithEntail::checkWithAssumption(
- x_plus_five_lt_five, neg_x, zero, false));
+ ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_five, neg_x, zero, false));
// x + 5 < 5 |= 0 > x --> true
- ASSERT_TRUE(
- ArithEntail::checkWithAssumption(x_plus_five_lt_five, zero, x, false));
+ ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_five, zero, x, false));
// 0 < x |= x >= (str.len (int.to.str x))
Node assm = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, zero, x));
- ASSERT_TRUE(ArithEntail::checkWithAssumption(
+ ASSERT_TRUE(ae.checkWithAssumption(
assm,
x,
d_nodeManager->mkNode(kind::STRING_LENGTH,
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
{
+ StringsRewriter sr(d_rewriter, nullptr);
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
// (str.substr "A" x x) --> ""
Node n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, x);
- Node res = StringsRewriter(nullptr).rewriteSubstr(n);
+ Node res = sr.rewriteSubstr(n);
ASSERT_EQ(res, empty);
// (str.substr "A" (+ x 1) x) -> ""
a,
d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
x);
- res = StringsRewriter(nullptr).rewriteSubstr(n);
+ res = sr.rewriteSubstr(n);
ASSERT_EQ(res, empty);
// (str.substr "A" (+ x (str.len s2)) x) -> ""
d_nodeManager->mkNode(
kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
x);
- res = StringsRewriter(nullptr).rewriteSubstr(n);
+ res = sr.rewriteSubstr(n);
ASSERT_EQ(res, empty);
// (str.substr "A" x y) -> (str.substr "A" x y)
n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y);
- res = StringsRewriter(nullptr).rewriteSubstr(n);
+ res = sr.rewriteSubstr(n);
ASSERT_EQ(res, n);
// (str.substr "ABCD" (+ x 3) x) -> ""
abcd,
d_nodeManager->mkNode(kind::PLUS, x, three),
x);
- res = StringsRewriter(nullptr).rewriteSubstr(n);
+ res = sr.rewriteSubstr(n);
ASSERT_EQ(res, empty);
// (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
n = d_nodeManager->mkNode(
kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
- res = StringsRewriter(nullptr).rewriteSubstr(n);
+ res = sr.rewriteSubstr(n);
ASSERT_EQ(res, n);
// (str.substr (str.substr s x x) x x) -> ""
TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains)
{
+ StringsEntail& se = d_seqRewriter->getStringsEntail();
TypeNode strType = d_nodeManager->stringType();
Node empty = d_nodeManager->mkConst(::cvc5::String(""));
d_nodeManager->mkNode(kind::AND,
d_nodeManager->mkNode(kind::EQUAL, empty, x),
d_nodeManager->mkNode(kind::EQUAL, empty, y));
- sameNormalForm(StringsEntail::inferEqsFromContains(empty, xy), empty_x_y);
+ sameNormalForm(se.inferEqsFromContains(empty, xy), empty_x_y);
// inferEqsFromContains(x, (str.++ x y)) returns false
Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, {b, y, x, a});
- sameNormalForm(StringsEntail::inferEqsFromContains(x, bxya), f);
+ sameNormalForm(se.inferEqsFromContains(x, bxya), f);
// inferEqsFromContains(x, y) returns null
- Node n = StringsEntail::inferEqsFromContains(x, y);
+ Node n = se.inferEqsFromContains(x, y);
ASSERT_TRUE(n.isNull());
// inferEqsFromContains(x, x) returns something equivalent to (= x x)
Node eq_x_x = d_nodeManager->mkNode(kind::EQUAL, x, x);
- sameNormalForm(StringsEntail::inferEqsFromContains(x, x), eq_x_x);
+ sameNormalForm(se.inferEqsFromContains(x, x), eq_x_x);
// inferEqsFromContains((str.replace x "B" "A"), x) returns something
// equivalent to (= (str.replace x "B" "A") x)
Node repl = d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a);
Node eq_repl_x = d_nodeManager->mkNode(kind::EQUAL, repl, x);
- sameNormalForm(StringsEntail::inferEqsFromContains(repl, x), eq_repl_x);
+ sameNormalForm(se.inferEqsFromContains(repl, x), eq_repl_x);
// inferEqsFromContains(x, (str.replace x "B" "A")) returns something
// equivalent to (= (str.replace x "B" "A") x)
Node eq_x_repl = d_nodeManager->mkNode(kind::EQUAL, x, repl);
- sameNormalForm(StringsEntail::inferEqsFromContains(x, repl), eq_x_repl);
+ sameNormalForm(se.inferEqsFromContains(x, repl), eq_x_repl);
}
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix)
TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints)
{
+ StringsEntail& se = d_seqRewriter->getStringsEntail();
TypeNode intType = d_nodeManager->integerType();
TypeNode strType = d_nodeManager->stringType();
std::vector<Node> n2 = {a};
std::vector<Node> nb;
std::vector<Node> ne;
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, 0);
ASSERT_FALSE(res);
}
std::vector<Node> n2 = {a, d_nodeManager->mkNode(kind::STRING_ITOS, n)};
std::vector<Node> nb;
std::vector<Node> ne;
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, 0);
ASSERT_FALSE(res);
}
std::vector<Node> ne;
std::vector<Node> n1r = {cd};
std::vector<Node> nbr = {ab};
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, 1);
ASSERT_TRUE(res);
ASSERT_EQ(n1, n1r);
ASSERT_EQ(nb, nbr);
std::vector<Node> ne;
std::vector<Node> n1r = {c, x};
std::vector<Node> nbr = {ab};
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, 1);
ASSERT_TRUE(res);
ASSERT_EQ(n1, n1r);
ASSERT_EQ(nb, nbr);
std::vector<Node> ne;
std::vector<Node> n1r = {a};
std::vector<Node> ner = {bc};
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, -1);
ASSERT_TRUE(res);
ASSERT_EQ(n1, n1r);
ASSERT_EQ(ne, ner);
std::vector<Node> ne;
std::vector<Node> n1r = {x, a};
std::vector<Node> ner = {bc};
- bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
+ bool res = se.stripConstantEndpoints(n1, n2, nb, ne, -1);
ASSERT_TRUE(res);
ASSERT_EQ(n1, n1r);
ASSERT_EQ(ne, ner);
projects / cvc5.git / commitdiff