Add support for re.all (#2980)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 71ba81124565cd9ce6a6f8ae320a8a32a94a3f59..2e1abf7102a542e4c81536ee076eec4bfefe02fa 100644 (file)
--- 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 8ab86e772ee5ba3e580c05d6bed66bf670b46be5..b767d6c12ade493ec829dd8712533997544b4ba9 100644 (file)
--- 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 (file)
index 0000000..5200b92
--- /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)