Struct InstGraph 

pub struct InstGraph {
    pub raw: RawInstGraph,
    pub subgraphs: Subgraphs,
    pub analysis: Analysis,
}

Fields

raw: RawInstGraph

subgraphs: Subgraphs

analysis: Analysis

Implementations

impl InstGraph

pub fn initialise_cdcl(&mut self, parser: &Z3Parser)

impl InstGraph

pub fn search_matching_loops(&mut self, parser: &mut Z3Parser) -> &MlData

Search for matching loops in the graph.

pub fn found_matching_loops(&self) -> Option<(usize, usize)>

pub fn found_sure_matching_loop_graphs(&self) -> Option<usize>

pub fn quants_per_matching_loop( &self, ) -> Option<impl Iterator<Item = QuantPat> + '_>

pub fn nth_matching_loop_graph(&self, n: usize) -> Option<&MatchingLoop>

impl InstGraph

pub fn topo_analysis<I: TopoAnalysis<FORWARD, SKIP_DISABLED>, const FORWARD: bool, const SKIP_DISABLED: bool>( &self, analysis: &mut I, ) -> TiVec<RawNodeIndex, I::Value>

pub fn initialise_collect<I: CollectInitialiser<FORWARD, SKIP_DISABLED, ID>, const FORWARD: bool, const SKIP_DISABLED: bool, const ID: u8>( &mut self, initialiser: I, parser: &Z3Parser, )

pub fn initialise_transfer<I: TransferInitialiser<FORWARD, ID>, const FORWARD: bool, const ID: u8>( &mut self, initialiser: I, parser: &Z3Parser, )

impl InstGraph

pub fn initialise_first(&mut self, parser: &Z3Parser, n: usize)

pub fn initialise_default(&mut self, parser: &Z3Parser, n: usize)

pub fn analyse(&mut self, n: usize)

impl InstGraph

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

Updates which nodes are disabled based on the predicate f. The hidden of all nodes is reset to false so any filters will need to be reapplied. The default analyses are also reapplied.

pub fn disabled_nodes(&self) -> impl Iterator<Item = RawNodeIndex> + '_

impl InstGraph

pub fn keep_first_n_cost(&mut self, n: usize) -> bool

pub fn keep_first_n_children(&mut self, n: usize) -> bool

pub fn keep_first_n_fwd_depth_min(&mut self, n: usize) -> bool

impl InstGraph

pub fn to_visible(&self) -> VisibleInstGraph

impl InstGraph

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

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

pub fn visible_unchanged(&self, old: &VisibleInstGraph) -> bool

Trait Implementations

impl Debug for InstGraph

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

Formats the value using the given formatter.