Struct chalk_recursive::fixed_point::search_graph::SearchGraph

pub(super) struct SearchGraph<K, V>
where
    K: Hash + Eq + Debug + Clone,
    V: Debug + Clone,
{
    indices: FxHashMap<K, DepthFirstNumber>,
    nodes: Vec<Node<K, V>>,
}

The “search graph” stores in-progress goals that are still being solved.

Fields

indices: FxHashMap<K, DepthFirstNumber>

nodes: Vec<Node<K, V>>

Implementations

impl<K, V> SearchGraph<K, V>

where K: Hash + Eq + Debug + Clone, V: Debug + Clone,

pub(crate) fn new() -> Self

pub(crate) fn lookup(&self, goal: &K) -> Option<DepthFirstNumber>

pub(crate) fn insert( &mut self, goal: &K, stack_depth: StackDepth, solution: V ) -> DepthFirstNumber

Insert a new search node in the tree. The node will be in the initial state for a search node:

• stack depth as given
• links set to its own DFN
• solution is initially an identity substitution for coinductive goals or NoSolution for other goals

pub(crate) fn rollback_to(&mut self, dfn: DepthFirstNumber)

Clears all nodes with a depth-first number greater than or equal dfn.

pub(crate) fn move_to_cache( &mut self, dfn: DepthFirstNumber, cache: &Cache<K, V> )

Removes all nodes with a depth-first-number greater than or equal to dfn, adding their final solutions into the cache.

Trait Implementations

impl<K, V> Index<DepthFirstNumber> for SearchGraph<K, V>

where K: Hash + Eq + Debug + Clone, V: Debug + Clone,

type Output = Node<K, V>

The returned type after indexing.

fn index(&self, table_index: DepthFirstNumber) -> &Node<K, V>

Performs the indexing (container[index]) operation.

impl<K, V> IndexMut<DepthFirstNumber> for SearchGraph<K, V>

where K: Hash + Eq + Debug + Clone, V: Debug + Clone,

fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node<K, V>

Performs the mutable indexing (container[index]) operation.