-
Notifications
You must be signed in to change notification settings - Fork 55
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Re-add herbie tests and python benchmarks
- Loading branch information
1 parent
555faf4
commit 3bfde2e
Showing
4 changed files
with
2,716 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,137 @@ | ||
(datatype Math | ||
(Num BigRat) | ||
(Var String) | ||
(Add Math Math) | ||
(Div Math Math) | ||
(Mul Math Math)) | ||
|
||
(let zero (Num (bigrat (bigint 0) (bigint 1)))) | ||
(let one (Num (bigrat (bigint 1) (bigint 1)))) | ||
(let two (Num (bigrat (bigint 2) (bigint 1)))) | ||
|
||
(rewrite (Add a b) (Add b a)) | ||
(rewrite (Add a zero) a) | ||
(rewrite (Add (Num r1) (Num r2)) | ||
(Num (+ r1 r2))) | ||
|
||
(let one-two (Add one two)) | ||
|
||
(push) | ||
(run 1) | ||
;; yay, constant folding works | ||
(check (= one-two (Num (bigrat (bigint 3) (bigint 1))))) | ||
;; also, commutativity works | ||
(check (= (Add two one) one-two)) | ||
(pop) | ||
|
||
(push) | ||
;; rule is like rewrite, but more general | ||
;; the following rule doesn't union (Num r) with the result: | ||
(rule ((Num r)) | ||
((union one (Div (Num r) (Num r))))) | ||
;; uh oh, division by zero! | ||
(run 1) | ||
|
||
(pop) | ||
|
||
;; we need to detect when things are non-zero | ||
(function lower-bound (Math) BigRat :merge (max old new)) | ||
(function upper-bound (Math) BigRat :merge (min old new)) | ||
|
||
(rule ((Num r)) | ||
((set (lower-bound (Num r)) r) | ||
(set (upper-bound (Num r)) r))) | ||
(rule ((= e (Add a b)) (= x (lower-bound a)) (= y (lower-bound b))) | ||
((set (lower-bound e) (+ x y)))) | ||
(rule ((= e (Add a b)) (= x (upper-bound a)) (= y (upper-bound b))) | ||
((set (upper-bound e) (+ x y)))) | ||
(rule ((= e (Mul a b))) | ||
((set (lower-bound e) | ||
(min (* (lower-bound a) (lower-bound b)) | ||
(min (* (lower-bound a) (upper-bound b)) | ||
(min (* (upper-bound a) (lower-bound b)) | ||
(* (upper-bound a) (upper-bound b)))))) | ||
(set (upper-bound e) | ||
(max (* (lower-bound a) (lower-bound b)) | ||
(max (* (lower-bound a) (upper-bound b)) | ||
(max (* (upper-bound a) (lower-bound b)) | ||
(* (upper-bound a) (upper-bound b)))))))) | ||
|
||
(rule ((= e (Add a b)) | ||
(> (lower-bound e) (bigrat (bigint 0) (bigint 1)))) | ||
((union one (Div (Add a b) (Add a b))))) | ||
|
||
(let x (Var "x")) | ||
(let x1 (Add x one)) | ||
|
||
(push) | ||
(set (lower-bound x) (bigrat (bigint 0) (bigint 1))) | ||
(set (upper-bound x) (bigrat (bigint 1) (bigint 1))) | ||
|
||
(run 3) | ||
|
||
(query-extract (lower-bound x1)) | ||
(query-extract (upper-bound x1)) | ||
(check (= one (Div x1 x1))) | ||
|
||
(pop) | ||
|
||
|
||
;; Set the variable x to a particular input value 200/201 | ||
(set (lower-bound x) (bigrat (bigint 200) (bigint 201))) | ||
(set (upper-bound x) (bigrat (bigint 200) (bigint 201))) | ||
|
||
(run 3) | ||
|
||
(query-extract (lower-bound x1)) | ||
(query-extract (upper-bound x1)) | ||
|
||
(function true-value (Math) f64) | ||
|
||
(rule ((= (to-f64 (lower-bound e)) | ||
(to-f64 (upper-bound e)))) | ||
((set (true-value e) | ||
(to-f64 (lower-bound e))))) | ||
|
||
(run 1) | ||
(query-extract (true-value x1)) | ||
|
||
(function best-error (Math) f64 :merge new :default (to-f64 (bigrat (bigint 10000) (bigint 1)))) | ||
|
||
(rule ((Num n)) | ||
((set (best-error (Num n)) (to-f64 n)))) | ||
(rule ((Add a b)) ((best-error (Add a b)))) | ||
|
||
;; finally, the mega rule for finding more accurate programs | ||
(rule ((= expr (Add a b)) | ||
(= (best-error a) va) | ||
(= (best-error b) vb) | ||
(= true-v (true-value (Add a b))) | ||
(= computed (+ va vb)) | ||
(< (abs (- computed true-v)) | ||
(best-error (Add a b)))) | ||
((set (best-error (Add a b)) computed))) | ||
|
||
|
||
|
||
(push) | ||
|
||
(let target | ||
(Add | ||
(Add (Num (bigrat (bigint 1) (bigint 100))) (Num (bigrat (bigint 1) (bigint 100)))) | ||
(Num (bigrat (bigint -2) (bigint 100))))) | ||
|
||
(run 1) | ||
|
||
;; set a default | ||
(best-error target) | ||
;; error is bad, constant folding hasn't fired enough | ||
(query-extract (best-error target)) | ||
|
||
(run 1) | ||
|
||
;; error is good, constant folding has fired enough | ||
(query-extract (best-error target)) | ||
|
||
|
||
(pop) |
Oops, something went wrong.