diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/list_recursor.sy | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c98dd1be2..aa5329e2f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1718,6 +1718,7 @@ set(regress_1_tests regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy + regress1/sygus/list_recursor.sy regress1/sygus/logiccell_help.sy regress1/sygus/max.sy regress1/sygus/max2-bv.sy diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy new file mode 100644 index 000000000..53c55397e --- /dev/null +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho + +(set-logic ALL) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int + (ite ((_ is nil) l) x + (y (head l) (tail l) (List_rec x y (tail l))))) + +(synth-fun f () Int + ((I Int)) + ((I Int (0 1 (+ I I))))) + +(synth-fun g ((x Int) (y List) (z Int)) Int + ((I Int) (L List)) + ((I Int (x z (+ I I) (head L) 0 1)) + (L List (y (tail y))))) + + +(constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2)) +(constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2)) +(constraint (= (List_rec f g (cons 5 (cons 3 (cons 3 (cons 0 nil))))) 4)) +(constraint (= (List_rec f g nil) 0)) +(check-synth) |