From 028734db01a00414a0396fad97a3ee4139e000ea Mon Sep 17 00:00:00 2001 From: Saul Shanabrook Date: Fri, 5 Jun 2026 03:44:16 -0700 Subject: [PATCH 1/4] Remove constructors from merge encodings --- Cargo.lock | 28 +-- Cargo.toml | 7 +- dag_in_context/Cargo.lock | 20 +- dag_in_context/Cargo.toml | 7 +- dag_in_context/src/interval_analysis.egg | 190 ++++++++++-------- .../conditional_invariant_code_motion.egg | 39 ++-- dag_in_context/src/optimizations/ivt.egg | 40 ++-- .../src/optimizations/mem_simple.egg | 12 +- dag_in_context/src/optimizations/memory.egg | 4 +- dag_in_context/src/optimizations/select.egg | 8 +- .../src/optimizations/switch_rewrites.egg | 8 +- dag_in_context/src/utility/terms.egg | 124 ++++++------ src/util.rs | 11 +- 13 files changed, 260 insertions(+), 238 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 55e99cb4f..e5dd0516e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -789,7 +789,7 @@ dependencies = [ [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "chrono", "clap", @@ -821,7 +821,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "quote", "syn 2.0.114", @@ -830,7 +830,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "ordered-float", ] @@ -838,7 +838,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "anyhow", "dyn-clone", @@ -861,7 +861,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "arc-swap", "bumpalo", @@ -873,7 +873,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "anyhow", "bumpalo", @@ -902,7 +902,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental?rev=08771f9#08771f9f69de51cc8cdc58e3760b7f00a03e40d8" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Fexperimental-body-primitive#0050f279fd8a343d0fe9247846041f62373aea20" dependencies = [ "egglog", "egglog-ast", @@ -915,7 +915,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "rayon", ] @@ -923,7 +923,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "clap", "hashbrown 0.16.1", @@ -937,7 +937,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "crossbeam", "egglog-concurrency", @@ -1035,7 +1035,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -2060,7 +2060,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -2293,7 +2293,7 @@ dependencies = [ "getrandom 0.4.1", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -2605,7 +2605,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 3562080d6..3899fea30 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ name = "files" [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog-experimental", rev = "08771f9", package = "egglog-experimental" } +egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/experimental-body-primitive", package = "egglog-experimental" } egraph-serialize = "0.3.0" log = "0.4.19" thiserror = "1" @@ -63,3 +63,8 @@ write-intermediates = [] # Runs tests relying on LLVM. This may not be available on all systems. llvm = [] default = ["llvm"] + +[patch."https://github.com/saulshanabrook/egg-smol.git"] +egglog = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } +egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } +egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } diff --git a/dag_in_context/Cargo.lock b/dag_in_context/Cargo.lock index d3510e861..1fb5c32d5 100644 --- a/dag_in_context/Cargo.lock +++ b/dag_in_context/Cargo.lock @@ -430,7 +430,7 @@ checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "chrono", "clap", @@ -462,7 +462,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "quote", "syn 2.0.90", @@ -471,7 +471,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "ordered-float", ] @@ -479,7 +479,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "anyhow", "dyn-clone", @@ -502,7 +502,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "arc-swap", "bumpalo", @@ -514,7 +514,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "anyhow", "bumpalo", @@ -543,7 +543,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental?rev=08771f9#08771f9f69de51cc8cdc58e3760b7f00a03e40d8" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Fexperimental-body-primitive#0050f279fd8a343d0fe9247846041f62373aea20" dependencies = [ "egglog", "egglog-ast", @@ -556,7 +556,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "rayon", ] @@ -564,7 +564,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "clap", "hashbrown 0.16.1", @@ -578,7 +578,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/saulshanabrook/egg-smol.git?branch=codex%2Fsplit-scheduler-can-stop-report#ebba7bb902bdc1b0f377b6bb22c06ac305912674" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" dependencies = [ "crossbeam", "egglog-concurrency", diff --git a/dag_in_context/Cargo.toml b/dag_in_context/Cargo.toml index 6f77441e4..c0bfb691a 100644 --- a/dag_in_context/Cargo.toml +++ b/dag_in_context/Cargo.toml @@ -6,7 +6,7 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog-experimental", rev = "08771f9", package = "egglog-experimental" } +egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/experimental-body-primitive", package = "egglog-experimental" } smallvec = "1.11.1" strum = "0.25" strum_macros = "0.25" @@ -33,3 +33,8 @@ clap = { version = "4.4.7", features = ["derive"] } tempfile = "3.10" libc = "0.2" rayon = "1" + +[patch."https://github.com/saulshanabrook/egg-smol.git"] +egglog = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } +egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } +egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } diff --git a/dag_in_context/src/interval_analysis.egg b/dag_in_context/src/interval_analysis.egg index 899d032e6..ccd3a375f 100644 --- a/dag_in_context/src/interval_analysis.egg +++ b/dag_in_context/src/interval_analysis.egg @@ -1,12 +1,53 @@ (ruleset interval-analysis) (ruleset interval-rewrite) -(datatype Bound - (IntB i64) - (BoolB bool) - (Dead) ;; a bound on dead code, so any value can be chosen - (bound-max Bound Bound) - (bound-min Bound Bound)) +(sort CombineInt (UnstableFn (i64 i64) i64)) +(sort CombineBool (UnstableFn (bool bool) bool)) +(sort IntOrBool (Either i64 bool)) +;; A none bound is dead code, so any value can be chosen. +(sort Bound (Maybe IntOrBool)) +(sort I64ToIntOrBool (UnstableFn (i64) IntOrBool)) +(sort BoolToIntOrBool (UnstableFn (bool) IntOrBool)) +(sort IntOrBoolToBound (UnstableFn (IntOrBool) Bound)) + +(primitive IntB (i64) Bound (maybe-some (either-left _0))) +(primitive BoolB (bool) Bound (maybe-some (either-right _0))) +(primitive Dead () Bound (maybe-none)) +(primitive bound-int (Bound) i64 (either-unwrap-left (maybe-unwrap _0))) +(primitive bound-bool (Bound) bool (either-unwrap-right (maybe-unwrap _0))) + +(primitive merge-int-or-bool-left (CombineInt IntOrBool i64) IntOrBool + (either-left (unstable-app _0 _2 (either-unwrap-left _1)))) + +(primitive merge-int-or-bool-right (CombineBool IntOrBool bool) IntOrBool + (either-right (unstable-app _0 _2 (either-unwrap-right _1)))) + +(primitive merge-int-or-bool (CombineInt CombineBool IntOrBool IntOrBool) IntOrBool + (either-match + _2 + (unstable-fn "merge-int-or-bool-left" _0 _3) + (unstable-fn "merge-int-or-bool-right" _1 _3))) + +(primitive bound-merge-somes (CombineInt CombineBool IntOrBool IntOrBool) Bound + (maybe-some (merge-int-or-bool _0 _1 _2 _3))) + +(primitive bound-merge-with-old (CombineInt CombineBool Bound IntOrBool) Bound + (unstable-maybe-match + _2 + (unstable-fn "bound-merge-somes" _0 _1 _3) + (maybe-none))) + +(primitive bound-merge (CombineInt CombineBool Bound Bound) Bound + (unstable-maybe-match + _2 + (unstable-fn "bound-merge-with-old" _0 _1 _3) + (maybe-none))) + +(primitive bound-min (Bound Bound) Bound + (bound-merge (unstable-fn "min") (unstable-fn "and") _0 _1)) + +(primitive bound-max (Bound Bound) Bound + (bound-merge (unstable-fn "max") (unstable-fn "or") _0 _1)) ; bound tables (function lo-bound (Expr) Bound :merge (bound-max old new)) @@ -16,47 +57,21 @@ ; In this case, interval analysis might start going crazy and fail to saturate ; So we immediately set the bounds to (Dead) (rule ( - (= (IntB lo) (lo-bound expr)) - (= (IntB hi) (hi-bound expr)) + (= lo (bound-int (lo-bound expr))) + (= hi (bound-int (hi-bound expr))) (> lo hi) - ) + ) ((set (lo-bound expr) (Dead)) (set (hi-bound expr) (Dead))) :ruleset interval-analysis) (rule ( - (= (BoolB true) (lo-bound expr)) - (= (BoolB false) (hi-bound expr)) - ) + (= true (bound-bool (lo-bound expr))) + (= false (bound-bool (hi-bound expr))) + ) ((set (lo-bound expr) (Dead)) (set (hi-bound expr) (Dead))) :ruleset interval-analysis) -; combinators -(rewrite (bound-max (IntB x) (IntB y)) - (IntB (max x y)) - :ruleset interval-analysis) -(rewrite (bound-min (IntB x) (IntB y)) - (IntB (min x y)) - :ruleset interval-analysis) -(rewrite (bound-max (BoolB x) (BoolB y)) - (BoolB (or x y)) - :ruleset interval-analysis) -(rewrite (bound-min (BoolB x) (BoolB y)) - (BoolB (and x y)) - :ruleset interval-analysis) -(rewrite (bound-max (Dead) anything) - (Dead) - :ruleset interval-analysis) -(rewrite (bound-max anything (Dead)) - (Dead) - :ruleset interval-analysis) -(rewrite (bound-min (Dead) anything) - (Dead) - :ruleset interval-analysis) -(rewrite (bound-min anything (Dead)) - (Dead) - :ruleset interval-analysis) - ; ================================= ; Constants ; ================================= @@ -78,8 +93,8 @@ ; Constant Folding ; ================================= (rule ( - (= (IntB x) (lo-bound expr)) - (= (IntB x) (hi-bound expr)) + (= x (bound-int (lo-bound expr))) + (= x (bound-int (hi-bound expr))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -87,8 +102,8 @@ :ruleset interval-analysis) (rule ( - (= (BoolB x) (lo-bound expr)) - (= (BoolB x) (hi-bound expr)) + (= x (bound-bool (lo-bound expr))) + (= x (bound-bool (hi-bound expr))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -97,7 +112,7 @@ ; lower bound being true means the bool must be true (rule ( - (= (BoolB true) (lo-bound expr)) + (= true (bound-bool (lo-bound expr))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -106,7 +121,7 @@ ; upper bound being false means the bool must be false (rule ( - (= (BoolB false) (hi-bound expr)) + (= false (bound-bool (hi-bound expr))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -119,15 +134,15 @@ ; + a b interval is (+ la lb) (+ ha hb) (rule ( (= lhs (Bop (Add) a b)) - (= (IntB la) (lo-bound a)) - (= (IntB lb) (lo-bound b)) + (= la (bound-int (lo-bound a))) + (= lb (bound-int (lo-bound b))) ) ((set (lo-bound lhs) (IntB (+ la lb)))) :ruleset interval-analysis) (rule ( (= lhs (Bop (Add) a b)) - (= (IntB ha) (hi-bound a)) - (= (IntB hb) (hi-bound b)) + (= ha (bound-int (hi-bound a))) + (= hb (bound-int (hi-bound b))) ) ((set (hi-bound lhs) (IntB (+ ha hb)))) :ruleset interval-analysis) @@ -135,15 +150,15 @@ ; - a b interval is (- la hb) (- ha lb) (rule ( (= lhs (Bop (Sub) a b)) - (= (IntB la) (lo-bound a)) - (= (IntB hb) (hi-bound b)) + (= la (bound-int (lo-bound a))) + (= hb (bound-int (hi-bound b))) ) ((set (lo-bound lhs) (IntB (- la hb)))) :ruleset interval-analysis) (rule ( (= lhs (Bop (Sub) a b)) - (= (IntB ha) (hi-bound a)) - (= (IntB lb) (lo-bound b)) + (= ha (bound-int (hi-bound a))) + (= lb (bound-int (lo-bound b))) ) ((set (hi-bound lhs) (IntB (- ha lb)))) :ruleset interval-analysis) @@ -152,10 +167,10 @@ ; TODO: Make fancier interval analysis (rule ( (= lhs (Bop (Mul) a b)) - (= (IntB x) (lo-bound a)) - (= (IntB x) (hi-bound a)) - (= (IntB y) (lo-bound b)) - (= (IntB y) (hi-bound b)) + (= x (bound-int (lo-bound a))) + (= x (bound-int (hi-bound a))) + (= y (bound-int (lo-bound b))) + (= y (bound-int (hi-bound b))) ) ( (set (lo-bound lhs) (IntB (* x y))) @@ -166,10 +181,10 @@ ; negative * negative is positive (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB hi-x) (hi-bound x)) - (= (IntB hi-y) (hi-bound y)) + (= hi-x (bound-int (hi-bound x))) + (= hi-y (bound-int (hi-bound y))) (< hi-x 0) - (< hi-y 0) + (< hi-y 0) ) ((set (lo-bound lhs) (IntB 1))) :ruleset interval-analysis) @@ -177,8 +192,8 @@ ; negative * positive is negative (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB hi-x) (hi-bound x)) - (= (IntB lo-y) (lo-bound y)) + (= hi-x (bound-int (hi-bound x))) + (= lo-y (bound-int (lo-bound y))) (< hi-x 0) ; x < 0 (x is negative) (> lo-y 0) ; y > 0 (y is positive) ) @@ -188,8 +203,8 @@ ; positive * positive is positive (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB lo-x) (lo-bound x)) - (= (IntB lo-y) (lo-bound y)) + (= lo-x (bound-int (lo-bound x))) + (= lo-y (bound-int (lo-bound y))) (> lo-x 0) (> lo-y 0) ) @@ -199,10 +214,10 @@ ; non-positive * non-positive is non-negative (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB hi-x) (hi-bound x)) - (= (IntB hi-y) (hi-bound y)) + (= hi-x (bound-int (hi-bound x))) + (= hi-y (bound-int (hi-bound y))) (<= hi-x 0) - (<= hi-y 0) + (<= hi-y 0) ) ((set (lo-bound lhs) (IntB 0))) :ruleset interval-analysis) @@ -210,8 +225,8 @@ ; non-positive * non-negative is non-positive (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB hi-x) (hi-bound x)) - (= (IntB lo-y) (lo-bound y)) + (= hi-x (bound-int (hi-bound x))) + (= lo-y (bound-int (lo-bound y))) (<= hi-x 0) ; x <= 0 (x is non-positive) (>= lo-y 0) ; y >= 0 (y is non-negative) ) @@ -221,8 +236,8 @@ ; non-negative * non-negative is non-negative (rule ( (= lhs (Bop (Mul) x y)) - (= (IntB lo-x) (lo-bound x)) - (= (IntB lo-y) (lo-bound y)) + (= lo-x (bound-int (lo-bound x))) + (= lo-y (bound-int (lo-bound y))) (>= lo-x 0) (>= lo-y 0) ) @@ -232,8 +247,8 @@ ; < a b interval is (< ha lb) (< la hb) (rule ( (= lhs (Bop (LessThan) a b)) - (= (IntB ha) (hi-bound a)) - (= (IntB lb) (lo-bound b)) + (= ha (bound-int (hi-bound a))) + (= lb (bound-int (lo-bound b))) ) ( (set (lo-bound lhs) (BoolB (bool-< ha lb))) @@ -241,8 +256,8 @@ :ruleset interval-analysis) (rule ( (= lhs (Bop (LessThan) a b)) - (= (IntB la) (lo-bound a)) - (= (IntB hb) (hi-bound b)) + (= la (bound-int (lo-bound a))) + (= hb (bound-int (hi-bound b))) ) ((set (hi-bound lhs) (BoolB (bool-< la hb)))) :ruleset interval-analysis) @@ -251,7 +266,7 @@ ; abs(x) = x if x >= 0 (rule ( (= lhs (Uop (Abs) x)) - (= (IntB lx) (lo-bound x)) + (= lx (bound-int (lo-bound x))) (>= lx 0) ) ((union lhs x)) @@ -260,7 +275,7 @@ ; abs(x) = -x if x <= 0 (rule ( (= lhs (Uop (Abs) x)) - (= (IntB hx) (hi-bound x)) + (= hx (bound-int (hi-bound x))) (<= hx 0) (HasArgType lhs ty) (ContextOf lhs ctx) @@ -275,7 +290,7 @@ (rule ( (= lhs (If cond inputs thn els)) (ContextOf lhs if_ctx) - (= (BoolB true) (lo-bound cond)) + (= true (bound-bool (lo-bound cond))) ) ((union lhs (Subst if_ctx inputs thn))) :ruleset interval-rewrite) @@ -284,7 +299,7 @@ (rule ( (= lhs (If cond inputs thn els)) (ContextOf lhs if_ctx) - (= (BoolB false) (hi-bound cond)) + (= false (bound-bool (hi-bound cond))) ) ((union lhs (Subst if_ctx inputs els))) :ruleset interval-rewrite) @@ -330,7 +345,7 @@ ; the left operand of the < is an input to the if region (= expr (Get inputs i)) ; the right operand of the < has an upper bound - (= (IntB v) (hi-bound value)) + (= v (bound-int (hi-bound value))) ; context node inside the if region (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) @@ -345,13 +360,13 @@ ; the left operand of the < is an input to the if region (= expr (Get inputs i)) ; the right operand of the < has a lower bound - (= (IntB v) (lo-bound value)) + (= v (bound-int (lo-bound value))) ; context node inside the if region (= ctx (Arg ty (InIf false pred inputs))) (HasType inputs ty) ) ; expr < value was false, so we know expr is at least (lo-bound value) - ((set (lo-bound (Get ctx i)) (IntB v))) + ((set (lo-bound (Get ctx i)) (IntB v))) :ruleset interval-analysis) (rule ( @@ -361,13 +376,13 @@ ; the right operand of the < is an input to the if region (= expr (Get inputs i)) ; the left operand of the < has a lower bound - (= (IntB v) (lo-bound value)) + (= v (bound-int (lo-bound value))) ; context node inside the if region (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) ) ; value < expr was true, so we know expr is at least (lo-bound value) + 1 - ((set (lo-bound (Get ctx i)) (IntB (+ v 1)))) + ((set (lo-bound (Get ctx i)) (IntB (+ v 1)))) :ruleset interval-analysis) (rule ( ; value < expr @@ -376,13 +391,13 @@ ; the right operand of the < is an input to the if region (= expr (Get inputs i)) ; the left operand of the < has an upper bound - (= (IntB v) (hi-bound value)) + (= v (bound-int (hi-bound value))) ; context node inside the if region (= ctx (Arg ty (InIf false pred inputs))) (HasType inputs ty) ) ; value < expr was false, so we know expr is at most (hi-bound value) - ((set (hi-bound (Get ctx i)) (IntB v))) + ((set (hi-bound (Get ctx i)) (IntB v))) :ruleset interval-analysis) ;; Push intervals for inputs into if region @@ -414,7 +429,7 @@ (= expr (Get inputs i)) (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) - (= (IntB lo) (lo-bound val)) + (= lo (bound-int (lo-bound val))) ) ((set (lo-bound (Get ctx i)) (IntB lo))) :ruleset interval-analysis) @@ -425,7 +440,7 @@ (= expr (Get inputs i)) (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) - (= (IntB hi) (hi-bound val)) + (= hi (bound-int (hi-bound val))) ) ((set (hi-bound (Get ctx i)) (IntB hi))) :ruleset interval-analysis) @@ -456,4 +471,3 @@ (set (hi-bound (Get (Arg ty (InLoop inputs outputs)) ith)) bound) ) :ruleset interval-analysis) - diff --git a/dag_in_context/src/optimizations/conditional_invariant_code_motion.egg b/dag_in_context/src/optimizations/conditional_invariant_code_motion.egg index 7892a0895..5196c207a 100644 --- a/dag_in_context/src/optimizations/conditional_invariant_code_motion.egg +++ b/dag_in_context/src/optimizations/conditional_invariant_code_motion.egg @@ -6,7 +6,7 @@ ;; speeds up the InvCodeMotionCandidate relation by removing indirection (relation ExtractedExprCache (Term Expr Assumption)) -(rule ((= (TCPair t1 c1) (ExtractedExpr e1)) +(rule ((= t1 (pair-first (ExtractedExpr e1))) (ContextOf e1 ctx1)) ((ExtractedExprCache t1 e1 ctx1)) :ruleset cicm-index) @@ -28,25 +28,24 @@ (= e1 (Uop o x)) (HasType e1 (Base ty)) - (= (TCPair t1 c1) (ExtractedExpr e1)) + (= t1 (pair-first (ExtractedExpr e1))) (> 10 (Expr-size e1)) (ExprIsPure e1) (ContextOf e1 (InIf true pred orig_ins)) (= e2 (Uop o y)) (HasType e2 (Base ty)) - (= (TCPair t2 c2) (ExtractedExpr e2)) + (= t1 (pair-first (ExtractedExpr e2))) (> 10 (Expr-size e2)) (ExprIsPure e2) (ContextOf e2 (InIf false pred orig_ins)) - (= t1 t2) (= orig_ins_len (TypeList-length tylist)) ) ( ; pull the term out to the outer context - (let new_term (TermSubst outer_ctx orig_ins t1)) - + (let new_term (TermSubst outer_ctx orig_ins t1)) + ; Add it as an input to the new if (let new_ins (Concat orig_ins (Single new_term))) (let new_ins_ty (TupleT (TLConcat tylist (TCons ty (TNil))))) @@ -63,11 +62,11 @@ ; New regions (let new_thn (Subst if_tr st_tr thn)) (let new_els (Subst if_fa st_fa els)) - + ; Union the new arg with the original expr in each branch (union (Get (Arg new_ins_ty if_tr) orig_ins_len) (Subst if_tr st_tr e1)) (union (Get (Arg new_ins_ty if_fa) orig_ins_len) (Subst if_fa st_fa e2)) - + ; Subsume the original exprs now that the new arg is there ; Doing this prevents us from pulling the same exprs out of the new if ; Can only subsume an e-node (not an e-class), and we don't want to @@ -87,7 +86,7 @@ ) :ruleset cicm) - + (rule ( (InvCodeMotionCandidate e1 e2) @@ -99,28 +98,27 @@ (ContextOf e1 (InIf true pred orig_ins)) (ContextOf e2 (InIf false pred orig_ins)) (= e1 (Bop o x1 y1)) - + (= e2 (Bop o x2 y2)) - - (= (TCPair t1 c1) (ExtractedExpr e1)) + + (= t1 (pair-first (ExtractedExpr e1))) (> 10 (Expr-size e1)) (ExprIsPure e1) (HasType e1 (Base ty)) - - + + (HasType e2 (Base ty)) - (= (TCPair t2 c2) (ExtractedExpr e2)) + (= t1 (pair-first (ExtractedExpr e2))) (> 10 (Expr-size e2)) (ExprIsPure e2) - (= t1 t2) (= orig_ins_len (TypeList-length tylist)) ) ( ; pull the term out to the outer context - (let new_term (TermSubst outer_ctx orig_ins t1)) - + (let new_term (TermSubst outer_ctx orig_ins t1)) + ; Add it as an input to the new if (let new_ins (Concat orig_ins (Single new_term))) (let new_ins_ty (TupleT (TLConcat tylist (TCons ty (TNil))))) @@ -137,11 +135,11 @@ ; New regions (let new_thn (Subst if_tr st_tr thn)) (let new_els (Subst if_fa st_fa els)) - + ; Union the new arg with the original expr in each branch (union (Get (Arg new_ins_ty if_tr) orig_ins_len) (Subst if_tr st_tr e1)) (union (Get (Arg new_ins_ty if_fa) orig_ins_len) (Subst if_fa st_fa e2)) - + ; Subsume the original exprs now that the new arg is there ; Doing this prevents us from pulling the same exprs out of the new if ; Can only subsume an e-node (not an e-class), and we don't want to @@ -160,4 +158,3 @@ (union if_e (If pred new_ins new_thn new_els)) ) :ruleset cicm) - diff --git a/dag_in_context/src/optimizations/ivt.egg b/dag_in_context/src/optimizations/ivt.egg index 5e5fbdfd4..270fbee3b 100644 --- a/dag_in_context/src/optimizations/ivt.egg +++ b/dag_in_context/src/optimizations/ivt.egg @@ -2,19 +2,17 @@ (ruleset ivt-analysis) -(sort IVTRes) -;; perm passthrough-perm passthrough-type passthrough-type-len -(constructor IVTAnalysisRes (Expr Expr TypeList i64) IVTRes) -(constructor IVTMin (IVTRes IVTRes) IVTRes) +(sort IVTPayload) +;; perm passthrough-perm passthrough-type +(constructor IVTAnalysisPayload (Expr Expr TypeList) IVTPayload) +(sort IVTRes (Pair IVTPayload i64)) -(rule ((= lhs (IVTMin (IVTAnalysisRes _a _b _c len1) (IVTAnalysisRes _d _e _f len2))) - (<= len1 len2)) - ((union lhs (IVTAnalysisRes _a _b _c len1))) - :ruleset ivt-analysis) -(rule ((= lhs (IVTMin (IVTAnalysisRes _a _b _c len1) (IVTAnalysisRes _d _e _f len2))) - (> len1 len2)) - ((union lhs (IVTAnalysisRes _d _e _f len2))) - :ruleset ivt-analysis) +;; perm passthrough-perm passthrough-type passthrough-type-len +(primitive IVTAnalysisRes (Expr Expr TypeList i64) IVTRes + (pair (IVTAnalysisPayload _0 _1 _2) _3)) + +(primitive IVTMin (IVTRes IVTRes) IVTRes + (unstable-if (unstable-fn "<=" (pair-second _0) (pair-second _1)) _0 _1)) ;; use an analysis to avoid exploring all combinations of passthrough vs not passed through values. Always prefer not passed through @@ -55,7 +53,9 @@ ;; recursive case for accessing the if statement (rule ( - (= (IVTNewInputsAnalysisImpl loop-body curr ifnode) (IVTAnalysisRes perm pperm passthrough-tys len)) + (= ivt-res (IVTNewInputsAnalysisImpl loop-body curr ifnode)) + (= (IVTAnalysisPayload perm pperm passthrough-tys) (pair-first ivt-res)) + (= len (pair-second ivt-res)) (= ifnode (IfNode if-eclass pred inputs then else)) (= curr (Concat (Single (Get if-eclass ith)) rest)) ) ( @@ -66,7 +66,9 @@ ;; recursive case for accessing a passed-through argument (rule ( - (= (IVTNewInputsAnalysisImpl loop-body curr ifnode) (IVTAnalysisRes perm pperm passthrough-tys len)) + (= ivt-res (IVTNewInputsAnalysisImpl loop-body curr ifnode)) + (= (IVTAnalysisPayload perm pperm passthrough-tys) (pair-first ivt-res)) + (= len (pair-second ivt-res)) (= ifnode (IfNode if-eclass pred inputs then else)) (= curr (Concat (Single (Get (Arg ty ctx) ith)) rest)) (= (Get loop-body (+ ith 1)) (Get curr 0)) @@ -84,7 +86,9 @@ ; base case for accessing if statement (rule ( - (= (IVTNewInputsAnalysisImpl loop-body (Single last) ifnode) (IVTAnalysisRes perm pperm passthrough-tys len)) + (= ivt-res (IVTNewInputsAnalysisImpl loop-body (Single last) ifnode)) + (= (IVTAnalysisPayload perm pperm passthrough-tys) (pair-first ivt-res)) + (= len (pair-second ivt-res)) (= ifnode (IfNode if-eclass pred inputs then else)) (= last (Get if-eclass ith)) ) ( @@ -94,7 +98,9 @@ ; base case for accessing a passed-through argument (rule ( - (= (IVTNewInputsAnalysisImpl loop-body curr ifnode) (IVTAnalysisRes perm pperm passthrough-tys len)) + (= ivt-res (IVTNewInputsAnalysisImpl loop-body curr ifnode)) + (= (IVTAnalysisPayload perm pperm passthrough-tys) (pair-first ivt-res)) + (= len (pair-second ivt-res)) (= ifnode (IfNode if-eclass pred inputs then else)) (= curr (Single (Get (Arg ty ctx) ith))) (= (Get loop-body (+ ith 1)) (Get curr 0)) @@ -114,7 +120,7 @@ (rule ( (= loop (DoWhile inpW outW)) - (= (IVTNewInputsAnalysis outW ifnode) (IVTAnalysisRes perm pperm passthrough-tys _len)) + (= (IVTAnalysisPayload perm pperm passthrough-tys) (pair-first (IVTNewInputsAnalysis outW ifnode))) (= ifnode (IfNode if if-cond if-inputs then else)) (= if-inputs-len (tuple-length if-inputs)) (= passthrough-len (TypeList-length passthrough-tys)) diff --git a/dag_in_context/src/optimizations/mem_simple.egg b/dag_in_context/src/optimizations/mem_simple.egg index 9cba1ecf3..6e0664caf 100644 --- a/dag_in_context/src/optimizations/mem_simple.egg +++ b/dag_in_context/src/optimizations/mem_simple.egg @@ -18,41 +18,41 @@ :ruleset mem-simple) (rule ((Bop (PtrAdd) e i) - (= (lo-bound i) (IntB lo)) + (= lo (bound-int (lo-bound i))) (> lo 0)) ((NoAlias e (Bop (PtrAdd) e i))) :ruleset mem-simple) (rule ((Bop (PtrAdd) e i) - (= (hi-bound i) (IntB hi)) + (= hi (bound-int (hi-bound i))) (< hi 0)) ((NoAlias e (Bop (PtrAdd) e i))) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Add) i diff))) - (= (lo-bound diff) (IntB lo)) + (= lo (bound-int (lo-bound diff))) (> lo 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Add) i diff))) - (= (hi-bound diff) (IntB hi)) + (= hi (bound-int (hi-bound diff))) (< hi 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Sub) i diff))) - (= (lo-bound diff) (IntB lo)) + (= lo (bound-int (lo-bound diff))) (> lo 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Sub) i diff))) - (= (hi-bound diff) (IntB hi)) + (= hi (bound-int (hi-bound diff))) (< hi 0)) ((NoAlias p1 p2)) :ruleset mem-simple) diff --git a/dag_in_context/src/optimizations/memory.egg b/dag_in_context/src/optimizations/memory.egg index 43c9d9fff..8b6773a2a 100644 --- a/dag_in_context/src/optimizations/memory.egg +++ b/dag_in_context/src/optimizations/memory.egg @@ -291,8 +291,8 @@ (AddIntIntervalToPtrPointees (MkIntInterval (I lo) (I hi)) (UnwrapPtrPointsTo (PointsToCells x aps)))) - :when ((= (IntB lo) (lo-bound e)) - (= (IntB hi) (hi-bound e))) + :when ((= lo (bound-int (lo-bound e))) + (= hi (bound-int (hi-bound e)))) :ruleset memory-helpers) (rewrite (PointsToCells (If c inputs t e) aps) diff --git a/dag_in_context/src/optimizations/select.egg b/dag_in_context/src/optimizations/select.egg index b43edace0..f26599460 100644 --- a/dag_in_context/src/optimizations/select.egg +++ b/dag_in_context/src/optimizations/select.egg @@ -8,11 +8,11 @@ (ExprIsPure (Get thn i)) (ExprIsPure (Get els i)) - + (> 10 (Expr-size (Get thn i))) ; TODO: Tune these size limits (> 10 (Expr-size (Get els i))) - (= (TCPair t1 c1) (ExtractedExpr (Get thn i))) - (= (TCPair t2 c2) (ExtractedExpr (Get els i))) + (= t1 (pair-first (ExtractedExpr (Get thn i)))) + (= t2 (pair-first (ExtractedExpr (Get els i)))) (ContextOf if_e ctx) ) @@ -21,4 +21,4 @@ (Top (Select) pred (TermSubst ctx inputs t1) (TermSubst ctx inputs t2))) ) :ruleset select_opt -) \ No newline at end of file +) diff --git a/dag_in_context/src/optimizations/switch_rewrites.egg b/dag_in_context/src/optimizations/switch_rewrites.egg index b825aaa88..7a158a726 100644 --- a/dag_in_context/src/optimizations/switch_rewrites.egg +++ b/dag_in_context/src/optimizations/switch_rewrites.egg @@ -73,8 +73,8 @@ (= (Get thn k) (Get (Arg _ty (InIf true pred inputs)) i)) (= els_out (Get els k)) - (= (IntB y) (lo-bound els_out)) - (= (IntB y) (hi-bound els_out)) + (= y (bound-int (lo-bound els_out))) + (= y (bound-int (hi-bound els_out))) ) ( (union (Get if_e k) (Top (Select) pred a (Const (Int y) ty ctx))) @@ -90,8 +90,8 @@ (HasArgType if_e ty) (= thn_out (Get thn k)) - (= (IntB y) (lo-bound thn_out)) - (= (IntB y) (hi-bound thn_out)) + (= y (bound-int (lo-bound thn_out))) + (= y (bound-int (hi-bound thn_out))) ; input to the if (= b (Get inputs i)) diff --git a/dag_in_context/src/utility/terms.egg b/dag_in_context/src/utility/terms.egg index 1cc241c4b..2f5afe083 100644 --- a/dag_in_context/src/utility/terms.egg +++ b/dag_in_context/src/utility/terms.egg @@ -1,11 +1,15 @@ (ruleset terms) ;; helpers keeps track of the new best extracted terms (ruleset terms-helpers) -;; helpers-helpers runs `Smaller` rules, resolving the merge function for helpers +;; Kept as a nested helper ruleset in the existing schedule shape. (ruleset terms-helpers-helpers) -(sort TermAndCost) -(constructor Smaller (TermAndCost TermAndCost) TermAndCost) +(sort TermAndCost (Pair Term i64)) +(sort UnitThunk (UnstableFn () Unit)) + +;; Returns the smaller of the two, keeping the old value on ties. +(primitive Smaller (TermAndCost TermAndCost) TermAndCost + (unstable-if (unstable-fn "<=" (pair-second _0) (pair-second _1)) _0 _1)) (function ExtractedExpr (Expr) TermAndCost :merge (Smaller old new)) @@ -13,92 +17,78 @@ ;; this preserves egglog's timestamp of when the last time ExtractedExpr was changed, fixing a big performance problem (relation PotentialExtractedExpr (Expr TermAndCost)) -(constructor TCPair (Term i64) TermAndCost) - (constructor NoTerm () Term) ;; set extracted expr to default value (rule ((PotentialExtractedExpr expr termandcost)) - ((set (ExtractedExpr expr) (TCPair (NoTerm) 10000000000000000))) + ((set (ExtractedExpr expr) (pair (NoTerm) 10000000000000000))) :ruleset terms-helpers) ;; set extracted expr to new value as long as not equal -(rule ((PotentialExtractedExpr expr (TCPair term cost)) - (= (ExtractedExpr expr) (TCPair oldterm oldcost)) - (< cost oldcost)) - ((set (ExtractedExpr expr) (TCPair term cost))) +(rule ((PotentialExtractedExpr expr termandcost) + (< (pair-second termandcost) (pair-second (ExtractedExpr expr)))) + ((set (ExtractedExpr expr) termandcost)) :ruleset terms-helpers) ;; if the cost is negative panic, terms got too big -(rule ((PotentialExtractedExpr expr (TCPair term cost)) - (< cost 0)) +(rule ((PotentialExtractedExpr expr termandcost) + (< (pair-second termandcost) 0)) ((panic "Negative cost")) :ruleset terms-helpers) -;; Resolve Smaller -(rule ( - (= lhs (Smaller (TCPair t1 cost1) (TCPair t2 cost2))) - (< cost1 cost2) - ) - ((union lhs (TCPair t1 cost1))) - :ruleset terms-helpers-helpers) - -(rule ( - (= lhs (Smaller (TCPair t1 cost1) (TCPair t2 cost2))) - (> cost1 cost2) - ) - ((union lhs (TCPair t2 cost2))) - :ruleset terms-helpers-helpers) - - -(rule ( - (= lhs (Smaller (TCPair t1 cost1) (TCPair t2 cost2))) - (= cost1 cost2) - ) - ;; arbitrarily pick first one - ((union lhs (TCPair t1 cost1))) - :ruleset terms-helpers-helpers) - - ; Compute smallest Expr bottom-up (rule ((= lhs (Const c ty ass))) - ((PotentialExtractedExpr lhs (TCPair (TermConst c) 1))) + ((PotentialExtractedExpr lhs (pair (TermConst c) 1))) :ruleset terms) (rule ((= lhs (Arg ty ass))) - ((PotentialExtractedExpr lhs (TCPair (TermArg) 1))) + ((PotentialExtractedExpr lhs (pair (TermArg) 1))) :ruleset terms) (rule ( (= lhs (Bop o e1 e2)) - (= (TCPair t1 c1) (ExtractedExpr e1)) - (= (TCPair t2 c2) (ExtractedExpr e2)) + (= tc1 (ExtractedExpr e1)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) + (= tc2 (ExtractedExpr e2)) + (= t2 (pair-first tc2)) + (= c2 (pair-second tc2)) ) - ((PotentialExtractedExpr lhs (TCPair (TermBop o t1 t2) (+ 1 (+ c1 c2))))) + ((PotentialExtractedExpr lhs (pair (TermBop o t1 t2) (+ 1 (+ c1 c2))))) :ruleset terms) (rule ( (= lhs (Top o e1 e2 e3)) - (= (TCPair t1 c1) (ExtractedExpr e1)) - (= (TCPair t2 c2) (ExtractedExpr e2)) - (= (TCPair t3 c3) (ExtractedExpr e3)) + (= tc1 (ExtractedExpr e1)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) + (= tc2 (ExtractedExpr e2)) + (= t2 (pair-first tc2)) + (= c2 (pair-second tc2)) + (= tc3 (ExtractedExpr e3)) + (= t3 (pair-first tc3)) + (= c3 (pair-second tc3)) ) - ((PotentialExtractedExpr lhs (TCPair (TermTop o t1 t2 t3) (+ (+ 1 c1) (+ c2 c3))))) + ((PotentialExtractedExpr lhs (pair (TermTop o t1 t2 t3) (+ (+ 1 c1) (+ c2 c3))))) :ruleset terms) (rule ( (= lhs (Uop o e1)) - (= (TCPair t1 c1) (ExtractedExpr e1)) + (= tc1 (ExtractedExpr e1)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) ) - ((PotentialExtractedExpr lhs (TCPair (TermUop o t1) (+ 1 c1)))) + ((PotentialExtractedExpr lhs (pair (TermUop o t1) (+ 1 c1)))) :ruleset terms) (rule ( (= lhs (Get tup i)) - (= (TCPair t1 c1) (ExtractedExpr tup)) + (= tc1 (ExtractedExpr tup)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) ) ; cost of the get is the same as the cost of the whole tuple - ((PotentialExtractedExpr lhs (TCPair (TermGet t1 i) c1))) + ((PotentialExtractedExpr lhs (pair (TermGet t1 i) c1))) :ruleset terms) ; todo Alloc @@ -107,32 +97,46 @@ (rule ( (= lhs (Single e1)) - (= (TCPair t1 c1) (ExtractedExpr e1)) + (= tc1 (ExtractedExpr e1)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) ) ; cost of single is same as cost of the element - ((PotentialExtractedExpr lhs (TCPair (TermSingle t1) c1))) + ((PotentialExtractedExpr lhs (pair (TermSingle t1) c1))) :ruleset terms) (rule ( (= lhs (Concat e1 e2)) - (= (TCPair t1 c1) (ExtractedExpr e1)) - (= (TCPair t2 c2) (ExtractedExpr e2)) + (= tc1 (ExtractedExpr e1)) + (= t1 (pair-first tc1)) + (= c1 (pair-second tc1)) + (= tc2 (ExtractedExpr e2)) + (= t2 (pair-first tc2)) + (= c2 (pair-second tc2)) ) ; cost of concat is sum of the costs - ((PotentialExtractedExpr lhs (TCPair (TermConcat t1 t2) (+ c1 c2)))) + ((PotentialExtractedExpr lhs (pair (TermConcat t1 t2) (+ c1 c2)))) :ruleset terms) ; todo Control flow - not sure if needed ; (rule ( ; (= lhs (If pred inputs thn els)) -; (= (TCPair t1 c1) (ExtractedExpr pred)) -; (= (TCPair t2 c2) (ExtractedExpr inputs)) -; (= (TCPair t3 c3) (ExtractedExpr thn)) -; (= (TCPair t4 c4) (ExtractedExpr els)) +; (= tc1 (ExtractedExpr pred)) +; (= t1 (pair-first tc1)) +; (= c1 (pair-second tc1)) +; (= tc2 (ExtractedExpr inputs)) +; (= t2 (pair-first tc2)) +; (= c2 (pair-second tc2)) +; (= tc3 (ExtractedExpr thn)) +; (= t3 (pair-first tc3)) +; (= c3 (pair-second tc3)) +; (= tc4 (ExtractedExpr els)) +; (= t4 (pair-first tc4)) +; (= c4 (pair-second tc4)) ; ) ; ; cost of if is 10 + cost of pred + cost of input + max of branch costs -; ((PotentialExtractedExpr lhs (TCPair (TermIf t1 t2 t3 t4) (+ 10 (+ (+ c1 c2) (max c3 c4)))))) +; ((PotentialExtractedExpr lhs (pair (TermIf t1 t2 t3 t4) (+ 10 (+ (+ c1 c2) (max c3 c4)))))) ; :ruleset terms) (sort Node) diff --git a/src/util.rs b/src/util.rs index 359802f5a..56ca79ff8 100644 --- a/src/util.rs +++ b/src/util.rs @@ -865,18 +865,9 @@ impl Run { eggcc_config.use_context, eggcc_config.disable_hacker_rules, ); - let mut egraph = egglog::new_experimental_egraph(); - let resolved = egraph - .resolve_program(None, &egglog) - .map_err(EggCCError::EggLog)?; - let desugared_egglog = egglog::ast::sanitize_internal_names(&resolved) - .iter() - .map(|cmd| cmd.to_string()) - .collect::>() - .join("\n"); ( vec![Visualization { - result: desugared_egglog, + result: egglog, file_extension: ".egg".to_string(), name: "".to_string(), }], From 261d953ec10761c8f8708d489b0497dd113a64c0 Mon Sep 17 00:00:00 2001 From: Saul Shanabrook Date: Mon, 29 Jun 2026 10:16:47 -0400 Subject: [PATCH 2/4] Use generic container merge helpers --- Cargo.lock | 20 +- Cargo.toml | 7 +- dag_in_context/Cargo.lock | 20 +- dag_in_context/Cargo.toml | 7 +- dag_in_context/src/interval_analysis.egg | 210 +++++++----------- dag_in_context/src/interval_analysis.rs | 24 +- dag_in_context/src/optimizations/ivt.egg | 22 +- .../src/optimizations/mem_simple.egg | 12 +- dag_in_context/src/optimizations/memory.egg | 8 +- dag_in_context/src/optimizations/memory.rs | 2 +- .../src/optimizations/switch_rewrites.egg | 10 +- dag_in_context/src/type_analysis.egg | 2 +- dag_in_context/src/utility/terms.egg | 7 +- dag_in_context/src/utility/util.egg | 4 +- 14 files changed, 144 insertions(+), 211 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e5dd0516e..106f3adba 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -789,7 +789,7 @@ dependencies = [ [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "chrono", "clap", @@ -821,7 +821,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "quote", "syn 2.0.114", @@ -830,7 +830,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "ordered-float", ] @@ -838,7 +838,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "anyhow", "dyn-clone", @@ -861,7 +861,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "arc-swap", "bumpalo", @@ -873,7 +873,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "anyhow", "bumpalo", @@ -902,7 +902,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Fexperimental-body-primitive#0050f279fd8a343d0fe9247846041f62373aea20" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#6b37b6b31cf878fd7384e470b216398d9cc006fe" dependencies = [ "egglog", "egglog-ast", @@ -915,7 +915,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "rayon", ] @@ -923,7 +923,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "clap", "hashbrown 0.16.1", @@ -937,7 +937,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "crossbeam", "egglog-concurrency", diff --git a/Cargo.toml b/Cargo.toml index 3899fea30..f28f6f870 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ name = "files" [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/experimental-body-primitive", package = "egglog-experimental" } +egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/eggcc-proof-baseline-pr927", package = "egglog-experimental" } egraph-serialize = "0.3.0" log = "0.4.19" thiserror = "1" @@ -63,8 +63,3 @@ write-intermediates = [] # Runs tests relying on LLVM. This may not be available on all systems. llvm = [] default = ["llvm"] - -[patch."https://github.com/saulshanabrook/egg-smol.git"] -egglog = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } -egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } -egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } diff --git a/dag_in_context/Cargo.lock b/dag_in_context/Cargo.lock index 1fb5c32d5..69684741c 100644 --- a/dag_in_context/Cargo.lock +++ b/dag_in_context/Cargo.lock @@ -430,7 +430,7 @@ checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "chrono", "clap", @@ -462,7 +462,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "quote", "syn 2.0.90", @@ -471,7 +471,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "ordered-float", ] @@ -479,7 +479,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "anyhow", "dyn-clone", @@ -502,7 +502,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "arc-swap", "bumpalo", @@ -514,7 +514,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "anyhow", "bumpalo", @@ -543,7 +543,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Fexperimental-body-primitive#0050f279fd8a343d0fe9247846041f62373aea20" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#6b37b6b31cf878fd7384e470b216398d9cc006fe" dependencies = [ "egglog", "egglog-ast", @@ -556,7 +556,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "rayon", ] @@ -564,7 +564,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "clap", "hashbrown 0.16.1", @@ -578,7 +578,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Feager-merge-containers#a27e60833f09374ada9cb9c7fad41d47747f75ad" +source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" dependencies = [ "crossbeam", "egglog-concurrency", diff --git a/dag_in_context/Cargo.toml b/dag_in_context/Cargo.toml index c0bfb691a..3da2e40f0 100644 --- a/dag_in_context/Cargo.toml +++ b/dag_in_context/Cargo.toml @@ -6,7 +6,7 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/experimental-body-primitive", package = "egglog-experimental" } +egglog = { git = "https://github.com/egraphs-good/egglog-experimental.git", branch = "codex/eggcc-proof-baseline-pr927", package = "egglog-experimental" } smallvec = "1.11.1" strum = "0.25" strum_macros = "0.25" @@ -33,8 +33,3 @@ clap = { version = "4.4.7", features = ["derive"] } tempfile = "3.10" libc = "0.2" rayon = "1" - -[patch."https://github.com/saulshanabrook/egg-smol.git"] -egglog = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } -egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } -egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", branch = "codex/eager-merge-containers" } diff --git a/dag_in_context/src/interval_analysis.egg b/dag_in_context/src/interval_analysis.egg index ccd3a375f..d382fff30 100644 --- a/dag_in_context/src/interval_analysis.egg +++ b/dag_in_context/src/interval_analysis.egg @@ -1,75 +1,31 @@ (ruleset interval-analysis) (ruleset interval-rewrite) -(sort CombineInt (UnstableFn (i64 i64) i64)) -(sort CombineBool (UnstableFn (bool bool) bool)) (sort IntOrBool (Either i64 bool)) ;; A none bound is dead code, so any value can be chosen. (sort Bound (Maybe IntOrBool)) -(sort I64ToIntOrBool (UnstableFn (i64) IntOrBool)) -(sort BoolToIntOrBool (UnstableFn (bool) IntOrBool)) -(sort IntOrBoolToBound (UnstableFn (IntOrBool) Bound)) - -(primitive IntB (i64) Bound (maybe-some (either-left _0))) -(primitive BoolB (bool) Bound (maybe-some (either-right _0))) -(primitive Dead () Bound (maybe-none)) -(primitive bound-int (Bound) i64 (either-unwrap-left (maybe-unwrap _0))) -(primitive bound-bool (Bound) bool (either-unwrap-right (maybe-unwrap _0))) - -(primitive merge-int-or-bool-left (CombineInt IntOrBool i64) IntOrBool - (either-left (unstable-app _0 _2 (either-unwrap-left _1)))) - -(primitive merge-int-or-bool-right (CombineBool IntOrBool bool) IntOrBool - (either-right (unstable-app _0 _2 (either-unwrap-right _1)))) - -(primitive merge-int-or-bool (CombineInt CombineBool IntOrBool IntOrBool) IntOrBool - (either-match - _2 - (unstable-fn "merge-int-or-bool-left" _0 _3) - (unstable-fn "merge-int-or-bool-right" _1 _3))) - -(primitive bound-merge-somes (CombineInt CombineBool IntOrBool IntOrBool) Bound - (maybe-some (merge-int-or-bool _0 _1 _2 _3))) - -(primitive bound-merge-with-old (CombineInt CombineBool Bound IntOrBool) Bound - (unstable-maybe-match - _2 - (unstable-fn "bound-merge-somes" _0 _1 _3) - (maybe-none))) - -(primitive bound-merge (CombineInt CombineBool Bound Bound) Bound - (unstable-maybe-match - _2 - (unstable-fn "bound-merge-with-old" _0 _1 _3) - (maybe-none))) - -(primitive bound-min (Bound Bound) Bound - (bound-merge (unstable-fn "min") (unstable-fn "and") _0 _1)) - -(primitive bound-max (Bound Bound) Bound - (bound-merge (unstable-fn "max") (unstable-fn "or") _0 _1)) ; bound tables -(function lo-bound (Expr) Bound :merge (bound-max old new)) -(function hi-bound (Expr) Bound :merge (bound-min old new)) +(function lo-bound (Expr) Bound :merge (maybe-either-i64-bool-max old new)) +(function hi-bound (Expr) Bound :merge (maybe-either-i64-bool-min old new)) ; if lo > hi, we have proven that this code is dead (as long as all our rules are sound) ; In this case, interval analysis might start going crazy and fail to saturate -; So we immediately set the bounds to (Dead) +; So we immediately set the bounds to maybe-none. (rule ( - (= lo (bound-int (lo-bound expr))) - (= hi (bound-int (hi-bound expr))) + (= lo (either-unwrap-left (maybe-unwrap (lo-bound expr)))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound expr)))) (> lo hi) ) - ((set (lo-bound expr) (Dead)) - (set (hi-bound expr) (Dead))) + ((set (lo-bound expr) (maybe-none)) + (set (hi-bound expr) (maybe-none))) :ruleset interval-analysis) (rule ( - (= true (bound-bool (lo-bound expr))) - (= false (bound-bool (hi-bound expr))) + (= true (either-unwrap-right (maybe-unwrap (lo-bound expr)))) + (= false (either-unwrap-right (maybe-unwrap (hi-bound expr)))) ) - ((set (lo-bound expr) (Dead)) - (set (hi-bound expr) (Dead))) + ((set (lo-bound expr) (maybe-none)) + (set (hi-bound expr) (maybe-none))) :ruleset interval-analysis) ; ================================= @@ -77,15 +33,15 @@ ; ================================= (rule ((= lhs (Const (Int x) ty ctx))) ( - (set (lo-bound lhs) (IntB x)) - (set (hi-bound lhs) (IntB x)) + (set (lo-bound lhs) (maybe-some (either-left x))) + (set (hi-bound lhs) (maybe-some (either-left x))) ) :ruleset interval-analysis) (rule ((= lhs (Const (Bool x) ty ctx))) ( - (set (lo-bound lhs) (BoolB x)) - (set (hi-bound lhs) (BoolB x)) + (set (lo-bound lhs) (maybe-some (either-right x))) + (set (hi-bound lhs) (maybe-some (either-right x))) ) :ruleset interval-analysis) @@ -93,8 +49,8 @@ ; Constant Folding ; ================================= (rule ( - (= x (bound-int (lo-bound expr))) - (= x (bound-int (hi-bound expr))) + (= x (either-unwrap-left (maybe-unwrap (lo-bound expr)))) + (= x (either-unwrap-left (maybe-unwrap (hi-bound expr)))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -102,8 +58,8 @@ :ruleset interval-analysis) (rule ( - (= x (bound-bool (lo-bound expr))) - (= x (bound-bool (hi-bound expr))) + (= x (either-unwrap-right (maybe-unwrap (lo-bound expr)))) + (= x (either-unwrap-right (maybe-unwrap (hi-bound expr)))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -112,7 +68,7 @@ ; lower bound being true means the bool must be true (rule ( - (= true (bound-bool (lo-bound expr))) + (= true (either-unwrap-right (maybe-unwrap (lo-bound expr)))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -121,7 +77,7 @@ ; upper bound being false means the bool must be false (rule ( - (= false (bound-bool (hi-bound expr))) + (= false (either-unwrap-right (maybe-unwrap (hi-bound expr)))) (HasArgType expr ty) (ContextOf expr ctx) ) @@ -134,139 +90,139 @@ ; + a b interval is (+ la lb) (+ ha hb) (rule ( (= lhs (Bop (Add) a b)) - (= la (bound-int (lo-bound a))) - (= lb (bound-int (lo-bound b))) + (= la (either-unwrap-left (maybe-unwrap (lo-bound a)))) + (= lb (either-unwrap-left (maybe-unwrap (lo-bound b)))) ) - ((set (lo-bound lhs) (IntB (+ la lb)))) + ((set (lo-bound lhs) (maybe-some (either-left (+ la lb))))) :ruleset interval-analysis) (rule ( (= lhs (Bop (Add) a b)) - (= ha (bound-int (hi-bound a))) - (= hb (bound-int (hi-bound b))) + (= ha (either-unwrap-left (maybe-unwrap (hi-bound a)))) + (= hb (either-unwrap-left (maybe-unwrap (hi-bound b)))) ) - ((set (hi-bound lhs) (IntB (+ ha hb)))) + ((set (hi-bound lhs) (maybe-some (either-left (+ ha hb))))) :ruleset interval-analysis) ; - a b interval is (- la hb) (- ha lb) (rule ( (= lhs (Bop (Sub) a b)) - (= la (bound-int (lo-bound a))) - (= hb (bound-int (hi-bound b))) + (= la (either-unwrap-left (maybe-unwrap (lo-bound a)))) + (= hb (either-unwrap-left (maybe-unwrap (hi-bound b)))) ) - ((set (lo-bound lhs) (IntB (- la hb)))) + ((set (lo-bound lhs) (maybe-some (either-left (- la hb))))) :ruleset interval-analysis) (rule ( (= lhs (Bop (Sub) a b)) - (= ha (bound-int (hi-bound a))) - (= lb (bound-int (lo-bound b))) + (= ha (either-unwrap-left (maybe-unwrap (hi-bound a)))) + (= lb (either-unwrap-left (maybe-unwrap (lo-bound b)))) ) - ((set (hi-bound lhs) (IntB (- ha lb)))) + ((set (hi-bound lhs) (maybe-some (either-left (- ha lb))))) :ruleset interval-analysis) ; Multiplication for two constants ; TODO: Make fancier interval analysis (rule ( (= lhs (Bop (Mul) a b)) - (= x (bound-int (lo-bound a))) - (= x (bound-int (hi-bound a))) - (= y (bound-int (lo-bound b))) - (= y (bound-int (hi-bound b))) + (= x (either-unwrap-left (maybe-unwrap (lo-bound a)))) + (= x (either-unwrap-left (maybe-unwrap (hi-bound a)))) + (= y (either-unwrap-left (maybe-unwrap (lo-bound b)))) + (= y (either-unwrap-left (maybe-unwrap (hi-bound b)))) ) ( - (set (lo-bound lhs) (IntB (* x y))) - (set (hi-bound lhs) (IntB (* x y))) + (set (lo-bound lhs) (maybe-some (either-left (* x y)))) + (set (hi-bound lhs) (maybe-some (either-left (* x y)))) ) :ruleset interval-analysis) ; negative * negative is positive (rule ( (= lhs (Bop (Mul) x y)) - (= hi-x (bound-int (hi-bound x))) - (= hi-y (bound-int (hi-bound y))) + (= hi-x (either-unwrap-left (maybe-unwrap (hi-bound x)))) + (= hi-y (either-unwrap-left (maybe-unwrap (hi-bound y)))) (< hi-x 0) (< hi-y 0) ) - ((set (lo-bound lhs) (IntB 1))) + ((set (lo-bound lhs) (maybe-some (either-left 1)))) :ruleset interval-analysis) ; negative * positive is negative (rule ( (= lhs (Bop (Mul) x y)) - (= hi-x (bound-int (hi-bound x))) - (= lo-y (bound-int (lo-bound y))) + (= hi-x (either-unwrap-left (maybe-unwrap (hi-bound x)))) + (= lo-y (either-unwrap-left (maybe-unwrap (lo-bound y)))) (< hi-x 0) ; x < 0 (x is negative) (> lo-y 0) ; y > 0 (y is positive) ) - ((set (hi-bound lhs) (IntB -1))) + ((set (hi-bound lhs) (maybe-some (either-left -1)))) :ruleset interval-analysis) ; positive * positive is positive (rule ( (= lhs (Bop (Mul) x y)) - (= lo-x (bound-int (lo-bound x))) - (= lo-y (bound-int (lo-bound y))) + (= lo-x (either-unwrap-left (maybe-unwrap (lo-bound x)))) + (= lo-y (either-unwrap-left (maybe-unwrap (lo-bound y)))) (> lo-x 0) (> lo-y 0) ) - ((set (lo-bound lhs) (IntB 1))) + ((set (lo-bound lhs) (maybe-some (either-left 1)))) :ruleset interval-analysis) ; non-positive * non-positive is non-negative (rule ( (= lhs (Bop (Mul) x y)) - (= hi-x (bound-int (hi-bound x))) - (= hi-y (bound-int (hi-bound y))) + (= hi-x (either-unwrap-left (maybe-unwrap (hi-bound x)))) + (= hi-y (either-unwrap-left (maybe-unwrap (hi-bound y)))) (<= hi-x 0) (<= hi-y 0) ) - ((set (lo-bound lhs) (IntB 0))) + ((set (lo-bound lhs) (maybe-some (either-left 0)))) :ruleset interval-analysis) ; non-positive * non-negative is non-positive (rule ( (= lhs (Bop (Mul) x y)) - (= hi-x (bound-int (hi-bound x))) - (= lo-y (bound-int (lo-bound y))) + (= hi-x (either-unwrap-left (maybe-unwrap (hi-bound x)))) + (= lo-y (either-unwrap-left (maybe-unwrap (lo-bound y)))) (<= hi-x 0) ; x <= 0 (x is non-positive) (>= lo-y 0) ; y >= 0 (y is non-negative) ) - ((set (hi-bound lhs) (IntB 0))) + ((set (hi-bound lhs) (maybe-some (either-left 0)))) :ruleset interval-analysis) ; non-negative * non-negative is non-negative (rule ( (= lhs (Bop (Mul) x y)) - (= lo-x (bound-int (lo-bound x))) - (= lo-y (bound-int (lo-bound y))) + (= lo-x (either-unwrap-left (maybe-unwrap (lo-bound x)))) + (= lo-y (either-unwrap-left (maybe-unwrap (lo-bound y)))) (>= lo-x 0) (>= lo-y 0) ) - ((set (lo-bound lhs) (IntB 0))) + ((set (lo-bound lhs) (maybe-some (either-left 0)))) :ruleset interval-analysis) ; < a b interval is (< ha lb) (< la hb) (rule ( (= lhs (Bop (LessThan) a b)) - (= ha (bound-int (hi-bound a))) - (= lb (bound-int (lo-bound b))) + (= ha (either-unwrap-left (maybe-unwrap (hi-bound a)))) + (= lb (either-unwrap-left (maybe-unwrap (lo-bound b)))) ) ( - (set (lo-bound lhs) (BoolB (bool-< ha lb))) + (set (lo-bound lhs) (maybe-some (either-right (bool-< ha lb)))) ) :ruleset interval-analysis) (rule ( (= lhs (Bop (LessThan) a b)) - (= la (bound-int (lo-bound a))) - (= hb (bound-int (hi-bound b))) + (= la (either-unwrap-left (maybe-unwrap (lo-bound a)))) + (= hb (either-unwrap-left (maybe-unwrap (hi-bound b)))) ) - ((set (hi-bound lhs) (BoolB (bool-< la hb)))) + ((set (hi-bound lhs) (maybe-some (either-right (bool-< la hb))))) :ruleset interval-analysis) ; Abs ; abs(x) = x if x >= 0 (rule ( (= lhs (Uop (Abs) x)) - (= lx (bound-int (lo-bound x))) + (= lx (either-unwrap-left (maybe-unwrap (lo-bound x)))) (>= lx 0) ) ((union lhs x)) @@ -275,7 +231,7 @@ ; abs(x) = -x if x <= 0 (rule ( (= lhs (Uop (Abs) x)) - (= hx (bound-int (hi-bound x))) + (= hx (either-unwrap-left (maybe-unwrap (hi-bound x)))) (<= hx 0) (HasArgType lhs ty) (ContextOf lhs ctx) @@ -290,7 +246,7 @@ (rule ( (= lhs (If cond inputs thn els)) (ContextOf lhs if_ctx) - (= true (bound-bool (lo-bound cond))) + (= true (either-unwrap-right (maybe-unwrap (lo-bound cond)))) ) ((union lhs (Subst if_ctx inputs thn))) :ruleset interval-rewrite) @@ -299,7 +255,7 @@ (rule ( (= lhs (If cond inputs thn els)) (ContextOf lhs if_ctx) - (= false (bound-bool (hi-bound cond))) + (= false (either-unwrap-right (maybe-unwrap (hi-bound cond)))) ) ((union lhs (Subst if_ctx inputs els))) :ruleset interval-rewrite) @@ -311,14 +267,14 @@ (= lo-thn (lo-bound thn)) (= lo-els (lo-bound els)) ) - ((set (lo-bound lhs) (bound-min lo-thn lo-els))) + ((set (lo-bound lhs) (maybe-either-i64-bool-min lo-thn lo-els))) :ruleset interval-analysis) (rule ( (= lhs (If cond inputs thn els)) (= hi-thn (hi-bound thn)) (= hi-els (hi-bound els)) ) - ((set (hi-bound lhs) (bound-max hi-thn hi-els))) + ((set (hi-bound lhs) (maybe-either-i64-bool-max hi-thn hi-els))) :ruleset interval-analysis) ; Same rules, but for Ifs that have multiple outputs @@ -327,14 +283,14 @@ (= lo-thn (lo-bound (Get thn i))) (= lo-els (lo-bound (Get els i))) ) - ((set (lo-bound (Get lhs i)) (bound-min lo-thn lo-els))) + ((set (lo-bound (Get lhs i)) (maybe-either-i64-bool-min lo-thn lo-els))) :ruleset interval-analysis) (rule ( (= lhs (If cond inputs thn els)) (= hi-thn (hi-bound (Get thn i))) (= hi-els (hi-bound (Get els i))) ) - ((set (hi-bound (Get lhs i)) (bound-max hi-thn hi-els))) + ((set (hi-bound (Get lhs i)) (maybe-either-i64-bool-max hi-thn hi-els))) :ruleset interval-analysis) ; If the If takes a tuple @@ -345,13 +301,13 @@ ; the left operand of the < is an input to the if region (= expr (Get inputs i)) ; the right operand of the < has an upper bound - (= v (bound-int (hi-bound value))) + (= v (either-unwrap-left (maybe-unwrap (hi-bound value)))) ; context node inside the if region (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) ) ; expr < value was true, so we know expr is at most (hi-bound value) - 1 - ((set (hi-bound (Get ctx i)) (IntB (- v 1)))) + ((set (hi-bound (Get ctx i)) (maybe-some (either-left (- v 1))))) :ruleset interval-analysis) (rule ( ; expr < value @@ -360,13 +316,13 @@ ; the left operand of the < is an input to the if region (= expr (Get inputs i)) ; the right operand of the < has a lower bound - (= v (bound-int (lo-bound value))) + (= v (either-unwrap-left (maybe-unwrap (lo-bound value)))) ; context node inside the if region (= ctx (Arg ty (InIf false pred inputs))) (HasType inputs ty) ) ; expr < value was false, so we know expr is at least (lo-bound value) - ((set (lo-bound (Get ctx i)) (IntB v))) + ((set (lo-bound (Get ctx i)) (maybe-some (either-left v)))) :ruleset interval-analysis) (rule ( @@ -376,13 +332,13 @@ ; the right operand of the < is an input to the if region (= expr (Get inputs i)) ; the left operand of the < has a lower bound - (= v (bound-int (lo-bound value))) + (= v (either-unwrap-left (maybe-unwrap (lo-bound value)))) ; context node inside the if region (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) ) ; value < expr was true, so we know expr is at least (lo-bound value) + 1 - ((set (lo-bound (Get ctx i)) (IntB (+ v 1)))) + ((set (lo-bound (Get ctx i)) (maybe-some (either-left (+ v 1))))) :ruleset interval-analysis) (rule ( ; value < expr @@ -391,13 +347,13 @@ ; the right operand of the < is an input to the if region (= expr (Get inputs i)) ; the left operand of the < has an upper bound - (= v (bound-int (hi-bound value))) + (= v (either-unwrap-left (maybe-unwrap (hi-bound value)))) ; context node inside the if region (= ctx (Arg ty (InIf false pred inputs))) (HasType inputs ty) ) ; value < expr was false, so we know expr is at most (hi-bound value) - ((set (hi-bound (Get ctx i)) (IntB v))) + ((set (hi-bound (Get ctx i)) (maybe-some (either-left v)))) :ruleset interval-analysis) ;; Push intervals for inputs into if region @@ -429,9 +385,9 @@ (= expr (Get inputs i)) (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) - (= lo (bound-int (lo-bound val))) + (= lo (either-unwrap-left (maybe-unwrap (lo-bound val)))) ) - ((set (lo-bound (Get ctx i)) (IntB lo))) + ((set (lo-bound (Get ctx i)) (maybe-some (either-left lo)))) :ruleset interval-analysis) (rule ( (= pred (Bop (Eq) expr val)) @@ -440,9 +396,9 @@ (= expr (Get inputs i)) (= ctx (Arg ty (InIf true pred inputs))) (HasType inputs ty) - (= hi (bound-int (hi-bound val))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound val)))) ) - ((set (hi-bound (Get ctx i)) (IntB hi))) + ((set (hi-bound (Get ctx i)) (maybe-some (either-left hi)))) :ruleset interval-analysis) diff --git a/dag_in_context/src/interval_analysis.rs b/dag_in_context/src/interval_analysis.rs index f1484867e..70a844eb9 100644 --- a/dag_in_context/src/interval_analysis.rs +++ b/dag_in_context/src/interval_analysis.rs @@ -13,8 +13,8 @@ fn int_interval_test( let with_arg_types = inp.clone().with_arg_types(emptyt(), expected_ty.clone()); let check = format!( " - (check (lo-bound {with_arg_types}) (IntB {lo})) - (check (hi-bound {with_arg_types}) (IntB {hi})) + (check (lo-bound {with_arg_types}) (maybe-some (either-left {lo}))) + (check (hi-bound {with_arg_types}) (maybe-some (either-left {hi}))) " ); interval_test(with_arg_types, expected_ty, arg, expected_val, check) @@ -32,8 +32,8 @@ fn bool_interval_test( let with_arg_types = inp.clone().with_arg_types(emptyt(), expected_ty.clone()); let check = format!( " - (check (lo-bound {with_arg_types}) (BoolB {lo})) - (check (hi-bound {with_arg_types}) (BoolB {hi})) + (check (lo-bound {with_arg_types}) (maybe-some (either-right {lo}))) + (check (hi-bound {with_arg_types}) (maybe-some (either-right {hi}))) " ); interval_test(with_arg_types, expected_ty, arg, expected_val, check) @@ -135,8 +135,8 @@ fn if_interval() -> crate::Result { &format!("{f}"), &format!( " - (check (lo-bound {e}) (IntB 4)) - (check (hi-bound {e}) (IntB 5)) + (check (lo-bound {e}) (maybe-some (either-left 4))) + (check (hi-bound {e}) (maybe-some (either-left 5))) " ), vec![f.to_program(base(intt()), base(intt()))], @@ -168,10 +168,10 @@ fn nested_if() -> crate::Result { &format!("{f}"), &format!( " - (check (lo-bound {inner}) (IntB 4)) - (check (hi-bound {inner}) (IntB 5)) - (check (lo-bound {outer}) (IntB 20)) - (check (hi-bound {outer}) (IntB 20))" + (check (lo-bound {inner}) (maybe-some (either-left 4))) + (check (hi-bound {inner}) (maybe-some (either-left 5))) + (check (lo-bound {outer}) (maybe-some (either-left 20))) + (check (hi-bound {outer}) (maybe-some (either-left 20)))" ), vec![f.to_program(base(intt()), base(intt()))], intv(2), @@ -186,7 +186,7 @@ fn context_if() -> crate::Result { let cond = less_eq(iarg(), int_ty(0, base(intt()))); // y = if cond {-1 * input} else {input} - // interval analysis should tell us that y is always positive (= (lo-bound y) (IntB 0)) + // interval analysis should tell us that y is always positive. let y = tif(cond, parallel!(arg()), mul(getat(0), int(-1)), getat(0)); // z = y < 0 @@ -232,7 +232,7 @@ fn context_if_rev() -> crate::Result { let cond = less_eq(int_ty(0, base(intt())), iarg()); // y = if cond {-1 * input} else {input} - // interval analysis should tell us that y is always negative (= (hi-bound y) (IntB 0)) + // interval analysis should tell us that y is always negative. let y = tif(cond, parallel!(iarg()), mul(getat(0), int(-1)), getat(0)); // z = 0 < y diff --git a/dag_in_context/src/optimizations/ivt.egg b/dag_in_context/src/optimizations/ivt.egg index 270fbee3b..d1837f4c7 100644 --- a/dag_in_context/src/optimizations/ivt.egg +++ b/dag_in_context/src/optimizations/ivt.egg @@ -7,17 +7,9 @@ (constructor IVTAnalysisPayload (Expr Expr TypeList) IVTPayload) (sort IVTRes (Pair IVTPayload i64)) -;; perm passthrough-perm passthrough-type passthrough-type-len -(primitive IVTAnalysisRes (Expr Expr TypeList i64) IVTRes - (pair (IVTAnalysisPayload _0 _1 _2) _3)) - -(primitive IVTMin (IVTRes IVTRes) IVTRes - (unstable-if (unstable-fn "<=" (pair-second _0) (pair-second _1)) _0 _1)) - - ;; use an analysis to avoid exploring all combinations of passthrough vs not passed through values. Always prefer not passed through ;; expr1 curr if result -(function IVTNewInputsAnalysisImpl (Expr Expr Node) IVTRes :merge (IVTMin old new)) +(function IVTNewInputsAnalysisImpl (Expr Expr Node) IVTRes :merge (pair-min-by-second-i64 old new)) ;; IVTNewInputsAnalysis computes a permutation perm which corresponds to accessing elements of an if region. ;; It also makes accesses of passthrough arguments access new indices after the length of the if region. @@ -27,7 +19,7 @@ ;; This new permutation is intended to be used with a substitution argument (Concat if-statement passthrough-args) ;; Also produced is a passthrough-perm, which selects all of the passthrough arguments and puts them in a single tuple ;; expr1 if result -(function IVTNewInputsAnalysis (Expr Node) IVTRes :merge (IVTMin old new)) +(function IVTNewInputsAnalysis (Expr Node) IVTRes :merge (pair-min-by-second-i64 old new)) (rule ( @@ -48,7 +40,7 @@ (let perm (Empty (TmpType) (InFunc "no-ctx"))) (set (IVTNewInputsAnalysisImpl loop-body rest (IfNode if-eclass pred inputs thn else)) - (IVTAnalysisRes perm perm (TNil) 0)) + (pair (IVTAnalysisPayload perm perm (TNil)) 0)) ) :ruleset ivt-analysis) ;; recursive case for accessing the if statement @@ -61,7 +53,7 @@ ) ( (let new-perm (Concat perm (Single (Get (Arg (TmpType) (InFunc "no-ctx")) ith)))) (set (IVTNewInputsAnalysisImpl loop-body rest ifnode) - (IVTAnalysisRes new-perm pperm passthrough-tys len)) + (pair (IVTAnalysisPayload new-perm pperm passthrough-tys) len)) ) :ruleset ivt-analysis) ;; recursive case for accessing a passed-through argument @@ -81,7 +73,7 @@ (let new-pperm (Concat pperm original-get-index)) (let new-passthrough-tys (TLConcat passthrough-tys (TCons new-ty (TNil)))) (set (IVTNewInputsAnalysisImpl loop-body rest ifnode) - (IVTAnalysisRes new-perm new-pperm new-passthrough-tys (+ len 1))) + (pair (IVTAnalysisPayload new-perm new-pperm new-passthrough-tys) (+ len 1))) ) :ruleset ivt-analysis) ; base case for accessing if statement @@ -93,7 +85,7 @@ (= last (Get if-eclass ith)) ) ( (let new-perm (Concat perm (Single (Get (Arg (TmpType) (InFunc "no-ctx")) ith)))) - (set (IVTNewInputsAnalysis loop-body ifnode) (IVTAnalysisRes new-perm pperm passthrough-tys len)) + (set (IVTNewInputsAnalysis loop-body ifnode) (pair (IVTAnalysisPayload new-perm pperm passthrough-tys) len)) ) :ruleset ivt-analysis) ; base case for accessing a passed-through argument @@ -112,7 +104,7 @@ (let original-get-index (Single (Get (Arg (TmpType) (InFunc "no-ctx")) ith))) (let new-pperm (Concat pperm original-get-index)) (let new-passthrough-tys (TLConcat passthrough-tys (TCons new-ty (TNil)))) - (set (IVTNewInputsAnalysis loop-body ifnode) (IVTAnalysisRes new-perm new-pperm new-passthrough-tys (+ len 1))) + (set (IVTNewInputsAnalysis loop-body ifnode) (pair (IVTAnalysisPayload new-perm new-pperm new-passthrough-tys) (+ len 1))) ) :ruleset ivt-analysis) diff --git a/dag_in_context/src/optimizations/mem_simple.egg b/dag_in_context/src/optimizations/mem_simple.egg index 6e0664caf..83a6add42 100644 --- a/dag_in_context/src/optimizations/mem_simple.egg +++ b/dag_in_context/src/optimizations/mem_simple.egg @@ -18,41 +18,41 @@ :ruleset mem-simple) (rule ((Bop (PtrAdd) e i) - (= lo (bound-int (lo-bound i))) + (= lo (either-unwrap-left (maybe-unwrap (lo-bound i)))) (> lo 0)) ((NoAlias e (Bop (PtrAdd) e i))) :ruleset mem-simple) (rule ((Bop (PtrAdd) e i) - (= hi (bound-int (hi-bound i))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound i)))) (< hi 0)) ((NoAlias e (Bop (PtrAdd) e i))) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Add) i diff))) - (= lo (bound-int (lo-bound diff))) + (= lo (either-unwrap-left (maybe-unwrap (lo-bound diff)))) (> lo 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Add) i diff))) - (= hi (bound-int (hi-bound diff))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound diff)))) (< hi 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Sub) i diff))) - (= lo (bound-int (lo-bound diff))) + (= lo (either-unwrap-left (maybe-unwrap (lo-bound diff)))) (> lo 0)) ((NoAlias p1 p2)) :ruleset mem-simple) (rule ((= p1 (Bop (PtrAdd) p i)) (= p2 (Bop (PtrAdd) p (Bop (Sub) i diff))) - (= hi (bound-int (hi-bound diff))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound diff)))) (< hi 0)) ((NoAlias p1 p2)) :ruleset mem-simple) diff --git a/dag_in_context/src/optimizations/memory.egg b/dag_in_context/src/optimizations/memory.egg index 8b6773a2a..45c9073f6 100644 --- a/dag_in_context/src/optimizations/memory.egg +++ b/dag_in_context/src/optimizations/memory.egg @@ -12,7 +12,7 @@ (rewrite (ExprSet-insert (ES set1) x) (ES (set-insert set1 x)) :ruleset memory-helpers) -(function ExprSet-length (ExprSet) i64 :no-merge) +(function ExprSet-length (ExprSet) i64 :merge old) (rule ((ES set1)) ((set (ExprSet-length (ES set1)) (set-length set1))) :ruleset memory-helpers) @@ -291,8 +291,8 @@ (AddIntIntervalToPtrPointees (MkIntInterval (I lo) (I hi)) (UnwrapPtrPointsTo (PointsToCells x aps)))) - :when ((= lo (bound-int (lo-bound e))) - (= hi (bound-int (hi-bound e)))) + :when ((= lo (either-unwrap-left (maybe-unwrap (lo-bound e)))) + (= hi (either-unwrap-left (maybe-unwrap (hi-bound e))))) :ruleset memory-helpers) (rewrite (PointsToCells (If c inputs t e) aps) @@ -331,7 +331,7 @@ :ruleset memory-helpers) ; avoid quadratic query -(function succ (i64) i64 :no-merge) +(function succ (i64) i64 :merge old) (rule ((PointsToCellsAtIter aps inputs pred-body i)) ((set (succ i) (+ i 1))) :ruleset memory-helpers) diff --git a/dag_in_context/src/optimizations/memory.rs b/dag_in_context/src/optimizations/memory.rs index ef3573fa1..8173efb74 100644 --- a/dag_in_context/src/optimizations/memory.rs +++ b/dag_in_context/src/optimizations/memory.rs @@ -16,7 +16,7 @@ fn listlike(el_tys: Vec<&str>, el_relations: Vec<&str>) -> String { (Nil-{datatype}) (Cons-{datatype} {tys_s} {datatype})) -(function Length-{datatype} ({datatype}) i64 :no-merge) +(function Length-{datatype} ({datatype}) i64 :merge old) (rule ((= x (Nil-{datatype}))) ((set (Length-{datatype} x) 0)) :ruleset always-run) diff --git a/dag_in_context/src/optimizations/switch_rewrites.egg b/dag_in_context/src/optimizations/switch_rewrites.egg index 7a158a726..8c65ab801 100644 --- a/dag_in_context/src/optimizations/switch_rewrites.egg +++ b/dag_in_context/src/optimizations/switch_rewrites.egg @@ -73,8 +73,8 @@ (= (Get thn k) (Get (Arg _ty (InIf true pred inputs)) i)) (= els_out (Get els k)) - (= y (bound-int (lo-bound els_out))) - (= y (bound-int (hi-bound els_out))) + (= y (either-unwrap-left (maybe-unwrap (lo-bound els_out)))) + (= y (either-unwrap-left (maybe-unwrap (hi-bound els_out)))) ) ( (union (Get if_e k) (Top (Select) pred a (Const (Int y) ty ctx))) @@ -90,8 +90,8 @@ (HasArgType if_e ty) (= thn_out (Get thn k)) - (= y (bound-int (lo-bound thn_out))) - (= y (bound-int (hi-bound thn_out))) + (= y (either-unwrap-left (maybe-unwrap (lo-bound thn_out)))) + (= y (either-unwrap-left (maybe-unwrap (hi-bound thn_out)))) ; input to the if (= b (Get inputs i)) @@ -151,4 +151,4 @@ (let inner (If inner_pred sub_arg_false inner_X inner_Y)) (union lhs (If a outer_ins outer_X inner ))) - :ruleset switch_rewrite) \ No newline at end of file + :ruleset switch_rewrite) diff --git a/dag_in_context/src/type_analysis.egg b/dag_in_context/src/type_analysis.egg index 019a5cbf6..d72dbea63 100644 --- a/dag_in_context/src/type_analysis.egg +++ b/dag_in_context/src/type_analysis.egg @@ -7,7 +7,7 @@ (TCons hd (TLConcat tl r)) :ruleset type-helpers) -(function TypeList-length (TypeList) i64 :no-merge) +(function TypeList-length (TypeList) i64 :merge old) (constructor TypeList-ith (TypeList i64) BaseType :unextractable) ;; Don't match on TypeList-ith because it is now lazily instantiated! (rule () ((set (TypeList-length (TNil)) 0)) :ruleset type-helpers) diff --git a/dag_in_context/src/utility/terms.egg b/dag_in_context/src/utility/terms.egg index 2f5afe083..85a1f8826 100644 --- a/dag_in_context/src/utility/terms.egg +++ b/dag_in_context/src/utility/terms.egg @@ -5,14 +5,9 @@ (ruleset terms-helpers-helpers) (sort TermAndCost (Pair Term i64)) -(sort UnitThunk (UnstableFn () Unit)) - -;; Returns the smaller of the two, keeping the old value on ties. -(primitive Smaller (TermAndCost TermAndCost) TermAndCost - (unstable-if (unstable-fn "<=" (pair-second _0) (pair-second _1)) _0 _1)) (function ExtractedExpr (Expr) TermAndCost - :merge (Smaller old new)) + :merge (pair-min-by-second-i64 old new)) ;; potential extractions- use so that when the costs are equal, we don't change the term ;; this preserves egglog's timestamp of when the last time ExtractedExpr was changed, fixing a big performance problem (relation PotentialExtractedExpr (Expr TermAndCost)) diff --git a/dag_in_context/src/utility/util.egg b/dag_in_context/src/utility/util.egg index 47052eb8d..b90993d1d 100644 --- a/dag_in_context/src/utility/util.egg +++ b/dag_in_context/src/utility/util.egg @@ -1,4 +1,4 @@ -(function ListExpr-length (ListExpr) i64 :no-merge) +(function ListExpr-length (ListExpr) i64 :merge old) (constructor ListExpr-ith (ListExpr i64) Expr :unextractable) (constructor ListExpr-suffix (ListExpr i64) ListExpr :unextractable) (constructor Append (ListExpr Expr) ListExpr :unextractable) @@ -19,7 +19,7 @@ (Cons e (Nil)) :ruleset always-run) -(function tuple-length (Expr) i64 :no-merge) +(function tuple-length (Expr) i64 :merge old) (rule ((HasType expr (TupleT tl)) (= len (TypeList-length tl))) From cf7c2de28155d2f53cea4d1ecca4593ca76dd019 Mon Sep 17 00:00:00 2001 From: Saul Shanabrook Date: Mon, 29 Jun 2026 11:01:18 -0400 Subject: [PATCH 3/4] Update egglog proof fixture dependencies --- Cargo.lock | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 106f3adba..9e03ac4f0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -789,7 +789,7 @@ dependencies = [ [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "chrono", "clap", @@ -821,7 +821,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "quote", "syn 2.0.114", @@ -830,7 +830,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "ordered-float", ] @@ -838,7 +838,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "anyhow", "dyn-clone", @@ -861,7 +861,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "arc-swap", "bumpalo", @@ -873,7 +873,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "anyhow", "bumpalo", @@ -902,7 +902,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#6b37b6b31cf878fd7384e470b216398d9cc006fe" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#fcdaccba715569e0b4c05938db267a2eb219b52a" dependencies = [ "egglog", "egglog-ast", @@ -915,7 +915,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "rayon", ] @@ -923,7 +923,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "clap", "hashbrown 0.16.1", @@ -937,7 +937,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/oflatt/egglog-duckdb.git?branch=oflatt-container-proofs#07650bedfe246ecaf4490d3074bc30bc5442bfe3" +source = "git+https://github.com/egraphs-good/egglog.git?branch=codex%2Fpr927-plus-pr930-eggcc-proof#9b5ce1114ac1cf407be78f1ec9493324fd296920" dependencies = [ "crossbeam", "egglog-concurrency", @@ -2605,7 +2605,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.59.0", + "windows-sys 0.52.0", ] [[package]] From 15ee7cbabe70d3b2e72d796bcf81cc2604626e7b Mon Sep 17 00:00:00 2001 From: Saul Shanabrook Date: Mon, 29 Jun 2026 11:24:55 -0400 Subject: [PATCH 4/4] Repin experimental after fixture cleanup --- Cargo.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 9e03ac4f0..eca6f27fe 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -902,7 +902,7 @@ dependencies = [ [[package]] name = "egglog-experimental" version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#fcdaccba715569e0b4c05938db267a2eb219b52a" +source = "git+https://github.com/egraphs-good/egglog-experimental.git?branch=codex%2Feggcc-proof-baseline-pr927#19ed86667733c56e4072956ce3b414b6860660bc" dependencies = [ "egglog", "egglog-ast", @@ -1035,7 +1035,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.59.0", + "windows-sys 0.52.0", ] [[package]] @@ -2060,7 +2060,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.59.0", + "windows-sys 0.52.0", ] [[package]] @@ -2293,7 +2293,7 @@ dependencies = [ "getrandom 0.4.1", "once_cell", "rustix", - "windows-sys 0.59.0", + "windows-sys 0.52.0", ] [[package]]