Struct seer_z3::Ast

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

Methods

impl<'ctx> Ast<'ctx>

fn new(ctx: &Context, ast: Z3_ast) -> Ast

fn new_const(sym: &Symbol<'ctx>, sort: &Sort<'ctx>) -> Ast<'ctx>

fn fresh_const(ctx: &'ctx Context, prefix: &str, sort: &Sort<'ctx>) -> Ast<'ctx>

fn from_bool(ctx: &'ctx Context, b: bool) -> Ast<'ctx>

fn from_i64(ctx: &'ctx Context, i: i64) -> Ast<'ctx>

fn from_u64(ctx: &'ctx Context, u: u64) -> Ast<'ctx>

fn bv_from_u64(ctx: &'ctx Context, u: u64, sz: u32) -> Ast<'ctx>

fn from_real(ctx: &'ctx Context, num: i32, den: i32) -> Ast<'ctx>

fn as_bool(&self) -> Option<bool>

fn as_i64(&self) -> Option<i64>

fn as_u64(&self) -> Option<u64>

fn as_real(&self) -> Option<(i64, i64)>

fn extract(&self, high: u32, low: u32) -> Ast

fn distinct(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn ite(&self, a: &Ast<'ctx>, b: &Ast<'ctx>) -> Ast<'ctx>

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

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

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

fn and(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn or(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn add(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn sub(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn mul(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn not(&self) -> Ast<'ctx>

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

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

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

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

fn minus(&self) -> Ast<'ctx>

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

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

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

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

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

fn int2real(&self) -> Ast<'ctx>

fn real2int(&self) -> Ast<'ctx>

fn is_int(&self) -> Ast<'ctx>

fn bvnot(&self) -> Ast<'ctx>

fn bvneg(&self) -> Ast<'ctx>

fn bvredand(&self) -> Ast<'ctx>

fn bvredor(&self) -> Ast<'ctx>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fn store(&self, a: &Ast<'ctx>, b: &Ast<'ctx>) -> Ast<'ctx>

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

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

fn set_union(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

fn set_intersect(&self, other: &[&Ast<'ctx>]) -> Ast<'ctx>

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

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

fn set_complement(&self) -> Ast<'ctx>

Trait Implementations

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

fn drop(&mut self)

A method called when the value goes out of scope.

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>