blob: 75837695dadf1c90ab2cb6b73ff827ca11ea7b9a (
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
33
34
35
36
37
38
39
40
41
42
|
; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
(set-logic BV)
(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool
( (Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool) )
((Start Bool (
(and depth1 depth1)
(not depth1)
(or depth1 depth1)
(xor depth1 depth1)
))
(depth1 Bool (
(and depth2 depth2)
(not depth2)
(or depth2 depth2)
(xor depth2 depth2)
x
))
(depth2 Bool (
(and depth3 depth3)
(not depth3)
(or depth3 depth3)
(xor depth3 depth3)
w
))
(depth3 Bool (
(and depth4 depth4)
(not depth4)
(or depth4 depth4)
(xor depth4 depth4)
y
))
(depth4 Bool (
z
)))
)
(check-synth)
|
