一些教程Rosette https://docs.racket-lang.org/rosette-guide/index.html引入程序综合使用浅嵌入 https://docs.racket-lang.org/rosette-guide/ch_essentials.html#%28part._sec~3asynthesize%29和其他人使用深嵌入 https://homes.cs.washington.edu/~bornholt/post/building-synthesizer.html.
阅读 Torlak 和 Bodik 的文章后“使用 ROSETTE 发展求解器辅助语言” https://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf，似乎浅嵌入有利于快速原型设计（因为它不需要定义 DSL 和解释器），而深嵌入有利于进行具有更强正确性保证的查询。这是决定使用哪种嵌入的良好经验法则吗？
使用 Rosette 的浅嵌入与深嵌入进行程序综合的充分理由是什么？
作为一般经验法则，浅嵌入最适合使用求解器搜索程序处理的值的应用程序，这对于程序验证和天使执行来说是典型的。
如果您正在进行程序综合并搜索（表示的值）代码，那么深度嵌入是最佳选择。
如果您的应用程序仅搜索常量，则浅嵌入可能是程序综合的不错选择。但是，如果您正在搜索更复杂的内容（例如表达式或语句），那么深度嵌入就是正确的选择。
通过浅嵌入，您对 Rosette 将搜索的程序空间的控制有限。基本上，您只能使用 Rosette 的基于宏的草图结构编码的任何内容。这些允许您定义基本搜索空间并编写快速原型，但如果您想构建可扩展的工具，您将需要严格控制搜索空间。
通过深度嵌入，您可以完全控制要搜索的程序空间。本质上，您可以编写任意 Rosette / Racket 函数来生成代表要搜索的所有具体程序的符号程序。然后，您还可以完全控制最后一步，即代码生成。一旦 Rosette 返回一个代表深度嵌入中的程序的值（例如 AST），您就可以根据需要生成代码来处理它。对于浅嵌入，您只能使用 Rosette 的内置代码生成器。
因此，总而言之，如果您正在进行或计划进行综合，请使用深度嵌入。对于其他一切（验证和天使执行），浅嵌入将更容易、更快。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
