pub struct Ast<'ctx> { /* private fields */ }
Expand description
Abstract syntax tree node. That is, the data structure used in Z3 to represent terms, formulas, and types.
Implementations
sourceimpl<'ctx> Ast<'ctx>
impl<'ctx> Ast<'ctx>
pub fn new(ctx: &Context, ast: Z3_ast) -> Ast<'_>
pub fn new_const(sym: &Symbol<'ctx>, sort: &Sort<'ctx>) -> Ast<'ctx>
pub fn fresh_const(
ctx: &'ctx Context,
prefix: &str,
sort: &Sort<'ctx>
) -> Ast<'ctx>
pub fn from_bool(ctx: &'ctx Context, b: bool) -> Ast<'ctx>
pub fn from_i64(ctx: &'ctx Context, i: i64) -> Ast<'ctx>
pub fn from_u64(ctx: &'ctx Context, u: u64) -> Ast<'ctx>
pub fn from_real(ctx: &'ctx Context, num: i32, den: i32) -> Ast<'ctx>
pub fn as_bool(&self) -> Option<bool>
pub fn as_i64(&self) -> Option<i64>
pub fn as_u64(&self) -> Option<u64>
pub fn as_real(&self) -> Option<(i64, i64)>
pub fn distinct(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn ite(&self, a: &Ast<'ctx>, b: &Ast<'ctx>) -> Ast<'ctx>
pub fn iff(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn implies(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn xor(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn and(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn or(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn add(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn sub(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn mul(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn not(&self) -> Ast<'ctx>
pub fn div(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn rem(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn modulo(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn power(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn minus(&self) -> Ast<'ctx>
pub fn lt(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn le(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn _eq(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn ge(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn gt(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn int2real(&self) -> Ast<'ctx>
pub fn real2int(&self) -> Ast<'ctx>
pub fn is_int(&self) -> Ast<'ctx>
pub fn bvnot(&self) -> Ast<'ctx>
pub fn bvneg(&self) -> Ast<'ctx>
pub fn bvredand(&self) -> Ast<'ctx>
pub fn bvredor(&self) -> Ast<'ctx>
pub fn bvand(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvor(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvxor(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvnand(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvnor(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvxnor(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvadd(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsub(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvmul(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvudiv(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsdiv(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvurem(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsrem(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsmod(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvult(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvslt(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvule(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsle(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvuge(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsge(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvugt(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvsgt(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn concat(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvshl(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvlshr(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn bvashr(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn select(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn store(&self, a: &Ast<'ctx>, b: &Ast<'ctx>) -> Ast<'ctx>
pub fn set_add(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn set_del(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn set_union(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn set_intersect(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>
pub fn set_member(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn set_subset(&self, other: &Ast<'ctx>) -> Ast<'ctx>
pub fn set_complement(&self) -> Ast<'ctx>
pub fn pb_le(&self, other: &[&Ast<'ctx>], coeffs: Vec<i32>, k: i32) -> Ast<'ctx>
pub fn pb_ge(&self, other: &[&Ast<'ctx>], coeffs: Vec<i32>, k: i32) -> Ast<'ctx>
pub fn pb_eq(&self, other: &[&Ast<'ctx>], coeffs: Vec<i32>, k: i32) -> Ast<'ctx>
Trait Implementations
impl<'ctx> Eq for Ast<'ctx>
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Ast<'ctx>
impl<'ctx> !Send for Ast<'ctx>
impl<'ctx> !Sync for Ast<'ctx>
impl<'ctx> Unpin for Ast<'ctx>
impl<'ctx> UnwindSafe for Ast<'ctx>
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more