Proving Unrealizability for SyntaxGuided Synthesis
Abstract
We consider the problem of automatically establishing that a given syntaxguidedsynthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encoding the synthesis problem’s grammar G as a nondeterministic program \(P_G\), we reduce the unrealizability problem to a reachability problem such that, if a standard programanalysis tool can establish that a certain assertion in \(P_G\) always holds, then the synthesis problem is unrealizable.
Our method can be used to augment existing SyGuS tools so that they can establish that a successfully synthesized program q is optimal with respect to some syntactic cost—e.g., q has the fewest possible ifthenelse operators. Using known techniques, grammar G can be transformed to generate the set of all programs with lower costs than q—e.g., fewer conditional expressions. Our algorithm can then be applied to show that the resulting synthesis problem is unrealizable. We implemented the proposed technique in a tool called nope. nope can prove unrealizability for 59/132 variants of existing linearintegerarithmetic SyGuS benchmarks, whereas all existing SyGuS solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.
1 Introduction
The goal of program synthesis is to find a program in some search space that meets a specification—e.g., satisfies a set of examples or a logical formula. Recently, a large family of synthesis problems has been unified into a framework called syntaxguided synthesis (SyGuS). A SyGuS problem is specified by a regulartree grammar that describes the search space of programs, and a logical formula that constitutes the behavioral specification. Many synthesizers now support a specific format for SyGuS problems [1], and compete in annual synthesis competitions [2]. Thanks to these competitions, these solvers are now quite mature and are finding a wealth of applications [9].
A key property of the previous example is that the grammar is infinite. When such a SyGuS problem is realizable, any search technique that systematically explores the infinite search space of possible programs will eventually identify a solution to the synthesis problem. In contrast, proving that a problem is unrealizable requires showing that every program in the infinite search space fails to satisfy the specification. This problem is in general undecidable [6]. Although we cannot hope to have an algorithm for establishing unrealizability, the challenge is to find a technique that succeeds for the kinds of problems encountered in practice. Existing synthesizers can detect the absence of a solution in certain cases (e.g., because the grammar is finite, or is infinite but only generate a finite number of functionally distinct programs). However, in practice, as our experiments show, this ability is limited—no existing solver was able to show unrealizability for any of the examples considered in this paper.
In this paper, we present a technique for proving that a possibly infinite SyGuS problem is unrealizable. Our technique builds on two ideas.
 1.
We observe that unrealizability can often be proven using finitely many input examples. In Sect. 2, we show how the example discussed above can be proven to be unrealizable using four input examples—(0, 0), (0, 1), (1, 0), and (1, 1).
 2.
We devise a way to encode a SyGuS problem \((\psi (f,\bar{x}), G)\) over a finite set of examples E as a reachability problem in a recursive program \(P[{G},{E}]\). In particular, the program that we construct has an assertion that holds if and only if the given SyGuS problem is unrealizable. Consequently, unrealizability can be proven by establishing that the assertion always holds. This property can often be established by a conventional programanalysis tool.
The encoding mentioned in item 2 is nontrivial for three reasons. The following list explains each issue, and sketches how they are addressed
(1) Infinitely many terms. We need to model the infinitely many terms generated by the grammar of a given synthesis problem \((\psi (f,\bar{x}), G)\).
To address this issue, we use nondeterminism and recursion, and give an encoding \(P[{G},{E}]\) such that (i) each nondeterministic path p in the program \(P[{G},{E}]\) corresponds to a possible expression \(e_p\) that G can generate, and (ii) for each expression e that G can generate, there is a path \(p_e\) in \(P[{G},{E}]\). (There is an isomorphism between paths and the expressiontrees of G)
(2) Nondeterminism. We need the computation performed along each path p in \(P[{G},{E}]\) to mimic the execution of expression \(e_p\). Because the program uses nondeterminism, we need to make sure that, for a given path p in the program \(P[{G},{E}]\), computational steps are carried out that mimic the evaluation of \(e_p\) for each of the finitely many example inputs in E.
We address this issue by threading the expressionevaluation computations associated with each example in E through the same nondeterministic choices.
(3) Complex Specifications. We need to handle specifications that allow for nested calls of the programs being synthesized.
For instance, consider the specification \(f(f(x)) = x\). To handle this specification, we introduce a new variable y and rewrite the specification as \(f(x) = y \wedge f(y) = x\). Because y is now also used as an input to f, we will thread both the computations of x and y through the nondeterministic recursive program.

We reduce the SyGuS unrealizability problem to a reachability problem to which standard programanalysis tools can be applied (Sects. 2 and 4).

We observe that, for many SyGuS problems, unrealizability can be proven using finitely many input examples, and use this idea to apply the CounterExampleGuided Inductive Synthesis (CEGIS) algorithm to the problem of proving unrealizability (Sect. 3).

We give an encoding of a SyGuS problem \((\psi (f,\bar{x}), G)\) over a finite set of examples E as a reachability problem in a nondeterministic recursive program \(P[{G},{E}]\), which has the following property: if a certain assertion in \(P[{G},{E}]\) always holds, then the synthesis problem is unrealizable (Sect. 4).

We implement our technique in a tool nope using the ESolver synthesizer [2] as the SyGuS solver and the SeaHorn tool [8] for checking reachability. nope is able to establish unrealizability for 59 out of 132 variants of benchmarks taken from the SyGuS competition. In particular, nope solves all benchmarks with no more than 15 productions in the grammar and requiring no more than 9 input examples for proving unrealizability. Existing SyGuS solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.
Section 6 discusses related work. Some additional technical material, proofs, and full experimental results are given in [13].
2 Illustrative Example
In this section, we illustrate the main components of our framework for establishing the unrealizability of a SyGuS problem.
Our method can be seen as a variant of CounterExampleGuided Inductive Synthesis (CEGIS), in which the goal is to create a program P in which a certain assertion always holds. Until such a program is created, each round of the algorithm returns a counterexample, from which we extract an additional input example for the original SyGuS problem. On the \(i^{\text {th}}\) round, the current set of input examples \(E_i\) is used, together with the grammar—in this case \(G_2\)—and the specification of the desired behavior—\(\psi _{\texttt {max2}}(f,x,y)\), to create a candidate program \(P[{G_2},{E_i}]\). The program \(P[{G_2},{E_i}]\) contains an assertion, and a standard program analyzer is used to check whether the assertion always holds.
Note that with path (1), when control returns to main, variable I_0 has the value 1, and thus the assertion at line (23) fails.
A sound program analyzer will discover that some such path exists in the program, and will return the sequence of nondeterministic choices required to follow one such path. Suppose that the analyzer chooses to report path (1); the sequence of choices would be t, f, t, f, f, f, t, which can be decoded to create the expressiontree Plus(x,1). At this point, we have a candidate definition for f: \(f = x + 1\). This formula can be checked using an SMT solver to see whether it satisfies the behavioral specification \(\psi _{\texttt {max2}}(f,x,y)\). In this case, the SMT solver returns “false.” One counterexample that it could return is (0, 0).
At this point, program \(P[{G_2},{E_2}]\) would be constructed using both of the example inputs (0, 1) and (0, 0). Rather than describe \(P[{G_2},{E_2}]\), we will describe the final program constructed, \(P[{G_2},{E_4}]\) (see Fig. 2).
As can be seen from the comments in the two programs, program \(P[{G_2},{E_4}]\) has the same basic structure as \(P[{G_2},{E_1}]\).

main begins with initialization statements for the four example inputs.

Start has five cases that correspond to the five productions of \(G_2\).
The main difference is that because the encoding of \(G_2\) in Start uses nondeterminism, we need to make sure that along each path p in \(P[{G_2},{E_4}]\), each of the example inputs is used to evaluate the same expressiontree. We address this issue by threading the expressionevaluation computations associated with each of the example inputs through the same nondeterministic choices. That is, each of the five “production cases” in Start has four encodings of the production’s semantics—one for each of the four expression evaluations. By this means, the statements that are executed along path p perform four simultaneous bottomup evaluations of the expressiontree from \(G_2\) that corresponds to p.
Programs \(P[{G_2},{E_2}]\) and \(P[{G_2},{E_3}]\) are similar to \(P[{G_2},{E_4}]\), but their paths carry out two and three simultaneous bottomup evaluations, respectively. The actions taken during rounds 2 and 3 to generate a new counterexample—and hence a new example input—are similar to what was described for round 1. On round 4, however, the program analyzer will determine that the assertion on lines (34)–(35) always holds, which means that there is no path through \(P[{G_2},{E_4}]\) for which the behavioral specification holds for all of the input examples. This property means that there is no expressiontree that satisfies the specification—i.e., the SyGuS problem \((\psi _{\texttt {max2}}(f,x,y), G_2)\) is unrealizable.
Our implementation uses the programanalysis tool SeaHorn [8] as the assertion checker. In the case of \(P[{G_2},{E_4}]\), SeaHorn takes only 0.5 s to establish that the assertion in \(P[{G_2},{E_4}]\) always holds.
3 SyGuS, Realizability, and CEGIS
3.1 Background
Trees and Tree Grammars. A ranked alphabet is a tuple \((\varSigma ,rk_\varSigma )\) where \(\varSigma \) is a finite set of symbols and \(rk_\varSigma :\varSigma \rightarrow \mathbb {N}\) associates a rank to each symbol. For every \(m\ge 0\), the set of all symbols in \(\varSigma \) with rank m is denoted by \(\varSigma ^{(m)}\). In our examples, a ranked alphabet is specified by showing the set \(\varSigma \) and attaching the respective rank to every symbol as a superscript—e.g., \(\varSigma =\{+^{(2)},c^{(0)}\}\). (For brevity, the superscript is sometimes omitted). We use \(T_\varSigma \) to denote the set of all (ranked) trees over \(\varSigma \)—i.e., \(T_\varSigma \) is the smallest set such that (i) \(\varSigma ^{(0)} \subseteq T_\varSigma \), (ii) if \(\sigma ^{(k)} \in \varSigma ^{(k)}\) and \(t_1,\ldots ,t_k\in T_\varSigma \), then \(\sigma ^{(k)}(t_1,\cdots ,t_k)\in T_\varSigma \). In what follows, we assume a fixed ranked alphabet \((\varSigma ,rk_\varSigma )\).
In this paper, we focus on typed regular tree grammars, in which each nonterminal and each symbol is associated with a type. There is a finite set of types \(\{ \tau _1, \ldots , \tau _k \}\). Associated with each symbol \(\sigma ^{(i)} \in \varSigma ^{(i)}\), there is a type assignment \(a_{\sigma ^{(i)}} = (\tau _0, \tau _1, \ldots , \tau _i)\), where \(\tau _0\) is called the lefthandside type and \(\tau _1, \ldots , \tau _i\) are called the righthandside types. Tree grammars are similar to word grammars, but generate trees over a ranked alphabet instead of words.
Definition 1
(Regular Tree Grammar). A typed regular tree grammar (RTG) is a tuple \(G=(N,\varSigma ,S,a,\delta )\), where N is a finite set of nonterminal symbols of arity 0; \(\varSigma \) is a ranked alphabet; \(S\in N\) is an initial nonterminal; a is a type assignment that gives types for members of \(\varSigma \cup N\); and \(\delta \) is a finite set of productions of the form \(A_0 \rightarrow \sigma ^{(i)}(A_1, \ldots , A_i)\), where for \(1 \le j \le i\), each \(A_j \in N\) is a nonterminal such that if \(a(\sigma ^{(i)}) = (\tau _0, \tau _1, \ldots , \tau _i)\) then \(a(A_j) = \tau _j\).
In a SyGuS problem, each variable, such as x and y in the example RTGs in Sect. 1, is treated as an arity0 symbol—i.e., \(x^{(0)}\) and \(y^{(0)}\).
Given a tree \(t\in T_{\varSigma \cup N}\), applying a production \(r = A\rightarrow \beta \) to t produces the tree \(t'\) resulting from replacing the leftmost occurrence of A in t with the righthand side \(\beta \). A tree \(t\in T_\varSigma \) is generated by the grammar G—denoted by \(t\in L(G)\)—iff it can be obtained by applying a sequence of productions \(r_1\cdots r_n\) to the tree whose root is the initial nonterminal S.
SyntaxGuided Synthesis. A SyGuS problem is specified with respect to a background theory T—e.g., linear arithmetic—and the goal is to synthesize a function f that satisfies two constraints provided by the user. The first constraint, \(\psi (f,\bar{x})\), describes a semantic property that f should satisfy. The second constraint limits the search space S of f, and is given as a set of expressions specified by an RTG G that defines a subset of all terms in T.
Definition 2
Open image in new window A SyGuS problem over a background theory T is a pair \({sy}=(\psi (f,\bar{x}), G)\) where G is a regular tree grammar that only contains terms in T—i.e., \(L(G)\subseteq T\)—and \(\psi (f,\bar{x})\) is a Boolean formula constraining the semantic behavior of the synthesized program f.
A SyGuS problem is realizable if there exists a expression \(e\in L(G)\) such that \(\forall \bar{x}{.} \psi ([\![e ]\!],\bar{x})\) is true. Otherwise we say that the problem is unrealizable.
Theorem 1
(Undecidability [6]). Given a SyGuS problem \({sy}\), it is undecidable to check whether \({sy}\) is realizable.
 1.
Call the synthesizer S to find an expression e such that Open image in new window holds and go to step 2; return unrealizable if no expression exists.
 2.
Call the verifier V to find a model c for the formula \(\lnot \psi ([\![e ]\!],\bar{x})\), and add c to the counterexample set \({E} \); return e as a valid solution if no model is found.
Because SyGuS problems are only defined over firstorder decidable theories, any SMT solver can be used as the verifier V to check whether the formula \(\lnot \psi ([\![e ]\!],\bar{x})\) is satisfiable. On the other hand, providing a synthesizer S to find solutions such that \(\forall \bar{x}\in {E} {.}\psi ([\![e ]\!],\bar{x})\) holds is a much harder problem because e is a secondorder term drawn from an infinite search space. In fact, checking whether such an e exists is an undecidable problem [6].
The main contribution of our paper is a reduction of the unrealizability problem—i.e., the problem of proving that there is no expression \(e\in L(G)\) such that \(\forall \bar{x}\in {E}.\psi ([\![e ]\!],\bar{x})\) holds—to an unreachability problem (Sect. 4). This reduction allows us to use existing (un)reachability verifiers to check whether a SyGuS instance is unrealizable.
3.2 CEGIS and Unrealizability
The CEGIS algorithm is sound but incomplete for proving unrealizability. Given a SyGuS problem \({sy}=(\psi (f,\bar{x}),G)\) and a finite set of inputs \({E} \), we denote with \({sy}^{E}:=(\psi ^{E} (f,\bar{x}),G)\) the corresponding SyGuS problem that only requires the function f to be correct on the examples in E.
Lemma 1
(Soundness). If \({sy}^{E} \) is unrealizable then \({sy}\) is unrealizable.
Even when given a perfect synthesizer S—i.e., one that can solve a problem \(sy^{E} \) for every possible set \({E} \)—there are SyGuS problems for which the CEGIS algorithm is not powerful enough to prove unrealizability.
Lemma 2
(Incompleteness). There exists an unrealizable SyGuS problem \({sy}\) such that for every finite set of examples \({E} \) the problem \({sy}^{E} \) is realizable.
Despite this negative result, we will show that a CEGIS algorithm can prove unrealizability for many SyGuS instances (Sect. 5).
4 From Unrealizability to Unreachability
In this section, we show how a SyGuS problem for finitely many examples can be reduced to a reachability problem in a nondeterministic, recursive program in an imperative programming language.
4.1 Reachability Problems
For the programs \(P[{G},{E}]\) used in our unrealizability algorithm, the only calls to \(\texttt {nd()}\) are ones that control whether or not a production is selected from grammar G during a topdown, lefttoright generation of an expressiontree. Given \(\texttt {n}\), we can decode it to identify which expressiontree \(\texttt {n}\) represents.
Example 1
Consider again the SyGuS problem \((\psi _{\texttt {max2}}(f,x,y), G_2)\) discussed in Sect. 2. In the discussion of the initial program \(P[{G_2},{E_1}]\) (Fig. 1), we hypothesized that the program analyzer chose to report path (1) in P, for which the sequence of nondeterministic choices is t, f, t, f, f, f, t. That sequence means that for \({\hat{P}}[\texttt {n}]\), the value of \(\texttt {n}\) is \(1000101~(\text {base}~2)\) (or \(69~(\text {base}~10)\)). The 1s, from loworder to highorder position, represent choices of production instances in a topdown, lefttoright generation of an expressiontree. (The 0s represent rejected possible choices). The rightmost 1 in \(\texttt {n}\) corresponds to the choice in line (3) of “ Open image in new window ”; the 1 in the thirdfromrightmost position corresponds to the choice in line (10) of “ Open image in new window ” as the left child of the Plus node; and the 1 in the leftmost position corresponds to the choice in line (12) of “ Open image in new window ” as the right child. By this means, we learn that the behavioral specification \(\psi _{\texttt {max2}}(f,x,y)\) holds for the example set \(E_1 = \{ (0,1) \}\) for \(f \mapsto \texttt {Plus(x,1)}\). \(\square \)
Definition 3
(Reachability Problem). Given a program \(\hat{P}[\texttt {n}]\), containing assertion statements and a nondeterministic integer input \(\texttt {n}\), we use \(re_P\) to denote the corresponding reachability problem. The reachability problem \(re_P\) is satisfiable if there exists a value n that, when bound to \(\texttt {n}\), falsifies any of the assertions in \(\hat{P}[\texttt {n}]\). The problem is unsatisfiable otherwise.
4.2 Reduction to Reachability
The main component of our framework is an encoding \(\textit{enc} \) that given a SyGuS problem \({sy}^{E} =(\psi ^{E} (f,{x}), G)\) over a set of examples \({E} = \{c_1,\ldots ,c_k\}\), outputs a program \(P[{G},{{E}}]\) such that \({sy}^{E} \) is realizable if and only if \(re_{\textit{enc} ({sy}, E)}\) is satisfiable. In this section, we define all the components of \(P[{G},{{E}}]\), and state the correctness properties of our reduction.
Remark: In this section, we assume that in the specification \(\psi (f,x)\) every occurrence of f has x as input parameter. We show how to overcome this restriction in App. A [13]. In the following, we assume that the input x has type \(\tau _I\), where \(\tau _I\) could be a complex type—e.g., a tuple type.
Lemma 3
Let A be a nonterminal, \(e\in L(G,A)\) an expression, and \(\{i_1,\dots ,i_k\}\) an input set. Then, \(([\![e ]\!] (i_1),\dots ,[\![e ]\!] (i_k))=[\![\texttt {funcA}[{\#}(e)] ]\!] (i_1,\dots ,i_k)\).

Nontermination. Some numbers can cause \(\texttt {funcA}[n]\) to fail to terminate. For instance, if the case for “ Open image in new window ” in program \(P[{G_2},{E_1}]\) from Fig. 1 were moved from the first branch (lines (3)–(8)) to the final else case (line (13)), the number \(\texttt {n} = 0 = \ldots 0000000~(\text {base}~2)\) would cause Start to never terminate, due to repeated selections of Plus nodes. However, note that the only assert statement in the program is placed at the end of the main procedure. Now, consider a value of n such that \(re_{\textit{enc} ({sy}, E)}\) is satisfiable. Definition 3 implies that the flow of control will reach and falsify the assertion, which implies that \(\texttt {funcA}[{n}]\) terminates.^{4}

Shared suffixes of sufficient length. In Example 1, we showed how for program \(P[{G_2},{E_1}]\) (Fig. 1) the number \(\texttt {n} = 1000101~(\text {base}~2)\) corresponds to the topdown, lefttoright generation of Plus(x,1). That derivation consumed exactly seven bits; thus, any number that, written in \(\text {base}~2\), shares the suffix 1000101—e.g., 11010101000101—will also generate Plus(x,1).
The issue of shared suffixes is addressed in the following lemma:
Lemma 4
For every nonterminal A and number \(\texttt {n}\) such that \([\![\texttt {funcA}[{n}] ]\!] (i_1,\dots ,i_k) \ne \bot \) (i.e., \(\texttt {funcA}\) terminates when the nondeterministic choices are controlled by \(\texttt {n}\)), there exists a minimal \(\texttt {n}'\) that is a (\(\text {base}~2\)) suffix of \(\texttt {n}\) for which (i) there is an \(e \in L(G)\) such that \({\#}(e) = {n}'\), and (ii) for every input \(\{i_1,\dots ,i_k\}\), we have \([\![\texttt {funcA}[{n}] ]\!] (i_1,\dots ,i_k)=[\![\texttt {funcA}[{n}'] ]\!] (i_1,\dots ,i_k)\).
We are now ready to state the correctness property of our construction.
Theorem 2
Given a SyGuS problem \({sy}^{E} =(\psi _E(f,x), G)\) over a finite set of examples \({E} \), the problem \({sy}^{E} \) is realizable iff \( re_{\textit{enc} ({sy}, E)}\) is satisfiable.
5 Implementation and Evaluation
nope is a tool that can return twosided answers to unrealizability problems of the form \({sy}= (\psi , G)\). When it returns unrealizable, no expressiontree in L(G) satisfies \(\psi \); when it returns realizable, some \(e \in L(G)\) satisfies \(\psi \); nope can also time out. nope incorporates several existing pieces of software.
 1.
The (un)reachability verifier SeaHorn is applied to the reachability problems of the form \(re_{\textit{enc} ({sy},{E})}\) created during successive CEGIS rounds.
 2.
The SMT solver Z3 is used to check whether a generated expressiontree e satisfies \(\psi \). If it does, nope returns realizable (along with e); if it does not, nope creates a new input example to add to \({E} \).
It is important to observe that SeaHorn, like most reachability verifiers, is only sound for un satisfiability—i.e., if SeaHorn returns unsatisfiable, the reachability problem is indeed unsatisfiable. Fortunately, SeaHorn ’s onesided answers are in the correct direction for our application: to prove unrealizability, nope only requires the reachability verifier to be sound for unsatisfiability.
There is one aspect of nope that differs from the technique that has been presented earlier in the paper. While SeaHorn is sound for \({{\varvec{un}}}{\text {reachability}}\), it is not sound for reachability—i.e., it cannot soundly prove whether a synthesis problem is realizable. To address this problem, to check whether a given SyGuS problem \({sy}^{E} \) is realizable on the finite set of examples \({E} \), nope also calls the SyGuS solver ESolver [2] to synthesize an expressiontree e that satisfies \({sy}^{E} \).^{5}
In practice, for every intermediate problem \({sy}^{E} \) generated by the CEGIS algorithm, nope runs the ESolver on \(sy^{E} \) and SeaHorn on \(re_{\textit{enc} ({sy},{E})}\) in parallel. If ESolver returns a solution e, SeaHorn is interrupted, and Z3 is used to check whether e satisfies \(\psi \). Depending on the outcome, nope either returns realizable or obtains an additional input example to add to \({E} \). If SeaHorn returns unsatisfiable, nope returns unrealizable.
Modulo bugs in its constituent components, nope is sound for both realizability and unrealizability, but because of Lemma 2 and the incompleteness of SeaHorn, nope is not complete for unrealizability.
Benchmarks. We perform our evaluation on 132 variants of the 60 LIA benchmarks from the LIA SyGuS competition track [2]. We do not consider the other SyGuS benchmark track, BitVectors, because the SeaHorn verifier is unsound for most bitvector operations–e.g., bitshifting. We used three suites of benchmarks. LimitedIf (resp. LimitedPlus) contains 57 (resp. 30) benchmarks in which the grammar bounds the number of times an IfThenElse (resp. Plus) operator can appear in an expressiontree to be 1 less than the number required to solve the original synthesis problem. We used the tool Quasi to automatically generate the restricted grammars. LimitedConst contains 45 benchmarks in which the grammar allows the program to contain only constants that are coprime to any constants that may appear in a valid solution—e.g., the solution requires using odd numbers, but the grammar only contains the constant 2. The numbers of benchmarks in the three suites differ because for certain benchmarks it did not make sense to create a limited variant—e.g., if the smallest program consistent with the specification contains no IfThenElse operators, no variant is created for the LimitedIf benchmark. In all our benchmarks, the grammars describing the search space contain infinitely many terms.
Our experiments were performed on an Intel Core i7 4.00 GHz CPU, with 32 GB of RAM, running Lubuntu 18.10 via VirtualBox. We used version 4.8 of Z3, commit 97f2334 of SeaHorn, and commit d37c50e of ESolver. The timeout for each individual SeaHorn/ESolver call is set at 10 min.
Finding: nope can prove unrealizability for \(59/132 \) benchmarks. For the \(59 \) benchmarks solved by nope, the average time taken is \(15.59 \) s. The time taken to perform the last iteration of the algorithm—i.e., the time taken by SeaHorn to return unsatisfiable—accounts for \(87\%\) of the total running time.
nope can solve all of the LimitedIf benchmarks for which the grammar allows at most one IfThenElse operator. Allowing more IfThenElse operators in the grammar leads to larger programs and larger sets of examples, and consequently the resulting reachability problems are harder to solve for SeaHorn.
For a similar reason, nope can solve only one of the LimitedPlus benchmarks. All other LimitedPlus benchmarks allow 5 or more Plus statements, resulting in grammars that have at least 130 productions.
Note that Z3 can produce different models for the same query, and thus different runs of NOPE can produce different sequences of examples. Hence, there is no guarantee that NOPE finds a good sequence of examples that prove unrealizability. One measure of success is whether nope is generally able to find a small number of examples, when it succeeds in proving unrealizability.
Finding: The number of examples required to prove unrealizability depends mainly on the arity of the synthesized function and the complexity of the grammar. The number of examples seems to grow quadratically with the number of bounded operators allowed in the grammar. In particular, problems in which the grammar allows zero IfThenElse operators require 2–4 examples, while problems in which the grammar allows one IfThenElse operator require 7–9 examples.
Figure 3 plots the running time of nope against the number of examples generated by the CEGIS algorithm. Finding: The solving time appears to grow exponentially with the number of examples required to prove unrealizability.
6 Related Work
The SyGuS formalism was introduced as a unifying framework to express several synthesis problems [1]. Caulfield et al. [6] proved that it is undecidable to determine whether a given SyGuS problem is realizable. Despite this negative result, there are several SyGuS solvers that compete in yearly SyGuS competitions [2] and can efficiently produce solutions to SyGuS problems when a solution exists. Existing SyGuS synthesizers fall into three categories: (i) Enumeration solvers enumerate programs with respect to a given total order [7]. If the given problem is unrealizable, these solvers typically only terminate if the language of the grammar is finite or contains finitely many functionally distinct programs. While in principle certain enumeration solvers can prune infinite portions of the search space, none of these solvers could prove unrealizability for any of the benchmarks considered in this paper. (ii) Symbolic solvers reduce the synthesis problem to a constraintsolving problem [3]. These solvers cannot reason about grammars that restrict allowed terms, and resort to enumeration whenever the candidate solution produced by the constraint solver is not in the restricted search space. Hence, they also cannot prove unrealizability. (iii) Probabilistic synthesizers randomly search the search space, and are typically unpredictable [14], providing no guarantees in terms of unrealizability.
Synthesis as Reachability. CETI [12] introduces a technique for encoding templatebased synthesis problems as reachability problems. The CETI encoding only applies to the specific setting in which (i) the search space is described by an imperative program with a finite number of holes—i.e., the values that the synthesizer has to discover—and (ii) the specification is given as a finite number of inputoutput test cases with which the target program should agree. Because the number of holes is finite, and all holes correspond to values (and not terms), the reduction to a reachability problem only involves making the holes global variables in the program (and no more elaborate transformations).
In contrast, our reduction technique handles search spaces that are described by a grammar, which in general consist of an infinite set of terms (not just values). Due to this added complexity, our encoding has to account for (i) the semantics of the productions in the grammar, and (ii) the use of nondeterminism to encode the choice of grammar productions. Our encoding creates one expressionevaluation computation for each of the example inputs, and threads these computations through the program so that each expressionevaluation computation makes use of the same set of nondeterministic choices.
Using the inputthreading, our technique can handle specifications that contain nested calls of the synthesized program (e.g., \(f(f(x)) = x\)). (App. A [13]).
The inputthreading technique builds a product program that performs multiple executions of the same function as done in relational program verification [4]. Alternatively, a different encoding could use multiple function invocations on individual inputs and require the verifier to thread the same bitstream for all input evaluations. In general, verifiers perform much better on product programs [4], which motivates our choice of encoding.
Unrealizability in Program Synthesis. For certain synthesis problems—e.g., reactive synthesis [5]—the realizability problem is decidable. The framework tackled in this paper, SyGuS, is orthogonal to such problems, and it is undecidable to check whether a given SyGuS problem is realizable [6].
Mechtaev et al. [11] propose to use a variant of SyGuS to efficiently prune irrelevant paths in a symbolicexecution engine. In their approach, for each path \(\pi \) in the program, a synthesis problem \(p_\pi \) is generated so that if \(p_\pi \) is unrealizable, the path \(\pi \) is infeasible. The synthesis problems generated by Mechtaev et al. (which are not directly expressible in SyGuS) are decidable because the search space is defined by a finite set of templates, and the synthesis problem can be encoded by an SMT formula. To the best of our knowledge, our technique is the first one that can check unrealizability of general SyGuS problems in which the search space is an infinite set of functionally distinct terms.
Footnotes
 1.
Grammar \(G_2\) only generates terms that are equivalent to some linear function of x and y; however, the maximum function cannot be described by a linear function.
 2.
The synthesis problem presented above is one that is generated by a recent tool called QSyGuS, which extends SyGuS with quantitative syntactic objectives [10]. The advantage of using quantitative objectives in synthesis is that they can be used to produce higherquality solutions—e.g., smaller, more readable, more efficient, etc. The synthesis problem \((\psi _{\texttt {max2}}(f,x,y), G_2)\) arises from a QSyGuS problem in which the goal is to produce an expression that (i) satisfies the specification \(\psi _{\texttt {max2}}(f,x,y)\), and (ii) uses the smallest possible number of ifthenelse operators. Existing SyGuS solvers can easily produce a solution that uses one ifthenelse operator, but cannot prove that no better solution exists—i.e., \((\psi _{\texttt {max2}}(f,x,y), G_2)\) is unrealizable.
 3.
Grammar \(G_2\) generates all linear functions of x and y, and hence generates an infinite number of functionally distinct programs; however, the maximum function cannot be described by a linear function.
 4.
If the SyGuS problem deals with the synthesis of programs for a language that can express nonterminating programs, that would be an additional source of nontermination, different from that discussed in item Nontermination. That issue does not arise for LIA SyGuS problems. Dealing with the more general kind of nontermination is postponed for future work.
 5.
We chose ESolver because on the benchmarks we considered, ESolver outperformed other SyGuS solvers (e.g., CVC4 [3]).
Notes
Acknowledgment
This work was supported, in part, by a gift from Rajiv and Ritu Batra; by AFRL under DARPA MUSE award FA87501420270 and DARPA STAC award FA875015C0082; by ONR under grant N000141712889; by NSF under grants CNS1763871 and CCF1704117; and by the UWMadison OVRGE with funding from WARF.
References
 1.Alur, R., et al.: Syntaxguided synthesis. In: Formal Methods in ComputerAided Design (FMCAD), pp. 1–8. IEEE (2013)Google Scholar
 2.Alur, R., Fisman, D., Singh, R., SolarLezama, A.: SyGuSComp 2016: results and analysis. arXiv preprint arXiv:1611.07627 (2016)
 3.Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642221101_14CrossRefGoogle Scholar
 4.Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642214370_17CrossRefGoogle Scholar
 5.Bloem, R.: Reactive synthesis. In: Formal Methods in ComputerAided Design (FMCAD), p. 3 (2015)Google Scholar
 6.Caulfield, B., Rabe, M.N., Seshia, S.A., Tripakis, S.: What’s decidable about syntaxguided synthesis? arXiv preprint arXiv:1510.08393 (2015)
 7.
 8.Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 447–450. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662466810_41CrossRefGoogle Scholar
 9.Hu, Q., D’Antoni, L.: Automatic program inversion using symbolic transducers. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 376–389 (2017)Google Scholar
 10.Hu, Q., D’Antoni, L.: Syntaxguided synthesis with quantitative syntactic objectives. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 386–403. Springer, Cham (2018). https://doi.org/10.1007/9783319961453_21CrossRefGoogle Scholar
 11.Mechtaev, S., Griggio, A., Cimatti, A., Roychoudhury, A.: Symbolic execution with existential secondorder constraints. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 389–399 (2018)Google Scholar
 12.Nguyen, T.V., Weimer, W., Kapur, D., Forrest, S.: Connecting program synthesis and reachability: automatic program repair using testinput generation. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 301–318. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662545775_17CrossRefGoogle Scholar
 13.Qinheping, H., Jason, B., John, C., Loris, D., Reps, T.: Proving unrealizability for syntaxguided synthesis. arXiv preprint arXiv:1905.05800 (2019)
 14.Schkufza, E., Sharma, R., Aiken, A.: Stochastic program optimization. Commun. ACM 59(2), 114–122 (2016)CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.