diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-10 08:45:39 -0600 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-10 11:45:39 -0300 |
commit | 7f7c4e5f7bfb5c38611afa3a016f4f767d5b86fd (patch) | |
tree | b3d4c7afeb18305d662fe07907f88126b3890e4d /test/regress/regress1/sygus | |
parent | 1bceb5036a208746bfba1ec42d65862d0d231a83 (diff) |
Fix bugs related to sygus higher-order + recursive functions (#3448)
Diffstat (limited to 'test/regress/regress1/sygus')
-rw-r--r-- | test/regress/regress1/sygus/list_recursor.sy | 26 |
1 files changed, 26 insertions, 0 deletions
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) |