Editing Program synthesis (section)

=== Syntax-guided synthesis ===

In 2013, a unified framework for program synthesis problems called Syntax-guided Synthesis (stylized SyGuS) was proposed by researchers at [[UPenn]], [[UC Berkeley]], and [[MIT]].<ref>{{cite conference |title =Syntax-guided Synthesis |last1 = Alur |first1 = Rajeev| last2 = al.| first2 = et| date = 2013| publisher = IEEE| book-title = Proceedings of Formal Methods in Computer-Aided Design| pages = 8}}</ref> The input to a SyGuS algorithm consists of a logical specification along with a [[context-free grammar]] of expressions that constrains the syntax of valid solutions.<ref>{{harv|David|Kroening}}</ref> For example, to synthesize a function {{var|f}} that returns the maximum of two integers, the logical specification might look like this:

{{math|(''f''(''x'',''y'') {{=}} ''x'' ∨ ''f''(''x'',''y'') {{=}} ''y'') ∧ ''f''(''x'',''y'') ≥ x ∧ ''f''(''x'',''y'') ≥ y}}

and the grammar might be:

<syntaxhighlight lang="bnf">
<Exp> ::= x | y | 0 | 1 | <Exp> + <Exp> | ite(<Cond>, <Exp>, <Exp>)
<Cond> ::= <Exp> <= <Exp>
</syntaxhighlight>

where "ite" stands for "if-then-else". The expression

 ite(x <= y, y, x)

would be a valid solution, because it conforms to the grammar and the specification.

From 2014 through 2019, the yearly Syntax-Guided Synthesis Competition (or SyGuS-Comp) compared the different algorithms for program synthesis in a competitive event.<ref>[https://sygus-org.github.io/comp/ SyGuS-Comp (Syntax-Guided Synthesis Competition)]</ref> The competition used a standardized input format, SyGuS-IF, based on [[SMT-LIB|SMT-Lib 2]]. For example, the following SyGuS-IF encodes the problem of synthesizing the maximum of two integers (as presented above):

 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
   ((i Int) (c Int) (b Bool))
   ((i Int (c x y (+ i i) (ite b i i)))
    (c Int (0 1))
    (b Bool ((<= i i)))))
 (declare-var x Int)
 (declare-var y Int)
 (constraint (>= (f x y) x))
 (constraint (>= (f x y) y))
 (constraint (or (= (f x y) x) (= (f x y) y)))
 (check-synth)

A compliant solver might return the following output:

 ((define-fun f ((x Int) (y Int)) Int (ite (<= x y) y x)))