Fix enumerative search halting before budget for refined types (issue #89)

[alcides]

Summary

Fixes #89: the enumerative synthesizer was returning None for refined integer types like {y:Int | 0 < y && y < 100} because the grammar's unlimited-range Int literal (-100,000,000 to 100,000,000) exhausted the time budget before reaching any valid values.

• Replace unlimited Int literal with a metahandler-based one (IntRange(-1, 256)) — the enumerative search now iterates a small, practical default range instead of 200 million integers
• Use the refined type to generate a targeted metahandler literal — when the hole type is refined (e.g. {y:Int | 0 < y && y < 100}), an IntRange(1, 99) literal is added as a direct grammar alternative for æInt, with no refined abstract class as starting symbol
• Fix get_core() for refined literals — returns Literal(v, base_type) so the type checker handles it correctly
• Strip refinements from context variable types in grammar generation to avoid KeyError from mangled variable names in type_info
• Fix SynquidSynthesizer to strip the refined type before synthesis (Synquid only handles unrefined types)

Test plan

• New regression test test_enumerative_halts_within_budget passes: synthesizes a valid Int in (0, 100) within 0.25s budget (with a 10s SIGALRM safety guard)
• All existing synthesis tests still pass
• Full test suite: 184 passed, 3 skipped

🤖 Generated with Claude Code

[alcides]

Found and fixed the CI failure (build (3.11)).

Root cause: examples/synthesis/hole_refined_synthesis.ae defines (?hole: {x:Int | x > 0}) * i where i is a function parameter. During synthesis grammar generation, the bounds analysis in conditional_to_interval calls sympy's reduce_rational_inequalities with the constraint i² - x < 0 (non-linear, because i is also a variable). Sympy raises NotImplementedError for non-linear inequalities, which was re-raised as a generic Exception and crashed the whole synthesis run.

Fix (aeon/synthesis/grammar/bounds.py): catch the exception in conditional_to_interval and fall back to Interval(-oo, oo) (unbounded) instead of crashing. Synthesis continues normally — it just won't benefit from a tighter literal range for that constraint.

Pushed as branch fix-enumerative-bounds-nonlinear. All 18 synthesis tests still pass.