Skip to content

Commit f26711c

Browse files
authored
Merge pull request #627 from herbie-fp/oflatt-egg0.9.5
update to egg 0.9.5
2 parents 578f711 + f682ae6 commit f26711c

File tree

3 files changed

+19
-13
lines changed

3 files changed

+19
-13
lines changed

egg-herbie/Cargo.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ authors = [ "Oliver Flatt <[email protected]>", "Max Willsey <[email protected]>" ]
55
edition = "2018"
66

77
[dependencies]
8-
# egg = "0.9.4"
9-
egg = { git="https://github.com/egraphs-good/egg", rev="f7e9fd6cb87136d48f5275c8f60d98173ffc170a" }
8+
egg = "0.9.5"
9+
# egg = { git="https://github.com/egraphs-good/egg", rev="f7e9fd6cb87136d48f5275c8f60d98173ffc170a" }
1010

1111
log = "0.4"
1212
indexmap = "1"

src/config.rkt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@
9191
;; The maximum size of an egraph
9292
(define *node-limit* (make-parameter 8000))
9393
(define *proof-max-length* (make-parameter 200))
94+
(define *proof-max-string-length* (make-parameter 10000))
9495

9596
;; In localization, the maximum number of locations returned
9697
(define *localize-expressions-limit* (make-parameter 4))

src/core/egg-herbie.rkt

Lines changed: 16 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -462,17 +462,22 @@
462462
(define res (cast pointer _pointer _string/utf-8))
463463
(destroy_string pointer)
464464
(define env (make-hash))
465-
(define converted
466-
(for/list ([line (in-list (string-split res "\n"))])
467-
(egg-expr->expr line egraph-data)))
468-
(define expanded
469-
(expand-proof
470-
converted
471-
(box (*proof-max-length*))))
472-
473-
(if (member #f expanded)
474-
#f
475-
expanded))
465+
(cond
466+
;; TODO: sometimes the proof is *super* long and it takes us too long just string-split
467+
;; Ideally we would skip the string-splitting
468+
[(< (string-length res) 10000)
469+
(define converted
470+
(for/list ([line (in-list (string-split res "\n"))])
471+
(egg-expr->expr line egraph-data)))
472+
(define expanded
473+
(expand-proof
474+
converted
475+
(box (*proof-max-length*))))
476+
(if (member #f expanded)
477+
#f
478+
expanded)]
479+
[else
480+
#f]))
476481

477482
(struct egg-add-exn exn:fail ())
478483

0 commit comments

Comments
 (0)