st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: remove commented tests from prev iteration

Browse source
This commit is contained in:
ProgramSnail 2026-05-09 15:49:07 +00:00
parent e79b7fa7bc
commit 1a61fb01ee
2 changed files with 0 additions and 111 deletions
Download patch file Download diff file Expand all files Collapse all files

2
model_with_structures/tests.ml
View file

@ -76,5 +76,3 @@ let%expect_test "simple synthesis test, reference forbidden write" = print_endli
let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ()); let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ());
[%expect {| [Cp; Cp; Cp; Cp] |}] [%expect {| [Cp; Cp; Cp; Cp] |}]
(* TODO *)

109
model_with_structures/tests_f.ml
View file

@ -485,112 +485,3 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog st }) prog_evalo prog st })
(fun q -> q#reify (CopyCap.prj_exn)))) (fun q -> q#reify (CopyCap.prj_exn))))
(* annotation gen prog test *)
(* let synt_t2 _ = show(answerTag) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> q#reify (Tag.prj_exn)))) *)
(* annotation gen prog test *)
(* let synt_t3 _ = show(answerTags) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *)
(* annotation gen prog test *)
(* let synt_t4 _ = show(answerTags) (Stream.take (run q *)
(* (fun q -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {i_any q & is_not_reado q & *)
(* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *)
(* annotation gen prog test *)
(* let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
(* annotation gen prog test *)
(* let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_not_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
(* annotation gen prog test *)
(* let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
(* annotation gen prog test *)
(* let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
(* annotation gen prog test *)
(* let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr *)
(* (fun q r -> let open Prog in *)
(* let open FunDecl in *)
(* let open Tag in *)
(* let open Stmt in *)
(* let open St in *)
(* ocanren {fresh q', r' in *)
(* i_any q' & is_not_reado q' & *)
(* i_any r' & is_reado r' & is_never_writeo r' & *)
(* eq_copyo q' q & eq_copyo r' r & *)
(* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *)
(* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
(* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)