8.12
4.5 Procedures
Rosette procedures are references to procedure objects, just like in Racket. Two procedure references are eq? and equal? only if they point to the same procedure object. Procedures may be concrete or symbolic. Symbolic procedures may, in the worst case, take as much time to execute as the slowest concrete procedure to which any symbolic procedure could evaluate under any solution?.
Examples:
> (define-symbolic b boolean?) > (define-symbolic x integer?) > (define p (if b * -)) ; p is a symbolic procedure.
> (define sol (synthesize #:forall (list x) #:guarantee (assert (= x (p x 1))))) > (evaluate p sol) *
> (define sol (synthesize #:forall (list x) #:guarantee (assert (= x (p x 0))))) > (evaluate p sol) -
Rosette lifts the following operations on procedures: