queue-rosette.rkt

#lang s-exp rosette

(require "queue-racket.rkt" "special.rkt" "ops-rosette.rkt")
(provide queue-in-rosette% queue-out-rosette%)

(define queue-in-rosette%
  (class* special% (equal<%> printable<%>)
    (super-new)
    (init-field get-fresh-val
                [size 4]
                [init (make-vector size #f)]
                [queue (make-vector size #f)]
                [ref #f])

    (public pop create-concrete clone)

    (define/public (custom-print port depth)
      (print `(queue-in-rosette% content: ,init ,queue) port depth))

    (define/public (custom-write port)
      (write `(queue-in-rosette% content: ,init ,queue) port))

    (define/public (custom-display port)
      (display `(queue-in-rosette% content: ,init ,queue) port))

    (define/public (equal-to? other recur)
      (and (is-a? other queue-in-rosette%)
           (equal? queue (get-field* queue other))))
      
    (define/public (equal-hash-code-of hash-code)
      (hash-code queue))

    (define/public (equal-secondary-hash-code-of hash-code)
      (hash-code queue))

    (define (get-size [index 0])
      (if (vector-ref queue index)
          (get-size (add1 index))
          index))
    
    ;; Create concrete memory object by evaluating symbolic memory.
    (define (create-concrete eval)
      (new queue-in-racket% [queue (eval init)]))        
    
    ;; Clone a new queue object with the same queue.
    ;; Use this method to clone new memory for every program interpretation.
    (define (clone [ref #f])
      (new queue-in-rosette% [ref ref] [init init] [queue (vector-copy queue)]
           [get-fresh-val get-fresh-val]))

    (define (pop-spec)
      (define size (get-size))
      (define val (vector-ref init size))
      (unless val
              (set! val (get-fresh-val))
              (vector-set! init size val))
      (vector-set! queue size val)
      val)

    (define (pop-cand)
      (define size (get-size))
      (define val (vector-ref init size))
      (vector-set! queue size val)
      val)

    (define (pop)
      (if ref (pop-cand) (pop-spec)))
    
    ))

(define queue-out-rosette%
  (class* special% (equal<%> printable<%>)
    (super-new)
    (init-field get-fresh-val
                [ref #f]
                [size 4]
                [queue (make-vector size #f)])

    (public push create-concrete clone)

    (define/public (custom-print port depth)
      (print `(queue-out-rosette% content: ,queue size: ,(get-size)) port depth))

    (define/public (custom-write port)
      (write `(queue-out-rosette% content: ,queue size: ,(get-size)) port))

    (define/public (custom-display port)
      (display `(queue-out-rosette% content: ,queue size: ,(get-size)) port))

    (define/public (equal-to? other recur)
      ;; (pretty-display `(equal-to? ,queue ,(get-field queue other)
      ;;                             ,(and (is-a? other queue-out-rosette%)
      ;;                                   (equal? queue (get-field queue other)))))
      (and (is-a? other queue-out-rosette%)
           (equal? queue (get-field* queue other))))
      
    (define/public (equal-hash-code-of hash-code)
      (hash-code queue))

    (define/public (equal-secondary-hash-code-of hash-code)
      (hash-code queue))

    (define (get-size [index 0])
      (if (vector-ref queue index)
          (get-size (add1 index))
          index))

    (define/public (get-at index) (vector-ref queue index))

    ;; Create concrete memory object by evaluating symbolic memory.
    (define (create-concrete eval)
      (new queue-out-racket% [queue (eval queue)]))               
    
    ;; Clone a new queue object with the same queue.
    ;; Use this method to clone new memory for every program interpretation.
    (define (clone [ref #f])
      (new queue-out-rosette% [ref ref] [queue (vector-copy queue)] [get-fresh-val get-fresh-val]))
    
    (define (push-spec val)
      (vector-set! queue (get-size) val))

    (define (push-cand val)
      (define size (get-size))
      (define val-ref (send* ref get-at size))
      (assert (equal? val val-ref) "push-cand: push a value different from spec does")
      (vector-set! queue size val))

    (define (push val)
      (if ref (push-cand val) (push-spec val)))
    
    ))

(define (test1)
  (define func (lambda () (define-symbolic* val number?) val))
  (define q-init (new queue-in-rosette% [get-fresh-val func]))
  (define q (send q-init clone))
  (pretty-display `(pop ,(send q pop)))
  (pretty-display `(pop ,(send q pop)))
  (pretty-display `(queue-init ,q-init))
  (pretty-display `(queue ,q))

  (define q1 (send q-init clone q))
  (pretty-display `(pop ,(send q1 pop)))
  (pretty-display `(queue-init ,q1))
  (pretty-display `(pop ,(send q1 pop)))
  (pretty-display `(pop ,(send q1 pop))) ;; assert: pop-cand: pop more than spec does
  )

(define (test2)
  (define func (lambda () (define-symbolic* val number?) val))
  (define q-init (new queue-out-rosette% [get-fresh-val func]))
  (define q (send q-init clone))
  (send q push 1)
  (send q push 2)
  (pretty-display `(queue-init ,q-init))
  (pretty-display `(queue ,q))

  (define q2 (send q-init clone q))
  (send q2 push 1)
  (pretty-display `(queue ,q2))
  (send q2 push 22) ;; assert: push-cand: push a value different from spec does
  )