Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi Max Willsey Adam Anderson James R. Wilcox Eva Darulova Dan Grossman Zachary Tatlock



]Synthesizing Structured CAD Models with 
 Equality Saturation and Inverse Transformations



                                        
                                        


                                        
                                        













































  University of Washington            
  USA                    

cnandi@cs.washington.edu          


  University of Washington            
  USA                    

mwillsey@cs.washington.edu          


  University of Washington            
  USA                    

adamand2@cs.washington.edu          


  Certora            
  USA                    

james@certora.com          


  MPI-SWS            
  Germany                    

eva@mpi-sws.org          


  University of Washington            
  USA                    

djg@cs.washington.edu          


  University of Washington            
  USA                    

ztatlock@cs.washington.edu          









  Recent program synthesis techniques
  help users customize CAD models (e.g., for 3D printing)
  by decompiling low-level triangle meshes to
  Constructive Solid Geometry (CSG) expressions.
Without loops or functions,
  editing CSG can require
  many coordinated changes,
  and existing mesh decompilers use heuristics that
  can obfuscate high-level structure.

This paper proposes a second decompilation stage
  to robustly “shrink” unstructured CSG expressions
  into more editable programs with map and fold operators.
We present ,
  a tool that uses Equality Saturation 
  with semantics-preserving CAD rewrites
  to efficiently search for smaller equivalent programs.
relies on ,
  a novel way for solvers to speculatively add
  equivalences to an .
We qualitatively evaluate in case studies,
  show how it composes with an
  existing mesh decompiler, and
  demonstrate that can shrink
  large models in seconds.






















































































































  






[
    Zachary Tatlock
    December 30, 2023
=====================



grammar



§ INTRODUCTION






The programming languages and machine learning communities
  have developed techniques to
  decompile Computer-Aided Design (CAD) models from
  low-level numerical representations to
  Constructive Solid Geometry (CSG) expressions <cit.>.
These techniques aim to help users
  modify designs shared in online repositories <cit.>.

Recent program synthesis results <cit.>
  decompile meshes,

  sets of triangles defining an object's surface,
  into equivalent CSG expressions.
CSG includes
  geometric primitives like cylinders,
  affine transformations like translate,
  and set theoretic operators like union.






Existing mesh decompilers
  synthesize flat output:
  CSG has no loops or functions (<ref>, left).
Therefore, CSG synthesized from
  large meshes with repetitive features
  also tends to be large and repetitive.
As in traditional programming,
  repetition makes otherwise intuitive edits
  tedious and error-prone.



Mesh decompilation is under-constrained <cit.>, so
  past tools rely on heuristics which cause them to
  exhibit two challenging features:
  synthesize equivalent but dissimilar CSG expressions for
  the same feature repeated under different transformations, and
  arbitrarily order CSG subexpressions. These two
features, and obfuscate
  high-level structure latent in synthesized CSG.

This paper proposes a second decompilation stage
  that composes with prior work:
  given a flat CSG expression,
  produce an equivalent, smaller, and more editable program
  with map and fold operators for expressing repetition.
We present [The protagonist in the hit movie Honey I Shrunk the Kids was named Dr. Szalinski. Our work shrinks CADs rather than kids.]
(<ref>),
  a tool which combines semantics-preserving rewrites
  with simple solvers to
  synthesize structured CAD programs
  in a language called .

is designed to robustly handle the
  noisy and unstructured outputs of
  existing mesh decompilers.
In many of these outputs,
  high-level structure is only apparent after
  a set of CAD-specific rewrites
  have been judiciously applied .
Past work on Equality Saturation <cit.>
  suggests that Equality Graphs () <cit.>—an
  efficient data structure underlying SMT solvers <cit.>
  and program optimizers <cit.>—would
  make a good fit for because can compactly encode many of the
  equivalent ways to express a program
  with respect to a set of rewrites.


Unfortunately,
  reordering with associative and commutative rewrites
  can cause to blow up exponentially.
This is known as the
AC-matching problem <cit.>.
It presents a significant challenge for because
  existing mesh decompilers typically output CSG features
  ordered by heuristics (e.g., geometric proximity)
  rather than high-level structure .

To address the AC-matching problem in we present ,
  a novel way for solvers to
  speculatively unify
  expressions in an which would be equivalent modulo
  reordering or partitioning.
Before unifying a result R with its input I,
  a solver can annotate R with an which encodes
  how it manipulated I to find
  the more-profitable R.
then uses syntactic rewrites to
  propagate and eliminate when opportunities to use such results arise.

To summarize, the contributions of this paper include:


  * , a tool that takes
  a flat CSG expression as input and synthesizes
  a smaller equivalent program in
  , a language that extends CSG with
  map and fold operators for expressing repetition.


  * , a new technique for
    interfacing simple-yet-effective
    structure finding solvers with .
  The technique is not CAD-specific,
    but is particularly useful for
    reordering CAD operations.



  * A case study composing with a
  recent mesh decompiler <cit.>
  to synthesize smaller CAD models.


  * A large scale evaluation demonstrating
  the performance and scalability of on models downloaded from a popular online
    repository <cit.>.














This paper proceeds gradually,
  first introducing and a
  running example (<ref>).
primarily exploits opportunities
  to “reroll loops” (<ref>).
Finding such opportunities
  is challenging due to variations in
  mesh decompiler output ,
so uses to
  implement a robust
  CAD rewrite system (<ref>).
Finding the right CAD reordering is
  crucial to expose high-level structure ,
  but difficult with rewrites alone
  due to AC-matching.
Solvers in propagate profitable reorderings
  through the by unifying order-inequivalent
  expressions annotated with
  (<ref>).

We developed a library of
  CAD rewrites
  and prototyped in
  lines of Rust
  (<ref>).
<ref> shows how composing
  with an existing mesh decompiler <cit.>
  qualitatively improves editability
  (sketched in <ref>)
  and describes an evaluation of
  's performance and correctness
  on real-world CAD models
  downloaded from Thingiverse.
<ref> briefly surveys the
  most relevant related work and
  <ref> concludes.

























































































































































































































































































































































































































§ AND SECOND STAGE DECOMPILATION





The  language (<ref>) provides
  map- and fold-like functional list operators to express
  repetitive structure in CAD models,
  as well as a Core  fragment that
  corresponds directly to CSG.
The semantics
  fully unroll a program's functional list operators
  to produce a Core (CSG) expression.
“goes the other way,”
  decompiling a Core Caddy expression to
  a Caddy program that aims to
  expose latent repetitive structure.
This section introduces a running example
  that subsequent sections extend
  to illustrate challenges that arise when
  shrinking noisy, unstructured outputs
  from existing mesh decompilers.



 §.§ Core Caddy, Caddy, Equivalence



Core includes various primitives parametrized by dimensions—
  cuboids parametrized by side length,
  spheres by radius,
  cylinders and hexagonal prisms by height and radius,
  .
also provides binary[
    We use syntactic sugar to present binary nested operators as
    left-associative over multiple arguments, e.g.,
    (Union a b c) means (Union (Union a b) c).]
  set theoretic operators
  Union, Difference, and Intersection, and
affine transformations
  like Translate, Rotate, and Scale that
  are parameterized by 3D vectors.
For example, (Translate [1,0,0] (Sphere 2))
  shifts a sphere with radius 2
  a single unit of distance along the x-axis.
TranslateSpherical (not present in Core Caddy or CSG)
  captures a common pattern in models relying on translations in
  spherical rather than Cartesian coordinates.

  Here affine means that parallel lines remain
  parallel after transformation.













<ref> gives semantics
  for the functional list operators provides on top of Core .
takes pairs of variables and positive integers
  (x_1   b_1)  ...  (x_n   b_n)
  as well as a expression e, and
  returns the list of length Π b_i generated by
  n nested loops evaluating e
  over the variables x_1  ...  x_n up to
  the bounds b_1  ...  b_n:
  
    (  ex_10...x_n0  …  ex_1b_1 - 1...x_nb_n - 1)

  where exi denotes
  substituting all free occurrences
  (not bound by nested ) of
  x in e with i.
For example,
[xleftmargin=0em]
(Tabulate (i 2) (j 3) (Cuboid [2 × i + 2, 7, j + 1])) ⇒
    (List (Cuboid [2, 7, 1]) (Cuboid [2, 7, 2]) (Cuboid [2, 7, 3])
          (Cuboid [4, 7, 1]) (Cuboid [4, 7, 2]) (Cuboid [4, 7, 3]))

For the frequent special case of
  ((x n) e) when
  x is not free in e,
  we write (n e) as syntactic sugar.





























produces a list of Core expressions by
  applying an affine operator to a
  list of transformation parameters and a
  list of CAD arguments.
For example,

[xleftmargin=1em]
(Map2 Scale (List [2,2,2] [3,3,3]) (Repeat 2 (Sphere 1))) ⇒
    (List (Scale [2,2,2] (Sphere 1)) (Scale [3,3,3] (Sphere 1)))









programs are equivalent iff they evaluate to
  equivalent Core programs.
By design, Core directly corresponds to CSG,
  whose semantics is given in prior work <cit.>.
<ref> describes practically testing equivalence by
  evaluating programs to Core , compiling them to meshes,
  and comparing Hausdorff distances.[Informally,
    the Hausdorff distance between two meshes is small if
    every point on each mesh is near some point on the other.]










 §.§ A Running Example for Shrinking Caddy











<ref> shows a
  simple CAD model of a ship's wheel and
  <ref> shows the
  corresponding desired output from .
<ref> reifies repetitive structure:
  making a change to all the spokes
  only requires a single edit instead of
  six coordinated modifications in different locations.

When repetitive structure is easily exposed,
  as in the ideal Core of <ref>,





  solvers can infer the
  arithmetic function relating instances
  of repeated design components.
<ref> describes
  's rewrite-driven approach to
  infer such functions and shrink programs
  by rerolling loops.





In practice,
  given a mesh representing <ref>,
  mesh decompilers can generate CSG expressions
  equivalent to <ref>, but
  which obfuscate repetitive structure.

Affine transformations may be different or missing and,
  from a solver's perspective,
  lists may be inconveniently ordered or partitioned.
Comparing Figure <ref> to <ref>,
  Rotate [0,0,180] has been replaced with
  an equivalent Scale [-1,-1,1],
  identity transformations have been omitted,
  the Union has been reordered,
  and Scales and Translates have been inconsistently swapped.
Sections <ref> and <ref>
  walk through progressively more challenging variants of
  Core inputs for the ship's wheel to illustrate
  how uses and to robustly handle such variation.





§ SHRINKING BY REROLLING LOOPS




shrinks repetitive programs
  by “rerolling loops”.



First, rewrites find structure by
  separating affine operators from
  their parameters and CAD arguments under .
This can expose program repetition as
  repetitive .



Next, arithmetic solvers find
  equivalent closed form for repetitive lists.
These generalize the program
  and provide parameters that simplify future edits.

Finally, rewrites restore structure
  by recombining the (generalized)
  affine parameters and CAD arguments
  from into a single .
<ref> shows this strategy's key rewrites.







Because uses an ,
  these rewrites can actually be repeatedly applied in any order
  and still efficiently yield the same final result.
For simplicity,
  this section steps through the ship's wheel
  example assuming a particular fortuitous order of rewrites
  that just so happens to nicely shrink the
  ideal Core input from <ref>.




















 §.§ Finding Structure: A Bird's-eye View










Applying Binop Fold to the
inner in <ref> produces:

[t]0.4
    [style=rewrite]
    (Union (Union (Union ...
     (Rotate |[0,0,0]|   𝑐𝑎𝑑_1)
     (Rotate |[0,0,60]|  𝑐𝑎𝑑_2)
     (Rotate |[0,0,120]| 𝑐𝑎𝑑_3) ...)
    

[t]0.1
  
    ▸


[t]0.4
    [style=rewrite]
    (Fold Union (List
     (Rotate |[0,0,0]|   𝑐𝑎𝑑_1)
     (Rotate |[0,0,60]|  𝑐𝑎𝑑_2)
     (Rotate |[0,0,120]| 𝑐𝑎𝑑_3) ...))
    





A structure finder
  (detailed in <ref>)
  searches for a list of affine transformations
  all using the same operator 𝑎𝑓𝑓.
Structure Finding separates the
  affine parameters and CAD arguments out into
  two under a with 𝑎𝑓𝑓:

[t]0.4
    [style=rewrite]
    (Fold Union (List
     (Rotate |[0,0,0]|   𝑐𝑎𝑑_1)
     (Rotate |[0,0,60]|  𝑐𝑎𝑑_2)
     (Rotate |[0,0,120]| 𝑐𝑎𝑑_3) ...))
    

[t]0.1
  
    ▸


[t]0.45
    [style=rewrite]
    (Fold Union
     (Map2 Rotate
      (List [0,0,0] [0,0,60] [0,0,120] ...)
      (List 𝑐𝑎𝑑_1 𝑐𝑎𝑑_2 𝑐𝑎𝑑_3 ...)))
    





The structure finder is applied repeatedly.
Here it exposes lists of identical elements,
  letting the Repeat rewrite produce:

[t]0.45
[basicstyle=]
(Fold Union
 (Map2 Rotate
  (List [0,0,0] [0,0,60] [0,0,120] ...)
  (Map2 Translate
   (List [1,-0.5,0] ...)
   (List (Cube [10,1,1]) ...))))


[t]0.1
  
    ▸


[t]0.45
[basicstyle=]
(Fold Union
 (Map2 Rotate
  (List [0,0,0] [0,0,60] [0,0,120] ...)
  (Map2 Translate
   (Repeat 6 [1,-0.5,0])
   (Repeat 6 (Cube [10,1,1])))))






 §.§ Introducing by Solving Lists



Once structure finding has
  isolated a of vectors ℓ,
  arithmetic solvers attempt to find
  equivalent .
The current prototype
  provides simple solvers for
  first- and second-degree polynomials in both
  Cartesian and spherical coordinates.
Given ℓ = (  [x_1, y_1, z_1]   ...   [x_n, y_n, z_n]),
  these solvers infer independent functions
  f_x, f_y, f_z for the
  x, y, z components of ℓ respectively.



In practice,
  running arithmetic solvers on
  floating point numbers output by
  existing mesh decompilers requires
  accepting within some ϵ of ℓ,
  especially for tools that rely on
  randomized algorithms <cit.>
  like RANSAC <cit.>.


For the Rotate parameters (  [0,0,0]   [0,0,60]   ...   [0,0,300]),
  solvers find (Tabulate (i   6) [0, 0, 60i]).
List Solve then produces:

[t]0.45
[basicstyle=]
(Fold Union
 (Map2 Rotate
  (List [0,0,0] [0,0,60] [0,0,120] ...)
  (Map2 Translate
   (Repeat 6 [1,-0.5,0])
   (Repeat 6 (Cube [10,1,1])))))


[t]0.1
  
    ▸


[t]0.45
[basicstyle=]
(Fold Union
 (Map2 Rotate
  (Tabulate (i   6) [0, 0, 60i])
  (Map2 Translate
   (Repeat 6 [1,-0.5,0])
   (Repeat 6 (Cube [10,1,1])))))






In this example,
  the solvers relied on their input
  arriving in just the right order.
<ref> shows how allow
  solvers to reorder their input
  to infer better while preserving equivalence.
























































 §.§ The Final Squeeze: Recombining 



Finally,
  since both the and have matching bounds,
  Repeat over Map2 and
  Tabulate over Map2 recombine the
  separated affine parameters and CAD arguments
  to produce the desired output from
  the inner of <ref>:

[t]0.4
    [style=rewrite]
    (Fold Union
     (Map2 Rotate
      (Tabulate (i 6) [0,0,60i])
       (Map2 Translate
        (Repeat 6 [1,-0.5,0])
        (Repeat 6 (Cube [10,1,1])))))
    

[t]0.1
  
    ▸


[t]0.45
    [style=rewrite]
    (Fold Union
     (Tabulate (i 6)
      (Rotate [0,0,60i]
       (Translate [1,-0.5,0]
        (Cube [10,1,1])))))
    





This section illustrated 's core strategy:
  shrinking by rerolling loops.
However, the example relied on a
  specific rewrite order and
  <ref> as an
  unrealistically ideal input.
Subsequent sections show how
  and enable
  to robustly shrink
  noisy and unstructured CSGs.


















§ AND CAD EQUALITY SATURATION






Rewrites to shrink by rerolling loops
  must be applied in just the right order
  to programs that already make structure apparent
  as in <ref>.
Simply interleaving additional CAD rewrites to
  expose repetitive structure

  initially seems infeasible because
  the necessary rewrites are not confluent



  and the space of possible orderings explodes exponentially.
However, past work on Equality Saturation <cit.>
  demonstrates how  <cit.> can make this strategy
  efficient for many rewrite rules.
This section shows how applies
  Equality Saturation in the CAD domain
  to robustly handle CSG variations
  when shrinking programs.














 §.§ Rewrite Phase Ordering: What, When, Where
 


A slightly perturbed example for
  the spokes of the ship's wheel
  omits Rotate [0,0,0] and
  replaces Rotate [0,0,180] by the equivalent
  Scale [-1,-1,1]:





[basicstyle=]
(Fold Union  (List
  (Translate |[1,-0.5,0]| (Cube |[10,1,1]|))
  (Rotate |[0,0,60]|   (Translate |[1,-0.5,0]| (Cube |[10,1,1]|)))
  (Rotate |[0,0,120]|  (Translate |[1,-0.5,0]| (Cube |[10,1,1]|)))
  (Scale  |[-1,-1,1]| (Translate |[1,-0.5,0]| (Cube |[10,1,1]|)))
  (Rotate |[0,0,240]|  (Translate |[1,-0.5,0]| (Cube |[10,1,1]|)))
  (Rotate |[0,0,300]|  (Translate |[1,-0.5,0]| (Cube |[10,1,1]|)))))


The three-phase loop rerolling strategy
  from <ref> now breaks:
  must interleave its search
  with additional CAD rewrites (<ref>)
  to expose the repeated affine transformations
  as in <ref>.
This phase ordering problem <cit.>
  makes it difficult to determine
  when to apply which rewrites and where.
Poor choices will only further obfuscate repetitive structure
  and no single strategy is best in general.





















Equality Saturation <cit.> is a technique to
  mitigate phase ordering that uses
  to compactly represent equivalence relations
  over large sets of expressions.
Instead of destructively modifying a particular concrete term,
  rewrites extend the by
  adding and unifying classes of expressions.
This eliminates the need to choose any
  particular rewrite ordering.

By repeatedly applying the rules in
  Figures <ref> and <ref> to an and using a structure finding heuristic (<ref>),
  's loop rerolling strategy can robustly handle
  variations in how mesh decompilers synthesize affine operators.








 §.§ Background





An is a set of , and
each is a set of equivalent .
An is an operator (, , literal, )
  applied to zero or more child .
An c represents expression e if
  c contains an n
  with the same operator as e and
  the children of n represent
  the children of e.
Each represents an exponential number of
  equivalent expressions (w.r.t. the number of ),
  since each of its point to themselves.

Adding an expression to an works bottom up:
  first add the leaves as each in their own ,
  then recursively add operators as pointing to
  the of their operands as children.
Hashconsing ensures are
  never duplicated in an .


This sharing compactly represents many
  equivalent expressions.

also provide a unify operation that
  combines two and
  maintains their congruence closure.
For example,
  if c_1 and c_2 represent
  (+ x y) and (+ x z) respectively,
  then unifying the representing y and z
  would cause c_1 and c_2 to be unified as well
  since they both contain “+” enodes with
  equivalent children.
<ref> shows how an
  can compactly represent equivalent expressions
  generated by rewrites, in this case,
  one of the CAD rewrites needed to expose
  repetitive structure for the ship's wheel example.











can easily be extended with
  syntactic rewrites a  b:
  whenever an c represents
  an expression that matches pattern a under substitution ϕ,
  the representing ϕ(b) is found (or constructed)
  and unified with c;
  the resulting eclass will represent both
  expressions ϕ(a) and ϕ(b).
Rewrites only expand the ,
  all previous expressions are still represented.

We slightly generalize rewrites
  from two patterns to
  a pattern L and a function R that,
  given a substitution ϕ,
  returns an expression to be added to the
  and unified with the
  that matched L.
This generalization allows rewrites to implement
  rules which are not purely syntactic,
  like constant folding
  (ex: rewriting 2 + 3 to 5).
Many of 's list-manipulating rewrites
  are implemented this way,
  which is convenient for rules like
  Repeat which need to extract
  the length of a matched list pattern.
This generalization also allows to
  integrate arithmetic solvers with the
  —expressions returned by
  solvers are unified with the that
  matched the List Solve
  rule's list pattern.










 §.§ Equality Saturation in 


implements Equality Saturation <cit.>
  for (<ref>).
First, an is created from the input
  Core expression.



Then expands the by
  repeatedly applying rewrites.
Searching the for a
  rewrite's left-hand side pattern results in
  a list of (, substitution) pairs that
  indicate where and how a pattern was matched.
For each pair (c, ϕ),
  generates an expression e by
    applying the rewrite's right-hand side function to ϕ,
  adding e to the yielding c', and
  unifying c and c'.
continues applying rewrites until
  the saturates
  (reaches a fixpoint where no rewrites further expand the ),
  or a timeout is reached.
In the case of saturation,
  has discovered all equivalences
  derivable from its rewrites.






Finally, extracts the smallest
  program represented by the
  initial Core input's in a simple
  bottom-up traversal of the .
uses program size as a proxy for editability.

Past work provides extraction strategies for
  various kinds of cost functions <cit.>,
  but we leave further exploration of CAD cost functions
  in to future work.


















 §.§ Structure Finding in 



Since 's rewrites contain CAD identities that
can fire in every iteration,
the structure finding procedure as
presented in <ref> must be
  enhanced.
It must consider that multiple affine transformations
  may be introduced in the same by the CAD identities.
Given a list of e_1,e_2,...,e_n, the structure finder aims to
  extract Map2s that remove one level of structure.
However, due to rules like Affine Combination from
  <ref>, each eclass may contain multiple equivalent
  enodes with the same affine operation.
If e_i has 2 with the operator, for example,
  the structure finder can choose from 2 different Rotates at
  each of the n in the list.
Each of these 2^n Map2s has
  distinct children, and will therefore be a distinct in the
  , all unified in the same as the list itself.
must operate on large lists of Core programs,
  but such an exponential number of would blow up the .



instead capitalizes on the observation that it is not useful
  to pick different affine enodes within similar-looking eclasses.
Consider again the ship's wheel example presented in
  <ref>.
After applying the two identities from <ref>,
  the for the top-level affines in the list contain the following
  enodes (one per row, shown with their parameters for clarity):





a:     ( [1,-0.5,0] x_1)     ( [0,0,0] a)     

b:     ( [0,0,60] x_2)     ( [0,0,0] b)     

c:     ( [0,0,120] x_3)      ( [0,0,0] c)     

d:     ( [-1,-1,1] x_4)      ( [0,0,0] d)     ( [0,0,180] x_4) 

e:     ( [0,0,240] x_5)     ( [0,0,0] e)     

f:     ( [0,0,300] x_6)     ( [0,0,0] f)    






The structure finder calculates the affine signature of each
  as the multiset of the kinds affine operators in the .
In the above example,
  a's affine signature is {, },
  d's is {, , },
  and the others all share the same signature: {, }.
  
  
A group is a set of that
  share the same affine signature.
When trying to extract a , the structure finder
  will not take the Cartesian product of the Rotates in each
  —doing so would lead to 2^5 possible ways to combine .



Instead, it takes the Cartesian product of affine choices for each
  group, and extends the same choice of affine over
  all within the group
  (using the order of affines in the ).
In this example, the only affine that can be extracted is ,
  since the other affines do not appear in the affine signature of all groups.
For the affine,
  group a has one choice,
  group d has 2 choices, and
  group b, c, e, f also has 2 choices.




This reduces the number of (Map2 Rotate ...)
  expressions introduced from
  2^5 = 32 to 4.
  
  





















































































§ 



and CAD rewrites allow to
  expose repetitive structure and reroll loops
  even when a Core input
  exhibits obfuscating variations
  (e.g., Scale [-1,-1,1] instead of Rotate [0,0,180]).
However, existing mesh decompilers tend to also
  order and group CAD subexpressions
  by geometric proximity or other heuristics that,
  from 's perspective,
  make recovering high-level structure challenging.
Unless the right reordering and regrouping of subexpressions
  can be found, list solvers will
  fail to infer and will be unable to reroll loops and shrink programs.

To address this challenge,
  we introduce ,
  a novel way for solvers to optimistically
  unify expressions in an that
  would be equivalent modulo reordering or regrouping.























<ref> shows
  how far CAD rewrites combined with techniques from
  previous sections get for the <ref> example.
Unfortunately, is still
  Unioned with Cuboids,
  preventing the structure finder from
  pulling out the .
Even if the were removed,
  the list order would prevent
  solvers from inferring a for
  the Rotate parameters.















Unlike the previous section,
  adding more rewrites does not help.[
    We can report that AC-matching is
    a problem both in theory and practice.]
  
do not compactly represent equivalences
  due to reordering associative and commutative operators
  like . This is known as the AC-matching problem <cit.>
  (A stands for associativity, and C for commutativity)
  and it prevents efficiently exploring all
  possible reorderings and regroupings.











addresses this with a new technique, ,
  that allows solvers to
  speculatively transform their inputs to allow for more
  profitable rewriting.
A solver that cannot simplify input A may,
  for some transformation F,
  be able simplify F(A) to B.
simply allows the solver to
  “wrap” B with F^-1 before unifying it with A,
  even though A and B are not equivalent.

enable locally-reasoning solvers to
  register potentially profitable
  regroupings and reorderings in an .
Simple syntactic rewrites then
  propagate these “hints” globally through the ,
  allowing other solvers to try them,
  and contextually eliminate inverse transformations when possible
  (e.g., under order-insensitive operations like Fold Union).
































































 §.§ Extended 



Extended (<ref> and <ref>)
  adds that allow solvers to
  record how they manipulated their input.
These extended forms are only introduced in the ;
  's cost function ensures extraction produces
  regular programs.
Semantically, these constructs either
  undo the transformation performed by the solver to recover the input, or
  perform the transformation on some other part of the program.
and take a permutation p and a list ℓ,
  imposing (respectively, undoing) p on ℓ.
takes a partitioning P (a list of lengths) and a list ℓ,
  breaking down ℓ into a list of sublists according to P.
takes a partitioning and a list of lists and flattens the
  latter; the partitioning is only use to propagate information.
and take a 3D vector c and a list of 3D vectors in spherical
  coordinates about c, returning a list of the vectors in Cartesian
  coordinates (and vice versa).






























 §.§ Restructuring with and 




Using , can finally get the desired output given the
  realistic input for the ship's wheel (<ref>).
Starting from <ref>,
  separates the from the Cuboids with partitioning and
  sorts the list of Cuboids on their parameters,
  revealing repetitive structure similar to
  the ideal input (<ref>).



  
Partitioning
includes a partitioning solver that
  uses and a set of heuristics to
  restructure lists in ways that group
  similar list elements together
  (e.g., by kind of geometric primitive).
The partitioner can split up elements of a list by
  equivalence class,
  individual components of 3D vectors,
  and kinds of affine transformations.
In <ref>, the partitioner will
  split the list into:
[xleftmargin=0mm,basicstyle=]
(Fold Union
  (Unpart ⟨ 1, 6 ⟩
    (List (Cylinder |[1,5]|))
    (List (Rotate |[0,0,120]| (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))
          (Rotate |[0,0,0]|   (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))
          (Rotate |[0,0,300]| (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))
          (Rotate |[0,0,180]| (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))
          (Rotate |[0,0,240]| (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))
          (Rotate |[0,0,60]|  (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|)))))


The introduced is equivalent to ,
  but additionally stores partitioning hints.
Now that the Rotates are gathered uniformly in a list,
  the structure finder will rewrite the list to:

[xleftmargin=1.5mm,basicstyle=]
(Map2 Rotate
    (List |[0,0,120]| |[0,0,0]| |[0,0,300]| |[0,0,180]| |[0,0,240]| |[0,0,60]|)
    (Repeat 6 (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|))))


The arithmetic solver from <ref>
  cannot find a closed form for
  this list of parameters.
The solver could, however,
  find a closed form if it were free to sort the list
  (by z-coordinate, in this case).
The sorted list is not equivalent to the original.
Since the solver only rewrites locally,
  it does not know if the list appears under
  a Fold Union (which is AC) or
  a Fold Diff (which is not AC).
In the ,
  both situations could actually
  hold due to sharing.
The solver cannot soundly rewrite the
  original list to the closed form ,
  but it can soundly rewrite the list to:

[xleftmargin=1.5mm,basicstyle=]
  (Unsort ⟨ 1, 5, 0, 3, 4, 2⟩ (Tabulate (i 6) [0, 0, 60i]))


The allows the solver to introduce
  the closed form in the ,
  but will never extract it or any other program
  using the forms from Extended Caddy.
Instead,
  rewrites propagate between
  invocations of locally-reasoning solvers,
  and additional rules eliminate in
  contexts invariant to the relevant transformation;
  these rules are shown in <ref>.
The Map2 Unsort Params rewrite applies
  to our running example, producing:
[xleftmargin=1.5mm,basicstyle=]
(Unsort ⟨ 1, 5, 0, 3, 4, 2 ⟩ (Sort ⟨ 1, 5, 0, 3, 4, 2 ⟩
  (Map2 Rotate
    (Unsort ⟨ 1, 5, 0, 3, 4, 2⟩ (Tabulate (i 6) [0, 0, 60i]))
    (Repeat 6 (Translate |[1,-0.5,0]| (Cuboid |[10,1,1]|))))))


Semantically, this is no different, as (Unsort p (Sort p x)) = x,
  but since the is in the same as the original list of
  Rotates, the Sort Application rule can fire,
  communicating the profitable ordering of the parameters to the outer list.
Now, the structure finder and arithmetic solver apply to the sorted
  list of Rotates, bringing the whole program to:
[xleftmargin=5mm,basicstyle=]
(Fold Union
  (Unpart ⟨ 1,6 ⟩
    (List (Cylinder |[1,5]|))
    (Unsort ⟨ 1, 5, 0, 3, 4, 2 ⟩
      (Tabulate (i 6)
        (Rotate [0, 0, 60i]
          (Translate |[1,-0.5,0]|
            (Cuboid |[10,1,1]|))))))))


From here an additional rewrite (elided from <ref>)
  can lift the over the :
[xleftmargin=5mm,basicstyle=]
(Fold Union
  (Unsort ⟨ 0, 2, 6, 1, 4, 5, 3 ⟩
    (Unpart ⟨ 1, 6 ⟩
      (List (Cylinder |[1,5]|))
      (Tabulate (i 6)
        (Rotate [0, 0, 60i]
          (Translate |[1,-0.5,0]|
            (Cuboid |[10,1,1]|))))))))


Next, the Unsort Elimination rule removes the ,
  since Fold Union is invariant to order.
Finally one additional rule that transforms a
  of an into a of (not shown),
  produces the desired output (<ref>).








































































































































































































































































































































 §.§ Solving for Spherical Coordinates

















are not restricted to list manipulations.
In addition to sorting,
  's arithmetic solvers can
  convert lists to spherical coordinates <cit.>.
The resulting list may be easier to find a closed form for,
  but it is not equivalent to the input.









Therefore, the solver wraps the in an , , before passing it to
  the for unification.
If the propagates under a , then
  the Unspherical Trans rule can replace it with TranslateSpherical
  form.
This approach allows to solve for closed forms of lists in
  spherical coordinates without the solver knowing whether or not it
  is solving for a list of parameters.






























 §.§ Inverse Transformations, Broadly



This section and our evaluation show that are
  effective for shrinking programs, but the technique could
  be applied more broadly to other uses of Equality Saturation.
The key insight is that solvers can remain simple because they only
  have to reason locally.
They are given the flexibility to speculate on potentially profitable
  ways to transform their inputs.
Rewrites can then propagate this information and contextually
  eliminate the transformations.
As in traditional Equality Saturation, these rewrites (and now simple
  solvers) compose in emergent ways, leading to unexpectedly powerful
  outcomes, that would have otherwise required more complicated
  solvers with deep, contextual reasoning ability.








§ IMPLEMENTATION



is implemented in 3000 lines of and uses  <cit.>, an open source library.




<ref> provides a break down of
the LOC for each of 's components.
uses only simple, custom solvers for arithmetic and list
partitioning.
The most of 's 65 rewrites are syntactic and compactly expressed,
and the remainder either call out to the solvers or manipulate lists.
is publicly available at
https://github.com/uwplse/szalinski.git.





















 §.§ Correctness



To validate 's correctness, we test that the initial and final
programs compile to similar meshes (<ref>).


first evaluates a program back to a flat Core program which is then pretty printed to a CSG program.
We use the open source OpenSCAD <cit.> tool to compile
  the CSGs to triangular meshes.
We then use the CGAL <cit.> library to compute the Hausdorff
  distance <cit.> between the two meshes.
A Hausdorff distance less than a small ϵ indicates
  equivalence (ideally it should be zero, but due to rounding errors,
  it is sufficient to check against ϵ).





























§ EVALUATION



In evaluating , were interested in the following research questions:




  * End-to-End. (<ref>)
Does compose with prior mesh decompilation
    tools and find parametrizable programs from
the flat CSG expressions generated by the latter?


  * Scalability. (<ref>)
Does scale to large flat CSGs?
How fast can it find equivalent smaller programs?


  * Sensitivity analysis.
How do the different components of , in particular CAD rewrites
and , affect its results?



We ran our evaluation on a 6 core Intel i7-8700K processor with 32 GB of RAM.









































 §.§ End-to-End Experiments



To evaluate the composability of with mesh decompilation tools,
  we ran on flat CSGs generated by the
  Reincarnate <cit.> mesh decompiler.


This required investigating what kinds of models Reincarnate
supports; we found that it worked best on models that do not
contain round edges.
We found 10 such models from Thingiverse <cit.> and ran Reincarnate
on their mesh files to get flat CSGs and converted those to Core .

Given the Core inputs, synthesizes programs
  (<ref>).
We compared the parametrized programs
synthesized by from Reincarnate's output with manually written
parametrized programs in OpenSCAD (column 1 in <ref>).
For four of the 10 models, we found a parametrized
OpenSCAD implementation on Thingiverse.
For the other six, we manually wrote a parametrized implementation in OpenSCAD.


<ref>
shows the comparison of the lines of code  at every stage of the
end-to-end synthesis process,
and the cost of the flat input Core and the output .
was able to reduce the cost of the programs by
86% on average. The last two columns report a sensitivity analysis of on
Reincarnate's output. It shows that both CAD identities and contribute significantly to shrinking programs.

Compiling the programs to mesh resulted in meshes equivalent to
  the source meshes (Hausdorff distance < 0.001).
We also manually validated that all 10 inferred programs are
  structurally similar to the parameterized input OpenSCAD programs.





 §.§ Large Scale Evaluation on Thingiverse Models



Mesh decompilation tools have limitations.
Reincarnate for example, works mainly on
shapes without rounded corners and edges.
Therefore, in order to evaluate further,
we performed a larger scale evaluation on models from
Thingiverse <cit.>, a popular online model sharing website.

The goals for this part of the evaluation are: (1) to simulate
the behavior of mesh decompilation tools by flattening
parametrized programs and perturbing them to
reproduce the challenges and (introduced in <ref>),
and run on these flat CSGs, (2)
to analyze the scalability, correctness and efficiency of on large-scale real world programs.



  
Data Collection
We built a scraper that downloaded customizable models from
Thingiverse. While most models in Thingiverse
are shared as triangular meshes which are hard to customize, models under the
"Customizable" category <cit.> are intended to be editable,
and are therefore more likely
to be accompanied with higher-level programmatic representation. Our scraper
found 12,939 OpenSCAD files from the "Customizable".
912 of these files were
invalid, i.e. they were empty, could not be compiled, or used debug features.
We filtered out files using features we do not support (like linear extrusion),
leaving 2,127 models.
Similar to ,
the OpenSCAD language supports CSG and also has features like for loops that can
be used to write more parametrizable CAD programs.
OpenSCAD can compile these programs
to flat CSG, which then accepts as input.
Figure <ref> summarizes the AST sizes of these inputs.



OpenSCAD primitives like spheres and cylinders are parameterized by their
geometric precision.
The geometric precision indicates the
  quality of the mesh obtained when the CSG is compiled.
For example, a sphere with resolution 100 has a more
fine-grained mesh than a sphere with resolution 10.
We found several examples where the precision of the primitives was as high as 100.
However, OpenSCAD's compiler is slower when generating finer resolution meshes.
Since our verifier (<ref>) uses the OpenSCAD
compiler, we capped the precision of all primitives to 25.



  
Results
<ref> shows our results with a 60 second timeout.
We refer to the baseline result (leftmost) as slightly perturbed, as
  OpenSCAD represents affine transformations in an ambiguous way in
  its CSG format (ex: the representation of Scale [-1,-1,1] and
  Rotate [0,0,180] are identical).
The second result shows that is fast; limiting it to 1 second
  has very little effect on the result.
The third result shows is robust to reordering of the inputs.
The final two results show CAD rewrites or significantly
  contribute to 's performance.
We validated all results with the by comparing the meshes.
All Hausdorff distances were under 0.01, except for 148 cases where
  CGAL failed to compute the distance
  and we visually compared the meshes.






















 §.§ Case Studies and Editability





This section discusses three models from the end-to-end evaluation
in <ref>
(a fourth is illustrated in <ref>)
and three models from the large scale
evaluation in <ref>.
The goal is to highlight some edits made easily possible by , which
in the flat CSG (and mesh) are nearly impossible.
<ref> shows a rendering of these models and the
parametrized program found by .
We discuss three categories of edits.

Adding or removing components: consider the gear shown in <ref>.
Changing the tooth count in a flat CSG version of this model requires manually computing
the position of every teeth and ensuring that the spacing between them is still
equal. The program synthesized by makes this modification trivial—it exposes a
function (6 × i) for and the number of teeth ( in the ), which can both be easily changed to get a different
tooth count. Adding rows or columns of components is also easy in a parametrized model. For example, in
the first model in <ref>, another set of compartments can be added by changing the bounds
of .

Modifying the shape of multiple components: in the last model in <ref>, the cylinders
can be all changed to by changing it in two places only. These modification in the flat CSGs require changing the shape of
each cylinder individually, which is undesirable. <ref> shows more examples of edits
where the shape of the hex-wrench holder can be changed by changing
the parameters inferred by .

Applying additional affine transformations to components:
consider the SD card rack (the second model) in <ref>.
This model can be easily customized in the program to adjust the size of the slots. The program
in the figure shows that in each iteration (in ), two sizes of are removed from the outer box.
The dimensions of these can be changed in the function inferred for the
parameters:
(Cuboid [4.5, 25, j + 0.5]) to change the slot size. Similarly, <ref> showed how
an additional rotation can be easily added to to make an entirely different model.

Performing these modifications in a flat CSG is tedious and error-prone
because they require manually recomputing many parameters for multiple
components in the models. makes these modifications much easier by exposing
different design parameters.






























































































 §.§ Limitations



Some mesh decompilation tools like InverseCSG synthesize
flat CSG programs using enumerative synthesis and random sampling
based algorithms like RANSAC <cit.>. Inferring structure from
the output generated by these tools requires
equivalence under context using geometric reasoning that
our prototype currently does not support.
InverseCSG provides 50 benchmarks, on all of which we ran .
The majority of the benchmarks lacked the repetitive structure is
intended to infer.
For one of the models (benchmark 157, a gear),
was able to infer a function.
However, due to the structure of their outputs,
we had to add rewrites like:

(Difference (Union a b) c)  (Union (Difference a c) b)
which are unsound without a geometric solver that can check that the intersection of
b and c is empty.
We manually applied this rewrite to benchmark-157
but did not add these rewrites to
's rule database due to their unsoundness.



































§ RELATED WORK





  
based Deductive Program Synthesis

E-graphs have been used extensively in
superoptimizers <cit.>, and SMT solvers <cit.>. 's core algorithm is
a generalized version of equality saturation <cit.>.
Integrating linear solvers with compiler optimizers has a long history with
tools like Omega Calculator <cit.>.
Our approach of using syntactic rewrites
and an arithmetic function solver to
modify the can be considered similar to Simplify <cit.> which
uses an module for finding equivalent expressions containing
uninterpreted functions, and a Simplex module that is used for arithmetic
computations.

However, unlike ,
past work does not allow solvers to speculatively add potentially
profitable expressions in the .
allows to accomplish this while also
mitigating the AC-matching problem for associative and
commutative operations like list reordering and regrouping.















  
2D and 3D design synthesis Nandi et al. <cit.> and Du
et al. <cit.> have developed tools that can decompile low-level polygon
meshes to flat CSGs.
These tools use program synthesis together with domain specific
computational geometric algorithms to discover structure in the meshes.


CSGNet <cit.> uses machine learning to generate flat CSG programs for 2D
and 3D shapes.  Shape2Prog <cit.> uses machine learning to infer
programs from voxel-based 3D models. They use LSTMs to infer programs with
loops. We ran on the flat CSGs from both CSGNet and Shape2Prog—
since their program lengths are very small (AST depth < 7),
they are not good candidates for design parameter inference. however
did find some structure in these program and generated correct
outputs.







Ellis et al. <cit.> developed a tool that can automatically generate
programs that correspond to hand-drawn images. They first use machine learning
to detect primitives in the drawings and then use Sketch <cit.> to find
loops and conditionals. 's technique is different from theirs in that they
use enumerative search to explore all programs within a given depth (their max AST depth is 3),
based on a language grammar, a specification, and a cost, whereas uses a rewrite-based
synthesis technique where the specification is given as the initial CSG, and
constructs an and updates it using semantics preserving rewrites.
In order to compare with Ellis et al.'s <cit.> tool, we
ported their 2D models to 3D and ran on them. 's results
had similar loop structure as theirs but further comparison is not possible since their DSL is different.
Another line of work <cit.> uses reinforcement
learning to synthesize programs for 2D and 3D models.
However, the programs inferred by these
approaches are much smaller compared to .


In computer graphics and vision, symmetry detection <cit.> in 3D shapes is
a well studied topic. It can improve performance of geometry processing
algorithms. The ability to detect folds and maps in 3D models is more general
than symmetry detection because it can find patterns in models that have
repetitive structure that is not symmetry. A simple example of this is a union of
n cubes increasing in size.
In fabrication, Schulz et al. <cit.> developed
algorithms for optimizing parametric CAD models
using interpolation methods.
While their approach can optimize parameters,
it does not automatically infer maps and folds from flat CSG inputs.











































§ CONCLUSION









This paper addresses the challenge
  of synthesizing smaller high-level CAD models
  from the noisy and unstructured outputs
  of existing triangle mesh to CSG decompilers.





We developed ,
  a prototype tool to synthesize  programs
  using semantics-preserving rewrites and simple solvers to “reroll loops.”
By adapting Equality Saturation to the CAD domain,
  can robustly handle common CSG variations
  exhibited by existing mesh decompilers.
relies on novel 
  to mitigate the AC-matching problem that
  arises when reordering CAD operations:
  solvers annotate and merge terms that
  are only equivalent modulo reordering,
  then propagate and eliminate such annotations
  through an to expose repetitive structure
  and robustly enable loop rerolling.
are not CAD-specific;
  we are excited to explore future work
  investigating how they may be applied
  in other ordering-sensitive optimization problems,
  e.g., instruction scheduling <cit.>.

To the best of our knowledge,
  is the first tool of its kind.




We performed an early survey of
  real-world CAD models from Thingiverse.
Our evaluation shows that can
  dramatically shrink many CAD models in seconds.

In future work,
  we are excited to explore richer rewrites for
  contextual equivalence (<ref>),
  more expressive cost functions for capturing
  richer notions of editability,
  and connections to interactive CAD editing
  using direct manipulation tools like Sketch-n-Sketch <cit.>.
























































