rosette - Synthesize 可以打印多个满足规范的结果吗？

Question

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

例如，

(define-symbolic p boolean?)
(define-grammar (boolfast p)
  [expr
   (choose p (?? boolean?)
           ((bool_op) (expr) (expr))
           (not (expr)))]
  [bool_op (choose && || xor => <=>)])

(define (bfunc p) (boolfast p #:depth 3))
(define-symbolic q boolean?)
(define sol4
  (synthesize
   #:forall (list q p)
   #:guarantee (assert (equal? (bfunc q) (&& q (|| p q))))))

这打印

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

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