diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-23 14:43:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-23 14:43:20 -0500 |
| commit | 2f11cfd563ef96402042e9a3b0086712de660ae6 (patch) | |
| tree | 29d507f91278a31b466d7cbe54342f016451eaa0 /test/regress/regress0/sygus | |
| parent | 6b5c27d7f634eb5985ce455989fcda36e1261929 (diff) | |
Document sygus programming-by-examples utility (#1260)
* Initial documentation and clean up of SyGuS PBE class, fix issue with concat strategy.
* More documentation, cleanup.
* Do not use concat strategy for 3+ arguments to concat, add regression.
* Minor
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/strings-concat-3-args.sy | 18 |
2 files changed, 20 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index a297cee81..6dfcb922a 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -65,7 +65,8 @@ TESTS = commutative.sy \ parse-bv-let.sy \ cegar1.sy \ triv-type-mismatch-si.sy \ - nia-max-square-ns.sy + nia-max-square-ns.sy \ + strings-concat-3-args.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy new file mode 100644 index 000000000..3c93c51d3 --- /dev/null +++ b/test/regress/regress0/sygus/strings-concat-3-args.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((x String)) String +((Start String (ntString)) + +(ntString String (x "" (str.++ ntStringConst ntString ntString))) + +(ntStringConst String ("a" "b" " ")) + +)) + +; can be solved with concat PBE strategy, although we currently are not (issue #1259) +; regardless, this is small enough to solve quickly +(constraint (= (f "def") "ab def")) + +(check-synth) + |