理论计算机科学电子笔记147（2006）93-111www.elsevier.com/locate/entcs约束的自动隐含检查Tom Schrijversa，Bart DemoenaGregoryDuckbeter Stuc eyb，cThomFruühwirthd一比利时鲁汶大学计算机科学系B澳大利亚墨尔本大学计算机科学系CNICTA维多利亚实验室，澳大利亚D德国乌尔姆大学计算机科学学院摘要约束处理规则（英语：Constraint Handling Rules，CHR）是一种基于规则的高级编程语言，通常用于定义约束求解器。我们提出了一种方法，自动隐含检查之间的约束条件的求解器。支持蕴涵对于实现可扩展的求解器和具体化以及构建层次化的约束求解器是很重要的。我们的方法并不复制整个约束存储，而是使用尾随机制在适当的位置执行检查。必要的代码增强可以通过基于求解器规则的自动程序转换来完成。我们扩展我们的方法，工作层次结构组织的模块化求解器。我们证明了我们的方法的可靠性和它的完整性的一个限制类的典型的求解器，以及特定的现有的非典型的求解器。我们通过与复制方法进行比较来评估我们的跟踪方法：运行时间几乎减半。关键词：约束处理规则，隐含检查，程序转换，约束求解器层次1介绍约束处理规则[7]（CHR）是一种非常灵活的形式主义，用于编写增量约束求解器和其他反应式系统。因此，规则定义了从一个约束集到等效约束集的转换*科学研究基金研究助理-佛兰德斯（比利时）（F.W.O.）- Vlaanderen）1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.03994T. Schrijvers等人/理论计算机科学电子笔记147（2006）93转换用于简化约束并检测满意度和不满意度。CHR已被广泛使用（见例如[9]）。有效的实现已经可用于语言SICStus Prolog和Eclipse Prolog、SWI-Prolog、HAL和Java。CHR为创建可执行的用户定义的约束求解器提供了迄今为止最好的机制。在本文中，我们将研究如何自动扩展的约束求解器，不仅回答问题的满意度，但也回答问题的含义。支持蕴涵的约束许多流行的约束求解器都以某种形式提供了隐含检查，例如Mozart [14]的条件约束组合子和SICStus [2]中的clp（FD）库的reified约束。类似地，隐含允许构造分层的约束求解器，其中，保护由CHR中实现的底层约束求解器定义，因为约束求解器中的一个重要步骤是确定当前存储是否隐含保护。隐含也是有用的，以建立多个合作的求解器。在本文中，我们扩展了一个并行求解器，能够回答的含义检查，也就是说，一个基本的约束c，它隐含的当前并行约束存储。CHR的隐含检查是Chameleon编程语言[16]的重要组成部分，它使用CHR进行类型类重载（参见[15]）。我们改进了Chameleon使用的基本版本的含义检查。之前，已经在[4]中展示了如何使用隐含检查扩展内置求解器以支持递归求解器。在本文中，我们已经增加了一种方法来扩展与其他cross-solvers的cross-solvers。文[3]给出了一种将基本约束的蕴涵检验扩展到任意逻辑公式的蕴涵检验的一般方法。本文提出的蕴涵检验方法可以推广到任意公式。第一个相关的技术已经在[6]中概述。然而，这种技术并不代表一种隐含检查，而是一种具体化的约束：隐含不仅可能成功或失败，而且还可能延迟，直到它可以被决定。然而，由于更高级别的约束不会被移除，因此自动生成的规则可能会导致终止问题。在这种情况下，用户必须修改规则，这可能会导致更多的不完整性。T. Schrijvers等人/理论计算机科学电子笔记147（2006）93952搜索解算器2.1语义学和操作语义在这一小节中，我们简要介绍了可编程语言或求解器的语法和语义本节的其余部分对于更广泛的介绍和调查，我们建议读者[7]。一个规则求解器CS由一系列规则求解器规则组成。有三种不同的规则。我们用一个例子来介绍它们例2.1下面的四个等式解算器eq定义了一个等式解算器，eq/2等式约束：自反@ eq（X，Y）<=> X == Y|真 的redundant@ eq（X1，Y1）\eq（X2，Y2）<=> X1 == X2，Y1 == Y2|真的symmetric @ eq（X，Y）==> eq（Y，X）.transitive@ eq（X1，Y1），eq（X2，Y2）==> Y1 == X2|等式（X1，Y2）。具有eq/2变量标识符的参数，并且==/2是用于语法身份的内置检查。自反规则是简化规则的一个例子。它指出，如果保护x≠y成立，我们可以用右边的真替换左边的eq（x，y），也就是说，我们可以消除形式为eq（v，v）的东西。对称规则是传播规则的一个示例。它指出，当我们有匹配左侧eq（x，y）的东西时，我们应该添加右侧eq（y，x）。冗余规则是简化（简化和传播）规则的一个例子，它说如果我们有两个约束匹配左手边的eq（x1，y1）和eq（x2，y2），满足保护x1<$x2，y1≠y2我们可以消除\之后的部分匹配，即eq（x2，y2）。换句话说，我们可以消除重复的eq约束。最后的规则是另一个传播规则，它定义了等式是传递封闭的。@符号前面的部分是规则的名称，它是可选的。箭头之前的部分称为规则的头部。箭头和管道符号之间的部分（|）称为规则的守卫（可选）。管道符号后面的部分是规则的主体规则的头部是一系列的约束条件。守卫是给定的内置约束的序列。主体是一系列的约束和内置约束。规则部分地定义了头部中的约束。内置约束是未定义的，它们在现有的求解器中实现在 一般我们 能想到 每 Chr规则 作为简化规则，96T. Schrijvers等人/理论计算机科学电子笔记147（2006）93CSHk\Hr<=>G|B，其中Hk和Hr是头部约束的序列，G是保护，B是规则的主体。如果Hk为空，则该规则是一个简化规则;如果Hr为空，则该规则是一个传播规则。操作语义：可将操作语义描述为一个状态转换系统[1]。执行从包括初始多约束集合（也是查询或约束存储）的初始状态σ0规则应用程序对应于状态转换σi>CSσi+1，并更新多组约束。如果在当前状态中存在与规则头部匹配的不同约束，并且如果（在此匹配下）当前状态的内置约束暗示了保护，则规则是适用的。一个终止导数d是从初始状态σ0开始，经过有限个过渡步骤后到达最终状态σ的导数。最终状态σ是其中不可能有更多过渡步骤的状态。 一般来说，对于相同的初始状态，可以通过许多不同的推导达到许多不同的最终状态。我们表示从σ0到σ的特殊导子dσ0>dσ。此外，我们表示通过推导d获得的最终状态从初始状态σ0开始求解d（σ0）。 请注意，是一个已提交的选择语言，即规则应用程序无法撤消。 因此，查询的特定执行将只涉及可能的派生之一在本文中，我们将使用一个特定的语义实例定义的操作语义[5]是大多数操作系统实现的实际操作语义，例如SICStus [8]，HAL [10]和K.U.Leuven操作系统[11]。这些语义描述了一个特定的执行策略，大大减少了任何初始状态的不同可能的派生的数量以自上而下的方式应用这些规则。状态被分成两部分：从左到右处理的目标序列使用活动约束的概念来应用规则，活动约束是最后添加的约束，它在变为非活动之前在匹配中被彻底使用更多详情请参见[5]。示例2.2下面的示例非正式地描述了在精化操作语义下的派生。考虑执行例2.1中定义的eq/2求解器的目标eq（a，b），eq（b，c）。添加eq（a，b）自反规则不适用，因为a==b不成立，冗余规则缺少第二个约束，对称规则添加eq（b，a）。此约束使用对称规则添加eq（a，b），然后通过冗余规则删除。传递规则现在可以匹配（eq（a，b），eq（b，a）==>b == b|eq（a，a））因此添加了由自反规则去除的eq（a，a）。类似地，传递规则添加了被删除的eq（b，bT. Schrijvers等人/理论计算机科学电子笔记147（2006）9397反身规则。当前存储为{eq（a，b），eq（b，a）}。eq（b，c）的添加导致使用对称规则添加eq（c，b），并且传递规则添加eq（b，b）和eq（c，c），它们被自反规则立即删除，以及eq（c，a）（eq（c，b），eq（b，a）==>b == b|eq（c，a）），其使用对称规则将eq（a，c）相加。 之后，传递规则添加eq（a，c）的另一个副本（eq（a，b），eq（b，c）==>b == b|等式（a，c）），其使用冗余规则被删除。最终存储为{eq（a，b），eq（b，a），eq（b，c），eq（c，b），eq（a，c），eq（c，a）}下面说明了部分推导过程，状态的两个部分显示为“目标”、“存储”和活动约束（粗体），匹配约束加下划线。[eq（a，b），eq（b，c）]，>CS[eq（b，c）]，{eq（a，b）}symmetric>CS<$[eq（b，c）]，{eq（a，b），eq（b，a）}<$symmetric>CS<$[eq（b，c）]，{eq（a，b），eq（b，a），eq（a，b）}<$冗余>CS[eq（b，c）]，{eq（a，b），eq（b，a）}transitive>CS<$[eq（b，c）]，{eq（a，b），eq（b，a），eq（b，b）}<$自反>CS<$[eq（b，c）]，{eq（a，b），eq（b，a）}<$transitive>CS<$[eq（b，c）]，{eq（a，b），eq（b，a），eq（a，a）}<$自反>CS<$[eq（b，c）]，{eq（a，b），eq（b，a）}<$>CS[]，{eq（a，b），eq（b，a），eq（b，c）}symmetric>CS<$[]，{eq（a，b），eq（b，a），eq（b，c），eq（c，b）}<$symmetric>CS<$[]，{eq（a，b），eq（b，a），eq（b，c），eq（c，b），eq（b，c）}<$冗余>CS[]，{eq（a，b），eq（b，a），eq（b，c），eq（c，b）}.>CS[]，{eq（a，b），eq（b，a），eq（b，c），eq（c，b），eq（a，c），eq（c，a）}请注意，传播规则最多应用于同一个约束序列一次，以避免平凡的非终止性。2.2说明性语义约束是一阶逻辑的特殊谓词，其意义由约束理论定义。约束求解器程序98T. Schrijvers等人/理论计算机科学电子笔记147（2006）93CS具有逻辑读数（含义）[CS]]。这个理论[CS]包含了内置约束的约束理论和程序CS中每个规则的一个公式。设vars（F）表示公式F，vars（F）F的唯一闭包为vars（F）F，f或vvF为vars（F）F的唯一闭包。其中W=vars（F）−V，称为F在V上的投影。T. Schrijvers等人/理论计算机科学电子笔记147（2006）93991d2d变量（C）1vars（C）2re =x=y→（eq（x，y）Participtrue）冗余x1<$x2<$y1<$y2→（eq（x1，y1）→（eq（x2，y2）参与）对称eq（x，y）→eq（y，x）传递y1<$x2→（eq（x1，y1）<$eq（x2，y2）→eq（x1，y2））简单规则Hk\Hr<=> G的逻辑解读|B是：（G→（Hk→（HrParticipation<$B）。当你的变量在B体中没有出现时，即vars（B）−（vars（G）vars（Hk）vars（Hr））。 如果Hk、Hr、G或B中的任何一个为空，则它们在公式中被认为是真的通常，求解器编写者的意图是使[CS]近似于某个约束理论D，即[CS]仅覆盖与特定用途相关的D部分。 为了近似的正确性，我们要求[CS]]是约束理论D的模型，即D| = [[CS]（但通常为[CS]）|= D）。由于逻辑读数[CS]，连续状态之间的逻辑等价性得以保持。例2.3例2.1的eq求解器的逻辑读数[eq]]是下面的公式集（其中我们使用[eq]作为语法恒等式）：显然，上述规则描述了等式的经典性质2.3规划求解程序属性约束求解器的一个非常有用的属性是连续性，它确保目标的每个可能的推导都会导致相同的结果。定义2.4[连续求解器]连续约束求解器CS是连续的如果：C，d，dJ：C=solve（C）|=（C）参与者（ C）在一般操作语义下，可终止程序连续的一个可判定的充要条件见[1我们通常不提及并发求解器的具体推导d，如果我们在中间状态中不存在整数，并且写C>nC1或简单地写C1= solve（C）。例2.5等式求解器eq是一个连续求解器。例如，对于查询eq（a，a），自反规则的单个应用或一个appli，100T. Schrijvers等人/理论计算机科学电子笔记147（2006）93对称规则的阳离子和自反规则的两个都产生空的约束存储。一个结合了连续性和声明性语义的属性是正规性它要求语义等价的目标产生相同的结果。定义2.6[规范解算器]一个连续约束解算器CS是canonicalif：J J J JC，C，d， d：（[CS]]|=CParticipC）（C1=solv ed（C））（C2=solv edJ（C））|=(∃¯v ars(C∧C J)C1)↔(∃¯v ars(C∧C J)C2)在[15]中，给出了正则解的一个充分但非必要的条件.一个连续的、范围受限的、所有的简化规则都是单头的迭代求解器给出了一个规范的求解器。如果出现在规则的保护和主体中的所有变量都出现在规则的头部中，则该规则求解器是受范围限制的一般来说，显示求解器是规范的可能是不平凡的。例2.7等式求解器eq是一个规范的范围限制求解器。很明显，它是受范围限制的。显示它是规范的依赖于显示它返回一个store {eq（x，y），eq（y，x）|x和y在由目标中的所有eq约束创建的图中连接。3基本隐含检查基于逻辑蕴涵和合取的性质，我们可以使用以下技术来验证约束c是否被约束的合取所隐含D| = C → c惠D| =（Cc）参与C也就是说，我们可以利用连接词的等价性来推断蕴涵。原则上，我们将通过以下方式验证等效性。求解的形式solve（C）和solve（Cc）沿着一些导数计算。然后，将这些解出的形式投影到Cc的变量上，并检查句法对等这种方法不一定是完整的，但却是合理的，即如果解出的形式的投影在句法上是相同的，那么C就隐含了C。定理3.1（合理性）对于任何非线性解算器CS：C，c：|=v ars（Cc）solv e（C）参与者v ars（Cc）solv e（Cc）解[[CS]]|=（C→c）T. Schrijvers等人/理论计算机科学电子笔记147（2006）93101我的律师。 我们有一个VET TTCS|=CParticipativars（Cc）solv e（C）anddCS|=Cc参与从The或em4.2或[7]中解出（C）。 Henceif|=v ars（Cc）求解（C）参与者如果有CS，则将（C c）求解（Cc）|=CParticipate（Cc）anddhenceCS|=C→C.Q在实际实现中，投影约束的逻辑等价性测试仅限于多集的语法等价性（solve（C）solve（Cc））。对于范围受限的CHR，由于变量（求解（C）），vars（C蕴涵检验的直接实现方法是将C 的一个拷贝CJ，同时将C>CJJ和CJ∈C>CJJj，并检验CJ与CJJ的等价性。我们称这种方法为复制方法，它是Chameleon [16]目前使用的含义检查在实践中C已经是解出的形式，所以C<$CJJ。然而，上述复制方法可能相当昂贵。C可以由两个部分C=C1<$C2组成，使得C1是隐含c的约束的最小集合。通过完全复制C，C2被不必要地复制，并在最终等价性测试中引起不必要的开销。我们提出了跟踪的方法来解决问题。它只考虑最小的约束集：在适当的位置求解合取C_（？）c，并保持变化的踪迹。随后对轨迹的分析告诉我们结果存储是否与原始存储等价。 如果是这样，更新商店可以保留。否则，该轨迹用于恢复到原始情况。例3.2下面的规则在概念上代表了上述策略。请记住，通过从左到右的顺序执行约束和从上到下的规则试验来implications @ check_eq（X，Y）<=> eq（X，Y），analyze_trail.检查eq/2约束表示隐含检查。调用这个约束要么成功要么失败，因为如果结果存储是等价的，则analyse trail/0成功，否则失败。我们的跟踪分析必须考虑约束的添加和删除，以确定等效性。粗略地说，如果在隐含检查期间添加或删除任何约束，则结果存储将不等同于原始存储。更确切地说，如果只是临时添加或删除一个约束，则存储也是等效的，因为添加和删除同一个约束会相互抵消。下面的一组规则反映了这种方法：temporary@ analyse_trail\added（C），removed（C）<=> true。102T. Schrijvers等人/理论计算机科学电子笔记147（2006）93addition@ analyse_trail\added（C）<=>fail.removal@ analyze_trail\removed（C）<=>fail.success@ analyze_trail< => true。这里的added/1和removed/1表示添加和删除约束的跟踪条目。上面的代码使用了细化的语义[5]来正确工作。analyze trail的调用查找匹配的添加/1和删除/1约束，并使用第一条规则删除它们。如果仍然存在任何（不匹配的）added/1和removed/1约束，则第二个或第三个规则将导致其失败。否则，它就达到了第四条规则，它就成功了。通常，原始求解程序会按照下表中给出的规则进行转换，以维护有关更改的信息。实体新规则pp（x<$）==>adde d（p（x<$））添加到程序Hk\Hr<=>G|BHk\Hr<=>G|remov e d（p1（x<$1））， .. . ，removed（pn（x<$n））， B取代旧规则例3.3eq/2求解器被转换如下，以显式生成必要的添加/1和删除/1约束。new @ eq（X，Y）==> added（eq（X，Y））.自反@ eq（X，Y）<=> X == Y|移除（等式（X，Y））。冗余@ eq（X1，Y1）\eq（X2，Y2）=>X1 == X2，Y1 == Y2|去除（等式（X2，Y2））。symmetric @ eq（X，Y）==> eq（Y，X）.transitive@ eq（X1，Y1），eq（X2，Y2）==> Y1 == X2|等 式（X1，Y2）。我们要检查eq（a，c）是否由eq（a，b）eq（b，c）隐含。我们称目标为eq（a，b），eq（b，c），检查eq（a，c）。前两个约束导致存储eq（a，b）、eq（b，c）、eq（a，c）、eq（b，a）、eq（c，b）、eq（c，a），如示例2.2所示。约束检查eq（a，c）首先使用新规则添加added（eq（a，c）），然后冗余规则成功添加removed（eq（a，c））。对analyze trail的调用使用临时规则删除这两个，然后使用成功规则成功。上面的转换求解程序有一个缺点，它总是落后。下面的一组规则仅在T. Schrijvers等人/理论计算机科学电子笔记147（2006）93103隐含期间启用显式尾随104T. Schrijvers等人/理论计算机科学电子笔记147（2006）93正在检查这些规则最初需要在约束存储中保留拖尾隐含@check_eq（X，Y）=> enable_trail，eq（X，Y），analyse_trail，disable_trail.enable@ trail_off，enable_trail< => trail_on.disable@ trail_on，disable_trail< => trail_off.filter_add@ trail_off\added（C）<=> true。filter_remove @ trail_off\removed（C）<=> true。我们的方法是完整的规范范围限制的CHR的唯一解决方案的含义检查。定理3.4（完备性）如果CS是一个规范的范围限制求解器，则蕴涵检验是完备的。即C，c：（[CS]]|= C c）solve（C）solve（C c）证据 根据定义2.6，我们有C，c：（[CS]]|=C参与（Cc）求解（C）参与（C c）求解（C c）由于CS是范围受限的vars（solve（C））变量（Cc）和vars（solve（C c（c））var（Cc）. 因此，solve（C）solve（Cc）。Q请注意，在Cc失败的特殊情况下，c并不被C隐含为Cc并不令人满意。 我们的方法正确地涵盖了这种情况。一个约束求解器不需要是规范的，我们的含义检查是完整的。在第5节中，我们将证明我们的方法对于几个非规范的，甚至是非连续的，递归求解器也是完备的。4模块化求解器层次结构在这一节中，我们将上一节的隐含检查技术扩展到模块化的递归求解器层次结构。约束解算器可以分层嵌套：一个解算器依赖于某些解算器，而这些解算器又依赖于其他解算器。我们说一个求解器依赖于另一个求解器，如果它使用的约束是在其他求解器中定义的。特别地，一个边界求解器可以在边界规则的保护和主体中使用其他求解器的约束。以前只能在guards中使用内置解算器的约束[4]。在这里，我们将展示如何构造可在守卫中使用约束的约束求解器层次结构。在并行求解器层次结构中，依赖图是非循环的。我们将使用父解算器和子解算器来引用依赖于另一个解算器的一个解算器T. Schrijvers等人/理论计算机科学电子笔记147（2006）93105一个模块化的并行计算求解器是一个并行计算求解器，可以使用其依赖关系的接口进行编译。特别是，不需要了解受抚养人。例4.1下面的小于等于求解器leq依赖于eq求解器：leq_new@ leq（X，Y）<=> check_eq（X，Y）|真的leq_antisymmetric @ leq（X1，Y1），leq（X2，Y2）=>check_eq（X1，Y2），check_eq（X2，Y1）|等式（X1，Y1）。leq_redundant @ leq（X1，Y1）\leq（X2，Y2）<=>check_eq（X1，X2），check_eq（Y1，Y2）|真的leq_transitive @ leq（X1，Y1），leq（X2，Y2）==>check_eq（Y1，X2）|l e q （X1，Y1）.这个leq解算器在两个方面依赖于eq解算器。首先，它在leq反对称规则的主体中调用eq/2约束。其次，它还使用了eq/2蕴涵检查来保护所有规则。由于约束和隐含检查都可以很容易地从eq求解器导出，这并不违反模块化。我们还没有处理守卫的一部分操作语义。我们称一个事件为向子解算器或它所依赖的解算器之一添加约束，以便可以满足保护。一个安全规则应用程序可能不会立即成功，因为一个警卫不满意，但一个事件可能会导致它在稍后的时间点得到满足。如果一个事件现在满足了先前未满足的保护，则重新激活父解算器的约束。在实践中，DRM实现高估了事件的影响即，重新激活超过所需的次数。通常对于内建求解器，相关事件由求解器程序员在求解器接口中提供，同时提供一种机制来通知相关方。以下规则描述了eq求解器的事件和通知机制的必要操作new_event @ eq（X，Y）==> touched（X），touched（Y）.trigger @ touched（X），delayed（X，Goal，ID）==> call（Goal）. end_event @ touched（X）=> true。kill_goal @ kill（ID）\ delayed（X，Goal，ID）<=> true. kill_end@ kill（ID）<=> true。eq求解器在其接口中提供了一个触摸（X）事件，而不知道任何关于特定用途的信息。新事件规则为新eq/2约束中涉及的每个变量生成触摸使用者在-106T. Schrijvers等人/理论计算机科学电子笔记147（2006）93接口，如leq求解器将通过调用delayed/3约束来通知这些事件。这个约束提供了一个回调目标，当适当的touched/1事件触发时调用，并允许通知方采取适当的行动。kill/1约束允许基于标识符删除一个或多个延迟回调，并允许通知方不再接收任何事件。下面的伪代码显示了leq求解器如何将自己订阅到触摸事件。它是伪代码，因为它访问了JavaScript实现的一些内部组件。listen@leq（X，Y）# CID ==> new_delay_id（ID），延 迟 （ X ， 重 新 激 活（CID），ID）、延迟（Y，重新激活（CID），ID）、监听（CID，ID）。这里CID是一个内部标识符的约束。这个伪规则在leq（X，Y）约束首次被激活时执行。 的呼声新的延迟ID/1生成新的通知标识符。通过两次延迟调用，将向≤通知后，调用内部目标重新激活（CID），重新激活相应的约束。监听调用在内部将no-tification identifier与相应的leq/2约束相关联。当标识符CID的leq/2约束被删除时，内部kill/1约束会在所有相关的通知标识符上调用。这可避免重新激活已删除的约束。然而，现在需要对原始方案的隐含检查进行几处修改，以适应层次结构和模性。下面我们将解释如何为多个递归求解器做跟踪，如何区分递归调用的隐含检查的跟踪，以及隐含检查应该如何与事件机制交互跟踪接口：首先，由于层次结构，在对父求解器进行隐含检查期间，可以添加和删除子求解器中的约束。因此，父解算器跟踪机制必须递归地依赖于子解算器跟踪机制。子解算器必须为此导出必要的跟踪操作。例4.2下面的一组规则对leq/2求解器对eq/2求解器的尾部依赖性进行编码：rec_analysis@ leq_analyze_trail ==> eq_analyze_trail.rec_enable@ leq_enable_trail==> eq_enable_trail.rec_disable@ leq_disable_trail ==> eq_disable_trail.T. Schrijvers等人/理论计算机科学电子笔记147（2006）93107隐含层：其次，由于层次结构，隐含检查也可以是递归的。例如，leq/2约束的隐含检查可能需要eq/2约束的隐含检查。我们的浅跟踪方法不再涵盖这一点。事实上，它并不区分在递归eq/2蕴涵检查期间添加和删除的eq/2约束和在顶级leq/2蕴涵检查期间添加和删除的eq/2约束。需要一个更复杂的跟踪机制我们的解决方案是将每个隐含层（即隐含检查嵌套的级别）与层标识符相关联。不在任何隐含检查内的顶层具有stratum identi ier 0，从顶层调用的隐含检查具有identi ier-1，等等。每个约束都标有它被调用的层。 比如说，eq（X，Y）如果在S层中调用，则变为eq（X，Y，S）。在顶层查询中调用的约束被分配为层0。在规则体中调用的约束继承规则头中任何约束的最低层，而蕴涵检查将层降低一层。例4.3例如，leq/2求解器转换如下：leq_new@ leq（X，Y，S）<=> check_eq（X，Y，S-1）|真的leq_反对称@ leq（X1，Y1，S1），leq（X2，Y2，S2）=>check_eq（X1，Y2，min（S1，S2）-1），check_eq（X2，Y1，min（S1，S2）-1）| e q （X1，Y1，min（S1，S2））。leq_redundant@leq（X1，Y1，S1）\ leq（X2，Y2，S2）=>check_eq（X1，X2，min（S1，S2）-1），check_eq（Y1，Y2，min（S1，S2）-1）|真 的leq_transitive@ leq（X1，Y1，S1），leq（X2，Y2，S2）==> check_eq（Y1，X2，min（S1，S2）-1）|leq（X1，Y1，min（S1，S2））。现在，通过查看层标识符，可以在单个层上进行蕴涵跟踪操作然而，如果尾随操作被限制在一个层中，则隐含检查被削弱。原因是临时规则：temporary@ analyse_trail（S）\added（C，S），removed（C，S）<=> true.此规则仅取消同一层中的添加和删除。不再被抵消的是在较高层中添加的约束，该约束在较低层中被移除并在该较低层中重新添加。我们有可能在下文中重新描述这种可能性每次删除时后者是移除的原因。为108T. Schrijvers等人/理论计算机科学电子笔记147（2006）93例如，leq2规则看起来像：leq2@leq（X1，Y1，S1），leq（X2，Y2，S2）=>check_eq（X1，Y2，min（S1，S2）-1），check_eq（X2，Y1，min（S1，S2）-1）|移 除 （leq（X1，Y1），S1，min（S1，S2）），移除（leq（X2，Y2），S2，min（S1，S2）），eq（X1，Y1，min（S1，S2））。下面的规则处理这个新删除的/3约束。temporary@analyse_trail（S）\added（leq（X，Y），S），删除（leq（X，Y），S，S）<=> true.promotion@analyze_trail（S）\ added（leq（X，Y），S），leq（X，Y，S），去除（leq（X，Y），Sr，S）<=> S< Sr| leq（X，Y，Sr）。临时规则仍然取消同一层中的添加和删除，但提升规则将新约束提升到先前删除的约束所在的层。通过这种方式，求解器层次结构保留了基本含义检查的全部功能。检查eq/3的定义如下。我们可以摆脱显式的trail启用和禁用，因为我们有了隐含层：层0永远不需要trailing，而其他层总是需要。toplevel_add @ added（_，0）=> true。toplevel_rem @ removed（_，_，0）=>true。含义@check_eq（X，Y，S）<=> eq（X，Y，S），eq_analyze_trail（S）.层间事件：在子解算器中发生的含义检查期间，可能会触发一个事件，唤醒一些父解算器约束，导致在更高层中添加或删除一些父解算器约束。然而，这些事件不一定要穿越地层。隐含检查可以安全地解决，而无需将任何信息传播到更高层中的父求解器：由于子求解器不依赖于父求解器，因此对子求解器的隐含检查的结果不需要与父求解器交互反过来说，在低层存在的情况下，高层永远不会生成任何事件，因为它在低层执行时会暂时中止，只有在低层的隐含检查完成后才消失，因此低层消失了T. Schrijvers等人/理论计算机科学电子笔记147（2006）93109全部因此，事件只在同一层内触发回调是安全和便宜的。以下修改的事件代码反映了这一点。new_event @ eq（X，Y，S）==> touched（X，S），触摸（Y，S）。trigger @ touched （X ，S ），delayed （X ，Goal ，S ，ID）==> call（Goal）. end_event @ touched（X，S）=> true。听@leq（X，Y，S）# CID ==> new_delay_id（ID），延迟（X，重新激活（CID），S，ID），延迟（Y，重新激活（ CID ） ， S ， ID ） ， 监 听（CID，ID）。5案例研究：非规范求解器我们在第3节中已经证明，我们的正则解算器的隐式检查是完全的。在本节中，我们将研究一些经典的、非正则的求解器的完备性。结果是，在许多情况下，隐含检查仍然是完整的，或者在特定情况下可以通过一点定制来完成。5.1朴素联合-查找等式求解器在[13]中，给出了朴素并集查找算法的一个简单实现（源代码见附录A）。该实现中的union/2约束可以用作等式约束。朴素的union-find将相同的变量表示为同一树中的节点任何一棵树中有相同的变量，都表示它的元素相等没有一个优选的标准形式。由于这个原因，它甚至是不连续的：union/2约束的顺序决定了树的形状如果两个已经相等的变量被联合，它们的公共树不会被修改，也不会删除或添加任何其他约束然而，如果两个变量还不相等，联合会将它们的树合并为一个。因此，我们的隐含检查对于这个并集查找等式求解器是完整的5.2最优并求等式解算器除了朴素算法之外，[12]中还给出了一个最优并集查找算法的快速实现（源代码见附录B该算法结合了路径压缩和按秩合并。同样，当两个变量不相等时，它们各自的树被合并110T. Schrijvers等人/理论计算机科学电子笔记147（2006）93（按秩），这是由我们的隐含方法检测然而，在变量已经相等的情况下，路径压缩仍然可以通过缩短从节点到根的路径来修改树。 由于压缩后的树在语法上与初始树不同，我们的蕴涵方法将拒绝它。然而，可以自定义trail analysis/0规则来克服这个问题，并安全地允许路径压缩，同时真正拒绝新的平等 也就是说，而不是这些一般规则：addition@ analyse_trail（S）\ added（C，S）<=>fail.removal@ analyse_trail（S）\ removed（C，_，S）<=> fail.仅需要检测根约束的移除来检测两棵树的链接：removal@ analyze_trail（S）\ removed（root（_，_），_，S）<=> fail.cleanup1@analyse_trail（S）\ added（_，S）<=> true.cleanup2@analyze_trail（S）\ removed（_，_，S）<=> true. cleanup3@analyse_trail（S）\<'~'（X，Y，S）=> '~'（X，Y，S+1）.由于这些规则不考虑路径压缩作为可能的非等价树。实际上，它们甚至不会在隐含检查之后撤销路径压缩，而是将新创建的边提升到更高层。因此，在后续的隐含检查之后，保留更简单的树表示，使得未来的操作更便宜。6实验评价我们将我们的跟踪方法与朴素复制方法进行比较以验证它。出于这个原因，我们考虑了eq求解器的特定基准。对于1≤i n，施加n− 1个约束eq（Vi，Vi+1）。这个连接我们称之为C的等式约束我们测试的约束c是eq（V1，Vn）在一种情况下和在另一种情况下的eq（ V1，Vn+1）。前一种测试成功，后一种测试失败。表1列出了在具有512 MB RAM的Intel Pentium 4 2.0GHz上使用SWI-Prolog中的K. U. Leuven Pentium系统在n=20的情况下针对该基准获得的以秒为单位的实验结果。执行复制方法的隐含检查的总时间等于solve（C）和solve（Cc）1的时间之和。 通过我们的跟踪方法，计算时间C=c对应于求解时间（Cc）。 虽然约有16%对于普通使用（solve（C））的开销，拖尾方法显然优于隐含测试的复制方法：它几乎是我们的两倍1对于这个基准测试，比较约束悬挂物的时间可以忽略不计。T. Schrijvers等人/理论计算机科学电子笔记147（2006）93111方法求解（C）求解（Cc）C =0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000c=eq（V1，Vn）副本尾随4.345.024.425
我的内容管理
展开
