Make sound-/ rules normal rules

Author: pavpanchekha

src/core/egg-herbie.rkt

@@ -1248,9 +1248,6 @@
           ['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*))]))
@@ -1292,14 +1289,13 @@
 ;; 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 unsound rewrite))
+    (unless (memq step '(lift lower rewrite))
       (oops! "unknown schedule step `~a`" step)))
 
   (define-values (root-ids egg-graph) (egraph-run-schedule batch brfs schedule ctx))

src/core/egglog-herbie.rkt

@@ -60,14 +60,13 @@
 ;; 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-egglog-runner 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 unsound rewrite))
+    (unless (memq step '(lift lower rewrite))
       (oops! "unknown schedule step `~a`" step)))
 
   ; make the runner
@@ -147,7 +146,6 @@
     (match step
       ['lift (egglog-send subproc '(run-schedule (saturate lift)))]
       ['lower (egglog-send subproc '(run-schedule (saturate lower)))]
-      ['unsound (egglog-send subproc '(run-schedule (saturate unsound)))]
       ;; Run the rewrite ruleset interleaved with const-fold until the best iteration
       ['rewrite (egglog-unsound-detected-subprocess step subproc)]))
 
@@ -189,7 +187,6 @@
                        `(constructor do-lift (MTy) M :unextractable)
                        `(ruleset lower)
                        `(ruleset lift)
-                       `(ruleset unsound)
                        `(function bad-merge? () bool :merge (or old new))
                        `(ruleset bad-merge-rule)
                        `(set (bad-merge?) false)
@@ -203,7 +200,6 @@
                  (num-lowering-rules)
                  (num-lifting-rules)
                  (list (approx-lifting-rule))
-                 (egglog-rewrite-rules (*sound-removal-rules*) 'unsound)
                  (list `(ruleset rewrite))
                  (egglog-rewrite-rules (*rules*) 'rewrite)))
 

src/core/patch.rkt

@@ -164,7 +164,7 @@
   (timeline-event! 'rewrite)
 
   ; egg schedule (4-phases for mathematical rewrites, sound-X removal, and implementation selection)
-  (define schedule '(lift rewrite unsound lower))
+  (define schedule '(lift rewrite lower))
 
   (define brfs (map alt-expr altns))
   (define reprs (map (batch-reprs global-batch (*context*)) brfs))

src/core/rules.rkt

@@ -620,7 +620,9 @@
                                                 ,(string->symbol (format "t_~a" (unsound-counter))))]
     [(list op args ...) (cons op (map add-unsound args))]))
 
-(define (*sound-removal-rules*)
-  (list (rule 'remove-sound-/ '(/ a b) '(sound-/ a b 0) '(sound-removal))
-        (rule 'remove-sound-pow '(pow a b) '(sound-pow a b 0) '(sound-removal))
-        (rule 'remove-sound-log '(log a) '(sound-log a 0) '(sound-removal))))
+(define-rules arithmetic
+  [add-sound-/ '(/ a b) '(sound-/ a b 0)]
+  [add-sound-pow '(pow a b) '(sound-pow a b 0)]
+  [add-sound-log '(log a) '(sound-log a 0)]
+  [remove-sound-/ '(sound-/ a 0 b) b]
+  [remove-sound-log '(sound-log 0 b) b])