反向CAD模型重构及其在网格反编译中的应用

31等饱和反变换综合结构化CAD模型Chandrakana Nandi华盛顿大学美国cnandi@cs.washington.eduJames R.威尔科克斯CertoraUSAjames@certora.comMax Willsey华盛顿大学美国mwillsey@cs.washington.edu伊娃·达鲁洛娃MPI-SWS德国eva@mpi-sws.org美国华盛顿大学ztatlock@cs.washington.edu美国华盛顿大学adamand2@cs.washington.edu丹·格罗斯曼华盛顿大学美国djg@cs.washington.edu摘要最近的程序合成技术帮助用户定制CAD模型（例如，用于3D打印），将低级三角形网格反编译为构造性实体几何（CSG）模型。如果没有循环或函数，编辑CSG可能需要进行许多协调的更改，而现有的网格解压缩器使用的算法可能会混淆高级结构。本文提出了第二个反编译阶段，鲁棒性地将非结构化CSG表达式压缩成具有映射和折叠运算符的更可编辑的程序。我们提出Szalinski，一个工具，使用平等饱和与语义保持CAD重写有效地搜索较小的等效程序。Szalinski依赖于逆变换，这是求解器推测性地向E-图添加等值的一种新方法。我们定性评估Szalinski的案例研究，显示它如何与现有的网格反编译组成，并证明Szalinski可以缩小大模型在几秒钟内。CCS概念：·软件及其工程→编译器;领域特定语言;软件逆向工程;·计算理论→程序语义学;·计算方法学→参数曲线和曲面模型。允许免费制作本作品的全部或部分的数字或硬拷贝，以供个人或课堂使用，前提是制作或分发副本的目的不是为了盈利或商业利益，并且副本的第一页上有本声明和完整的引用本作品的版权归ACM以外的其他人所有，必须予以尊重。允许使用学分进行摘要以其他方式复制、重新发布、在服务器上发布或重新分发到列表中，需要事先获得特定许可和/或付费。请求权限请发邮件至permissions@acm.org。PLDI© 2020计算机协会。ACM ISBN 978-1-4503-7613-6/20/06。. . 15美元https://doi.org/10.1145/3385412.3386012关键词：等饱和，程序综合，反编译，计算机辅助设计ACM参考格式：放大图片作者：James R.Wilcox，Eva Darulova，DanGrossman，and Zachary Tatlock. 2020.用等饱和和逆变换综合结构化CAD模型.在第41届ACM SIGPLAN编程语言设计和实现国际会议（PLDI '20）的会议记录中，2020年6月15日至20日，英国伦敦。ACM，纽约州纽约市，美国，14页。https://doi.org/10.1145/3385412.33860121引言编程语言和机器学习社区已经开发出将计算机辅助设计（CAD）模型从低级数值表示反编译为构造性立体几何（CSG）表示的技术[11，13，14，21，30，31，36]。这些技术旨在帮助用户修改在线存储库中共享的设计[1，15，35]。最近的程序合成结果[11，21]反编译网格，定义对象表面的三角形集合，转换为等效的CSG表达式。CSG包括几何图元（如圆柱体）、仿射变换（如平移）和集合理论运算符（如并集）。现有的网格反编译器合成平面输出：CSG没有循环或函数（图1，左）。因此，由具有重复特征的大网格合成的CSG也趋向于大且重复。在传统的编程中，重复使得原本直观的编辑变得乏味和容易出错。网格反编译是欠约束的[11，21]，因此过去的工具依赖于算法，这导致它们表现出两个具有挑战性的特征：（C1）为在不同变换下重复的相同特征合成等效但耗散的CSG表达式，以及（C2）任意排序的CSGPLDIC.Nandi，M.Willsey，A.安德森，J。R. Wilcox，E.Darulova，D.Grossman，Z.塔特洛克32~1600μ m，网孔~50μ m，CSG图1. 现有的网格反编译器将三角形网格转换为CSG表达式。Szalinski稳健地从CSG表达式合成了较小的结构化Caddy程序这可以通过简化编辑来简化定制：小的，主要是局部的更改会产生有用的不同模型。照片显示了定制孔尺寸后的3D打印六角扳手支架子表达式。这两个特征（C1）和（C2）混淆了合成CSG中潜在的高级结构。本文提出了第二个反编译阶段，与以前的工作组成：给定一个平面CSG表达式，产生一个等效的，更小的，更可编辑的程序与地图和折叠操作符表示重复。我们提出了Szalinski1（图1），这是一种将语义保持重写与简单求解器相结合的工具，可以在一种名为Caddy的语言中合成结构化CAD程序。Szalinski被设计为鲁棒地处理现有网格反编译器的噪声和非结构化输出在这些输出中，只有在明智地应用了一组CAD特定的重写之后，高级结构才变得明显（C1）。过去关于等式饱和度的工作[34]表明，等式图（E-graphs）[22]是SMT求解器[8，10]和程序优化器[16，33，34，42]的有效数据结构，它非常适合Szalinski，因为E-graphs可以对许多等价的方式进行压缩编码，以表达一组重写的程序不幸的是，结合和交换重写的重新排序可能导致E-图以指数方式爆炸。这被称为AC匹配问题[3，6，17]。这对Szalinski提出了一个重大挑战，因为现有的网格反编译器通常输出按几何学排序的CSG特征（例如，几何邻近性）而不是高级结构（C2）。为了解决Szalinski的AC匹配问题，我们提出了逆变换，求解器的一种新的方式来推测统一的E-图中的表达式，这将是等价的模重排或分区。在将结果R与其输入I统一之前，求解器可以使用逆变换来注释R，该逆变换对如何操纵R进行电影《亲爱的，我缩小了孩子们》（Honey I Shrunk the Kids）中的主角名叫萨林斯基博士。我们的工作缩小了CAD而不是孩子。我想找到更有利可图的R。Szalinski然后使用语法重写来传播和消除逆变换时，使用这样的结果出现的机会。总之，本文的贡献包括：• Szalinski是一个工具，它将一个平面CSG表达式作为输入，并在Caddy中合成一个较小的等效程序，Caddy是一种用映射和折叠运算符扩展CSG以表达重复的语言• 逆变换，一种新的技术，接口，ING简单而有效的结构发现求解器与E图。该技术不是CAD专用的，但对于重新排序CAD操作特别有用。• 案例研究将Szalinski与最近的网格反编译器[21]组合，以合成较小的CAD模型。• 一项大规模评估，展示了Szalinski在从流行的在线存储库下载的模型上的性能和可扩展性[35]。本文循序渐进，首先介绍了球童和一个运行的例子（第2）。 Szalinski主要是利用机会重新滚动loopsweek（第3节）。 由于网格解压缩器输出（C1）的变化，找到这样的机会是具有挑战性的，因此Szalinski使用E图来实现一个强大的CAD重写系统（第4节）。找到正确的CAD重新排序对于暴露高级结构（C2）至关重要，但由于AC匹配，仅重写很困难Szalinski中的求解器通过E-图传播有益的重新排序，通过统一的顺序不等价的表达式，用逆变换表示（第5节）。我们开发了一个包含65个CAD重写的库，并在3，000行Rust中使用原型Szalinski（第6节）。第7节展示了如何将Szalinski与现有的网格反编译器[21]组合在一起，从而在质量上提高可编辑性（见Szalinski核心盒E图球童求解器重写6分，球童编辑（差异）（长方体[140，30，4]）（折叠并合（列表（i8））（翻译[i2+10i+6，15，2]（差异（翻译（70152））（比额表（140304）（翻译（-0.5-0.5-0.5）（长方体（111）（并集（翻译）（6152）（比例（65.1964）（000）（比例（0.50.5771）（HexPrism（11）（翻译）（125152）（比例（2017.324）（000）（比例（0.50.5771）（HexPrism（11））（翻译）（102152）（比例（1815.5884）（000）（比例（0.50.5771）（HexPrism（11））（翻译（81152））（比例（1613.8564）（差异）（长方体[140，30，4]）（折叠并合（列表（i6））（翻译[20i+20，15，2]（旋转[0，0，45i]（长方体[12，12，4]）（差异）（长方体[140，30，4]）（折叠并合（列表（i8））（翻译[i2+10i+6，15，2]（差异）（长方体[140，30，4]）(Fold联盟（（翻译[i2+38i+6，15，2]（HexPrism [i+3，4]）制表（i4）（差异）（长方体[140，30，4]）（折叠并（列表（i10））（翻译[i2+10i+6，15，2]（HexPrism [（i+3）/2，4]）小平面法线000外环顶点9150顶点7.517.59644vertex7.517.59640endloop端面小平面法线000外环顶点7.517.59644顶点9150顶点9154endloop端面小平面法线000外环顶点4.517.59640顶点7.517.59644vertex4.517.59644endloop端面…3D打印网格反编译器等饱和反变换综合结构化CAD模型PLDI33图1），并描述了对Szalinski在从Thingiverse下载的真实CAD模型上的性能和正确性的评估。第8节简要介绍了最相关的相关工作，第9节总结了这些工作。2Caddy和第二阶段反编译Caddy语言（图2）提供了类似于map和fold的函数列表操作符，CAD模型，以及一个核心球童片段，corre-直接发送给CSG。Caddy语义完全展开程序Szalinski则走了另一条路，将Core Caddy表达式分解为Caddy程序，目的是暴露潜在的重复结构。本节介绍了一个运行的示例，随后的章节将扩展该示例，以说明在从现有网格反编译器中缩减噪声、非结构化输出时出现的挑战2.1核心盒，盒，等同性核心球童包括各种图元参数化的尺寸-长方体参数化的边长，球体的半径，圆柱体和六棱柱的高度和半径等球童还提供了二进制2集理论运算符联盟，差异和交叉，仿射3transformation- tions喜欢平移，旋转和规模是参数化的3D矢量。例如，（Translate [1，0，0]（Sphere 2））将半径为2的球体沿x轴移动一个单位的距离。TranslateSpherical（在Core Caddy或CSG中不存在）捕获依赖于球面坐标而不是笛卡尔坐标中的平移的模型中的常见模式。图3给出了Caddy在Core Caddy之上提供的函数列表操作符的语义。Tabulate接受成对的变量和正整数（x1b1）.（x n b n）以及一个Caddy表达式e，并返回由n个嵌套循环对变量x1.. x n直到边界b1. b n：（名单 e[0/x1]. [0/x n]. . .e[b1− 1/x1]. [bn−1/xn]）其中e[i/x]表示用i替换e中x的所有自由出现（不受嵌套列表的约束）。比如说，（列表（i）） （二） （j） 第三章（长方体[2× i +2，7, j + 1]））（名单 （长方体[2， 7, 第1页]）（长方体[2，7, 第2节） （长方体[2，（第7、3段）（长方体[4， 7, 第1页]） （长方体[4，7, 第2节） （长方体[4，7、3]））对于（Tabulate（x n）e）的常见特殊情况，当x在e中不是自由的时，我们写（Repeatn e）作为语法糖。Map2通过将仿射运算符应用于变换参数列表和CAD参数列表来生成Core Caddy表达式列表。比如说，2我们使用语法糖来表示二元嵌套运算符，操作：：= +|--一种|×|/num：：=R|瓦鲁瓦|num|旋转|规模|平移球面双切口：：=联合|差异|路口cad：：=（长方体vec3）|（Spherenum）|（气缸体2）|（HexPrism vec2）|. . .| （仿射向量3）| （binopcadcad）| （Foldbinopcad-list）CAD列表 ：：=（List cad+）|（Concat目录-列表+）|（制表（var Z+）+cad）| （映射2仿射映射vec 3-list映射cad-list映射）vec3-list：：=（Listvec3+）|（Concat vec3-list+）|（制表（var Z+）+V3V3）图2. Caddy语法。Core Caddy（CSG）子集省略变量、列表表单（使用Fold的表单）和TranslateSpherical。e（Listv1. vn）f1=v1fi=（binopfi−1vi）(Foldbinope）briefne（List（Listv1，1v1，2.）(List一对二，一对二，二……）......）的情况。（Concate）（Listv1，1v1，2. 一对二，一对二，二……）e[i1/x1]. [in/xn] n = n（i1，. . . ，in）（列表（x1b1）. （xnbn）e）n（List v（0，. 、0）. v（b1 −1，. . . ，bn −1））ps（List [a1，b1，c1][a2，b2，c2].） es（Listv1v2.）（Map 2affine ps es）（List （仿射[a1，b1，c1] v1） （仿射[a2，b2，c2]v2）.）evto_carr（r，θ，θ）=（x，y，z）（TranslateSpherical[r，θ，θ]e）（Translate[x，y，z]v）图3. 大步骤语义将格式良好的Caddy程序减少到CoreCaddy表达式。e[i/x]表示用i替换e中x的所有自由出现。其他规则（未显示）也在List、affines和binops下进行评估。(Map2比例（列表【二、二、二】[3，3，3]）（重复2（球体1)))⇒（名单 （比例） 【二、二、二】（第一球） （比例）【三、三、三】（第1类））Caddy程序是等效的，只要它们评估为等效的CoreCaddy程序。通过设计，Core Caddy直接对应于CSG，其语义在先前的工作中给出[21，27，31]。第7节描述了通过评估Core Caddy的程序、将其编译为网格并比较Hausdorff距离来实际测试Caddy等效性。42.2缩小球童图4a显示了一个简单的CAD模型的船舶的车轮和图4b显示了相应的所需的左结合 超过 多 争论， 例如，在一个实施例中， （工会a b c）意味（联合（联合a b）c）。3这里仿射意味着平行线在变换后保持平行。等饱和反变换综合结构化CAD模型PLDI344非正式地说，如果两个网格上的每个点都靠近另一个网格上的某个点，则两个网格之间的Hausdorff距离很小。PLDIC.Nandi，M.Willsey，A.安德森，J。R. Wilcox，E.Darulova，D.Grossman，Z.塔特洛克35(a) 船舶车轮CAD模型（联合国（气缸[1，5]）（管接头（联合国（气缸[1，5，5]）（折叠接头（表一6）（旋转[0， 0， 60i]（翻译[1，-0。5、 0]（长方体[10， 1，1]）(b) 球童程序Binop折叠（binop c1c2.） （Foldbinop（Listc1c2...））结构发现（名单 （affp1c1）（affp2c2）.） （Map 2aff（Listp1p2.）(Listc1c2.））重复（名单 一个一个n次） （重复n a）列表求解（单循环）（List[fx（0），fy（0），fz（0）] ... [fx（n − 1），fy（n − 1），fz（n −1）]）[fx（i），fy（i），fz（i）]在地图2上重复（旋转[0，0，0]（翻译 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，60]（翻译 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，120]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，180]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，240]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，300]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]）(c) 公开结构（联合国（旋转[0，0，120]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（比例[10，1，1]（翻译 [0。1，-0。（长方体[1，1，1]）（旋转[0，0，300]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（刻度[5， 5， 1]（柱面[ 1， 1]））（翻译 [-1，0. 5、0] （刻度[−1，− 1， 1]长方体[ 10， 1， 1]）（旋转[0，0，240]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，60]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]）(d) 混淆结构的等效Core Caddy表达式图4. （a）船舶车轮的计算机辅助设计模型。（b）像Tabulate这样的球童功能表示重复的设计组件。这种重复在Core Caddy（c）中是显而易见的，但是现有的网格反编译器混淆了结构（d）。从Szalinski。图4b具体化了重复结构：对所有辐条进行更改只需要一次编辑，而不是在不同位置进行六次协调修改。当重复结构很容易暴露时，如图4c的理想核心盒中，求解器可以推断与重复设计组件的实例相关的算术函数。第3节描述了Szalinski的重写驱动的方法来推断这样的功能和缩小程序通过重新滚动循环。在实践中，给定表示图4a的网格，网格反编译器可以生成与图4c等效的CSG表达式，但是其混淆了重复结构。仿射变换可能不同或缺失，并且从求解器（地图2aff（重复np）（重复nc） 重复次数n（aff p c）在地图2上制表，其中b=bi(Map2 AFF（列表（x1b1）. p）的范围内 （列表（x1b1）. （c））（制表（x1b1）.（afp c））(Map2aff（Tabulate（x1b1）. p）（重复b和c））（制表（x1b1）.（afp c））(Map2aff（重复bp）（制表（x1b1）. （c））（制表（x1b1）.（afp c））图5. 用于循环重滚的3收缩球童通过重新滚动循环Szalinski收缩重复球童程序通过重新滚动循环。首先，通过分离仿射运算重写查找结构的参数和CAD参数中的地图2这可能会将程序重复暴露为重复列表。接下来，算术求解器为重复列表找到等价的闭合形式的表格这些表格概括了程序，并提供了简化未来编辑的参数。最后，通过将来自Map2s的（广义）仿射参数和CAD参数重新组合到单个Tabulate中来重写恢复结构。图5显示了该策略由于Szalinski使用了E图，这些重写实际上可以以任何顺序重复应用，并且仍然有效地产生相同的最终结果。为了简单起见，本节将逐步介绍轮船3.1寻找结构：鸟瞰将Binop Fold应用于图4c中的内接头，产生：分割。比较图4c和图4d，Rotate [0，0，180]被替换为等效的Scale [-1，-1，1]，恒等变换被省略，Union被重新排序，Scale和Translates被不一致地交换。（联盟）（联盟）（旋转[0，0，0]cad1）（Rotate[0， 0，60]cad2）（Rotate[0，0，120]cad3）.）（折叠联合（列表►（旋转[0，0，0]cad1）（Rotate[0， 0， 60]cad2）（Rotate[0，0，120]cad3）...））第4节和第5节逐步介绍了用于船舶车轮的Core Caddy输入的更多复杂变量，结构查找器（在第4节中详细描述）搜索所有使用相同运算符aff的仿射变换列表。结构查找将仿射参数和CAD参数分离到Map 2下的两个列表中，其中aff：等饱和反变换综合结构化CAD模型PLDI36(Fold联盟（列表（旋转[0，0，0]cad1）（Rotate[0， 0， 60]cad2）（Rotate[0，0，120]cad3）...））(Fold联盟►(Map2旋转（List [0，0，0][0，0，60][0，0，120]...）（名单 cad1cad2cad3.）理想的输入随后的部分将展示E图和逆变换如何使Szalinski能够鲁棒地收缩噪声和非结构化的CSG。4E-图与CAD等式饱和反复应用结构查找器。在这里它暴露了相同元素的列表，让Repeat重写产生：通过重滚循环来缩小Caddy的重写必须以正确的顺序应用于已经使结构化的程序(Fold联盟(Map2旋转（List[0，0，0] [0，0，60] [0，0，120]...） ▶(Map2翻译（名单 [1，-0。.）（名单 (Cube [10、1、1]）.）（折叠工会）(Map2旋转（List [0，0，0][0，0，60][0，0，120]...）(Map2翻译（重复6[1，-0。5、 0]）（重复6（Cube[10， 1， 1]）如图4C所示。简单地交错额外的CAD重写来暴露重复的结构最初似乎是不可行的，因为必要的重写是不融合的，并且可能的排序空间呈指数级爆炸然而，过去关于平等饱和的工作[34]证明了E图[22]如何使这种策略对许多人3.2通过求解列表引入制表一旦结构发现已经分离出一个向量列表，算法求解器试图找到等价 的列表。目前的给定n=（List[x1，y1，z1].[xn，yn，zn]），这些求解器分别为x，y，z分量推断独立函数fx，fy，fz在实践中，在现有网格反编译器输出的浮 点 数 上 运 行 算 术 求 解 器 需 要 在 一 定 范 围 内 接 受Tabulates，特别是对于依赖随机算法[11 ]的工具，如RANSAC [28]。对于“旋转”参数（列表[0，0，0] [0，0，60]. [0，0，300]），求解器找到（Tabulate（i6）[0，0，60i]）。列表求解然后产生：重写规则。本节显示Szalinski如何在CAD域中应用等饱和度，以在收缩Caddy程序时稳健地处理CSG变化。4.1 重写阶段排序：什么、何时、何地一个稍微扰动的Caddy示例，用于船[1，-1， 1]：(Fold联盟 （名单（翻译 [1，-0。5， 0]（Cube[ 10， 1， 1]））（旋转[0，0，60]（翻译[1，-0。5， 0]（Cube[ 10， 1， 1]））（旋转[0，0，120]（翻译[1，-0。5， 0]（Cube[ 10， 1， 1]））（比例）[-1，-1，1]（翻译 [1，-0。5， 0]（Cube[ 10， 1， 1]））（旋转[0，0，240]（翻译[1，-0。5， 0]（Cube[ 10， 1， 1]））（旋转[0，0，300]（翻译 [1，-0。5， 0]（Cube[ 10， 1， 1]）第3中的三相回路重滚策略(Fold联盟(Map2旋转（List[0，0，0] [0，0，60] [0，0，120]...） ▶(Map2翻译（重复6[1，-0。5、 0]）（重复6（Cube[10， 1， 1]）（折叠工会）(Map2旋转（Tabulate（i6）[ 0， 0，60i]）（映射2翻译（重复6[1，-0。5、 0]）（重复6（Cube[10， 1，1]）现在中断：Szalinski必须将其搜索与附加的CAD重写（图6）交错，以暴露如图4c中的重复仿射变换。这种阶段排序问题[34，38]使得难以确定何时应用哪些重写以及在何处应用。糟糕的选择只会进一步混淆重复的结构，没有单一的策略是最好的在本例中，求解器依赖于输入到达按照正确的顺序第5节展示了逆变换如何允许求解器重新排序其输入，以在保持等价性的同时推断出更好的表格3.3最后的挤压：隐藏Map2s最后，由于Repeats和Tabulate都具有匹配的边界，因此Repeat over Map 2和Tabulate over Map 2重新组合分离的仿射参数和CAD参数，以从图4c的内部Union产生所需的输出：梗概.相等饱和[34]是一种减轻相位排序的技术，它使用E图来在大量表达式上复杂地表示等价关系。重写不是破坏性地修改特定的具体术语，而是通过添加和统一ex-graph类来扩展E-graph。这消除了选择任何特定重写顺序的需要。通过将图5和图6中的规则重复应用于E图并使用结构发现启发式（第4.4），Szalinski(Fold联盟(Map2旋转轴（表（i 6）[0， 0， 60i]）(Map2翻译（重复6[1，-0。5、 0]）（重复6（Cube[10， 1， 1]）（折叠工会）（表一6）（旋转[0， 0， 60i]（翻译 [1，-0。5、 0]（Cube[10， 1， 1]）仿射算子的大小4.2E-graph背景一个E-图是一个类的集合，每个类是一个等价结点的集合。enode是一个运算符（Translate，Union，本节说明了Szalinski的核心策略：通过重新滚动循环来缩小Caddy。然而，该示例依赖于特定的重写顺序，图4c是不切实际的文字等）适用于零个或多个子类。一个类c表示表达式e，如果c包含一个与e具有相同运算符的enoden，并且n的孩子表示e的孩子。PLDIC.Nandi，M.Willsey，A.安德森，J。R. Wilcox，E.Darulova，D.Grossman，Z.塔特洛克37[1，-0.5，0]反式[-1，-1，1][1，-0.5，0]仿射恒等式（Rotate[0， 0， 180]cad）缩放 （Scale[− 1，− 1，1]cad）（Rotate[0， 0， 0]cad）旋转cad（Translate[0， 0， 0]cad）cad（Scale[1，1，1]cad）缩放cad仿射互换def Szalinski（csg：core_caddy）：egraph，root = make_egraph（csg）whileegraph.changed（）for（lhs，rhs）inSZALINSKI_REWRITES：matches = egraph.search（lhs）for（eclass，subst）inmatches：c = egraph.add（apply（rhs，subst））（比例表[a，b，c]（翻译 [d，e，f]CAD））仿射组合（比例表[a，b，c]（Scale[d，e，f]cad））（Translate[a，b，c]（翻译 [d，e，f]CAD））翻译 [ad，be，cf]（比例[a，b，c]cad））（Scale [ad，be，cf]cad）翻译 [a+d，b+e，c+f]cad）egraph.unify（eclass，c）returnegraph.extract（root，min_size）图8. Szalinski中球童的相等饱和度基元-仿射转换（长方体[x，y，z]）↭（比例[x，y，z]（长方体[1，1，1]））（球面r）↭（比例[r，r，r]（球体1））（气缸[h，r]）↭（比例） [r，r，h]（柱面[1，1]））（六棱柱[h，r]）↭（比例） [r，r，h]（六棱柱[1，1]）图6. 选定的CAD标识。双向箭头指示Szalinski对每个方向都有一个规则。包含具有等效子节点的n + n个节点。图7显示了一个E图如何能够复杂地表示重写所生成的等效表达式，在本例中，是暴露船轮示例的重复结构所需的CAD重写之一E-图可以很容易地通过语法重写来扩展ab：每当一个类c表示一个表达式，该表达式在替换下与模式a匹配时，表示（b）的类被找到（或构造）并与c统一;得到的类将表示表达式（a）和（b）。（比例）[-1，-1， 1]（翻译[1，-0。5、 0]（Cube[10， 1，1]））[-1，-1，1]规模（旋转[0， 0， 180]►（翻译[1，-0。5、 0]（Cube[10， 1，1]））重写只会扩展E图，所有以前的表达式仍然被表示。我们稍微将重写从两个模式推广到一个模式L和一个函数R，给定一个替换函数R，返回一个要添加到E-图的表达式，并与匹配L的类统一。这种泛化允许重写实现不纯粹语法的规则，如常量折叠（例如：重写2+ 3到5）。Sza- linski的许多列表操作重写都是以这种方式实现的，这对于像Repeat这样需要执行的图7.CAD重写前后的电子图。包装盒代表-重新发送的节点和虚线边缘表示等价（在同一类中的优先级）。定向实体边将节点连接到它们的子类。原始程序和变换后的程序都表示在生成的E图中。每个类表示指数数量的等价表达式（w.r.t.节点的数量），因为它的每个节点都指向类本身。将表达式添加到E图中是自下而上的：首先将叶子作为节点添加到它们自己的类中，然后递归地添加操作符作 为 节 点 ， 指 向 它 们 的 操 作 数 的 类 作 为 子 类 。Hashconsing确保节点在E图中永远不会重复。这个共享压缩表示许多等价的表达式。E-图还提供了一个统一的操作，结合两个eclasses和维护他们的同余闭包。例如，如果类c1和c2表示（+xy）和（+xz）的关系，那么统一表示y和z的类将导致c1和c2也被统一，因为它们都跟踪匹配列表模式的长度。这种泛化也允许Szalinski将算术求解器与E-graphic集成，由求解器返回的表格表达式与匹配List Solve规则4.3Szalinski中的等式饱和Szalinski为Caddy实现了等式饱和[34]（图8）。首先，从输入Core Caddy表达式创建E图然后Szalinski通过重复地应用重写来扩展E-图。在E图中搜索重写的左侧模式会得到一个（类，替换）对列表，该列表对于每一对（c，c ′），Szalinski通过将重写的右侧函数应用于c ′，将e添加到E-图中产生e类c ′，并统一c和c ′来生成表达式eSzalinski继续应用重写，直到E图饱和（达到不重写进一步扩展E图的固定点），或者达到超时。在饱和的情况下，Szalinski已经发现了所有的等价推导从它的重写。立方体反式立方体【0，0，180】规模旋转等饱和反变换综合结构化CAD模型PLDI38最后，Szalinski提取最小的Caddy程序表示的初始核心Caddy输入的类在一个简单的自下而上遍历的E图。Szalinski使用程序大小作为可编辑性的代理。过去的工作提供了各种成本函数的提取策略[24，34]，但我们将Szalinski中CAD成本函数的进一步探索留给未来的工作。4.4E-图的结构发现由于Szalinski必须考虑CAD恒等式可能在同一类中引入多个给定类e1，e2，.的列表，例如，结构查找器旨在提取去除一个结构级别的Map 2。然而，由于来自图6的仿射组合的规则，每个类可以包含具有相同仿射操作的多个等效节点。例如，如果eclassei有2个带有Rotate操作符的节点，那么结构查找器可以在列表中的n个eclass中的每一个上从2个不同的Rotates这2n个Map2中的每一个都有不同的子节点，因此在E图中是一个不同的enode，所有这些都统一在与列表本身相同的eclassSzalinski必须在Core Caddy程序的大列表上操作，但是这样一个指数数量的节点会炸毁E图。相反，Szalinski利用了这样的观察：在看起来相似的类中挑选不同的仿射节点是没有用的再考虑一下4.1节中提到的轮船在应用图6中的两个Rotate恒等式之后，列表中的顶级仿射的eclass包含以下节点（每行一个eclass，为了清楚起见，节点与它们的参数一起显示）：答：（平移[1，-0.5，0]x1）（旋转[0，0，0]a）B组：（旋转[0，0，60]x2）（旋转[0，0，0]b）c：（Rotate [0，0，120]x3）（Rotate [0，0，0]c）d：（缩放[-1，-1，1]x4）（旋转[0，0，0]d）（旋转[0，0，180]x4）e：（Rotate [0，0，240]x5）（Rotate [0，0，0]e）F级：（Rotate [0，0，300]x6）（Rotate [0，0，0]f）结构发现器计算每个类的仿射签名在上面的例子中，类a{Translate，Rotate}，d群是共享相同仿射签名的类的集合。当试图提取 旋转时，结构查找器将不会在每个eclassertion中获取旋转的笛卡尔积，这样做将导致25种可能的方法来组合旋转。相反，它取每个群的仿射选择的笛卡尔积，并将相同的仿射选择扩展到群内的所有类在这个例子中，唯一可以提取的仿射是旋转，因为（折叠联合（列表（旋转[0，0，120]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，0]（翻译 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，300]（平移[1，− 0. 5， 0]（长方体[ 10， 1， 1]））（气缸[1， 5]）（旋转[0，0，180]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，240]（平移 [1，-0。5， 0]（长方体[ 10， 1， 1]））（旋转[0，0，60]（翻译 [1，-0。5， 0]（长方体[ 10， 1， 1]）图9. 第3节和第4节技术从真实的图4d中找到了“旋转然后平移”的结构。如果没有逆变换，循环重滚现在会卡住。d组有2个选择，b，c，e，f组也有2个选择。这将减少（贴图2旋转...）从25= 32到4引入的表达式5逆变换E图和CAD重写允许Szalinski暴露重复结构和重滚循环，即使当Core Caddy输入表现出混淆变化（例如，缩放[-1，-1，1]而不是旋转[0，0，180]）。然而，现有的网格反编译器也倾向于通过几何接近度或其他算法对CAD子表达式进行排序和除非能找到子表达式的正确重新排序和重新分组，否则列表求解器将无法推断出列表，Szalinski将无法重新滚动循环并缩小Caddy程序。为了解决这一挑战，我们引入了逆变换，一种新的方式，求解器乐观地统一在E-图，这将是等效的模重新排序或重新分组的ex-principle。图9显示了对于图4d示例，CAD重写与前面部分的技术相结合的程度不幸的是，圆柱体仍然与长方体结合，防止结构查找器拉出旋转。即使移除了“圆柱体”，列表顺序也会阻止解算器推断“旋转”参数的“制表”与前一节不同，添加更多重写并没有帮助。5E-图并不完全表示等价，这是由于对结合算子和交换算子（如Union）进行了重新排序。这被称为AC匹配问题[3]（A代表结合性，C代表交换性），它阻止了有效地探索所有可能的重新排序和重新分组。Szalinski用一种新的技术--逆变换来解决这个问题，它允许求解器推测性地变换他们的输入，以允许更有利可图的重写。对于某些变换F，不能简化输入A的求解器可以将F（A）简化为B。逆变换只是允许求解器在用A统一B之前用F−1对B进行反包，即使A和B不等价。其他仿射不出现在所有的仿射签名组对于旋转仿射，组a有一个选择，组5我们可以报告AC匹配在理论和实践中都是一个问题。PLDIC.Nandi，M.Willsey，A.安德森，J。R. Wilcox，E.Darulova，D.Grossman，Z.塔特洛克39permutation：：= n，n，.n =n，n，. ⟩inv：：=（Sortpermutation *-list）|（Unsort permutation*-list）|（Part III分区计划大纲*-一览表 A）|（Unpartpartitioning*-list）| （球面球坐标3球坐标3-列表）| （非球面矢量3-列表矢量3）图10. 扩展的Caddy。逆变换使局部推理求解器能够在E图中注册潜在的有利可图的重新分组和重新排序。简单的语法重写，然后通过E图全局地传播这些提示，e（Listv1v2. vn）(Sorti1，i2，.