Struct EGraph 

pub struct EGraph { /* private fields */ }

The state associated with an egglog program.

Implementations

impl EGraph

pub fn new_rule(&mut self, desc: &str, seminaive: bool) -> RuleBuilder<'_>

Add a rewrite rule for this EGraph using a RuleBuilder. If you aren’t sure, use egraph.new_rule("", true).

pub fn free_rule(&mut self, id: RuleId)

Remove a rewrite rule from this EGraph.

impl EGraph

pub fn with_tracing() -> EGraph

Create a new EGraph with tracing (aka ‘proofs’) enabled.

Execution of queries against a tracing-enabled EGraph will be slower, but will annotate the egraph with annotations that can explain how rows came to appear.

pub fn base_values_mut(&mut self) -> &mut BaseValues

Get a mutable reference to the underlying table of base values for this EGraph.

pub fn container_values_mut(&mut self) -> &mut ContainerValues

Get a mutable reference to the underlying table of containers for this EGraph.

pub fn container_values(&self) -> &ContainerValues

Get a reference to the underlying table of containers for this EGraph.

pub fn get_container_value<C: ContainerValue>(&mut self, val: C) -> Value

Intern the given container value into the EGraph.

pub fn register_container_ty<C: ContainerValue>(&mut self)

Register the given ContainerValue type with this EGraph.

The given container will use the EGraph’s union-find to manage rebuilding and the merging of containers with a common id.

pub fn base_values(&self) -> &BaseValues

Get a reference to the underlying table of base values for this EGraph.

pub fn base_value_constant<T>(&self, x: T) -> QueryEntry

where T: BaseValue,

Create a QueryEntry for a base value.

pub fn register_external_func( &mut self, func: impl ExternalFunction + 'static, ) -> ExternalFunctionId

pub fn free_external_func(&mut self, func: ExternalFunctionId)

pub fn fresh_id(&mut self) -> Value

Generate a fresh id.

pub fn get_canon_repr(&self, val: Value, ty: ColumnTy) -> Value

Get the canonical representation for val based on type.

For ColumnTy::Id, it looks up the union find; otherwise, it returns the value itself.

pub fn add_values( &mut self, values: impl IntoIterator<Item = (FunctionId, Vec<Value>)>, )

Load the given values into the database.

Panics

This method panics if the values do not match the arity of the function.

NB: this is not an efficient interface for bulk loading. We should add one that allows us to pass through a series of RowBuffers before incrementing the timestamp.

pub fn add_term( &mut self, func: FunctionId, inputs: &[Value], desc: &str, ) -> Value

A term-oriented means of adding data to the database: hand back a “term id” for the given function and keys for the function. Proofs for this term will include desc.

Panics

This method panics if the values do not match the arity of the function.

pub fn lookup_id(&self, func: FunctionId, key: &[Value]) -> Option<Value>

Lookup the id associated with a function func and the given arguments (key).

pub fn add_values_with_desc( &mut self, desc: &str, values: impl IntoIterator<Item = (FunctionId, Vec<Value>)>, )

Load the given values into the database. If tracing is enabled, the proof rows will be tagged with “desc” as their proof.

Panics

This method panics if the values do not match the arity of the function.

NB: this is not an efficient interface for bulk loading. We should add one that allows us to pass through a series of RowBuffers before incrementing the timestamp.

pub fn approx_table_size(&self, table: FunctionId) -> usize

pub fn table_size(&self, table: FunctionId) -> usize

pub fn explain_term( &mut self, id: Value, store: &mut ProofStore, ) -> Result<TermProofId>

Generate a proof explaining why a given term is in the database.

Errors

This method will return an error if tracing is not enabled, or if the row is not in the database.

Panics

This method may panic if key does not match the arity of the function, or is otherwise malformed.

pub fn explain_terms_equal( &mut self, id1: Value, id2: Value, store: &mut ProofStore, ) -> Result<EqProofId>

Generate a proof explaining why the term corresponding to id1 is equal to that corresponding to id2.

Errors

This method will return an error if tracing is not enabled, if the row is not in the database, or if the terms themselves are not equal.

pub fn for_each(&self, table: FunctionId, f: impl FnMut(FunctionRow<'_>))

Read the contents of the given function.

The callback f is called with each row and its subsumption status.

pub fn for_each_while( &self, table: FunctionId, f: impl FnMut(FunctionRow<'_>) -> bool, )

Iterate over the rows of a function table, calling f on each row. If f returns false the function returns early and stops reading rows from the table.

pub fn dump_debug_info(&self)

A basic method for dumping the state of the database to log::info!.

For large tables, this is unlikely to give particularly useful output.

pub fn add_table(&mut self, config: FunctionConfig) -> FunctionId

Register a function in this EGraph.

pub fn run_rules(&mut self, rules: &[RuleId]) -> Result<IterationReport>

Run the given rules, returning whether the database changed.

If the given rules are malformed, this method can return an error.

pub fn with_execution_state<R>( &self, f: impl FnOnce(&mut ExecutionState<'_>) -> R, ) -> R

Gives the user a handle to the underlying ExecutionState. Useful for staging updates to the database.

The staged updates are not immediately reflected in the EGraph, so you may want to manually flush the updates using EGraph::flush_updates.

pub fn flush_updates(&mut self) -> bool

Flush the pending update buffers to the EGraph. Returns true if the database is updated.

impl EGraph

pub fn new_panic(&mut self, message: String) -> ExternalFunctionId

Create a new ExternalFunction that panics with the given message.

pub fn new_panic_lazy( &mut self, message: impl FnOnce() -> String + Send + 'static, ) -> ExternalFunctionId

Trait Implementations

impl Clone for EGraph

fn clone(&self) -> EGraph

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Default for EGraph

fn default() -> Self

Returns the “default value” for a type.