Struct CvlrAnd 

pub struct CvlrAnd<A, B>(/* private fields */);

A boolean expression representing the logical AND of two expressions.

This expression evaluates to true only when both sub-expressions evaluate to true. When asserting or assuming, both sub-expressions are processed.

Trait Implementations

impl<A: Clone, B: Clone> Clone for CvlrAnd<A, B>

fn clone(&self) -> CvlrAnd<A, B>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<A, B> CvlrFormula for CvlrAnd<A, B>

where A: CvlrFormula, B: CvlrFormula<Context = A::Context>,

type Context = <A as CvlrFormula>::Context

fn eval(&self, ctx: &Self::Context) -> bool

Evaluates the expression in the given context.

fn assert(&self, ctx: &Self::Context)

Asserts that the expression holds in the given context.

fn assume(&self, ctx: &Self::Context)

Assumes that the expression holds in the given context.

fn eval_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) -> bool

Evaluates the expression over two states (pre-state and post-state).

fn assert_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context)

Asserts that the expression holds across two states (pre-state and post-state).

fn assume_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context)

Assumes that the expression holds across two states (pre-state and post-state).

impl<A: Copy, B: Copy> Copy for CvlrAnd<A, B>