search

data61 / PSL

Other
65 stars 9 forks source link

Abduction: Parallel quickcheck. #189

Closed yutakang closed 1 year ago

yutakang commented 1 year ago

We should run quickcheck in parallel here and here.

Probably, we should introduce an auxiliary function for find_counterexample_update: Proof.state -> key -> proof_graph -> proof_graph.

try_to_refute_key: Proof.state -> proof_graph -> key -> (key * bool)

Then, val pairs = parallel_map (try_to_refute_key proof_state proof_graph) keys: (key * bool) list val updated_graph = fold find_counter_example_update' pairs proof_graph

yutakang commented 1 year ago

Mostly done in 4c7f7d2f0682fb3adfc952a09903e6c96b6984ad.

Still need refactoring.

I should also switch to one_of_ands_child_nodes_is_refuted for or-nodes.

yutakang commented 1 year ago

I revert this change.

We should focus on processing work_on_ornode_if_original_goral_is_unproved in parallel.