diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-09-25 22:00:58 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-09-25 22:02:12 +0200 |
| commit | 42ab7386b7d1a312712bf8dd4031c06fce5bc1ff (patch) | |
| tree | 8ef70e4c949587c41a8faaa2adfd2b569b7fdd91 /src/hls/PrintAbstr.ml | |
| parent | f9511b82f6f0edb484b80e77fd531b510728aadc (diff) | |
| download | vericert-42ab7386b7d1a312712bf8dd4031c06fce5bc1ff.tar.gz vericert-42ab7386b7d1a312712bf8dd4031c06fce5bc1ff.zip | |
Add incremental evaluability check
Diffstat (limited to 'src/hls/PrintAbstr.ml')
| -rw-r--r-- | src/hls/PrintAbstr.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/hls/PrintAbstr.ml b/src/hls/PrintAbstr.ml index e1341b1..857b89c 100644 --- a/src/hls/PrintAbstr.ml +++ b/src/hls/PrintAbstr.ml @@ -81,9 +81,22 @@ let print_forest_exit pp f = fprintf pp "------------------- Exit -------------------\n"; print_predicated_exit pp f +let print_evaluability_list pp = function + | [] -> () + | r -> (fprintf pp "------------------- Eval -------------------\n"; + fprintf pp "["; List.iter (fun x -> fprintf pp "%a = %a\n" res (fst x) print_predicated (snd x)) r; fprintf pp "]"; + ) + +let print_evaluability_list2 pp = function + | [] -> () + | r -> (fprintf pp "------------------- Eval2 -------------------\n"; + fprintf pp "["; List.iter (fun x -> fprintf pp "%a\n" print_predicated x) r; fprintf pp "]"; + ) + let print_forest pp f = fprintf pp "#############################################\n"; fprintf pp "%a\n%a\n%a\n" print_forest_regs f.forest_regs print_forest_preds f.forest_preds print_forest_exit f.forest_exit + |