;; 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)))
 #""
 #"")
((define-symbolic xs integer? #:length 4)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (sum xs) (foldl + xs)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((verify (assert (= (sum xs) (sum (filter-not zero? xs)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model)\n"))))
 #""
 #"")
((define-symbolic opt boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((synthesize
  #:forall
  xs
  #:guarantee
  (assert (= (sum xs) (apply (if opt + -) xs))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((require rackunit) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define (post xs) (assert (= (sum xs) (sum (filter-not zero? xs)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (query xs) (verify (post xs)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define example-tests
   (test-suite
    "An example suite for a sum query."
    #:before
    clear-vc!
    #:after
    clear-vc!
    (test-case
     "Test sum with concrete values."
     (check = (sum '()) 0)
     (check = (sum '(-1)) -1)
     (check = (sum '(-2 2)) 0)
     (check = (sum '(-1 0 3)) 2))
    (test-case
     "Test query post for exceptions."
     (before (clear-vc!) (check-not-exn (thunk (post xs)))))
    (test-case
     "Test query outcome."
     (before (clear-vc!) (check-pred unsat? (query xs))))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((format-opaque "~a" (run-test example-tests))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(#<test-error> #<test-failure> #<test-failure>)\n"))))
 #""
 #"")
((define (sum xs)
   (cond
    ((null? xs) 0)
    ((null? (cdr xs)) (car xs))
    ((andmap (curry = (car xs)) (cdr xs)) (* (length xs) (cdr xs)))
    (else (apply + xs))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((assume (positive? (sum xs))) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((verify (assert (ormap positive? xs)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((define (pre xs) (assume (positive? (sum xs))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (post xs) (assert (ormap positive? xs)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define (query xs) (pre xs) (verify (post xs)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define example-tests
   (test-suite
    "An example suite for a sum query."
    #:before
    clear-vc!
    #:after
    clear-vc!
    (test-case
     "Test sum with concrete values."
     (check = (sum '()) 0)
     (check = (sum '(-1)) -1)
     (check = (sum '(-2 2)) 0)
     (check = (sum '(-1 0 3)) 2))
    (test-case
     "Test query post for exceptions."
     (before (clear-vc!) (check-not-exn (thunk (pre xs)))))
    (test-case
     "Test query post for exceptions."
     (before (clear-vc!) (check-not-exn (thunk (post xs)))))
    (test-case
     "Test query outcome."
     (before (clear-vc!) (check-pred unsat? (query xs))))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((format-opaque "~a" (run-test example-tests))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0
    (u
     .
     "(#<test-success> #<test-success> #<test-success> #<test-success>)\n"))))
 #""
 #"")
((test-case "Test sum for any failures." (check-pred unsat? (verify (sum xs))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"--------------------\nTest sum for any failures.\nFAILURE\nname:       check-pred\nlocation:   eval:20:0\nparams:\n  '(#<procedure:unsat?> (model\n   [xs$0 0]\n   [xs$1 0]\n   [xs$2 0]\n   [xs$3 0]))\n--------------------\n")
((verify (begin (assume (positive? (sum xs))) (assert (ormap positive? xs))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0 (u . "(model\n [xs$0 1]\n [xs$1 1]\n [xs$2 1]\n [xs$3 1])\n"))))
 #""
 #"")
((assume (positive? (sum xs))) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((verify (assert (ormap positive? xs)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((define (select xs n)
   (cond
    ((empty? xs) (assert #f "unexpected empty list"))
    (else
     (define pivot (first xs))
     (define non-pivot (rest xs))
     (define <pivot (filter (λ (x) (< x pivot)) non-pivot))
     (define >=pivot (filter (λ (x) (>= x pivot)) non-pivot))
     (define len< (length <pivot))
     (cond
      ((= n len<) pivot)
      ((< n len<) (select <pivot))
      (else (select >=pivot (- n len< 1)))))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define-symbolic n k integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assume (and (<= 0 n (sub1 (length xs))) (= k (select xs n))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((verify (assert (= k (list-ref (sort xs <) n))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
