From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Sep 2020 19:12:52 +0000 (-0500)
Subject: Fixes for regular expressions + sygus (#5044)
X-Git-Tag: cvc5-1.0.0~2884
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=060eedcd5fdb0316d323c4528402034629285b97;p=cvc5.git

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.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 960d17cdc..2cc6c8973 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -661,6 +661,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::REGEXP_RANGE:
   case kind::REGEXP_LOOP:
   case kind::REGEXP_COMPLEMENT:
+  case kind::REGEXP_DIFF:
   case kind::REGEXP_EMPTY:
   case kind::REGEXP_SIGMA:
   case kind::SEQ_UNIT:
@@ -1242,6 +1243,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::REGEXP_RANGE: return "re.range";
   case kind::REGEXP_LOOP: return "re.loop";
   case kind::REGEXP_COMPLEMENT: return "re.comp";
+  case kind::REGEXP_DIFF: return "re.diff";
   case kind::SEQUENCE_TYPE: return "Seq";
   case kind::SEQ_UNIT: return "seq.unit";
   case kind::SEQ_NTH: return "seq.nth";
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 802271858..2709bc8f4 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -527,7 +527,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
 void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
   if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
     d_preinitialized_types[tn] = true;
-    if (!tn.isFunction() || options::ufHo())
+    if (tn.isFirstClass())
     {
       Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
       Node mb = fm->getModelBasisTerm(tn);
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)