Struct CacheBool

pub struct CacheBool<'ctx, S: SmtSolver<'ctx>> { /* private fields */ }

Cacheable SMT Bool type.

Trait Implementations

impl<'ctx, S: SmtSolver<'ctx>> BitAnd for CacheBool<'ctx, S>

type Output = CacheBool<'ctx, S>

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl<'ctx, S: SmtSolver<'ctx>> BitOr for CacheBool<'ctx, S>

type Output = CacheBool<'ctx, S>

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl<'ctx, S: SmtSolver<'ctx>> BitXor for CacheBool<'ctx, S>

type Output = CacheBool<'ctx, S>

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: Self) -> Self::Output

Performs the ^ operation.

impl<'ctx, S: SmtSolver<'ctx>> Clone for CacheBool<'ctx, S>

fn clone(&self) -> Self

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx, S: SmtSolver<'ctx>> Debug for CacheBool<'ctx, S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'ctx, S: SmtSolver<'ctx>> Display for CacheBool<'ctx, S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'ctx, S: SmtSolver<'ctx>> Not for CacheBool<'ctx, S>

type Output = CacheBool<'ctx, S>

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBool<'ctx, CachedSolver<'ctx, S, C>> for CacheBool<'ctx, S>

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn _eq(self, other: Self) -> CacheBool<'ctx, S>

Returns an SMT expression that performs an equality comparison between the two bools.

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn ite_bv( self, lhs: CacheBV<'ctx, S>, rhs: CacheBV<'ctx, S>, ) -> CacheBV<'ctx, S>

Creates an If-Then-Else expression that returns bitvectors.

fn ite_int( self, lhs: CacheInt<'ctx, S>, rhs: CacheInt<'ctx, S>, ) -> CacheInt<'ctx, S>

Creates an If-Then-Else expression that returns integers.

fn ite_bool( self, lhs: CacheBool<'ctx, S>, rhs: CacheBool<'ctx, S>, ) -> CacheBool<'ctx, S>

Creates an If-Then-Else expression that returns booleans.

fn ite_bv_array( self, lhs: CacheBVArray<'ctx, S>, rhs: CacheBVArray<'ctx, S>, ) -> CacheBVArray<'ctx, S>

Creates an If-Then-Else expression that returns bitvector arrays.

fn as_bool(&self) -> Option<bool>

Converts the SMT boolean expression to a bool, if possible.

fn ite_dynamic(self, lhs: Dynamic<'a, S>, rhs: Dynamic<'a, S>) -> Dynamic<'a, S>

Creates an If-Then-Else expression that returns Dynamics.

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bool into a Dynamic expression.