Trait SmtBool

pub trait SmtBool<'a, S: SmtSolver<'a, Bool = Self>>:
    Clone
    + Debug
    + Display
    + BitOr<Output = Self>
    + BitAnd<Output = Self>
    + BitXor<Output = Self>
    + Not<Output = Self> {
    // Required methods
    fn is_identical(&self, other: &Self) -> bool;
    fn _eq(self, other: Self) -> S::Bool;
    fn simplify(self) -> Self;
    fn ite_bv(self, lhs: S::BV, rhs: S::BV) -> S::BV;
    fn ite_int(self, lhs: S::Int, rhs: S::Int) -> S::Int;
    fn ite_bool(self, lhs: S::Bool, rhs: S::Bool) -> S::Bool;
    fn ite_bv_array(self, lhs: S::BvArray, rhs: S::BvArray) -> S::BvArray;
    fn as_bool(&self) -> Option<bool>;

    // Provided methods
    fn ite_dynamic(
        self,
        lhs: Dynamic<'a, S>,
        rhs: Dynamic<'a, S>,
    ) -> Dynamic<'a, S> { ... }
    fn into_dynamic(self) -> Dynamic<'a, S> { ... }
}

Boolean expressions in the SMT solver.

Required Methods

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

Returns true if both expressions are structurally identical.

fn _eq(self, other: Self) -> S::Bool

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: S::BV, rhs: S::BV) -> S::BV

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

lhs is returned if the boolean value is true, rhs if it is false.

fn ite_int(self, lhs: S::Int, rhs: S::Int) -> S::Int

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

lhs is returned if the boolean value is true, rhs if it is false.

fn ite_bool(self, lhs: S::Bool, rhs: S::Bool) -> S::Bool

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

lhs is returned if the boolean value is true, rhs if it is false.

fn ite_bv_array(self, lhs: S::BvArray, rhs: S::BvArray) -> S::BvArray

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

lhs is returned if the boolean value is true, rhs if it is false.

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

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

Provided Methods

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

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

lhs is returned if the boolean value is true, rhs if it is false.

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

Converts the bool into a Dynamic expression.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

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

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