arXiv:2504.06542v1 交叉类型：公告 摘要：我们提出了一种新的符号推理引擎，它可以高效地为SQL查询$P_1, \cdots, P_n$生成一个输入$I$，使得在$I$上的输出满足给定的性质（用SMT表达）。这在不同的上下文中都非常有用，例如反驳两个SQL查询的等价性以及澄清一组查询。我们的第一个想法是对每个$P_i$进行推理，即$P_i$的部分输入-输出行为。这种方法既使我们的方法具有语义意识又简化了方法，但这本身是不完整的（因为固定的近似可能会错过某些感兴趣的行为）。因此，我们的第二个想法是对一个表达性较强的近似家族进行搜索（这些近似共同涵盖了所有感兴趣的程序行为），从而使我们的方法变得完整。我们在一个名为Polygon的工具中实现了这些想法，并对其进行了多次基准测试（涵盖SQL等价反驳和查询澄清两个任务）。我们的评估结果表明，Polygon在所有先前的技术中表现显著更优。