Synthesis Basics

UCLID5 supports a full integratation of Syntax-Guided Synthesis(SyGuS) across all verification modes. Given any UCLID5 model containing a synthesis function and a verification command and an external SyGuS solver such as CVC5, UCLID5 will generate a SyGuS problem that aims to find a body for the synthesis function such that the UCLID5 model passes verification.

Synthesis Functions

Synthesis functions are identified by the keyword phrase synthesis function: they have a list of input types and an output type, similar to uninterpreted functions. Synthesis functions can be declared function declaration. These functions are typed, mapping a tuple of typed arguments to a return type.

	synthesis function <function_name>(<input_type_list>) : <output_type>;

For example, the following synthesis function models the mapping of an instrution to an opcode.

	synthesis function inst2op(i : word_t) : op_t;

Synthesis functions can be used throughout uclid code in exactly the same way as uninterpreted functions. The SyGuS problem generated by UCLID5 will try to find bodies for all synthesis functions in the UCLID5 model.

Invoking a SyGuS solver

To solve a synthesis problem with UCLID5, UCLID5 should be called with the command line argument -s /path/to/sygus/solver. This will trigger UCLID5 to generate a synthesis problem instead of a verification problem.

Example Synthesis Problem

The following example uses a synthesis function to strengthen the invariant hole, such that the invariant passes verification by induction.

module main {
  // Part 1: System Description .
  var a , b : integer;

  init {
    a , b = 0 , 1;
  }
  next {
    a ' , b ' = b , a + b ;
  }

  // Part 2: System Specification .
  invariant a_le_b : a <= b;

  // Part 3: Synthesis Integration
  synthesis function h (x : integer , y : integer ) : boolean ;
  invariant hole : h(a , b ) ;

  // Part 4: Proof Script .
  control {
    induction ;
    check ;
    print_results ;
  }
}