Skip to content

Commit

Permalink
Update doc log files.
Browse files Browse the repository at this point in the history
  • Loading branch information
@emina
emina committed Feb 26, 2021
1 parent 90739dd commit 55f0239
Show file tree
Hide file tree
Showing 7 changed files with 34 additions and 34 deletions.
2 changes: 1 addition & 1 deletion rosette/guide/scribble/datatypes/uninterpreted-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@
()
(q
exn
"~>: arity mismatch;\n the expected number of arguments does not match the given number\n expected: at least 2\n given: 1\n arguments...:\n real?"))
"~>: arity mismatch;\n the expected number of arguments does not match the given number\n expected: at least 2\n given: 1"))
#""
#"")
((define t0? (~> integer? real? boolean? (bitvector 4)))
Expand Down
18 changes: 9 additions & 9 deletions rosette/guide/scribble/error-tracing/error-tracer-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
((verify (assert (= (sum xs) (sum (filter-not zero? xs)))))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand All @@ -28,7 +28,7 @@
(assert (= (sum xs) (apply (if opt + -) xs))))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand Down Expand Up @@ -71,7 +71,7 @@
((format-opaque "~a" (run-test example-tests))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand All @@ -93,7 +93,7 @@
((verify (assert (ormap positive? xs)))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand Down Expand Up @@ -142,7 +142,7 @@
((format-opaque "~a" (run-test example-tests))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand All @@ -160,11 +160,11 @@
((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.\neval:20:0: FAILURE\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")
#"--------------------\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
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand All @@ -177,7 +177,7 @@
((verify (assert (ormap positive? xs)))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand Down Expand Up @@ -210,7 +210,7 @@
((verify (assert (= k (list-ref (sort xs <) n))))
((3)
1
((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt"
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
Expand Down
24 changes: 12 additions & 12 deletions rosette/guide/scribble/essentials/essentials-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@
0
()
()
(c values c (0 (u . "(= y$0 y$1)"))))
(c values c (0 (u . "(= y$1 y$2)"))))
#""
#"")
((define (yet-another-x) (define-symbolic x boolean?) x)
Expand Down Expand Up @@ -438,7 +438,7 @@
values
c
(0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
#"cpu time: 1 real time: 39 gc time: 0\n"
#"cpu time: 0 real time: 37 gc time: 0\n"
#"")
((time (verify (check-mid-slow bvmid l h)))
((3)
Expand All @@ -453,7 +453,7 @@
values
c
(0 (u . "(model\n [l (bv #x2faef9a1 32)]\n [h (bv #x5eefb8dd 32)])"))))
#"cpu time: 4 real time: 175 gc time: 0\n"
#"cpu time: 1 real time: 172 gc time: 0\n"
#"")
((time (verify (check-mid bvmid-no-overflow l h)))
((3)
Expand All @@ -465,7 +465,7 @@
()
()
(c values c (0 (u . "(unsat)"))))
#"cpu time: 1 real time: 156 gc time: 0\n"
#"cpu time: 1 real time: 157 gc time: 0\n"
#"")
((error 'call-with-deep-time-limit "out of time")
((3) 0 () 0 () () (q exn "call-with-deep-time-limit: out of time"))
Expand All @@ -486,7 +486,7 @@
values
c
(0 (u . "(model\n [l (bv #x00000001 32)]\n [h (bv #x7fffffff 32)])"))))
#"cpu time: 3 real time: 25 gc time: 0\n"
#"cpu time: 1 real time: 23 gc time: 0\n"
#"")
((time (verify (check-mid-slow bvmid-no-overflow l h)))
((3)
Expand All @@ -498,7 +498,7 @@
()
()
(c values c (0 (u . "(unsat)"))))
#"cpu time: 1 real time: 157 gc time: 0\n"
#"cpu time: 0 real time: 157 gc time: 0\n"
#"")
((current-bitwidth 32) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((time (verify (check-mid-slow bvmid l h)))
Expand Down Expand Up @@ -526,7 +526,7 @@
values
c
(0 (u . "(model\n [l (bv #x71979fa3 32)]\n [h (bv #x76b91b88 32)])"))))
#"cpu time: 1 real time: 149 gc time: 0\n"
#"cpu time: 1 real time: 152 gc time: 0\n"
#"")
((current-bitwidth 512) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((time (verify (check-mid-slow bvmid l h)))
Expand All @@ -542,7 +542,7 @@
values
c
(0 (u . "(model\n [l (bv #x70000006 32)]\n [h (bv #x73fffffa 32)])"))))
#"cpu time: 2 real time: 380 gc time: 0\n"
#"cpu time: 1 real time: 379 gc time: 0\n"
#"")
((time (verify (check-mid-slow bvmid-no-overflow l h)))
((3)
Expand All @@ -554,7 +554,7 @@
()
()
(c values c (0 (u . "(unsat)"))))
#"cpu time: 1 real time: 430 gc time: 0\n"
#"cpu time: 0 real time: 429 gc time: 0\n"
#"")
((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((require rosette/solver/smt/z3)
Expand All @@ -578,7 +578,7 @@
values
c
(0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
#"cpu time: 4 real time: 34 gc time: 0\n"
#"cpu time: 4 real time: 33 gc time: 0\n"
#"")
((time (verify (check-mid-slow bvmid l h)))
((3)
Expand Down Expand Up @@ -765,7 +765,7 @@
#"")
((define cex (time (verify (check-sqrt bvsqrt l))))
((3) 0 () 0 () () (c values c (void)))
#"cpu time: 6 real time: 1047 gc time: 0\n"
#"cpu time: 4 real time: 1016 gc time: 0\n"
#"")
((bvsqrt (evaluate l cex))
((3) 0 () 0 () () (q exn "[assert] Out of fuel."))
Expand All @@ -783,5 +783,5 @@
()
()
(c values c (0 (u . "(unsat)"))))
#"cpu time: 4 real time: 68595 gc time: 0\n"
#"cpu time: 4 real time: 68673 gc time: 0\n"
#"")
8 changes: 4 additions & 4 deletions rosette/guide/scribble/forms/rosette-forms-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@
0
()
()
(c values c (0 (u . "(list y$0 y$1)"))))
(c values c (0 (u . "(list y$4 y$5)"))))
#""
#"")
((always-different-n 3)
Expand All @@ -137,7 +137,7 @@
0
()
()
(c values c (0 (u . "(list y$2 y$3 y$4)"))))
(c values c (0 (u . "(list y$6 y$7 y$8)"))))
#""
#"")
((equal? (always-different-n 4) (always-different-n 4))
Expand All @@ -152,7 +152,7 @@
(c
values
c
(0 (u . "(&& (= y$5 y$9) (= y$6 y$10) (= y$7 y$11) (= y$8 y$12))"))))
(0 (u . "(&& (= y$9 y$13) (= y$10 y$14) (= y$11 y$15) (= y$12 y$16))"))))
#""
#"")
((assert #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -669,7 +669,7 @@
()
(q
exn
"solver-push: contract violation:\nexpected: solver?\ngiven: #f\nargument position: 1st"))
"solver-push: contract violation:\n expected: solver?\n given: #f\n argument position: 1st"))
#""
#"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down
2 changes: 1 addition & 1 deletion rosette/guide/scribble/libs/libs-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@
(0
(u
.
"'((union\n [xi?$0 #(struct:Add arg$0)]\n [(&& xi?$1 (! xi?$0)) #(struct:Mul arg$0)]\n [(&& (! xi?$0) (! xi?$1)) #(struct:Sqr)])\n (union\n [xi?$2 #(struct:Add arg$1)]\n [(&& xi?$3 (! xi?$2)) #(struct:Mul arg$1)]\n [(&& (! xi?$2) (! xi?$3)) #(struct:Sqr)])\n (union\n [xi?$4 #(struct:Add arg$2)]\n [(&& xi?$5 (! xi?$4)) #(struct:Mul arg$2)]\n [(&& (! xi?$4) (! xi?$5)) #(struct:Sqr)]))\n"))))
"'((union\n [xi?$1 #(struct:Add arg$0)]\n [(&& xi?$2 (! xi?$1)) #(struct:Mul arg$0)]\n [(&& (! xi?$1) (! xi?$2)) #(struct:Sqr)])\n (union\n [xi?$4 #(struct:Add arg$3)]\n [(&& xi?$5 (! xi?$4)) #(struct:Mul arg$3)]\n [(&& (! xi?$4) (! xi?$5)) #(struct:Sqr)])\n (union\n [xi?$7 #(struct:Add arg$6)]\n [(&& xi?$8 (! xi?$7)) #(struct:Mul arg$6)]\n [(&& (! xi?$7) (! xi?$8)) #(struct:Sqr)]))\n"))))
#""
#"")
((define sol
Expand Down
4 changes: 2 additions & 2 deletions rosette/guide/scribble/performance/performance-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@
0
()
()
(c values c (0 (u . "(union #:size 6 #:hash 2883417510948978588)"))))
(c values c (0 (u . "(union #:size 6 #:hash -437127353640646723)"))))
#""
#"")
((define (list-set* lst idx val)
Expand Down Expand Up @@ -86,7 +86,7 @@
0
()
()
(c values c (0 (u . "(union #:size 4 #:hash 3537189751407371886)"))))
(c values c (0 (u . "(union #:size 4 #:hash 350627999700259086)"))))
#""
#"")
((define-values (width height) (values 5 5))
Expand Down
10 changes: 5 additions & 5 deletions rosette/guide/scribble/reflection/state-log.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
0
()
()
(c values c (0 (u . "(list a d b c)"))))
(c values c (0 (u . "(list b c d a)"))))
#""
#"")
((assume a) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -87,7 +87,7 @@
(0
(u
.
"(list\n (|| d (! (&& a (! b))))\n (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))\n (! d)\n (|| (! b) (|| c (! (&& a b))))\n (! a)\n ...)\n"))))
"(list\n b\n c\n d\n a\n (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))\n ...)\n"))))
#""
#"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -363,7 +363,7 @@
((length (terms)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((time (unused-terms! 50000))
((3) 0 () 0 () () (c values c (void)))
#"cpu time: 240 real time: 240 gc time: 20\n"
#"cpu time: 402 real time: 410 gc time: 49\n"
#"")
((length (terms)) ((3) 0 () 0 () () (q values 50000)) #"" #"")
((collect-garbage) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand All @@ -374,7 +374,7 @@
((length (terms)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((time (unused-terms! 50000))
((3) 0 () 0 () () (c values c (void)))
#"cpu time: 321 real time: 321 gc time: 27\n"
#"cpu time: 420 real time: 427 gc time: 42\n"
#"")
(50000 ((3) 0 () 0 () () (q values 50000)) #"" #"")
((collect-garbage) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -402,7 +402,7 @@
()
()
(c values c (0 (u . "(model\n [a 1]\n [b 0])"))))
#"(list (= 0 (+ a b)) b (! (= 0 (+ a b))) a (+ a b))\n"
#"(list (! (= 0 (+ a b))) a b (= 0 (+ a b)) (+ a b))\n"
#"")
((terms)
((3)
Expand Down

0 comments on commit 55f0239

Please sign in to comment.