diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 13:56:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-02 13:56:39 -0500 |
commit | 12bad5f9c981dd1a328dd769176e87e39a041f91 (patch) | |
tree | a677cef3e87318ae088ac4896710d5a081688931 /test | |
parent | daeab65ac6c6715a3e0c2f6fc0e61b1a7925b932 (diff) |
Support default sygus grammar for strings (#3148)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress1/sygus/strings-no-syntax.sy | 13 | ||||
-rw-r--r-- | test/regress/regress2/sygus/strings-no-syntax-len.sy | 13 |
3 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 99b464d09..19e5fa899 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1696,6 +1696,7 @@ set(regress_1_tests regress1/sygus/real-grammar.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy + regress1/sygus/strings-no-syntax.sy regress1/sygus/strings-concat-3-args.sy regress1/sygus/strings-double-rec.sy regress1/sygus/strings-small.sy @@ -1833,6 +1834,7 @@ set(regress_2_tests regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy + regress2/sygus/strings-no-syntax-len.sy regress2/sygus/three.sy regress2/sygus/vcb.sy regress2/typed_v1l50016-simp.cvc diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy new file mode 100644 index 000000000..4959d6fe1 --- /dev/null +++ b/test/regress/regress1/sygus/strings-no-syntax.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String) (y String)) String) + +(declare-var x String) +(declare-var y String) + +(constraint (>= (str.len (f x y)) (str.len x))) +(constraint (>= (str.len (f x y)) (str.len y))) + +(check-synth) diff --git a/test/regress/regress2/sygus/strings-no-syntax-len.sy b/test/regress/regress2/sygus/strings-no-syntax-len.sy new file mode 100644 index 000000000..22048f1ec --- /dev/null +++ b/test/regress/regress2/sygus/strings-no-syntax-len.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String)) Int) + +(declare-var x String) +(constraint (>= (f (str.++ "A" x)) (f x))) +(constraint (= (f "A") 2)) +(constraint (= (f "BB") 4)) +(constraint (= (f "BCB") 6)) + +(check-synth) |