rosette-guide-sec2-tests.rkt (6424B)
1 #lang s-exp "../../rosette/rosette2.rkt" 2 (require "../rackunit-typechecking.rkt" 3 "check-type+asserts.rkt") 4 5 ;; all examples from the Rosette Guide, Sec 2 6 7 (define-symbolic b boolean? : Bool) 8 (check-type b : Bool) 9 (check-type (boolean? b) : Bool -> #t) 10 (check-type (integer? b) : Bool -> #f) 11 12 ;; TODO: fix these tests 13 (check-type (vector b 1) : (CMVectorof (U Bool CPosInt)) -> (vector b 1)) 14 (check-not-type (vector b 1) : (CIVectorof (U Bool CPosInt))) 15 (check-not-type (vector b 1) : (CMVectorof (CU CBool CPosInt))) 16 ;; but this is ok 17 (check-type (vector b 1) : (CMVectorof (U CBool CPosInt))) 18 ;; mutable vectors are invariant 19 (check-not-type (vector b 1) : (CMVectorof (U Bool CInt))) 20 (check-type (vector b 1) : (CVectorof (U Bool PosInt))) 21 ;; vectors are also invariant, because it includes mvectors 22 (check-not-type (vector b 1) : (CVectorof (U Bool CInt))) 23 (check-not-type (vector b 1) : (CVectorof (U Bool Int))) 24 25 (check-type (not b) : Bool -> (! b)) 26 (check-type (boolean? (not b)) : Bool -> #t) 27 28 (define-symbolic* n integer? : Int) 29 30 ;; TODO: support internal definition contexts 31 (define (static -> Bool) 32 (let-symbolic ([(x) boolean? : Bool]) x)) 33 #;(define (static -> Bool) 34 (define-symbolic x boolean? : Bool) ; creates the same constant when evaluated 35 x) 36 37 (define (dynamic -> Int) 38 (let-symbolic* ([(y) integer? : Int]) y)) 39 #;(define (dynamic -> Int) 40 (define-symbolic* y integer? : Int) ; creates a different constant when evaluated 41 y) 42 43 (check-type static : (C→ Bool)) 44 (check-not-type static : (C→ CBool)) 45 (check-type dynamic : (C→ Int)) 46 (check-type dynamic : (C→ Num)) 47 (check-not-type dynamic : (C→ CInt)) 48 (check-type (eq? (static) (static)) : Bool -> #t) 49 50 (define sym*1 (dynamic)) 51 (define sym*2 (dynamic)) 52 (check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2)) 53 54 (define (yet-another-x -> Bool) 55 (let-symbolic ([(x) boolean? : Bool]) x)) 56 57 (check-type (eq? (static) (yet-another-x)) 58 : Bool -> (<=> (static) (yet-another-x))) 59 60 (check-type+asserts (assert #t) : Unit -> (void) (list)) 61 (check-runtime-exn (assert #f)) 62 63 (check-type+asserts (assert (not b)) : Unit -> (void) (list (! b) #f)) 64 65 (check-type (clear-asserts!) : Unit -> (void)) 66 (check-type (asserts) : (CListof Bool) -> (list)) 67 68 ;; sec 2.3 69 (define (poly [x : Int] -> Int) 70 (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x))) 71 72 (define (factored [x : Int] -> Int) 73 (* x (+ x 1) (+ x 2) (+ x 2))) 74 75 (define (same [p : (C→ Int Int)] [f : (C→ Int Int)] [x : Int] -> Unit) 76 (assert (= (p x) (f x)))) 77 78 ; check zeros; all seems well ... 79 (check-type+asserts (same poly factored 0) : Unit -> (void) (list)) 80 (check-type+asserts (same poly factored -1) : Unit -> (void) (list)) 81 (check-type+asserts (same poly factored -2) : Unit -> (void) (list)) 82 83 ;; 2.3.1 Verification 84 85 (define-symbolic i integer? : Int) 86 (define cex (verify (same poly factored i))) 87 (check-type cex : CSolution) 88 (check-type (sat? cex) : Bool -> #t) 89 (check-type (unsat? cex) : Bool -> #f) 90 (check-type (evaluate i cex) : Int -> 12) 91 (check-runtime-exn (same poly factored 12)) 92 (clear-asserts!) 93 94 ;; 2.3.2 Debugging 95 96 (require "../../rosette/query/debug.rkt" 97 "../../rosette/lib/render.rkt") 98 (define/debug (factored/d [x : Int] -> Int) 99 (* x (+ x 1) (+ x 2) (+ x 2))) 100 101 (define ucore (debug [integer?] (same poly factored/d 12))) 102 (check-type ucore : CSolution) 103 ;; TESTING TODO: requires visual inspection (in DrRacket) 104 (check-type (render ucore) : CPict) 105 106 ;; 2.3.3 Synthesis 107 108 (require "../../rosette/lib/synthax.rkt") 109 (define (factored/?? [x : Int] -> Int) 110 (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??)))) 111 112 (define binding 113 (synthesize #:forall (list i) 114 #:guarantee (same poly factored/?? i))) 115 (check-type binding : CSolution) 116 (check-type (sat? binding) : Bool -> #t) 117 (check-type (unsat? binding) : Bool -> #f) 118 ;; TESTING TODO: requires visual inspection of stdout 119 (check-type (print-forms binding) : Unit -> (void)) 120 ;; typed/rosette should print: 121 ;; '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0))) 122 ;; (untyped) rosette should print: 123 ;; '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0))) 124 125 ;; 2.3.4 Angelic Execution 126 127 (define-symbolic x y integer? : Int) 128 (define sol 129 (solve (begin (assert (not (= x y))) 130 (assert (< (abs x) 10)) 131 (assert (< (abs y) 10)) 132 (assert (not (= (poly x) 0))) 133 (assert (= (poly x) (poly y)))))) 134 (check-type sol : CSolution) 135 (check-type (sat? sol) : Bool -> #t) 136 (check-type (unsat? sol) : Bool -> #f) 137 (check-type (evaluate x sol) : Int -> -5) 138 (check-type (evaluate y sol) : Int -> 2) 139 (check-type (evaluate (poly x) sol) : Int -> 120) 140 (check-type (evaluate (poly y) sol) : Int -> 120) 141 142 ;; 2.4 Symbolic Reasoning 143 144 (define-symbolic x1 y1 real? : Num) 145 (check-type (current-bitwidth) : (CU CPosInt CFalse) -> 5) 146 (check-type (current-bitwidth #f) : CUnit -> (void)) 147 (check-type (current-bitwidth) : (CU CPosInt CFalse) -> #f) 148 (check-not-type (current-bitwidth) : CFalse) 149 (typecheck-fail (current-bitwidth #t) #:with-msg "expected \\(CU CFalse CPosInt\\), given True") 150 (typecheck-fail (current-bitwidth 0) #:with-msg "expected \\(CU CFalse CPosInt\\), given Zero") 151 (typecheck-fail (current-bitwidth -1) #:with-msg "expected \\(CU CFalse CPosInt\\), given NegInt") 152 (check-type (current-bitwidth 5) : CUnit -> (void)) 153 154 ; there is no solution under 5-bit signed integer semantics 155 (check-type (solve (assert (= x1 3.5))) : CSolution -> (unsat)) 156 (check-type (solve (assert (= x1 64))) : CSolution -> (unsat)) 157 158 ; and quantifiers are not supported 159 (check-runtime-exn (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) 160 ;; expected err: 161 ;; finitize: cannot use (current-bitwidth 5) with a quantified formula 162 ;; (forall (x1) (= x1 (+ x1 y1))); use (current-bitwidth #f) instead 163 164 ;; infinite precision semantics 165 (current-bitwidth #f) 166 167 (define sol1 (solve (assert (= x1 3.5)))) 168 ;; sol1 = (model [x1 7/2]) 169 (check-type sol1 : CSolution) 170 (check-type (sat? sol1) : Bool -> #t) 171 (check-type (evaluate x1 sol1) : Num -> 7/2) 172 173 (define sol2 (solve (assert (= x1 64)))) 174 ;; sol2 = (model [x1 64.0]) 175 (check-type sol2 : CSolution) 176 (check-type (sat? sol2) : Bool -> #t) 177 (check-type (evaluate x1 sol2) : Num -> 64.0) 178 179 ;; and quantifiers work 180 (define sol3 (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) 181 ;; sol3 = (model [y1 0.0]) 182 (check-type sol3 : CSolution) 183 (check-type (sat? sol3) : Bool -> #t) 184 (check-type (evaluate y1 sol3) : Num -> 0.0)