Skip to content

Speed up proof encoding using egglog's :merge and unboxing pairs #933

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
oflatt wants to merge 23 commits into
base: main
Choose a base branch
from
Draft

Speed up proof encoding using egglog's :merge and unboxing pairs #933

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
aa4f6a5
WIP: FD proof encoding — block-merge, TableInsert, multi-value bridge…
oflatt Jun 23, 2026
716964f
Multi-value bridge: generalize the merge eval to a value tuple
oflatt Jun 23, 2026
8c083d0
Multi-value front-end: transparent box/unbox for Pair-output functions
oflatt Jun 23, 2026
7a382be
Proof encoding: pair-valued FD views with per-row congruence proofs
oflatt Jun 23, 2026
4de3bdd
Proofs: add term-free MergeFnFree justification (reconstruct conclusion)
oflatt Jun 24, 2026
2f43eb6
Proofs: evolve MergeFnFree into index-carrying MergeFnIdx
oflatt Jun 24, 2026
aaa11ab
Proofs: FD pair-view for primitive-bodied custom functions (Phase A)
oflatt Jun 24, 2026
225be70
Proofs: fold single-parent UF invariant into the UF index :merge
oflatt Jun 24, 2026
007f5ac
Proofs: remove dead begin/uf-set primitives (block-merge superseded t…
oflatt Jun 24, 2026
36c46ef
egglog-bridge: add multi-value mint-in-merge (MergeFn::Construct)
oflatt Jun 24, 2026
65af7a0
Proofs: split MergeRow (view-row) from MergeIdx (bare body node)
oflatt Jun 24, 2026
7d7f8ae
Phase B: function-bodied custom FD encoder + fix desugar-rerun term-p…
oflatt Jun 24, 2026
d40d5e9
Phase C: reflexivize FD merge premises for eq-sort inputs (primitive-…
oflatt Jun 24, 2026
7083628
Phase C: document constructor-bodied eq-sort-input stays legacy; CHAN…
oflatt Jun 24, 2026
74ae66a
Phase C: constructor-bodied eq-sort-input customs on FD via identity-…
oflatt Jun 24, 2026
e0a971c
Scope identity-column merge short-circuit to FD views via :identity-v…
oflatt Jun 24, 2026
a1b3144
Remove legacy handle_merge_fn; trivial eq-sort-output merges on FD
oflatt Jun 24, 2026
7f713c7
Merge remote-tracking branch 'origin/main' into fd-proof-encoding
oflatt Jun 24, 2026
10156c0
Proofs: reject function-reading merges at the file-level gate (close …
oflatt Jun 24, 2026
e05e1cc
Typecheck: reject reading a function inside a :merge body in ALL modes
oflatt Jun 24, 2026
0c96720
test: a DB-reading primitive in :merge is rejected (merges are pure w…
oflatt Jun 24, 2026
6465a32
Revert CHANGELOG entries (PR should not modify the changelog)
oflatt Jun 24, 2026
8d07483
Tone down FD-proof documentation per review
oflatt Jun 24, 2026
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
4 changes: 4 additions & 0 deletions egglog-bridge/examples/ac.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,17 @@ fn main() {
let int_base = egraph.base_values_mut().register_type::<i64>();
let num_table = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "num".into(),
can_subsume: false,
});
let add_table = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id; 3],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "add".into(),
Expand Down
26 changes: 26 additions & 0 deletions egglog-bridge/examples/math.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,17 @@ fn main() {
// tables
let diff = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "diff".into(),
can_subsume: false,
});
let integral = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "integral".into(),
Expand All @@ -36,13 +40,17 @@ fn main() {

let add = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "add".into(),
can_subsume: false,
});
let sub = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "sub".into(),
Expand All @@ -51,6 +59,8 @@ fn main() {

let mul = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "mul".into(),
Expand All @@ -59,6 +69,8 @@ fn main() {

let div = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "div".into(),
Expand All @@ -67,6 +79,8 @@ fn main() {

let pow = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "pow".into(),
Expand All @@ -75,6 +89,8 @@ fn main() {

let ln = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "ln".into(),
Expand All @@ -83,6 +99,8 @@ fn main() {

let sqrt = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "sqrt".into(),
Expand All @@ -91,6 +109,8 @@ fn main() {

let sin = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "sin".into(),
Expand All @@ -99,6 +119,8 @@ fn main() {

let cos = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Id, ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "cos".into(),
Expand All @@ -107,6 +129,8 @@ fn main() {

let rat = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Base(rational_ty), ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "rat".into(),
Expand All @@ -115,6 +139,8 @@ fn main() {

let var = egraph.add_table(FunctionConfig {
schema: vec![ColumnTy::Base(string_ty), ColumnTy::Id],
num_values: 1,
identity_values: None,
default: DefaultVal::FreshId,
merge: MergeFn::UnionId,
name: "var".into(),
Expand Down
Loading
Loading