Struct EGraph 

pub struct EGraph {
    pub equalities: Equalities,
    /* private fields */
}

Fields

equalities: Equalities

Implementations

impl EGraph

pub fn get_blame( &self, tidx: TermIdx, inst: Option<(InstIdx, FxHashSet<EqTransIdx>)>, terms: &Terms, stack: &Stack, ) -> ENodeBlame

pub fn new_enode( &mut self, blame: ENodeBlame, term: TermIdx, z3_generation: NonMaxU32, stack: &Stack, ) -> Result<ENodeIdx>

pub fn get_enode(&mut self, term: TermIdx, stack: &Stack) -> Result<ENodeIdx>

pub fn get_enode_imm(&self, term: TermIdx, stack: &Stack) -> Option<ENodeIdx>

pub fn get_given(&self, from: ENodeIdx, to: ENodeIdx) -> Option<EqGivenIdx>

pub fn new_given_equality( &mut self, from: ENodeIdx, expl: EqualityExpl, stack: &Stack, ) -> Result<()>

pub fn new_trans_equality( &mut self, from: ENodeIdx, to: ENodeIdx, stack: &Stack, mismatch: TransEqAllowed, ) -> Result<Result<EqTransIdx, ENodeIdx>>

pub fn check_eq(&self, from: ENodeIdx, to: ENodeIdx, stack: &Stack) -> bool

pub fn path_to_root( &self, from: ENodeIdx, root: Option<ENodeIdx>, stack: &Stack, ) -> Result<(Option<ENodeIdx>, Vec<ENodeIdx>)>

impl EGraph

pub fn insert_tte( &mut self, term: TermIdx, enode: ENodeIdx, stack: &Stack, ) -> Result<()>

Trait Implementations

impl Debug for EGraph

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for EGraph

fn default() -> EGraph

Returns the “default value” for a type.

impl Index<ENodeIdx> for EGraph

type Output = ENode

The returned type after indexing.

fn index(&self, idx: ENodeIdx) -> &Self::Output

Performs the indexing (container[index]) operation.