blob: 73a3dc2e24bab0ad73402d497840afc625754c38 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-active-gen=enum
(set-logic ALL)
(declare-datatype Formula (
(P (Id Int))
(Op1 (op1 Int) (f Formula))
(Op2 (op2 Int) (f1 Formula) (f2 Formula))
)
)
(synth-fun phi () Formula
((<F> Formula) (<O2> Int))
((<F> Formula (
(P <O2>)
(Op1 <O2> <F>)
(Op2 <O2> <F> <F>)
)
)
(<O2> Int (0 1))
)
)
(define-fun holds ((f Formula)) Bool
(and ((_ is Op2) f) (= (op2 f) 1))
)
(define-fun holds2 ((f Formula)) Bool
(and ((_ is Op2) f) (= (op1 (f1 f)) 1))
)
(constraint (holds phi))
(check-synth)
|
