Fixes for regular expressions + sygus (#5044)

Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.

2 files changed, 61 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e06abc0a5..ea012a279 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2001,6 +2001,7 @@ set(regress_1_tests
   regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
+  regress1/sygus/rex-strings-alarm.sy
   regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
diff --git a/test/regress/regress1/sygus/rex-strings-alarm.sy b/test/regress/regress1/sygus/rex-strings-alarm.sy
new file mode 100644
index 000000000..aa2ddb2a3
--- /dev/null
+++ b/test/regress/regress1/sygus/rex-strings-alarm.sy
@@ -0,0 +1,60 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --strings-exp
+
+(set-logic S)
+
+(set-option :sygus-rec-fun true)
+(set-option :e-matching false)
+
+(define-sort Rex () RegLan)
+    
+    
+;SyGuS Grammar Definition.
+(synth-fun phi () Rex
+
+  ((<R> Rex))  
+  ((<R> Rex (
+    
+    ; alphabets
+    (str.to_re "r") ; r = request 
+    (str.to_re "g") ; g = grant
+    (str.to_re "e") ; e = empty 
+    (str.to_re "b") ; b = request, grant
+
+;    (re.none <R>)
+;    (re.all <R>)
+    
+    ; CHOICE
+    (re.union <R> <R>)
+    
+    ; CONCATENATION
+    (re.++    <R> <R>)
+    
+    ; INTERSECTION
+    (re.inter <R> <R>)
+    
+    ; STAR 
+    (re.* <R>)
+
+    ; PLUS
+    (re.+ <R>)
+
+    ; Complement / Don't work
+    (re.comp <R>)
+    
+    ; Difference / Don't work
+    (re.diff <R> <R>)
+
+    (re.opt <R>)
+
+   )))
+)
+
+(define-fun w1() String "ee")
+
+(constraint (str.in_re  w1 phi))
+
+(define-fun n1() String "bbegre")
+(constraint (str.in_re n1 (re.comp  phi)))
+
+(check-synth)