Revision f3574a72
Added by Pierre-Loïc Garoche almost 4 years ago
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 3 | 3 |
open Seal_utils |
| 4 | 4 |
open Zustre_data (* Access to Z3 context *) |
| 5 | 5 |
|
| 6 |
let _ = |
|
| 7 |
Z3.Params.update_param_value !ctx "timeout" "10000" |
|
| 8 | 6 |
|
| 9 | 7 |
(* Switched system extraction: expression are memoized *) |
| 10 | 8 |
(*let expr_mem = Hashtbl.create 13*) |
| ... | ... | |
| 918 | 916 |
update) meaning "if cond then update" where update shall define all |
| 919 | 917 |
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) |
| 920 | 918 |
let node_as_switched_sys consts (mems:var_decl list) nd = |
| 919 |
Z3.Params.update_param_value !ctx "timeout" "10000"; |
|
| 920 |
|
|
| 921 |
|
|
| 921 | 922 |
(* rescheduling node: has been scheduled already, no need to protect |
| 922 | 923 |
the call to schedule_node *) |
| 923 | 924 |
let nd_report = Scheduling.schedule_node nd in |
Also available in: Unified diff
Moved some code