Struct Accel 

pub struct Accel { /* private fields */ }

The incremental sequence evaluator of one assertion.

Implementations

impl Accel

pub fn new( ir: &PropertyIr, n_clocks: usize, has_calls: bool, locals_read: bool, ) -> Option<Accel>

The accelerator for ir, or None when it has a shape the accelerator does not model (see the module docs).

locals_read: some leaf reads a local variable, which makes evaluating it fallible (an unassigned read), so the accelerator then never skips work the reference does (exact).

pub fn set_base(&mut self, base: u64)

The absolute index of the first position of the window the next queries are over.

pub fn evict_before(&mut self, base: u64)

Forgets the searches that started before absolute position base.

pub fn base(&self) -> u64

The absolute index of the window’s first position.

pub fn final_reach(&self, id: PropId) -> Option<u32>

How many ticks past a start the verdict of id can look, when the verdicts of id can be settled and shared across attempts (see [Fin]); None when they cannot.

pub fn final_next(&mut self, id: PropId) -> (u64, bool)

The first absolute tick whose verdict of id is not settled yet, and whether settling stopped there (an error): the settled ticks are base..next.

pub fn final_record(&mut self, id: PropId, at: u64, verdict: Option<bool>)

Settles tick at (which must be Self::final_next) of id: its verdict, or None when evaluating it is an error.

pub fn final_first(&self, id: PropId, v: bool, from: u64) -> Option<u64>

The first settled tick of id at or after from whose verdict is v (only the verdicts the operators ask for are kept: false for the operand of an always or the left of an until, true for eventually and the right of an until).

pub fn matches( &mut self, au: &Automaton, env: &dyn PropEnv, entry: ThreadStateId, real: u32, top: bool, pos: u32, frame: &Frame, ) -> Option<Matches>

Every nonempty match of the sequence starting at entry at position pos with frame, on the word of real samples and the tail top: what Evaluator::matches returns, ascending by (end tick, frame).

pub fn strong( &mut self, au: &Automaton, env: &dyn PropEnv, entry: ThreadStateId, real: u32, top: bool, pos: u32, frame: &Frame, ) -> Option<bool>

Whether the sequence has a match at all (strong(seq)).

pub fn weak( &mut self, au: &Automaton, env: &dyn PropEnv, entry: ThreadStateId, real: u32, top: bool, pos: u32, frame: &Frame, ) -> Option<bool>

weak(seq) from pos (F.5.3.1): every cut of the word, completed with ⊤, has a match.

Trait Implementations

impl Clone for Accel

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.