From 562ee7da1637353a73884af6c9869cd21554b534 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 6 Aug 2018 22:39:21 -0500
Subject: [PATCH] Add RegLan to smt2/sygus parsers. (#2276)

---
 src/parser/smt2/smt2.cpp                     |  1 +
 test/regress/Makefile.tests                  |  1 +
 test/regress/regress1/sygus/simple-regexp.sy | 37 ++++++++++++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 test/regress/regress1/sygus/simple-regexp.sy

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 257ee1171..a0cc750b3 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -287,6 +287,7 @@ void Smt2::addTheory(Theory theory) {
 
   case THEORY_STRINGS:
     defineType("String", getExprManager()->stringType());
+    defineType("RegLan", getExprManager()->regExpType());
     defineType("Int", getExprManager()->integerType());
     addStringOperators();
     break;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 34855e81d..aec72993c 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1544,6 +1544,7 @@ REG1_TESTS = \
 	regress1/sygus/process-10-vars.sy \
 	regress1/sygus/qe.sy \
 	regress1/sygus/real-grammar.sy \
+	regress1/sygus/simple-regexp.sy \
 	regress1/sygus/stopwatch-bt.sy \
 	regress1/sygus/strings-concat-3-args.sy \
 	regress1/sygus/strings-double-rec.sy \
diff --git a/test/regress/regress1/sygus/simple-regexp.sy b/test/regress/regress1/sygus/simple-regexp.sy
new file mode 100644
index 000000000..b4c248de9
--- /dev/null
+++ b/test/regress/regress1/sygus/simple-regexp.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+(synth-fun P ((x String)) Bool (
+(Start Bool (
+  (str.in.re StartStr StartRL)
+  ))
+(StartStr String (
+  x
+  (str.++ StartStr StartStr)
+  ))
+(StartStrC String (
+  "A" "B" ""
+  (str.++ StartStrC StartStrC)))
+(StartRL RegLan (
+(re.++ StartRLi StartRLi)
+(re.inter StartRL StartRL)
+(re.union StartRL StartRL)
+(re.* StartRLi)
+))
+(StartRLi RegLan (
+(str.to.re StartStrC)
+(re.inter StartRLi StartRLi)
+(re.union StartRLi StartRLi)
+(re.++ StartRLi StartRLi)
+(re.* StartRLi)
+))
+))
+
+(constraint (P "AAAAA"))
+(constraint (P "AAA"))
+(constraint (P "AA"))
+(constraint (not (P "AB")))
+(constraint (not (P "B")))
+
+; (str.in.re x (re.* (str.to.re "A"))) is a solution
+(check-synth)
-- 
2.30.2