Struct seer_z3::Ast

pub struct Ast<'ctx> { /* fields omitted */ }

Methods

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 bv_from_u64(ctx: &'ctx Context, u: u64, sz: u32) -> 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 extract(&self, high: u32, low: u32) -> Ast

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>

Trait Implementations

impl<'ctx> Drop for Ast<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> Hash for Ast<'ctx>

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

Feeds a slice of this type into the given [Hasher].

impl<'ctx> PartialEq<Ast<'ctx>> for Ast<'ctx>

fn eq(&self, other: &Ast<'ctx>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

impl<'ctx> Eq for Ast<'ctx>