blob: 70aec7c4c483e6b968e53acc823e7b3c2434fe5f (
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
(set-logic BV)
(define-fun origCir ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool) ) Bool
(not (not (not (xor (not (xor (not (and LN24 k3 ) ) LN129 ) ) LN141 ) ) ) )
)
(synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool) ) Bool
((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool)
(depth5 Bool) (depth6 Bool) (depth7 Bool) (depth8 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)
))
(depth2 Bool (
(and depth3 depth3)
(not depth3)
(or depth3 depth3)
(xor depth3 depth3)
))
(depth3 Bool (
(and depth4 depth4)
(not depth4)
(or depth4 depth4)
(xor depth4 depth4)
))
(depth4 Bool (
(and depth5 depth5)
(not depth5)
(or depth5 depth5)
(xor depth5 depth5)
LN141
))
(depth5 Bool (
(and depth6 depth6)
(not depth6)
(or depth6 depth6)
(xor depth6 depth6)
))
(depth6 Bool (
(and depth7 depth7)
(not depth7)
(or depth7 depth7)
(xor depth7 depth7)
LN129
))
(depth7 Bool (
(and depth8 depth8)
(not depth8)
(or depth8 depth8)
(xor depth8 depth8)
LN24
))
(depth8 Bool (
k3
)))
)
(declare-var LN24 Bool)
(declare-var k3 Bool)
(declare-var LN129 Bool)
(declare-var LN141 Bool)
(constraint (= (origCir LN24 k3 LN129 LN141 ) (skel LN24 k3 LN129 LN141 )))
(check-synth)
|