Towards support for the strings standard.
This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).
This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.
Also fixes #4161.
util/proof.h
util/rational_cln_imp.h
util/rational_gmp_imp.h
+ util/regexp.h
util/resource_manager.h
util/result.h
util/sexpr.h
{REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
{REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
{REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
+ {REGEXP_REPEAT, CVC4::Kind::REGEXP_REPEAT},
{REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
{REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
{REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
{CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
{CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
{CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
+ {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT},
{CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
{CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
{CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
kind,
*mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
break;
+ case REGEXP_REPEAT:
+ res = Op(kind,
+ *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
+ .d_expr.get());
+ break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
<< "operator kind with uint32_t argument";
CVC4::FloatingPointToFPGeneric(arg1, arg2))
.d_expr.get());
break;
+ case REGEXP_LOOP:
+ res = Op(kind,
+ *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
+ .d_expr.get());
+ break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
<< "operator kind with two uint32_t arguments";
*/
REGEXP_RANGE,
/**
- * Regexp loop.
- * Parameters: 2 (3)
- * -[1]: Term of sort RegExp
- * -[2]: Lower bound for the number of repetitions of the first argument
- * -[3]: Upper bound for the number of repetitions of the first argument
+ * Operator for regular expression repeat.
+ * Parameters: 1
+ * -[1]: The number of repetitions
* Create with:
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, Term child1, Term child2, Term child3)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkOp(Kind kind, uint32_t param)
+ *
+ * Apply regular expression loop.
+ * Parameters: 2
+ * -[1]: Op of kind REGEXP_REPEAT
+ * -[2]: Term of regular expression sort
+ * Create with:
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
+ */
+ REGEXP_REPEAT,
+ /**
+ * Operator for regular expression loop, from lower bound to upper bound
+ * number of repetitions.
+ * Parameters: 2
+ * -[1]: The lower bound
+ * -[2]: The upper bound
+ * Create with:
+ * mkOp(Kind kind, uint32_t param, uint32_t param)
+ *
+ * Apply regular expression loop.
+ * Parameters: 2
+ * -[1]: Op of kind REGEXP_LOOP
+ * -[2]: Term of regular expression sort
+ * Create with:
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
REGEXP_LOOP,
/**
${CMAKE_CURRENT_BINARY_DIR}/RecordUpdate.java
${CMAKE_CURRENT_BINARY_DIR}/RecordUpdateHashFunction.java
${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java
+ ${CMAKE_CURRENT_BINARY_DIR}/RegExpLoop.java
+ ${CMAKE_CURRENT_BINARY_DIR}/RegExpRepeat.java
${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java
${CMAKE_CURRENT_BINARY_DIR}/Result.java
${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
%include "util/cardinality.i"
%include "util/hash.i"
%include "util/proof.i"
+%include "util/regexp.i"
%include "util/result.i"
%include "util/sexpr.i"
%include "util/statistics.i"
{ f = MK_TERM(CVC4::api::REGEXP_OPT, f); }
| REGEXP_RANGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_TERM(CVC4::api::REGEXP_RANGE, f, f2); }
- | REGEXP_LOOP_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
- { f = MK_TERM(CVC4::api::REGEXP_LOOP, f, f2, f3); }
+ | REGEXP_LOOP_TOK LPAREN formula[f] COMMA lo=numeral COMMA hi=numeral RPAREN
+ {
+ api::Op lop = SOLVER->mkOp(CVC4::api::REGEXP_LOOP, lo, hi);
+ f = MK_TERM(lop, f);
+ }
| REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN
{ f = MK_TERM(CVC4::api::REGEXP_COMPLEMENT, f); }
| REGEXP_EMPTY_TOK
addOperator(api::REGEXP_STAR, "re.*");
addOperator(api::REGEXP_PLUS, "re.+");
addOperator(api::REGEXP_OPT, "re.opt");
+ addIndexedOperator(api::REGEXP_REPEAT, api::REGEXP_REPEAT, "re.^");
+ addIndexedOperator(api::REGEXP_LOOP, api::REGEXP_LOOP, "re.loop");
addOperator(api::REGEXP_RANGE, "re.range");
- addOperator(api::REGEXP_LOOP, "re.loop");
addOperator(api::REGEXP_COMPLEMENT, "re.comp");
addOperator(api::REGEXP_DIFF, "re.diff");
addOperator(api::STRING_LT, "str.<");
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
-operator REGEXP_LOOP 2:3 "regexp loop"
operator REGEXP_COMPLEMENT 1 "regexp complement"
operator REGEXP_EMPTY 0 "regexp empty"
operator REGEXP_SIGMA 0 "regexp all characters"
+constant REGEXP_REPEAT_OP \
+ ::CVC4::RegExpRepeat \
+ ::CVC4::RegExpRepeatHashFunction \
+ "util/regexp.h" \
+ "operator for regular expression repeat; payload is an instance of the CVC4::RegExpRepeat class"
+parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term"
+
+constant REGEXP_LOOP_OP \
+ ::CVC4::RegExpLoop \
+ ::CVC4::RegExpLoopHashFunction \
+ "util/regexp.h" \
+ "operator for regular expression loop; payload is an instance of the CVC4::RegExpLoop class"
+parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term"
+
#internal
operator REGEXP_RV 1 "regexp rv (internal use only)"
typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
-typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>"
+typerule REGEXP_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
+typerule REGEXP_REPEAT "SimpleTypeRule<RRegExp, ARegExp>"
+typerule REGEXP_LOOP_OP "SimpleTypeRule<RBuiltinOperator>"
+typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
{
d_constCache[cur] = RE_C_UNKNOWN;
visit.push_back(cur);
- if (ck == REGEXP_LOOP)
- {
- // only add the first child of loop
- visit.push_back(cur[0]);
- }
- else
- {
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
+ visit.insert(visit.end(), cur.begin(), cur.end());
}
}
else if (it->second == RE_C_UNKNOWN)
break;
}
case kind::REGEXP_LOOP: {
- if(r[1] == d_zero) {
+ uint32_t lo = utils::getLoopMinOccurrences(r);
+ if (lo == 0)
+ {
ret = 1;
} else {
ret = delta(r[0], exp);
break;
}
case kind::REGEXP_LOOP: {
- if(r[1] == r[2] && r[1] == d_zero) {
+ uint32_t l = utils::getLoopMinOccurrences(r);
+ uint32_t u = utils::getLoopMaxOccurrences(r);
+ if (l == u && l == 0)
+ {
ret = 2;
//retNode = d_emptyRegexp;
} else {
Node dc;
ret = derivativeS(r[0], c, dc);
if(dc==d_emptyRegexp) {
- unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
- unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
- Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0],
- NodeManager::currentNM()->mkConst(CVC4::Rational(l==0? 0 : (l-1))),
- NodeManager::currentNM()->mkConst(CVC4::Rational(u-1)));
+ Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1));
+ Node r2 = nm->mkNode(REGEXP_LOOP, lop, r[0]);
retNode = dc==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r2 );
} else {
retNode = d_emptyRegexp;
break;
}
case kind::REGEXP_LOOP: {
- if(r[1] == r[2] && r[1] == d_zero) {
+ uint32_t l = utils::getLoopMinOccurrences(r);
+ uint32_t u = utils::getLoopMaxOccurrences(r);
+ if (l == u || l == 0)
+ {
retNode = d_emptyRegexp;
} else {
Node dc = derivativeSingle(r[0], c);
if(dc != d_emptyRegexp) {
- unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
- unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
- Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0],
- NodeManager::currentNM()->mkConst(CVC4::Rational(l==0? 0 : (l-1))),
- NodeManager::currentNM()->mkConst(CVC4::Rational(u-1)));
+ Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1));
+ Node r2 = nm->mkNode(REGEXP_LOOP, lop, r[0]);
retNode = dc==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r2 );
} else {
retNode = d_emptyRegexp;
{
return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
}
- TNode n1 = node[1];
NodeManager* nm = NodeManager::currentNM();
CVC4::Rational rMaxInt(String::maxSize());
- AlwaysAssert(n1.isConst()) << "re.loop contains non-constant integer (1).";
- AlwaysAssert(n1.getConst<Rational>().sgn() >= 0)
- << "Negative integer in string REGEXP_LOOP (1)";
- Assert(n1.getConst<Rational>() <= rMaxInt)
- << "Exceeded UINT32_MAX in string REGEXP_LOOP (1)";
- uint32_t l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
+ uint32_t l = utils::getLoopMinOccurrences(node);
std::vector<Node> vec_nodes;
for (unsigned i = 0; i < l; i++)
{
vec_nodes.push_back(r);
}
- if (node.getNumChildren() == 3)
+ Node n =
+ vec_nodes.size() == 0
+ ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))
+ : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes);
+ uint32_t u = utils::getLoopMaxOccurrences(node);
+ if (u < l)
{
- TNode n2 = Rewriter::rewrite(node[2]);
- Node n =
- vec_nodes.size() == 0
- ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))
- : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes);
- AlwaysAssert(n2.isConst()) << "re.loop contains non-constant integer (2).";
- AlwaysAssert(n2.getConst<Rational>().sgn() >= 0)
- << "Negative integer in string REGEXP_LOOP (2)";
- Assert(n2.getConst<Rational>() <= rMaxInt)
- << "Exceeded UINT32_MAX in string REGEXP_LOOP (2)";
- uint32_t u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
- if (u <= l)
- {
- retNode = n;
- }
- else
- {
- std::vector<Node> vec2;
- vec2.push_back(n);
- TypeNode rtype = nm->regExpType();
- for (unsigned j = l; j < u; j++)
- {
- vec_nodes.push_back(r);
- n = utils::mkConcat(vec_nodes, rtype);
- vec2.push_back(n);
- }
- retNode = nm->mkNode(REGEXP_UNION, vec2);
- }
+ std::vector<Node> nvec;
+ retNode = nm->mkNode(REGEXP_EMPTY, nvec);
+ }
+ else if (u == l)
+ {
+ retNode = n;
}
else
{
- Node rest = nm->mkNode(REGEXP_STAR, r);
- retNode = vec_nodes.size() == 0
- ? rest
- : vec_nodes.size() == 1
- ? nm->mkNode(REGEXP_CONCAT, r, rest)
- : nm->mkNode(REGEXP_CONCAT,
- nm->mkNode(REGEXP_CONCAT, vec_nodes),
- rest);
+ std::vector<Node> vec2;
+ vec2.push_back(n);
+ TypeNode rtype = nm->regExpType();
+ for (uint32_t j = l; j < u; j++)
+ {
+ vec_nodes.push_back(r);
+ n = utils::mkConcat(vec_nodes, rtype);
+ vec2.push_back(n);
+ }
+ retNode = nm->mkNode(REGEXP_UNION, vec2);
}
Trace("strings-lp") << "Strings::lp " << node << " => " << retNode
<< std::endl;
{
retNode = rewriteLoopRegExp(node);
}
+ else if (nk == REGEXP_REPEAT)
+ {
+ // ((_ re.^ n) R) --> ((_ re.loop n n) R)
+ unsigned r = utils::getRepeatAmount(node);
+ Node lop = nm->mkConst(RegExpLoop(r, r));
+ retNode = nm->mkNode(REGEXP_LOOP, lop, node[0]);
+ }
Trace("strings-postrewrite")
<< "Strings::postRewrite returning " << retNode << std::endl;
return tn;
}
+unsigned getRepeatAmount(TNode node)
+{
+ Assert(node.getKind() == REGEXP_REPEAT);
+ return node.getOperator().getConst<RegExpRepeat>().d_repeatAmount;
+}
+
+unsigned getLoopMaxOccurrences(TNode node)
+{
+ Assert(node.getKind() == REGEXP_LOOP);
+ return node.getOperator().getConst<RegExpLoop>().d_loopMaxOcc;
+}
+
+unsigned getLoopMinOccurrences(TNode node)
+{
+ Assert(node.getKind() == REGEXP_LOOP);
+ return node.getOperator().getConst<RegExpLoop>().d_loopMinOcc;
+}
+
} // namespace utils
} // namespace strings
} // namespace theory
*/
TypeNode getOwnerStringType(Node n);
+/* Get the number of repetitions for a regexp repeat node */
+unsigned getRepeatAmount(TNode node);
+
+/* Get the maximum occurrences of given regexp loop node. */
+unsigned getLoopMaxOccurrences(TNode node);
+/* Get the minimum occurrences of given regexp loop node. */
+unsigned getLoopMinOccurrences(TNode node);
+
} // namespace utils
} // namespace strings
} // namespace theory
resource_manager.h
result.cpp
result.h
+ regexp.cpp
+ regexp.h
safe_print.cpp
safe_print.h
sampler.cpp
--- /dev/null
+/********************* */
+/*! \file regexp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of data structures for regular expression operators.
+ **/
+
+#include "util/regexp.h"
+
+#include <ostream>
+
+namespace CVC4 {
+
+RegExpRepeat::RegExpRepeat(uint32_t repeatAmount) : d_repeatAmount(repeatAmount) {}
+
+bool RegExpRepeat::operator==(const RegExpRepeat& r) const
+{
+ return d_repeatAmount == r.d_repeatAmount;
+}
+
+RegExpLoop::RegExpLoop(uint32_t l, uint32_t h) : d_loopMinOcc(l), d_loopMaxOcc(h) {}
+
+bool RegExpLoop::operator==(const RegExpLoop& r) const
+{
+ return d_loopMinOcc == r.d_loopMinOcc
+ && d_loopMaxOcc == r.d_loopMaxOcc;
+}
+
+size_t RegExpRepeatHashFunction::operator()(const RegExpRepeat& r) const
+{
+ return r.d_repeatAmount;
+}
+
+size_t RegExpLoopHashFunction::operator()(const RegExpLoop& r) const
+{
+ return r.d_loopMinOcc + r.d_loopMaxOcc;
+}
+
+std::ostream& operator<<(std::ostream& os, const RegExpRepeat& r)
+{
+ return os << r.d_repeatAmount;
+}
+
+std::ostream& operator<<(std::ostream& os, const RegExpLoop& r)
+{
+ return os << "[" << r.d_loopMinOcc << ".." << r.d_loopMaxOcc << "]";
+}
+
+} // namespace CVC4
+
--- /dev/null
+/********************* */
+/*! \file regexp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Data structures for regular expression operators.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__UTIL__REGEXP_H
+#define CVC4__UTIL__REGEXP_H
+
+#include <cstdint>
+#include <iosfwd>
+
+namespace CVC4 {
+
+struct CVC4_PUBLIC RegExpRepeat
+{
+ RegExpRepeat(uint32_t repeatAmount);
+
+ bool operator==(const RegExpRepeat& r) const;
+ /** The amount of repetitions of the regular expression */
+ uint32_t d_repeatAmount;
+};
+
+struct CVC4_PUBLIC RegExpLoop
+{
+ RegExpLoop(uint32_t l, uint32_t h);
+
+ bool operator==(const RegExpLoop& r) const;
+ /** The minimum number of repetitions of the regular expression */
+ uint32_t d_loopMinOcc;
+ /** The maximum number of repetitions of the regular expression */
+ uint32_t d_loopMaxOcc;
+};
+
+/* -----------------------------------------------------------------------
+ ** Hash Function structs
+ * ----------------------------------------------------------------------- */
+
+/*
+ * Hash function for the RegExpRepeat constants.
+ */
+struct CVC4_PUBLIC RegExpRepeatHashFunction
+{
+ size_t operator()(const RegExpRepeat& r) const;
+};
+
+/**
+ * Hash function for the RegExpLoop objects.
+ */
+struct CVC4_PUBLIC RegExpLoopHashFunction
+{
+ size_t operator()(const RegExpLoop& r) const;
+};
+
+/* -----------------------------------------------------------------------
+ ** Output stream
+ * ----------------------------------------------------------------------- */
+
+std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv) CVC4_PUBLIC;
+
+std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv) CVC4_PUBLIC;
+
+} // namespace CVC4
+
+#endif /* CVC4__UTIL__REGEXP_H */
--- /dev/null
+%{
+#include "util/regexp.h"
+%}
+
+%rename(equals) CVC4::RegExpRepeat::operator==(const RegExpRepeat&) const;
+
+%rename(equals) CVC4::RegExpLoop::operator==(const RegExpLoop&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const RegExpRepeat&);
+%ignore CVC4::operator<<(std::ostream&, const RegExpLoop&);
+
+%include "util/regexp.h"
regress0/strings/large-model.smt2
regress0/strings/leadingzero001.smt2
regress0/strings/loop001.smt2
+ regress0/strings/loop-wrong-sem.smt2
regress0/strings/model001.smt2
regress0/strings/model-code-point.smt2
regress0/strings/model-friendly.smt2
(set-info :status sat)
; regex = [\*-,\t\*-\|](.{6,}()?)+
-(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) )
+(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ((_ re.^ 6) re.allchar) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) )
(assert (not (strinre "6O\1\127\n?")))
(check-sat)
--- /dev/null
+(set-logic ALL)
+(set-info :status unsat)
+(assert (str.in.re "" ((_ re.loop 1 0) (str.to.re ""))))
+(check-sat)
(declare-fun root6 () T)
(assert (and
-(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )
-(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )
+(str.in.re root5 ((_ re.loop 4 4) (re.range "0" "9")) )
+(str.in.re (TCb root6) ((_ re.loop 4 4) (re.range "0" "9")) )
) )
(check-sat)
(define-fun stringEval ((?s String)) Bool (str.in.re ?s \r
(re.union \r
(str.to.re "H")\r
-(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range "\1d" "]") (re.range "\ e" "^") ) 2 4 ) ) ) ) )\r
+(re.++ ((_ re.loop 2 2) (str.to.re "{") ) ((_ re.loop 2 4) (re.union re.nostr (re.range "\1d" "]") (re.range "\ e" "^") ) ) ) ) ) )\r
(declare-fun s0() String)\r
(declare-fun s1() String)\r
(declare-fun s2() String)\r
(declare-fun z () String)
(declare-fun w () String)
-(assert (str.in.re x (re.loop (str.to.re "a") 5)))
-(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))
-(assert (str.in.re z (re.loop (str.to.re "c") 5)))
+(assert (str.in.re x ((_ re.^ 5) (str.to.re "a"))))
+(assert (str.in.re y ((_ re.loop 2 5) (str.to.re "b"))))
+(assert (str.in.re z ((_ re.loop 5 15) (str.to.re "c"))))
(assert (> (str.len z) 7))
-(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))
+(assert (str.in.re w ((_ re.loop 2 7) (str.to.re "b"))))
(assert (> (str.len w) 2))
(assert (< (str.len w) 5))
; EXPECT: sat
(set-logic QF_SLIA)
(declare-const x String)
-(assert (str.in.re x (re.loop (re.range "0" "9") 12 12)))
+(assert (str.in.re x ((_ re.loop 12 12) (re.range "0" "9"))))
(assert (str.in.re x (re.++ (re.* re.allchar) (str.to.re "01") (re.* re.allchar))))
(check-sat)
projects / cvc5.git / commitdiff