diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-30 16:29:23 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-30 16:29:23 -0500 |
commit | 6838885b1250e0abbb1b8d56e6b400a5d7f3ca95 (patch) | |
tree | 3c1a7417d471aeea531a36024a460d605cb5d5f1 /src/api | |
parent | 3ff70d61c111b70d5bf770669b0aa3f1d47a502e (diff) |
Support indexed operators re.loop and re.^ (#4167)
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.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 12 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 38 |
2 files changed, 42 insertions, 8 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f563e83f5..fa727088e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -277,6 +277,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {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}, @@ -544,6 +545,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {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}, @@ -3490,6 +3492,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const 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"; @@ -3550,6 +3557,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const 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"; diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index d399ad616..f8e1fb90c 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2175,15 +2175,37 @@ enum CVC4_PUBLIC Kind : int32_t */ 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, /** |