Crate liblisa_synth

This library contains the default synthesis implementation for libLISA. It can be invoked as follows (for x64):

// let encoding = ...; // see the `liblisa-enc` crate
let semantics = liblisa_x64_observer::with_oracle(|mut oracle| {
    liblisa_synth::synthesize_semantics(encoding, &mut oracle)
});

println!("{semantics}");

Structs

Output

A synthesis output. Corresponds to a dataflow output in an Encoding.

SynthesisLoop

A CEGIS synthesis loop.

SynthesisResult

The result of synthesis.

Traits

Requester

A type that returns the output of a dataflow, given its inputs.

Synthesizer

A semantics synthesizer. Generic over input and output types.

SynthesizerBase

A semantics synthesizer.

SynthesizerOutput

The output values used for synthesis. These are usually Values or OwnedValues.

Functions

determine_overlapping_write_order

Determines the WriteOrderings for an Encoding’s outputs.

merge_semantics_into_encoding

Merges the SynthesisResults returned by the SynthesisLoop into an Encoding.

prepare_templates

Prepares the templates needed for synthesis. If this function is not called, templates are prepared the first time synthesis is run. This may cause the first synthesis attempt to time out.

synthesize_from_fn

A simple synthesizer that synthesizes a computation from a function.

synthesize_outputs

Synthesizes semantics for all outputs in the provided Encoding.

synthesize_semantics

Synthesizes semantics for an Encoding.

Type Aliases

DefaultTreeTemplateSynthesizer

The default synthesizer, using templates and decision trees.