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

add optimize, remaining sec3 tests; fix CList-CListof subtyping

Browse Source
This commit is contained in:
Stephen Chang 2016-09-01 14:59:57 -04:00
parent dfdc0eae37
commit 79abcce491
4 changed files with 148 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
turnstile/examples/rosette/rosette-notes.txt
View File

@ -53,7 +53,8 @@ TODOs:
- fix type of Vector and List to differentiate homogeneous/hetero
- 2016-09-01: add CList for hetero lists
- variable arity polymorphism
- CSolution?
- CSolution
- DONE 2016-08-30
- make libs have appropriate require paths
- eg typed/rosette/query/debug
- make typed/rosette a separate pkg

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

@ -562,6 +562,18 @@
(C→ Num Num Num)
(C→ Num Num Num Num)
(C→ Num Num Num Num Num))]
[- : (Ccase-> (C→ CInt CInt CInt)
(C→ CInt CInt CInt CInt)
(C→ CInt CInt CInt CInt CInt)
(C→ Int Int Int)
(C→ Int Int Int Int)
(C→ Int Int Int Int Int)
(C→ CNum CNum CNum)
(C→ CNum CNum CNum CNum)
(C→ CNum CNum CNum CNum CNum)
(C→ Num Num Num)
(C→ Num Num Num Num)
(C→ Num Num Num Num Num))]
[* : (Ccase-> (C→ CNat CNat CNat)
(C→ CNat CNat CNat CNat)
(C→ CNat CNat CNat CNat CNat)
@ -611,6 +623,12 @@
[real? : (C→ Any Bool)]
[positive? : (Ccase-> (C→ CNum CBool)
(C→ Num Bool))]
[even? : (Ccase-> (C→ CInt CBool)
(C→ Int Bool))]
[odd? : (Ccase-> (C→ CInt CBool)
(C→ Int Bool))]
[remainder : (Ccase-> (C→ CInt CInt CInt)
(C→ Int Int Int))]
;; rosette-specific
[asserts : (C→ (CListof Bool))]
@ -702,6 +720,17 @@
--------
[⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]])
(define-typed-syntax and
[(_ e ...) ≫
[⊢ [e ≫ e- ⇐ : Bool] ...]
--------
[⊢ [_ ≫ (ro:and e- ...) ⇒ : Bool]]])
(define-typed-syntax or
[(_ e ...) ≫
[⊢ [e ≫ e- ⇐ : Bool] ...]
--------
[⊢ [_ ≫ (ro:or e- ...) ⇒ : Bool]]])
;; ---------------------------------
;; solver forms
@ -753,6 +782,34 @@
--------
[⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]])
(define-typed-syntax optimize
[(_ #:guarantee ge) ≫
[⊢ [ge ≫ ge- ⇒ : _]]
--------
[⊢ [_ ≫ (ro:optimize #:guarantee ge-) ⇒ : CSolution]]]
[(_ #:minimize mine #:guarantee ge) ≫
[⊢ [ge ≫ ge- ⇒ : _]]
[⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
--------
[⊢ [_ ≫ (ro:optimize #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]]
[(_ #:maximize maxe #:guarantee ge) ≫
[⊢ [ge ≫ ge- ⇒ : _]]
[⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
--------
[⊢ [_ ≫ (ro:optimize #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]]
[(_ #:minimize mine #:maximize maxe #:guarantee ge) ≫
[⊢ [ge ≫ ge- ⇒ : _]]
[⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
[⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
--------
[⊢ [_ ≫ (ro:optimize #:minimize mine- #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]]
[(_ #:maximize maxe #:minimize mine #:guarantee ge) ≫
[⊢ [ge ≫ ge- ⇒ : _]]
[⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
[⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
--------
[⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]])
;; ---------------------------------
;; Subtyping
@ -772,12 +829,12 @@
[((~CList . tys1) (~CList . tys2))
(and (stx-length=? #'tys1 #'tys2)
(typechecks? #'tys1 #'tys2))]
[((~CList . tys) (~CListof . ty))
[((~CList . tys) (~CListof ty))
(for/and ([t (stx->list #'tys)])
(typecheck? t #'ty))]
;; vectors, only immutable vectors are invariant
[((~CIVectorof . tys1) (~CIVectorof . tys2))
(stx-andmap (current-sub?) #'tys1 #'tys2)]
[((~CIVectorof ty1) (~CIVectorof ty2))
(typecheck? #'ty1 #'ty2)]
; 2 U types, subtype = subset
[((~CU* . ts1) _)
(for/and ([t (stx->list #'ts1)])

81
turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
View File

@ -34,3 +34,84 @@
(check-type (second res) : Nat -> (if (first res) 0 3))
;; 3.2 Solver-Aided Forms
;; 3.2.1 Symbolic Constants
(define (always-same -> Int)
(let-symbolic ([(x) integer? : Int])
x))
(check-type (always-same) : Int)
(check-type (eq? (always-same) (always-same)) : Bool -> #t)
(define (always-different -> Int)
(let-symbolic* ([(x) integer? : Int])
x))
(check-type (always-different) : Int)
(define diff-sym*1 (always-different))
(define diff-sym*2 (always-different))
(check-type (eq? diff-sym*1 diff-sym*2) : Bool -> (= diff-sym*1 diff-sym*2))
;; 3.2.2 Assertions
(check-type+asserts (assert #t) : Unit -> (void) (list))
(check-type+asserts (assert 1) : Unit -> (void) (list))
(define-symbolic x123 boolean? : Bool)
(check-type+asserts (assert x123) : Unit -> (void) (list x123))
(check-runtime-exn (assert #f "bad value"))
(check-type (asserts) : (CListof Bool) -> (list #f))
(check-type (clear-asserts!) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list))
;; 3.2.3 Angelic Execution
(define-symbolic x y boolean? : Bool)
(check-type (assert x) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list x))
(define solve-sol (solve (assert y)))
(check-type solve-sol : CSolution)
(check-type (sat? solve-sol) : Bool -> #t)
(check-type (evaluate x solve-sol) : Bool -> #t) ; x must be true
(check-type (evaluate y solve-sol) : Bool -> #t) ; y must be true
(check-type (solve (assert (not x))) : CSolution -> (unsat))
(clear-asserts!)
;; 3.2.4 Verification
(check-type (assert x) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list x))
(define verif-sol (verify (assert y)))
(check-type (asserts) : (CListof Bool) -> (list x))
(check-type (evaluate x verif-sol) : Bool -> #t) ; x must be true
(check-type (evaluate y verif-sol) : Bool -> #f) ; y must be false
(check-type (verify #:assume (assert y) #:guarantee (assert (and x y)))
: CSolution -> (unsat))
(clear-asserts!)
;; 3.2.5 Synthesis
(define-symbolic synth-x synth-c integer? : Int)
(check-type (assert (even? synth-x)) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
(define synth-sol
(synthesize #:forall (list synth-x)
#:guarantee (assert (odd? (+ synth-x synth-c)))))
(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
(check-type (evaluate synth-x synth-sol) : Int -> synth-x) ; x is unbound
(check-type (evaluate synth-c synth-sol) : Int -> 1) ; c must an odd integer
(clear-asserts!)
;; 3.2.6 Optimization
(current-bitwidth #f) ; use infinite-precision arithmetic
(define-symbolic opt-x opt-y integer? : Int)
(check-type (assert (< opt-x 2)) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
(define opt-sol
(optimize #:maximize (list (+ opt-x opt-y))
#:guarantee (assert (< (- opt-y opt-x) 1))))
; assertion store same as before
(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
; x + y is maximal at x = 1 and y = 1
(check-type (evaluate opt-x opt-sol) : Int -> 1)
(check-type (evaluate opt-y opt-sol) : Int -> 1)
;; 3.2.8 Reasoning Precision
;; see rosette-guide-sec2-tests.rkt, Sec 2.4 Symbolic Reasoning

5
turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
View File

@ -4,10 +4,15 @@
(require "rosette-guide-sec2-tests.rkt")
(require "rosette-guide-sec3-tests.rkt")
(require "bv-tests.rkt")
;(require "bv-ref-tests.rkt")
; visit but dont instantiate, o.w. will get unsat
;(dynamic-require "fsm-test.rkt" #f)
<<<<<<< HEAD
(require "ifc-tests.rkt")
; don't run this file for testing:
(module test racket/base)
=======
;(require "ifc-tests.rkt")
>>>>>>> add optimize, remaining sec3 tests; fix CList-CListof subtyping