#lang rosette

; default bitwidth is #f
(displayln "----- current-bitwidth #f -----")

(current-bitwidth)
(define-symbolic x integer?)
(solve (assert (= x 64)))
(verify (assert (not (= x 64))))

; change the bitwidth to 5
(displayln "----- current-bitwidth 5 -----")

(current-bitwidth 5)
(solve (assert (= x 64)))
(verify (assert (not (= x 64))))

; okay, let's go back to #f 

(current-bitwidth #f)

; self-finitization
(displayln "----- self-finitization -----")

(define (search x xs)
  (cond
    [(null? xs) #f]
    [(equal? x (car xs)) #t]
    [else (search x (cdr xs))]))

(define-symbolic xs integer? [5])
(define-symbolic xl i integer?)
(define ys (take xs xl))
(verify
 (when (<= 0 i (- xl 1))
   (assert (search (list-ref ys i) ys))))

; let's clear the assertion stack:
; note that (take xs xl) introduces assertions.
(asserts)
(clear-asserts!)

; unbounded loops
(require (only-in racket/sandbox call-with-limits))

(displayln "----- unbounded loops -----")

(define (ticker state)
  (lambda (msg)
    (if msg (ticker (+ 1 state)) state)))

(define (ff t k)
  (if (> k 0) 
      (ff (t #t) (- k 1)) 
      t))

(define-symbolic s k integer?)

(with-handlers ([exn:fail? (lambda (e) (displayln (exn-message e)))])
  (call-with-limits
   3 ; seconds
   #f ; unlimited memory
   (thunk
    (parameterize ([term-cache (hash-copy (term-cache))])
      (verify
       (let ([t (ticker s)])
         (assert (= ((ff t k) #f) 
                    (+ (max 0 k) (t #f))))))))))

; bounding loops ...
(displayln "----- bounding loops -----")

(define (ffb t k g)
  (assert (> g 0))
  (if (> k 0) 
      (ffb (t #t) (- k 1) (- g 1)) 
      t))

(verify ; cex because ffb fails when k >= g
 (let ([t (ticker s)])
   (assert (= ((ffb t k 5) #f) 
              (+ (max 0 k) (t #f))))))

(verify ; no cex because ffb succeeds when k < g
 (when (< k 5)
   (let ([t (ticker s)])
     (assert (= ((ffb t k 5) #f) 
                (+ (max 0 k) (t #f)))))))

; unsafe features
(displayln "----- unsafe features -----")
(define v (vector 1 2))
(vector-ref v k)

(define h (make-hash '((0 . 1)(1 . 2))))

(with-handlers ([exn:fail? (lambda (e) (displayln (exn-message e)))])
  (hash-ref h k))

(hash-set! h k 3)
(hash-ref h k)