Encoders

knuth_encoder

The knuth_encoder class is based on the exact synthesis formulation developed by That implementation is itself based on earlier work by Éen [1] and Knuth [2].

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

class percy::knuth_encoder

Public Functions

template <typename TT>

void percy::knuth_encoderextract_chain(synth_spec<TT> &spec, chain<FI> &chain)

Extracts chain from encoded CNF solution.

template <typename TT>

bool percy::knuth_encoderencode(const synth_spec<TT> &spec)

Encodes specifciation for use in standard synthesis flow.

template <typename TT>

bool percy::knuth_encodercegar_encode(const synth_spec<TT> &spec)

Encodes specifciation for use in CEGAR based synthesis flow.

template <typename TT>

bool percy::knuth_encoderblock_solution(const synth_spec<TT> &spec)

Assumes that a solution has been found by the current encoding. Blocks the current solution such that the solver is forced to find different ones (if they exist).

template <typename TT>

bool percy::knuth_encoderblock_struct_solution(const synth_spec<TT> &spec)

Similar to block_solution, but blocks all solutions with the same structure. This is more restrictive, since the other method allows for the same structure but different operators.

fence_encoder

The fence_encoder is intended to be used by a synthesizer that generates families of DAG topologies, also known as fences.

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

class percy::fence_encoder

Public Functions

template <typename TT>

void percy::fence_encoderextract_chain(synth_spec<TT> &spec, chain<FI> &chain)

Extracts chain from encoded CNF solution.

template <typename TT>

bool percy::fence_encoderencode(const synth_spec<TT> &spec, const fence &f)

Encodes specifciation for use in standard synthesis flow.

template <typename TT>

bool percy::fence_encodercegar_encode(const synth_spec<TT> &spec, const fence &f)

Encodes specifciation for use in CEGAR based synthesis flow.

template <typename TT>

bool percy::fence_encoderblock_solution(const synth_spec<TT> &spec)

Assumes that a solution has been found by the current encoding. Blocks the current solution such that the solver is forced to find different ones (if they exist).

template <typename TT>

bool percy::fence_encoderblock_struct_solution(const synth_spec<TT> &spec)

Similar to block_solution, but blocks all solutions with the same structure. This is more restrictive, since the other method allows for the same structure but different operators.

dag_encoder

The fence_encoder is intended to be used by a synthesizer that generates DAGs. Encoding DAGs requires much fewer variables, since their structure is completely fixed.

template <typename Dag, typename Solver = sat_solver*>

class percy::dag_encoder

Public Functions

template <typename TT>

bool percy::dag_encoderencode(const synth_spec<TT> &spec, const Dag &dag)

Encodes specifciation for use in standard synthesis flow.

template <typename TT>

bool percy::dag_encodercegar_encode(const synth_spec<TT> &spec, const Dag &dag)

Encodes specifciation for use in CEGAR based synthesis flow.

template <typename TT>

void percy::dag_encoderextract_chain(const synth_spec<TT> &spec, const Dag &dag, chain<Dag::NrFanin> &chain)

Extracts chain from encoded CNF solution.

void percy::dag_encoderblock_solution()

Assumes that a solution was found by the synthesizer. In that case, we can block the current solution by blocking the current assignment to the operator variables.

[1]	Niklas Éen, “Practical SAT – a tutorial on applied satisfiability solving,” 2007, slides of invited talk at FMCAD.

[2]	Donald Ervin Knuth, “The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability,” 2015