一句话：提出基于中国剩余定理的求解技术，使 Sketch 的整数编码能高效处理大整数值程序草图。
程序草图（program sketching）要求合成器为带洞和断言的程序自动找出整数填充值。主流工具 Sketch 虽能高效求解复杂草图，但其整数编码在程序操作大整数值时性能很差。本文提出一种新求解技术，在保留 Sketch 整数编码的前提下处理大整数：利用数论中的中国剩余定理（CRT）重写程序草图，使变量值仅按若干素数的余数进行跟踪。作者证明了该变换的可靠性，并说明所得程序的编码比现有 Sketch 编码指数级更紧凑。在大量操作大整数的基准上，该技术相较现有 Sketch 求解器取得加速，且能求解已有求解器无法处理的基准。
Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, Sketch , can efficiently solve complex program sketches but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this article, we propose a new solving technique that allows Sketch to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing Sketch encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing Sketch solvers and can solve benchmarks that existing Sketch solvers cannot handle.
@article{paperbot1614,
title = {Solving Program Sketches with Large Integer Values},
author = {Qinheping Hu and Rishabh Singh and Loris D’Antoni},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {2},
year = {2022},
doi = {10.1145/3532849}
}