Commit 45d7f4bd authored by phlo's avatar phlo

moved state updates to the end

parent 4cfb144b
......@@ -176,8 +176,8 @@ void Encoder::encode ()
declare_states();
declare_inputs();
define_transitions();
define_states();
define_constraints();
define_states();
}
// btor2::Encoder::assert_exit -------------------------------------------------
......
......@@ -162,13 +162,12 @@ void Encoder::encode ()
declare_states();
declare_transitions();
define_transitions();
define_constraints ();
if (step)
define_states();
else
init_states();
define_constraints ();
}
}
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -98,177 +98,177 @@
43 and 1 27 35 exec_1_1
44 and 1 28 35 exec_1_2
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; scheduling constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
45 or 1 34 35
46 or 1 36 45
47 or 1 37 46
48 or 1 32 47
49 constraint 48
50 nand 1 34 35
51 nand 1 34 36
52 nand 1 34 37
53 nand 1 34 32
54 nand 1 35 36
55 nand 1 35 37
56 nand 1 35 32
57 nand 1 36 37
58 nand 1 36 32
59 nand 1 37 32
60 and 1 50 51
61 and 1 52 60
62 and 1 53 61
63 and 1 54 62
64 and 1 55 63
65 and 1 56 64
66 and 1 57 65
67 and 1 58 66
68 and 1 59 67
69 constraint 68
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; store buffer constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
70 or 1 23 24
71 or 1 25 70
72 implies 1 71 -34
73 ite 1 20 72 -36
74 constraint 73 flush_0
75 implies 1 28 -35
76 ite 1 21 75 -37
77 constraint 76 flush_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; halt constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
78 implies 1 29 -34
79 constraint 78 halt_0
80 implies 1 30 -35
81 constraint 80 halt_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; state variable definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; accu variables - accu_<thread>
45 init 2 12 6
46 add 2 12 7
47 ite 2 38 46 12 0:0:ADDI:1
48 next 2 12 47 accu_0
49 init 2 13 6
50 read 2 31 7
51 eq 1 17 7
52 and 1 21 51
53 ite 2 52 19 50
54 ite 2 42 53 13 1:0:LOAD:1
55 read 2 31 6
56 eq 1 17 6
57 and 1 21 56
58 ite 2 57 19 55
59 ite 2 43 58 54 1:1:LOAD:0
60 next 2 13 59 accu_1
82 init 2 12 6
83 add 2 12 7
84 ite 2 38 83 12 0:0:ADDI:1
85 next 2 12 84 accu_0
86 init 2 13 6
87 read 2 31 7
88 eq 1 17 7
89 and 1 21 88
90 ite 2 89 19 87
91 ite 2 42 90 13 1:0:LOAD:1
92 read 2 31 6
93 eq 1 17 6
94 and 1 21 93
95 ite 2 94 19 92
96 ite 2 43 95 91 1:1:LOAD:0
97 next 2 13 96 accu_1
; mem variables - mem_<thread>
61 init 2 14 6
62 next 2 14 14 mem_0
98 init 2 14 6
99 next 2 14 14 mem_0
63 init 2 15 6
64 next 2 15 15 mem_1
100 init 2 15 6
101 next 2 15 15 mem_1
; store buffer address variables - sb-adr_<thread>
65 init 2 16 6
66 ite 2 39 6 16 0:1:STORE:0
67 ite 2 40 7 66 0:2:STORE:1
68 next 2 16 67 sb-adr_0
102 init 2 16 6
103 ite 2 39 6 16 0:1:STORE:0
104 ite 2 40 7 103 0:2:STORE:1
105 next 2 16 104 sb-adr_0
69 init 2 17 6
70 next 2 17 17 sb-adr_1
106 init 2 17 6
107 next 2 17 17 sb-adr_1
; store buffer value variables - sb-val_<thread>
71 init 2 18 6
72 ite 2 39 12 18 0:1:STORE:0
73 ite 2 40 12 72 0:2:STORE:1
74 next 2 18 73 sb-val_0
108 init 2 18 6
109 ite 2 39 12 18 0:1:STORE:0
110 ite 2 40 12 109 0:2:STORE:1
111 next 2 18 110 sb-val_0
75 init 2 19 6
76 next 2 19 19 sb-val_1
112 init 2 19 6
113 next 2 19 19 sb-val_1
; store buffer full variables - sb-full_<thread>
77 init 1 20 4
78 or 1 39 40
79 or 1 20 78
80 ite 1 36 4 79
81 next 1 20 80 sb-full_0
114 init 1 20 4
115 or 1 39 40
116 or 1 20 115
117 ite 1 36 4 116
118 next 1 20 117 sb-full_0
82 init 1 21 4
83 ite 1 37 4 21
84 next 1 21 83 sb-full_1
119 init 1 21 4
120 ite 1 37 4 21
121 next 1 21 120 sb-full_1
; statement activation variables - stmt_<thread>_<pc>
85 init 1 22 5
86 and 1 22 -38 0:0:ADDI:1
87 next 1 22 86 stmt_0_0
88 init 1 23 4
89 and 1 23 -39 0:1:STORE:0
90 ite 1 22 38 89 0:0:ADDI:1
91 next 1 23 90 stmt_0_1
92 init 1 24 4
93 and 1 24 -40 0:2:STORE:1
94 ite 1 23 39 93 0:1:STORE:0
95 next 1 24 94 stmt_0_2
96 init 1 25 4
97 and 1 25 -41 0:3:HALT
98 ite 1 24 40 97 0:2:STORE:1
99 next 1 25 98 stmt_0_3
100 init 1 26 5
101 and 1 26 -42 1:0:LOAD:1
102 next 1 26 101 stmt_1_0
103 init 1 27 4
104 and 1 27 -43 1:1:LOAD:0
105 ite 1 26 42 104 1:0:LOAD:1
106 next 1 27 105 stmt_1_1
107 init 1 28 4
108 and 1 28 -44 1:2:HALT
109 ite 1 27 43 108 1:1:LOAD:0
110 next 1 28 109 stmt_1_2
122 init 1 22 5
123 and 1 22 -38 0:0:ADDI:1
124 next 1 22 123 stmt_0_0
125 init 1 23 4
126 and 1 23 -39 0:1:STORE:0
127 ite 1 22 38 126 0:0:ADDI:1
128 next 1 23 127 stmt_0_1
129 init 1 24 4
130 and 1 24 -40 0:2:STORE:1
131 ite 1 23 39 130 0:1:STORE:0
132 next 1 24 131 stmt_0_2
133 init 1 25 4
134 and 1 25 -41 0:3:HALT
135 ite 1 24 40 134 0:2:STORE:1
136 next 1 25 135 stmt_0_3
137 init 1 26 5
138 and 1 26 -42 1:0:LOAD:1
139 next 1 26 138 stmt_1_0
140 init 1 27 4
141 and 1 27 -43 1:1:LOAD:0
142 ite 1 26 42 141 1:0:LOAD:1
143 next 1 27 142 stmt_1_1
144 init 1 28 4
145 and 1 28 -44 1:2:HALT
146 ite 1 27 43 145 1:1:LOAD:0
147 next 1 28 146 stmt_1_2
; halt variables - halt_<thread>
111 init 1 29 4
112 or 1 41 29
113 next 1 29 112 halt_0
148 init 1 29 4
149 or 1 41 29
150 next 1 29 149 halt_0
114 init 1 30 4
115 or 1 44 30
116 next 1 30 115 halt_1
151 init 1 30 4
152 or 1 44 30
153 next 1 30 152 halt_1
; heap variable
117 init 3 31 11
118 write 3 31 16 18
119 ite 3 36 118 31 flush_0
120 write 3 31 17 19
121 ite 3 37 120 119 flush_1
122 next 3 31 121 heap
154 init 3 31 11
155 write 3 31 16 18
156 ite 3 36 155 31 flush_0
157 write 3 31 17 19
158 ite 3 37 157 156 flush_1
159 next 3 31 158 heap
; exit flag variable
123 init 1 32 4
124 and 1 112 115
125 or 1 32 124
126 next 1 32 125 exit
160 init 1 32 4
161 and 1 149 152
162 or 1 32 161
163 next 1 32 162 exit
; exit code variable
127 init 2 33 6
128 next 2 33 33 exit-code
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; scheduling constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
129 or 1 34 35
130 or 1 36 129
131 or 1 37 130
132 or 1 32 131
133 constraint 132
134 nand 1 34 35
135 nand 1 34 36
136 nand 1 34 37
137 nand 1 34 32
138 nand 1 35 36
139 nand 1 35 37
140 nand 1 35 32
141 nand 1 36 37
142 nand 1 36 32
143 nand 1 37 32
144 and 1 134 135
145 and 1 136 144
146 and 1 137 145
147 and 1 138 146
148 and 1 139 147
149 and 1 140 148
150 and 1 141 149
151 and 1 142 150
152 and 1 143 151
153 constraint 152
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; store buffer constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
154 or 1 23 24
155 or 1 25 154
156 implies 1 155 -34
157 ite 1 20 156 -36
158 constraint 157 flush_0
159 implies 1 28 -35
160 ite 1 21 159 -37
161 constraint 160 flush_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; halt constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
162 implies 1 29 -34
163 constraint 162 halt_0
164 implies 1 30 -35
165 constraint 164 halt_1
164 init 2 33 6
165 next 2 33 33 exit-code
......@@ -100,186 +100,186 @@
45 and 1 28 36 exec_1_2
46 and 1 29 36 exec_1_3
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; scheduling constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
47 or 1 35 36
48 or 1 37 47
49 or 1 38 48
50 or 1 33 49
51 constraint 50
52 nand 1 35 36
53 nand 1 35 37
54 nand 1 35 38
55 nand 1 35 33
56 nand 1 36 37
57 nand 1 36 38
58 nand 1 36 33
59 nand 1 37 38
60 nand 1 37 33
61 nand 1 38 33
62 and 1 52 53
63 and 1 54 62
64 and 1 55 63
65 and 1 56 64
66 and 1 57 65
67 and 1 58 66
68 and 1 59 67
69 and 1 60 68
70 and 1 61 69
71 constraint 70
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; store buffer constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
72 or 1 24 25
73 implies 1 72 -35
74 ite 1 20 73 -37
75 constraint 74 flush_0
76 or 1 28 29
77 implies 1 76 -36
78 ite 1 21 77 -38
79 constraint 78 flush_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; halt constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
80 implies 1 30 -35
81 constraint 80 halt_0
82 implies 1 31 -36
83 constraint 82 halt_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; state variable definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; accu variables - accu_<thread>
47 init 2 12 6
48 read 2 32 6
49 eq 1 16 6
50 and 1 20 49
51 ite 2 50 18 48
52 ite 2 39 51 12 0:0:MEM:0
53 add 2 12 7
54 ite 2 40 53 52 0:1:ADDI:1
55 next 2 12 54 accu_0
56 init 2 13 6
57 read 2 32 7
58 eq 1 17 7
59 and 1 21 58
60 ite 2 59 19 57
61 ite 2 43 60 13 1:0:MEM:1
62 add 2 13 7
63 ite 2 44 62 61 1:1:ADDI:1
64 next 2 13 63 accu_1
84 init 2 12 6
85 read 2 32 6
86 eq 1 16 6
87 and 1 20 86
88 ite 2 87 18 85
89 ite 2 39 88 12 0:0:MEM:0
90 add 2 12 7
91 ite 2 40 90 89 0:1:ADDI:1
92 next 2 12 91 accu_0
93 init 2 13 6
94 read 2 32 7
95 eq 1 17 7
96 and 1 21 95
97 ite 2 96 19 94
98 ite 2 43 97 13 1:0:MEM:1
99 add 2 13 7
100 ite 2 44 99 98 1:1:ADDI:1
101 next 2 13 100 accu_1
; mem variables - mem_<thread>
65 init 2 14 6
66 ite 2 39 51 14 0:0:MEM:0
67 next 2 14 66 mem_0
102 init 2 14 6
103 ite 2 39 88 14 0:0:MEM:0
104 next 2 14 103 mem_0
68 init 2 15 6
69 ite 2 43 60 15 1:0:MEM:1
70 next 2 15 69 mem_1
105 init 2 15 6
106 ite 2 43 97 15 1:0:MEM:1
107 next 2 15 106 mem_1
; store buffer address variables - sb-adr_<thread>
71 init 2 16 6
72 ite 2 41 7 16 0:2:STORE:1
73 next 2 16 72 sb-adr_0
108 init 2 16 6
109 ite 2 41 7 16 0:2:STORE:1
110 next 2 16 109 sb-adr_0
74 init 2 17 6
75 ite 2 45 6 17 1:2:STORE:0
76 next 2 17 75 sb-adr_1
111 init 2 17 6
112 ite 2 45 6 17 1:2:STORE:0
113 next 2 17 112 sb-adr_1
; store buffer value variables - sb-val_<thread>
77 init 2 18 6
78 ite 2 41 12 18 0:2:STORE:1
79 next 2 18 78 sb-val_0
114 init 2 18 6
115 ite 2 41 12 18 0:2:STORE:1
116 next 2 18 115 sb-val_0
80 init 2 19 6
81 ite 2 45 13 19 1:2:STORE:0
82 next 2 19 81 sb-val_1
117 init 2 19 6
118 ite 2 45 13 19 1:2:STORE:0
119 next 2 19 118 sb-val_1
; store buffer full variables - sb-full_<thread>
83 init 1 20 4
84 or 1 41 20
85 ite 1 37 4 84
86 next 1 20 85 sb-full_0
120 init 1 20 4
121 or 1 41 20
122 ite 1 37 4 121
123 next 1 20 122 sb-full_0
87 init 1 21 4
88 or 1 45 21
89 ite 1 38 4 88
90 next 1 21 89 sb-full_1
124 init 1 21 4
125 or 1 45 21
126 ite 1 38 4 125
127 next 1 21 126 sb-full_1
; statement activation variables - stmt_<thread>_<pc>
91 init 1 22 5
92 and 1 22 -39 0:0:MEM:0
93 next 1 22 92 stmt_0_0
94 init 1 23 4
95 and 1 23 -40 0:1:ADDI:1
96 ite 1 22 39 95 0:0:MEM:0
97 next 1 23 96 stmt_0_1
98 init 1 24 4
99 and 1 24 -41 0:2:STORE:1
100 ite 1 23 40 99 0:1:ADDI:1
101 next 1 24 100 stmt_0_2
102 init 1 25 4
103 and 1 25 -42 0:3:HALT
104 ite 1 24 41 103 0:2:STORE:1
105 next 1 25 104 stmt_0_3
106 init 1 26 5
107 and 1 26 -43 1:0:MEM:1
108 next 1 26 107 stmt_1_0
109 init 1 27 4
110 and 1 27 -44 1:1:ADDI:1
111 ite 1 26 43 110 1:0:MEM:1
112 next 1 27 111 stmt_1_1
113 init 1 28 4
114 and 1 28 -45 1:2:STORE:0
115 ite 1 27 44 114 1:1:ADDI:1
116 next 1 28 115 stmt_1_2
117 init 1 29 4
118 and 1 29 -46 1:3:HALT
119 ite 1 28 45 118 1:2:STORE:0
120 next 1 29 119 stmt_1_3
128 init 1 22 5
129 and 1 22 -39 0:0:MEM:0
130 next 1 22 129 stmt_0_0
131 init 1 23 4
132 and 1 23 -40 0:1:ADDI:1
133 ite 1 22 39 132 0:0:MEM:0
134 next 1 23 133 stmt_0_1
135 init 1 24 4
136 and 1 24 -41 0:2:STORE:1
137 ite 1 23 40 136 0:1:ADDI:1
138 next 1 24 137 stmt_0_2
139 init 1 25 4
140 and 1 25 -42 0:3:HALT
141 ite 1 24 41 140 0:2:STORE:1
142 next 1 25 141 stmt_0_3
143 init 1 26 5
144 and 1 26 -43 1:0:MEM:1
145 next 1 26 144 stmt_1_0
146 init 1 27 4
147 and 1 27 -44 1:1:ADDI:1
148 ite 1 26 43 147 1:0:MEM:1
149 next 1 27 148 stmt_1_1
150 init 1 28 4
151 and 1 28 -45 1:2:STORE:0
152 ite 1 27 44 151 1:1:ADDI:1
153 next 1 28 152 stmt_1_2
154 init 1 29 4
155 and 1 29 -46 1:3:HALT
156 ite 1 28 45 155 1:2:STORE:0
157 next 1 29 156 stmt_1_3
; halt variables - halt_<thread>
121 init 1 30 4
122 or 1 42 30
123 next 1 30 122 halt_0
158 init 1 30 4
159 or 1 42 30
160 next 1 30 159 halt_0
124 init 1 31 4
125 or 1 46 31
126 next 1 31 125 halt_1
161 init 1 31 4
162 or 1 46 31
163 next 1 31 162 halt_1
; heap variable
127 init 3 32 11
128 write 3 32 16 18
129 ite 3 37 128 32 flush_0
130 write 3 32 17 19
131 ite 3 38 130 129 flush_1
132 next 3 32 131 heap
164 init 3 32 11
165 write 3 32 16 18
166 ite 3 37 165 32 flush_0
167 write 3 32 17 19
168 ite 3 38 167 166 flush_1
169 next 3 32 168 heap
; exit flag variable
133 init 1 33 4
134 and 1 122 125
135 or 1 33 134
136 next 1 33 135 exit
170 init 1 33 4
171 and 1 159 162
172 or 1 33 171
173 next 1 33 172 exit
; exit code variable
137 init 2 34 6
138 next 2 34 34 exit-code
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; scheduling constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
139 or 1 35 36
140 or 1 37 139
141 or 1 38 140
142 or 1 33 141
143 constraint 142
144 nand 1 35 36
145 nand 1 35 37
146 nand 1 35 38
147 nand 1 35 33
148 nand 1 36 37
149 nand 1 36 38
150 nand 1 36 33
151 nand 1 37 38
152 nand 1 37 33
153 nand 1 38 33
154 and 1 144 145
155 and 1 146 154
156 and 1 147 155
157 and 1 148 156
158 and 1 149 157
159 and 1 150 158
160 and 1 151 159
161 and 1 152 160
162 and 1 153 161
163 constraint 162
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; store buffer constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
164 or 1 24 25
165 implies 1 164 -35
166 ite 1 20 165 -37
167 constraint 166 flush_0