Struct PBEProblem

pub struct PBEProblem {
    pub logic: String,
    pub synthfuns: Vec<SynthFun>,
    pub problem_index: usize,
    pub examples: IOExamples,
}

A struct representing a synthesis problem to be solved. This structure contains four fields: logic, a string specifying the logic or domain in which the synthesis problem is defined; synthfuns, a vector of SynthFun instances representing the functions to be synthesized as part of solving the problem; problem_index, a usize value denoting the particular index or identifier of this problem within a broader set of problems; and examples, an IOExamples instance that holds input-output exemplars relevant to the synthesis task, to ground the problem solution in practical demonstrations of expected behavior.

Fields

logic: String

synthfuns: Vec<SynthFun>

problem_index: usize

examples: IOExamples

Implementations

impl PBEProblem

pub fn synthfun(&self) -> &SynthFun

Provides access to a specific SynthFun based on the current problem_index.

This function retrieves a reference to the SynthFun within the synthfuns vector of the PBEProblem instance. The problem_index specifies which SynthFun to access, allowing direct retrieval of the active synthesis function’s details, such as its signature and configuration, from the list of available functions.

pub fn parse(input: &str) -> Result<PBEProblem, Error>

Parses a string input to create an instance of PBEProblem.

This method uses the ProblemParser to initially parse the input string according to predefined grammar rules, extracting relevant components for logic, synthesis functions, examples, and checks. It specifically targets obtaining the logic definition, synthesizing problem configurations, and IO examples used in problem-solving. The method processes these components to extract the inner details of logic and synthesis, where synthesis functions are parsed individually. A verification step ensures that only one main synthesis function (synth-fun) is designated as the primary problem by filtering out those marked as subproblems. The synthesis examples are parsed to ensure they match the signature of the main synthesis function. It constructs and returns a PBEProblem comprising the logic, a vector of synthesis functions, the index of the main problem, and the parsed examples. The method will fail if the input does not conform to expected structures or logic, returning an error.

Trait Implementations

impl Debug for PBEProblem

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.