Revision 333e3a25
Added by Pierre-Loïc Garoche over 5 years ago
| src/normalization.ml | ||
|---|---|---|
| 399 | 399 |
List.for_all ((!=) v) inputs_outputs in |
| 400 | 400 |
let orig_vars = inputs_outputs@node.node_locals in |
| 401 | 401 |
let defs, vars = |
| 402 |
List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in |
|
| 402 |
let eqs, auts = get_node_eqs node in |
|
| 403 |
if auts != [] then assert false; (* Automata should be expanded by now. *) |
|
| 404 |
List.fold_left (normalize_eq node) ([], orig_vars) eqs in |
|
| 403 | 405 |
(* Normalize the asserts *) |
| 404 | 406 |
let vars, assert_defs, asserts = |
| 405 | 407 |
List.fold_left ( |
Also available in: Unified diff
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons