Merge pull request #1416 from herbie-fp/sound-X-rewrites

Drop `sound-X` operations with rewrites

Author: pavpanchekha

AGENTS.md

@@ -8,6 +8,12 @@
 - Run `racket src/main.rkt report bench/tutorial.fpcore tmp` to test
   that your changes work; this should take about 5-10 seconds and all
   of the tests should pass, getting basically perfect accuracy.
+- After running tests, you should be able to look into `tmp`, and see
+  one directory per benchmark. Each directory has a `graph.html` with
+  more detail on what happened, including tracebacks for crashes.
+- Herbie prints a seed every time it runs; you can pass --seed N after
+  the "report" argument to fix a seed. That should be perfectly
+  reproducible.
 - You can also run the unit tests with `raco test <file>`, when unit
   tests exist. Often they don't.
 

src/core/egg-herbie.rkt

@@ -289,7 +289,7 @@
       [(list 'Rewrite<= rule expr) (list 'Rewrite<= (get-canon-rule-name rule rule) (loop expr type))]
       [(list op args ...)
        #:when (string-prefix? (symbol->string op) "sound-")
-       (define op* (string->symbol (substring (symbol->string (car expr)) (string-length "sound-"))))
+       (define op* (string->symbol (substring (symbol->string op) (string-length "sound-"))))
        (define args* (drop-right args 1))
        (cons op* (map loop args* (map (const 'real) args*)))]
       [(list op args ...)
@@ -525,16 +525,13 @@
 ;; Synthesizes lowering rules for a given platform.
 (define (platform-lowering-rules [pform (*active-platform*)])
   (define impls (platform-impls pform))
-  (append*
-   (for/list ([impl (in-list impls)])
-     (hash-ref!
-      (*lowering-rules*)
-      (cons impl pform)
-      (lambda ()
-        (define name (sym-append 'lower- impl))
-        (define-values (vars spec-expr impl-expr) (impl->rule-parts impl))
-        (list (rule name spec-expr impl-expr '(lowering))
-              (rule (sym-append 'lower-sound- impl) (add-sound spec-expr) impl-expr '(lowering))))))))
+  (append* (for/list ([impl (in-list impls)])
+             (hash-ref! (*lowering-rules*)
+                        (cons impl pform)
+                        (lambda ()
+                          (define name (sym-append 'lower- impl))
+                          (define-values (vars spec-expr impl-expr) (impl->rule-parts impl))
+                          (list (rule name spec-expr impl-expr '(lowering))))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Racket egraph
@@ -1257,6 +1254,9 @@
           ['lower
            (define rules (expand-rules (platform-lowering-rules)))
            (egraph-run-rules egg-graph rules #:iter-limit 1 #:scheduler 'simple)]
+          ['unsound
+           (define rules (expand-rules (*sound-removal-rules*)))
+           (egraph-run-rules egg-graph rules #:iter-limit 1 #:scheduler 'simple)]
           ['rewrite
            (define rules (expand-rules (*rules*)))
            (egraph-run-rules egg-graph rules #:node-limit (*node-limit*))]))
@@ -1298,13 +1298,14 @@
 ;; The schedule is a list of step symbols:
 ;;  - `lift`: run lifting rules for 1 iteration with simple scheduler
 ;;  - `rewrite`: run rewrite rules up to node limit with backoff scheduler
+;;  - `unsound`: run sound-removal rules for 1 iteration with simple scheduler
 ;;  - `lower`: run lowering rules for 1 iteration with simple scheduler
 (define (make-egraph batch brfs reprs schedule ctx)
   (define (oops! fmt . args)
     (apply error 'verify-schedule! fmt args))
   ; verify the schedule
   (for ([step (in-list schedule)])
-    (unless (memq step '(lift lower rewrite))
+    (unless (memq step '(lift lower unsound rewrite))
       (oops! "unknown schedule step `~a`" step)))
 
   (define-values (root-ids egg-graph) (egraph-run-schedule batch brfs schedule ctx))

src/core/patch.rkt

@@ -157,11 +157,9 @@
 
 (define (run-rr altns global-batch)
   (timeline-event! 'rewrite)
-  ; generate required rules
-  (define rules (*rules*))
 
-  ; egg schedule (3-phases for mathematical rewrites and implementation selection)
-  (define schedule '(lift rewrite lower))
+  ; egg schedule (4-phases for mathematical rewrites, sound-X removal, and implementation selection)
+  (define schedule '(lift rewrite unsound lower))
 
   (define brfs (map alt-expr altns))
   (define reprs (map (batch-reprs global-batch (*context*)) brfs))

src/core/rules.rkt

@@ -6,8 +6,8 @@
          "../syntax/syntax.rkt")
 
 (provide *rules*
-         (struct-out rule)
-         add-sound)
+         *sound-removal-rules*
+         (struct-out rule))
 
 ;; A rule represents "find-and-replacing" `input` by `output`. Both
 ;; are patterns, meaning that symbols represent pattern variables.
@@ -24,13 +24,6 @@
 (define (*rules*)
   (filter rule-enabled? *all-rules*))
 
-(define (add-sound expr)
-  (match expr
-    [(list (and (or '/ 'pow 'log) op) args ...)
-     `(,(sym-append "sound-" op) ,@(map add-sound args) ,(gensym))]
-    [(list op args ...) (cons op (map add-sound expr))]
-    [_ expr]))
-
 (define-syntax-rule (define-rule rname group input output)
   (set! *all-rules* (cons (rule 'rname 'input 'output '(group)) *all-rules*)))
 
@@ -612,3 +605,9 @@
   [cosh-atanh-rev (/ 1 (sqrt (- 1 (* x x)))) (cosh (atanh x))]
   [asinh-2 (acosh (+ (* 2 (* x x)) 1)) (* 2 (asinh (fabs x)))]
   [acosh-2-rev (* 2 (acosh x)) (acosh (- (* 2 (* x x)) 1))])
+
+; Sound-X removal rules: run these before lowering
+(define (*sound-removal-rules*)
+  (list (rule 'remove-sound-/ '(sound-/ a b fallback) '(/ a b) '(sound-removal))
+        (rule 'remove-sound-pow '(sound-pow a b fallback) '(pow a b) '(sound-removal))
+        (rule 'remove-sound-log '(sound-log a fallback) '(log a) '(sound-removal))))