pub struct Real<'ctx> { /* fields omitted */ }
Expand description
Ast
node representing a real value.
Create an integer from a real.
This is just a convenience wrapper around
Int::from_real
; see notes there
pub fn div(&self, other: &Self) -> Self
pub fn power(&self, other: &Self) -> Self
pub fn lt(&self, other: &Self) -> Bool<'ctx>
pub fn le(&self, other: &Self) -> Bool<'ctx>
pub fn gt(&self, other: &Self) -> Bool<'ctx>
pub fn ge(&self, other: &Self) -> Bool<'ctx>
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
impl<'ctx> Ast<'ctx> for Real<'ctx>
Compare this Ast
with another Ast
, and get a Bool
representing the result. Read more
Compare this Ast
with another Ast
, and get a Result. Errors if the sort does not
match for the two values. Read more
Compare this Ast
with a list of other Ast
s, and get a Bool
which is true only if all arguments (including Self) are pairwise distinct. Read more
Simplify the Ast
. Returns a new Ast
which is equivalent,
but simplified using algebraic simplification rules, such as
constant propagation. Read more
Performs substitution on the Ast
. The slice substitutions
contains a
list of pairs with a “from” Ast
that will be substituted by a “to” Ast
. Read more
Return the number of children of this Ast
. Read more
Return the children of this node as a Vec<Dynamic>
.
Return the AstKind
for this Ast
.
Return true
if this is a Z3 function application. Read more
Return true
if this is a Z3 constant. Read more
Performs copy-assignment from source
. Read more
Formats the value using the given formatter. Read more
Formats the value using the given formatter. Read more
The resulting type after applying the /
operator.
The resulting type after applying the /
operator.
The resulting type after applying the /
operator.
The resulting type after applying the /
operator.
Executes the destructor for this type. Read more
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
The resulting type after applying the -
operator.
impl<'a, 'ctx> Neg for &'a Real<'ctx>
The resulting type after applying the -
operator.
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
The type returned in the event of a conversion error.
impl<T> Any for T where
T: 'static + ?Sized,
Immutably borrows from an owned value. Read more
Mutably borrows from an owned value. Read more
impl<T, U> Into<U> for T where
U: From<T>,
The resulting type after obtaining ownership.
Creates owned data from borrowed data, usually by cloning. Read more
🔬 This is a nightly-only experimental API. (toowned_clone_into
)
recently added
Uses borrowed data to replace owned data, usually by cloning. Read more
Converts the given value to a String
. Read more
The type returned in the event of a conversion error.
The type returned in the event of a conversion error.