Yield every goal of a partial-term query, and each of them once - #99
Merged
Conversation
`goal_from_tree` describes the subterms that complete a term with a variable at one position into an inhabitant. It returned after the first goal it found -- "one goal is enough ??!!!" -- although its own docstring promises "Yields all valid goals" four lines above. A non-terminal is in general reached by more than one clause: for an intersection of arrows the inhabitation emits one clause per admissible subset of paths, and those clauses ask different sorts of their arguments. With `f : (A -> C) & (B -> C)` over `c : A & B`, `a : A` and `b : B`, all three constants complete `f(_)` and the query offered two of them. The root position was wrong in a way the early return hid. For `pos == ()` the whole term is replaced, so nothing of it constrains the query, but the initial goals were still matched against the root of the term about to be discarded -- which keeps only the clauses sharing its terminal. In the expression space of the new tests that is one clause out of three. Dropping the early return alone makes it worse. The traversal expanded every open subgoal in one step and pushed all the results, reaching the same goal once per order in which those positions happened to be expanded: six times for the variable at (0, 0) of add(add(x, x), neg(x)), eight for (1, 0). It expands one subgoal per step now, the deepest open one other than `pos`, which is the selection the uninformed resolution strategies already use. Measured on the expression space: a query at an inner position is unchanged, a root query streams the terms it was missing (169 -> 183 within depth 3) at +7% time, and a prescribed term with many open positions gets cheaper because the factorial expansion is gone -- a chain of seven add nodes queried at (1, 0) drops from 0.527 ms to 0.402 ms. `resolution` is the only caller, reached through `depth_first_resolution`, `breadth_first_resolution` and `sample_tree` when `tree` and `pos` are given, and through `sample_tree` by `ResolutionMutation`. The resolutions return more results than before. `sample_tree` returns one, and for `pos == ()` it now returns what `sample_tree` without `tree` and `pos` returns -- the first ground clause -- because the root filter that used to hide it is gone. `ResolutionMutation` is unaffected: it mutates neither the root nor a leaf, and an inner position leaves every goal open. Calls without `tree` and `pos` are unaffected.
![tudo-seal-workflows[bot]](https://avatars.githubusercontent.com/in/2312552?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Benchmark CoSy
Details
| Benchmark suite | Current: e41a3ae | Previous: be71b5d | Ratio |
|---|---|---|---|
benchmarks/test_benchmark_maximal_elements.py::test_benchmark_maximal_elements |
16.54398307334902 iter/sec (stddev: 0.0007198152092830312) |
9.608281351562356 iter/sec (stddev: 0.010017085420616013) |
0.58 |
benchmarks/test_benchmark_maze.py::test_benchmark_maze |
6.405888544593071 iter/sec (stddev: 0.01093601297431421) |
3.9235166334572096 iter/sec (stddev: 0.018797551923491352) |
0.61 |
benchmarks/test_benchmark_maze_contains.py::test_benchmark_maze_contains |
5.890040602372219 iter/sec (stddev: 0.01157984005005016) |
3.5391214334611916 iter/sec (stddev: 0.025877608823890046) |
0.60 |
benchmarks/test_benchmark_maze_loopfree.py::test_benchmark_maze_loopfree |
6.3832975991926135 iter/sec (stddev: 0.014913532822996654) |
3.8477221717914887 iter/sec (stddev: 0.02072136799063595) |
0.60 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #99 +/- ##
===========================================
+ Coverage 78.69% 79.28% +0.59%
===========================================
Files 45 47 +2
Lines 3703 3833 +130
Branches 532 532
===========================================
+ Hits 2914 3039 +125
- Misses 688 693 +5
Partials 101 101
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
mrhaandi
approved these changes
Aug 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem:
SolutionSpace.goal_from_tree(start, tree, pos)builds the goals of the query that prescribestreeeverywhere except atpos, where it leaves a variable. It returned after the first goalit found:
Four lines above, its own docstring promises "Yields all valid goals". Three defects follow:
inhabitation emits one clause per admissible subset of paths, and those clauses ask different
sorts of their arguments. With
f : (A -> C) & (B -> C)overc : A & B,a : Aandb : B, the variable inf(_)is completed by all three constants; the query offeredwhichever two the search reached first.
pos == ()thewhole term is replaced, yet the initial goals kept only clauses whose terminal matches the
root of
tree. InE -> lit | neg(E) | add(E, E), handedneg(lit)and asked to replace itentirely, the query returned
negterms and nothing else — one clause out of three.subgoal in one step, so a goal with several open positions was reached once per order in which
they happened to be expanded — six times for
(0, 0)ofadd(add(x, x), neg(x)), eight for(1, 0). Invisible while the search stops at the first hit, a factorial over-count once itdoes not.
What changes:
Each goal is yielded once. The success test is applied when a goal leaves the frontier, and such
a goal is not expanded further. For
pos == ()the clauses ofstartbecome goals directly,without the root match. The traversal expands one subgoal per step: the deepest open one other
than
pos, leftmost among those — the selectiondepth_first_resolutionandbreadth_first_resolutionalready document and use, so the reachable goals are the same and onlythe derivation tree walked to reach them changes.