We study the problem of synthesizing programs from nonlinear real arithmetic (NRA) specifications. Existing techniques, such as syntax-guided synthesis (SyGuS), fail to synthesize programs when the specification is unrealizable. We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary NRA specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to work on rational inputs and outputs. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by SyGuS for NRA (real inputs and outputs) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications. We have implemented our approach in a prototype tool called NQSynth that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specifications realizable.

翻译：我们研究从非线性实数算术（NRA）规范合成程序的问题。现有技术（如语法引导合成SyGuS）在规范不可实现时无法合成程序。我们认为这在许多情况下不尽人意，旨在从任意NRA规范中合成程序，使得对于任何输入，合成的程序要么产生满足规范的输出，要么报告不存在此类输出。为避免浮点运算固有的舍入误差，我们将程序限制为处理有理数输入和输出。首先，我们证明该合成问题的变体与数论中一个长期未解的开放问题难度相当，且通常不可能从任意NRA规范中合成具有有理数输入和输出的无环程序。其次，针对涉及单个输出变量的规范，我们提出一种完备的合成算法。同时表明，对于可实现规范，SyGuS针对NRA生成（实数输入和输出）的程序可作为我们问题的解（其中输入和输出为有理数）。第三，我们为一般规范提供一种完备（但必然不完备）的合成算法。我们已在原型工具NQSynth中实现该方法，该工具能够解决许多超出最先进SyGuS工具能力范围的基准测试，即使将规范设定为可实现时也是如此。