Struct mikino_api::check::BaseRes

pub struct BaseRes<'sys> { /* private fields */ }

Result of a base check, simply wraps a CheckRes.

Implementations

impl<'sys> BaseRes<'sys>

pub fn as_inner(&self) -> &CheckRes<'sys>

Inner result accessor (borrow).

pub fn into_inner(self) -> CheckRes<'sys>

Inner result accessor (move).

impl<'sys> BaseRes<'sys>

pub fn merge_base_with_step(&self, step: &StepRes<'sys>) -> Res<BmcRes<'sys>>

Merges a base result with a step result for BMC.

The result res is such that

• okay contains POs that are in self.okay ⧵ step.okay, and
• cexs is empty.

That is, the result only contains POs that

• hold in the initial states, and
• are not inductive.

Errors

• when the two results mention inconsistent POs.

Methods from Deref<Target = CheckRes<'sys>>

pub fn all_falsified(&self) -> bool

True if all POs have been falsified.

pub fn has_falsifications(&self) -> bool

True if some POs have been falsified.

pub fn register_falsification(
    &mut self,
    po: &'s String,
    solver: &mut SFSolver
) -> Res<()>

Registers a falsification.

Errors

• when po does not belong to self.okay;
• when a falsification for po has already been registered.

Trait Implementations

impl<'sys> Deref for BaseRes<'sys>

type Target = CheckRes<'sys>

The resulting type after dereferencing.

fn deref(&self) -> &CheckRes<'sys>

Dereferences the value.

impl<'sys> DerefMut for BaseRes<'sys>

fn deref_mut(&mut self) -> &mut CheckRes<'sys>

Mutably dereferences the value.

impl<'sys> From<CheckRes<'sys>> for BaseRes<'sys>

fn from(res: CheckRes<'sys>) -> BaseRes<'_>

Converts to this type from the input type.