diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-09 14:12:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-09 14:12:52 -0500 |
commit | 060eedcd5fdb0316d323c4528402034629285b97 (patch) | |
tree | ee7a93f408a7b18113e1b29b081afab9639e11fe | |
parent | b115aecf296b8d712363c506daecfab364f71712 (diff) |
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.
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 2 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/rex-strings-alarm.sy | 60 |
4 files changed, 64 insertions, 1 deletions
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) |