Rosette解算器辅助的编程语言

联合创作 · 2023-09-27 23:25

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)))
浏览 4
点赞
评论
收藏
分享

手机扫一扫分享

编辑
举报
评论
图片
表情
推荐
点赞
评论
收藏
分享

手机扫一扫分享

编辑
举报