Struct Bool

pub struct Bool<'ctx>(/* private fields */);

A Z3 Bool.

Implementations

impl<'ctx> Bool<'ctx>

pub fn from_z3(bool: Bool<'ctx>) -> Self

Wraps a [z3::ast::Bool].

pub fn as_z3(&self) -> &Bool<'_>

Returns the wrapped [z3::ast::Bool].

Trait Implementations

impl BitAnd for Bool<'_>

type Output = Bool<'_>

The resulting type after applying the & operator.

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

Performs the & operation.

impl BitOr for Bool<'_>

type Output = Bool<'_>

The resulting type after applying the | operator.

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

Performs the | operation.

impl BitXor for Bool<'_>

type Output = Bool<'_>

The resulting type after applying the ^ operator.

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

Performs the ^ operation.

impl<'ctx> Clone for Bool<'ctx>

fn clone(&self) -> Bool<'ctx>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for Bool<'ctx>

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

Formats the value using the given formatter.

impl Display for Bool<'_>

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

Formats the value using the given formatter.

impl Not for Bool<'_>

type Output = Bool<'_>

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx>

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

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

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

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

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

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

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

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

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

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

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

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

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

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

Returns true if both expressions are structurally identical.

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.