Struct RawInstGraph

pub struct RawInstGraph {
    pub graph: DiGraph<Node, EdgeKind, RawIx>,
    /* private fields */
}

Fields

graph: DiGraph<Node, EdgeKind, RawIx>

Implementations

impl RawInstGraph

pub fn reset_disabled_to_raw( &mut self, f: impl Fn(RawNodeIndex, &RawInstGraph) -> bool, ) -> (bool, bool)

Updates which nodes are disabled based on the predicate f. The hidden of all non-disabled nodes is reset to false so any filters will need to be reapplied. It returns two booleans: the first indicates if any state was modified, the second indicates if any node was enabled/disabled.

Analyses should be reapplied after this function is called! (unless the second boolean is false)

impl RawInstGraph

pub fn reset_visibility_to(&mut self, hidden: bool) -> bool

pub fn can_set_visibility(&self, node: &Node, hidden: bool) -> bool

pub fn set_visibility<I: IndexesInstGraph>( &mut self, node: I, hidden: bool, ) -> bool

pub fn keep_first_n( &mut self, nodes: impl Iterator<Item = RawNodeIndex>, n: usize, ) -> bool

pub fn set_visibility_when( &mut self, hidden: bool, p: impl FnMut(&Self, RawNodeIndex, &Node) -> bool, ) -> bool

When predicate p evaluates to true the visibility of the corresponding node is set to hidden. Use this when hiding nodes and the predicate is expensive as it avoids calling the predicate a lot more than set_visibility_all.

pub fn set_visibility_all( &mut self, p: impl FnMut(&Self, RawNodeIndex, &Node) -> Option<bool>, ) -> bool

When predicate p evaluates to Some the visibility of the corresponding node is set to hidden (true) or visible (false).

pub fn set_visibility_many<I: IndexesInstGraph>( &mut self, hidden: bool, nodes: impl Iterator<Item = I>, ) -> bool

pub fn path_to_root_graph( &self, longest: bool, ) -> EdgeFiltered<Reversed<&DiGraph<Node, EdgeKind, RawIx>>, impl Fn(ReversedEdgeReference<EdgeReference<'_, EdgeKind, RawIx>>) -> bool + '_>

A graph with edges that aren’t part of any longest/shortest path to a root filtered out. The edges are also reversed, so the graph can be walked from any node to find the longest/shortest path to a root.

pub fn path_to_leaf_graph( &self, longest: bool, ) -> EdgeFiltered<&DiGraph<Node, EdgeKind, RawIx>, impl Fn(EdgeReference<'_, EdgeKind, RawIx>) -> bool + '_>

A graph with edges that aren’t part of any longest/shortest path to a leaf filtered out. The graph can be walked from any node to find the longest/shortest path to a leaf.

pub fn show_longest_path_through( &mut self, node: RawNodeIndex, ) -> (bool, Vec<RawNodeIndex>)

impl RawInstGraph

pub fn new(parser: &Z3Parser) -> Result<Self>

pub fn index(&self, kind: NodeKind) -> RawNodeIndex

pub fn rev(&self) -> Reversed<&DiGraph<Node, EdgeKind, RawIx>>

pub fn visible_nodes(&self) -> usize

pub fn node_indices(&self) -> impl Iterator<Item = RawNodeIndex>

pub fn neighbors<'a>( &'a self, node: RawNodeIndex, reach: &'a TiVec<RawNodeIndex, ReachNonDisabled>, ) -> Neighbors<'a>

Similar to self.graph.neighbors but will walk through disabled nodes.

Note: Iterating the neighbors is not a O(1) operation.

pub fn neighbors_directed<'a>( &'a self, node: RawNodeIndex, dir: Direction, reach: &'a TiVec<RawNodeIndex, ReachNonDisabled>, ) -> Neighbors<'a>

Similar to self.graph.neighbors_directed but will walk through disabled nodes.

Note: Iterating the neighbors is not a O(1) operation.

pub fn inst_to_raw_idx(&self) -> impl Fn(InstIdx) -> RawNodeIndex

pub fn hypotheses(&self, parser: &Z3Parser, proof: ProofIdx) -> Vec<ProofIdx>

impl RawInstGraph

pub fn partition(&mut self) -> Result<Subgraphs>

Trait Implementations

impl Debug for RawInstGraph

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

Formats the value using the given formatter.

impl Index<RawEdgeIndex> for RawInstGraph

type Output = EdgeKind

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl<T: IndexesInstGraph> Index<T> for RawInstGraph

type Output = Node

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl<T: IndexesInstGraph> IndexMut<T> for RawInstGraph

fn index_mut(&mut self, index: T) -> &mut Self::Output

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