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.

2 files changed, 20 insertions, 0 deletions

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)