Initial support for string reverse (#3581)

Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).

Also improves support in a few places for tolower/toupper.

10 files changed, 103 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 67cc44a42..c85065ef9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -893,6 +893,7 @@ set(regress_0_tests
   regress0/strings/ncontrib-rewrites.smt2
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
+  regress0/strings/parser-syms.cvc
   regress0/strings/re.all.smt2
   regress0/strings/regexp-native-simple.cvc
   regress0/strings/regexp_inclusion.smt2
@@ -907,6 +908,7 @@ set(regress_0_tests
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
   regress0/strings/str_unsound_ext_rew_eq.smt2
+  regress0/strings/str-rev-simple.smt2
   regress0/strings/strings-charat.cvc
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
@@ -1669,6 +1671,12 @@ set(regress_1_tests
   regress1/strings/repl-soundness-sem.smt2
   regress1/strings/replaceall-len.smt2
   regress1/strings/replaceall-replace.smt2
+  regress1/strings/rev-conv1.smt2
+  regress1/strings/rev-ex1.smt2
+  regress1/strings/rev-ex2.smt2
+  regress1/strings/rev-ex3.smt2
+  regress1/strings/rev-ex4.smt2
+  regress1/strings/rev-ex5.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/rew-check1.smt2
   regress1/strings/simple-re-consume.smt2
@@ -1678,6 +1686,7 @@ set(regress_1_tests
   regress1/strings/str-code-unsat-2.smt2
   regress1/strings/str-code-unsat-3.smt2
   regress1/strings/str-code-unsat.smt2
+  regress1/strings/str-rev-simple-s.smt2
   regress1/strings/str001.smt2
   regress1/strings/str002.smt2
   regress1/strings/str006.smt2
diff --git a/test/regress/regress0/strings/parser-syms.cvc b/test/regress/regress0/strings/parser-syms.cvc
new file mode 100644
index 000000000..20c37cf52
--- /dev/null
+++ b/test/regress/regress0/strings/parser-syms.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+
+x : STRING;
+y : STRING;
+
+ASSERT CONCAT( REVERSE("abc"), "d") = x;
+ASSERT CONCAT( TOLOWER("ABC"), TOUPPER("abc")) = y;
+
+CHECKSAT;
diff --git a/test/regress/regress0/strings/str-rev-simple.smt2 b/test/regress/regress0/strings/str-rev-simple.smt2
new file mode 100644
index 000000000..00011681c
--- /dev/null
+++ b/test/regress/regress0/strings/str-rev-simple.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= (str.rev "ABC") "CBA"))
+(assert (= (str.rev "") ""))
+(assert (= (str.rev "A") x))
+(assert (= (str.rev (str.++ x y)) "BCA"))
+(assert (= (str.rev "BC") y))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-conv1.smt2 b/test/regress/regress1/strings/rev-conv1.smt2
new file mode 100644
index 000000000..ca20076cb
--- /dev/null
+++ b/test/regress/regress1/strings/rev-conv1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (= (str.rev (str.toupper x)) "CBA"))
+(assert (not (= x "ABC")))
+(assert (not (= x "abc")))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex1.smt2 b/test/regress/regress1/strings/rev-ex1.smt2
new file mode 100644
index 000000000..36d40fcdd
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (not (= (str.rev (str.++ x y)) (str.rev (str.++ x z)))))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex2.smt2 b/test/regress/regress1/strings/rev-ex2.smt2
new file mode 100644
index 000000000..163785bdc
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= x (str.rev (str.++ y "A"))))
+(assert (> (str.len x) (+ (str.len y) 1)))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex3.smt2 b/test/regress/regress1/strings/rev-ex3.smt2
new file mode 100644
index 000000000..e317191ad
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex3.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (= x (str.rev (str.++ y "A"))))
+(assert (= x (str.rev (str.++ "B" z))))
+(assert (= z (str.++ w "C")))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex4.smt2 b/test/regress/regress1/strings/rev-ex4.smt2
new file mode 100644
index 000000000..a3eed8e35
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (= x (str.rev y)))
+(assert (= y (str.rev z)))
+(assert (distinct x z w))
+(assert (< (str.len x) 2))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex5.smt2 b/test/regress/regress1/strings/rev-ex5.smt2
new file mode 100644
index 000000000..74a374962
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex5.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (= x (str.rev x)))
+(assert (> (str.len x) 1))
+(check-sat)
diff --git a/test/regress/regress1/strings/str-rev-simple-s.smt2 b/test/regress/regress1/strings/str-rev-simple-s.smt2
new file mode 100644
index 000000000..5445a19ea
--- /dev/null
+++ b/test/regress/regress1/strings/str-rev-simple-s.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= (str.rev "ABC") "CBA"))
+(assert (= (str.rev "") ""))
+(assert (= (str.rev "A") x))
+(assert (= (str.rev (str.++ x y)) "BCA"))
+(assert (= (str.rev y) "BC"))
+(check-sat)