feat(synthesis): support (Array Float) holes in FloatHoleNG#404
Merged
alcides merged 3 commits intoJun 20, 2026
Conversation
a6501b7 to
4919562
Compare
c32b930 to
5cc5ff7
Compare
Extends FloatHoleNG beyond scalar Float holes to holes of type (Array Float): a single array hole becomes one optimisation dimension per element. Each hole now maps to a contiguous slice of one flat float vector — scalar holes take one dimension, an (Array Float) hole takes its length, read from a `size a == k` refinement — and is decoded back into either a Float literal or a list-valued Array Float literal substituted into the program. - (Array Float) holes require a fixed-size refinement (`size a == k`); the length is extracted by walking the refinement for an `Array_size == int` equality. Holes without one are rejected with a clear message. - Precondition is now stated in float dimensions (>= 2) rather than hole count, so a single (Array Float) hole of size >= 2 qualifies while a lone scalar Float hole still routes to the grammar backends. - examples/synthesis/float_ng/sphere_array.ae: sphere over a size-5 (Array Float) hole; both NGOpt and CMA reach the optimum, gp cannot. - Tests: _is_array_float, _array_length (size extraction, reversed operands, no-fixed-size case), end-to-end array convergence, and the updated dimension-count precondition message. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…he array Restructures the (Array Float) demo so the synthesized hole is the body of `sphere` and the function itself returns the array, matching the canonical Aeon pattern (objective decorates the hole-bearing function). Replaces the previous separate `def v = ?h` + `def sphere` split with a single function. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
With the stack rebased onto master (which has UFCS method calls, issue #27), the (Array Float) demo reads elements via `sphere.get i` (dispatching to Array.get) instead of the qualified `Array.get sphere i`. Also migrates the demo and the array test to master's surface syntax (`:=` definitions, single `=` in refinements). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
4919562 to
2c992d9
Compare
5cc5ff7 to
ebe487e
Compare
3 tasks
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
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.
Stacked on #403 (base:
claude/genomic-ng-float-holes), which is itself stacked on #401. Review/merge those first; this PR's diff is only the third commit.Summary
Extends FloatHoleNG (#403) beyond scalar
Floatholes to holes of type(Array Float)— a single array hole becomes one optimization dimension per element, which is the most natural framing for vector-valued continuous optimization.Each hole now maps to a contiguous slice of one flat float vector:
Floathole → one dimension → substituted as aFloatliteral;(Array Float)hole → its length k dimensions → substituted as a list-valuedArray Floatliteral ([v₀ … v_{k-1}], which the backend evaluates directly to a Python list).Determining the length
The length comes from a fixed-size refinement,
{a:(Array Float) | size a == k}— the sameArray_sizemeasure the multi-objective decorators use. The extractor walks the refinement for anArray_size == intequality (either operand order, inside conjunctions). An array hole without a fixed-size refinement is rejected with a clear message (its length is unknowable).Precondition
Now stated in float dimensions (≥ 2) rather than hole count, so a single
(Array Float)hole of size ≥ 2 qualifies, while a lone scalarFloathole still routes to the grammar backends.Benchmark —
examples/synthesis/float_ng/sphere_array.aeSphere over a single size-5
(Array Float)hole (scripts/bench_float_ng.py, 3s, 2 seeds):Both float backends reach the optimum;
gpcannot produce a usable array for this hole.Test plan
uv run pytest tests/float_ng_test.py— 15 passed, incl._is_array_float,_array_length(size extraction / reversed operands / no-fixed-size), end-to-end array convergence, and the updated precondition messagegenomic_ng/knee_point/synth_fitnesssuites still green🤖 Generated with Claude Code