Stop emitting rules a predicate already forbids

[FelixLaarmann]

Problem:

Synthesizer.construct_solution_space_rules builds rules that can never be applied, and puts them
into the SolutionSpace anyway. Ten literal values and one predicate are enough to show it on
develop:

DIGITS = DataGroup("digits", range(10))
DIGIT = Constructor("Digit")

def digit(d): return f"digit {d}"
def above_seven(values): return values["d"] > 7

repo = {digit: SpecificationBuilder().parameter("d", DIGITS).constraint(above_seven).suffix(DIGIT)}
space = Synthesizer(repo).construct_solution_space(DIGIT)

len(list(space[DIGIT]))                                  # develop: 10, this branch: 2
[t.interpret() for t in space.enumerate_trees(DIGIT)]     # both: ['digit 8', 'digit 9']

Eight of the ten rules are unsatisfiable: d is fixed to a rejected value, and no later choice can
change that. enumerate_trees knows it -- it applies the predicate and returns two terms -- but the
eight rules stay in the space, and everything that reads the space rather than the terms is misled
by them.

prune treats such non-terminals as productive. It computes productivity purely structurally,
over RHSRule.non_terminals; predicates take no part in the algorithm at all. A rule with no
non-terminal argument is a base case for prune, whether or not its predicate admits it. Add a
consumer and the lie propagates:

repo = {digit: SpecificationBuilder().parameter("d", DataGroup("z", [0]))
               .constraint(above_seven).suffix(DIGIT),
        use:   Arrow(DIGIT, START)}
space = Synthesizer(repo).construct_solution_space(START)

[str(n) for n in space.nonterminals()]           # develop: ['Start', 'Digit'], this branch: ['Start']
[str(n) for n in space.prune().nonterminals()]   # develop: ['Digit', 'Start'], this branch: []

Digit has no term. prune keeps it, and keeps Start with it.

Depth-first resolution fails to terminate where it could have. Replace the consumer by a
recursive rule -- Digit -> zero whose predicate rejects the only literal value, plus
Digit -> wrap(Digit). Digit still has no term, and prune still keeps it, so the pruned space
is no help. develop answers wrap (digit 0), a term its own repository forbids and
contains_tree rejects. With the predicate check in Goal (the parallel pull request, see below)
the wrong answer is gone but the search descends into wrap(wrap(...)) without end. If the
rejected rule is never created, Digit is unproductive and prune() removes it, so a search over
the pruned space returns the empty result immediately.

How much of that reaches a caller who does not prune depends on whether the non-terminal keeps any
rule at all. If every one of its rules is rejected, it does not appear in the generated space to
begin with, and the search ends at once without pruning -- that is the case in the example above,
where space.nonterminals() no longer lists Digit. If it keeps a recursive rule, as here, it
stays in the space and an unpruned depth-first search still descends forever. That is correct for a
semi-decidable search on a query with no answer, and construct_solution_space does not prune on
its own -- prune() is the caller's decision, and this change is what finally makes it an informed
one.

Every count taken over the rules counts terms that do not exist. Rule counts, non-terminal
counts and anything derived from them are off by whatever the predicates forbid -- eight rules out
of ten in the example above.

Cause:

The rules are constructed without ever consulting the predicates. construct_solution_space_rules
carries specification_info.term_predicates through to the RHSRule it yields and hands the
decision to whoever reads the space later. For most rules that is the only thing it can do. For one
class of rules it is not, and that class is the one above.

The description of rules in SolutionSpace fixes what a predicate can see:

These arguments can be named, where the name corresponds to the variable in the logic program, or
unnamed, where the name is None. An unnamed argument still corresponds to NT_i(X_i) in the
logic program, but it cannot be used in the predicates [...] The predicates [...] are applied to
the specific substitution of the rule, which is given by the constant arguments and the
non-terminals arguments that have a name.

The synthesizer names exactly those non-terminal arguments that a component declares with
argument(...), that is, the TermParameters in its prefix. The non-terminal arguments it derives
from arrows inside the suffix stay unnamed. A combinator without a term parameter therefore
produces rules whose named part consists of constants alone, and the substitution its predicates
are applied to is exactly RHSRule.literal_substitution -- fully determined by the instantiation,
before a single argument type has been looked at. enumerate_trees confirms it from the other
side: its specific_substitution is the named non-terminal arguments unioned with
rule.literal_substitution, which collapses to the literal substitution when there are no named
arguments.

What changes:

One guard in construct_solution_space_rules, once per enumerated literal assignment, before any
subquery is computed for it:

if specification_info.term_predicates and not any(
    isinstance(parameter, TermParameter) for parameter in specification_info.prefix
):
    literal_substitution = {
        parameter.name: instantiation[parameter.name]
        for parameter in specification_info.prefix
        if isinstance(parameter, LiteralParameter)
    }
    if not all(predicate(literal_substitution) for predicate in specification_info.term_predicates):
        continue

No term parameter means no named non-terminal argument, which means the predicate substitution is
the literal substitution and nothing later can add to it. If a predicate is false on it, no rule is
constructed for this instantiation -- for any arity of the combinator type and any minimal cover.

[tudo-seal-workflows]

Benchmark CoSy

Details

Benchmark suite	Current: 852fd0f	Previous: be71b5d	Ratio
benchmarks/test_benchmark_maximal_elements.py::test_benchmark_maximal_elements	9.232243867255239 iter/sec (stddev: 0.0022244478848171415)	9.608281351562356 iter/sec (stddev: 0.010017085420616013)	1.04
benchmarks/test_benchmark_maze.py::test_benchmark_maze	3.9591295007486313 iter/sec (stddev: 0.012015487926278896)	3.9235166334572096 iter/sec (stddev: 0.018797551923491352)	0.99
benchmarks/test_benchmark_maze_contains.py::test_benchmark_maze_contains	3.6654905439301566 iter/sec (stddev: 0.014693018045307234)	3.5391214334611916 iter/sec (stddev: 0.025877608823890046)	0.97
benchmarks/test_benchmark_maze_loopfree.py::test_benchmark_maze_loopfree	3.802635910400676 iter/sec (stddev: 0.014009371245450463)	3.8477221717914887 iter/sec (stddev: 0.02072136799063595)	1.01

This comment was automatically generated by workflow using github-action-benchmark.

[codecov-commenter]

Codecov Report

❌ Patch coverage is 97.29730% with 3 lines in your changes missing coverage. Please review.
✅ Project coverage is 74.96%. Comparing base (2e318a2) to head (852fd0f).
⚠️ Report is 1 commits behind head on develop.
✅ All tests successful. No failed tests found.

Files with missing lines	Patch %	Lines
tests/test_unsatisfiable_clauses.py	97.19%	3 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop      #97      +/-   ##
===========================================
+ Coverage    73.02%   74.96%   +1.93%     
===========================================
  Files           39       41       +2     
  Lines         2944     3151     +207     
  Branches       494      500       +6     
===========================================
+ Hits          2150     2362     +212     
+ Misses         686      677       -9     
- Partials       108      112       +4     

Flag	Coverage Δ
macos-latest-3.10	74.57% <97.29%> (+1.75%)	⬆️
macos-latest-3.11	74.83% <97.29%> (+1.83%)	⬆️
macos-latest-3.12	74.83% <97.29%> (+1.93%)	⬆️
macos-latest-3.13	74.83% <97.29%> (+1.83%)	⬆️
ubuntu-latest-3.10	74.86% <97.29%> (+1.93%)	⬆️
ubuntu-latest-3.11	74.83% <97.29%> (+1.93%)	⬆️
ubuntu-latest-3.12	74.86% <97.29%> (+1.86%)	⬆️
ubuntu-latest-3.13	74.86% <97.29%> (+1.97%)	⬆️
windows-latest-3.10	74.86% <97.29%> (+2.14%)	⬆️
windows-latest-3.11	74.76% <97.29%> (+1.77%)	⬆️
windows-latest-3.12	74.92% <97.29%> (+1.93%)	⬆️
windows-latest-3.13	74.92% <97.29%> (+2.03%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.