ExecutionState unsafe with seminaive

[oflatt]

ExecutionState currently allows reads and writes everywhere. This means that queries can write and actions can read, which breaks seminaive. Queries writing means a rule can write even while running a query, which shouldn't happen in egglog. Actions reading means that we need to run them every iteration in case they behave differently, breaking saturation.

@yihozhang and I discussed and came up with a proposed fix.

• In queries, neither reading or writing from the database is allowed unless seminaiive is disabled.
• In actions, reading is disallowed but writing is allowed.
• In global queries, reading is allowed but not writing.
• In global actions, you can do whatever you want as you can now

[saulshanabrook]

I think @yihozhang and @oflatt and I agreed that this made sense, it is just a lift to implement and refactor things.

[oflatt]

Claude came up with a proposal to fix this, it looks good to me

Proposal: typed execution states for seminaive safety (#772)

Problem

ExecutionState currently grants primitives and external functions unrestricted read and write access to the database, regardless of whether they are being invoked from a rule query, a rule action, or a global (top-level) command. This is unsafe under seminaive evaluation:

• A query that writes allows a rule to mutate the database while it is still matching atoms. Rules can fire off one another within a single iteration, and "the database state at the start of the iteration" is no longer well-defined.
• A query that reads arbitrary database state bypasses the only mechanism seminaive uses to decide when to re-fire a rule. See the detailed explanation below.
• An action that reads makes the effect of a match depend on live database state rather than only on the matched bindings. Saturation detection (nothing-changed → stop) becomes unsound, because the same match can do different things across iterations.

There is already an acknowledging comment at core-relations/src/action/mod.rs:481 ("Dangerous: Reading from a table during action execution may break the semi-naive evaluation"). PR #832 patched one container-specific manifestation of this; #772 is the broader architectural fix.

Semi-naive recap

Each iteration, seminaive restricts matches so that at least one atom comes from a "new" timestamp slice. That is only sound if:

1. Queries are pure functions of the pre-iteration database state, and egglog knows every table they read from. Reads of tables that are explicitly named as atoms in the query are fine — seminaive tracks their timestamps and re-fires the rule when those rows change. No writes during matching.
2. Actions are pure functions of the matched bindings (no reads of live database state during application).

Any primitive or external function invoked from inside a rule must honor the same rules.

Why reads are also forbidden in queries

The specific reason reads are disallowed in queries (not just writes) is that seminaive's re-firing logic only tracks reads it knows about. The atoms listed in a rule's body tell egglog which tables that rule depends on; those tables' timestamps drive the decision to re-run the rule. A primitive that reaches into the database on the side to read some other table leaves seminaive blind to that dependency, so the rule will not be re-fired when those reads could produce different answers. This is the same class of issue PR #832 fixed narrowly for container-backed reads; disallowing arbitrary reads from queries is the soundness-preserving default.

Future work could relax this: a primitive that reads from the database could declare which tables (or columns, or value ranges) it read, and seminaive could treat those declared reads as additional virtual dependencies — re-firing the rule when any of them change. That would require dependency reporting from primitives, reverse invalidation indexes, and scheduler support for waking matches without a real row delta (as outlined in #832's "longer-term alternatives" section). The typed-state design in this proposal is a natural place to hang that extension: a new capability trait (say ExecStateDeclaredReadDb) could expose a lookup API that also records what was read, and a future RuleQueryState could implement it.

Four execution contexts

Context	DB reads	DB writes	Used for
RuleQuery	no	no	rule LHS, seminaive on
RuleAction	no	yes	rule RHS, seminaive on
GlobalQuery	yes	no	top-level query-shaped commands (check)
GlobalAction	yes	yes	top-level action-shaped commands, eval

When seminaive is disabled, rule bodies degrade to GlobalQuery / GlobalAction respectively.

Design

Core stays internal; a user-facing wrapper layer is added

core_relations::ExecutionState stays unchanged. Internals that need unrestricted access continue to use it directly. The public primitive / external-function surface moves to four wrapper types that each borrow &mut ExecutionState and expose only the methods safe in their context.

pub struct RuleQueryState<'a, 'b>    { inner: &'a mut ExecutionState<'b> }
pub struct RuleActionState<'a, 'b>   { inner: &'a mut ExecutionState<'b> }
pub struct GlobalQueryState<'a, 'b>  { inner: &'a mut ExecutionState<'b> }
pub struct GlobalActionState<'a, 'b> { inner: &'a mut ExecutionState<'b> }

Capability traits (for code sharing across wrappers)

pub trait ExecStateCore {
    fn base_values(&self) -> &BaseValues;
    fn read_counter(&self, c: CounterId) -> usize;
    fn inc_counter(&self, c: CounterId) -> usize;
    fn trigger_early_stop(&self);
    fn should_stop(&self) -> bool;
    // + container reads (idempotent interning, safe everywhere)
}

pub trait ExecStateReadDb: ExecStateCore {
    fn get_table(&self, id: TableId) -> &WrappedTable;
    fn table_lookup(&mut self, ...);     // TableAction::lookup
    fn predict_val(&mut self, ...);
    fn predict_col(&mut self, ...);
}

pub trait ExecStateWriteDb: ExecStateCore {
    fn stage_insert(&mut self, id: TableId, row: &[Value]);
    fn stage_remove(&mut self, id: TableId, key: &[Value]);
    // TableAction::insert / remove / subsume, UnionAction::union
    // container register_val
}

Impl matrix:

Wrapper	ExecStateCore	ExecStateReadDb	ExecStateWriteDb
RuleQueryState	yes	no	no
RuleActionState	yes	no	yes
GlobalQueryState	yes	yes	no
GlobalActionState	yes	yes	yes

Code sharing happens naturally: a method that only needs ExecStateCore is written once as a default-methods-on-trait or a free function generic over S: ExecStateCore, and all four wrappers get it.

Primitive trait with a GAT

Each primitive declares the minimum state wrapper it needs via an associated type. That single declaration serves three jobs at once:

1. The Rust type checker enforces (at compile time, not in egglog's own type checker) that the primitive body only uses capabilities available on its declared wrapper.
2. Registration derives which contexts the primitive is valid in, via a UserState::valid_contexts() const.
3. The dispatch wrapper knows how to construct the right user-facing wrapper from &mut ExecutionState at call time.

pub trait UserState<'a, 'b>: Sized + ExecStateCore {
    fn wrap(es: &'a mut ExecutionState<'b>) -> Self;
    fn valid_contexts() -> &'static [Context];
}

impl<'a, 'b> UserState<'a, 'b> for RuleQueryState<'a, 'b> {
    fn wrap(es: &'a mut ExecutionState<'b>) -> Self { RuleQueryState { inner: es } }
    fn valid_contexts() -> &'static [Context] {
        &[Context::RuleQuery, Context::RuleAction, Context::GlobalQuery, Context::GlobalAction]
    }
}
impl<'a, 'b> UserState<'a, 'b> for RuleActionState<'a, 'b> {
    fn wrap(es: &'a mut ExecutionState<'b>) -> Self { RuleActionState { inner: es } }
    fn valid_contexts() -> &'static [Context] {
        &[Context::RuleAction, Context::GlobalAction]
    }
}
// ... GlobalQueryState, GlobalActionState similar

pub trait Primitive: Send + Sync + 'static
where for<'a, 'b> Self::State<'a, 'b>: UserState<'a, 'b>,
{
    type State<'a, 'b>;

    fn name(&self) -> &str;
    fn get_type_constraints(&self, span: &Span) -> Box<dyn TypeConstraint>;
    fn apply<'a, 'b>(&self, state: &mut Self::State<'a, 'b>, args: &[Value]) -> Option<Value>;
}

Typical primitive impls:

impl Primitive for AddI64 {
    type State<'a, 'b> = RuleQueryState<'a, 'b>;   // pure — most restrictive, valid everywhere
    fn apply<'a, 'b>(&self, s: &mut RuleQueryState<'a, 'b>, args: &[Value]) -> Option<Value> { ... }
}

impl Primitive for Union {
    type State<'a, 'b> = RuleActionState<'a, 'b>;  // needs writes
    fn apply<'a, 'b>(&self, s: &mut RuleActionState<'a, 'b>, args: &[Value]) -> Option<Value> { ... }
}

Single add_primitive

Because the Primitive trait carries all the information, registration is one method:

impl EGraph {
    pub fn add_primitive<P: Primitive>(&mut self, p: P)
    where for<'a, 'b> P::State<'a, 'b>: UserState<'a, 'b>,
    {
        let arc = Arc::new(p);
        let erased: Arc<dyn ErasedPrimitive> = Arc::new(Wrap(arc));
        let ctxs = <P::State<'static, 'static> as UserState>::valid_contexts();
        for ctx in ctxs {
            self.prims_by_context[*ctx].insert(erased.name().into(), erased.clone());
        }
    }
}

ErasedPrimitive is the standard Box<dyn> façade over the generic apply:

trait ErasedPrimitive: Send + Sync {
    fn name(&self) -> &str;
    fn invoke(&self, es: &mut ExecutionState, args: &[Value]) -> Option<Value>;
}

struct Wrap<P: Primitive>(Arc<P>);
impl<P: Primitive> ErasedPrimitive for Wrap<P>
where for<'a, 'b> P::State<'a, 'b>: UserState<'a, 'b>,
{
    fn name(&self) -> &str { self.0.name() }
    fn invoke(&self, es: &mut ExecutionState, args: &[Value]) -> Option<Value> {
        let mut s = <P::State<'_, '_> as UserState>::wrap(es);
        self.0.apply(&mut s, args)
    }
}

Bridge wiring

The bridge already knows which context it is emitting into: BackendRule::query() compiles LHS primitives, BackendRule::actions() compiles RHS primitives. Each looks up the primitive in the context-appropriate registry and uses the associated ExternalFunctionId. If the primitive is not registered for the requested context, rule-build fails with a clear error ("primitive foo writes to the database and cannot be used in a rule query"). Global contexts (check_facts, eval_expr, etc.) pick their own registries accordingly.

No Instr::SetPermissions marker or other core-relations change is needed: the typed wrappers + per-context registry are enough.

Validation (already prototyped)

Two minimal Rust examples have been compiled and run:

1. Dispatch works. A generic Primitive with GAT State<'a, 'b>, stored behind Arc<dyn ErasedPrimitive>, dispatches correctly. A pure primitive registers in all four contexts; a writing primitive registers only in RuleAction and GlobalAction.
2. Compile-time enforcement works. A primitive declaring type State = RuleQueryState whose body calls a write method fails to compile with:

   error[E0599]: no method named write found for mutable reference &mut RuleQueryState<'a>
   the following traits define an item write: ExecStateWriteDb, ...

Implementation plan

1. Add ExecStateCore / ExecStateReadDb / ExecStateWriteDb traits and the four *State wrappers (likely in egglog-bridge so the bridge can expose TableAction-style operations on the write trait).
2. Define the new Primitive trait with the State GAT and HRTB bound, plus UserState and ErasedPrimitive.
3. Implement per-context registries keyed on name, plus the single add_primitive entry point and the context-aware lookups used by the rule builder and global command paths.
4. Migrate the ~14 in-tree impl Primitive for … sites (vec, multiset, fn, InnerProduct, RustRuleRhs, the add_primitive! proc macro, etc.) to declare a State type. Most are pure and pick RuleQueryState.
5. Delete RustRuleContext; its role is subsumed by the new wrappers. Existing rust_rule callers pick the appropriate wrapper (likely RuleActionState).
6. Audit container APIs: register_val is a write (placed on ExecStateWriteDb); get_val is a read that is idempotent and safe everywhere (placed on ExecStateCore). Containers should only be registered at the top level, not inside rule queries.
7. Add regression tests: a rule that tries to use a writing primitive on the LHS should fail at rule-build time; a rule that tries to use a reading primitive on the RHS should fail similarly.

Open questions

1. FunctionContainer::apply mixes modes: the Lookup variant writes, the Prim variant is whatever the wrapped primitive is. Either split it into query-safe and action-only variants, or require the write capability conservatively. Needs someone familiar with the higher-order function sort.
2. Rust/ergonomics polish: hide HRTB syntax behind type aliases (type RuleQueryPrim = dyn for<'a, 'b> Primitive<State<'a, 'b> = RuleQueryState<'a, 'b>>), and consider a derive or macro helper for the common case of "pure primitive, just give me a function body".

Trade-offs and non-concerns

• Breaking change to every impl Primitive for X, but the migration is mechanical (one extra associated-type line per impl, occasional tightening if the body happened to rely on forbidden capabilities).
• One entry point (add_primitive) for users, regardless of capability.
• Core ExecutionState stays untouched.
• Runtime cost is negligible: each primitive is still stored once and wrapped once.

[saulshanabrook]

Feedback from the agent with context about #832, which fixed a seminaive container bug, but in a not comprehensive way.

This proposal looks like the right public API direction, but I think it should explicitly encode the lesson from #832: seminaive unsoundness is caused by hidden dependencies, not only by obvious DB reads/writes through ExecutionState.

PR #832 fixed a case where the hidden dependency was internal container state. A rule row stored the same outer container id before and after rebuild, but the container’s contents changed from a non-matching shape to a matching shape. Since no parent-row delta was produced, seminaive did not revisit the row. The dirty_ids refresh path repairs exactly that missing delta.

So I would adjust the proposal in these ways:

1. Do not say container reads are “safe everywhere” without qualification.

Container lookup can be seminaive-sensitive. It is safe in rule queries only if the container id is an explicit matched value and changes to that container’s semantics are surfaced back to seminaive, currently via ContainerRebuildSummary::dirty_ids and refresh_rows_for_values.

register_val / interning a container is a write and should not be in ExecStateCore.

2. Make ExecStateCore smaller.

I would not put inc_counter in ExecStateCore; incrementing a counter is a side effect and should not be available in RuleQueryState.

I would also think carefully about read_counter. If a query primitive branches on a counter value, that is a hidden read dependency unless the counter is guaranteed stable for the rule’s lifetime or tracked as a dependency.

A safer starting point for ExecStateCore is mostly immutable services like base-value access and control/status hooks that do not affect rule matching.

3. Distinguish “public primitive restrictions” from “internal runtime dependencies.”

Typed wrappers can prevent user primitives and external functions from performing seminaive-unsafe reads/writes. They do not by themselves replace #832’s dirty-id repair, because #832 is about internal rebuild changing the meaning of an existing value without changing the parent row.

The proposal should say that #832’s container refresh remains required until/unless there is a general dependency reporting system.

4. Add a fifth future capability for declared reads.

The proposal already hints at ExecStateDeclaredReadDb; I would make that more central. That is the general version of what #832 did manually.

A query primitive that wants to read DB/container/UF state should eventually have to report what it read. Seminaive can then treat those reads as dependencies and refire affected rules when they change.

5. Be careful with “seminaive disabled => GlobalQuery / GlobalAction.”

Naive rule execution can tolerate more hidden reads because it reruns all rules, but it is still not exactly the same as top-level global execution. Query-side writes during matching are still suspicious even without seminaive. I would phrase this as “seminaive-disabled rule contexts may use less restrictive wrappers” rather than equating them directly with global contexts.

6. Treat FunctionContainer::apply as a real design blocker, not a minor open question.

The higher-order function path was involved in the original reproductions. If a function container can either look up a table, call a primitive, or allocate/register containers, its capability should be the join of what it may do. The plan should either split query-safe/action-only function application or conservatively mark mixed application as unavailable in RuleQueryState.

Suggested addition:

Lessons from #832: seminaive safety also depends on value-level rebuilds. A primitive or matcher may only inspect evolving value semantics in a rule query if those changes are reflected as table deltas or declared dependencies. Container rebuild currently does this through ContainerRebuildSummary::dirty_ids; the typed-state design should preserve that mechanism and eventually provide a general dependency-reporting replacement.

So: yes, this plan builds on the same model we learned from the bug. The change I’d push for is to make #832’s dirty-id mechanism an explicit constraint in the design, not just background context.

[saulshanabrook]

I also have three examples that use containers a bit. The first two should work out of the box on the main branches of egglog and egglog-experimental. The last one requires using my two in progress branches that add more primitives and also a (primitive ..) command in experimental.

Tracing Scikit-learn code and JIT compiling into a string

https://github.com/egraphs-good/egglog-python/blob/8812ec9585f68342fb0e9817326ea84828accf56/python/tests/test_array_api.py#L484-L492

generated egg file (too big for this comment): https://gist.github.com/saulshanabrook/604b417792dc4d2c65a773b3129aac0c

Converting to/from polynomials and factoring

https://github.com/egraphs-good/egglog-python/blob/8812ec9585f68342fb0e9817326ea84828accf56/python/tests/test_array_api.py#L464-L466

(sort Value)
(constructor %z () Value)
(let $__expr_0 (%z))
(constructor Value___pow__ (Value Value) Value)
(constructor %x () Value)
(sort Int)
(constructor Value_from_int (Int) Value)
(constructor Int___init__ (i64) Int)
(let $__expr_1 (Value___pow__ (%x) (Value_from_int (Int___init__ 2))))
(constructor %y () Value)
(let $__expr_2 (%y))
(constructor Value___add__ (Value Value) Value)
(constructor Value___mul__ (Value Value) Value)
(constructor %q () Value)
(let $x (Value___add__ (Value___mul__ (Value___mul__ $__expr_1 $__expr_0) $__expr_2) (Value___mul__ (Value___mul__ (Value___mul__ $__expr_1 (%q)) $__expr_0) $__expr_2)))
(ruleset egglog.exp.array_api.to_polynomial_ruleset)
(sort MultiSet[Value] (MultiSet Value))
(sort MultiSet[MultiSet[Value]] (MultiSet MultiSet[Value]))
(constructor polynomial (MultiSet[MultiSet[Value]]) Value)
(function get_sole_polynomial (MultiSet[Value]) MultiSet[MultiSet[Value]] :merge new)
(rule ((= _n3 (Value___add__ _n1 _n2))
       (= _mss (multiset-of (multiset-of _n1) (multiset-of _n2))))
      ((union _n3 (polynomial _mss))
       (set (get_sole_polynomial (multiset-of (polynomial _mss))) _mss)
       (delete (Value___add__ _n1 _n2)))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "add")
(function get_monomial (Value) MultiSet[Value] :merge new)
(rule ((= _n3 (Value___mul__ _n1 _n2))
       (= _ms (multiset-of _n1 _n2)))
      ((union _n3 (polynomial (multiset-of _ms)))
       (set (get_monomial (polynomial (multiset-of _ms))) _ms)
       (delete (Value___mul__ _n1 _n2)))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "mul")
(rule ((= _n3 (Value___pow__ _n1 (Value_from_int (Int___init__ _i))))
       (>= _i 0)
       (= _ms (multiset-single _n1 _i)))
      ((union _n3 (polynomial (multiset-of _ms)))
       (set (get_monomial (polynomial (multiset-of _ms))) _ms)
       (delete (Value___pow__ _n1 (Value_from_int (Int___init__ _i)))))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "pow")
(sort UnstableFn[MultiSet[Value],MultiSet[Value]] (UnstableFn (MultiSet[Value]) MultiSet[Value]))
(sort UnstableFn[MultiSet[Value],Value] (UnstableFn (Value) MultiSet[Value]))
(rule ((= _n1 (polynomial _mss))
       (= _mss1 (unstable-multiset-map (unstable-fn "unstable-multiset-flat-map" (unstable-fn "get_monomial")) _mss))
       (!= _mss _mss1))
      ((union _n1 (polynomial _mss1))
       (delete (polynomial _mss))
       (set (get_sole_polynomial (multiset-of _n1)) _mss1))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "unwrap monomial")
(sort UnstableFn[MultiSet[MultiSet[Value]],MultiSet[Value]] (UnstableFn (MultiSet[Value]) MultiSet[MultiSet[Value]]))
(rule ((= _n1 (polynomial _mss))
       (= _mss1 (unstable-multiset-flat-map (unstable-fn "get_sole_polynomial") _mss))
       (!= _mss _mss1))
      ((union _n1 (polynomial _mss1))
       (delete (polynomial _mss))
       (set (get_sole_polynomial (multiset-of _n1)) _mss1))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "unwrap polynomial")
(ruleset egglog.exp.array_api.factor_ruleset)
(sort UnstableFn[Unit,MultiSet[Value]] (UnstableFn (MultiSet[Value]) Unit))
(sort UnstableFn[MultiSet[Value],MultiSet[Value],MultiSet[Value]] (UnstableFn (MultiSet[Value] MultiSet[Value]) MultiSet[Value]))
(rule ((= _n (polynomial _mss))
       (= _counts (multiset-sum-multisets (unstable-multiset-map (unstable-fn "multiset-reset-counts") _mss)))
       (= _picked_term (multiset-pick-max _counts))
       (> (multiset-count _counts _picked_term) 1)
       (= _picked (unstable-multiset-filter (unstable-fn "multiset-contains-swapped" _picked_term) _mss))
       (= _factor (unstable-multiset-reduce (unstable-fn "multiset-intersection") (multiset-pick _picked) _picked))
       (= _divided (unstable-multiset-map (unstable-fn "multiset-subtract-swapped" _factor) _picked))
       (= _remainder (unstable-multiset-filter (unstable-fn "multiset-not-contains-swapped" _picked_term) _mss)))
      ((union _n (polynomial (multiset-sum (multiset-of (multiset-insert _factor (polynomial _divided))) _remainder)))
       (delete (polynomial _mss)))
        :ruleset egglog.exp.array_api.factor_ruleset :name "factor")
(ruleset egglog.exp.array_api.from_polynomial_ruleset)
(sort UnstableFn[Value,Value,Value] (UnstableFn (Value Value) Value))
(sort UnstableFn[Value,MultiSet[Value]] (UnstableFn (MultiSet[Value]) Value))
(rule ((= _n (polynomial _mss)))
      ((union _n (unstable-multiset-reduce (unstable-fn "Value___add__") (Value_from_int (Int___init__ 0)) (unstable-multiset-map (unstable-fn "unstable-multiset-reduce" (unstable-fn "Value___mul__") (Value_from_int (Int___init__ 1))) _mss)))
       (delete (polynomial _mss)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ _n _n)))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ 2))))
       (delete (Value___mul__ _n _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ (Value___pow__ _n (Value_from_int (Int___init__ _i))) _n)))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ (+ _i 1)))))
       (delete (Value___mul__ (Value___pow__ _n (Value_from_int (Int___init__ _i))) _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ _n (Value___pow__ _n (Value_from_int (Int___init__ _i))))))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ (+ _i 1)))))
       (delete (Value___mul__ _n (Value___pow__ _n (Value_from_int (Int___init__ _i))))))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ _n _n)))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ 2)) _n))
       (delete (Value___add__ _n _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ (Value___mul__ (Value_from_int (Int___init__ _i)) _n) _n)))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ (+ _i 1))) _n))
       (delete (Value___add__ (Value___mul__ (Value_from_int (Int___init__ _i)) _n) _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ _n (Value___mul__ (Value_from_int (Int___init__ _i)) _n))))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ (+ _i 1))) _n))
       (delete (Value___add__ _n (Value___mul__ (Value_from_int (Int___init__ _i)) _n))))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(run-schedule (seq (seq (saturate (run egglog.exp.array_api.to_polynomial_ruleset)) (saturate (run egglog.exp.array_api.factor_ruleset))) (saturate (run egglog.exp.array_api.from_polynomial_ruleset))))
(extract $x 0)

Symbolic Regression Simplification Example

Requires these branches:

https://github.com/egraphs-good/egglog-python/blob/169f45be43394eb78d443ee834019d542bec1a54/python/egglog/exp/param_eq/pipeline.py

https://github.com/saulshanabrook/egg-smol/tree/scheduler-fix pinned at a1820cc
https://github.com/egraphs-good/egglog-experimental/tree/egglog-compat pinned at 9416608e01ab614cca77c8565991f1fd14114aee

This Python code produces this trace:

from egglog.exp.param_eq.original_results import load_original_results
from egglog.exp.param_eq.pipeline import (
    parse_expression,
    parse_expression_container,
    run_paper_pipeline,
    run_paper_pipeline_container,
)

rows = load_original_results()

row = rows[
    (rows["dataset"] == "kotanchek")
    & (rows["raw_index"] == 96)
    & (rows["algorithm_raw"] == "GOMEA")
    & (rows["algo_row"] == 7)
    & (rows["input_kind"] == "sympy")
].iloc[0]
expr = row["orig_parsed_expr"]
container_report = run_paper_pipeline_container(parse_expression_container(expr))

(sort Num)
(constructor Num_var (String) Num)
(let $_0 (Num_var "x1"))
(sort Map[Num,BigRat] (Map Num BigRat))
(sort Map[Map[Num,BigRat],f64] (Map Map[Num,BigRat] f64))
(constructor polynomial (Map[Map[Num,BigRat],f64]) Num)
(constructor egglog_exp_param_eq_domain_exp (Num) Num)
(constructor Num___init__ (f64) Num)
(polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (polynomial (map-insert (map-empty) (map-insert (map-empty) (polynomial (map-insert (map-insert (map-insert (map-insert (map-insert (map-empty) (map-empty) -6.619000000000001) (map-insert (map-empty) $_0 (bigrat (from-string "1") (from-string "1"))) -15.509) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) 1.0) (map-insert (map-empty) (egglog_exp_param_eq_domain_exp $_0) (bigrat (from-string "1") (from-string "1"))) 1.0) (map-insert (map-empty) (egglog_exp_param_eq_domain_exp (polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) (polynomial (map-insert (map-insert (map-empty) (map-empty) -2.0) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) 1.0)) (bigrat (from-string "1") (from-string "1"))) 1.0))) (bigrat (from-string "1") (from-string "1"))) 0.30129507364144237)) (bigrat (from-string "1") (from-string "1"))) -0.007876)) (bigrat (from-string "1") (from-string "1"))) (egglog_exp_param_eq_domain_exp (polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) (polynomial (map-insert (map-insert (map-empty) (map-empty) 2.0) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) -1.0)) (bigrat (from-string "1") (from-string "1"))) 1.0))) (bigrat (from-string "1") (from-string "1"))) 1.0))
(Num___init__ 0.0)
(print-size )
(ruleset egglog.exp.param_eq.pipeline.shared_analysis_rules)
(rewrite (egglog_exp_param_eq_domain_exp (Num___init__ _a)) (Num___init__ (exp _a)) :subsume :ruleset egglog.exp.param_eq.pipeline.shared_analysis_rules)
(constructor egglog_exp_param_eq_domain_log (Num) Num)
(rewrite (egglog_exp_param_eq_domain_log (Num___init__ _a)) (Num___init__ (log _a)) :subsume :when ((> _a 0.0)) :ruleset egglog.exp.param_eq.pipeline.shared_analysis_rules)
(rule ((egglog_exp_param_eq_domain_log (Num___init__ _a))
       (<= _a 0.0))
      ((panic "Log of non-positive number"))
        :ruleset egglog.exp.param_eq.pipeline.shared_analysis_rules )
(constructor Num___abs__ (Num) Num)
(rewrite (Num___abs__ (Num___init__ _a)) (Num___init__ (abs _a)) :subsume :ruleset egglog.exp.param_eq.pipeline.shared_analysis_rules)
(ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(sort Map[Num,f64] (Map Num f64))
(sort UnstableFn[f64,f64,f64] (UnstableFn (f64 f64) f64))
(primitive _lambda_0 (f64 f64) f64 (collapse-floats-with-tol _0 _1 0.000001))
(function %CONSTS () Map[Num,f64] :merge (map-merge-with (unstable-fn "_lambda_0") old new))
(sort Map[Num,Map[Num,BigRat]] (Map Num Map[Num,BigRat]))
(sort UnstableFn[Map[Num,BigRat],Map[Num,BigRat],Map[Num,BigRat]] (UnstableFn (Map[Num,BigRat] Map[Num,BigRat]) Map[Num,BigRat]))
(primitive _lambda_1 (Map[Num,BigRat] Map[Num,BigRat]) Map[Num,BigRat] _0)
(function %SOLE_MONOMIALS () Map[Num,Map[Num,BigRat]] :merge (map-merge-with (unstable-fn "_lambda_1") old new))
(rule ()
      ((set (%CONSTS) (map-empty))
       (set (%SOLE_MONOMIALS) (map-empty)))
        :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules )
(rule ((= _n (Num___init__ _a)))
      ((set (%CONSTS) (map-insert (map-empty) _n _a)))
        :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules )
(rule ((= (polynomial _poly) _n)
       (= (map-length _poly) 1)
       (= _key (map-pick-key _poly)))
      ((set (%SOLE_MONOMIALS) (map-insert (map-empty) _n (map-insert _key (Num___init__ (map-get _poly _key)) (bigrat (bigint 1) (bigint 1))))))
        :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules )
(sort UnstableFn[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64],Map[Num,BigRat],f64] (UnstableFn (Map[Map[Num,BigRat],f64] Map[Num,BigRat] f64) Map[Map[Num,BigRat],f64]))
(sort Pair[Map[Num,BigRat],f64] (Pair Map[Num,BigRat] f64))
(sort UnstableFn[Pair[Map[Num,BigRat],f64],Pair[Map[Num,BigRat],f64],Num,BigRat] (UnstableFn (Pair[Map[Num,BigRat],f64] Num BigRat) Pair[Map[Num,BigRat],f64]))
(sort Maybe[Unit] (Maybe Unit))
(sort UnstableFn[Unit] (UnstableFn () Unit))
(primitive _lambda_4 BigRat Unit (!= _0 (bigrat (bigint 0) (bigint 1))))
(sort UnstableFn[Pair[Map[Num,BigRat],f64],Unit] (UnstableFn (Unit) Pair[Map[Num,BigRat],f64]))
(sort Maybe[f64] (Maybe f64))
(sort UnstableFn[f64] (UnstableFn () f64))
(primitive _lambda_6 (Num Map[Num,f64]) f64 (map-get _1 _0))
(sort UnstableFn[Pair[Map[Num,BigRat],f64],f64] (UnstableFn (f64) Pair[Map[Num,BigRat],f64]))
(sort UnstableFn[f64,f64] (UnstableFn (f64) f64))
(primitive _lambda_8 (f64 BigRat f64) f64 (* _2 (bigrat-pow-const-value _0 _1)))
(primitive _lambda_7 (Pair[Map[Num,BigRat],f64] BigRat f64) Pair[Map[Num,BigRat],f64] (unstable-pair-map-right _0 (unstable-fn "_lambda_8" _2 _1)))
(sort UnstableFn[Map[Num,BigRat],Map[Num,BigRat]] (UnstableFn (Map[Num,BigRat]) Map[Num,BigRat]))
(primitive _lambda_9 (Num BigRat Map[Num,BigRat]) Map[Num,BigRat] (map-insert _2 _0 _1))
(primitive _lambda_5 (Num Pair[Map[Num,BigRat],f64] Map[Num,f64] BigRat Unit) Pair[Map[Num,BigRat],f64] (unstable-maybe-match (unstable-catch (unstable-fn "_lambda_6" _0 _2)) (unstable-fn "_lambda_7" _1 _3) (unstable-pair-map-left _1 (unstable-fn "_lambda_9" _0 _3))))
(primitive _lambda_3 (Map[Num,f64] Pair[Map[Num,BigRat],f64] Num BigRat) Pair[Map[Num,BigRat],f64] (unstable-maybe-match (unstable-catch (unstable-fn "_lambda_4" _3)) (unstable-fn "_lambda_5" _2 _1 _0 _3) _1))
(sort UnstableFn[Map[Map[Num,BigRat],f64],Map[Num,BigRat],f64] (UnstableFn (Map[Num,BigRat] f64) Map[Map[Num,BigRat],f64]))
(primitive _lambda_11 (Map[Num,BigRat] Map[Map[Num,BigRat],f64]) f64 (map-get _1 _0))
(primitive _lambda_10 (Map[Map[Num,BigRat],f64] Map[Num,BigRat] f64) Map[Map[Num,BigRat],f64] (map-insert _0 _1 (+ _2 (maybe-unwrap-or (unstable-catch (unstable-fn "_lambda_11" _1 _0)) 0.0))))
(primitive _lambda_2 (Map[Num,f64] Map[Map[Num,BigRat],f64] Map[Num,BigRat] f64) Map[Map[Num,BigRat],f64] (unstable-pair-match (map-fold-kv (unstable-fn "_lambda_3" _0) (pair (map-empty) _3) _2) (unstable-fn "_lambda_10" _1)))
(rewrite (polynomial _poly) (polynomial _poly1) :subsume :when ((= _consts (%CONSTS)) (= _poly1 (map-fold-kv (unstable-fn "_lambda_2" _consts) (map-empty) _poly)) (!= _poly _poly1)) :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(rewrite (polynomial _poly) (Num___init__ (map-get _poly (map-empty))) :subsume :when ((= (map-length _poly) 1) (= (map-empty) (map-pick-key _poly))) :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(rewrite (polynomial _poly) (polynomial _poly1) :subsume :when ((= _poly1 (map-drop-zero-values _poly)) (!= _poly _poly1)) :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(rewrite (polynomial (map-empty)) (Num___init__ 0.0) :subsume :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(rewrite (polynomial _poly) _n :subsume :when ((= (map-length _poly) 1) (= _key (map-pick-key _poly)) (= (map-get _poly _key) 1.0) (= (map-length _key) 1) (= _n (map-pick-key _key)) (= (map-get _key _n) (bigrat (bigint 1) (bigint 1)))) :ruleset egglog.exp.param_eq.pipeline.container_analysis_rules)
(unstable-combined-ruleset _combined_ruleset_1 egglog.exp.param_eq.pipeline.shared_analysis_rules egglog.exp.param_eq.pipeline.container_analysis_rules)
(run-schedule (saturate (run _combined_ruleset_1)))
(ruleset egglog.exp.param_eq.pipeline.shared_fun_rules)
(rewrite (egglog_exp_param_eq_domain_log (egglog_exp_param_eq_domain_exp _x)) _x :ruleset egglog.exp.param_eq.pipeline.shared_fun_rules)
(rewrite (egglog_exp_param_eq_domain_log (egglog_exp_param_eq_domain_log _x)) _x :ruleset egglog.exp.param_eq.pipeline.shared_fun_rules)
(ruleset egglog.exp.param_eq.pipeline.shared_extra_rules)
(rewrite (egglog_exp_param_eq_domain_log (Num___abs__ (egglog_exp_param_eq_domain_exp _x))) _x :ruleset egglog.exp.param_eq.pipeline.shared_extra_rules)
(unstable-combined-ruleset _combined_ruleset_2 egglog.exp.param_eq.pipeline.shared_fun_rules egglog.exp.param_eq.pipeline.shared_extra_rules)
(ruleset egglog.exp.param_eq.pipeline.container_basic_rules)
(sort UnstableFn[Unit,Map[Num,BigRat],f64] (UnstableFn (Map[Num,BigRat] f64) Unit))
(primitive _lambda_12 (Map[Num,BigRat] f64) Unit (!= _1 1.0))
(primitive _lambda_13 (Map[Num,BigRat] f64) Unit (!= _0 (map-empty)))
(sort UnstableFn[f64,Map[Num,BigRat],f64] (UnstableFn (Map[Num,BigRat] f64) f64))
(primitive _lambda_14 (f64 Map[Num,BigRat] f64) f64 (/ _2 _0))
(rewrite (polynomial _poly) (polynomial (map-insert (map-empty) (map-insert (map-empty) (polynomial _poly1) (bigrat (bigint 1) (bigint 1))) _coef)) :when ((> (map-length _poly) 1) (= _poly2 (map-filter-kv (unstable-fn "_lambda_12") (map-filter-kv (unstable-fn "_lambda_13") _poly))) (= _coef (map-get _poly2 (map-pick-key _poly2))) (= _poly1 (map-map-values (unstable-fn "_lambda_14" _coef) _poly))) :ruleset egglog.exp.param_eq.pipeline.container_basic_rules)
(sort UnstableFn[Map[Num,BigRat],Map[Num,BigRat],Num,BigRat] (UnstableFn (Map[Num,BigRat] Num BigRat) Map[Num,BigRat]))
(sort Maybe[Map[Num,BigRat]] (Maybe Map[Num,BigRat]))
(sort UnstableFn[Map[Num,BigRat]] (UnstableFn () Map[Num,BigRat]))
(sort UnstableFn[BigRat,Num,BigRat] (UnstableFn (Num BigRat) BigRat))
(primitive _lambda_18 (BigRat Num BigRat) BigRat (* _2 (bigrat (bigint (to-i64 _0)) (bigint 1))))
(primitive _lambda_17 (Map[Num,Map[Num,BigRat]] Num BigRat) Map[Num,BigRat] (map-map-values (unstable-fn "_lambda_18" _2) (map-get _0 _1)))
(sort UnstableFn[BigRat,BigRat,BigRat] (UnstableFn (BigRat BigRat) BigRat))
(primitive _lambda_20 (BigRat BigRat) BigRat (+ _0 _1))
(primitive _lambda_19 (Map[Num,BigRat] Map[Num,BigRat]) Map[Num,BigRat] (map-merge-with (unstable-fn "_lambda_20") _1 _0))
(primitive _lambda_16 (Map[Num,Map[Num,BigRat]] Map[Num,BigRat] Num BigRat) Map[Num,BigRat] (unstable-maybe-match (unstable-catch (unstable-fn "_lambda_17" _0 _2 _3)) (unstable-fn "_lambda_19" _1) (map-insert _1 _2 _3)))
(primitive _lambda_15 (Map[Num,Map[Num,BigRat]] Map[Map[Num,BigRat],f64] Map[Num,BigRat] f64) Map[Map[Num,BigRat],f64] (map-insert _1 (map-fold-kv (unstable-fn "_lambda_16" _0) (map-empty) _2) _3))
(rewrite (polynomial _poly) (polynomial _poly1) :when ((= _sole_monomials (%SOLE_MONOMIALS)) (= _poly1 (map-fold-kv (unstable-fn "_lambda_15" _sole_monomials) (map-empty) _poly))) :ruleset egglog.exp.param_eq.pipeline.container_basic_rules)
(sort Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] (Pair Map[Map[Num,BigRat],f64] Map[Map[Num,BigRat],f64]))
(sort MultiSet[Num] (MultiSet Num))
(sort UnstableFn[MultiSet[Num],MultiSet[Num],Map[Num,BigRat],f64] (UnstableFn (MultiSet[Num] Map[Num,BigRat] f64) MultiSet[Num]))
(primitive _lambda_21 (MultiSet[Num] Map[Num,BigRat] f64) MultiSet[Num] (multiset-sum _0 (map-keys _1)))
(sort UnstableFn[BigRat,BigRat,Map[Num,BigRat],f64] (UnstableFn (BigRat Map[Num,BigRat] f64) BigRat))
(primitive _lambda_23 (Map[Num,BigRat] Num BigRat) Unit (< (map-get _0 _1) _2))
(sort UnstableFn[BigRat,Unit] (UnstableFn (Unit) BigRat))
(primitive _lambda_24 (Map[Num,BigRat] Num Unit) BigRat (map-get _0 _1))
(primitive _lambda_22 (Num BigRat Map[Num,BigRat] f64) BigRat (unstable-maybe-match (unstable-catch (unstable-fn "_lambda_23" _2 _0 _1)) (unstable-fn "_lambda_24" _2 _0) _1))
(sort UnstableFn[Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]],Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]],Map[Num,BigRat],f64] (UnstableFn (Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] Map[Num,BigRat] f64) Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]]))
(sort Maybe[BigRat] (Maybe BigRat))
(sort UnstableFn[BigRat] (UnstableFn () BigRat))
(primitive _lambda_26 (Map[Num,BigRat] Num) BigRat (map-get _0 _1))
(sort UnstableFn[Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]],BigRat] (UnstableFn (BigRat) Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]]))
(sort UnstableFn[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] (UnstableFn (Map[Map[Num,BigRat],f64]) Map[Map[Num,BigRat],f64]))
(primitive _lambda_28 (Map[Num,BigRat] BigRat BigRat f64 Num Map[Map[Num,BigRat],f64]) Map[Map[Num,BigRat],f64] (map-insert _5 (map-insert _0 _4 (- _2 _1)) _3))
(primitive _lambda_27 (Map[Num,BigRat] Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] BigRat f64 Num BigRat) Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] (unstable-pair-map-left _1 (unstable-fn "_lambda_28" _0 _2 _5 _3 _4)))
(primitive _lambda_29 (Map[Num,BigRat] f64 Map[Map[Num,BigRat],f64]) Map[Map[Num,BigRat],f64] (map-insert _2 _0 _1))
(primitive _lambda_25 (Num BigRat Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] Map[Num,BigRat] f64) Pair[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64]] (unstable-maybe-match (unstable-catch (unstable-fn "_lambda_26" _3 _0)) (unstable-fn "_lambda_27" _3 _2 _1 _4 _0) (unstable-pair-map-right _2 (unstable-fn "_lambda_29" _3 _4))))
(rewrite (polynomial _poly) (polynomial (map-insert (pair-right _poly_pair) (map-insert (map-insert (map-empty) _n _exp) (polynomial (pair-left _poly_pair)) (bigrat (bigint 1) (bigint 1))) 1.0)) :when ((= _counts (map-fold-kv (unstable-fn "_lambda_21") (multiset-of) _poly)) (= _n (multiset-pick-max _counts)) (> (multiset-count _counts _n) 1) (= _exp (map-fold-kv (unstable-fn "_lambda_22" _n) (bigrat (bigint 9223372036854775807) (bigint 1)) _poly)) (= _poly_pair (map-fold-kv (unstable-fn "_lambda_25" _n _exp) (pair (map-empty) (map-empty)) _poly))) :ruleset egglog.exp.param_eq.pipeline.container_basic_rules)
(primitive _lambda_30 (f64 f64) f64 (+ _0 _1))
(rewrite (polynomial _poly) (polynomial (map-insert (map-empty) (map-insert (map-empty) (polynomial (map-merge-with (unstable-fn "_lambda_30") _poly1 (map-insert (map-empty) (map-empty) (/ _coef (map-get _poly _mono))))) (bigrat (bigint 1) (bigint 1))) (map-get _poly _mono))) :when ((= (map-length _poly) 2) (= _coef (map-get _poly (map-empty))) (= (map-pick-key (map-remove _poly (map-empty))) _mono) (= (map-length _mono) 1) (= (map-pick-key _mono) _n) (= (map-get _mono _n) (bigrat (bigint 1) (bigint 1))) (= _n (polynomial _poly1))) :ruleset egglog.exp.param_eq.pipeline.container_basic_rules)
(unstable-combined-ruleset _combined_ruleset_6 _combined_ruleset_2 egglog.exp.param_eq.pipeline.container_basic_rules)
(ruleset egglog.exp.param_eq.pipeline.container_fun_rules)
(sort UnstableFn[Map[Map[Num,BigRat],f64],Map[Map[Num,BigRat],f64],Num,BigRat] (UnstableFn (Map[Map[Num,BigRat],f64] Num BigRat) Map[Map[Num,BigRat],f64]))
(primitive _lambda_31 (Map[Map[Num,BigRat],f64] Num BigRat) Map[Map[Num,BigRat],f64] (map-insert _0 (map-insert (map-empty) (egglog_exp_param_eq_domain_log _1) (bigrat (bigint 1) (bigint 1))) (to-f64 _2)))
(rewrite (egglog_exp_param_eq_domain_log (polynomial _poly)) (polynomial _poly1) :when ((= (map-length _poly) 1) (= _m (map-pick-key _poly)) (> (map-get _poly _m) 0.0) (= _poly1 (map-fold-kv (unstable-fn "_lambda_31") (map-insert (map-empty) (map-empty) (log (map-get _poly _m))) _m))) :ruleset egglog.exp.param_eq.pipeline.container_fun_rules)
(unstable-combined-ruleset _combined_ruleset_7 _combined_ruleset_6 egglog.exp.param_eq.pipeline.container_fun_rules)
(ruleset egglog.exp.param_eq.pipeline.container_extra_rules)
(unstable-combined-ruleset _combined_ruleset_8 _combined_ruleset_7 egglog.exp.param_eq.pipeline.container_extra_rules)
(let-scheduler _persistent_scheduler_c34b0731098d4358a4be4bcfb1c0304f (back-off-fresh :match-limit 1000 :ban-length 30))
(run-schedule (run-with _persistent_scheduler_c34b0731098d4358a4be4bcfb1c0304f _combined_ruleset_8))
(run-schedule (saturate (run _combined_ruleset_1)))
(print-size )
(run-schedule (run-with _persistent_scheduler_c34b0731098d4358a4be4bcfb1c0304f _combined_ruleset_8))
(run-schedule (saturate (run _combined_ruleset_1)))
(print-size )
(run-schedule (run-with _persistent_scheduler_c34b0731098d4358a4be4bcfb1c0304f _combined_ruleset_8))
(run-schedule (saturate (run _combined_ruleset_1)))
(print-size )
(run-schedule (run-with _persistent_scheduler_c34b0731098d4358a4be4bcfb1c0304f _combined_ruleset_8))
(run-schedule (saturate (run _combined_ruleset_1)))
(print-size )
(extract (polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (polynomial (map-insert (map-empty) (map-insert (map-empty) (polynomial (map-insert (map-insert (map-insert (map-insert (map-insert (map-empty) (map-empty) -6.619000000000001) (map-insert (map-empty) $_0 (bigrat (from-string "1") (from-string "1"))) -15.509) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) 1.0) (map-insert (map-empty) (egglog_exp_param_eq_domain_exp $_0) (bigrat (from-string "1") (from-string "1"))) 1.0) (map-insert (map-empty) (egglog_exp_param_eq_domain_exp (polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) (polynomial (map-insert (map-insert (map-empty) (map-empty) -2.0) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) 1.0)) (bigrat (from-string "1") (from-string "1"))) 1.0))) (bigrat (from-string "1") (from-string "1"))) 0.30129507364144237)) (bigrat (from-string "1") (from-string "1"))) -0.007876)) (bigrat (from-string "1") (from-string "1"))) (egglog_exp_param_eq_domain_exp (polynomial (map-insert (map-empty) (map-insert (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) (polynomial (map-insert (map-insert (map-empty) (map-empty) 2.0) (map-insert (map-empty) (Num_var "x0") (bigrat (from-string "1") (from-string "1"))) -1.0)) (bigrat (from-string "1") (from-string "1"))) 1.0))) (bigrat (from-string "1") (from-string "1"))) 1.0)) 0)