Skip to content

Commit

Permalink
Merge pull request #1142 from herbie-fp/dump-rival
Browse files Browse the repository at this point in the history
Dump Rival commands from Herbie
  • Loading branch information
pavpanchekha authored Jan 27, 2025
2 parents e45969d + 5c378e9 commit 5f9ba85
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 6 deletions.
2 changes: 1 addition & 1 deletion src/config.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
special
bools
branches)]
[dump . (egg)]))
[dump . (egg rival)]))

(define default-flags
#hash([precision . ()]
Expand Down
32 changes: 28 additions & 4 deletions src/core/rival.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@

#lang racket

(require rival)
(require math/bigfloat
rival)

(require "../config.rkt"
"../syntax/types.rkt"
Expand Down Expand Up @@ -49,7 +50,7 @@
(lambda (x y) (- (ulp-difference x y repr) 1))))

;; Herbie's wrapper around the Rival machine abstraction.
(struct real-compiler (pre vars var-reprs exprs reprs machine))
(struct real-compiler (pre vars var-reprs exprs reprs machine dump-file))

;; Creates a Rival machine.
;; Takes a context to encode input variables and their representations,
Expand All @@ -66,18 +67,41 @@
(timeline-push! 'compiler
(apply + 1 (expr-size pre) (map expr-size specs))
(+ (length vars) (rival-profile machine 'instructions)))

(define dump-file
(cond
[(flag-set? 'dump 'rival)
(define dump-dir "dump-rival")
(unless (directory-exists? dump-dir)
(make-directory dump-dir))
(define name
(for/first ([i (in-naturals)]
#:unless (file-exists? (build-path dump-dir (format "~a.rival" i))))
(build-path dump-dir (format "~a.rival" i))))
(define dump-file (open-output-file name #:exists 'replace))
(pretty-print `(define (f ,@vars)
,@specs)
dump-file
1)
dump-file]
[else #f]))

; wrap it with useful information for Herbie
(real-compiler pre vars var-reprs specs reprs machine))
(real-compiler pre vars var-reprs specs reprs machine dump-file))

;; Runs a Rival machine on an input point.
(define (real-apply compiler pt [hint #f])
(match-define (real-compiler _ vars var-reprs _ _ machine) compiler)
(match-define (real-compiler _ vars var-reprs _ _ machine dump-file) compiler)
(define start (current-inexact-milliseconds))
(define pt*
(for/vector #:length (length vars)
([val (in-list pt)]
[repr (in-list var-reprs)])
((representation-repr->bf repr) val)))
(when dump-file
(define args (map bigfloat->rational (vector->list pt*)))
;; convert to rational, because Rival reads as exact
(pretty-print `(eval f ,@args) dump-file 1))
(define-values (status value)
(with-handlers ([exn:rival:invalid? (lambda (e) (values 'invalid #f))]
[exn:rival:unsamplable? (lambda (e) (values 'exit #f))])
Expand Down
2 changes: 1 addition & 1 deletion src/core/sampling.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@
((make-hyperrect-sampler two-point-hyperrects (list repr repr))))))

(define (make-sampler compiler)
(match-define (real-compiler pre vars var-reprs _ reprs _) compiler)
(match-define (real-compiler pre vars var-reprs _ reprs _ _) compiler)
(cond
[(and (flag-set? 'setup 'search)
(not (empty? var-reprs))
Expand Down

0 comments on commit 5f9ba85

Please sign in to comment.