Struct Real 

pub struct Real {
    pub id: TermId,
}

A real-sorted term, analogous to z3::Real<'ctx>.

Fields

id: TermId

The underlying term identifier.

Implementations

impl Real

pub fn gt(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Bool

Strict greater-than comparison: lhs > rhs.

pub fn ge(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Bool

Greater-than-or-equal comparison: lhs >= rhs.

pub fn neg(ctx: &Z3Context, arg: &Real) -> Real

Arithmetic negation: -arg.

pub fn div(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Real

Real division: lhs / rhs.

pub fn from_i64(ctx: &Z3Context, value: i64) -> Real

Create a real literal from an i64 value (denominator = 1).

impl Real

pub fn from_id(id: TermId) -> Self

Wrap a raw TermId as a Real.

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

Declare a fresh real constant named name.

pub fn from_frac(ctx: &Z3Context, num: i64, den: i64) -> Self

Create a real literal from a numerator/denominator pair.

pub fn add(ctx: &Z3Context, args: &[Real]) -> Self

Arithmetic addition of a slice of real terms.

pub fn sub(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Self

Arithmetic subtraction: lhs - rhs.

pub fn mul(ctx: &Z3Context, args: &[Real]) -> Self

Arithmetic multiplication of a slice of real terms.

pub fn lt(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Bool

Strict less-than comparison: lhs < rhs.

pub fn le(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Bool

Less-than-or-equal comparison: lhs <= rhs.

pub fn eq(ctx: &Z3Context, lhs: &Real, rhs: &Real) -> Bool

Equality: lhs = rhs.

Trait Implementations

impl Clone for Real

fn clone(&self) -> Real

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Real

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

Formats the value using the given formatter.

impl From<Real> for TermId

fn from(x: Real) -> Self

Converts to this type from the input type.