Alternate between DD and AR until goal is found.
(
g: gh.Graph,
theorems: list[pr.Problem],
controller: pr.Problem,
max_level: int = 1000,
timeout: int = 600,
)
| 75 | |
| 76 | |
| 77 | def solve( |
| 78 | g: gh.Graph, |
| 79 | theorems: list[pr.Problem], |
| 80 | controller: pr.Problem, |
| 81 | max_level: int = 1000, |
| 82 | timeout: int = 600, |
| 83 | ) -> tuple[gh.Graph, list[float], str, list[int], list[pr.Dependency]]: |
| 84 | """Alternate between DD and AR until goal is found.""" |
| 85 | status = 'saturated' |
| 86 | level_times = [] |
| 87 | |
| 88 | dervs, eq4 = g.derive_algebra(level=0, verbose=False) |
| 89 | derives = [dervs] |
| 90 | eq4s = [eq4] |
| 91 | branches = [] |
| 92 | all_added = [] |
| 93 | |
| 94 | while len(level_times) < max_level: |
| 95 | dervs, eq4, next_branches, added = saturate_or_goal( |
| 96 | g, theorems, level_times, controller, max_level, timeout=timeout |
| 97 | ) |
| 98 | all_added += added |
| 99 | |
| 100 | derives += dervs |
| 101 | eq4s += eq4 |
| 102 | branches += next_branches |
| 103 | |
| 104 | # Now, it is either goal or saturated |
| 105 | if controller.goal is not None: |
| 106 | goal_args = g.names2points(controller.goal.args) |
| 107 | if g.check(controller.goal.name, goal_args): # found goal |
| 108 | status = 'solved' |
| 109 | break |
| 110 | |
| 111 | if not derives: # officially saturated. |
| 112 | break |
| 113 | |
| 114 | # Now we resort to algebra derivations. |
| 115 | added = [] |
| 116 | while derives and not added: |
| 117 | added += dd.apply_derivations(g, derives.pop(0)) |
| 118 | |
| 119 | if added: |
| 120 | continue |
| 121 | |
| 122 | # Final help from AR. |
| 123 | while eq4s and not added: |
| 124 | added += dd.apply_derivations(g, eq4s.pop(0)) |
| 125 | |
| 126 | all_added += added |
| 127 | |
| 128 | if not added: # Nothing left. saturated. |
| 129 | break |
| 130 | |
| 131 | return g, level_times, status, branches, all_added |
| 132 | |
| 133 | |
| 134 | def get_proof_steps( |
nothing calls this directly
no test coverage detected