add remaining logic ops; add sec4 tests; TODO: add hash and fix sol ops
This commit is contained in:
Stephen Chang
parent
f22619f47b
commit
4007d64ff1
|
|
@ -11,6 +11,8 @@ Is concrete? broken?
|
|||
Rosette TODO:
|
||||
- fix documentation of synthesize
|
||||
- #:forall accepts everything, not just constant?s
|
||||
- doc typo: core
|
||||
- Returns the unsatisfiable core stored in the given satisfiable solution
|
||||
|
||||
Rosette use case questions:
|
||||
- does the predicate in define-symbolic need to be an arbitrary expression?
|
||||
|
|
|
|||
|
|
@ -561,6 +561,7 @@
|
|||
(provide (rosette-typed-out [printf : (Ccase-> (C→ CString CUnit)
|
||||
(C→ CString Any CUnit)
|
||||
(C→ CString Any Any CUnit))]
|
||||
[displayln : (C→ Any CUnit)]
|
||||
[error : (Ccase-> (C→ (CU CString CSymbol) Nothing)
|
||||
(C→ CSymbol CString Nothing))]
|
||||
[void : (C→ CUnit)]
|
||||
|
|
@ -706,7 +707,9 @@
|
|||
(C→ Num Num))]
|
||||
[truncate : (Ccase-> (C→ CNum CNum)
|
||||
(C→ Num Num))]
|
||||
[sgn : (Ccase-> (C→ CInt CInt)
|
||||
[sgn : (Ccase-> (C→ CZero CZero)
|
||||
(C→ Zero Zero)
|
||||
(C→ CInt CInt)
|
||||
(C→ Int Int)
|
||||
(C→ CNum CNum)
|
||||
(C→ Num Num))]
|
||||
|
|
@ -834,8 +837,7 @@
|
|||
[bitvector->natural : (C→ BV Nat)]
|
||||
[integer->bitvector : (C→ Int BVPred BV)]
|
||||
|
||||
[bitvector-size : (C→ CBVPred CPosInt)]
|
||||
|
||||
[bitvector-size : (C→ CBVPred CPosInt)]))
|
||||
|
||||
;; ---------------------------------
|
||||
;; Uninterpreted functions
|
||||
|
|
@ -848,9 +850,9 @@
|
|||
|
||||
;; ---------------------------------
|
||||
;; Logic operators
|
||||
|
||||
[! : (C→ Bool Bool)]
|
||||
[<=> : (C→ Bool Bool Bool)]))
|
||||
(provide (rosette-typed-out [! : (C→ Bool Bool)]
|
||||
[<=> : (C→ Bool Bool Bool)]
|
||||
[=> : (C→ Bool Bool Bool)]))
|
||||
|
||||
(define-typed-syntax &&
|
||||
[(_ e ...) ≫
|
||||
|
|
@ -914,14 +916,18 @@
|
|||
|
||||
(define-base-types CSolution CPict)
|
||||
|
||||
(provide (rosette-typed-out [core : (C→ Any Any)]
|
||||
(provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
|
||||
; TODO: implement hash
|
||||
[model : (C→ CSolution Any)]
|
||||
[sat : (Ccase-> (C→ CSolution)
|
||||
(C→ Any CSolution))]
|
||||
[sat? : (C→ Any Bool)]
|
||||
[unsat? : (C→ Any Bool)]
|
||||
[unsat : (Ccase-> (C→ CSolution)
|
||||
(C→ (CListof Bool) CSolution))]
|
||||
[forall : (C→ (CListof Any) Bool Bool)]
|
||||
[exists : (C→ (CListof Any) Bool Bool)]))
|
||||
|
||||
|
||||
(define-typed-syntax verify
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : _]]
|
||||
|
|
|
|||
245
turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
Normal file
245
turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
Normal file
|
|
@ -0,0 +1,245 @@
|
|||
#lang s-exp "../../rosette/rosette2.rkt"
|
||||
(require "../rackunit-typechecking.rkt"
|
||||
"check-type+asserts.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4
|
||||
|
||||
;; 4.1 Equality
|
||||
|
||||
;; should equal? produce CBool?
|
||||
;; (check-type (equal? 1 #t) : CBool -> #f)
|
||||
;; (check-type (equal? 1 1.0) : CBool -> #t)
|
||||
;; (check-type (equal? (list 1) (list 1.0)) : CBool -> #t)
|
||||
;; (check-type (equal? (box 1) (box 1)) : CBool -> #t)
|
||||
;; (check-type (equal? (box 1) (box 1.0)) : CBool -> #t)
|
||||
;; (check-type (equal? (list (box 1)) (list (box 1))) : CBool -> #t)
|
||||
;; (check-type (equal? (list (box 1)) (list (box 1.0))) : CBool -> #t)
|
||||
(check-type (equal? 1 #t) : Bool -> #f)
|
||||
(check-type (equal? 1 1.0) : Bool -> #t)
|
||||
(check-type (equal? (list 1) (list 1.0)) : Bool -> #t)
|
||||
(check-type (equal? (box 1) (box 1)) : Bool -> #t)
|
||||
(check-type (equal? (box 1) (box 1.0)) : Bool -> #t)
|
||||
(check-type (equal? (list (box 1)) (list (box 1))) : Bool -> #t)
|
||||
(check-type (equal? (list (box 1)) (list (box 1.0))) : Bool -> #t)
|
||||
|
||||
(define-symbolic n integer? : Int)
|
||||
(check-type (equal? n 1) : Bool -> (= 1 n))
|
||||
(check-type (equal? (box n) (box 1)) : Bool -> (= 1 n))
|
||||
(check-not-type (equal? n 1) : CBool)
|
||||
(check-not-type (equal? (box n) (box 1)) : CBool)
|
||||
(define-symbolic f g (~> integer? integer?) : (→ Int Int))
|
||||
(typecheck-fail
|
||||
(define-symbolic f g (~> integer? integer?) : (C→ Int Int))
|
||||
#:with-msg "symbolic value cannot have a concrete type")
|
||||
(check-type f : (→ Int Int))
|
||||
(check-type g : (→ Int Int))
|
||||
(check-type (equal? f g) : Bool -> #f)
|
||||
(check-type (f 1) : Int -> (f 1))
|
||||
|
||||
(check-type (eq? 1 #t) : Bool -> #f)
|
||||
(check-type (eq? 1 1.0) : Bool -> #t) ; equal? transparent solvable values
|
||||
(check-type (eq? (list 1) (list 1.0)) : Bool -> #t) ; transparent immutable values with eq? contents
|
||||
(check-type (eq? (box 1) (box 1)) : Bool -> #f); but boxes are mutable, so eq? follows Racket
|
||||
(check-type (eq? (list (box 1)) (list (box 1))) : Bool -> #f)
|
||||
(check-type (eq? n 1) : Bool -> (= 1 n))
|
||||
(check-type (eq? (box n) (box 1)) : Bool -> #f)
|
||||
(check-type (eq? f g) : Bool -> #f) ; and procedures are opaque, so eq? follows Racket
|
||||
(check-type (eq? f f) : Bool -> #t)
|
||||
|
||||
(check-type (distinct?) : Bool -> #t)
|
||||
(check-type (distinct? 1) : Bool -> #t)
|
||||
(check-type (distinct? (list 1 2) (list 3) (list 1 2)) : Bool -> #f)
|
||||
(define-symbolic x y z integer? : Int)
|
||||
(check-type (distinct? 3 z x y 2) : Bool -> (distinct? 2 3 x y z))
|
||||
(define-symbolic b boolean? : Bool)
|
||||
(check-type (distinct? 3 (bv 3 4) (list 1) (list x) y 2)
|
||||
: Bool -> (&& (! (= 3 y)) (&& (! (= 1 x)) (! (= 2 y)))))
|
||||
(clear-asserts!)
|
||||
|
||||
;; 4.2 Booleans, Integers, and Reals
|
||||
|
||||
;(define-symbolic b boolean? : Bool)
|
||||
(check-type (boolean? b) : Bool -> #t)
|
||||
(check-type (boolean? #t) : Bool -> #t)
|
||||
(check-type (boolean? #f) : Bool -> #t)
|
||||
(check-type (boolean? true) : Bool -> #t)
|
||||
(check-type (boolean? false) : Bool -> #t)
|
||||
(check-type (boolean? 1) : Bool -> #f)
|
||||
(check-type (not b) : Bool -> (! b))
|
||||
|
||||
(check-type (nand) : CFalse -> #f)
|
||||
(check-type (nand #t #t) : Bool -> #f)
|
||||
(check-type (nand 1 2) : Bool -> #f)
|
||||
(check-type (nor) : CTrue -> #t)
|
||||
(check-type (nor #f #f) : Bool -> #t)
|
||||
(check-type (nor 1 2) : Bool -> #f)
|
||||
|
||||
(check-type (nand #f #t) : Bool -> #t)
|
||||
(check-type (nand #f (error 'ack "we don't get here")) : Bool -> #t)
|
||||
(check-type (nor #f #t) : Bool -> #f)
|
||||
(check-type (nor #t (error 'ack "we don't get here")) : Bool -> #f)
|
||||
(check-type (implies #f #t) : Bool -> #t)
|
||||
(check-type (implies #f #f) : Bool -> #t)
|
||||
(check-type (implies #t #f) : Bool -> #f)
|
||||
(check-type (implies #f (error 'ack "we don't get here")) : Bool -> #t)
|
||||
;; (check-type (xor 11 #f) : Any -> 11)
|
||||
;; (check-type (xor #f 22) : Any -> 22)
|
||||
;; (check-type (xor 11 22) : Any -> #f)
|
||||
;; (check-type (xor #f #f) : Any -> #f)
|
||||
|
||||
(check-type +inf.0 : CFloat)
|
||||
(check-type -inf.0 : CFloat)
|
||||
(check-type +nan.0 : CFloat)
|
||||
(check-type -nan.0 : CFloat)
|
||||
|
||||
(check-type (number? 1) : Bool -> #t)
|
||||
(typecheck-fail (number? 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (number? "hello") : Bool -> #f)
|
||||
(check-type (real? 1) : Bool -> #t)
|
||||
(check-type (real? +inf.0) : Bool -> #t)
|
||||
(typecheck-fail (real? 2+3i) #:with-msg "Unsupported literal")
|
||||
(typecheck-fail (real? 2.0+0.0i) #:with-msg "Unsupported literal")
|
||||
(check-type (real? "hello") : Bool -> #f)
|
||||
(check-type (integer? 1) : Bool -> #t)
|
||||
(check-type (integer? 2.3) : Bool -> #f)
|
||||
(check-type (integer? 4.0) : Bool -> #t)
|
||||
(check-type (integer? +inf.0) : Bool -> #f)
|
||||
(typecheck-fail (integer? 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (integer? "hello") : Bool -> #f)
|
||||
(check-type (zero? 0) : CBool -> #t)
|
||||
(check-type (zero? -0.0) : CBool -> #t)
|
||||
(check-type (positive? 10) : CBool -> #t)
|
||||
(check-type (positive? -10) : CBool -> #f)
|
||||
(check-type (positive? 0.0) : CBool -> #f)
|
||||
(check-type (negative? 10) : CBool -> #f)
|
||||
(check-type (negative? -10) : CBool -> #t)
|
||||
(check-type (negative? -0.0) : CBool -> #f)
|
||||
(check-type (even? 10.0) : CBool -> #t)
|
||||
(check-type (even? 11) : CBool -> #f)
|
||||
(check-type +inf.0 : CNum)
|
||||
(typecheck-fail (even? +inf.0) #:with-msg "expected.*Int")
|
||||
(check-type (odd? 10.0) : Bool -> #f)
|
||||
(check-type (odd? 11) : Bool -> #t)
|
||||
(typecheck-fail (odd? +inf.0) #:with-msg "expected.*Int")
|
||||
(check-type (inexact->exact 1) : CNum -> 1)
|
||||
(check-type (inexact->exact 1.0) : CNum -> 1)
|
||||
(check-type (exact->inexact 1) : CNum -> 1.0)
|
||||
(check-type (exact->inexact 1.0) : CNum -> 1.0)
|
||||
|
||||
(check-type (+ 1 2) : CInt -> 3)
|
||||
(typecheck-fail (+ 1.0 2+3i 5) #:with-msg "Unsupported literal")
|
||||
(check-type (+) : CInt -> 0)
|
||||
(check-type (- 5 3.0) : CInt -> 2.0)
|
||||
(check-type (- 1) : CInt -> -1)
|
||||
(typecheck-fail (- 2+7i 1 3) #:with-msg "Unsupported literal")
|
||||
(check-type (* 2 3) : CInt -> 6)
|
||||
(check-type (* 8.0 9) : CInt -> 72.0)
|
||||
(typecheck-fail (* 1+2i 3+4i) #:with-msg "Unsupported literal")
|
||||
(check-type (/ 3 4) : CNum -> 3/4)
|
||||
(check-type (/ 81 3 3) : CNum -> 9)
|
||||
(check-type (/ 10.0) : CNum -> 0.1)
|
||||
(typecheck-fail (/ 1+2i 3+4i) #:with-msg "Unsupported literal")
|
||||
(check-type (quotient 10 3) : CInt -> 3)
|
||||
(check-type (quotient -10.0 3) : CInt -> -3.0)
|
||||
(typecheck-fail (quotient +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (remainder 10 3) : CInt -> 1)
|
||||
(check-type (remainder -10.0 3) : CInt -> -1.0)
|
||||
(check-type (remainder 10.0 -3) : CInt -> 1.0)
|
||||
(check-type (remainder -10 -3) : CInt -> -1)
|
||||
(typecheck-fail (remainder +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (modulo 10 3) : CInt -> 1)
|
||||
(check-type (modulo -10.0 3) : CInt -> 2.0)
|
||||
(check-type (modulo 10.0 -3) : CInt -> -2.0)
|
||||
(check-type (modulo -10 -3) : CInt -> -1)
|
||||
(typecheck-fail (modulo +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (abs 1.0) : CInt -> 1.0)
|
||||
(check-type (abs -1) : CInt -> 1)
|
||||
(check-type (max 1 3 2) : CInt -> 3)
|
||||
(check-type (max 1 3 2.0) : CInt -> 3) ; Racket coerces to inexact, but Rosette does not?
|
||||
(check-type (min 1 3 2) : CInt -> 1)
|
||||
(check-type (min 1 3 2.0) : CInt -> 1) ; Racket coerces to inexact, but Rosette does not?
|
||||
(check-type (floor 17/4) : CNum -> 4)
|
||||
(check-type (floor -17/4) : CNum -> -5)
|
||||
(check-type (floor 2.5) : CNum -> 2.0)
|
||||
(check-type (floor -2.5) : CNum -> -3.0)
|
||||
(check-type (floor +inf.0) : CNum -> +inf.0)
|
||||
(check-type (ceiling 17/4) : CNum -> 5)
|
||||
(check-type (ceiling -17/4) : CNum -> -4)
|
||||
(check-type (ceiling 2.5) : CNum -> 3.0)
|
||||
(check-type (ceiling -2.5) : CNum -> -2.0)
|
||||
(check-type (ceiling +inf.0) : CNum -> +inf.0)
|
||||
(check-type (truncate 17/4) : CNum -> 4)
|
||||
(check-type (truncate -17/4) : CNum -> -4)
|
||||
(check-type (truncate 2.5) : CNum -> 2.0)
|
||||
(check-type (truncate -2.5) : CNum -> -2.0)
|
||||
(check-type (truncate +inf.0) : CNum -> +inf.0)
|
||||
(check-type (= 1 1.0) : CBool -> #t)
|
||||
(check-type (= 1 2) : CBool -> #f)
|
||||
(typecheck-fail (= 2+3i 2+3i 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (< 1 1) : CBool -> #f)
|
||||
(check-type (< 1 2 3) : CBool -> #t)
|
||||
(check-type (< 1 +inf.0) : CBool -> #t)
|
||||
(check-type (< 1 +nan.0) : CBool -> #f)
|
||||
(check-type (<= 1 1) : CBool -> #t)
|
||||
(check-type (<= 1 2 1) : CBool -> #f)
|
||||
(check-type (> 1 1) : CBool -> #f)
|
||||
(check-type (> 3 2 1) : CBool -> #t)
|
||||
(check-type (> +inf.0 1) : CBool -> #t)
|
||||
(check-type (> +nan.0 1) : CBool -> #f)
|
||||
(check-type (>= 1 1) : CBool -> #t)
|
||||
(check-type (>= 1 2 1) : CBool -> #f)
|
||||
(check-type (expt 2 3) : CInt -> 8)
|
||||
(check-type (expt 4 0.5) : CNum -> 2.0)
|
||||
(check-type (expt +inf.0 0) : CInt -> 1)
|
||||
(check-type pi : CNum -> 3.141592653589793)
|
||||
(check-type (sgn 10) : CInt -> 1)
|
||||
(check-type (sgn -10.0) : CInt -> -1.0)
|
||||
(check-type (sgn 0) : CInt -> 0)
|
||||
(check-type (sgn +nan.0) : CNum -> +nan.0)
|
||||
|
||||
(clear-asserts!)
|
||||
|
||||
;; 4.2.1 Additional Logic Operators
|
||||
(check-type (! #f) : Bool -> #t)
|
||||
(check-type (! #t) : Bool -> #f)
|
||||
; this typechecks only when b is true
|
||||
(check-type (! (assert-type (if b #f 3) : Bool)) : Bool -> #t)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
(check-type (&&) : Bool -> #t)
|
||||
(check-type (||) : Bool -> #f)
|
||||
; no shortcircuiting
|
||||
(check-type (&& #f (begin (displayln "hello") #t)) : Bool -> #f)
|
||||
(define-symbolic a boolean? : Bool)
|
||||
; this typechecks only when b is true
|
||||
(check-type (&& a (assert-type (if b #t 1) : Bool)) : Bool -> a)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
; no shortcircuiting
|
||||
(check-type (=> #f (begin (displayln "hello") #f)) : Bool -> #t)
|
||||
; this typechecks only when b is true
|
||||
(check-type (<=> a (assert-type (if b #t 1) : Bool)) : Bool -> a)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
|
||||
(current-bitwidth #f)
|
||||
|
||||
(define-symbolic a1 b1 integer? : Int)
|
||||
(check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1))
|
||||
(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
|
||||
; so the model has no bindings
|
||||
(define sol1 (solve (assert f1)))
|
||||
(check-type sol1 : CSolution) ; -> (sat) ; TODO: how to check empty model?
|
||||
(check-type (sat? sol1) : Bool -> #t)
|
||||
(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b is free in g
|
||||
; so the model has a binding for b
|
||||
(define sol2 (solve (assert g1)))
|
||||
(check-type sol2 : CSolution)
|
||||
(check-type (sat? sol2) : Bool -> #t)
|
||||
(check-type (evaluate b1 sol2) : Int -> 0)
|
||||
(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1))))) ; body refers to the innermost a
|
||||
; so h is unsatisfiable.
|
||||
(check-type (solve (assert h)) : CSolution -> (unsat))
|
||||
Loading…
Reference in New Issue
Block a user