;; This file was created by make-log-based-eval
((require (only-in rosette/guide/scribble/util/lifted format-opaque))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((current-bitwidth 5) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((solve (assert (> x 15)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((define (list-set lst idx val)
   (let-values (((front back) (split-at lst idx)))
     (append front (cons val (cdr back)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((list-set '(a b c) 1 'd)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'(a d c)\n"))))
 #""
 #"")
((define-symbolic idx len integer?)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define lst (take '(a b c) len))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((format-opaque "~a" (list-set lst idx 'd))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(union #:size 6 #:hash -437123915298968900)\n"))))
 #""
 #"")
((define (list-set* lst idx val)
   (for/all
    ((lst lst))
    (map
     (lambda (i v) (if (= idx i) val v))
     (build-list (length lst) identity)
     lst)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((list-set* '(a b c) 1 'd)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'(a d c)\n"))))
 #""
 #"")
((format-opaque "~a" (list-set* lst idx 'd))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(union #:size 4 #:hash -976833215883912073)\n"))))
 #""
 #"")
((define-values (width height) (values 5 5))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define grid/2d (for/vector ((_ height)) (make-vector width #f)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((vector-set! (vector-ref grid/2d y) x 'a)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define grid/flat (make-vector (* width height) #f))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((vector-set! grid/flat (+ (* y width) x) 'a)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (maybe-ref lst idx) (if (<= 0 idx 1) (list-ref lst idx) -1))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define-symbolic idx integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((maybe-ref '(5 6 7) idx)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0
    (u
     .
     "(ite\n (&& (<= 0 idx) (<= idx 1))\n (ite* (⊢ (= 0 idx) 5) (⊢ (= 1 idx) 6) (⊢ (= 2 idx) 7))\n -1)\n\n"))))
 #""
 #"")
((define (maybe-ref* lst idx)
   (cond ((= idx 0) (list-ref lst 0)) ((= idx 1) (list-ref lst 1)) (else -1)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((maybe-ref* '(5 6 7) idx)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(ite (= 0 idx) 5 (ite (= 1 idx) 6 -1))\n"))))
 #""
 #"")
((define-values (Add Sub Sqr Nop) (values (bv 0 2) (bv 1 2) (bv 2 2) (bv 3 2)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (calculate prog (acc (bv 0 4)))
   (cond
    ((null? prog) acc)
    (else
     (define ins (car prog))
     (define op (car ins))
     (calculate
      (cdr prog)
      (cond
       ((eq? op Add) (bvadd acc (cadr ins)))
       ((eq? op Sub) (bvsub acc (cadr ins)))
       ((eq? op Sqr) (bvmul acc acc))
       (else acc))))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (list-set lst idx val)
   (match
    lst
    ((cons x xs)
     (if (= idx 0) (cons val xs) (cons x (list-set xs (- idx 1) val))))
    (_ lst)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (sub->add prog idx)
   (define ins (list-ref prog idx))
   (if (eq? (car ins) Sub)
     (list-set prog idx (list Add (bvneg (cadr ins))))
     prog))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (verify-xform xform N)
   (define P
     (for/list
      ((i N))
      (define-symbolic* op (bitvector 2))
      (define-symbolic* arg (bitvector 4))
      (if (eq? op Sqr) (list op) (list op arg))))
   (define-symbolic* acc (bitvector 4))
   (define-symbolic* idx integer?)
   (define xP (xform P idx))
   (verify (assert (eq? (calculate P acc) (calculate xP acc)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((verify-xform sub->add 5)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((clear-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic idx integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((list-set '(1 2 3) idx 4)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0
    (u
     .
     "(list\n (ite (= 0 idx) 4 1)\n (ite (= 0 idx) 2 (ite (= 0 (+ -1 idx)) 4 2))\n (ite (= 0 idx) 3 (ite (= 0 (+ -1 idx)) 3 (ite (= 0 (+ -2 idx)) 4 3))))\n\n"))))
 #""
 #"")
((define (list-set* lst idx val)
   (match
    lst
    ((cons x xs) (cons (if (= idx 0) val x) (list-set* xs (- idx 1) val)))
    (_ lst)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((list-set* '(1 2 3) idx 4)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0
    (u
     .
     "(list\n (ite (= 0 idx) 4 1)\n (ite (= 0 (+ -1 idx)) 4 2)\n (ite (= 0 (+ -2 idx)) 4 3))\n\n"))))
 #""
 #"")
