research-article

Public Access

Synthesizing structured CAD models with equality saturation and inverse transformations

Authors:

Chandrakana Nandi,

James R. Wilcox,

Zachary TatlockAuthors Info & Claims

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 31 - 44

https://doi.org/10.1145/3385412.3386012

Published: 11 June 2020 Publication History

Abstract

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 Szalinski, a tool that uses Equality Saturation with semantics-preserving CAD rewrites to efficiently search for smaller equivalent programs. Szalinski relies on inverse transformations, a novel way for solvers to speculatively add equivalences to an E-graph. We qualitatively evaluate Szalinski in case studies, show how it composes with an existing mesh decompiler, and demonstrate that Szalinski can shrink large models in seconds.

References

[1]

Celena Alcock, Nathaniel Hudson, and Parmit K. Chilana. 2016. Barriers to Using, Customizing, and Printing 3D Designs on Thingiverse. In Proceedings of the 19th International Conference on Supporting Group Work (GROUP ’16). ACM, New York, NY, USA, 195–199.

Digital Library

[2]

Sorav Bansal and Alex Aiken. 2008. Binary Translation Using Peephole Superoptimizers. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI’08). USENIX Association, Berkeley, CA, USA, 177–192. http://dl.acm.org/citation. cfm?id=1855741.1855754

Digital Library

[3]

Walid Belkhir and Alain Giorgetti. 2012. Lazy AC-Pattern Matching for Rewriting. Electronic Proceedings in Theoretical Computer Science 82 (Apr 2012), 37–51.

[4]

CGAL. 2018. CGAL. https://www.cgal.org.

[5]

Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and Direct Manipulation, Together at Last. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA, 341– 354.

Digital Library

[6]

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. 2007. All About Maude - a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, Heidelberg. PLDI ’20, June 15–20, 2020, London, UK C.Nandi, M. Willsey, A. Anderson, J. R. Wilcox, E. Darulova, D. Grossman, Z. Tatlock

[7]

Customizable. 2019. Thingiverse Customizable. https://www. thingiverse.com/customizable.

[8]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. http://dl.acm.org/citation.cfm?id=1792734.1792766

Digital Library

[9]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378– 388.

[10]

David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking. J. ACM 52, 3 (May 2005), 365–473.

Digital Library

[11]

Tao Du, Jeevana Priya Inala, Yewen Pu, Andrew Spielberg, Adriana Schulz, Daniela Rus, Armando Solar-Lezama, and Wojciech Matusik. 2018. InverseCSG: automatic conversion of 3D models to CSG trees. 1–16.

Digital Library

[12]

Kevin Ellis, Maxwell I. Nye, Yewen Pu, Felix Sosa, Joshua B. Tenenbaum, and Armando Solar-Lezama. 2019. Write, Execute, Assess: Program Synthesis with a REPL. In NeurIPS.

[13]

Kevin Ellis, Daniel Ritchie, Armando Solar-Lezama, and Joshua B. Tenenbaum. 2018. Learning to Infer Graphics Programs from Hand-Drawn Images. https://openreview.net/forum?id=H1DJFybC-

[14]

Markus Friedrich, Pierre-Alain Fayolle, Thomas Gabor, and Claudia Linnhoff-Popien. 2019. Optimizing Evolutionary CSG Tree Extraction. In Proceedings of the Genetic and Evolutionary Computation Conference (GECCO ’19). ACM, New York, NY, USA, 1183–1191.

Digital Library

[15]

10.1145/3321707.3321771

Digital Library

[16]

Nathaniel Hudson, Celena Alcock, and Parmit K. Chilana. 2016. Understanding Newcomers to 3D Printing: Motivations, Workflows, and Barriers of Casual Makers. In Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems (CHI ’16). ACM, New York, NY, USA, 384–396.

Digital Library

[17]

Rajeev Joshi, Greg Nelson, and Keith Randall. 2002. Denali: A Goaldirected Superoptimizer. SIGPLAN Not. 37, 5 (May 2002), 304–314.

Digital Library

[18]

Hélène Kirchner and Pierre-Etienne Moreau. 2001. Promoting Rewriting to a Programming Language: A Compiler for Non-deterministic Rewrite Programs in Associative-commutative Theories. J. Funct. Program. 11, 2 (March 2001), 207–251. http://dl.acm.org/citation.cfm?id= 968486.968488

[19]

Niloy J. Mitra, Mark Pauly, Michael Wand, and Duygu Ceylan. 2013. Symmetry in 3D Geometry: Extraction and Applications. Comput. Graph. Forum 32, 6 (Sept. 2013), 1–23.

Digital Library

[20]

P.H. Moon and D.E. Spencer. 1988. Field theory handbook: including coordinate systems, differential equations, and their solutions. Springer-Verlag.

[21]

https://books.google.com/books?id=EDnvAAAAMAAJ

[22]

James R Munkers. 2000. Topology.

[23]

Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, and Zachary Tatlock. 2018. Functional Programming for Compiling and Decompiling Computer-aided Design. Proc. ACM Program. Lang. 2, ICFP, Article 99 (July 2018), 31 pages. org/10.1145/3236794

Digital Library

[24]

Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph.D. Dissertation. Stanford, CA, USA. AAI8011683.

[25]

OpenScad. 2019. OpenScad. The Programmers Solid 3D CAD Modeller. http://www.openscad.org/.

[26]

Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. 2015. Automatically Improving Accuracy for Floating Point Expressions. SIGPLAN Not. 50, 6 (June 2015), 1–11. 1145/2813885.2737959

Digital Library

[27]

William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings Supercomputing ’91, Albuquerque, NM, USA, November 18-22, 1991. 4–13.

Digital Library

[28]

William Pugh and David Wonnacott. 1992. Eliminating False Data Dependences using the Omega Test. In Proceedings of the ACM SIGPLAN’92 Conference on Programming Language Design and Implementation (PLDI), San Francisco, California, USA, June 17-19, 1992. 140–151.

Digital Library

[29]

C. Ronse. 1990. Regular open or closed sets.

[30]

R. Schnabel, R. Wahl, and R. Klein. 2007. Efficient RANSAC for Point-Cloud Shape Detection. Computer Graphics Forum (2007).

[31]

Adriana Schulz, Jie Xu, Bo Zhu, Changxi Zheng, Eitan Grinspun, and Wojciech Matusik. 2017. Interactive Design Space Exploration and Optimization for CAD Models. ACM Trans. Graph. 36, 4, Article 157 (July 2017), 14 pages.

Digital Library

[32]

Gopal Sharma, Rishabh Goyal, Difan Liu, Evangelos Kalogerakis, and Subhransu Maji. 2017. CSGNet: Neural Shape Parser for Constructive Solid Geometry. CoRR abs/1712.08290 (2017). arXiv: 1712.08290 http: //arxiv.org/abs/1712.08290

[33]

Benjamin Sherman, Jesse Michel, and Michael Carbin. 2019. Sound and Robust Solid Modeling via Exact Real Arithmetic and Continuity. Proc. ACM Program. Lang. 3, ICFP, Article 99 (July 2019), 29 pages.

Digital Library

[34]

Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. Berkeley, CA, USA. Advisor(s) Bodik, Rastislav. AAI3353225.

Digital Library

[35]

Michael Stepp, Ross Tate, and Sorin Lerner. 2011. Equality-Based Translation Validator for LLVM. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 737–742.

[36]

Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality Saturation: A New Approach to Optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). ACM, New York, NY, USA, 264–276.

Digital Library

[37]

Thingiverse. 2019. Thingiverse. https://www.thingiverse.com/.

[38]

Yonglong Tian, Andrew Luo, Xingyuan Sun, Kevin Ellis, William T. Freeman, Joshua B. Tenenbaum, and Jiajun Wu. 2019. Learning to Infer and Execute 3D Shape Programs. In International Conference on Learning Representations.

[39]

Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). ACM, New York, NY, USA, 530–541.

Digital Library

[40]

Sid-Ahmed-Ali Touati and Denis Barthou. 2006. On the Decidability of Phase Ordering Problem in Optimizing Compilation. In Proceedings of the 3rd Conference on Computing Frontiers (CF ’06). ACM, New York, NY, USA, 147–156.

Digital Library

[41]

Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations. SIGPLAN Not. 43, 1 (Jan. 2008), 17–27. 10.1145/1328897.1328444

Digital Library

[42]

Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion. SIGPLAN Not. 44, 6 (June 2009), 316–326.

Digital Library

[43]

Max Willsey, Yisu Remy Wang, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, and Zachary Tatlock. 2020. egg: Easy, Efficient, and Extensible E-graphs. arXiv: cs.PL/2004.03082

Cited By

Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Patton NRahmani KMissula MBiswas JDillig I(2024)Programming-by-Demonstration for Long-Horizon Robot TasksProceedings of the ACM on Programming Languages10.1145/36328608:POPL(512-545)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632860
Show More Cited By

Index Terms

Synthesizing structured CAD models with equality saturation and inverse transformations

Recommendations

Synthesizing transformations on hierarchically structured data
PLDI '16

This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-...
Synthesizing transformations on hierarchically structured data
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-...
Learning syntactic program transformations from examples
ICSE '17: Proceedings of the 39th International Conference on Software Engineering

Automatic program transformation tools can be valuable for programmers to help them with refactoring tasks, and for Computer Science students in the form of tutoring systems that suggest repairs to programming assignments. However, manually creating ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2020

1174 pages

ISBN:9781450376136

DOI:10.1145/3385412

General Chair:
Alastair F. Donaldson
Imperial College London, UK
,
Program Chair:
Emina Torlak
University of Washington, USA

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

PLDI '20

Sponsor:

SIGPLAN

PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 15 - 20, 2020

London, UK

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

44
Total Citations
View Citations
1,123
Total Downloads

Downloads (Last 12 months)335
Downloads (Last 6 weeks)47

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Patton NRahmani KMissula MBiswas JDillig I(2024)Programming-by-Demonstration for Long-Horizon Robot TasksProceedings of the ACM on Programming Languages10.1145/36328608:POPL(512-545)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632860
Thomas SBornholt JTsafrir DMUSUVATHI MGupta RAbu-Ghazaleh N(2024)Automatic Generation of Vectorizing Compilers for Customizable Digital Signal ProcessorsProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624873(19-34)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624873
Van der Cruysse JDubach CGrosser TDubach CSteuwer MXue JOttoni GQuintão Pereira F(2024)Latent Idiom Recognition for a Minimalist Functional Array Language Using Equality SaturationProceedings of the 2024 IEEE/ACM International Symposium on Code Generation and Optimization10.1109/CGO57630.2024.10444879(270-282)Online publication date: 2-Mar-2024
https://dl.acm.org/doi/10.1109/CGO57630.2024.10444879
Cabrera-Arteaga JFitzgerald NMonperrus MBaudry B(2024) Wasm-MutateComputers and Security10.1016/j.cose.2024.103731139:COnline publication date: 16-May-2024
https://dl.acm.org/doi/10.1016/j.cose.2024.103731
Veuskens TRamakers RLeen DLuyten K(2023)History in Motion: Interactive 3D Animated Visualizations for Understanding and Exploring the Modeling History of 3D CAD DesignsProceedings of the 8th ACM Symposium on Computational Fabrication10.1145/3623263.3623358(1-13)Online publication date: 8-Oct-2023
https://dl.acm.org/doi/10.1145/3623263.3623358
Pal ASaiki BTjoa RRichey CZhu AFlatt OWillsey MTatlock ZNandi C(2023)Equality Saturation Theory Exploration à la CarteProceedings of the ACM on Programming Languages10.1145/36228347:OOPSLA2(1034-1062)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622834
Feser JDillig ISolar-Lezama A(2023)Inductive Program Synthesis Guided by Observational Program SimilarityProceedings of the ACM on Programming Languages10.1145/36228307:OOPSLA2(912-940)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622830
Kodnongbua MJones BAhmad MKim VSchulz A(2023)ReparamCAD: Zero-shot CAD Re-Parameterization for Interactive ManipulationSIGGRAPH Asia 2023 Conference Papers10.1145/3610548.3618219(1-12)Online publication date: 10-Dec-2023
https://dl.acm.org/doi/10.1145/3610548.3618219
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents