Initialiser

Trait Initialiser 

Source
pub trait Initialiser<const FORWARD: bool, const ID: u8> {
    type Value: Debug;

    // Required methods
    fn direction() -> Direction;
    fn base(&mut self, node: &Node, parser: &Z3Parser) -> Self::Value;
    fn assign(&mut self, node: &mut Node, value: Self::Value);

    // Provided method
    fn reset(&mut self) { ... }
}
Expand description

FORWARD: Do a forward or reverse topological walk?

Required Associated Types§

Source

type Value: Debug

The value that is being initialised.

Required Methods§

Source

fn direction() -> Direction

Will I get to see the incoming parents or outgoing children?

Source

fn base(&mut self, node: &Node, parser: &Z3Parser) -> Self::Value

The starting value for a node.

Source

fn assign(&mut self, node: &mut Node, value: Self::Value)

Provided Methods§

Source

fn reset(&mut self)

Called between initialisations of different subgraphs.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§

Source§

impl<C: CostInitialiser<FORWARD>, const FORWARD: bool> Initialiser<FORWARD, 0> for C

Source§

impl<C: DepthInitialiser<FORWARD>, const FORWARD: bool> Initialiser<FORWARD, 1> for C

Source§

impl<const FORWARD: bool> Initialiser<FORWARD, 2> for NextInstsInit<FORWARD>

Source§

impl<const FORWARD: bool> Initialiser<FORWARD, 3> for ProofInitialiser<FORWARD>