未解释函数的等式逻辑约简与Acker-mann方法

理论计算机科学电子笔记144（2006）53-65www.elsevier.com/locate/entcs未解释函数阿米尔·普努埃利 Ofer Strichman21美国纽约州纽约大学和以色列Rehospital魏茨曼研究所。电子邮件地址：amir@cs.nyu.edu2以色列海法理工学院。 电子邮件地址：ofers@ie.technion.ac.il摘要将具有未解释函数的等式逻辑（EUF）约简为具有Acker-mann方法的等式逻辑，其我们提出了一个框架，在该框架中，函数实例的语法特征（签名）用于猜测哪些约束可能需要的证明。这个框架可以组合在抽象-细化循环中，或者在某些情况下，不需要细化迭代就可以使用。该框架适用于等价性验证问题，这是未解释函数的典型用途之一。 它使我们能够验证翻译验证产生的数十个验证条件，我们无法证明。关键词：等式与未解释的功能，阿克曼约化，功能一致性。1引言具有未解释函数的等式逻辑（EUF）是验证中的一个流行逻辑片段，特别是在证明转换系统之间的等价性时。证明电路的两个版本之间的等价性[6，4]或在称为翻译验证[10，8]的过程中编译器的源和目标之间的等价性是使用这种逻辑的两个突出例子。格式良好的EUF公式定义如下，其中左尖括号和右尖括号内的构造表示非终结符。定义1.1[具有未解释函数的等式逻辑1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.00654A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）53公式：：=公式公式|公式|atomatom：：= term =term|布尔变量term：：= term-variable|功能符号在本文中，我们将集中讨论这种逻辑的单排序版本：所有的术语变量都定义在一个无限域上。此外，我们将假设通过使用辅助宏变量来启用术语共享宏定义的形式为auxi：=termi，并与公式的其余部分相连auxi是一个辅助变量，可以在EUF公式中出现i项的地方用i项未解释的函数可以通过使用Ackermann的归约[ 1 ]（相当于Bryant等人的归约[5，3]）来消除减少需要用新的术语变量替换未解释的函数，并添加一组约束以强制函数一致性，即用相等的参数实例化的两个函数实例返回相同的值。从这里开始，我们将用大写字母表示功能符号 设F是一个n元函数ymol.我们注意到F（→t）是具有参数s →t的F的状态，并且通过|F|在给定的公式中，F的n个策略上不同的实例。我们假设这些实例{F1，.，Fk}，其中k = |F|.遵循Ackermann 然后，对于F的每一对不等式，sayF（→a）andF（→b），其中e→a=（a1， .. . . ，an）and-b=（bl，. . ，bn），我们将添加一个constraintn（一）l=1al=bl→fi=fj其中fi和fj是分别代替F（→a）和F（→b）的新变量。设F是EUF公式中未解释函数符号的集合。 这一推论的结果在<$F∈F中|F|·（|F|-1）/2con strai nts1. 我们在翻译验证[8]问题上的经验是，增长是核查过程中最常见的瓶颈，这促使我们开发了我们在此提出的技术设A和B是两个比较的转换系统（等价地，两个循环），其中部分或全部函数是用未解释函数抽象在不损失一般性的情况下，假设只有一个函数-[1] Bryant等人的另一种简化方法在句法上是不同的，但遵循类似的原则和结果在相同的复杂性。我们在这里不详细说明这两种归约之间的差别A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）5355问题是ymolF，并且具有F（t→1）。 . F（t→n）是F的距离。L∈（A，B）是表示等价验证条件的EUF公式在应用阿克曼具 有 新 的 可 变 量f1 ， . . ，fn 和 一 个 传 递 约 束 集 （ 形 式 为 （ 1 ） ）FCovert→1， . . ，t→n和f1， . . ，fn. 新的验证条件是（2）（f∈ FCf) ）→βE（A，B）我们感兴趣的是通过找到FCJFC来简化检查该公式所需的计算，使得：(3)一解决这个问题的一种方法是使用反例引导的抽象细化（CEGAR）循环：(i) 令FCJ= 0。(ii) 如果|=（f∈FCJf）→成立，返回“valid”。(iii) 如果反例与FC一致，则返回(iv) 将约束从（FC\FCJ）添加到FCJ。(v) 转到二号线。这个循环的终止是有保证的，因为在最坏的情况下FCJ=FC，在这种情况下，循环必须终止于线路ii或iii。这个循环中的主要挑战是在步骤iv中选择导致快速终止的细化策略。在模型检验的背景下，广泛的研究导致了几种基于对虚假反例的分析的改进技术虽然类似的技术可以在这里使用，我们声称，我们可以做得更好的基础上的典型性质的等价性检查- ING问题。特别是，我们可以不根据反例，而是根据我们对问题的认识来预先定义精化机制这导致了用更少的迭代终止，在我们的特殊情况下，终止根本没有迭代：我们能够准确地预测证明可能需要我们的技术所基于的关键观察是A和B不是任意的转换系统：其中一个，比如A，通常是另一个B的早期版本，等价性证明仅仅确保从A到B的转换保持A2的语义。如果确实如我们所假设的那样，A和B在功能一致性下是等价的，这可能意味着[2]无论从A到B的转换是机械的，例如使用编译器，还是像某些定制设计和面向重新命名的电路转换那样手动进行，56A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）53在转换过程中，功能的使用没有改变因此，证明很可能只依赖于相对侧上的函数实例之间的在极端情况下，两边的函数实例可以配对，这样它们之间的函数一致性就是证明所需要的全部基于这一观察，我们提出了一个名为Reduced Functional Consistency（RFC）的框架对这一框架的完善相当于削弱相似性的定义。在最坏的情况下，所有的例子都是相似的，这就把我们带回到Ackemrann相似性由函数实例的各种句法特征定义。 我们使用这些实例的签名来捕获这些特征。签名是将函数实例映射到字符串的函数。在给定签名的情况下，RFC将函数实例集划分为具有等效签名的小实例集;理想情况下，这些集合包含例如来自相反侧的一对函数实例然后，仅在属于同一分区的相对侧的函数实例对之间施加函数一致性我们将在第2节中更详细地描述这个想法。RFC的实例化可以用作细化策略，作为抽象/细化循环的一部分如果没有一个预定义的签名是足够的（导致收敛），则可以使用其他细化技术因此，保持了完整性。RFC也可以独立于这样的迭代过程使用，如果有理由相信给定的符号是足够的（这相当于有一个抽象-细化循环，只有一次迭代）。在我们的问题域中就是这种情况：我们能够仅用原始约束的一小部分来证明有效性，而不需要进一步的细化步骤。在第3节中给出了在证明程序等价性的上下文中使用RFC的详细示例。实验和结论在第4节中总结了本文。2简化的函数一致性约束在简化功能一致性（RFC）框架中，函数实例的集合被划分为小集合，使得当且仅当两个实例具有相同的签名时，它们才在同一集合中（见下文）。假设我们有一个定义良好的签名，我们强制一致性如下：(i) F（→t）中的一个函数，计算F（→t）的特征.(ii) 为F（→x）和F（→y）if和d添加函数常数constraintA. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）5357仅当（a）n（F（→x））=n（F（→y）），以及（b）F（→x）和F（→y）是方程的一个不动点.条件a和b是正交的。从这里开始，我们只关注条件a，即，假设条件B是固定的，则会发现签名此外，我们将假设我们定义的每个签名将实例划分为每一侧具有相等数量实例的集合首先考虑签名：定 义 2.1[ 签 名 ]LetF （ →t ） 是 一 个 UninterpretedFunctioninstance 。 F0 （ F（→t））是一个简单的递归定义，其中左和右尖括号（F·t）内的表达式被进一步递归扩展0（术语）：=案例术语为函数F（项1，. ，项n）： F（n = 0（项1）n，. . ，0（termn））一个宏定义aux：=term：0（term）输入数值常数c：c（term）：（任期）请注意，R0仅通过签名传播宏定义下面的例子演示了这个定义的使用例2.2考虑子公式辅助1：=F（i3，5）v1=G（F（i1，aux1），i2）我们递归计算0（G（F（i1，aux1），i2））为每个未解释函数实例3计算这样的签名。Q[3]签名的定义可以扩展到更一般的等式而不是宏赋值的情况在这种情况下，一种可能的策略是计算一组字符串而不是单个字符串作为签名的图像。例如，设f是一个EUF，其形式为aux=term1faux=term2faux′，其中f′使用F（aux）项。 则f（aux）={0（F（term1）），0（F（term2））}。对于每个函数实例，给定这样的签名集合，我们可以在如果s1 ∈ f0（F（t→1）），s2∈f0（F（t→2））的情况下，通过F（t → 1）和F（t→2）来增强一致性。 s1=s2。58A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）53函数0的一个独特特征是，如果两个函数实例F（→x）和F（→y）都具有一个函数0符号，则可以用一个项变量来表示n个y这是因为，E_（0）（F（→x））=E_（0）（F（→y））意味着F（→x）和F（→y）的乘积相等，因此，通过函数c_（y）的定义，F（→x）和F（→y）相等。正如我们现在将要看到的，问题在于，在依赖于它可能导致证明无效和需要改进的意义上，R02.1什么时候能证明失败？如果映射的有效性取决于不同输入的等价性（见下文）或不同函数实例的等价性，例如乘法表达式与加法表达式的等价性，则根据E100的映射 例如，考虑图11.一、我们的目标是证明O=OJ的有效性。在全面运作的情况下，o=情况G（in）=H（in）：F（G（in））;否则：0;〇J=情况G（in）=H（in）：F（H（in））;return 0;图1.一、 o和oJ的等价性依赖于两个不同的函数符号（即G和H）之间的功能一致性，这使得RFC的实例化失败。根据阿克曼的定义，公式o=oJ是有效的。另一方面，f（G（in））=f（F（H（in），因此根据RFC，没有添加强制其等价性的功能一致性约束。各自的变量。因此，证明失败。这样做的原因是，在这个例子中，正确性取决于两个不同函数之间的等价性，即G（in）和H（in）。我们从来没有遇到在实践中的一个例子，证明确实取决于两个不同的功能之间的等价性。另一方面，我们确实遇到过这样的情况，即证明依赖于两个函数实例的等价性，即它们的签名仅因输入而不同。换句话说，有效性取决于不同输入之间的关系，但定义0意味着我们不添加反映这一事实的函数一致性约束。例如，考虑图2中的两个表达式。这里，在函数一致性下，o=oJ有效。另一方面，0（F（in1）） /=0（F（in2）），因此A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）5359o= casein1 =in2：F（in1）;else：0;oJ= casein1 =in2：F（in2）;else：0;图二. o和oJ的等价性取决于输入之间的功能一致性，这使得RFC中的0失败。两个实例被给予不同的项变量，并且没有添加可以迫使它们相等的功能因此，证明失败。在这种情况下，正确性取决于两个不同输入i1和i2之间的等价性，这不受功能一致性约束的影响我们可以通过定义一个新的签名来解决这个问题。定 义 2.3[ 签名 1]LetF （ →t） 是一 个 UninterpretedFunctioninstance 。 F1 （ F（→t））是一个简单的定义如下的直接计算，其中左括号和右尖括号再次表示应进一步扩展的表达式1（term）：= caseterm is函数F（项1，. ，termn）： F（n = 1（term1）n，. . ，1（termn））一个宏观定义aux：=term：1（term）输入：i数值常数c：c（term）：（任期）请注意，除了所有输入都将相同的常量字符串“i”贡献给签名之外，“i1”与“i0”给定例2.2中的G（F（i1，v2），i2），G（F（i1，v2），i2）= G（F（i，F（i，5）），i）.通过这个签名，RFC将更多的函数实例组合在一起，并相应地添加了更多的功能一致性约束，这解决了图2中演示的问题。2.2布尔连接词和ITE表达式为了计算签名，函数调用中的布尔连接词（包括ITE表达式）可以被视为未解释的谓词。 在这种情况下，我们向签名添加一个新的字符串' p b '，用于所有b ∈ {<$，ITE，. . }。例如，如果函数的参数由ITE表达式给出，则我们在该表达式中嵌入一个字符串60A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）53j=1j=1j=1例2.4对于输入i1，i2，i3，i4，0（f（ITE（i12.3结果公式的大小如果在有效性方面，0是足够的，我们可以用相同的term变量替换所有具有相同签名的函数实例，因为很明显它们总是彼此相等 在这种情况下，根本不需要功能一致性约束（FC = 0）。另一方面，如果我们需要函数一致性约束，那么仍然需要函数一致性约束。给定一个函数F∈ F，F1将它的一个集划分为F1， .. . . F m，m≤|F|1/2函数系统，使得一个子集Fj，1 ≤j≤m包含来自方程两侧的相等数目的实例。然后，仅在较小的集合内强制执行功能一致性由于我们只在对象的相对两侧的实例之间强制一致性，方程（条件b），我们只有|2/4c在straints。|2/4con strai nt s. 不是其他人吗根据我们需要的原始Ackermann方案，|F|·（|F|-1）/2，或等价地（m|）·（m|)·(Σ m|-1）/2constraints.|−1)/2con strai nt s.如果我们假设具有相同签名的实例不超过固定数量l，则约束的总数变为线性的。事实上，在我们需要证明具有相同签名的实例的数量非常低的验证条件下（几乎从不超过4），导致约束的线性数量。3示例：证明程序等价性考虑验证图3中的两个C代码段返回相同的输出而不管它们在4中的输入的问题。首先，我们将程序转换为静态单赋值（SSA）形式：我们展开for循环两次，同时为每个赋值引入一个新的辅助变量，删除变量声明和输出语句，最后将所有程序语句。这些操作产生了两个转换关系4这种特殊的等价性可以在完全没有未解释函数的情况下证明，句法替换我们仍然使用这个例子，因为它足够简单，可以演示RFC。它不反映我们所处理的翻译验证问题的类型（这需要对翻译语言进行详细介绍A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）5361int n（int i）{ inti， out_a;out_a= in;for（i= 0;i 2; i++）out_a= out_a*in;100，恢复，持续，带|F|2/2>5000个约束。 在施加RFC后，|F|/2=50约束被生成，指示几乎完美的匹配，同时保持公式有效。在我们的实验中，由函数数量造成的瓶颈实际上消失了。我们没有显示求解时间结果的详细列表，因为我们所有的基准测试要么通过两种方法在不到3秒的时间内解决，要么只能在原始约束集超时时使用RFS下表中列出了一些代表性的基准测试，表明每个谓词或算术函数符号生成的约束数量（本表中只有s49与原始约束集超时这些基准是通过分解从一个更大的基准公式中提取出来的在大多数情况下，RISK1生成完美匹配，即函数/谓词符号的k个实例的k/当函数实例的参数在语法上等价时（如常量），我们只引入一个公共变量而不是两个。这解释了存在奇数个约束的情况，并且对于具有k个实例的函数符号，约束小于k/最后一行在括号中包含了如果使用原始的Ackermann约简的话将添加的约束的数量（注意，第i个数据库中的所有数据均由k表示，这些数据库等于iki·（ki−1）/2）。符号S27S44S49KRFCKRFCKRFC<105422022>126211610+211053023−93424232∗21313221/3173125总38十七（一百五十二）30十四（八十二）152113（2168）正如预期的那样，RFC在理论上和实践上都优于Acker-mann理论上，该方法对EUF公式的所有决策过程都是有它大大减少了公式的大小和唯一项的数量（实际上，它只是提取了64A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）53原始公式的子集），因此也应该有助于现代基于SAT的SMT求解器，如ICS[7]和MATHS[2]。我们自己的决策过程是基于BDD和[9]中报告的小域编码4.1总结我们提出了简化的功能一致性（RFC）框架，在该框架中，功能的签名用于划分的功能实例集，然后一致性只保持在分区内我们展示了两个这样的签名，它们被证明足以在我们的问题域中保持完整性我们认为，在实践中，应该有可能在其他领域得到类似的签名这是基于这样的假设，即在等价性检查中，两边不是任意的，而是其中一个是另一个的早期版本，因此我们可以期望在函数实例之间存在某种映射。在我们感兴趣的领域，没有必要在2011年之后进一步改进。一般来说，它可以在抽象-细化循环中使用。如果所有预定义的签名都失败了，可以调用其他细化技术在这种情况下，完整性得到保证，因为在最坏的情况下，所有原始约束都被添加。引用[1] W.阿克曼决策问题的可解情形。逻辑与数学基础研究。1954年阿姆斯特丹北荷兰[2] G. Audemard，P. Bertoli，A. Cimatti，A. Kornilowicz和R. 阿提亚尼 一个基于SAT的解决布尔和线性数学命题公式的方法。 第18届自动演绎国际会议（CADE'02），2002年[3] R.E. Bryant，S.German和M.维列夫在平等逻辑中利用积极平等日未解释的函数。 在proc 11Intl. 计算机辅助验证会议（CAV'99），1999年。[4] R.E. Bryant，S. German和M.维列夫使用未解释函数的逻辑到命题逻辑的有效归约的处理器验证。ACM Transactions on Computational Logic，2（1）：1[5] R.E. Bryant和M.维列夫决定一个具有未解释函数的正相等理论技术报告CMU-CS-98-141，CMU，1998年。[6] J. R. Burch和D.L. 迪尔流水线微处理器控制的自动验证 在proc6 thIntl.计算机辅助验证会议（CAV '94），计算机科学讲义第818卷。，第68-80页。Springer-Verlag，1994.[7] J.C. Filliquid，S.奥雷Rueb和N.史恩卡 ICS：集成的佳能和求解器。在日G. 贝里，H。Comon，和A.F i n k e l ，editors，Proc. 13 Intl. 计算机辅助验证会议（CAV'01），LNCS。Springer-Verlag，2001.A. 普努埃利岛Strichman/Electronic Notes in Theoretical Computer Science 144（2006）5365[8] A. Pnueli，Y.罗德岛Shtrichman和M. 西格尔 用小-域实例化。在11号国际会议中心。计算机辅助验证会议（CAV'99），计算机科学讲义。Springer-Verlag，1999.[9] A. Pnueli，Y.罗德岛Strichman和M.西格尔 小模型属性：它能有多小？信息与计算，178（1）：279[10] A. Pnueli，M. Siegel和E.辛格曼翻译验证。芽孢杆菌中Ste Escheren，编辑，第四国际。Conf.TACAS '98，卷1384 Lect. Notes in Comp. Sci. 第151-166页。Springer-Verlag，1998.