#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? #:length 5)
(define-symbolic xl i integer?)
(define ys (take xs xl)) 
(verify
 (begin
   (assume (<= 0 i (- xl 1)))
   (assert (search (list-ref ys i) ys))))

; let's clear the verification condition:
; note that (take xs xl) introduces assertions.
(vc)
(clear-vc!)

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

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

(define (factorial n)
  (cond [(= n 0) 1]
        [else (* n (factorial (- n 1)))]))

(define-symbolic k integer?)

(with-handlers ([exn:fail? (lambda (e) (displayln (exn-message e)))])
  (call-with-limits
   3 ; seconds
   #f ; unlimited memory
   (thunk
    (with-terms 
      (solve (assert (> (factorial k) 10)))))))

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

(define (factorial-bounded n g)
  (assert (>= g 0))
  (cond [(= n 0) 1]
        [else (* n (factorial-bounded (- n 1) (- g 1)))]))

(solve ; no solution because the bound is too small
 (assert (> (factorial-bounded k 3) 10)))

(solve ; no solution because the bound is too small
 (assert (> (factorial-bounded k 4) 10)))


; 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)