# Specification Language (Deprecated)

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. 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 max2 that computes the maximum of two variables x and y.

;; The background theory is linear integer arithmetic
(set-logic LIA)

;; Name and signature of the function to be synthesized
(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)


### Extensions

Over the years, several extensions to the original SyGuS-IF have been proposed for aiding specific synthesis scenarios.

• In 2015, we proposed the CLIA and INV extensions: SyGuS-IF 2015
• In 2016, we proposed the PBE extension: 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!