Rosette 解算器辅助的编程语言 项目简介
Rosette 是新的计算机辅助解析编程(SDSLs)语言,扩展了 Racket 的一些特性:合成,验证,调试和执行。Rosette 是一个解算器辅助的编程语言,扩展了 Racket 用于程序合成、校验等。为了校验和合成代码,Rosette 将其编译为带 SMT 解决逻辑的逻辑限制解算。示例代码:#lang rosette
(define (interpret formula)
(match formula
[`(∧ ,expr ...) (apply && (map interpret expr))]
[`(∨ ,expr ...) (apply || (map interpret expr))]
[`(¬ ,expr) (! (interpret expr))]
[lit (constant lit boolean?)]))
; This implements a SAT solver.
(define (SAT formula)
(solve (assert (interpret formula))))
(SAT `(∧ r o (∨ s e (¬ t)) t (¬ e)))
(define (interpret formula)
(match formula
[`(∧ ,expr ...) (apply && (map interpret expr))]
[`(∨ ,expr ...) (apply || (map interpret expr))]
[`(¬ ,expr) (! (interpret expr))]
[lit (constant lit boolean?)]))
; This implements a SAT solver.
(define (SAT formula)
(solve (assert (interpret formula))))
(SAT `(∧ r o (∨ s e (¬ t)) t (¬ e)))