Specifications

In percy we use specification objects to tell synthesizers both what and how to synthesize. Specifications are implemented by the synth_spec class, which can be found under <percy/spec.hpp>. We can specify the functions to synthesize, but we also control some optional parameters such as conflict limits, and various symmetry breaking flags. Symmetry breaking is used to rule out certain “symmetric” solutions. Often we’re not interested a solution if it is symmetric to one we have already found. [1] Ruling out such solutions makes the search space smaller and thus speeds up synthesis. Note that the symmetry breaking flags should be interpreted as hints and not as law: they may not be implemented in all synthesizers. In fact, depending on the implementation, not all flags may apply to some synthesizers’ synthesis process.

Note that synth_spec takes a template parameter. This parameter specifies the type of functions to synthesize (i.e. static or dynamic kitty truth tables).

template <typename TT>

class percy::synth_spec

Public Functions

percy::synth_specsynth_spec()

Default constructor leaves default settings untouched.

percy::synth_specsynth_spec(int nr_in, int nr_out)

Construct a spec with nr_in inputs and nr_out outputs.

void percy::synth_specset_nr_in(const int n)

void percy::synth_specset_nr_out(const int n)

int percy::synth_specget_nr_in() const

int percy::synth_specget_tt_size() const

int percy::synth_specget_nr_out() const

void percy::synth_specpreprocess(void)

Normalizes outputs by converting them to normal functions. Also checks for trivial outputs, such as constant functions or projections. This determines which of the specifeid functions need to be synthesized. This function expects the following invariants to hold:

1. The number of input variables has been set.
2. The number of output variables has been set.
3. The functions requested to be synthesized have been set.

Public Members

int percy::synth_specnr_steps

The number of Boolean operators to use.

int percy::synth_specverbosity = 0

Verbosity level for debugging purposes.

uint64_t percy::synth_specout_inv

Is 1 at index i if output i must be inverted.

uint64_t percy::synth_spectriv_flag

Is 1 at index i if output i is constant zero or one or a projection.

int percy::synth_specnr_triv

Number of trivial output functions.

int percy::synth_specnr_nontriv

Number of non-trivial output functions.

int percy::synth_specnr_rand_tt_assigns

Number of truth table bits to assign randomly in CEGAR loop.

bool percy::synth_specadd_nontriv_clauses = true

Symmetry break: do not allow trivial operators.

bool percy::synth_specadd_alonce_clauses = true

Symmetry break: all steps must be used at least once.

bool percy::synth_specadd_noreapply_clauses = true

Symmetry break: no re-application of operators.

bool percy::synth_specadd_colex_clauses = true

Symmetry break: order step fanins co-lexicographically.

bool percy::synth_specadd_lex_func_clauses = true

Symmetry break: order step operators co-lexicographically.

bool percy::synth_specadd_symvar_clauses = true

Symmetry break: impose order on symmetric variables.

bool percy::synth_specadd_lex_clauses = false

Symmetry break: order step fanins lexicographically.

template<>
const TT *percy::synth_spec<TT>functions[MAX_OUT]

The functions to synthesize.

template<>
int percy::synth_spec<TT>triv_functions[MAX_OUT]

Trivial outputs.

template<>
int percy::synth_spec<TT>synth_functions[MAX_OUT]

Nontrivial outputs.

int64_t percy::synth_specsynth_time

A place for synthesizers to log elapsed synthesis time. Measured in microseconds.

int percy::synth_specconflict_limit = 0

Limit on the number of SAT conflicts. Zero means no limit.

Private Members

int percy::synth_specnr_in

The number of inputs to the function.

int percy::synth_spectt_size

The size of the truth table.

int percy::synth_specnr_out

The number of outputs to synthesize.

[1]	An example would be a solution in which we simply swap two inputs.