nx_synth_oe.nx

nx_synth_oe.nx -- the synthesizer SCALED to S-class technique: bottom-up enumerative synthesis with OBSERVATIONAL-EQUIVALENCE pruning. Two sub-programs that produce the SAME output vector on the example inputs are interchangeable, so only ONE representative per distinct behaviour is kept. The search is then bounded by the number of distinct BEHAVIOURS, not the (exponential) number of programs -- the exact technique SOTA program synthesizers use to scale, and it lets us reach depth-3+ programs the naive <=2 enumerator never could. Research: Udupa et al., "TRANSIT: Specifying Protocols with Concolic Snippets," PLDI 2013 (observational equivalence); Alur et al., EUSolver / SyGuS; Massalin, AFIPS 1987 (superoptimizer). Exceed is MEASURED: candidates tried (P) vs distinct values kept (V); P/V is the collapse the pruning buys, A/B on the same task.