Grammar-to-Solver Handoff Lab

The grammar keeps candidates valid. The semantic target still stalls structured search. A bounded solver can then take over and either finish the witness or report that no witness exists inside the grammar's range.

random bytes → grammar-valid expressions → bounded local solve for a * b = target

What this lab shows

The grammar fixes syntax, but it does not automatically solve the remaining value constraint. The hybrid lane becomes useful only after structured search has already kept the candidate inside the language. This lab deliberately uses a smaller grammar than Tutorial 36 so the handoff stays easy to see.

Try this first

Run target 42 first. Then switch to 97. The first target has a witness inside the grammar range, while the second does not. That contrast shows what a bounded solver can and cannot honestly claim.

Start here Run the default target once, then compare the three lanes. The summary will tell you whether the solver finished a real witness or honestly reported that none exists inside the grammar range.

Tiny language and target

Raw bytes: any 3 printable chars
Grammar G:
  Expr ::= Digit Op Digit
  Digit ::= 1 | 2 | ... | 9
  Op    ::= + | * | /
Bad(x) holds if:
1. x parses as Digit Op Digit
2. x reaches semantic evaluation
3. op = *
4. a * b = target

Comparison

Random bytes

not run yet

Grammar only

not run yet

Grammar + solver

not run yet

Recent candidates

The key teaching point is not that the solver replaces the grammar. It does not. The grammar keeps the witness inside a valid language, then the solver works only over the remaining local value constraints.

Solver handoff

No run yet.

Detailed log