www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

rosette-util.rkt (2147B)

      1 #lang rosette
      2 
      3 (provide assert-pred
      4          bitvector?
      5          zero-integer?
      6          positive-integer?
      7          negative-integer?
      8          nonnegative-integer?)
      9 
     10 (require (only-in rosette [bitvector? concrete-bitvector?]))
     11 
     12 ;; bitvector? : Any -> Bool
     13 (define (bitvector? v)
     14   (for/all ([v v])
     15     (concrete-bitvector? v)))
     16 
     17 ;; assert-pred : A [A -> Bool] -> A
     18 (define (assert-pred a pred)
     19   (if (type? pred)
     20       (type-cast pred a)
     21       (begin
     22         (assert (pred a))
     23         a)))
     24 
     25 ;; zero-integer? : Any -> Bool
     26 (define (zero-integer? x)
     27   (and (integer? x) (zero? x)))
     28 
     29 ;; positive-integer? : Any -> Bool
     30 (define (positive-integer? x)
     31   (and (integer? x) (positive? x)))
     32 
     33 ;; negative-integer? : Any -> Bool
     34 (define (negative-integer? x)
     35   (and (integer? x) (negative? x)))
     36 
     37 ;; nonnegative-integer? : Any -> Bool
     38 (define (nonnegative-integer? x)
     39   (and (integer? x) (not (negative? x))))
     40 
     41 (module+ test
     42   (require rackunit "../tests/rosette/check-asserts.rkt")
     43   (define-symbolic b1 b2 b3 boolean?)
     44 
     45   ;; bitvector?
     46   (check-true (bitvector? (if b1 (bitvector 4) (bitvector 3))))
     47   (check-false (bitvector? (if b1 "bad" 'also-bad)))
     48   (check-equal? (bitvector? (if b1 (bitvector 4) "bad")) b1)
     49   (check-equal? (bitvector? (if b1 "bad" (bitvector 4))) (not b1))
     50   
     51   (check-true (bitvector? (if b1 (bitvector 4) (if b2 (bitvector 3) (bitvector 2)))))
     52   (check-false (bitvector? (if b1 "bad" (if b2 'also-bad 5))))
     53   (check-equal? (bitvector? (if b1 (bitvector 4) (if b2 "bad" (bitvector 2)))) (or b1 (not b2)))
     54   (check-equal? (bitvector? (if b1 "bad" (if b2 (bitvector 4) 'also-bad))) (and (not b1) b2))
     55 
     56   (clear-asserts!)
     57   
     58   ;; assert-pred with type? predicates
     59   (check-equal?/asserts (assert-pred (if b1 1 #f) integer?) 1 (list b1))
     60   (check-equal?/asserts (assert-pred (if b1 1 #f) boolean?) #f (list (not b1)))
     61   (check-equal?/asserts (assert-pred (if b1 (bv 3 4) "bad") (bitvector 4)) (bv 3 4) (list b1))
     62 
     63   ;; assert-pred with non-type? predicates
     64   (check-equal?/asserts (assert-pred (if b1 1 -1) positive?) (if b1 1 -1) (list b1))
     65   (check-equal?/asserts (assert-pred (if b1 1 -1) negative?) (if b1 1 -1) (list (not b1)))
     66   )