Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 32 additions & 29 deletions src/core/simplify.rkt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#lang racket

(require pkg/lib)
(require pkg/lib racket/lazy-require)
(require "../common.rkt" "../programs.rkt" "../timeline.rkt" "../errors.rkt"
"../syntax/rules.rkt" "../alternative.rkt")

Expand Down Expand Up @@ -90,100 +90,103 @@

out)

(define-syntax-rule (regraph method)
(dynamic-require 'regraph 'method))
(lazy-require
[regraph (make-regraph rule-phase precompute-phase prune-phase extractor-phase
regraph-count regraph-cost regraph-extract)])

(define/contract (simplify-batch-regraph exprs #:rules rls #:precompute precompute?)
(-> (listof expr?) #:rules (listof rule?) #:precompute boolean? (listof (listof expr?)))
(timeline-push! 'method "regraph")

(define start-time (current-inexact-milliseconds))
(define (log rg iter)
(define cnt ((regraph regraph-count) rg))
(define cost ((regraph regraph-cost) rg))
(define cnt (regraph-count rg))
(define cost (regraph-cost rg))
(debug #:from 'simplify #:depth 2 "iteration " iter ": " cnt " enodes " "(cost " cost ")")
(timeline-push! 'egraph iter cnt cost (- (current-inexact-milliseconds) start-time)))

(define rg ((regraph make-regraph) (map munge exprs) #:limit (*node-limit*)))
(define rg (make-regraph (map munge exprs) #:limit (*node-limit*)))

(define phases
(list ((regraph rule-phase) (map (compose munge rule-input) rls)
(list (rule-phase (map (compose munge rule-input) rls)
(map (compose munge rule-output) rls))
(and precompute? ((regraph precompute-phase) eval-application))
(regraph prune-phase)
(regraph extractor-phase)))
(and precompute? (precompute-phase eval-application))
prune-phase
extractor-phase))

(for/and ([iter (in-naturals 0)])
(log rg iter)
(define initial-cnt ((regraph regraph-count) rg))
(define initial-cnt (regraph-count rg))
;; Iterates the egraph by applying each of the given rules to the egraph
(for ([phase phases] #:when phase) (phase rg))
(and (< initial-cnt ((regraph regraph-count) rg) (*node-limit*))))
(and (< initial-cnt (regraph-count rg) (*node-limit*))))

(log rg "done")
(map list (map unmunge ((regraph regraph-extract) rg))))
(map list (map unmunge (regraph-extract rg))))

(define-syntax-rule (egg method)
(dynamic-require 'egg-herbie 'method))
(lazy-require
[egg-herbie (with-egraph egraph-add-exprs egraph-run
egraph-is-unsound-detected
egraph-get-times-applied egraph-get-simplest egraph-get-cost
egg-expr->expr make-ffi-rules free-ffi-rules
iteration-data-num-nodes iteration-data-time)])

(define/contract (simplify-batch-egg exprs #:rules rls #:precompute precompute?)
(-> (listof expr?) #:rules (listof rule?) #:precompute boolean? (listof (listof expr?)))
(timeline-push! 'method "egg-herbie")
(define irules (rules->irules rls))

((egg with-egraph)
(with-egraph
(lambda (egg-graph)
((egg egraph-add-exprs)
(egraph-add-exprs
egg-graph
exprs
(lambda (node-ids)
(define iter-data (egg-run-rules egg-graph (*node-limit*) irules node-ids (and precompute? true)))

(when ((egg egraph-is-unsound-detected) egg-graph)
(when (egraph-is-unsound-detected egg-graph)
(warn 'unsound-rules #:url "faq.html#unsound-rules"
"Unsound rule application detected in e-graph. Results from simplify may not be sound."))

(for ([rule rls])
(define count ((egg egraph-get-times-applied) egg-graph (rule-name rule)))
(define count (egraph-get-times-applied egg-graph (rule-name rule)))
(when (> count 0)
(timeline-push! 'rules (~a (rule-name rule)) count)))

(map
(lambda (id)
(for/list ([iter (in-range (length iter-data))])
((egg egg-expr->expr)
((egg egraph-get-simplest) egg-graph id iter)
egg-graph)))
(egg-expr->expr (egraph-get-simplest egg-graph id iter) egg-graph)))
node-ids))))))

(define (egg-run-rules egg-graph node-limit irules node-ids precompute?)
(define ffi-rules ((egg make-ffi-rules) irules))
(define ffi-rules (make-ffi-rules irules))
(define start-time (current-inexact-milliseconds))

#;(define (timeline-cost iter)

(define cnt ((egg egraph-get-size) egg-graph))
(define cnt (egraph-get-size egg-graph))

(timeline-push! 'egraph iter cnt cost (- (current-inexact-milliseconds) start-time)))

(define iteration-data ((egg egraph-run) egg-graph node-limit ffi-rules precompute?))
(define iteration-data (egraph-run egg-graph node-limit ffi-rules precompute?))

(let loop
([iter iteration-data] [counter 0] [time 0])
(cond
[(empty? iter)
void]
[else
(define cnt ((egg iteration-data-num-nodes) (first iter)))
(define cnt (iteration-data-num-nodes (first iter)))
(define cost
(apply +
(map (lambda (node-id) ((egg egraph-get-cost) egg-graph node-id counter)) node-ids)))
(map (lambda (node-id) (egraph-get-cost egg-graph node-id counter)) node-ids)))
(debug #:from 'simplify #:depth 2 "iteration " counter ": " cnt " enodes " "(cost " cost ")")
(define new-time (+ time ((egg iteration-data-time) (first iter))))
(define new-time (+ time (iteration-data-time (first iter))))
(timeline-push! 'egraph counter cnt cost new-time)
(loop (rest iter) (+ counter 1) new-time)]))

((egg free-ffi-rules) ffi-rules)
(free-ffi-rules ffi-rules)
iteration-data)

(define (munge expr)
Expand Down
Loading