suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add solve

Browse Source
This commit is contained in:
Stephen Chang 2016-08-31 15:19:12 -04:00
parent 90e9517b3a
commit af98a9dec9
2 changed files with 50 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
turnstile/examples/rosette/rosette2.rkt
View File

@ -459,7 +459,18 @@
(define-rosette-primop <= : (Ccase-> (C→ CInt CInt CBool)
(C→ Int Int Bool)))
(define-rosette-primop >= : (Ccase-> (C→ CInt CInt CBool)
(C→ Int Int Bool)))
(C→ Int Int Bool)))
(define-rosette-primop abs : (Ccase-> (C→ CPosInt CPosInt)
(C→ PosInt PosInt)
(C→ CZero CZero)
(C→ Zero Zero)
(C→ CNegInt CPosInt)
(C→ NegInt PosInt)
(C→ CInt CInt)
(C→ Int Int)
(C→ CNum CNum)
(C→ Num Num)))
(define-rosette-primop not : (C→ Any Bool))
(define-rosette-primop false? : (C→ Any Bool))
@ -552,6 +563,10 @@
(define-base-types CSolution CPict)
(define-rosette-primop core : (C→ Any Any))
(define-rosette-primop sat? : (C→ Any Bool))
(define-rosette-primop unsat? : (C→ Any Bool))
(define-typed-syntax verify
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : _]]
@ -570,8 +585,6 @@
--------
[⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
(define-rosette-primop core : (C→ Any Any))
(define-rosette-primop sat? : (C→ Any Bool))
(define-typed-syntax synthesize
[(_ #:forall ie #:guarantee ge) ≫
@ -586,6 +599,12 @@
--------
[⊢ [_ ≫ (ro:synthesize #:forall ie- #:assume ae- #:guarantee ge-) ⇒ : CSolution]]])
(define-typed-syntax solve
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : _]]
--------
[⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]])
;; ---------------------------------
;; Subtyping

28
turnstile/examples/tests/rosette/rosette-guide-tests.rkt
View File

@ -82,12 +82,19 @@
(check-type+asserts (same poly factored -1) : Unit -> (void) (list))
(check-type+asserts (same poly factored -2) : Unit -> (void) (list))
;; 2.3.1 Verification
(define-symbolic i integer? : Int)
(define cex (verify (same poly factored i)))
(check-type cex : CSolution)
(check-type (sat? cex) : Bool -> #t)
(check-type (unsat? cex) : Bool -> #f)
(check-type (evaluate i cex) : Int -> 12)
(check-runtime-exn (same poly factored 12))
(clear-asserts!)
;; 2.3.2 Debugging
(require "../../rosette/query/debug.rkt"
"../../rosette/lib/render.rkt")
(define/debug (factored/d [x : Int] -> Int)
@ -98,6 +105,8 @@
;; TESTING TODO: requires visual inspection (in DrRacket)
(check-type (render ucore) : CPict)
;; 2.3.3 Synthesis
(require "../../rosette/lib/synthax.rkt")
(define (factored/?? [x : Int] -> Int)
(* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
@ -107,9 +116,28 @@
#:guarantee (same poly factored/?? i)))
(check-type binding : CSolution)
(check-type (sat? binding) : Bool -> #t)
(check-type (unsat? binding) : Bool -> #f)
;; TESTING TODO: requires visual inspection of stdout
(check-type (print-forms binding) : Unit -> (void))
;; typed/rosette should print:
;; '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
;; (untyped) rosette should print:
;; '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
;; 2.3.4 Angelic Execution
(define-symbolic x y integer? : Int)
(define sol
(solve (begin (assert (not (= x y)))
(assert (< (abs x) 10))
(assert (< (abs y) 10))
(assert (not (= (poly x) 0)))
(assert (= (poly x) (poly y))))))
(check-type sol : CSolution)
(check-type (sat? sol) : Bool -> #t)
(check-type (unsat? sol) : Bool -> #f)
(check-type (evaluate x sol) : Int -> -5)
(check-type (evaluate y sol) : Int -> 2)
(check-type (evaluate (poly x) sol) : Int -> 120)
(check-type (evaluate (poly y) sol) : Int -> 120)