Rosette 解算器辅助的编程语言

Rosette 是新的计算机辅助解析编程（SDSLs）语言，扩展了 Racket 的一些特性：合成，验证，调试和执行。

Rosette 是一个解算器辅助的编程语言，扩展了 Racket 用于程序合成、校验等。为了校验和合成代码，Rosette 将其编译为带 SMT 解决逻辑的逻辑限制解算。

示例代码：

#langrosette(define(interpretformula)(matchformula[`(∧,expr...)(apply&&(mapinterpretexpr))][`(∨,expr...)(apply||(mapinterpretexpr))][`(¬,expr)(!(interpretexpr))][lit(constantlitboolean?)]));ThisimplementsaSATsolver.(define(SATformula)(solve(assert(interpretformula))))(SAT`(∧ro(∨se(¬t))t(¬e)))