Module functions 

Auto-generated module

🤖 Generated with SplitRS

Traits

Oracle

An oracle that can answer membership queries about the target function.

Functions

add_axiom

app

app2

app3

axiom_abstraction_refinement_correct_ty

Abstraction-based synthesis: abstraction refinement correctness.

axiom_astar_synth_admissible_ty

Program synthesis by A* search: admissible heuristic correctness.

axiom_behavioral_cloning_correct_ty

Learning from demonstrations: behavioral cloning correctness.

axiom_cegis_bounded_depth_ty

CEGIS with bounded counterexample depth.

axiom_cegis_convergence_rate_ty

CEGIS acceleration: convergence rate under a strong verifier.

axiom_church_synthesis_ty

Synthesis from specifications: Church’s synthesis problem.

axiom_constraint_encoding_correct_ty

Constraint-based synthesis: SAT encoding correctness.

axiom_execution_guided_consistency_ty

Execution-guided synthesis: observable semantics consistency.

axiom_execution_trace_complete_ty

Execution-guided synthesis: trace completeness.

axiom_finite_domain_decidable_ty

Constraint-based synthesis: finite domain decidability.

axiom_flashfill_unique_threshold_ty

FlashFill generalization: number of examples sufficient for uniqueness.

axiom_flashmeta_vsa_ty

FlashMeta: DSL synthesis via version space algebra.

axiom_inductive_completeness_ty

Inductive program synthesis: completeness over a finite hypothesis space.

axiom_inductive_generalization_ty

Inductive program synthesis: soundness of inductive generalization.

axiom_irl_soundness_ty

Learning from demonstrations: inverse reinforcement learning soundness.

axiom_liquid_type_soundness_ty

Refinement type synthesis: soundness of liquid type inference.

axiom_loop_invariant_correct_ty

Loop invariant synthesis: inductive invariant correctness.

axiom_lstar_query_complexity_ty

Oracle-guided synthesis: Angluin’s L* query complexity bound.

axiom_mdl_synthesis_ty

Minimal description length principle for inductive synthesis.

axiom_mw_resolution_correct_ty

Manna–Waldinger deductive synthesis: resolution correctness.

axiom_mw_termination_ty

Manna–Waldinger synthesis: goal reduction termination.

axiom_neural_synth_generalisation_ty

Neural program synthesis: generalisation bound (PAC-style).

axiom_neural_synth_soundness_ty

Neural program synthesis: soundness of learned synthesiser.

axiom_oracle_equivalence_query_ty

Oracle-guided synthesis with equivalence queries.

axiom_oracle_membership_query_ty

Oracle-guided synthesis with membership queries only.

axiom_refinement_subtype_complete_ty

Refinement type synthesis: completeness for subtyping.

axiom_refinement_type_decidable_ty

Type-driven synthesis: refinement type checking decidability.

axiom_sketch_hole_smt_ty

Sketch framework: hole satisfiability modulo theory.

axiom_sketch_relative_complete_ty

Synthesis with sketches: relative completeness wrt sketch language.

axiom_spec_realizability_ty

Synthesis from logical specifications: realizability.

axiom_spurious_cex_detection_ty

Abstraction-based synthesis: spurious counterexample detection.

axiom_stochastic_synth_soundness_ty

Stochastic program synthesis: probabilistic soundness.

axiom_strongest_invariant_exists_ty

Loop invariant synthesis: strongest inductive invariant existence.

axiom_superopt_equivalence_ty

Superoptimisation: equivalence preservation.

axiom_superopt_optimal_ty

Superoptimisation: optimality of synthesised loop-free program.

axiom_sygus_multi_function_ty

SyGuS multi-function: soundness when synthesising several functions jointly.

axiom_sygus_separability_ty

SyGuS separability: two grammars produce disjoint solution sets.

bool_ty

build_program_synthesis_env

Build the kernel environment with program synthesis axioms.

build_program_synthesis_env_ext

Build the extended program synthesis environment (new axioms).

bvar

cst

decl_cegis_complete

Build the CegisComplete axiom declaration.

decl_djinn_complete

Build the DjinnComplete axiom declaration.

decl_pbe_convergence

Build the PBEConvergence axiom declaration.

decl_spec_satisfied

Build a single SpecSatisfied axiom declaration.

decl_sygus_soundness

Build the SyGuSSoundness axiom declaration.

list_ty

nat_ty

option_ty

pair_ty

pi

prop

string_ty

type0