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 /debug/vericertTest.ml | |
| parent | f9511b82f6f0edb484b80e77fd531b510728aadc (diff) | |
| download | vericert-42ab7386b7d1a312712bf8dd4031c06fce5bc1ff.tar.gz vericert-42ab7386b7d1a312712bf8dd4031c06fce5bc1ff.zip | |
Add incremental evaluability check
Diffstat (limited to 'debug/vericertTest.ml')
| -rw-r--r-- | debug/vericertTest.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml index 48391db..87c9e60 100644 --- a/debug/vericertTest.ml +++ b/debug/vericertTest.ml @@ -26,7 +26,12 @@ let schedule_oracle l bb bbt = let (p2, m_expr_t) = p1 in let (bbt', reg_expr_t) = p2 in printf "F1:\n%a\n" PrintAbstr.print_forest bb'; - printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout; + printf "%a\n" PrintAbstr.print_evaluability_list reg_expr; + printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr; + printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; + printf "%a\n" PrintAbstr.print_evaluability_list reg_expr_t; + printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr_t; + flush stdout; (&&) ((&&) ((&&) (if check l bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt)) (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false))) @@ -179,12 +184,12 @@ let () = seteq None 2 12 13; add None 2 1 4; mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; - mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; goto (Some (Pand (plit false 1, plit false 2))) 10; mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; goto (Some (Pand (plit false 1, plit true 2))) 10; add (Some (plit true 1)) 1 2 4; - mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; goto (Some (Pand (plit true 1, plit false 2))) 10; mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; goto (Some (Pand (plit true 1, plit true 2))) 10; @@ -197,8 +202,8 @@ let () = add (Some (plit true 1)) 1 2 4; mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; - mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; - mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; + mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; goto None 10; ] ] ] then Printf.printf "Passed 110\n" |