Skip to content

Commit

Permalink
aditya-make-egglog-runner clean up code
Browse files Browse the repository at this point in the history
  • Loading branch information
adityaakhileshwaran committed Nov 6, 2024
1 parent 809eaf6 commit b18f8f7
Show file tree
Hide file tree
Showing 5 changed files with 25 additions and 70 deletions.
67 changes: 19 additions & 48 deletions src/core/egglog-herbie.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,6 @@

(process-egglog program-to-egglog))


;; Most calls to egglog should be done through this interface.
;; - `make-egglog-runner`: creates a struct that describes a _reproducible_ egglog instance
;; - `run-egglog`: takes an egglog runner and performs an extraction (exprs or proof)
Expand All @@ -88,7 +87,6 @@
[(define (write-proc alt port mode)
(fprintf port "#<egglog-runner>"))])


;; Constructs an egglog runner. Exactly same as egg-runner
;; But needs some amount of specifics - TODO
;;
Expand Down Expand Up @@ -132,75 +130,48 @@
;; - multi extraction: `(multi . <extractor>)`
;; - proofs: `(proofs . ((<start> . <end>) ...))`
(define (run-egglog runner cmd)
; (printf "egglog\n")
;; Run egg using runner
; (define ctx (egg-runner-ctx runner))

; (define-values (root-ids egg-graph)
; (egraph-run-schedule (egg-runner-batch runner)
; (egg-runner-roots runner)
; (egg-runner-schedule runner)
; ctx))
;; TODO : Need to run egglog to get the actual ids per

; Perform extraction
(match cmd
[`(single . ,extractor) ; single expression extraction
;; TODO : Need to run egglog to get the actual ids per

(define curr-batch (egg-runner-batch runner))
(define curr-batch (egg-runner-batch runner))

;; (Listof (Listof batchref))
(define out
(for/list ([root (batch-roots curr-batch)])
(list (batchref curr-batch root))))
;; (Listof (Listof batchref))
(define out
(for/list ([root (batch-roots curr-batch)])
(list (batchref curr-batch root))))

out]
out]

;; very hard - per id recruse one level and ger simplest child
[`(multi . ,extractor) ; multi expression extraction
;; TODO : Need to run egglog to get the actual ids per
(define curr-batch (egg-runner-batch runner))

(define curr-batch (egg-runner-batch runner))
;; (Listof (Listof batchref))
(define out
(for/list ([root (batch-roots curr-batch)])
(list (batchref curr-batch root))))

;; (Listof (Listof batchref))
; (define out
; (list (list (batchref curr-batch 0))))
(define out
(for/list ([root (batch-roots curr-batch)])
(list (batchref curr-batch root))))

out]
out]

;; egglog does not have proof
;; there is some value that herbie has which indicates we could not
;; find a proof. Might be (list #f #f ....)
;; find a proof. Might be (list #f #f ....)
[`(proofs . ((,start-exprs . ,end-exprs) ...)) ; proof extraction
(for/list ([start (in-list start-exprs)]
[end (in-list end-exprs)])
; (unless (egraph-expr-equal? egg-graph start end ctx)
; (error 'run-egg
; "cannot find proof; start and end are not equal.\n start: ~a \n end: ~a"
; start
; end))
; (define proof (egraph-get-proof egg-graph start end ctx))
; (when (null? proof)
; (error 'run-egg "proof extraction failed between`~a` and `~a`" start end))
; proof)

;; Currently defaults to false, but the above needs to run eventually somehow??
#f)]

#f)]

; 1. ask within egglog program what is id
; 2. Extract expression from each expr
; qn: if i have two expressions how di i know if they are in the same e-class
; TODO: if i have two expressions how di i know if they are in the same e-class
; if we are outside of egglog
[`(equal? . ((,start-exprs . ,end-exprs) ...)) ; term equality?
(for/list ([start (in-list start-exprs)]
(for/list ([start (in-list start-exprs)]
[end (in-list end-exprs)])
; (egraph-expr-equal? egg-graph start end ctx))
#f)]

#f)]

[_ (error 'run-egg "unknown command `~a`\n" cmd)]))

(define (prelude #:mixed-egraph? [mixed-egraph? #t])
Expand Down
16 changes: 5 additions & 11 deletions src/core/patch.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -154,8 +154,6 @@
(timeline-push! 'inputs (map ~a exprs))

(define runner (make-egg-runner global-batch roots reprs schedule #:context (*context*)))

; (printf "patch reached ")

(define generate-flags (hash-ref all-flags 'generate))

Expand All @@ -173,12 +171,9 @@
(for ([batchref* (in-list batchrefs)])
(sow (alt batchref* (list 'rr runner #f #f) (list altn) '()))))))


(timeline-push! 'outputs (map (compose ~a debatchref alt-expr) rewritten))
(timeline-push! 'count (length altns) (length rewritten))

; (printf "patch successful\n\n")

rewritten)

;;;;;;;;;;;;;;;;;;;;;;;;;;;; Public API ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down Expand Up @@ -208,13 +203,12 @@
(if (flag-set? 'generate 'rr)
(run-rr start-altns global-batch)
'()))

; (printf "patch after run-rr \n")

(define return-val (remove-duplicates (append approximations rewritten) #:key (λ (x) (batchref-idx (alt-expr x)))))

(define return-val
(remove-duplicates (append approximations rewritten) #:key (λ (x) (batchref-idx (alt-expr x)))))

; (printf "patch after rem-dev \n")

return-val
)

return-val)
5 changes: 0 additions & 5 deletions src/core/preprocess.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -117,18 +117,13 @@
;; run egg to check for identities
(define expr-pairs (map (curry cons spec) specs))

; (define equal?-lst (run-egg runner `(equal? . ,expr-pairs)))
(define generate-flags (hash-ref all-flags 'generate))

; (printf "preprocess reached ")

(define equal?-lst
(if (member 'egglog generate-flags)
(run-egglog runner `(equal? . ,expr-pairs))
(run-egg runner `(equal? . ,expr-pairs))))

; (printf "preprocess successful\n\n")

;; collect equalities
(define abs-instrs '())
(define negabs-instrs '())
Expand Down
6 changes: 1 addition & 5 deletions src/core/simplify.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@
(timeline-push! 'inputs (map ~a (batch->progs (egg-runner-batch runner) (egg-runner-roots runner))))
(timeline-push! 'method "egg-herbie")


; (printf "simplify reached ")
(define generate-flags (hash-ref all-flags 'generate))
(define simplifieds
(if (member 'egglog generate-flags)
Expand All @@ -38,10 +36,8 @@
[root (egg-runner-roots runner)])
(remove-duplicates (cons (batchref (egg-runner-batch runner) root) simplified)
#:key batchref-idx)))

(timeline-push! 'outputs (map (compose ~a debatchref) (apply append out)))

; (printf "simplify successful\n\n")
(timeline-push! 'outputs (map (compose ~a debatchref) (apply append out)))

out)

Expand Down
1 change: 0 additions & 1 deletion src/core/soundiness.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,6 @@
;; Result is a map from egg query to rewrites.
(define (compute-proofs query->rws)
(for/hash ([(runner rws) (in-hash query->rws)])
; (printf "soundiness reached ")

(define generate-flags (hash-ref all-flags 'generate))
(define proofs
Expand Down

0 comments on commit b18f8f7

Please sign in to comment.