pub struct Int<'ctx> { /* fields omitted */ }
Expand description
Ast
node representing an integer value.
Create a real from an integer.
This is just a convenience wrapper around
Real::from_int
; see notes there
Create an integer from a bitvector.
Signed and unsigned version.
let bv = ast::BV::new_const(&ctx, "x", 32);
solver.assert(&bv._eq(&ast::BV::from_i64(&ctx, -3, 32)));
let x = ast::Int::from_bv(&bv, true);
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();
assert_eq!(-3, model.eval(&x, true).unwrap().as_i64().unwrap());
Create a bitvector from an integer.
This is just a convenience wrapper around
BV::from_int
; see notes there
pub fn div(&self, other: &Self) -> Self
pub fn rem(&self, other: &Self) -> Self
pub fn modulo(&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>
impl<'a, 'ctx> Add<&'a Int<'ctx>> for Int<'ctx>
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<&'a Int<'ctx>> for &'a Int<'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<'a, 'ctx> Add<Int<'ctx>> for &'a Int<'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.
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 Int<'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
impl<'a, 'ctx> Div<&'a Int<'ctx>> for Int<'ctx>
The resulting type after applying the /
operator.
impl<'a, 'ctx> Div<&'a Int<'ctx>> for &'a Int<'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<'a, 'ctx> Div<Int<'ctx>> for &'a Int<'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.
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
impl<'a, 'ctx> Mul<&'a Int<'ctx>> for Int<'ctx>
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<&'a Int<'ctx>> for &'a Int<'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<'a, 'ctx> Mul<Int<'ctx>> for &'a Int<'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.
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 Int<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Neg for &'a Int<'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 !=
.
impl<'a, 'ctx> Rem<&'a Int<'ctx>> for Int<'ctx>
The resulting type after applying the %
operator.
impl<'a, 'ctx> Rem<&'a Int<'ctx>> for &'a Int<'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<'a, 'ctx> Rem<Int<'ctx>> for &'a Int<'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.
The resulting type after applying the %
operator.
The resulting type after applying the %
operator.
The resulting type after applying the %
operator.
impl<'a, 'ctx> Sub<&'a Int<'ctx>> for Int<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<&'a Int<'ctx>> for &'a Int<'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<'a, 'ctx> Sub<Int<'ctx>> for &'a Int<'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.
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<'ctx> Eq for Int<'ctx>
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.