Witch of Git - jade-mouse/blob - synthesis-base.rkt

   1 #lang rosette/safe
   2
   3 (require rosette/lib/angelic
   4          rosette/lib/match)
   5
   6 ; Most of the setup taken from Whitequark's synthesis demo
   7 ; https://gist.github.com/whitequark/1f7cc43c1cc2b179a1d4a668f0089804
   8
   9 (provide ??prog verify-prog synthesize-prog optimize-prog)
  10
  11 (define (??prog ??insn fuel)
  12   (if (= fuel 0) null
  13       (cons (??insn) (??prog ??insn (- fuel 1)))))
  14
  15 ; program verifier
  16 (define (verify-prog make-state run-insn prog asserts)
  17   (define S  (make-state))
  18   (define S* (make-state))
  19   (define solution
  20     (verify
  21      #:guarantee
  22      (begin
  23        (for-each (curry run-insn S*) prog)
  24        (asserts S S*))))
  25   (if (unsat? solution) #t
  26       (begin
  27         (displayln (evaluate S  solution))
  28         (displayln (evaluate S* solution))
  29         solution)))
  30
  31 ; program synthesizer
  32 (define (synthesize-prog make-state run-insn sketch asserts)
  33   (define S  (make-state))
  34   (define S* (make-state))
  35   (define solution
  36     (synthesize
  37      #:forall S
  38      #:guarantee
  39      (begin
  40        (for-each (curry run-insn S*) sketch)
  41        (asserts S S*))))
  42   (if (unsat? solution) #f
  43       (begin
  44         (evaluate sketch solution))))
  45
  46 (define (optimize-prog max-fuel make-state run-insn sketch-gen asserts)
  47   (define (worker fuel)
  48     (printf "fuel ~s~n" fuel)
  49     (or (synthesize-prog make-state run-insn (sketch-gen fuel) asserts)
  50         (if (>= fuel max-fuel) #f
  51             (worker (+ fuel 1)))))
  52   (worker 0))