Revision ebbe2fc3
Added by Lélio Brun over 3 years ago
| src/optimize_machine.ml | ||
|---|---|---|
| 134 | 134 |
( e_val g, |
| 135 | 135 |
List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl )) |
| 136 | 136 |
|
| 137 |
let rec fv_value s v = |
|
| 137 |
let rec fv_value m s v =
|
|
| 138 | 138 |
match v.value_desc with |
| 139 | 139 |
| Var v -> |
| 140 |
VSet.add v s |
|
| 140 |
if is_memory m v then s else VSet.add v s
|
|
| 141 | 141 |
| Fun (_, vl) |
| 142 | 142 |
| Array vl -> |
| 143 |
List.fold_left fv_value s vl
|
|
| 143 |
List.fold_left (fv_value m) s vl
|
|
| 144 | 144 |
| Access (v1, v2) |
| 145 | 145 |
| Power (v1, v2) -> |
| 146 |
fv_value (fv_value s v1) v2
|
|
| 146 |
fv_value m (fv_value m s v1) v2
|
|
| 147 | 147 |
| _ -> s |
| 148 | 148 |
|
| 149 |
let fv_expr s = function |
|
| 150 |
| Val v -> fv_value s v |
|
| 151 |
| Var v -> VSet.add v s |
|
| 149 |
let fv_expr m s = function |
|
| 150 |
| Val v -> fv_value m s v |
|
| 151 |
| Var v -> |
|
| 152 |
if is_memory m v then s else VSet.add v s |
|
| 152 | 153 |
| _ -> s |
| 153 | 154 |
|
| 154 |
let fv_predicate s = function |
|
| 155 |
let fv_predicate m s = function
|
|
| 155 | 156 |
| Transition (_, _, _, _, vars, _, _, _) -> |
| 156 |
List.fold_left fv_expr s vars
|
|
| 157 |
List.fold_left (fv_expr m) s vars
|
|
| 157 | 158 |
| _ -> s |
| 158 | 159 |
|
| 159 |
let rec fv_formula s = function |
|
| 160 |
let rec fv_formula m s = function
|
|
| 160 | 161 |
| Equal (e1, e2) |
| 161 | 162 |
| GEqual (e1, e2) -> |
| 162 |
fv_expr (fv_expr s e1) e2
|
|
| 163 |
fv_expr m (fv_expr m s e1) e2
|
|
| 163 | 164 |
| And f |
| 164 | 165 |
| Or f -> |
| 165 |
List.fold_left fv_formula s f
|
|
| 166 |
List.fold_left (fv_formula m) s f
|
|
| 166 | 167 |
| Imply (a, b) |
| 167 | 168 |
| ExistsMem (_, a, b) -> |
| 168 |
fv_formula (fv_formula s a) b
|
|
| 169 |
fv_formula m (fv_formula m s a) b
|
|
| 169 | 170 |
| Exists (xs, a) |
| 170 | 171 |
| Forall (xs, a) -> |
| 171 |
VSet.filter (fun v -> not (List.mem v xs)) (fv_formula s a) |
|
| 172 |
VSet.filter (fun v -> not (List.mem v xs)) (fv_formula m s a)
|
|
| 172 | 173 |
| Ternary (e, a, b) -> |
| 173 |
fv_expr (fv_formula (fv_formula s a) b) e
|
|
| 174 |
fv_expr m (fv_formula m (fv_formula m s a) b) e
|
|
| 174 | 175 |
| Predicate p -> |
| 175 |
fv_predicate s p |
|
| 176 |
fv_predicate m s p
|
|
| 176 | 177 |
| Value v -> |
| 177 |
fv_value s v |
|
| 178 |
fv_value m s v
|
|
| 178 | 179 |
| _ -> s |
| 179 | 180 |
|
| 180 | 181 |
let eliminate_transition m elim t = |
| 181 | 182 |
let tvars = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) t.tvars in |
| 182 | 183 |
let tformula = eliminate_formula m elim t.tformula in |
| 183 |
let fv = VSet.(elements (diff (fv_formula empty tformula) (of_list tvars))) in |
|
| 184 |
let fv = VSet.(elements (diff (fv_formula m empty tformula) (of_list tvars))) in
|
|
| 184 | 185 |
let tformula = Exists (fv, tformula) in |
| 185 | 186 |
{ t with
|
| 186 | 187 |
tvars; |
Also available in: Unified diff
state variables ar not free