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.

7 files changed, 14 insertions, 9 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d843eb5ed..b9835d919 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -942,6 +942,7 @@ set(regress_0_tests
   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
diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
index fd60089fd..5bf21ebb9 100644
--- a/test/regress/regress0/strings/bug002.smt2
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -4,7 +4,7 @@
 (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)
diff --git a/test/regress/regress0/strings/loop-wrong-sem.smt2 b/test/regress/regress0/strings/loop-wrong-sem.smt2
new file mode 100644
index 000000000..d0dd3fcb2
--- /dev/null
+++ b/test/regress/regress0/strings/loop-wrong-sem.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(set-info :status unsat)
+(assert (str.in.re "" ((_ re.loop 1 0) (str.to.re ""))))
+(check-sat)
diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index 0cb9fac26..b5c9457ff 100644
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -8,7 +8,7 @@
 (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)
diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index add60d534..e04db8e9a 100644
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -6,7 +6,7 @@
 (define-fun stringEval ((?s String)) Bool (str.in.re ?s 

 (re.union 

 (str.to.re "H")

-(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range "" "]") (re.range "" "^") ) 2 4 ) ) ) ) )

+(re.++ ((_ re.loop 2 2) (str.to.re "{") ) ((_ re.loop 2 4) (re.union re.nostr (re.range "" "]") (re.range "" "^") ) ) ) ) ) )

 (declare-fun s0() String)

 (declare-fun s1() String)

 (declare-fun s2() String)

diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 22537b957..6230d1656 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -8,11 +8,11 @@
 (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))
 
diff --git a/test/regress/regress2/strings/range-perf.smt2 b/test/regress/regress2/strings/range-perf.smt2
index 62ec10711..33960e124 100644
--- a/test/regress/regress2/strings/range-perf.smt2
+++ b/test/regress/regress2/strings/range-perf.smt2
@@ -2,6 +2,6 @@
 ; 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)