2

我在使用Rosette实现程序合成器时最常见的错误之一是以不安全的方式使用未提升的Racket 构造(unsat)，这会使合成器输出。

事实上，作为初学者的 Rosette 程序员，很难仅仅找出可能导致问题的未提升的 Racket 结构。我认为 DrRacket 可能会有所帮助，例如，通过不显示从#lang rosette线到未提升的球拍结构的箭头，例如assv，但事实并非如此，即它向两个未提升的球拍结构（assv例如和提升的运营商（例如，first）。

我一直在使用两种策略，(i)rosette/safe尽可能构建合成代码，然后切换到完整的语言，这很不方便，因为我不能使用更新和更高级的 Racker 构造，以及 (ii) 略读我的构造在我的代码中使用并检查它们是否由 提供rosette/base/base.rkt，这很烦人。

经验丰富的 Rosette 程序员有什么建议吗？

4

1 回答 1

3

一种方法是开始编程，rosette/safe然后根据需要显式地从 Racket 中获取所需的构造。然后，如果出现问题，将更容易找出它们发生的地点和时间。

因此，例如，您的代码将如下所示：

   #lang rosette/safe

   (require (only-in racket for assv))

随着代码库的增长，您还可以将所有这些导入收集到一个导出它们的模块中。然后，您的其余代码将需要该模块，该模块将充当您的自定义版本rosette/safe以及您需要的最少数量的 Racket 构造。

于 2018-12-10T23:12:04.883 回答