Synthesizers

synthesizer

template <typename Encoder, typename Solver>

class percy::synthesizer

The synthesizer base class. All synthesizers have some Encoder and some Solver, which they compose to perform synthesis.

Subclassed by percy::dag_synthesizer< FI, Encoder, Solver >, percy::fence_synthesizer< FI, Encoder, Solver >, percy::floating_dag_synthesizer< FI, Encoder, Solver >, percy::std_synthesizer< FI, Encoder, Solver >

std_synthesizer

template <int FI = 2, typename Encoder = knuth_encoder<FI>, typename Solver = sat_solver*>

class percy::std_synthesizer

Standard synthesizer class that uses conventional SAT based synthesis techniques.

Inherits from percy::synthesizer< Encoder, Solver >

Public Functions

template <typename TT>

synth_result percy::std_synthesizersynthesize(synth_spec<TT> &spec, chain<FI> &chain, const int initial_steps = 1)

Performs exact synthesis using a standard synthesis loop. Given the specifcation spec it stores the result of synthesis in chain. Using initial_steps we can give a specify the initial number of steps to start synthesis from. Note that this may lead to suboptimal results.

template <typename TT>

synth_result percy::std_synthesizercegar_synthesize(synth_spec<TT> &spec, chain<FI> &chain, const int initial_steps = 1)

Performs synthesis using a CEGAR loop.

template <typename TT>

synth_result percy::std_synthesizernext_solution(synth_spec<TT> &spec, chain<FI> &chain, const int initial_steps = 1)

Generates the next solution. This can be used in a loop to enumerate different solutions to a specification.

template <typename TT>

synth_result percy::std_synthesizernext_struct_solution(synth_spec<TT> &spec, chain<FI> &chain)

Generates the next structurally different solution, where structure refers to the underlying DAG structure of a solution. This method can be used in a loop to enumerate structurally different solutions to a specification.

void percy::std_synthesizerreset()

Resets synthesizer state. Used in generating multiple solutions.

fence_synthesizer

template <int FI = 2, typename Encoder = fence_encoder<FI>, typename Solver = sat_solver*>

class percy::fence_synthesizer

Inherits from percy::synthesizer< Encoder, Solver >

Public Functions

template <typename TT>

synth_result percy::fence_synthesizersynthesize(synth_spec<TT> &spec, chain<FI> &chain, const int initial_steps = 1)

template <typename TT>

synth_result percy::fence_synthesizersynthesize(synth_spec<TT> &spec, const fence &f, chain<FI> &chain)

template <typename TT>

synth_result percy::fence_synthesizercegar_synthesize(synth_spec<TT> &spec, chain<FI> &chain, const int initial_steps = 1)

template <typename TT>

synth_result percy::fence_synthesizercegar_synthesize(synth_spec<TT> &spec, const fence &f, chain<FI> &chain)

dag_synthesizer

template <int FI = 2, typename Encoder = dag_encoder<dag<FI>>, typename Solver = sat_solver*>

class percy::dag_synthesizer

Inherits from percy::synthesizer< Encoder, Solver >

Public Functions

template <typename TT>

synth_result percy::dag_synthesizersynthesize(synth_spec<TT> &spec, const dag<FI> &dag, chain<FI> &chain, bool preprocess_spec = true)