Abduction: something strange about cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals. about psl HOT 8 CLOSED

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.

from psl.

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.
     

     PSL/Abduction/Seed_Of_And_Node.ML

     Line 105 in 9084e8e

     if PGraph.is_edge graph (andnode_key, or2and_edge_key)

• 2. What is the point of computing this and_key here?
     

     PSL/Abduction/Seed_Of_And_Node.ML

     Line 110 in 9084e8e

     val and_key = hd and_keys: key;

  • This and_key is meant be identical to the same as andnode_key passed as an argument here.
    

    PSL/Abduction/Seed_Of_And_Node.ML

    Line 102 in 9084e8e

    (andnode_key: key) (or2and_edge_key:key) (graph:abduction_graph): abduction_graph =

from psl.

These issues are addressed in 8d490fc.

from psl.

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.

from psl.

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

from psl.

This function is also badly implemented.

from psl.

This function is also badly implemented.

PSL/Abduction/Seed_Of_And_Node.ML

Line 138 in 8d490fc

val script_opt: string option =

This issue is fixed in 8a95d25.

from psl.

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.

#205

from psl.