什么时候我应该使用Rosette的浅层和深层嵌入程序合成？

Question

Rosette的一些教程 使用浅嵌入引入程序合成,其他使用深嵌入.

在阅读了Torlak et Bodik的"使用ROSETTE增长解算器辅助语言"之后,浅嵌入似乎适用于快速原型设计(因为它不需要定义DSL和解释器),并且深度嵌入有助于使查询具有更强的正确性保证.这是决定使用哪种嵌入的一个很好的经验法则吗？

使用Rosette的浅嵌入和深嵌入进行程序合成有什么好的理由？

Answer 1

作为一般经验法则,浅嵌入最适合使用求解器搜索程序处理的值的应用程序,这是程序验证和天使执行的典型情况.

如果您正在进行程序综合和搜索(表示代码的值),则深度嵌入是最佳选择.

如果您的应用程序只搜索常量,浅嵌入可能是程序合成的一个很好的选择.但是如果你正在寻找更复杂的东西(例如表达式或语句),那么深层嵌入就是你要走的路.

通过浅嵌入,您可以有限地控制Rosette将搜索的程序空间.基本上,你只能使用Rosette的基于宏的草图结构编码.这些允许您定义基本搜索空间并编写快速原型,但如果您想构建可扩展的工具,则需要严格控制搜索空间.

通过深度嵌入,您可以完全控制将要搜索的程序空间.基本上,您可以编写任意Rosette/Racket函数来生成代表所有要搜索的具体程序的符号程序.然后,您还可以完全控制最后一步,即代码生成.一旦Rosette返回表示深度嵌入中的程序的值(例如,AST),您可以处理它,但是您想要生成代码.通过浅嵌入,您只能使用Rosette的内置代码生成器.

因此,总而言之,如果您正在或计划进行综合,请使用深度嵌入.对于其他一切(验证和天使执行),浅嵌入将更容易和更快.