oxilean_std/program_synthesis/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7use super::types::{
8    BottomUpSynth, Candidate, CegisState, Component, ComponentLibrary, FlashFillSynth, FoilLearner,
9    FuncProgram, Hole, ILPProblem, IOExample, OGISSynthesizer, OracleSynthLoop, ProgramSketch,
10    RefinementType, Sketch, Spec, SyGuSProblem, SynthContext, SynthType, TableOracle,
11    TypeDirectedSynth, VersionSpace, CFG,
12};
13
14pub fn app(f: Expr, a: Expr) -> Expr {
15    Expr::App(Box::new(f), Box::new(a))
16}
17pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
18    app(app(f, a), b)
19}
20pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
21    app(app2(f, a, b), c)
22}
23pub fn cst(s: &str) -> Expr {
24    Expr::Const(Name::str(s), vec![])
25}
26pub fn prop() -> Expr {
27    Expr::Sort(Level::zero())
28}
29pub fn type0() -> Expr {
30    Expr::Sort(Level::succ(Level::zero()))
31}
32pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
33    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
34}
35pub(super) fn arrow(a: Expr, b: Expr) -> Expr {
36    pi(BinderInfo::Default, "_", a, b)
37}
38pub fn bvar(n: u32) -> Expr {
39    Expr::BVar(n)
40}
41pub fn nat_ty() -> Expr {
42    cst("Nat")
43}
44pub fn bool_ty() -> Expr {
45    cst("Bool")
46}
47pub fn string_ty() -> Expr {
48    cst("String")
49}
50pub fn list_ty(elem: Expr) -> Expr {
51    app(cst("List"), elem)
52}
53pub fn option_ty(t: Expr) -> Expr {
54    app(cst("Option"), t)
55}
56pub fn pair_ty(a: Expr, b: Expr) -> Expr {
57    app2(cst("Prod"), a, b)
58}
59/// An oracle that can answer membership queries about the target function.
60pub trait Oracle {
61    /// Given an input, return the expected output (consulting the oracle).
62    fn query(&self, input: &[String]) -> Option<String>;
63}
64pub fn add_axiom(env: &mut Environment, name: &str, ty: Expr) -> Result<(), String> {
65    let decl = Declaration::Axiom {
66        name: Name::str(name),
67        univ_params: vec![],
68        ty,
69    };
70    env.add(decl).map_err(|e| format!("{:?}", e))
71}
72/// Build the kernel environment with program synthesis axioms.
73///
74/// Declares types and properties for:
75/// - Specification satisfiability
76/// - CEGIS completeness
77/// - SyGuS soundness
78/// - Type-directed synthesis completeness (Djinn)
79/// - Component-based soundness and completeness
80/// - Sketch-based correctness
81/// - Inductive synthesis correctness
82/// - Oracle-guided query complexity
83pub fn build_program_synthesis_env(env: &mut Environment) -> Result<(), String> {
84    add_axiom(
85        env,
86        "SpecSatisfied",
87        arrow(cst("Spec"), arrow(cst("Program"), prop())),
88    )?;
89    add_axiom(env, "SpecConsistent", arrow(cst("Spec"), prop()))?;
90    add_axiom(
91        env,
92        "SpecEquiv",
93        arrow(cst("Spec"), arrow(cst("Spec"), prop())),
94    )?;
95    add_axiom(env, "CegisSpec", arrow(cst("Spec"), cst("Spec")))?;
96    add_axiom(env, "CegisCandidate", cst("Spec"))?;
97    add_axiom(
98        env,
99        "CegisComplete",
100        arrow(cst("Spec"), arrow(prop(), prop())),
101    )?;
102    add_axiom(
103        env,
104        "CegisSound",
105        arrow(cst("Spec"), arrow(cst("Program"), prop())),
106    )?;
107    add_axiom(
108        env,
109        "CegisCounterexample",
110        arrow(cst("Program"), arrow(cst("Input"), prop())),
111    )?;
112    add_axiom(
113        env,
114        "SyGuSGrammarMembership",
115        arrow(cst("Program"), arrow(cst("Grammar"), prop())),
116    )?;
117    add_axiom(
118        env,
119        "SyGuSSoundness",
120        arrow(
121            cst("Spec"),
122            arrow(cst("Grammar"), arrow(cst("Program"), prop())),
123        ),
124    )?;
125    add_axiom(
126        env,
127        "SyGuSCompleteness",
128        arrow(cst("Spec"), arrow(cst("Grammar"), prop())),
129    )?;
130    add_axiom(
131        env,
132        "SyGuSEnumerationBound",
133        arrow(nat_ty(), arrow(cst("Grammar"), nat_ty())),
134    )?;
135    add_axiom(
136        env,
137        "DeductiveDerivation",
138        arrow(cst("Spec"), arrow(cst("Program"), prop())),
139    )?;
140    add_axiom(
141        env,
142        "DeductiveCorrect",
143        arrow(cst("Spec"), arrow(cst("Program"), prop())),
144    )?;
145    add_axiom(
146        env,
147        "WeakestPrecondition",
148        arrow(cst("Program"), arrow(cst("Assertion"), cst("Assertion"))),
149    )?;
150    add_axiom(
151        env,
152        "StrongestPostcondition",
153        arrow(cst("Program"), arrow(cst("Assertion"), cst("Assertion"))),
154    )?;
155    add_axiom(env, "TypeInhabited", arrow(cst("SynthType"), prop()))?;
156    add_axiom(
157        env,
158        "TypedTerm",
159        arrow(cst("SynthType"), arrow(cst("SynthContext"), prop())),
160    )?;
161    add_axiom(
162        env,
163        "DjinnComplete",
164        arrow(cst("SynthType"), arrow(cst("SynthContext"), prop())),
165    )?;
166    add_axiom(
167        env,
168        "DjinnSound",
169        arrow(cst("SynthType"), arrow(cst("Program"), prop())),
170    )?;
171    add_axiom(
172        env,
173        "TypeDirectedSearchDepth",
174        arrow(cst("SynthType"), nat_ty()),
175    )?;
176    add_axiom(
177        env,
178        "ComponentApplicable",
179        arrow(cst("Component"), arrow(cst("Input"), prop())),
180    )?;
181    add_axiom(
182        env,
183        "ComponentCorrect",
184        arrow(
185            cst("Component"),
186            arrow(cst("Input"), arrow(cst("Output"), prop())),
187        ),
188    )?;
189    add_axiom(
190        env,
191        "ComponentComposition",
192        arrow(cst("Component"), arrow(cst("Component"), cst("Component"))),
193    )?;
194    add_axiom(
195        env,
196        "ComponentSynthSound",
197        arrow(
198            cst("Spec"),
199            arrow(cst("ComponentLibrary"), arrow(cst("Program"), prop())),
200        ),
201    )?;
202    add_axiom(
203        env,
204        "SketchCompletion",
205        arrow(cst("Sketch"), arrow(cst("Spec"), option_ty(cst("Program")))),
206    )?;
207    add_axiom(
208        env,
209        "SketchCorrect",
210        arrow(
211            cst("Sketch"),
212            arrow(cst("Spec"), arrow(cst("Program"), prop())),
213        ),
214    )?;
215    add_axiom(env, "HoleCount", arrow(cst("Sketch"), nat_ty()))?;
216    add_axiom(
217        env,
218        "SketchSubsumes",
219        arrow(cst("Sketch"), arrow(cst("Grammar"), prop())),
220    )?;
221    add_axiom(
222        env,
223        "ExampleConsistency",
224        arrow(cst("Program"), arrow(list_ty(cst("IOExample")), prop())),
225    )?;
226    add_axiom(
227        env,
228        "VersionSpaceNonEmpty",
229        arrow(list_ty(cst("IOExample")), prop()),
230    )?;
231    add_axiom(
232        env,
233        "PBEConvergence",
234        arrow(nat_ty(), arrow(list_ty(cst("IOExample")), prop())),
235    )?;
236    add_axiom(
237        env,
238        "FlashFillCorrect",
239        arrow(list_ty(cst("IOExample")), arrow(cst("Program"), prop())),
240    )?;
241    add_axiom(
242        env,
243        "OracleQuery",
244        arrow(cst("Input"), option_ty(cst("Output"))),
245    )?;
246    add_axiom(
247        env,
248        "OracleGuided",
249        arrow(cst("Oracle"), arrow(nat_ty(), option_ty(cst("Program")))),
250    )?;
251    add_axiom(env, "OracleQueryComplexity", arrow(nat_ty(), nat_ty()))?;
252    add_axiom(
253        env,
254        "StructuralRecursion",
255        arrow(cst("FuncProgram"), prop()),
256    )?;
257    add_axiom(
258        env,
259        "FuncSynthCorrect",
260        arrow(cst("Spec"), arrow(cst("FuncProgram"), prop())),
261    )?;
262    add_axiom(
263        env,
264        "FuncSynthTerminating",
265        arrow(cst("Spec"), arrow(nat_ty(), prop())),
266    )?;
267    add_axiom(
268        env,
269        "BottomUpEnumCorrect",
270        arrow(nat_ty(), arrow(cst("Spec"), option_ty(cst("FuncProgram")))),
271    )?;
272    Ok(())
273}
274/// Inductive program synthesis: soundness of inductive generalization.
275pub fn axiom_inductive_generalization_ty() -> Expr {
276    arrow(list_ty(cst("IOExample")), arrow(cst("Program"), prop()))
277}
278/// Inductive program synthesis: completeness over a finite hypothesis space.
279pub fn axiom_inductive_completeness_ty() -> Expr {
280    arrow(
281        cst("HypothesisSpace"),
282        arrow(list_ty(cst("IOExample")), option_ty(cst("Program"))),
283    )
284}
285/// Minimal description length principle for inductive synthesis.
286pub fn axiom_mdl_synthesis_ty() -> Expr {
287    arrow(cst("Program"), arrow(list_ty(cst("IOExample")), nat_ty()))
288}
289/// SyGuS multi-function: soundness when synthesising several functions jointly.
290pub fn axiom_sygus_multi_function_ty() -> Expr {
291    arrow(list_ty(cst("SyGuSProblem")), arrow(cst("Grammar"), prop()))
292}
293/// SyGuS separability: two grammars produce disjoint solution sets.
294pub fn axiom_sygus_separability_ty() -> Expr {
295    arrow(cst("Grammar"), arrow(cst("Grammar"), prop()))
296}
297/// CEGIS with bounded counterexample depth.
298pub fn axiom_cegis_bounded_depth_ty() -> Expr {
299    arrow(nat_ty(), arrow(cst("Spec"), arrow(cst("Program"), prop())))
300}
301/// CEGIS acceleration: convergence rate under a strong verifier.
302pub fn axiom_cegis_convergence_rate_ty() -> Expr {
303    arrow(cst("Spec"), arrow(nat_ty(), nat_ty()))
304}
305/// Oracle-guided synthesis with membership queries only.
306pub fn axiom_oracle_membership_query_ty() -> Expr {
307    arrow(cst("Input"), bool_ty())
308}
309/// Oracle-guided synthesis with equivalence queries.
310pub fn axiom_oracle_equivalence_query_ty() -> Expr {
311    arrow(
312        cst("Program"),
313        arrow(cst("Oracle"), pair_ty(bool_ty(), option_ty(cst("Input")))),
314    )
315}
316/// Oracle-guided synthesis: Angluin's L* query complexity bound.
317pub fn axiom_lstar_query_complexity_ty() -> Expr {
318    arrow(nat_ty(), arrow(nat_ty(), nat_ty()))
319}
320/// Type-driven synthesis: refinement type checking decidability.
321pub fn axiom_refinement_type_decidable_ty() -> Expr {
322    arrow(cst("RefinementType"), arrow(cst("Program"), prop()))
323}
324/// Refinement type synthesis: soundness of liquid type inference.
325pub fn axiom_liquid_type_soundness_ty() -> Expr {
326    arrow(cst("Program"), arrow(cst("RefinementType"), prop()))
327}
328/// Refinement type synthesis: completeness for subtyping.
329pub fn axiom_refinement_subtype_complete_ty() -> Expr {
330    arrow(cst("RefinementType"), arrow(cst("RefinementType"), prop()))
331}
332/// Manna–Waldinger deductive synthesis: resolution correctness.
333pub fn axiom_mw_resolution_correct_ty() -> Expr {
334    arrow(cst("Goal"), arrow(cst("Program"), prop()))
335}
336/// Manna–Waldinger synthesis: goal reduction termination.
337pub fn axiom_mw_termination_ty() -> Expr {
338    arrow(cst("Goal"), prop())
339}
340/// Synthesis from logical specifications: realizability.
341pub fn axiom_spec_realizability_ty() -> Expr {
342    arrow(cst("Spec"), prop())
343}
344/// Synthesis from specifications: Church's synthesis problem.
345pub fn axiom_church_synthesis_ty() -> Expr {
346    arrow(cst("LTLSpec"), option_ty(cst("ReactiveProgram")))
347}
348/// Neural program synthesis: soundness of learned synthesiser.
349pub fn axiom_neural_synth_soundness_ty() -> Expr {
350    arrow(
351        cst("NeuralModel"),
352        arrow(list_ty(cst("IOExample")), option_ty(cst("Program"))),
353    )
354}
355/// Neural program synthesis: generalisation bound (PAC-style).
356pub fn axiom_neural_synth_generalisation_ty() -> Expr {
357    arrow(nat_ty(), arrow(cst("NeuralModel"), prop()))
358}
359/// Execution-guided synthesis: observable semantics consistency.
360pub fn axiom_execution_guided_consistency_ty() -> Expr {
361    arrow(
362        cst("Program"),
363        arrow(list_ty(cst("ExecutionTrace")), prop()),
364    )
365}
366/// Execution-guided synthesis: trace completeness.
367pub fn axiom_execution_trace_complete_ty() -> Expr {
368    arrow(list_ty(cst("ExecutionTrace")), option_ty(cst("Program")))
369}
370/// Constraint-based synthesis: SAT encoding correctness.
371pub fn axiom_constraint_encoding_correct_ty() -> Expr {
372    arrow(cst("SynthConstraint"), arrow(cst("Program"), prop()))
373}
374/// Constraint-based synthesis: finite domain decidability.
375pub fn axiom_finite_domain_decidable_ty() -> Expr {
376    arrow(cst("SynthConstraint"), prop())
377}
378/// Superoptimisation: optimality of synthesised loop-free program.
379pub fn axiom_superopt_optimal_ty() -> Expr {
380    arrow(cst("Program"), arrow(cst("CostModel"), prop()))
381}
382/// Superoptimisation: equivalence preservation.
383pub fn axiom_superopt_equivalence_ty() -> Expr {
384    arrow(cst("Program"), arrow(cst("Program"), prop()))
385}
386/// Loop invariant synthesis: inductive invariant correctness.
387pub fn axiom_loop_invariant_correct_ty() -> Expr {
388    arrow(cst("LoopBody"), arrow(cst("Assertion"), prop()))
389}
390/// Loop invariant synthesis: strongest inductive invariant existence.
391pub fn axiom_strongest_invariant_exists_ty() -> Expr {
392    arrow(cst("LoopBody"), option_ty(cst("Assertion")))
393}
394/// Sketch framework: hole satisfiability modulo theory.
395pub fn axiom_sketch_hole_smt_ty() -> Expr {
396    arrow(
397        cst("Sketch"),
398        arrow(cst("Theory"), option_ty(cst("Assignment"))),
399    )
400}
401/// FlashMeta: DSL synthesis via version space algebra.
402pub fn axiom_flashmeta_vsa_ty() -> Expr {
403    arrow(
404        list_ty(cst("IOExample")),
405        arrow(cst("DSL"), cst("VersionSpace")),
406    )
407}
408/// FlashFill generalization: number of examples sufficient for uniqueness.
409pub fn axiom_flashfill_unique_threshold_ty() -> Expr {
410    arrow(nat_ty(), arrow(list_ty(cst("IOExample")), prop()))
411}
412/// Abstraction-based synthesis: abstraction refinement correctness.
413pub fn axiom_abstraction_refinement_correct_ty() -> Expr {
414    arrow(cst("Abstraction"), arrow(cst("Spec"), prop()))
415}
416/// Abstraction-based synthesis: spurious counterexample detection.
417pub fn axiom_spurious_cex_detection_ty() -> Expr {
418    arrow(cst("Abstraction"), arrow(cst("Counterexample"), bool_ty()))
419}
420/// Learning from demonstrations: behavioral cloning correctness.
421pub fn axiom_behavioral_cloning_correct_ty() -> Expr {
422    arrow(list_ty(cst("Demonstration")), arrow(cst("Policy"), prop()))
423}
424/// Learning from demonstrations: inverse reinforcement learning soundness.
425pub fn axiom_irl_soundness_ty() -> Expr {
426    arrow(
427        list_ty(cst("Demonstration")),
428        arrow(cst("RewardFunction"), prop()),
429    )
430}
431/// Program synthesis by A* search: admissible heuristic correctness.
432pub fn axiom_astar_synth_admissible_ty() -> Expr {
433    arrow(cst("Heuristic"), arrow(cst("SynthState"), nat_ty()))
434}
435/// Stochastic program synthesis: probabilistic soundness.
436pub fn axiom_stochastic_synth_soundness_ty() -> Expr {
437    arrow(cst("ProbDistribution"), arrow(cst("Spec"), prop()))
438}
439/// Synthesis with sketches: relative completeness wrt sketch language.
440pub fn axiom_sketch_relative_complete_ty() -> Expr {
441    arrow(cst("SketchLanguage"), arrow(cst("Spec"), prop()))
442}
443/// Build the extended program synthesis environment (new axioms).
444///
445/// Adds 30+ new axioms covering:
446/// - Inductive synthesis (MDL, PBE generalization)
447/// - CEGIS extensions (bounded depth, convergence rate)
448/// - SyGuS extensions (multi-function, separability)
449/// - Oracle-guided synthesis (membership, equivalence, L*)
450/// - Refinement types (liquid types, subtyping)
451/// - Manna–Waldinger synthesis
452/// - Neural, execution-guided, and constraint-based synthesis
453/// - Superoptimisation
454/// - Loop invariant synthesis
455/// - Sketch / FlashFill / FlashMeta
456/// - Abstraction-based synthesis
457/// - Learning from demonstrations
458/// - Stochastic and search-based synthesis
459pub fn build_program_synthesis_env_ext(env: &mut Environment) -> Result<(), String> {
460    let axioms: &[(&str, Expr)] = &[
461        (
462            "InductiveGeneralization",
463            axiom_inductive_generalization_ty(),
464        ),
465        ("InductiveCompleteness", axiom_inductive_completeness_ty()),
466        ("MDLSynthesis", axiom_mdl_synthesis_ty()),
467        ("SyGuSMultiFunction", axiom_sygus_multi_function_ty()),
468        ("SyGuSSeparability", axiom_sygus_separability_ty()),
469        ("CegisBoundedDepth", axiom_cegis_bounded_depth_ty()),
470        ("CegisConvergenceRate", axiom_cegis_convergence_rate_ty()),
471        ("OracleMembershipQuery", axiom_oracle_membership_query_ty()),
472        (
473            "OracleEquivalenceQuery",
474            axiom_oracle_equivalence_query_ty(),
475        ),
476        ("LStarQueryComplexity", axiom_lstar_query_complexity_ty()),
477        (
478            "RefinementTypeDecidable",
479            axiom_refinement_type_decidable_ty(),
480        ),
481        ("LiquidTypeSoundness", axiom_liquid_type_soundness_ty()),
482        (
483            "RefinementSubtypeComplete",
484            axiom_refinement_subtype_complete_ty(),
485        ),
486        ("MWResolutionCorrect", axiom_mw_resolution_correct_ty()),
487        ("MWTermination", axiom_mw_termination_ty()),
488        ("SpecRealizability", axiom_spec_realizability_ty()),
489        ("ChurchSynthesis", axiom_church_synthesis_ty()),
490        ("NeuralSynthSoundness", axiom_neural_synth_soundness_ty()),
491        (
492            "NeuralSynthGeneralisation",
493            axiom_neural_synth_generalisation_ty(),
494        ),
495        (
496            "ExecutionGuidedConsistency",
497            axiom_execution_guided_consistency_ty(),
498        ),
499        (
500            "ExecutionTraceComplete",
501            axiom_execution_trace_complete_ty(),
502        ),
503        (
504            "ConstraintEncodingCorrect",
505            axiom_constraint_encoding_correct_ty(),
506        ),
507        ("FiniteDomainDecidable", axiom_finite_domain_decidable_ty()),
508        ("SuperoptOptimal", axiom_superopt_optimal_ty()),
509        ("SuperoptEquivalence", axiom_superopt_equivalence_ty()),
510        ("LoopInvariantCorrect", axiom_loop_invariant_correct_ty()),
511        (
512            "StrongestInvariantExists",
513            axiom_strongest_invariant_exists_ty(),
514        ),
515        ("SketchHoleSMT", axiom_sketch_hole_smt_ty()),
516        ("FlashMetaVSA", axiom_flashmeta_vsa_ty()),
517        (
518            "FlashFillUniqueThreshold",
519            axiom_flashfill_unique_threshold_ty(),
520        ),
521        (
522            "AbstractionRefinementCorrect",
523            axiom_abstraction_refinement_correct_ty(),
524        ),
525        ("SpuriousCexDetection", axiom_spurious_cex_detection_ty()),
526        (
527            "BehavioralCloningCorrect",
528            axiom_behavioral_cloning_correct_ty(),
529        ),
530        ("IRLSoundness", axiom_irl_soundness_ty()),
531        ("AStarSynthAdmissible", axiom_astar_synth_admissible_ty()),
532        (
533            "StochasticSynthSoundness",
534            axiom_stochastic_synth_soundness_ty(),
535        ),
536        (
537            "SketchRelativeComplete",
538            axiom_sketch_relative_complete_ty(),
539        ),
540    ];
541    for (name, ty) in axioms {
542        add_axiom(env, name, ty.clone())?;
543    }
544    Ok(())
545}
546/// Build a single `SpecSatisfied` axiom declaration.
547pub fn decl_spec_satisfied() -> Declaration {
548    Declaration::Axiom {
549        name: Name::str("SpecSatisfied"),
550        univ_params: vec![],
551        ty: arrow(cst("Spec"), arrow(cst("Program"), prop())),
552    }
553}
554/// Build the `CegisComplete` axiom declaration.
555pub fn decl_cegis_complete() -> Declaration {
556    Declaration::Axiom {
557        name: Name::str("CegisComplete"),
558        univ_params: vec![],
559        ty: arrow(cst("Spec"), arrow(prop(), prop())),
560    }
561}
562/// Build the `SyGuSSoundness` axiom declaration.
563pub fn decl_sygus_soundness() -> Declaration {
564    Declaration::Axiom {
565        name: Name::str("SyGuSSoundness"),
566        univ_params: vec![],
567        ty: arrow(
568            cst("Spec"),
569            arrow(cst("Grammar"), arrow(cst("Program"), prop())),
570        ),
571    }
572}
573/// Build the `DjinnComplete` axiom declaration.
574pub fn decl_djinn_complete() -> Declaration {
575    Declaration::Axiom {
576        name: Name::str("DjinnComplete"),
577        univ_params: vec![],
578        ty: arrow(cst("SynthType"), arrow(cst("SynthContext"), prop())),
579    }
580}
581/// Build the `PBEConvergence` axiom declaration.
582pub fn decl_pbe_convergence() -> Declaration {
583    Declaration::Axiom {
584        name: Name::str("PBEConvergence"),
585        univ_params: vec![],
586        ty: arrow(nat_ty(), arrow(list_ty(cst("IOExample")), prop())),
587    }
588}
589#[cfg(test)]
590mod tests {
591    use super::*;
592    #[test]
593    fn test_build_env() {
594        let mut env = Environment::new();
595        let result = build_program_synthesis_env(&mut env);
596        assert!(
597            result.is_ok(),
598            "build_program_synthesis_env failed: {:?}",
599            result
600        );
601    }
602    #[test]
603    fn test_spec_constraint_count() {
604        let s1 = Spec::logic("y = x * 2");
605        assert_eq!(s1.constraint_count(), 1);
606        let s2 = Spec::from_examples(vec![
607            (vec!["0".into()], "0".into()),
608            (vec!["1".into()], "2".into()),
609            (vec!["2".into()], "4".into()),
610        ]);
611        assert_eq!(s2.constraint_count(), 3);
612        let conj = Spec::Conjunction(Box::new(s1), Box::new(s2.clone()));
613        assert_eq!(conj.constraint_count(), 4);
614        let disj = Spec::Disjunction(Box::new(s2.clone()), Box::new(Spec::logic("z = 0")));
615        assert_eq!(disj.constraint_count(), 3);
616    }
617    #[test]
618    fn test_cegis_state() {
619        let spec = Spec::logic("y = x + 1");
620        let mut state = CegisState::new(spec, 10);
621        assert!(!state.is_solved());
622        assert!(!state.is_exhausted());
623        state.propose(Candidate::new("fun x -> x + 1"));
624        assert!(state.is_solved());
625        assert_eq!(state.iterations, 1);
626        state.add_counterexample(vec!["0".into()]);
627        assert!(!state.is_solved());
628        assert_eq!(state.counterexamples.len(), 1);
629    }
630    #[test]
631    fn test_cfg_productions() {
632        let mut cfg = CFG::new("E");
633        cfg.add_production("E", vec!["E".into(), "+".into(), "E".into()]);
634        cfg.add_production("E", vec!["0".into()]);
635        cfg.add_production("E", vec!["1".into()]);
636        cfg.add_terminal("0");
637        cfg.add_terminal("1");
638        cfg.add_terminal("+");
639        assert_eq!(cfg.productions_for("E").len(), 3);
640        assert_eq!(cfg.terminals.len(), 3);
641    }
642    #[test]
643    fn test_type_directed_synth_identity() {
644        let alpha = SynthType::Var("α".into());
645        let goal = SynthType::arrow(alpha.clone(), alpha.clone());
646        let ctx = SynthContext::new();
647        let mut synth = TypeDirectedSynth::new(3);
648        let result = synth.synthesise(&ctx, &goal, 0);
649        assert!(result.is_some(), "should synthesise identity: {:?}", result);
650        let prog = result.expect("result should be valid");
651        assert!(prog.contains("fun"), "should be a lambda: {}", prog);
652    }
653    #[test]
654    fn test_sketch_fill_and_complete() {
655        let holes = vec![Hole::new(0, "Nat"), Hole::new(1, "Nat")];
656        let sketch = Sketch::new("fun x -> ??0 + ??1", holes);
657        assert_eq!(sketch.num_holes(), 2);
658        assert!(!sketch.is_complete());
659        let s1 = sketch.fill_hole(0, "x");
660        assert_eq!(s1.num_holes(), 1);
661        let s2 = s1.fill_hole(1, "1");
662        assert!(s2.is_complete());
663        assert_eq!(s2.source, "fun x -> x + 1");
664    }
665    #[test]
666    fn test_flashfill_identity() {
667        let examples = vec![
668            IOExample::new(vec!["hello".into()], "hello"),
669            IOExample::new(vec!["world".into()], "world"),
670        ];
671        let synth = FlashFillSynth::new();
672        let result = synth.synthesise(&examples);
673        assert_eq!(result, Some("fun x -> x".into()));
674    }
675    #[test]
676    fn test_oracle_table_query() {
677        let mut oracle = TableOracle::new();
678        oracle.insert(vec!["0".into()], "1");
679        oracle.insert(vec!["1".into()], "2");
680        let mut loop_ = OracleSynthLoop::new();
681        let ans0 = loop_.query(&oracle, vec!["0".into()]);
682        let ans1 = loop_.query(&oracle, vec!["1".into()]);
683        let ans_miss = loop_.query(&oracle, vec!["99".into()]);
684        assert_eq!(ans0, Some("1".into()));
685        assert_eq!(ans1, Some("2".into()));
686        assert_eq!(ans_miss, None);
687        assert_eq!(loop_.num_queries(), 3);
688    }
689    #[test]
690    fn test_bottom_up_enum_size1() {
691        let synth = BottomUpSynth::new(
692            5,
693            vec!["x".into(), "y".into()],
694            vec!["0".into(), "1".into()],
695        );
696        let progs = synth.enumerate_size(1);
697        assert_eq!(progs.len(), 4);
698    }
699}
700#[cfg(test)]
701mod tests_program_synthesis_extended {
702    use super::*;
703    #[test]
704    fn test_ilp_problem_examples() {
705        let mut prob = ILPProblem::new("parent");
706        prob.add_positive("parent(tom, bob)");
707        prob.add_negative("parent(bob, ann)");
708        prob.add_background("ancestor(X, Y) :- parent(X, Y)");
709        assert_eq!(prob.total_examples(), 2);
710        assert_eq!(prob.positive_examples.len(), 1);
711    }
712    #[test]
713    fn test_foil_gain_calculation() {
714        let learner = FoilLearner::new(5, 0.1);
715        let gain = learner.foil_gain(10.0, 5.0, 5.0, 4.0, 1.0);
716        assert!(gain > 0.0);
717    }
718    #[test]
719    fn test_program_sketch_fill() {
720        let sketch = ProgramSketch::new("x + {hole_0} * y + {hole_1}", 2);
721        let filled = sketch.fill(&["2", "3"]);
722        assert_eq!(filled, "x + 2 * y + 3");
723        assert!(sketch.is_complete(&filled));
724    }
725    #[test]
726    fn test_program_sketch_space_size() {
727        let sketch = ProgramSketch::new("{hole_0} op {hole_1}", 2);
728        assert_eq!(sketch.sketch_space_size(5), 25);
729    }
730    #[test]
731    fn test_ogis_cegis_convergence() {
732        let mut synth = OGISSynthesizer::new(10);
733        synth.add_counter_example(vec![1, 2], 3);
734        synth.add_counter_example(vec![2, 3], 5);
735        assert_eq!(synth.cegis_iterations(), 2);
736        assert!(!synth.has_converged());
737        for i in 0..8 {
738            synth.add_counter_example(vec![i], i * 2);
739        }
740        assert!(synth.has_converged());
741    }
742    #[test]
743    fn test_foil_covering_clauses() {
744        let learner = FoilLearner::new(10, 0.1);
745        let clauses = learner.covering_clauses_needed(100);
746        assert!(clauses <= 10);
747    }
748}
oxilean_std/program_synthesis/functions.rs

oxilean_std/program_synthesis/
functions.rs
