blob: 0c4412bacbee721c688fc874623d07bcecb93d7f (
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
; Argmax Equivalence for reduced FashionMNIST
; Constant declaration
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const X_19 Real)
(declare-const X_20 Real)
(declare-const X_21 Real)
(declare-const X_22 Real)
(declare-const X_23 Real)
(declare-const X_24 Real)
(declare-const X_25 Real)
(declare-const X_26 Real)
(declare-const X_27 Real)
(declare-const X_28 Real)
(declare-const X_29 Real)
(declare-const X_30 Real)
(declare-const X_31 Real)
(declare-const X_32 Real)
(declare-const X_33 Real)
(declare-const X_34 Real)
(declare-const X_35 Real)
(declare-const Y_0 Real)
(declare-const Y_1 Real)
(declare-const Y_2 Real)
(declare-const Y_3 Real)
; Bounded inputs: X must be within [0, 1]
(assert (>= X_0 0.0))
(assert (<= X_0 1.0))
(assert (>= X_1 0.0))
(assert (<= X_1 1.0))
(assert (>= X_2 0.0))
(assert (<= X_2 1.0))
(assert (>= X_3 0.0))
(assert (<= X_3 1.0))
(assert (>= X_4 0.0))
(assert (<= X_4 1.0))
(assert (>= X_5 0.0))
(assert (<= X_5 1.0))
(assert (>= X_6 0.0))
(assert (<= X_6 1.0))
(assert (>= X_7 0.0))
(assert (<= X_7 1.0))
(assert (>= X_8 0.0))
(assert (<= X_8 1.0))
(assert (>= X_9 0.0))
(assert (<= X_9 1.0))
(assert (>= X_10 0.0))
(assert (<= X_10 1.0))
(assert (>= X_11 0.0))
(assert (<= X_11 1.0))
(assert (>= X_12 0.0))
(assert (<= X_12 1.0))
(assert (>= X_13 0.0))
(assert (<= X_13 1.0))
(assert (>= X_14 0.0))
(assert (<= X_14 1.0))
(assert (>= X_15 0.0))
(assert (<= X_15 1.0))
(assert (>= X_16 0.0))
(assert (<= X_16 1.0))
(assert (>= X_17 0.0))
(assert (<= X_17 1.0))
(assert (>= X_18 0.0))
(assert (<= X_18 1.0))
(assert (>= X_19 0.0))
(assert (<= X_19 1.0))
(assert (>= X_20 0.0))
(assert (<= X_20 1.0))
(assert (>= X_21 0.0))
(assert (<= X_21 1.0))
(assert (>= X_22 0.0))
(assert (<= X_22 1.0))
(assert (>= X_23 0.0))
(assert (<= X_23 1.0))
(assert (>= X_24 0.0))
(assert (<= X_24 1.0))
(assert (>= X_25 0.0))
(assert (<= X_25 1.0))
(assert (>= X_26 0.0))
(assert (<= X_26 1.0))
(assert (>= X_27 0.0))
(assert (<= X_27 1.0))
(assert (>= X_28 0.0))
(assert (<= X_28 1.0))
(assert (>= X_29 0.0))
(assert (<= X_29 1.0))
(assert (>= X_30 0.0))
(assert (<= X_30 1.0))
(assert (>= X_31 0.0))
(assert (<= X_31 1.0))
(assert (>= X_32 0.0))
(assert (<= X_32 1.0))
(assert (>= X_33 0.0))
(assert (<= X_33 1.0))
(assert (>= X_34 0.0))
(assert (<= X_34 1.0))
(assert (>= X_35 0.0))
(assert (<= X_35 1.0))
; Violation of argmax equivalence
(assert (or
(and
(> Y_0 Y_1)
(or
(> Y_3 Y_2)
)
)
(and
(> Y_1 Y_0)
(or
(> Y_2 Y_3)
)
)
))
|
