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

oxilean_std/program_synthesis/
functions.rs
