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!