[−][src]Struct rust_smt::z3::Z3Solver
Trait Implementations
impl SMTSolver for Z3Solver[src]
type S = Z3Sort
type T = Z3Term
type F = Z3UninterpretedFunction
fn new() -> Z3Solver[src]
fn declare_sort(&self, name: &str) -> Result<Z3Sort, SMTError>[src]
fn lookup_sort(&self, s: Sorts) -> Result<Z3Sort, SMTError>[src]
fn apply_sort(
&self,
s: Sorts,
s1: &Z3Sort,
s2: &Z3Sort
) -> Result<Z3Sort, SMTError>[src]
&self,
s: Sorts,
s1: &Z3Sort,
s2: &Z3Sort
) -> Result<Z3Sort, SMTError>
fn declare_record_sort(
&mut self,
name: &str,
fields: &[&str],
sorts: &[&Z3Sort]
) -> Result<Z3Sort, SMTError>[src]
&mut self,
name: &str,
fields: &[&str],
sorts: &[&Z3Sort]
) -> Result<Z3Sort, SMTError>
fn declare_fun(
&self,
name: &str,
args: &[&Z3Sort],
sort: &Z3Sort
) -> Result<Z3UninterpretedFunction, SMTError>[src]
&self,
name: &str,
args: &[&Z3Sort],
sort: &Z3Sort
) -> Result<Z3UninterpretedFunction, SMTError>
fn declare_const(&self, name: &str, sort: &Z3Sort) -> Result<Z3Term, SMTError>[src]
fn lookup_const(&self, f: Fn) -> Result<Z3Term, SMTError>[src]
fn const_from_int(&self, value: i64, sort: &Z3Sort) -> Result<Z3Term, SMTError>[src]
fn const_from_string(
&self,
value: &str,
sort: &Z3Sort
) -> Result<Z3Term, SMTError>[src]
&self,
value: &str,
sort: &Z3Sort
) -> Result<Z3Term, SMTError>
fn record_const(
&self,
record_sort: &Z3Sort,
field_values: &[Z3Term]
) -> Result<Z3Term, SMTError>[src]
&self,
record_sort: &Z3Sort,
field_values: &[Z3Term]
) -> Result<Z3Term, SMTError>
fn record_const_refs(
&self,
record_sort: &Z3Sort,
field_values: &[&Z3Term]
) -> Result<Z3Term, SMTError>[src]
&self,
record_sort: &Z3Sort,
field_values: &[&Z3Term]
) -> Result<Z3Term, SMTError>
fn apply_fun(
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[Z3Term]
) -> Result<Z3Term, SMTError>[src]
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[Z3Term]
) -> Result<Z3Term, SMTError>
fn apply_fun_refs(
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[&Z3Term]
) -> Result<Z3Term, SMTError>[src]
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[&Z3Term]
) -> Result<Z3Term, SMTError>
fn level(&self) -> u32[src]
fn push(&mut self, n: u32) -> Result<bool, SMTError>[src]
fn pop(&mut self, n: u32) -> Result<bool, SMTError>[src]
fn assert(&mut self, t: &Z3Term) -> Result<bool, SMTError>[src]
fn check_sat(&mut self) -> CheckSatResult[src]
fn get_value(&mut self, t: &Z3Term) -> Result<Z3Term, SMTError>[src]
impl Drop for Z3Solver[src]
Auto Trait Implementations
Blanket Implementations
impl<T> From for T[src]
impl<T, U> Into for T where
U: From<T>, [src]
U: From<T>,
impl<T, U> TryFrom for T where
U: Into<T>, [src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>[src]
impl<T, U> TryInto for T where
U: TryFrom<T>, [src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>[src]
impl<T> Borrow for T where
T: ?Sized, [src]
T: ?Sized,
impl<T> BorrowMut for T where
T: ?Sized, [src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T[src]
impl<T> Any for T where
T: 'static + ?Sized, [src]
T: 'static + ?Sized,