Struct Bool 

pub struct Bool { /* private fields */ }

A boolean term (predicate).

Mirrors the z3::ast::Bool call surface used by the semantics encoders.

Implementations

impl Bool

pub fn new_const(name: impl Into<String>) -> Self

A fresh free (symbolic) boolean variable.

ordeal’s fragment has no boolean variables, so this is encoded as var != 0 over a fresh 1-bit bitvector variable — an exact bridge.

pub fn from_bool(value: bool) -> Self

The boolean literal true / false.

pub fn eq(&self, other: impl Borrow<Bool>) -> Bool

Boolean equality (iff), encoded as (a ∧ b) ∨ (¬a ∧ ¬b) — the fragment has no native boolean =.

pub fn not(&self) -> Bool

Logical negation.

pub fn and(values: &[&Bool]) -> Bool

N-ary conjunction (empty slice is true).

pub fn or(values: &[&Bool]) -> Bool

N-ary disjunction (empty slice is false).

pub fn ite(&self, then_: impl Borrow<BV>, else_: impl Borrow<BV>) -> BV

If-then-else over bitvector branches (the bool→BV bridge; BvTerm::Ite is native in ordeal 0.4).

pub fn simplify(&self) -> Bool

Return self unchanged; pair with Bool::as_bool, which concretely evaluates closed predicates (the z3 simplify().as_bool() idiom).

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

Concrete value of a closed (variable-free) predicate.

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 Display for Bool

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

Formats the value using the given formatter.