Struct Bool 

pub struct Bool {
    pub id: TermId,
}

A boolean-sorted term, analogous to z3::Bool<'ctx>.

Fields

id: TermId

The underlying term identifier.

Implementations

impl Bool

pub fn from_id(id: TermId) -> Self

Wrap a raw TermId as a Bool.

pub fn new_const(ctx: &Z3Context, name: &str) -> Self

Declare a fresh boolean constant named name.

pub fn from_bool(ctx: &Z3Context, value: bool) -> Self

Create the boolean literal true.

pub fn and(ctx: &Z3Context, args: &[Bool]) -> Self

Logical conjunction (AND) of a slice of boolean terms.

pub fn or(ctx: &Z3Context, args: &[Bool]) -> Self

Logical disjunction (OR) of a slice of boolean terms.

pub fn not(ctx: &Z3Context, arg: &Bool) -> Self

Logical negation (NOT) of a boolean term.

pub fn implies(ctx: &Z3Context, lhs: &Bool, rhs: &Bool) -> Self

Logical implication: lhs => rhs.

pub fn iff(ctx: &Z3Context, lhs: &Bool, rhs: &Bool) -> Self

Logical bi-implication (IFF / XNOR): lhs <=> rhs.

Implemented as NOT (lhs XOR rhs) which is logically equivalent.

pub fn xor(ctx: &Z3Context, lhs: &Bool, rhs: &Bool) -> Self

Exclusive-or of two boolean terms.

Trait Implementations

impl Clone for Bool

fn clone(&self) -> Bool

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Bool

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

Formats the value using the given formatter.

impl From<Bool> for TermId

fn from(b: Bool) -> Self

Converts to this type from the input type.