Abduction: something strange about cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals.

data61 / PSL

Other

65 stars 9 forks source link

Abduction: something strange about cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals. #202

Closed yutakang closed 1 year ago

yutakang commented 1 year ago

There is something strange about this function.

Why do I have to establish an (or-node) -> (labelled edge) -> (and-node) -> (or-node) connection first and then cut the edge between (labelled edge) -> (and-node)?

Can we just establish the (labelled edge) -> (and-node) connection only if this test returns a proof script?

yutakang commented 1 year ago

I decided to keep all the labelled edges that have been already tried in the graph even if they failed.

The reason for this decision is the following:

If we leave such edges in the graph, these edges let me know what steps have been already tried for the corresponding or-nodes.

This information is likely help us when we change our evaluation strategy from the depth-first search to the best-first search.

yutakang commented 1 year ago

Still, there are things that do not seem right about cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals.

1. This checking on the existing of an edge between an and-node and a labelled-edge got the order wrong. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L105
1. What is the point of computing this and_key here? https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L110
  - This and_key is meant be identical to the same as andnode_key passed as an argument here. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L102

yutakang commented 1 year ago

These issues are addressed in 8d490fc3ef6ee80cda8cc4f07cb64cd6c2d09ff0.

yutakang commented 1 year ago

I decided to keep all the labelled edges that have been already tried in the graph even if they failed.

The reason for this decision is the following:

If we leave such edges in the graph, these edges let me know what steps have been already tried for the corresponding or-nodes.

This information is likely help us when we change our evaluation strategy from the depth-first search to the best-first search.

There aren't enough benefits in doing so to justify this complexity of the code.

Even after we adopt the best-first search, we still have to work on the same or-node multiple times.

If necessary, we can cache the results in a separate table, as well.

yutakang commented 1 year ago

I decided to keep all the labelled edges that have been already tried in the graph even if they failed.

The reason for this decision is the following:

If we leave such edges in the graph, these edges let me know what steps have been already tried for the corresponding or-nodes.

This information is likely help us when we change our evaluation strategy from the depth-first search to the best-first search.

Haha. I am even failing to save the failed or2and edges :D

https://github.com/data61/PSL/blob/8d490fc3ef6ee80cda8cc4f07cb64cd6c2d09ff0/Abduction/Seed_Of_And_Node.ML#LL158C3-L158C3

yutakang commented 1 year ago

This function is also badly implemented. https://github.com/data61/PSL/blob/8d490fc3ef6ee80cda8cc4f07cb64cd6c2d09ff0/Abduction/Seed_Of_And_Node.ML#L138

yutakang commented 1 year ago

This function is also badly implemented.

https://github.com/data61/PSL/blob/8d490fc3ef6ee80cda8cc4f07cb64cd6c2d09ff0/Abduction/Seed_Of_And_Node.ML#L138

This issue is fixed in 8a95d25b6a81955c5162b2d5df2b4b5a0e238aeb.

yutakang commented 1 year ago

It is mostly fixed now. The new flow is explained here.

We still need to work on bunched conjecturing. But that will be handled in a different issue.

https://github.com/data61/PSL/issues/205