synth.rkt

#lang rosette/safe



(require rosette/lib/synthax)     ; Require the sketching library.
(define-grammar (bsl-nums x)  ; Grammar of int32 expressions over two inputs:
  [expr
   (choose x (?? integer?) #;(/ (?? integer?) (?? integer?))        ; <expr> := x | y | <32-bit integer constant> |
           ((bop) (expr) (expr))  ;           (<bop> <expr> <expr>) |
           ((uop) (expr)))]       ;           (<uop> <expr>)
  [bop
   (choose + - * /)]        ;           bvlshr | bvashr
  [uop
   (choose -)])         ; <uop>  := bvneg | bvnot

(define (bsl-sketch lo)
  (bsl-nums lo #:depth 2))
(define-symbolic l h integer?)

(define (check-ctok impl l)
  (assert (= (impl 0) 273))
  (assert (= (impl 100) 373)))

(define (check-ftoc impl)
  (assert (= (impl 32) 0))
  (assert (= (impl -40) -40)))

(define sol
    (synthesize
     #:forall    (list l)
     #:guarantee (check-ftoc bsl-sketch)))