  Proving Unrealizability for Syntax-Guided Synthesis
  We consider the problem of automatically establishing that a given
syntax-guided-synthesis (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
program-analysis 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 any existing SyGus tool so that it can
establish that a successfully synthesized program q is optimal with respect to
some syntactic cost -- e.g., q has the fewest possible if-then-else operators.
Using known techniques, grammar G can be automatically transformed to generate
exactly all programs with lower cost 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/134 variants of
existing linear-integer-arithmetic SyGus benchmarks, whereas all existing SyGus
solvers lack the ability to prove that these benchmarks are unrealizable, and
time out on them.
