我用_20813实现程序合成器时最常见的错误之一是以不安全的方式使用unlifted Racket constructs，使合成器输出 (unsat) .
事实上，作为初学者Rosette程序员，很难在我不工作的代码中找到可能导致问题的未提升的Racket结构 . 我认为DrRacket可以提供帮助，例如，不显示从 #lang rosette 线到未提升的Racket结构的箭头，例如assv，但事实并非如此，即它显示两个未提升的箭头（例如， assv ）并解除了运营商（例如， first ） .
我一直在使用两种策略，（i）在 rosette/safe 中构建合成代码，然后我可以切换到完整的语言，但这种方式很不方便，因为我不能使用更新更好的Racker构造，以及（ii）浏览我在我的代码中使用的构造并检查它们是否是"provided"，但是这种方式很烦人 .
经验丰富的Rosette程序员的任何建议？
1 回答
一种方法是在
rosette/safe中开始编程，然后根据需要明确地从Racket中获取所需的构造 . 然后，如果出现问题，将更容易找到他们在何时何地 .因此，例如，您的代码看起来像这样：
随着代码库的增长，您还可以将所有这些导入收集到导出它们的单个模块中 . 然后，您的其余代码将需要该模块，该模块将充当
rosette/safe的自定义版本以及您需要的最少数量的Racket构造 .