From 1694c6b45dfa02ca22146755c89078bfa6b851ef Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 6 May 2019 06:05:19 -0700
Subject: Add support for re.all (#2980)

---
 src/parser/smt2/smt2.cpp                  | 5 +++++
 test/regress/CMakeLists.txt               | 3 ++-
 test/regress/regress0/strings/re.all.smt2 | 6 ++++++
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/strings/re.all.smt2

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 71ba81124..2e1abf710 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -122,6 +122,11 @@ void Smt2::addBitvectorOperators() {
 }
 
 void Smt2::addStringOperators() {
+  defineVar("re.all",
+            getSolver()
+                ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
+                .getExpr());
+
   addOperator(kind::STRING_CONCAT, "str.++");
   addOperator(kind::STRING_LENGTH, "str.len");
   addOperator(kind::STRING_SUBSTR, "str.substr" );
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8ab86e772..b767d6c12 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -841,6 +841,7 @@ set(regress_0_tests
   regress0/strings/ncontrib-rewrites.smt2
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
+  regress0/strings/re.all.smt2
   regress0/strings/repl-rewrites2.smt2
   regress0/strings/replaceall-eval.smt2
   regress0/strings/rewrites-re-concat.smt2
@@ -882,7 +883,6 @@ set(regress_0_tests
   regress0/test9.cvc
   regress0/tptp/ARI086=1.p
   regress0/tptp/DAT001=1.p
-  regress0/tptp/is_rat_simple.p
   regress0/tptp/KRS018+1.p
   regress0/tptp/KRS063+1.p
   regress0/tptp/MGT019+2.p
@@ -896,6 +896,7 @@ set(regress_0_tests
   regress0/tptp/SYN000_1.p
   regress0/tptp/SYN000_2.p
   regress0/tptp/SYN075-1.p
+  regress0/tptp/is_rat_simple.p
   regress0/tptp/tff0-arith.p
   regress0/tptp/tff0.p
   regress0/tptp/tptp_parser.p
diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2
new file mode 100644
index 000000000..5200b924f
--- /dev/null
+++ b/test/regress/regress0/strings/re.all.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x String)
+(assert (str.in.re x (re.++ (str.to.re "abc") re.all)))
+(assert (not (str.prefixof "abc" x)))
+(check-sat)
-- 
cgit v1.2.3