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 SyGuS Language Standard Version 2.0
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
;; Declare the non-terminals that would be used in the grammar
((I Int) (B Bool))
;; Define the grammar for allowed implementations of max2
((I Int (x y 0 1
(+ I I) (- I I)
(ite B I I)))
(B Bool ((and B B) (or B B) (not B)
(= I I) (<= I I) (>= I I))))
)
(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)
Our initial proposal for SyGuS-IF (ver. 1.0) and its extensions can be found here. However, this original proposal is now deprecated. We revised our input format in 2019 and proposed SyGuS-IF ver. 2.0, which is more compliant with SMT-LIB version 2.6, includes minor changes to the concrete syntax for commands, and eliminates several deprecated features of the previous format.