Struct CodeTree 

pub struct CodeTree { /* private fields */ }

E-matching code tree for multi-pattern matching.

Implementations

impl CodeTree

pub fn new() -> Self

Create a new code tree.

pub fn stats(&self) -> &CodeTreeStats

Get statistics.

pub fn reset_stats(&mut self)

Reset statistics.

pub fn add_patterns( &mut self, quantifier: TermId, patterns: &[Vec<TermId>], var_mapping: &FxHashMap<Spur, PatternVar>, tm: &TermManager, )

Compile and add patterns from a quantified formula.

Arguments

• quantifier - The quantified formula term ID
• patterns - List of pattern lists (multi-patterns)
• var_mapping - Maps bound variable names to pattern variable IDs
• tm - Term manager for accessing term structure

pub fn add_ground_term(&mut self, term: TermId, tm: &TermManager)

Add a ground term to the database.

This term will be considered for matching against patterns.

pub fn find_matches(&mut self, tm: &TermManager) -> Vec<Match>

Find all matches for the indexed patterns against the ground terms.

Returns a list of matches (quantifier, pattern_index, substitution).

pub fn clear_ground_terms(&mut self)

Clear all ground terms and reset matching state.

pub fn remove_quantifier(&mut self, quantifier: TermId)

Remove patterns associated with a quantifier.

Trait Implementations

impl Default for CodeTree

fn default() -> Self

Returns the “default value” for a type.