Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Bottom
UpSynth - A bottom-up enumerative synthesiser for functional programs.
- CFG
- A context-free grammar used as a syntax guide for synthesis.
- Candidate
- A candidate program in CEGIS, represented as a string expression.
- Cegis
State - The CEGIS synthesis loop state.
- Component
- A library component with pre/post-conditions.
- Component
Library - A component library used in component-based synthesis.
- Component
Synth Query - A component-based synthesis query.
- Constraint
Synth Engine - A constraint-based synthesis engine that encodes the problem as SMT.
- Deductive
Rule - A rule in a deductive synthesis calculus.
- Derivation
Node - A deductive synthesis derivation tree node.
- Enumerative
Solver - An enumerative SyGuS solver that exhaustively searches the grammar.
- Flash
Fill Synth - The FlashFill-style synthesis algorithm for string transformations.
- Foil
Learner - FOIL (First Order Inductive Learner) algorithm scaffolding.
- Hole
- A hole in a program sketch, parameterised by expected type.
- Houdini
Invariant Synth - An inductive loop invariant synthesiser using Houdini-style fixpoint.
- ILPProblem
- Represents a learning problem in Inductive Logic Programming. ILP learns logic programs (Horn clauses) from examples and background knowledge.
- IOExample
- An input/output example for programming by example.
- MWSynth
Goal - A Manna–Waldinger synthesis goal: (precondition, postcondition, output variable).
- OGIS
Synthesizer - Oracle-guided inductive synthesis (OGIS): uses a teacher oracle.
- Oracle
Synth Loop - Oracle-guided synthesis loop.
- Production
- A production rule in a context-free grammar.
- Program
Sketch - A program sketch: a program template with “holes” to be filled.
- Refinement
Type - A refinement type used in liquid type synthesis.
- Sketch
- A program sketch: a partial program with holes to fill.
- Sketch
Solver - A sketch-based synthesiser that fills holes using constraint solving.
- Superoptimiser
- A superoptimiser that searches for the shortest equivalent program.
- SyGuS
Problem - A SyGuS problem instance.
- Synth
Context - A type-directed synthesis context: typed components available.
- Table
Oracle - A finite-table oracle backed by a lookup table.
- Type
Directed Synth - Type-directed synthesiser: Djinn/Agsy-style proof search.
- Version
Space - A version space: the set of programs consistent with all examples seen.
Enums§
- Func
Program - A recursive program structure for inductive synthesis.
- Func
Template - A higher-order program template for functional synthesis.
- Spec
- A logical specification for a synthesis problem.
- SyGuS
Result - A SyGuS solver result.
- Synth
Type - A simple type language for type-directed synthesis.
- Verifier
Result - The result of a CEGIS verification query.