We propose a standard language for specifying syntax-guided synthesis (SyGuS) problems. The SyGuS input format (SyGuS-IF) is closely modeled on SMT-Lib 2.0. The original proposal for SyGuS-IF can be found here. This is the specification language used by the SyGuS benchmarks in the General track of the SyGuS-Comp.
Here is an example SyGuS problem for a function named
that computes the maximum of two variables
;; The background theory is linear integer arithmetic (set-logic LIA) ;; Name and signature of the function to be synthesize (synth-fun max2 ((x Int) (y Int)) Int) ;; Define the grammar for allowed implementations of max2 ((Start Int (x y 0 1 (+ Start Start) (- Start Start) (ite StartBool Start Start))) (StartBool Bool ((and StartBool StartBool) (or StartBool StartBool) (not StartBool) (<= Start Start) (= Start Start) (>= Start Start)))) (declare-var x Int) (declare-var y Int) ;; Define the semantic constraints on the function (constraint (>= (max2 x y) x)) (constraint (>= (max2 x y) y)) (constraint (or (= x (max2 x y)) (= y (max2 x y)))) (check-synth)
Over the years, several extensions to the original SyGuS-IF have been proposed for aiding specific synthesis scenarios.
- In 2015, we proposed the
INVextensions: SyGuS-IF 2015
- In 2016, we proposed the
PBEextension: SyGuS-IF 2016
UPDATE: We are currently in the process of drafting SyGuS-IF 2.0 which in addition to addressing several issues with the original SyGuS-IF, also consolidates these extensions. Stay tuned!