From 5436f70de37d2beb95b314c076eb526d9b67c5da Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 31 Aug 2016 16:22:08 -0400 Subject: [PATCH] add remaining Rosette guide, sec2 examples --- turnstile/examples/rosette/rosette-notes.txt | 2 +- turnstile/examples/rosette/rosette2.rkt | 24 ++++++---- .../tests/rosette/rosette-guide-tests.rkt | 48 +++++++++++++++++-- 3 files changed, 60 insertions(+), 14 deletions(-) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index fa180fe..4a71818 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -61,7 +61,7 @@ TODOs: - eg rename existing turnstile to turnstile/lang? - remove my-this-syntax stx param - add symbolic True and False? - +- orig stx prop confuses distinction between symbolic and non-sym values 2016-08-25 -------------------- diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 56213ff..b0bdc63 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -450,16 +450,16 @@ (C→ Num Num Num) (C→ Num Num Num Num) (C→ Num Num Num Num Num))) -(define-rosette-primop = : (Ccase-> (C→ CInt CInt CBool) - (C→ Int Int Bool))) -(define-rosette-primop < : (Ccase-> (C→ CInt CInt CBool) - (C→ Int Int Bool))) -(define-rosette-primop > : (Ccase-> (C→ CInt CInt CBool) - (C→ Int Int Bool))) -(define-rosette-primop <= : (Ccase-> (C→ CInt CInt CBool) - (C→ Int Int Bool))) -(define-rosette-primop >= : (Ccase-> (C→ CInt CInt CBool) - (C→ Int Int Bool))) +(define-rosette-primop = : (Ccase-> (C→ CNum CNum CBool) + (C→ Num Num Bool))) +(define-rosette-primop < : (Ccase-> (C→ CNum CNum CBool) + (C→ Num Num Bool))) +(define-rosette-primop > : (Ccase-> (C→ CNum CNum CBool) + (C→ Num Num Bool))) +(define-rosette-primop <= : (Ccase-> (C→ CNum CNum CBool) + (C→ Num Num Bool))) +(define-rosette-primop >= : (Ccase-> (C→ CNum CNum CBool) + (C→ Num Num Bool))) (define-rosette-primop abs : (Ccase-> (C→ CPosInt CPosInt) (C→ PosInt PosInt) @@ -580,6 +580,10 @@ (define-rosette-primop core : (C→ Any Any)) (define-rosette-primop sat? : (C→ Any Bool)) (define-rosette-primop unsat? : (C→ Any Bool)) +(define-rosette-primop unsat : (Ccase-> (C→ CSolution) + (C→ (CListof Bool) CSolution))) +(define-rosette-primop forall : (C→ (CListof Any) Bool Bool)) +(define-rosette-primop exists : (C→ (CListof Any) Bool Bool)) (define-typed-syntax verify [(_ e) ≫ diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt index b825e93..afc938e 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt @@ -49,9 +49,9 @@ (check-not-type dynamic : (C→ CInt)) (check-type (eq? (static) (static)) : Bool -> #t) -(define y0 (dynamic)) -(define y1 (dynamic)) -(check-type (eq? y0 y1) : Bool -> (= y0 y1)) +(define sym*1 (dynamic)) +(define sym*2 (dynamic)) +(check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2)) (define (yet-another-x -> Bool) (let-symbolic ([(x) boolean? : Bool]) x)) @@ -142,3 +142,45 @@ (check-type (evaluate (poly y) sol) : Int -> 120) ;; 2.4 Symbolic Reasoning + +(define-symbolic x1 y1 real? : Num) +(check-type (current-bitwidth) : (CU CPosInt CFalse) -> 5) +(check-type (current-bitwidth #f) : CUnit -> (void)) +(check-type (current-bitwidth) : (CU CPosInt CFalse) -> #f) +(check-not-type (current-bitwidth) : CFalse) +(typecheck-fail (current-bitwidth #t) #:with-msg "expected \\(CU CFalse CPosInt\\), given True") +(typecheck-fail (current-bitwidth 0) #:with-msg "expected \\(CU CFalse CPosInt\\), given Zero") +(typecheck-fail (current-bitwidth -1) #:with-msg "expected \\(CU CFalse CPosInt\\), given NegInt") +(check-type (current-bitwidth 5) : CUnit -> (void)) + +; there is no solution under 5-bit signed integer semantics +(check-type (solve (assert (= x1 3.5))) : CSolution -> (unsat)) +(check-type (solve (assert (= x1 64))) : CSolution -> (unsat)) + +; and quantifiers are not supported +(check-runtime-exn (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) +;; expected err: +;; finitize: cannot use (current-bitwidth 5) with a quantified formula +;; (forall (x1) (= x1 (+ x1 y1))); use (current-bitwidth #f) instead + +;; infinite precision semantics +(current-bitwidth #f) + +(define sol1 (solve (assert (= x1 3.5)))) +;; sol1 = (model [x1 7/2]) +(check-type sol1 : CSolution) +(check-type (sat? sol1) : Bool -> #t) +(check-type (evaluate x1 sol1) : Num -> 7/2) + +(define sol2 (solve (assert (= x1 64)))) +;; sol2 = (model [x1 64.0]) +(check-type sol2 : CSolution) +(check-type (sat? sol2) : Bool -> #t) +(check-type (evaluate x1 sol2) : Num -> 64.0) + +;; and quantifiers work +(define sol3 (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) +;; sol3 = (model [y1 0.0]) +(check-type sol3 : CSolution) +(check-type (sat? sol3) : Bool -> #t) +(check-type (evaluate y1 sol3) : Num -> 0.0)