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.

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,
   /**