问题标签 [rosette]

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

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

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

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

Rosette的一些教程介绍了使用浅嵌入和其他使用深度嵌入的 程序合成。

在阅读了 Torlak et Bodik 的“Growing Solver-Aided Languages with ROSETTE”之后，似乎浅嵌入有利于快速原型设计（因为它不需要定义 DSL 和解释器），而深度嵌入有利于进行具有更强正确性保证的查询。这是决定使用哪个嵌入的好经验法则吗？

使用 Rosette 的浅嵌入与深层嵌入进行程序合成的充分理由是什么？

我正在使用波斯语进行情绪分析项目，为此我使用 rapidminer..

我安装了玫瑰花结扩展，用于这种语言的某些文本预处理目的，例如标记化。我有过滤停用词（字典）运算符的问题...当我将此运算符应用于我的数据集（标记化后）时，我只收到标记化的数据集而不过滤停用词...

你知道这个问题的原因是什么吗？

我希望在 Rosette 中编写一个 DSL，目的是合成一个函数。DSL 基于一个非常小的 Haskell 子集，并且是强类型的。因此，我想确保 Rosette 生成的任何内容都是正确类型的。

我可以考虑解决这个问题的一种方法是编写一个“is-well-typed-code”函数（这是我在 Julia 中已经做过的事情，我正在从中移植），然后断言它必须适用于综合函数。但是，我没有看到define-synthax以及synthesize如何将代码视为句法对象（即，可以应用任何函数的 S-expr）和在合成时作为语义函数。

我还可以想象cond在模块内部使用define-synthax所有可能类型的参数（这是这个小型 DSL 的有限集），并为每种类型分别定义可能的形式。define-synthax但是，似乎不可能在里面包含 conds 。

有任何想法吗？

谢谢！

我正在阅读Rosette Essentials。

该指南解释了使用define-symbolic：

define-symbolic每次计算时，该表单都会将变量绑定到相同的（唯一的）[符号]常量。

打印的常量名称，例如xor b，只是注释。通过评估两个不同的define-symbolic（或，define-symbolic*）形式创建的两个 [符号] 常量是不同的，即使它们具有相同的打印名称。它们可能仍然代表相同的具体值，但这由求解器确定：

我真的不明白的解释define-symbolic：

为什么(eq? (static) (static))返回#t，但(eq? (static) (yet-another-x))返回(<=> x x)？

由于每次评估时都会define-symbolic将变量绑定到相同的（唯一）常量，为什么不返回？，就像？(eq? (static) (yet-another-x))#t(eq? (static) (static))

这是否意味着两个符号变量出现在不同的范围内并具有相同的名称仍然不同，即使我们使用define-symbolic?

<=>和有什么区别=？例如(<=> x x)与(= y$1 y$2)。

谢谢。

我按照 Rosette 网站上的说明下载了 Rosette ( https://docs.racket-lang.org/rosette-guide/ch_getting-started.html )。看来我可以运行这个程序并且没有输出错误。

但是，当我尝试使用比基本球拍关键字更多的内容运行此程序或任何类似程序时，我得到了不清楚（对我而言）的错误。

这给了我一个错误destruct: unbound identifier in: destruct。到底是怎么回事？这段代码不是我自己的，是从教程中复制粘贴的，所以我认为它应该可以工作。我还尝试了从 Rosette 网站粘贴的示例代码副本，并给出了类似的错误。我已遵循所有安装说明并更新了环境路径等。有帮助吗？

我已经看到了一些关于如何用 Rosette 合成小块代数或命题逻辑代码的示例。我的问题是，这些是你可以合成的唯一类型吗？我试图合成围绕类型列表的小段代码？但我收到错误，因为它不是可解决的类型。我希望做的是综合关于列表的定理，例如“Forall list x, (length x) = (length (reverse x))”。这可能吗？

文档说“综合查询使用求解器在由句法草图定义的候选实现空间中搜索正确的程序。” 有时有多个正确的程序，但运行 synthesize 会给出一个。有没有办法打印许多可能的结果？

例如，

这打印

'(define (bfunc p) (not (<=> (not #t) p)))

我可以让它打印多个程序吗？