From c6ac1deef133c2bacf019db2a993ba52edc29cad Mon Sep 17 00:00:00 2001 From: AYadrov Date: Mon, 6 Jan 2025 14:02:45 -0700 Subject: [PATCH 01/19] hint implementation --- src/core/bsearch.rkt | 2 +- src/core/rival.rkt | 11 +++++++---- src/core/sampling.rkt | 30 +++++++++++++++++------------- src/core/searchreals.rkt | 17 +++++++++++------ 4 files changed, 36 insertions(+), 24 deletions(-) diff --git a/src/core/bsearch.rkt b/src/core/bsearch.rkt index 25f48c5ba..1da950092 100644 --- a/src/core/bsearch.rkt +++ b/src/core/bsearch.rkt @@ -99,7 +99,7 @@ (for/list ([(pt ex) (in-pcontext pcontext)]) pt)) (define (new-sampler) - (cons val (random-ref pts))) + (cons (cons val (random-ref pts)) #f)) (apply mk-pcontext (cdr (batch-prepare-points evaluator new-sampler)))) (define/reset *prepend-arguement-cache* (make-hash)) diff --git a/src/core/rival.rkt b/src/core/rival.rkt index cd553376c..735ae340d 100644 --- a/src/core/rival.rkt +++ b/src/core/rival.rkt @@ -22,9 +22,11 @@ [ctxs (es) (and/c unified-contexts? (lambda (ctxs) (= (length es) (length ctxs))))]) (#:pre [pre any/c]) [c real-compiler?])] - [real-apply (-> real-compiler? list? (values symbol? any/c))] + [real-apply + (->* (real-compiler? list?) ((or/c (vectorof any/c) boolean?)) (values symbol? any/c))] [real-compiler-clear! (-> real-compiler-clear! void?)] - [real-compiler-analyze (-> real-compiler? (vectorof ival?) ival?)])) + [real-compiler-analyze + (-> real-compiler? (vectorof ival?) (values ival? (vectorof any/c)))])) (define (unified-contexts? ctxs) (and ((non-empty-listof context?) ctxs) @@ -66,7 +68,7 @@ (real-compiler pre vars var-reprs specs reprs machine)) ;; Runs a Rival machine on an input point. -(define (real-apply compiler pt) +(define (real-apply compiler pt [hint #f]) (match-define (real-compiler _ vars var-reprs _ _ machine) compiler) (define start (current-inexact-milliseconds)) (define pt* @@ -79,7 +81,8 @@ [exn:rival:unsamplable? (lambda (e) (values 'exit #f))]) (parameterize ([*rival-max-precision* (*max-mpfr-prec*)] [*rival-max-iterations* 5]) - (values 'valid (rest (vector->list (rival-apply machine pt*))))))) ; rest = drop precondition + (values 'valid + (rest (vector->list (rival-apply machine pt* hint))))))) ; rest = drop precondition (when (> (rival-profile machine 'bumps) 0) (warn 'ground-truth "Could not converge on a ground truth" diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index bd23f7db9..322996fa2 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -78,10 +78,11 @@ (when (> search-result 0) (check-true (<= (vector-ref arr (- search-result 1)) search-for))))) -(define (make-hyperrect-sampler hyperrects* reprs) - (when (null? hyperrects*) +(define (make-hyperrect-sampler hints-hyperrects* reprs) + (when (null? hints-hyperrects*) (raise-herbie-sampling-error "No valid values." #:url "faq.html#no-valid-values")) - (define hyperrects (list->vector hyperrects*)) + (define hints (list->vector (map car hints-hyperrects*))) + (define hyperrects (list->vector (map rest hints-hyperrects*))) (define lo-ends (for/vector #:length (vector-length hyperrects) ([hyperrect (in-vector hyperrects)]) @@ -103,10 +104,12 @@ (define idx (binary-search weights rand-ordinal)) (define los (vector-ref lo-ends idx)) (define his (vector-ref hi-ends idx)) - (for/list ([lo (in-list los)] - [hi (in-list his)] - [repr (in-list reprs)]) - ((representation-ordinal->repr repr) (random-integer lo hi))))) + (define hint (vector-ref hints idx)) + (cons (for/list ([lo (in-list los)] + [hi (in-list his)] + [repr (in-list reprs)]) + ((representation-ordinal->repr repr) (random-integer lo hi))) + hint))) #;(module+ test (define two-point-hyperrects (list (list (ival (bf 0) (bf 0)) (ival (bf 1) (bf 1))))) @@ -123,12 +126,14 @@ (equal? (representation-type repr) 'real))) (timeline-push! 'method "search") (define hyperrects-analysis (precondition->hyperrects pre vars var-reprs)) - (match-define (cons hyperrects sampling-table) + ; hyperrects is a (listof '(hint hyperrect)) + (match-define (cons hints-hyperrects sampling-table) (find-intervals compiler hyperrects-analysis #:fuel (*max-find-range-depth*))) - (cons (make-hyperrect-sampler hyperrects var-reprs) sampling-table)] + (cons (make-hyperrect-sampler hints-hyperrects var-reprs) sampling-table)] [else (timeline-push! 'method "random") - (cons (λ () (map random-generate var-reprs)) (hash 'unknown 1.0))])) + (println "opa") + (cons (λ () (cons (map random-generate var-reprs) #f)) (hash 'unknown 1.0))])) ;; Returns an evaluator for a list of expressions. (define (eval-progs-real specs ctxs) @@ -156,9 +161,8 @@ [skipped 0] [points '()] [exactss '()]) - (define pt (sampler)) - - (define-values (status exs) (real-apply compiler pt)) + (match-define (cons pt hint) (sampler)) + (define-values (status exs) (real-apply compiler pt hint)) (case status [(exit) (warn 'ground-truth diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index a8cad3c8a..1e34c278b 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -54,7 +54,12 @@ [false* false] [other* '()]) ([rect (in-list other)]) - (match-define (ival err err?) (real-compiler-analyze compiler (list->vector rect))) + ; if a rect has a hint stored already then drop that hint + (when (not (equal? (length vars) (length rect))) + (set! rect (rest rect))) + + (match-define-values ((ival err err?) hint) + (real-compiler-analyze compiler (list->vector rect))) (when (eq? err 'unsamplable) (warn 'ground-truth #:url "faq.html#ground-truth" @@ -69,7 +74,7 @@ (format "~a = ~a" var val)))) (cond [err (values true* (cons rect false*) other*)] - [(not err?) (values (cons rect true*) false* other*)] + [(not err?) (values (cons (cons hint rect) true*) false* other*)] [else (define range (list-ref rect split-var)) (define repr (list-ref reprs split-var)) @@ -77,15 +82,15 @@ [(cons midleft midright) (define rect-lo (list-set rect split-var (ival (ival-lo range) midleft))) (define rect-hi (list-set rect split-var (ival midright (ival-hi range)))) - (values true* false* (list* rect-lo rect-hi other*))] - [#f (values true* false* (cons rect other*))])]))) + (values true* false* (list* (cons hint rect-lo) (cons hint rect-hi) other*))] + [#f (values true* false* (cons (cons hint rect) other*))])]))) (search-space true* false* other*)) (define (make-sampling-table reprs true false other) (define denom (total-weight reprs)) - (define true-weight (apply + (map (curryr hyperrect-weight reprs) true))) + (define true-weight (apply + (map (curryr hyperrect-weight reprs) (map rest true)))) (define false-weight (apply + (map (curryr hyperrect-weight reprs) false))) - (define other-weight (apply + (map (curryr hyperrect-weight reprs) other))) + (define other-weight (apply + (map (curryr hyperrect-weight reprs) (map rest other)))) (define out (make-hash)) (hash-set! out 'valid (exact->inexact (/ true-weight denom))) (hash-set! out 'unknown (exact->inexact (/ other-weight denom))) From a2ac92b540203ae4daf43c52ba8e2eeacf13e978 Mon Sep 17 00:00:00 2001 From: AYadrov Date: Tue, 7 Jan 2025 11:31:50 -0700 Subject: [PATCH 02/19] some updates --- src/core/bsearch.rkt | 2 ++ src/core/sampling.rkt | 20 ++++++++++++++++++-- 2 files changed, 20 insertions(+), 2 deletions(-) diff --git a/src/core/bsearch.rkt b/src/core/bsearch.rkt index 1da950092..0c5f6471a 100644 --- a/src/core/bsearch.rkt +++ b/src/core/bsearch.rkt @@ -98,6 +98,8 @@ (define pts (for/list ([(pt ex) (in-pcontext pcontext)]) pt)) + ; new-sampler returns: (cons (cons val pts) hint) + ; Since the sampler does not call rival-analyze, the hint is set to #f (define (new-sampler) (cons (cons val (random-ref pts)) #f)) (apply mk-pcontext (cdr (batch-prepare-points evaluator new-sampler)))) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 322996fa2..8b7085a46 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -22,6 +22,19 @@ (define (precondition->hyperrects pre vars var-reprs) ;; FPBench needs unparameterized operators (define range-table (condition->range-table pre)) + (define initial-ranges + (for/list ([var-name vars] + [var-repr var-reprs]) + (map (lambda (interval) (fpbench-ival->ival var-repr interval)) + (range-table-ref range-table var-name)))) + (println initial-ranges) + ; split initial ranges in midpoints + (println (for*/list ([range (in-list initial-ranges)] + [r (in-list range)]) + (define-values (x y) (ival-split r (ival-midpoint r))) + (cons x y))) + (sleep 20) + (apply cartesian-product (for/list ([var-name vars] [var-repr var-reprs]) @@ -78,6 +91,7 @@ (when (> search-result 0) (check-true (<= (vector-ref arr (- search-result 1)) search-for))))) +;; hints-hyperrects* is a (listof '(hint hyperrect)) (define (make-hyperrect-sampler hints-hyperrects* reprs) (when (null? hints-hyperrects*) (raise-herbie-sampling-error "No valid values." #:url "faq.html#no-valid-values")) @@ -99,6 +113,8 @@ ((representation-bf->repr repr) (ival-hi interval))))))) (define weights (partial-sums (vector-map (curryr hyperrect-weight reprs) hyperrects))) (define weight-max (vector-ref weights (- (vector-length weights) 1))) + + ;; returns (cons (listof pts) hint) (λ () (define rand-ordinal (random-integer 0 weight-max)) (define idx (binary-search weights rand-ordinal)) @@ -126,13 +142,13 @@ (equal? (representation-type repr) 'real))) (timeline-push! 'method "search") (define hyperrects-analysis (precondition->hyperrects pre vars var-reprs)) - ; hyperrects is a (listof '(hint hyperrect)) + ; hints-hyperrects is a (listof '(hint hyperrect)) (match-define (cons hints-hyperrects sampling-table) (find-intervals compiler hyperrects-analysis #:fuel (*max-find-range-depth*))) (cons (make-hyperrect-sampler hints-hyperrects var-reprs) sampling-table)] [else (timeline-push! 'method "random") - (println "opa") + ; sampler return false hint since rival-analyze has not been called in random method (cons (λ () (cons (map random-generate var-reprs) #f)) (hash 'unknown 1.0))])) ;; Returns an evaluator for a list of expressions. From ac315c5a0c115455ee86b545b21039a75992c69b Mon Sep 17 00:00:00 2001 From: AYadrov Date: Tue, 7 Jan 2025 17:49:38 -0700 Subject: [PATCH 03/19] some additional search --- src/core/sampling.rkt | 40 ++++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 deletions(-) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 8b7085a46..cd4b04727 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -1,5 +1,6 @@ #lang racket (require math/bigfloat + math/flonum rival math/base (only-in fpbench interval range-table-ref condition->range-table [expr? fpcore-expr?])) @@ -22,25 +23,35 @@ (define (precondition->hyperrects pre vars var-reprs) ;; FPBench needs unparameterized operators (define range-table (condition->range-table pre)) - (define initial-ranges - (for/list ([var-name vars] - [var-repr var-reprs]) - (map (lambda (interval) (fpbench-ival->ival var-repr interval)) - (range-table-ref range-table var-name)))) - (println initial-ranges) - ; split initial ranges in midpoints - (println (for*/list ([range (in-list initial-ranges)] - [r (in-list range)]) - (define-values (x y) (ival-split r (ival-midpoint r))) - (cons x y))) - (sleep 20) - (apply cartesian-product (for/list ([var-name vars] [var-repr var-reprs]) (map (lambda (interval) (fpbench-ival->ival var-repr interval)) (range-table-ref range-table var-name))))) +(define (grind-hyperrects hyperrects var-reprs) + (define (ival-custom-midpoint iv repr) + (define (repr-round repr dir point) + ((representation-repr->bf repr) (parameterize ([bf-rounding-mode dir]) + ((representation-bf->repr repr) point)))) + (define <-ordinal (compose (representation-repr->bf repr) (representation-ordinal->repr repr))) + (define ->ordinal (compose (representation-repr->ordinal repr) (representation-bf->repr repr))) + (define lower (<-ordinal (floor (/ (+ (->ordinal (ival-hi iv)) (->ordinal (ival-lo iv))) 2)))) + (define higher (repr-round repr 'up (bfnext lower))) ; repr-next + (values lower higher)) + + (define hyperrects* '()) + (for* ([hyperrect (in-list hyperrects)]) + (set! hyperrects* + (append hyperrects* + (apply cartesian-product + (for/list ([range (in-list hyperrect)] + [repr (in-list var-reprs)]) + (define-values (lower higher) (ival-custom-midpoint range repr)) + (define-values (x y) (ival-split range lower)) + (list x y)))))) + hyperrects*) + (define (fpbench-ival->ival repr fpbench-interval) (match-define (interval lo hi lo? hi?) fpbench-interval) (match (representation-type repr) @@ -142,9 +153,10 @@ (equal? (representation-type repr) 'real))) (timeline-push! 'method "search") (define hyperrects-analysis (precondition->hyperrects pre vars var-reprs)) + (define hyperrects-analysis* (grind-hyperrects hyperrects-analysis var-reprs)) ; hints-hyperrects is a (listof '(hint hyperrect)) (match-define (cons hints-hyperrects sampling-table) - (find-intervals compiler hyperrects-analysis #:fuel (*max-find-range-depth*))) + (find-intervals compiler hyperrects-analysis* #:fuel (*max-find-range-depth*))) (cons (make-hyperrect-sampler hints-hyperrects var-reprs) sampling-table)] [else (timeline-push! 'method "random") From b49c46f522f3f6306c3850c222494d862c5eb58d Mon Sep 17 00:00:00 2001 From: AYadrov Date: Wed, 8 Jan 2025 13:33:05 -0700 Subject: [PATCH 04/19] a proper way of splitting hyperrect (same as during analyze stage) --- src/core/sampling.rkt | 30 +++++++++--------------------- src/core/searchreals.rkt | 18 +----------------- src/utils/float.rkt | 17 +++++++++++++++++ 3 files changed, 27 insertions(+), 38 deletions(-) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index cd4b04727..b794d4092 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -30,27 +30,15 @@ (range-table-ref range-table var-name))))) (define (grind-hyperrects hyperrects var-reprs) - (define (ival-custom-midpoint iv repr) - (define (repr-round repr dir point) - ((representation-repr->bf repr) (parameterize ([bf-rounding-mode dir]) - ((representation-bf->repr repr) point)))) - (define <-ordinal (compose (representation-repr->bf repr) (representation-ordinal->repr repr))) - (define ->ordinal (compose (representation-repr->ordinal repr) (representation-bf->repr repr))) - (define lower (<-ordinal (floor (/ (+ (->ordinal (ival-hi iv)) (->ordinal (ival-lo iv))) 2)))) - (define higher (repr-round repr 'up (bfnext lower))) ; repr-next - (values lower higher)) - - (define hyperrects* '()) - (for* ([hyperrect (in-list hyperrects)]) - (set! hyperrects* - (append hyperrects* - (apply cartesian-product - (for/list ([range (in-list hyperrect)] - [repr (in-list var-reprs)]) - (define-values (lower higher) (ival-custom-midpoint range repr)) - (define-values (x y) (ival-split range lower)) - (list x y)))))) - hyperrects*) + (reap [sow] + (for ([hyperrect (in-list hyperrects)]) + (sow (apply cartesian-product + (for/list ([range (in-list hyperrect)] + [repr (in-list var-reprs)]) + (match (two-midpoints repr (ival-lo range) (ival-hi range)) + [(cons midleft midright) + (list (ival (ival-lo range) midleft) (ival midright (ival-hi range)))] + [#f range]))))))) (define (fpbench-ival->ival repr fpbench-interval) (match-define (interval lo hi lo? hi?) fpbench-interval) diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 1e34c278b..831f0ff2b 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -18,10 +18,6 @@ (define (make-search-space . ranges) (search-space '() '() ranges)) -(define (repr-round repr dir point) - ((representation-repr->bf repr) (parameterize ([bf-rounding-mode dir]) - ((representation-bf->repr repr) point)))) - (define (total-weight reprs) (expt 2 (apply + (map representation-total-bits reprs)))) @@ -33,18 +29,6 @@ (compose (representation-repr->ordinal repr) (representation-bf->repr repr))) (+ 1 (- (->ordinal (ival-hi interval)) (->ordinal (ival-lo interval))))))) -(define (midpoint repr lo hi) - ; Midpoint is taken in repr-space, but values are stored in bf - (define <-ordinal (compose (representation-repr->bf repr) (representation-ordinal->repr repr))) - (define ->ordinal (compose (representation-repr->ordinal repr) (representation-bf->repr repr))) - - (define lower (<-ordinal (floor (/ (+ (->ordinal hi) (->ordinal lo)) 2)))) - (define higher (repr-round repr 'up (bfnext lower))) ; repr-next - - (and (bf>= lower lo) - (bf<= higher hi) ; False if lo and hi were already close together - (cons lower higher))) - (define (search-step compiler space split-var) (define vars (real-compiler-vars compiler)) (define reprs (real-compiler-var-reprs compiler)) @@ -78,7 +62,7 @@ [else (define range (list-ref rect split-var)) (define repr (list-ref reprs split-var)) - (match (midpoint repr (ival-lo range) (ival-hi range)) + (match (two-midpoints repr (ival-lo range) (ival-hi range)) [(cons midleft midright) (define rect-lo (list-set rect split-var (ival (ival-lo range) midleft))) (define rect-hi (list-set rect split-var (ival midright (ival-hi range)))) diff --git a/src/utils/float.rkt b/src/utils/float.rkt index 6f94be5ff..bd7e6e0b3 100644 --- a/src/utils/float.rkt +++ b/src/utils/float.rkt @@ -9,6 +9,7 @@ (provide ulp-difference ulps->bits midpoint + two-midpoints random-generate ordinal repr) p2)) 2)))) +(define (repr-round repr dir point) + ((representation-repr->bf repr) (parameterize ([bf-rounding-mode dir]) + ((representation-bf->repr repr) point)))) + +(define (two-midpoints repr lo hi) + ; Midpoint is taken in repr-space, but values are stored in bf + (define <-ordinal (compose (representation-repr->bf repr) (representation-ordinal->repr repr))) + (define ->ordinal (compose (representation-repr->ordinal repr) (representation-bf->repr repr))) + + (define lower (<-ordinal (floor (/ (+ (->ordinal hi) (->ordinal lo)) 2)))) + (define higher (repr-round repr 'up (bfnext lower))) ; repr-next + + (and (bf>= lower lo) + (bf<= higher hi) ; False if lo and hi were already close together + (cons lower higher))) + (define (ulps->bits x) (real->double-flonum (log x 2))) From 0e43e173446cdd7655ffd795284e242940f81cdb Mon Sep 17 00:00:00 2001 From: AYadrov Date: Wed, 8 Jan 2025 17:44:55 -0700 Subject: [PATCH 05/19] converged flag for hint has been added --- src/core/rival.rkt | 2 +- src/core/sampling.rkt | 23 +++++++++++------------ src/core/searchreals.rkt | 4 ++-- 3 files changed, 14 insertions(+), 15 deletions(-) diff --git a/src/core/rival.rkt b/src/core/rival.rkt index 735ae340d..d291d61c1 100644 --- a/src/core/rival.rkt +++ b/src/core/rival.rkt @@ -26,7 +26,7 @@ (->* (real-compiler? list?) ((or/c (vectorof any/c) boolean?)) (values symbol? any/c))] [real-compiler-clear! (-> real-compiler-clear! void?)] [real-compiler-analyze - (-> real-compiler? (vectorof ival?) (values ival? (vectorof any/c)))])) + (-> real-compiler? (vectorof ival?) (values ival? (vectorof any/c) boolean?))])) (define (unified-contexts? ctxs) (and ((non-empty-listof context?) ctxs) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index b794d4092..2889b491e 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -29,16 +29,16 @@ (map (lambda (interval) (fpbench-ival->ival var-repr interval)) (range-table-ref range-table var-name))))) -(define (grind-hyperrects hyperrects var-reprs) - (reap [sow] - (for ([hyperrect (in-list hyperrects)]) - (sow (apply cartesian-product - (for/list ([range (in-list hyperrect)] - [repr (in-list var-reprs)]) - (match (two-midpoints repr (ival-lo range) (ival-hi range)) - [(cons midleft midright) - (list (ival (ival-lo range) midleft) (ival midright (ival-hi range)))] - [#f range]))))))) +(define (subsplit-hyperrects hyperrects var-reprs) + (for/fold ([storage '()]) ([hyperrect (in-list hyperrects)]) + (append storage + (apply cartesian-product + (for/list ([range (in-list hyperrect)] + [repr (in-list var-reprs)]) + (match (two-midpoints repr (ival-lo range) (ival-hi range)) + [(cons midleft midright) + (list (ival (ival-lo range) midleft) (ival midright (ival-hi range)))] + [#f (list range)])))))) (define (fpbench-ival->ival repr fpbench-interval) (match-define (interval lo hi lo? hi?) fpbench-interval) @@ -141,10 +141,9 @@ (equal? (representation-type repr) 'real))) (timeline-push! 'method "search") (define hyperrects-analysis (precondition->hyperrects pre vars var-reprs)) - (define hyperrects-analysis* (grind-hyperrects hyperrects-analysis var-reprs)) ; hints-hyperrects is a (listof '(hint hyperrect)) (match-define (cons hints-hyperrects sampling-table) - (find-intervals compiler hyperrects-analysis* #:fuel (*max-find-range-depth*))) + (find-intervals compiler hyperrects-analysis #:fuel (*max-find-range-depth*))) (cons (make-hyperrect-sampler hints-hyperrects var-reprs) sampling-table)] [else (timeline-push! 'method "random") diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 831f0ff2b..c54f1d670 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -42,7 +42,7 @@ (when (not (equal? (length vars) (length rect))) (set! rect (rest rect))) - (match-define-values ((ival err err?) hint) + (match-define-values ((ival err err?) hint converged?) (real-compiler-analyze compiler (list->vector rect))) (when (eq? err 'unsamplable) (warn 'ground-truth @@ -58,7 +58,7 @@ (format "~a = ~a" var val)))) (cond [err (values true* (cons rect false*) other*)] - [(not err?) (values (cons (cons hint rect) true*) false* other*)] + [(and (not err?) converged?) (values (cons (cons hint rect) true*) false* other*)] [else (define range (list-ref rect split-var)) (define repr (list-ref reprs split-var)) From 60d1e16614891dbba9cf0aaa456f46fb98d1ea7f Mon Sep 17 00:00:00 2001 From: AYadrov Date: Thu, 9 Jan 2025 15:56:07 -0700 Subject: [PATCH 06/19] some pipelining for rival --- src/core/rival.rkt | 9 ++++++--- src/core/searchreals.rkt | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/core/rival.rkt b/src/core/rival.rkt index d291d61c1..b18a837d3 100644 --- a/src/core/rival.rkt +++ b/src/core/rival.rkt @@ -26,7 +26,7 @@ (->* (real-compiler? list?) ((or/c (vectorof any/c) boolean?)) (values symbol? any/c))] [real-compiler-clear! (-> real-compiler-clear! void?)] [real-compiler-analyze - (-> real-compiler? (vectorof ival?) (values ival? (vectorof any/c) boolean?))])) + (-> real-compiler? (vectorof ival?) (listof (or/c ival? (vectorof any/c) boolean?)))])) (define (unified-contexts? ctxs) (and ((non-empty-listof context?) ctxs) @@ -81,8 +81,11 @@ [exn:rival:unsamplable? (lambda (e) (values 'exit #f))]) (parameterize ([*rival-max-precision* (*max-mpfr-prec*)] [*rival-max-iterations* 5]) - (values 'valid - (rest (vector->list (rival-apply machine pt* hint))))))) ; rest = drop precondition + (define value + (rest (vector->list (if hint ; rest = drop precondition + (rival-apply machine pt* hint) + (rival-apply machine pt*))))) + (values 'valid value)))) (when (> (rival-profile machine 'bumps) 0) (warn 'ground-truth "Could not converge on a ground truth" diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index c54f1d670..274a9859d 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -42,7 +42,7 @@ (when (not (equal? (length vars) (length rect))) (set! rect (rest rect))) - (match-define-values ((ival err err?) hint converged?) + (match-define (list (ival err err?) hint converged?) (real-compiler-analyze compiler (list->vector rect))) (when (eq? err 'unsamplable) (warn 'ground-truth From 5db7003cd8326814488ea7256fd471ffc3d23b0f Mon Sep 17 00:00:00 2001 From: AYadrov Date: Mon, 20 Jan 2025 14:51:22 -0700 Subject: [PATCH 07/19] updating rival at installation --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 8d22149e1..e55090f3e 100644 --- a/Makefile +++ b/Makefile @@ -13,6 +13,8 @@ clean: raco pkg remove --force --no-docs egg-herbie-windows && echo "Uninstalled old egg-herbie" || : raco pkg remove --force --no-docs egg-herbie-osx && echo "Uninstalled old egg-herbie" || : raco pkg remove --force --no-docs egg-herbie-macosm1 && echo "Uninstalled old egg-herbie" || : + raco pkg remove --force --no-docs rival && echo "Uninstalled old rival" || : + raco pkg install rival && echo "Installing new rival" || : update: raco pkg install --skip-installed --no-docs --auto --name herbie src/ From b4cbf289c23001b553ec3ed6ecd7611ed7f8d40d Mon Sep 17 00:00:00 2001 From: AYadrov Date: Mon, 20 Jan 2025 14:57:42 -0700 Subject: [PATCH 08/19] rival got updated, no need for the rule at Makefile + raco fmt --- Makefile | 2 - src/syntax/syntax.rkt | 113 +++++++++++++++++++----------------------- 2 files changed, 51 insertions(+), 64 deletions(-) diff --git a/Makefile b/Makefile index e55090f3e..8d22149e1 100644 --- a/Makefile +++ b/Makefile @@ -13,8 +13,6 @@ clean: raco pkg remove --force --no-docs egg-herbie-windows && echo "Uninstalled old egg-herbie" || : raco pkg remove --force --no-docs egg-herbie-osx && echo "Uninstalled old egg-herbie" || : raco pkg remove --force --no-docs egg-herbie-macosm1 && echo "Uninstalled old egg-herbie" || : - raco pkg remove --force --no-docs rival && echo "Uninstalled old rival" || : - raco pkg install rival && echo "Installing new rival" || : update: raco pkg install --skip-installed --no-docs --auto --name herbie src/ diff --git a/src/syntax/syntax.rkt b/src/syntax/syntax.rkt index 4fcc8d7a2..086f7c4cc 100644 --- a/src/syntax/syntax.rkt +++ b/src/syntax/syntax.rkt @@ -105,76 +105,65 @@ ;; Rival-supported operators ; real constants (encoded as nullary operators) -(define-operators - [PI : -> real] - [E : -> real] - [INFINITY : -> real] - [NAN : -> real]) +(define-operators [PI : -> real] [E : -> real] [INFINITY : -> real] [NAN : -> real]) ; boolean constants (encoded as nullary operators) -(define-operators - [TRUE : -> bool] - [FALSE : -> bool]) +(define-operators [TRUE : -> bool] [FALSE : -> bool]) ; boolean operators -(define-operators - [not : bool -> bool] - [and : bool bool -> bool] - [or : bool bool -> bool]) +(define-operators [not : bool -> bool] [and : bool bool -> bool] [or : bool bool -> bool]) ; real-boolean operators -(define-operators - [== : real real -> bool] - [!= : real real -> bool] - [< : real real -> bool] - [> : real real -> bool] - [<= : real real -> bool] - [>= : real real -> bool]) +(define-operators [== : real real -> bool] + [!= : real real -> bool] + [< : real real -> bool] + [> : real real -> bool] + [<= : real real -> bool] + [>= : real real -> bool]) ; real operators -(define-operators - [acos : real -> real] - [acosh : real -> real] - [asin : real -> real] - [asinh : real -> real] - [atan : real -> real] - [atanh : real -> real] - [cbrt : real -> real] - [ceil : real -> real] - [cos : real -> real] - [cosh : real -> real] - [erf : real -> real] - [exp : real -> real] - [exp2 : real -> real] - [fabs : real -> real] - [floor : real -> real] - [lgamma : real -> real] - [log : real -> real] - [log10 : real -> real] - [log2 : real -> real] - [logb : real -> real] - [neg : real -> real] - [rint : real -> real] - [round : real -> real] - [sin : real -> real] - [sinh : real -> real] - [sqrt : real -> real] - [tan : real -> real] - [tanh : real -> real] - [tgamma : real -> real] - [trunc : real -> real] - [+ : real real -> real] - [- : real real -> real] - [* : real real -> real] - [/ : real real -> real] - [atan2 : real real -> real] - [copysign : real real -> real] - [fdim : real real -> real] - [fmax : real real -> real] - [fmin : real real -> real] - [fmod : real real -> real] - [pow : real real -> real] - [remainder : real real -> real]) +(define-operators [acos : real -> real] + [acosh : real -> real] + [asin : real -> real] + [asinh : real -> real] + [atan : real -> real] + [atanh : real -> real] + [cbrt : real -> real] + [ceil : real -> real] + [cos : real -> real] + [cosh : real -> real] + [erf : real -> real] + [exp : real -> real] + [exp2 : real -> real] + [fabs : real -> real] + [floor : real -> real] + [lgamma : real -> real] + [log : real -> real] + [log10 : real -> real] + [log2 : real -> real] + [logb : real -> real] + [neg : real -> real] + [rint : real -> real] + [round : real -> real] + [sin : real -> real] + [sinh : real -> real] + [sqrt : real -> real] + [tan : real -> real] + [tanh : real -> real] + [tgamma : real -> real] + [trunc : real -> real] + [+ : real real -> real] + [- : real real -> real] + [* : real real -> real] + [/ : real real -> real] + [atan2 : real real -> real] + [copysign : real real -> real] + [fdim : real real -> real] + [fmax : real real -> real] + [fmin : real real -> real] + [fmod : real real -> real] + [pow : real real -> real] + [remainder : real real -> real]) (module+ test ; check expected number of operators From d49a1a64bcd1ce7ad439a770f450cd50c6f4abff Mon Sep 17 00:00:00 2001 From: AYadrov Date: Mon, 20 Jan 2025 15:12:27 -0700 Subject: [PATCH 09/19] raco fmt + removed useless function --- src/core/programs.rkt | 3 ++- src/core/sampling.rkt | 11 --------- src/reports/history.rkt | 30 +++++++++++------------ src/syntax/matcher.rkt | 16 ++++++------ src/syntax/platform.rkt | 54 ++++++++++++++++++++--------------------- 5 files changed, 52 insertions(+), 62 deletions(-) diff --git a/src/core/programs.rkt b/src/core/programs.rkt index e00d0b0d8..388a62635 100644 --- a/src/core/programs.rkt +++ b/src/core/programs.rkt @@ -180,7 +180,8 @@ (define/contract (location-get loc prog) (-> location? expr? expr?) ; Clever continuation usage to early-return - (let/ec return (location-do loc prog return))) + (let/ec return + (location-do loc prog return))) (define/contract (replace-expression expr from to) (-> expr? expr? expr? expr?) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 2889b491e..8a0250eca 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -29,17 +29,6 @@ (map (lambda (interval) (fpbench-ival->ival var-repr interval)) (range-table-ref range-table var-name))))) -(define (subsplit-hyperrects hyperrects var-reprs) - (for/fold ([storage '()]) ([hyperrect (in-list hyperrects)]) - (append storage - (apply cartesian-product - (for/list ([range (in-list hyperrect)] - [repr (in-list var-reprs)]) - (match (two-midpoints repr (ival-lo range) (ival-hi range)) - [(cons midleft midright) - (list (ival (ival-lo range) midleft) (ival midright (ival-hi range)))] - [#f (list range)])))))) - (define (fpbench-ival->ival repr fpbench-interval) (match-define (interval lo hi lo? hi?) fpbench-interval) (match (representation-type repr) diff --git a/src/reports/history.rkt b/src/reports/history.rkt index 9b5de8e20..c6c34aeab 100644 --- a/src/reports/history.rkt +++ b/src/reports/history.rkt @@ -49,21 +49,21 @@ (define (splice-proof-step step) (let/ec k - (let loop ([expr step] - [loc '()]) - (match expr - [(list 'Rewrite=> rule sub) - (define loc* (reverse loc)) - (k 'Rewrite=> rule loc* (location-do loc* step (λ _ sub)))] - [(list 'Rewrite<= rule sub) - (define loc* (reverse loc)) - (k 'Rewrite<= rule loc* (location-do loc* step (λ _ sub)))] - [(list op args ...) - (for ([arg (in-list args)] - [i (in-naturals 1)]) - (loop arg (cons i loc)))] - [_ (void)])) - (k 'Goal #f '() step))) + (let loop ([expr step] + [loc '()]) + (match expr + [(list 'Rewrite=> rule sub) + (define loc* (reverse loc)) + (k 'Rewrite=> rule loc* (location-do loc* step (λ _ sub)))] + [(list 'Rewrite<= rule sub) + (define loc* (reverse loc)) + (k 'Rewrite<= rule loc* (location-do loc* step (λ _ sub)))] + [(list op args ...) + (for ([arg (in-list args)] + [i (in-naturals 1)]) + (loop arg (cons i loc)))] + [_ (void)])) + (k 'Goal #f '() step))) (define (altn-errors altn pcontext pcontext2 ctx) (define repr (context-repr ctx)) diff --git a/src/syntax/matcher.rkt b/src/syntax/matcher.rkt index e9a3c6269..949e4b8cc 100644 --- a/src/syntax/matcher.rkt +++ b/src/syntax/matcher.rkt @@ -11,14 +11,14 @@ (and binding1 binding2 (let/ec quit - (for/fold ([binding binding1]) ([(k v) (in-dict binding2)]) - (dict-update binding - k - (λ (x) - (if (equal? x v) - v - (quit #f))) - v))))) + (for/fold ([binding binding1]) ([(k v) (in-dict binding2)]) + (dict-update binding + k + (λ (x) + (if (equal? x v) + v + (quit #f))) + v))))) ;; Pattern matcher that returns a substitution or #f. ;; A substitution is an association list of symbols and expressions. diff --git a/src/syntax/platform.rkt b/src/syntax/platform.rkt index 7a6bdf23c..f19d55990 100644 --- a/src/syntax/platform.rkt +++ b/src/syntax/platform.rkt @@ -472,38 +472,38 @@ ;; Fails if the result is not well-typed. (define (try-lower expr repr op->impl) (let/ec k - (define env '()) - (define expr* - (let loop ([expr expr] - [repr repr]) - (match expr - [(? symbol? x) ; variable - (match (dict-ref env x #f) - [#f (set! env (cons (cons x repr) env))] - [(? (curry equal? repr)) (k #f env)] - [_ (void)]) - x] - ; number - [(? number? n) (literal n (representation-name repr))] - [(list 'if cond ift iff) ; if expression - (list 'if (loop cond (get-representation 'bool)) (loop ift repr) (loop iff repr))] - [(list op args ...) ; application - (define impl (dict-ref op->impl op)) - (unless (equal? (impl-info impl 'otype) repr) - (k #f env)) - (cons impl (map loop args (impl-info impl 'itype)))]))) - (define ctx (context (map car env) repr (map cdr env))) - (values (and (equal? (repr-of expr* ctx) repr) expr*) env))) + (define env '()) + (define expr* + (let loop ([expr expr] + [repr repr]) + (match expr + [(? symbol? x) ; variable + (match (dict-ref env x #f) + [#f (set! env (cons (cons x repr) env))] + [(? (curry equal? repr)) (k #f env)] + [_ (void)]) + x] + ; number + [(? number? n) (literal n (representation-name repr))] + [(list 'if cond ift iff) ; if expression + (list 'if (loop cond (get-representation 'bool)) (loop ift repr) (loop iff repr))] + [(list op args ...) ; application + (define impl (dict-ref op->impl op)) + (unless (equal? (impl-info impl 'otype) repr) + (k #f env)) + (cons impl (map loop args (impl-info impl 'itype)))]))) + (define ctx (context (map car env) repr (map cdr env))) + (values (and (equal? (repr-of expr* ctx) repr) expr*) env))) ;; Merges two variable -> value mappings. ;; If any mapping disagrees, the result is `#f`. (define (merge-envs env1 env2) (let/ec k - (for/fold ([env env1]) ([(x ty) (in-dict env2)]) - (match (dict-ref env x #f) - [#f (cons (cons x ty) env)] - [(? (curry equal? ty)) env] - [_ (k #f)])))) + (for/fold ([env env1]) ([(x ty) (in-dict env2)]) + (match (dict-ref env x #f) + [#f (cons (cons x ty) env)] + [(? (curry equal? ty)) env] + [_ (k #f)])))) ;; Synthesizes impl-to-impl rules for a given platform. ;; If a rule is over implementations, filters by supported implementations. From 39a4b1868488a477bef64cc1abc366fe3035558d Mon Sep 17 00:00:00 2001 From: AYadrov Date: Mon, 20 Jan 2025 15:34:36 -0700 Subject: [PATCH 10/19] contract bug fix --- src/core/rival.rkt | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/core/rival.rkt b/src/core/rival.rkt index f606e72c5..398a9399b 100644 --- a/src/core/rival.rkt +++ b/src/core/rival.rkt @@ -25,8 +25,7 @@ [real-apply (->* (real-compiler? list?) ((or/c (vectorof any/c) boolean?)) (values symbol? any/c))] [real-compiler-clear! (-> real-compiler-clear! void?)] - [real-compiler-analyze - (-> real-compiler? (vectorof ival?) (listof (or/c ival? (vectorof any/c) boolean?)))])) + [real-compiler-analyze (-> real-compiler? (vectorof ival?) (listof any/c))])) (define (unified-contexts? ctxs) (and ((non-empty-listof context?) ctxs) @@ -117,7 +116,4 @@ ;; for the given inputs range. The result is an interval representing ;; how certain the result is: no, maybe, yes. (define (real-compiler-analyze compiler input-ranges) - (define res (rival-analyze (real-compiler-machine compiler) input-ranges)) - (if (list? res) - (car res) - res)) + (rival-analyze (real-compiler-machine compiler) input-ranges)) From d371c1395d094c022e1145d7a7ed5cccdbf185b9 Mon Sep 17 00:00:00 2001 From: AYadrov Date: Tue, 21 Jan 2025 12:45:07 -0700 Subject: [PATCH 11/19] slight changes to make code look better + fmt --- src/core/sampling.rkt | 1 - src/core/searchreals.rkt | 12 +++-- src/syntax/syntax.rkt | 113 +++++++++++++++++++++------------------ 3 files changed, 69 insertions(+), 57 deletions(-) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 8a0250eca..8273cab54 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -1,6 +1,5 @@ #lang racket (require math/bigfloat - math/flonum rival math/base (only-in fpbench interval range-table-ref condition->range-table [expr? fpcore-expr?])) diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 274a9859d..368df378c 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -30,6 +30,11 @@ (+ 1 (- (->ordinal (ival-hi interval)) (->ordinal (ival-lo interval))))))) (define (search-step compiler space split-var) + (define (drop-hints-from-rects rect) + (match rect + [(cons _ rect*) rect*] + [_ rect])) + (define vars (real-compiler-vars compiler)) (define reprs (real-compiler-var-reprs compiler)) (match-define (search-space true false other) space) @@ -37,11 +42,7 @@ (for/fold ([true* true] [false* false] [other* '()]) - ([rect (in-list other)]) - ; if a rect has a hint stored already then drop that hint - (when (not (equal? (length vars) (length rect))) - (set! rect (rest rect))) - + ([rect (in-list (map drop-hints-from-rects other))]) (match-define (list (ival err err?) hint converged?) (real-compiler-analyze compiler (list->vector rect))) (when (eq? err 'unsamplable) @@ -72,6 +73,7 @@ (define (make-sampling-table reprs true false other) (define denom (total-weight reprs)) + ; map rest = drop hint (define true-weight (apply + (map (curryr hyperrect-weight reprs) (map rest true)))) (define false-weight (apply + (map (curryr hyperrect-weight reprs) false))) (define other-weight (apply + (map (curryr hyperrect-weight reprs) (map rest other)))) diff --git a/src/syntax/syntax.rkt b/src/syntax/syntax.rkt index 664ef1085..a6dc32606 100644 --- a/src/syntax/syntax.rkt +++ b/src/syntax/syntax.rkt @@ -94,65 +94,76 @@ ;; Rival-supported operators ; real constants (encoded as nullary operators) -(define-operators [PI : -> real] [E : -> real] [INFINITY : -> real] [NAN : -> real]) +(define-operators + [PI : -> real] + [E : -> real] + [INFINITY : -> real] + [NAN : -> real]) ; boolean constants (encoded as nullary operators) -(define-operators [TRUE : -> bool] [FALSE : -> bool]) +(define-operators + [TRUE : -> bool] + [FALSE : -> bool]) ; boolean operators -(define-operators [not : bool -> bool] [and : bool bool -> bool] [or : bool bool -> bool]) +(define-operators + [not : bool -> bool] + [and : bool bool -> bool] + [or : bool bool -> bool]) ; real-boolean operators -(define-operators [== : real real -> bool] - [!= : real real -> bool] - [< : real real -> bool] - [> : real real -> bool] - [<= : real real -> bool] - [>= : real real -> bool]) +(define-operators + [== : real real -> bool] + [!= : real real -> bool] + [< : real real -> bool] + [> : real real -> bool] + [<= : real real -> bool] + [>= : real real -> bool]) ; real operators -(define-operators [acos : real -> real] - [acosh : real -> real] - [asin : real -> real] - [asinh : real -> real] - [atan : real -> real] - [atanh : real -> real] - [cbrt : real -> real] - [ceil : real -> real] - [cos : real -> real] - [cosh : real -> real] - [erf : real -> real] - [exp : real -> real] - [exp2 : real -> real] - [fabs : real -> real] - [floor : real -> real] - [lgamma : real -> real] - [log : real -> real] - [log10 : real -> real] - [log2 : real -> real] - [logb : real -> real] - [neg : real -> real] - [rint : real -> real] - [round : real -> real] - [sin : real -> real] - [sinh : real -> real] - [sqrt : real -> real] - [tan : real -> real] - [tanh : real -> real] - [tgamma : real -> real] - [trunc : real -> real] - [+ : real real -> real] - [- : real real -> real] - [* : real real -> real] - [/ : real real -> real] - [atan2 : real real -> real] - [copysign : real real -> real] - [fdim : real real -> real] - [fmax : real real -> real] - [fmin : real real -> real] - [fmod : real real -> real] - [pow : real real -> real] - [remainder : real real -> real]) +(define-operators + [acos : real -> real] + [acosh : real -> real] + [asin : real -> real] + [asinh : real -> real] + [atan : real -> real] + [atanh : real -> real] + [cbrt : real -> real] + [ceil : real -> real] + [cos : real -> real] + [cosh : real -> real] + [erf : real -> real] + [exp : real -> real] + [exp2 : real -> real] + [fabs : real -> real] + [floor : real -> real] + [lgamma : real -> real] + [log : real -> real] + [log10 : real -> real] + [log2 : real -> real] + [logb : real -> real] + [neg : real -> real] + [rint : real -> real] + [round : real -> real] + [sin : real -> real] + [sinh : real -> real] + [sqrt : real -> real] + [tan : real -> real] + [tanh : real -> real] + [tgamma : real -> real] + [trunc : real -> real] + [+ : real real -> real] + [- : real real -> real] + [* : real real -> real] + [/ : real real -> real] + [atan2 : real real -> real] + [copysign : real real -> real] + [fdim : real real -> real] + [fmax : real real -> real] + [fmin : real real -> real] + [fmod : real real -> real] + [pow : real real -> real] + [remainder : real real -> real]) (module+ test ; check expected number of operators From 98301eaee42b4933ea7a29136fa3f82575bab555 Mon Sep 17 00:00:00 2001 From: AYadrov Date: Tue, 21 Jan 2025 14:00:34 -0700 Subject: [PATCH 12/19] bug --- src/core/searchreals.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 368df378c..0432bd0b4 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -32,7 +32,7 @@ (define (search-step compiler space split-var) (define (drop-hints-from-rects rect) (match rect - [(cons _ rect*) rect*] + [(cons (vector _ ...) rect*) rect*] [_ rect])) (define vars (real-compiler-vars compiler)) From 98ad6ae7f1d1dd17e53b95a177207441112ed3d8 Mon Sep 17 00:00:00 2001 From: AYadrov Date: Tue, 21 Jan 2025 14:05:53 -0700 Subject: [PATCH 13/19] fmt --- src/core/searchreals.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 0432bd0b4..286ba69e2 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -34,7 +34,7 @@ (match rect [(cons (vector _ ...) rect*) rect*] [_ rect])) - + (define vars (real-compiler-vars compiler)) (define reprs (real-compiler-var-reprs compiler)) (match-define (search-space true false other) space) @@ -73,7 +73,7 @@ (define (make-sampling-table reprs true false other) (define denom (total-weight reprs)) - ; map rest = drop hint + ; map rest = drop hint (define true-weight (apply + (map (curryr hyperrect-weight reprs) (map rest true)))) (define false-weight (apply + (map (curryr hyperrect-weight reprs) false))) (define other-weight (apply + (map (curryr hyperrect-weight reprs) (map rest other)))) From 092c3a12d552d8d4455cdef34d2d7ca811b5bf36 Mon Sep 17 00:00:00 2001 From: AYadrov Date: Wed, 22 Jan 2025 10:36:06 -0700 Subject: [PATCH 14/19] added analyze hint optimization --- src/core/rival.rkt | 14 ++++++------ src/core/sampling.rkt | 13 +++++------ src/core/searchreals.rkt | 49 +++++++++++++++++++++------------------- 3 files changed, 39 insertions(+), 37 deletions(-) diff --git a/src/core/rival.rkt b/src/core/rival.rkt index 398a9399b..255099f14 100644 --- a/src/core/rival.rkt +++ b/src/core/rival.rkt @@ -25,7 +25,10 @@ [real-apply (->* (real-compiler? list?) ((or/c (vectorof any/c) boolean?)) (values symbol? any/c))] [real-compiler-clear! (-> real-compiler-clear! void?)] - [real-compiler-analyze (-> real-compiler? (vectorof ival?) (listof any/c))])) + [real-compiler-analyze + (->* (real-compiler? (vectorof ival?)) + ((or/c (vectorof any/c) boolean?)) + (listof any/c))])) (define (unified-contexts? ctxs) (and ((non-empty-listof context?) ctxs) @@ -80,10 +83,7 @@ [exn:rival:unsamplable? (lambda (e) (values 'exit #f))]) (parameterize ([*rival-max-precision* (*max-mpfr-prec*)] [*rival-max-iterations* 5]) - (define value - (rest (vector->list (if hint ; rest = drop precondition - (rival-apply machine pt* hint) - (rival-apply machine pt*))))) + (define value (rest (vector->list (rival-apply machine pt* hint)))) ; rest = drop precondition (values 'valid value)))) (when (> (rival-profile machine 'bumps) 0) (warn 'ground-truth @@ -115,5 +115,5 @@ ;; Returns whether the machine is guaranteed to raise an exception ;; for the given inputs range. The result is an interval representing ;; how certain the result is: no, maybe, yes. -(define (real-compiler-analyze compiler input-ranges) - (rival-analyze (real-compiler-machine compiler) input-ranges)) +(define (real-compiler-analyze compiler input-ranges [hint #f]) + (rival-analyze (real-compiler-machine compiler) input-ranges hint)) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 8273cab54..1f0825afd 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -78,12 +78,11 @@ (when (> search-result 0) (check-true (<= (vector-ref arr (- search-result 1)) search-for))))) -;; hints-hyperrects* is a (listof '(hint hyperrect)) -(define (make-hyperrect-sampler hints-hyperrects* reprs) - (when (null? hints-hyperrects*) +(define (make-hyperrect-sampler hyperrects* hints* reprs) + (when (null? hyperrects*) (raise-herbie-sampling-error "No valid values." #:url "faq.html#no-valid-values")) - (define hints (list->vector (map car hints-hyperrects*))) - (define hyperrects (list->vector (map rest hints-hyperrects*))) + (define hints (list->vector hints*)) + (define hyperrects (list->vector hyperrects*)) (define lo-ends (for/vector #:length (vector-length hyperrects) ([hyperrect (in-vector hyperrects)]) @@ -130,9 +129,9 @@ (timeline-push! 'method "search") (define hyperrects-analysis (precondition->hyperrects pre vars var-reprs)) ; hints-hyperrects is a (listof '(hint hyperrect)) - (match-define (cons hints-hyperrects sampling-table) + (match-define (list hyperrects hints sampling-table) (find-intervals compiler hyperrects-analysis #:fuel (*max-find-range-depth*))) - (cons (make-hyperrect-sampler hints-hyperrects var-reprs) sampling-table)] + (cons (make-hyperrect-sampler hyperrects hints var-reprs) sampling-table)] [else (timeline-push! 'method "random") ; sampler return false hint since rival-analyze has not been called in random method diff --git a/src/core/searchreals.rkt b/src/core/searchreals.rkt index 286ba69e2..b430b195e 100644 --- a/src/core/searchreals.rkt +++ b/src/core/searchreals.rkt @@ -13,10 +13,10 @@ (provide find-intervals hyperrect-weight) -(struct search-space (true false other)) +(struct search-space (true false other true-hints other-hints)) (define (make-search-space . ranges) - (search-space '() '() ranges)) + (search-space '() '() ranges '() (make-list (length ranges) #f))) (define (total-weight reprs) (expt 2 (apply + (map representation-total-bits reprs)))) @@ -30,21 +30,19 @@ (+ 1 (- (->ordinal (ival-hi interval)) (->ordinal (ival-lo interval))))))) (define (search-step compiler space split-var) - (define (drop-hints-from-rects rect) - (match rect - [(cons (vector _ ...) rect*) rect*] - [_ rect])) - (define vars (real-compiler-vars compiler)) (define reprs (real-compiler-var-reprs compiler)) - (match-define (search-space true false other) space) - (define-values (true* false* other*) + (match-define (search-space true false other true-hints other-hints) space) + (define-values (true* false* other* true-hints* other-hints*) (for/fold ([true* true] [false* false] - [other* '()]) - ([rect (in-list (map drop-hints-from-rects other))]) - (match-define (list (ival err err?) hint converged?) - (real-compiler-analyze compiler (list->vector rect))) + [other* '()] + [true-hints* true-hints] + [other-hints* '()]) + ([rect (in-list other)] + [hint (in-list other-hints)]) + (match-define (list (ival err err?) hint* converged?) + (real-compiler-analyze compiler (list->vector rect) hint)) (when (eq? err 'unsamplable) (warn 'ground-truth #:url "faq.html#ground-truth" @@ -58,8 +56,9 @@ repr)) (format "~a = ~a" var val)))) (cond - [err (values true* (cons rect false*) other*)] - [(and (not err?) converged?) (values (cons (cons hint rect) true*) false* other*)] + [err (values true* (cons rect false*) other* true-hints* other-hints*)] + [(and (not err?) converged?) + (values (cons rect true*) false* other* (cons hint* true-hints*) other-hints*)] [else (define range (list-ref rect split-var)) (define repr (list-ref reprs split-var)) @@ -67,16 +66,19 @@ [(cons midleft midright) (define rect-lo (list-set rect split-var (ival (ival-lo range) midleft))) (define rect-hi (list-set rect split-var (ival midright (ival-hi range)))) - (values true* false* (list* (cons hint rect-lo) (cons hint rect-hi) other*))] - [#f (values true* false* (cons (cons hint rect) other*))])]))) - (search-space true* false* other*)) + (values true* + false* + (list* rect-lo rect-hi other*) + true-hints* + (list* hint* hint* other-hints*))] + [#f (values true* false* (cons rect other*) true-hints* (cons hint* other-hints*))])]))) + (search-space true* false* other* true-hints* other-hints*)) (define (make-sampling-table reprs true false other) (define denom (total-weight reprs)) - ; map rest = drop hint - (define true-weight (apply + (map (curryr hyperrect-weight reprs) (map rest true)))) + (define true-weight (apply + (map (curryr hyperrect-weight reprs) true))) (define false-weight (apply + (map (curryr hyperrect-weight reprs) false))) - (define other-weight (apply + (map (curryr hyperrect-weight reprs) (map rest other)))) + (define other-weight (apply + (map (curryr hyperrect-weight reprs) other))) (define out (make-hash)) (hash-set! out 'valid (exact->inexact (/ true-weight denom))) (hash-set! out 'unknown (exact->inexact (/ other-weight denom))) @@ -91,11 +93,12 @@ (map (curryr cons 'other) rects) (let loop ([space (apply make-search-space rects)] [n 0]) - (match-define (search-space true false other) space) + (match-define (search-space true false other true-hints other-hints) space) (timeline-push! 'sampling n (make-sampling-table var-reprs true false other)) (define n* (remainder n (length (first rects)))) (if (or (>= n depth) (empty? (search-space-other space)) (>= (length other) (expt 2 depth))) - (cons (append (search-space-true space) (search-space-other space)) + (list (append (search-space-true space) (search-space-other space)) + (append (search-space-true-hints space) (search-space-other-hints space)) (make-sampling-table var-reprs true false other)) (loop (search-step compiler space n*) (+ n 1)))))) From 6e1bf1d88497fae2ba335d3899e4620f8d972d14 Mon Sep 17 00:00:00 2001 From: Edward Misback Date: Thu, 23 Jan 2025 18:26:33 -0800 Subject: [PATCH 15/19] Add "e.g." to placeholder text --- src/api/demo.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/demo.rkt b/src/api/demo.rkt index 93c4fdbe3..9f2c1b80e 100644 --- a/src/api/demo.rkt +++ b/src/api/demo.rkt @@ -167,8 +167,8 @@ `(form ([action ,(url improve)] [method "post"] [id "formula"] [data-progress ,(url improve-start)]) (textarea ([name "formula"] [autofocus "true"] - [placeholder "(FPCore (x) (- (sqrt (+ x 1)) (sqrt x)))"])) - (input ([name "formula-math"] [placeholder "sqrt(x + 1) - sqrt(x)"])) + [placeholder "e.g. (FPCore (x) (- (sqrt (+ x 1)) (sqrt x)))"])) + (input ([name "formula-math"] [placeholder "e.g. sqrt(x + 1) - sqrt(x)"])) (table ([id "input-ranges"])) (ul ([id "errors"])) (ul ([id "warnings"])) From de99698371ea6567f9f546011036b1812df307d8 Mon Sep 17 00:00:00 2001 From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com> Date: Sun, 26 Jan 2025 01:28:29 +0000 Subject: [PATCH 16/19] Fix 1 occurrence of `inline-unnecessary-define` This variable is returned immediately and can be inlined. --- src/core/localize.rkt | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/src/core/localize.rkt b/src/core/localize.rkt index b092c0c5c..6a12e67ea 100644 --- a/src/core/localize.rkt +++ b/src/core/localize.rkt @@ -138,23 +138,20 @@ (- a b))) ; This `if` statement handles `inf - inf` ; rank subexpressions by cost opportunity - (define localize-costss - (for/list ([subexprs (in-list subexprss)]) - (sort (reap [sow] - (for ([subexpr (in-list subexprs)]) - (match subexpr - [(? literal?) (void)] - [(? symbol?) (void)] - [(approx _ impl) - (define cost-opp (cost-opportunity subexpr (list impl))) - (sow (cons cost-opp subexpr))] - [(list _ args ...) - (define cost-opp (cost-opportunity subexpr args)) - (sow (cons cost-opp subexpr))]))) - > - #:key car))) - - localize-costss) + (for/list ([subexprs (in-list subexprss)]) + (sort (reap [sow] + (for ([subexpr (in-list subexprs)]) + (match subexpr + [(? literal?) (void)] + [(? symbol?) (void)] + [(approx _ impl) + (define cost-opp (cost-opportunity subexpr (list impl))) + (sow (cons cost-opp subexpr))] + [(list _ args ...) + (define cost-opp (cost-opportunity subexpr args)) + (sow (cons cost-opp subexpr))]))) + > + #:key car))) (define (batch-localize-errors exprs ctx) (define subexprss (map all-subexpressions exprs)) From 35e1dd4f384b5e81127a9591916602ab6d295b3d Mon Sep 17 00:00:00 2001 From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com> Date: Sun, 26 Jan 2025 01:28:29 +0000 Subject: [PATCH 17/19] Fix 3 occurrences of `if-let-to-cond` `cond` with internal definitions is preferred over `if` with `let`, to reduce nesting --- src/core/localize.rkt | 14 ++++++++------ src/core/programs.rkt | 13 +++++++------ src/core/sampling.rkt | 8 +++++--- 3 files changed, 20 insertions(+), 15 deletions(-) diff --git a/src/core/localize.rkt b/src/core/localize.rkt index 6a12e67ea..c27d14663 100644 --- a/src/core/localize.rkt +++ b/src/core/localize.rkt @@ -361,12 +361,14 @@ (define exact-error (~s (translate-booleans (first (hash-ref data 'exact-values))))) (define actual-error (~s (translate-booleans (first (hash-ref data 'approx-values))))) (define percent-accurate - (if (nan? (first (hash-ref data 'absolute-error))) - 'invalid ; HACK: should specify if invalid or unsamplable - (let* ([repr (repr-of expr ctx)] - [total-bits (representation-total-bits repr)] - [bits-error (ulps->bits (first (hash-ref data 'ulp-errs)))]) - (* 100 (- 1 (/ bits-error total-bits)))))) + (cond + [(nan? (first (hash-ref data 'absolute-error))) + 'invalid] ; HACK: should specify if invalid or unsamplable + [else + (define repr (repr-of expr ctx)) + (define total-bits (representation-total-bits repr)) + (define bits-error (ulps->bits (first (hash-ref data 'ulp-errs)))) + (* 100 (- 1 (/ bits-error total-bits)))])) (hasheq 'ulps-error ulp-error 'avg-error diff --git a/src/core/programs.rkt b/src/core/programs.rkt index b3e58e8a1..f12f1ee2a 100644 --- a/src/core/programs.rkt +++ b/src/core/programs.rkt @@ -100,12 +100,13 @@ [else (let loop ([a a] [b b]) - (if (null? a) - 0 - (let ([cmp (expr-cmp (car a) (car b))]) - (if (zero? cmp) - (loop (cdr a) (cdr b)) - cmp))))])] + (cond + [(null? a) 0] + [else + (define cmp (expr-cmp (car a) (car b))) + (if (zero? cmp) + (loop (cdr a) (cdr b)) + cmp)]))])] [((? list?) _) 1] [(_ (? list?)) -1] [((? approx?) (? approx?)) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 1f0825afd..014aae187 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -66,9 +66,11 @@ (module+ test (define rand-list (let loop ([current 0]) - (if (> current 200) - empty - (let ([r (+ current (random-integer 1 10))]) (cons r (loop r)))))) + (cond + [(> current 200) empty] + [else + (define r (+ current (random-integer 1 10))) + (cons r (loop r))]))) (define arr (list->vector rand-list)) (for ([i (range 0 20)]) (define max-num (vector-ref arr (- (vector-length arr) 1))) From 1a6bcc3b00a0f43355fe6b141c26be2332b55c07 Mon Sep 17 00:00:00 2001 From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com> Date: Sun, 26 Jan 2025 01:28:29 +0000 Subject: [PATCH 18/19] Fix 1 occurrence of `zero-comparison-to-negative?` This expression is equivalent to calling the `negative?` predicate. --- src/core/programs.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/programs.rkt b/src/core/programs.rkt index f12f1ee2a..0cc43c0ca 100644 --- a/src/core/programs.rkt +++ b/src/core/programs.rkt @@ -132,7 +132,7 @@ [else 1])])) (define (expr Date: Sun, 26 Jan 2025 01:28:29 +0000 Subject: [PATCH 19/19] Fix 1 occurrence of `zero-comparison-to-positive?` This expression is equivalent to calling the `positive?` predicate. --- src/core/sampling.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/sampling.rkt b/src/core/sampling.rkt index 014aae187..f29a3c004 100644 --- a/src/core/sampling.rkt +++ b/src/core/sampling.rkt @@ -77,7 +77,7 @@ (define search-for (random-integer 0 max-num)) (define search-result (binary-search arr search-for)) (check-true (> (vector-ref arr search-result) search-for)) - (when (> search-result 0) + (when (positive? search-result) (check-true (<= (vector-ref arr (- search-result 1)) search-for))))) (define (make-hyperrect-sampler hyperrects* hints* reprs)