@@ -53,8 +53,8 @@ fn empty_poststate(num_vars: uint) -> poststate {
53
53
54
54
fn false_postcond ( num_vars : uint ) -> postcond {
55
55
let rslt = create_tritv ( num_vars) ;
56
- tritv_set_all ( rslt) ;
57
- ret rslt;
56
+ rslt. set_all ( ) ;
57
+ rslt
58
58
}
59
59
60
60
fn empty_pre_post ( num_vars : uint ) -> pre_and_post {
@@ -76,15 +76,11 @@ fn get_pre(&&p: pre_and_post) -> precond { ret p.precondition; }
76
76
77
77
fn get_post ( & & p: pre_and_post ) -> postcond { ret p. postcondition ; }
78
78
79
- fn difference ( p1 : precond , p2 : precond ) -> bool {
80
- ret tritv_difference ( p1, p2) ;
81
- }
79
+ fn difference ( p1 : precond , p2 : precond ) -> bool { p1. difference ( p2) }
82
80
83
- fn union ( p1 : precond , p2 : precond ) -> bool { ret tritv_union ( p1 , p2) ; }
81
+ fn union ( p1 : precond , p2 : precond ) -> bool { p1 . union ( p2) }
84
82
85
- fn intersect ( p1 : precond , p2 : precond ) -> bool {
86
- ret tritv_intersect ( p1, p2) ;
87
- }
83
+ fn intersect ( p1 : precond , p2 : precond ) -> bool { p1. intersect ( p2) }
88
84
89
85
fn pps_len ( p : pre_and_post ) -> uint {
90
86
// gratuitous check
@@ -95,13 +91,13 @@ fn pps_len(p: pre_and_post) -> uint {
95
91
96
92
fn require ( i : uint , p : pre_and_post ) {
97
93
// sets the ith bit in p's pre
98
- tritv_set ( i , p. precondition , ttrue) ;
94
+ p. precondition . set ( i , ttrue) ;
99
95
}
100
96
101
97
fn require_and_preserve ( i : uint , p : pre_and_post ) {
102
98
// sets the ith bit in p's pre and post
103
- tritv_set ( i , p. precondition , ttrue) ;
104
- tritv_set ( i , p. postcondition , ttrue) ;
99
+ p. precondition . set ( i , ttrue) ;
100
+ p. postcondition . set ( i , ttrue) ;
105
101
}
106
102
107
103
fn set_in_postcond ( i : uint , p : pre_and_post ) -> bool {
@@ -110,8 +106,8 @@ fn set_in_postcond(i: uint, p: pre_and_post) -> bool {
110
106
}
111
107
112
108
fn set_in_postcond_ ( i : uint , p : postcond ) -> bool {
113
- let was_set = tritv_get ( p , i) ;
114
- tritv_set ( i , p , ttrue) ;
109
+ let was_set = p . get ( i) ;
110
+ p . set ( i , ttrue) ;
115
111
ret was_set != ttrue;
116
112
}
117
113
@@ -121,8 +117,8 @@ fn set_in_poststate(i: uint, s: pre_and_post_state) -> bool {
121
117
}
122
118
123
119
fn set_in_poststate_ ( i : uint , p : poststate ) -> bool {
124
- let was_set = tritv_get ( p , i) ;
125
- tritv_set ( i , p , ttrue) ;
120
+ let was_set = p . get ( i) ;
121
+ p . set ( i , ttrue) ;
126
122
ret was_set != ttrue;
127
123
128
124
}
@@ -133,8 +129,8 @@ fn clear_in_poststate(i: uint, s: pre_and_post_state) -> bool {
133
129
}
134
130
135
131
fn clear_in_poststate_ ( i : uint , s : poststate ) -> bool {
136
- let was_set = tritv_get ( s , i) ;
137
- tritv_set ( i , s , tfalse) ;
132
+ let was_set = s . get ( i) ;
133
+ s . set ( i , tfalse) ;
138
134
ret was_set != tfalse;
139
135
}
140
136
@@ -144,61 +140,61 @@ fn clear_in_prestate(i: uint, s: pre_and_post_state) -> bool {
144
140
}
145
141
146
142
fn clear_in_prestate_ ( i : uint , s : prestate ) -> bool {
147
- let was_set = tritv_get ( s , i) ;
148
- tritv_set ( i , s , tfalse) ;
143
+ let was_set = s . get ( i) ;
144
+ s . set ( i , tfalse) ;
149
145
ret was_set != tfalse;
150
146
}
151
147
152
148
fn clear_in_postcond ( i : uint , s : pre_and_post ) -> bool {
153
149
// sets the ith bit in p's post
154
- let was_set = tritv_get ( s. postcondition , i) ;
155
- tritv_set ( i , s. postcondition , tfalse) ;
150
+ let was_set = s. postcondition . get ( i) ;
151
+ s. postcondition . set ( i , tfalse) ;
156
152
ret was_set != tfalse;
157
153
}
158
154
159
155
// Sets all the bits in a's precondition to equal the
160
156
// corresponding bit in p's precondition.
161
157
fn set_precondition ( a : ts_ann , p : precond ) {
162
- tritv_copy ( a. conditions . precondition , p) ;
158
+ a. conditions . precondition . become ( p) ;
163
159
}
164
160
165
161
166
162
// Sets all the bits in a's postcondition to equal the
167
163
// corresponding bit in p's postcondition.
168
164
fn set_postcondition ( a : ts_ann , p : postcond ) {
169
- tritv_copy ( a. conditions . postcondition , p) ;
165
+ a. conditions . postcondition . become ( p) ;
170
166
}
171
167
172
168
173
169
// Sets all the bits in a's prestate to equal the
174
170
// corresponding bit in p's prestate.
175
171
fn set_prestate ( a : ts_ann , p : prestate ) -> bool {
176
- ret tritv_copy ( a. states . prestate , p ) ;
172
+ a. states . prestate . become ( p )
177
173
}
178
174
179
175
180
176
// Sets all the bits in a's postcondition to equal the
181
177
// corresponding bit in p's postcondition.
182
178
fn set_poststate ( a : ts_ann , p : poststate ) -> bool {
183
- ret tritv_copy ( a. states . poststate , p ) ;
179
+ a. states . poststate . become ( p )
184
180
}
185
181
186
182
187
183
// Set all the bits in p that are set in new
188
184
fn extend_prestate ( p : prestate , newv : poststate ) -> bool {
189
- ret tritv_union ( p , newv) ;
185
+ p . union ( newv)
190
186
}
191
187
192
188
193
189
// Set all the bits in p that are set in new
194
190
fn extend_poststate ( p : poststate , newv : poststate ) -> bool {
195
- ret tritv_union ( p , newv) ;
191
+ p . union ( newv)
196
192
}
197
193
198
194
// Sets the given bit in p to "don't care"
199
195
fn relax_prestate ( i : uint , p : prestate ) -> bool {
200
- let was_set = tritv_get ( p , i) ;
201
- tritv_set ( i , p , dont_care) ;
196
+ let was_set = p . get ( i) ;
197
+ p . set ( i , dont_care) ;
202
198
ret was_set != dont_care;
203
199
}
204
200
@@ -211,10 +207,10 @@ fn relax_poststate(i: uint, p: poststate) -> bool {
211
207
fn relax_precond ( i : uint , p : precond ) { relax_prestate ( i, p) ; }
212
208
213
209
// Sets all the bits in p to "don't care"
214
- fn clear ( p : precond ) { tritv_clear ( p ) ; }
210
+ fn clear ( p : precond ) { p . clear ( ) ; }
215
211
216
212
// Sets all the bits in p to true
217
- fn set ( p : precond ) { tritv_set_all ( p ) ; }
213
+ fn set ( p : precond ) { p . set_all ( ) ; }
218
214
219
215
fn ann_precond ( a : ts_ann ) -> precond { ret a. conditions . precondition ; }
220
216
@@ -227,16 +223,16 @@ fn pp_clone(p: pre_and_post) -> pre_and_post {
227
223
postcondition : clone ( p. postcondition ) } ;
228
224
}
229
225
230
- fn clone ( p : prestate ) -> prestate { ret tritv_clone ( p ) ; }
226
+ fn clone ( p : prestate ) -> prestate { p . clone ( ) }
231
227
232
228
233
229
// returns true if a implies b
234
230
// that is, returns true except if for some bits c and d,
235
231
// c = 1 and d = either 0 or "don't know"
236
232
fn implies ( a : t , b : t ) -> bool {
237
- let tmp = tritv_clone ( b ) ;
238
- tritv_difference ( tmp, a) ;
239
- ret tritv_doesntcare ( tmp) ;
233
+ let tmp = b . clone ( ) ;
234
+ tmp. difference ( a) ;
235
+ tmp. doesntcare ( )
240
236
}
241
237
242
238
fn trit_str ( t : trit ) -> ~str {
0 commit comments