Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
118 commits
Select commit Hold shift + click to select a range
150f145
Add an occurrence-index catalog; post each row once per distinct value
oflatt Jul 27, 2026
8feaa93
Add occurrence atoms to the free-join query language
oflatt Jul 27, 2026
cdf3ad1
Expose occurrence atoms through the bridge
oflatt Jul 27, 2026
b1cf686
Add the (index name function (any cols...)) command
oflatt Jul 27, 2026
c642dee
Rebuild the encoding's eq-sort columns through a declared index
oflatt Jul 27, 2026
d0370dc
Document the index-driven rebuild; tidy the diff's comments
oflatt Jul 27, 2026
30d871a
Fix the defects two reviews found in the occurrence-index work
oflatt Jul 28, 2026
083ce8d
Test the silent defects; refuse the plan shapes an index cannot serve
oflatt Jul 28, 2026
6f9e989
Tell get_index which question a probe asks, rather than infer it
oflatt Jul 28, 2026
b561863
Test that an occurrence atom overrides the requested plan strategy
oflatt Jul 28, 2026
15bbe04
Tidy the comments added by the review fixes
oflatt Jul 28, 2026
39fbc88
Order a rule proof's substitution by first occurrence in the body
oflatt Jul 28, 2026
8104d89
Enumerate a rule head's conclusion sites in one place
oflatt Jul 28, 2026
5ddb853
Turn off the CSE prepass while the proof encoding is reworked
oflatt Jul 28, 2026
6fe4274
Record the integer_math cross-treatment failure as a bug, not an arti…
oflatt Jul 28, 2026
a1edaa0
Write down the proof-encoding rework plan
oflatt Jul 28, 2026
0ca6723
Check that a rule's conclusion can be rebuilt from its premises
oflatt Jul 28, 2026
87dfd0b
Make the encoding's set-if-empty read its own batch's pending inserts
oflatt Jul 28, 2026
17628ab
Record the check_shadowing clone as deferred, not taken
oflatt Jul 28, 2026
2a7303c
Split phase 2 into indexing and deletion
oflatt Jul 28, 2026
9670cc3
Stamp each rule proof with the head site it concludes at
oflatt Jul 28, 2026
9a6c61a
Make unchanged view row counts an explicit gate
oflatt Jul 28, 2026
09e4391
Record why a rule head's skeleton is not reconstructible from a site
oflatt Jul 28, 2026
14670be
Give encoder temporaries their own fresh-name counter
oflatt Jul 28, 2026
4db5308
Record how the canonicalization bridge is carried
oflatt Jul 28, 2026
40f2b14
Synthesize a rule head's proof skeleton instead of emitting it
oflatt Jul 28, 2026
4502d04
Read a deep proof without a deep call stack
oflatt Jul 28, 2026
75e7202
Write the sequenced plan down, and correct the Fiat note
oflatt Jul 28, 2026
fa5918a
Read each table once per extraction, not once per node
oflatt Jul 28, 2026
283e289
Apply the proof simplifier's reflexive identities before minting
oflatt Jul 28, 2026
f2f74b0
Record the premises-inline-then-chain design
oflatt Jul 28, 2026
ea9082f
Collapse the last reflexive composites, and stop reading a proof nobo…
oflatt Jul 28, 2026
403473d
Carry a rule's premises inline, and chain its later sites
oflatt Jul 29, 2026
c65362a
Stop storing a rule proof's terms, since nothing reads them
oflatt Jul 29, 2026
611c2d0
Record the refactor, two bugs, and correct the term-mode note
oflatt Jul 29, 2026
06b786d
Cover the indexed rebuild rule in unsafe_seminaive_matches_naive
oflatt Jul 29, 2026
365f068
Make correctness at every phase an invariant, not a hope
oflatt Jul 29, 2026
7fc8053
Drop the dd endpoints from the nightly for now
oflatt Jul 29, 2026
720065e
Pack a rebuild firing into one raw proof node
oflatt Jul 29, 2026
4c197d6
Stop re-minting the container anchor the rebuild primitive already wrote
oflatt Jul 29, 2026
d5c9d24
Stop minting the body Fiat triples nothing reads
oflatt Jul 29, 2026
7015b3a
Pack a rebuild firing's congruence steps into one row
oflatt Jul 29, 2026
a932b22
Fold a rebuild firing's e-class move into its packed row
oflatt Jul 29, 2026
9fa84f6
Defer the skeleton composites, so a head that reads none writes none
oflatt Jul 29, 2026
d5868f4
Narrow the row-count nondeterminism to merge-function invocations
oflatt Jul 29, 2026
b7b3028
Prototype the head-traversal unification over a sink
oflatt Jul 29, 2026
34fcda2
Revert the sink, keeping the congruence it made redundant
oflatt Jul 29, 2026
b0f8fbb
Require a rule's premises to cover its body facts
oflatt Jul 29, 2026
7ffbfbd
Let the nightly run be tried locally without publishing
oflatt Jul 29, 2026
ef231f1
Let the local nightly publish, since nothing is published
oflatt Jul 29, 2026
70479df
Pack a merge collision's displaced edge into one proof row
oflatt Jul 29, 2026
3912365
Restore the harness node count, and say how to count it
oflatt Jul 29, 2026
0feb461
Merge upstream main for the nightly uv and rustup bootstrap
oflatt Jul 29, 2026
9be2172
Stage a rule head's rows as a batch rather than one at a time
oflatt Jul 29, 2026
f948fe3
Record the follow-ups this PR is not doing
oflatt Jul 29, 2026
88586eb
Move the follow-ups out of the tree and into an issue
oflatt Jul 29, 2026
1da0392
Drop the rework plan from the tree
oflatt Jul 29, 2026
4d2e861
Remove the CSE prepass
oflatt Jul 29, 2026
bf881be
Fold a firing's five types into one
oflatt Jul 29, 2026
e24024d
Number a head's sites with a cursor instead of a shadow tree
oflatt Jul 29, 2026
1b00670
Give a head one lowering description instead of two
oflatt Jul 29, 2026
2815b8b
Stop offering a connector that is never absent
oflatt Jul 29, 2026
b8aa71f
Retire the reconstruction experiment
oflatt Jul 29, 2026
fbed16d
Name the head module after what is left in it
oflatt Jul 29, 2026
eeae874
Change-log the rework, and drop the entry for the removed prepass
oflatt Jul 29, 2026
037d26b
Check the site a rule proof names, not just that the head concludes it
oflatt Jul 29, 2026
e3462f3
Give rustup's shims PATH priority, not just PATH membership
oflatt Jul 29, 2026
c78b4a1
Read a chained rule proof's name off the row that carries it
oflatt Jul 29, 2026
4a17c3c
Fix the role a canonical-reflexive proof names
oflatt Jul 29, 2026
c135d84
Let a frame's stages branch directly instead of through a verdict type
oflatt Jul 29, 2026
53b5ec8
Describe the rule-head lowering the encoder emits
oflatt Jul 29, 2026
59b371b
Pin the preconditions the proof lowering relies on
oflatt Jul 30, 2026
6cf0fad
Say what the nightly measures, and reject a non-positive round count
oflatt Jul 30, 2026
ee2247a
Trim this branch's doc comments to the contract
oflatt Jul 30, 2026
441dc59
Say which globals add a premise, and point at the test for it
oflatt Jul 30, 2026
37afe30
Read a site's composition off the head, not off a re-encoding of it
oflatt Jul 30, 2026
1e739d7
Name a rule proof's conclusion with one integer
oflatt Jul 30, 2026
53751a9
Compose a head's proofs in one place, whichever side is asking
oflatt Jul 30, 2026
f42b6ed
Keep the conclusion site out of the checker
oflatt Jul 30, 2026
ca6c83a
Name a rule head's proofs by position, not by a role at a site
oflatt Jul 30, 2026
47cde85
Return a built term's two ids from the recursion, not through a map
oflatt Jul 30, 2026
8198f74
Tell the encoding doc as the proof it specifies, then the skeleton it…
oflatt Jul 30, 2026
e82ec30
Ask for the value-rebuild rule you want, not for a tag
oflatt Jul 30, 2026
8acefd1
Split a union's union-find edge by what justifies it
oflatt Jul 30, 2026
d7a45c4
Check a head's columns against the walk that fills them
oflatt Jul 30, 2026
7fe510c
Say out loud the shapes that would otherwise mint a wrong proof
oflatt Jul 30, 2026
ee809b6
Make a stale doc link fail the build
oflatt Jul 30, 2026
0dacb3e
Ask one thing which of the two layers is in force
oflatt Jul 30, 2026
bf0653f
Say that layer 1 is an algebra with two interpretations
oflatt Jul 30, 2026
bbefa37
Lay a head's columns out once, and check both walks against it
oflatt Jul 30, 2026
64fa634
Say what layer 1 does, not how obvious it is
oflatt Jul 30, 2026
9216c4a
Walk a nested term through layer 1, level by level
oflatt Jul 30, 2026
2e898d6
Trim this branch's new docs to the contract
oflatt Jul 30, 2026
579d119
Say why the natural node stays unseeded, and stop there
oflatt Jul 30, 2026
1da17fb
Ship a packed row's composition with the row
oflatt Jul 30, 2026
e8eccfb
Write a layer-1 composition as one row, not one per step
oflatt Jul 31, 2026
e1e00ec
Carry a packed row's skeleton in the row, not in its name
oflatt Jul 31, 2026
7fcf5ce
Hold a deferred group as its statements, nothing else
oflatt Jul 31, 2026
83f1f08
Hold both kinds of deferred proof in one map
oflatt Jul 31, 2026
a7c690d
Walk a rule head once per firing, not once per proof read out of it
oflatt Jul 31, 2026
91d8908
Take a row's bridges one at a time, rather than by position
oflatt Jul 31, 2026
8ecac21
Chain every rule proof row of a head, not only the composing ones
oflatt Jul 31, 2026
1422480
Lay a head out once, with its plan, not once per proof read out of it
oflatt Jul 31, 2026
a32cad1
Check the invariants three comments claim and nothing enforced
oflatt Jul 31, 2026
9eec432
Reflexivize a premise through the shared builders, not around them
oflatt Jul 31, 2026
1e48126
Stop reserving a head column nothing ever fills
oflatt Jul 31, 2026
230920e
State a rebuild row's shape once, so the test round-trips the encoder's
oflatt Jul 31, 2026
e4aa665
Hold a composition and its layout in one tree, not two
oflatt Jul 31, 2026
95e08a8
Describe each proof constructor once, for both readers of it
oflatt Jul 31, 2026
aaca9ae
Delete what nothing reads, and dedupe what two places matched
oflatt Jul 31, 2026
75251d4
Say each of the new docs' facts in one place
oflatt Jul 31, 2026
5cc4dc1
Say what proof mode costs a user, not how it is built
oflatt Jul 31, 2026
e15c13b
Clear every @UF table at the end of each maintenance run
oflatt Jul 31, 2026
f498e73
Measure the encoding's rebuild and search cost; make the @UF clear op…
oflatt Jul 31, 2026
b79d9b7
Report decomposed join plans, and stop binding the unread proof column
oflatt Aug 1, 2026
d8a6086
wip: dedup tuple-output view reads by inputs
oflatt Aug 1, 2026
0a85d44
Revert "wip: dedup tuple-output view reads by inputs"
oflatt Aug 1, 2026
b7d2d6c
Record why the FD dedup fix is reverted, and that decomposition is th…
oflatt Aug 1, 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
27 changes: 19 additions & 8 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
.PHONY: \
check nits test python-check python-nits rust-check rust-nits \
proof-tests benchmark-smoke nightly nightly-uv nightly-rustup \
proof-tests benchmark-smoke nightly nightly-local nightly-uv nightly-rustup \
update-snapshots format \
python-lock python-format-check python-lint python-typecheck python-test \
rust-format-check rust-clippy rust-test
rust-format-check rust-clippy rust-doc-links rust-test

BENCHMARK_SMOKE_REPORT ?= /tmp/egglog-encoding-bench-smoke.jsonl

Expand Down Expand Up @@ -47,7 +47,7 @@ python-test:

rust-check: rust-nits rust-test

rust-nits: rust-format-check rust-clippy
rust-nits: rust-format-check rust-clippy rust-doc-links

rust-format-check:
cargo fmt --all -- --check
Expand All @@ -60,6 +60,12 @@ rust-clippy:
cargo clippy --workspace --all-targets -- -D warnings
cargo clippy -p egglog-experimental --features dd-backend --all-targets -- -D warnings

# Clippy does not resolve doc links, and plain `cargo doc` skips the private
# items most of this codebase documents, so a rename leaves stale links behind
# unless rustdoc is run over them too.
rust-doc-links:
RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --document-private-items --workspace

# This is a name-filtered subset of rust-test, useful for proof iteration.
proof-tests:
cargo test --workspace --test files 'proofs/'
Expand All @@ -74,12 +80,12 @@ benchmark-smoke:
'from pathlib import Path; import sys; from benchmarking.reports.store import ReportStore; assert ReportStore(Path(sys.argv[1])).row_count > 0' \
"$(BENCHMARK_SMOKE_REPORT)"

# Benchmark every endpoint on this checkout and on main, then copy eval-live's
# interactive report to nightly/output/. The egraphs-good nightly service
# (nightly.cs.washington.edu) runs this target and serves that directory,
# matching `report=` in the nightly configuration.
# Benchmark each endpoint in nightly_bench.py's ENDPOINTS on this checkout and on
# main, then copy eval-live's interactive report to nightly/output/. The
# egraphs-good nightly service (nightly.cs.washington.edu) runs this target and
# serves that directory, matching `report=` in the nightly configuration.
nightly: nightly-uv nightly-rustup
$(NIGHTLY_UV) run --locked python scripts/nightly_bench.py
CARGO_HOME="$(CARGO_HOME_DIR)" $(NIGHTLY_UV) run --locked python scripts/nightly_bench.py

nightly-uv:
@command -v uv >/dev/null || test -x "$(UV_BOOTSTRAP_DIR)/uv" || \
Expand All @@ -92,6 +98,11 @@ nightly-rustup:
| env CARGO_HOME="$(CARGO_HOME_DIR)" sh -s -- \
-y --no-modify-path --default-toolchain none

# The nightly host's run at one round, for trying it locally. nightly/output/ is
# git-ignored, so this writes it just as the host does.
nightly-local: nightly-uv nightly-rustup
CARGO_HOME="$(CARGO_HOME_DIR)" $(NIGHTLY_UV) run --locked python scripts/nightly_bench.py --rounds 1

update-snapshots:
uv run --locked pytest -q --snapshot-update --snapshot-details

Expand Down
8 changes: 8 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ make rust-nits # rustfmt check and Clippy only
make proof-tests # proof-focused subset of the workspace tests
make benchmark-smoke
make nightly # benchmark the nightly endpoints and publish nightly/output/
make nightly-local # the same run at one round, for trying it out
make update-snapshots
make format # apply Ruff and rustfmt formatting
```
Expand Down Expand Up @@ -380,6 +381,9 @@ failing the run, and the output directory is only overwritten after a
successful run. Edit `TARGETS` and `ENDPOINTS` in `scripts/nightly_bench.py` to
change what is measured.

`make nightly-local` is the same run at `--rounds 1`, for trying the whole
pipeline out without waiting for a full nightly.

The [egraphs-good nightly service](https://nightly.cs.washington.edu) checks out
this repository, runs `make nightly`, and serves `nightly/output/`, matching the
`report=` entry in the nightly configuration. Two things that runner does not
Expand All @@ -390,6 +394,10 @@ the box has none. The runner also leaves rustup's `~/.cargo/bin` off `PATH`,
which would leave cargo resolving to Ubuntu's — too old for
`rust-toolchain.toml`'s pin — so `nightly_bench.py` puts those shims first.

Both installers run `curl … | sh`, so on a developer box prefer installing uv
and rustup yourself: `make nightly` and `make nightly-local` skip each one that
is already there. Only a bare CI runner needs them.

### CPU profiling

Benchmark reports answer whether and where performance changed. Use the
Expand Down
11 changes: 11 additions & 0 deletions egglog-experimental/dd/src/compile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -144,4 +144,15 @@ impl Slot {
pub struct ReadKey {
pub func: FunctionId,
pub mode: ReadMode,
/// Zero for an ordinary read. Otherwise this stream is the *occurrence view*
/// of `func`: one row per (value, base row) for each value the base row holds
/// in a column whose bit is set here, deduplicated per row.
pub occurrence_cols: u64,
}

impl ReadKey {
/// The columns the occurrence view reads, empty for an ordinary read.
pub fn occurrence_columns(&self) -> impl Iterator<Item = usize> + '_ {
(0..u64::BITS as usize).filter(|c| self.occurrence_cols & (1u64 << c) != 0)
}
}
50 changes: 48 additions & 2 deletions egglog-experimental/dd/src/dd_native.rs
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ pub const W: usize = 48;
/// A fixed-width relation or binding row flowing through the DD dataflow. Input
/// rows store relation columns in the low slots. Intermediate binding columns
/// are assigned by the current `ProjectionPlan` stage, and captured outputs
/// repack surviving variables into the low slots in [`JoinPlan::var_order`].
/// repack surviving variables into the low slots in [`JoinPlan`]'s variable order.
///
/// A NEWTYPE over `[u32; W]` (rather than the bare array) because timely's
/// `ExchangeData` bound required by DD joins is
Expand Down Expand Up @@ -181,6 +181,50 @@ pub fn plan_join(rule: &RuleSpec) -> Result<JoinPlan, String> {

for atom in &rule.core.body.atoms {
match atom.head {
// An index atom reads the occurrence view of `id`: the leading arg is
// the occurring value, then the base row. The relation's own unit
// output trails the args and is not part of the view.
RuleBodyCall::IndexTable {
id,
ref any_of,
read,
} => {
if let Some(col) = any_of.iter().find(|c| **c >= u64::BITS as usize) {
return Err(format!(
"index column {col} is beyond the {} a read key can track",
u64::BITS
));
}
let occurrence_cols = any_of.iter().fold(0u64, |m, c| m | (1u64 << c));
if occurrence_cols == 0 {
return Err("index atom lists no columns".to_string());
}
let view_args = atom
.args
.split_last()
.map(|(_unit, rest)| rest)
.unwrap_or(&atom.args);
if view_args.len() > W {
return Err(format!("atom arity {} > W {}", view_args.len(), W));
}
let slots = view_args
.iter()
.map(Slot::from_term)
.collect::<Result<Vec<_>, _>>()?;
for s in &slots {
if let Slot::Var(v) = s {
body_vars.insert(*v);
}
}
atoms.push(PlanAtom {
read_key: ReadKey {
func: id,
mode: read,
occurrence_cols,
},
slots,
});
}
RuleBodyCall::Table { id, read } => {
if atom.args.len() > W {
return Err(format!("atom arity {} > W {}", atom.args.len(), W));
Expand All @@ -199,6 +243,7 @@ pub fn plan_join(rule: &RuleSpec) -> Result<JoinPlan, String> {
read_key: ReadKey {
func: id,
mode: read,
occurrence_cols: 0,
},
slots,
});
Expand Down Expand Up @@ -406,7 +451,7 @@ pub struct FusedDdJoin {
/// The fused rules in caller-supplied build order. The sorted rule-index list
/// identifies the ruleset cache entry but does not reorder these outputs.
rules: Vec<FusedRule>,
/// Current epoch (monotonic; advanced once per [`step`]).
/// Current epoch (monotonic; advanced once per [`FusedDdJoin::step`]).
epoch: u32,
}

Expand Down Expand Up @@ -816,6 +861,7 @@ mod tests {

fn live(func: FunctionId) -> ReadKey {
ReadKey {
occurrence_cols: 0,
func,
mode: ReadMode::Live,
}
Expand Down
35 changes: 32 additions & 3 deletions egglog-experimental/dd/src/interpret.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,26 @@ use crate::{EGraph, TableDefault, ViewOp};
pub(crate) type Env = HashMap<u32, u32>;

type DdDeltaRows = HashMap<ReadKey, Vec<(Vec<u32>, isize)>>;

/// The occurrence view of `base`: for each row, one derived row `(value, row…)`
/// per distinct value the row holds in `read`'s columns. A value sitting in two
/// of them yields one derived row, not two — distinct base rows always give
/// distinct derived rows, so the map keys deduplicate exactly.
fn occurrence_view(base: &HashMap<Row, u64>, read: ReadKey) -> HashMap<Row, u64> {
let mut out = HashMap::new();
for (row, version) in base {
for col in read.occurrence_columns() {
let Some(&val) = row.get(col) else {
continue;
};
let mut derived = Vec::with_capacity(row.len() + 1);
derived.push(val);
derived.extend_from_slice(row);
out.insert(derived.into_boxed_slice(), *version);
}
}
out
}
type LookupIndex = HashMap<FunctionId, HashMap<Row, Row>>;

/// Retractions batched per function: the key length plus the set of keys to
Expand Down Expand Up @@ -219,7 +239,7 @@ pub fn run_iteration(eg: &mut EGraph, rules: &[(usize, RuleSpec)]) -> Result<Ite

/// Compute every rule's binding envs in ONE fused pass: the whole atom-bearing
/// ruleset's body joins run on a SINGLE shared timely worker
/// ([`dd_native::FusedDdJoin`]) clocked once this iteration, then each rule's
/// ([`crate::dd_native::FusedDdJoin`]) clocked once this iteration, then each rule's
/// host-side body primitives are re-run over its own bindings. Atom-less rules
/// (`(rule () …)`) have no input relation to drive the DD dataflow, so they are
/// fired once host-side. Returns a `Vec<Vec<Env>>` parallel to `rules` (same
Expand Down Expand Up @@ -321,13 +341,22 @@ fn fused_bindings(eg: &mut EGraph, rules: &[(usize, RuleSpec)]) -> Result<Vec<Ve
{
let fed = eg.dd_fused_fed_versions.entry(key.clone()).or_default();
for &read in &all_reads {
let cur = match read.mode {
let base = match read.mode {
ReadMode::Live => eg.live_versions.get(&read.func),
ReadMode::Subsumed => eg.subsumed_versions.get(&read.func),
ReadMode::All => eg.all_versions.get(&read.func),
};
let cur_empty: HashMap<Row, u64> = HashMap::new();
let cur = cur.unwrap_or(&cur_empty);
let base = base.unwrap_or(&cur_empty);
// An occurrence read is a view over the same rows, so deriving it
// here lets the delta diff below stay exactly the same.
let occurrence_rows;
let cur: &HashMap<Row, u64> = if read.occurrence_cols == 0 {
base
} else {
occurrence_rows = occurrence_view(base, read);
&occurrence_rows
};
let prev = fed.entry(read).or_default();
if prev == cur {
continue;
Expand Down
22 changes: 22 additions & 0 deletions egglog-experimental/dd/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,28 @@ impl EGraph {

for atom in &rule.core.body.atoms {
match atom.head {
RuleBodyCall::IndexTable { id, ref any_of, .. } => {
let info = relation(id, "rule body")?;
// The occurring value, the base row, and the index relation's
// own unit output.
let expected = info.arity + 2;
if atom.args.len() != expected {
bail!(
"DD backend cannot add rule {:?}: index atom over `{}` has {} columns, expected {expected}",
rule.name,
info.name,
atom.args.len()
);
}
if let Some(col) = any_of.iter().find(|c| **c >= info.arity) {
bail!(
"DD backend cannot add rule {:?}: index atom over `{}` reads column {col}, but it has arity {}",
rule.name,
info.name,
info.arity
);
}
}
RuleBodyCall::Table { id, .. } => {
if atom.args.len() > dd_native::W {
bail!(
Expand Down
2 changes: 1 addition & 1 deletion egglog-experimental/src/fresh_macro.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ fn collect_fresh_options(actions: Actions) -> Result<Vec<FreshOptions>, Error> {
}

/// Parse the arguments to unstable-fresh!
/// Syntax: (unstable-fresh! SortName [:cost N] [:unextractable])
/// Syntax: `(unstable-fresh! SortName [:cost N] [:unextractable])`
fn parse_fresh_args(span: &egglog::ast::Span, args: &[Expr]) -> Result<FreshOptions, Error> {
if args.is_empty() {
return Err(Error::ParseError(ParseError(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,4 @@ expression: snapshot
(substitution (a (Var "x")) (b (Var "y"))))
prf0
(Fiat (= () ())))
(substitution (?y (Var "x")) (?x t0)))
(substitution (?x t0) (?y (Var "x"))))
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,4 @@ expression: snapshot
(= t0 (Add (Num 3) (Num 2)))
(name "(rewrite (Add a b) (Add b a) :ruleset optimization)")
(premises (Fiat (= t0 t0)))
(substitution (a (Num 2)) (b (Num 3)) (@rewrite_var__ t0)))
(substitution (@rewrite_var__ t0) (a (Num 2)) (b (Num 3))))
Loading
Loading