Struct CheckInitCondSatSMT

Source

pub struct CheckInitCondSatSMT {}

Expand description

Preprocessor that checks whether the initial conditions of threshold automaton are satisfiable at all. If this is not the case, replaces them with false and deletes all rules

Implementations§

Source §

impl CheckInitCondSatSMT

Source

pub fn new() -> Self

Create a new instance of the CheckInitCondSatSMT preprocessor

Trait Implementations§

Source §

impl Default for CheckInitCondSatSMT

Source §

fn default() -> Self

Returns the “default value” for a type. Read more

Source §

impl<S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder> Preprocessor<GeneralThresholdAutomaton, S, C> for CheckInitCondSatSMT

Source §

fn process(&self, ta: &mut GeneralThresholdAutomaton, _spec: &S, ctx: &C)

Process the threshold automaton and attempt to simplify it

Auto Trait Implementations§

§

impl UnwindSafe for CheckInitCondSatSMT

Blanket Implementations§

Source §

impl<T> Any for T
where T: 'static + ?Sized,

Source §

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

Source §

impl<T> Borrow<T> for T
where T: ?Sized,

Source §

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

Source §

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source §

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

Source §

impl<T> From<T> for T

Source §

fn from(t: T) -> T

Returns the argument unchanged.

Source §

impl<T, U> Into for T
where U: From<T>,

Source §

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source §

impl<T> IntoEither for T

Source §

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

Source §

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

§