[−][src]Trait rust_smt::SMTSolver
Associated Types
Loading content...Required methods
fn new() -> Self
fn declare_sort(&self, name: &str) -> Result<Self::S, SMTError>
fn lookup_sort(&self, s: Sorts) -> Result<Self::S, SMTError>
fn apply_sort(
&self,
s: Sorts,
s1: &Self::S,
s2: &Self::S
) -> Result<Self::S, SMTError>
&self,
s: Sorts,
s1: &Self::S,
s2: &Self::S
) -> Result<Self::S, SMTError>
fn declare_record_sort(
&mut self,
name: &str,
fields: &[&str],
sorts: &[&Self::S]
) -> Result<Self::S, SMTError>
&mut self,
name: &str,
fields: &[&str],
sorts: &[&Self::S]
) -> Result<Self::S, SMTError>
fn declare_fun(
&self,
name: &str,
args: &[&Self::S],
sort: &Self::S
) -> Result<Self::F, SMTError>
&self,
name: &str,
args: &[&Self::S],
sort: &Self::S
) -> Result<Self::F, SMTError>
fn declare_const(&self, name: &str, sort: &Self::S) -> Result<Self::T, SMTError>
fn lookup_const(&self, f: Fn) -> Result<Self::T, SMTError>
fn const_from_int(
&self,
value: i64,
sort: &Self::S
) -> Result<Self::T, SMTError>
&self,
value: i64,
sort: &Self::S
) -> Result<Self::T, SMTError>
fn const_from_string(
&self,
value: &str,
sort: &Self::S
) -> Result<Self::T, SMTError>
&self,
value: &str,
sort: &Self::S
) -> Result<Self::T, SMTError>
fn record_const(
&self,
record_sort: &Self::S,
field_values: &[Self::T]
) -> Result<Self::T, SMTError>
&self,
record_sort: &Self::S,
field_values: &[Self::T]
) -> Result<Self::T, SMTError>
fn record_const_refs(
&self,
record_sort: &Self::S,
field_values: &[&Self::T]
) -> Result<Self::T, SMTError>
&self,
record_sort: &Self::S,
field_values: &[&Self::T]
) -> Result<Self::T, SMTError>
fn apply_fun(
&self,
f: &Function<Self::F>,
args: &[Self::T]
) -> Result<Self::T, SMTError>
&self,
f: &Function<Self::F>,
args: &[Self::T]
) -> Result<Self::T, SMTError>
fn apply_fun_refs(
&self,
f: &Function<Self::F>,
args: &[&Self::T]
) -> Result<Self::T, SMTError>
&self,
f: &Function<Self::F>,
args: &[&Self::T]
) -> Result<Self::T, SMTError>
fn level(&self) -> u32
fn push(&mut self, n: u32) -> Result<bool, SMTError>
fn pop(&mut self, n: u32) -> Result<bool, SMTError>
fn assert(&mut self, t: &Self::T) -> Result<bool, SMTError>
fn check_sat(&mut self) -> CheckSatResult
fn get_value(&mut self, t: &Self::T) -> Result<Self::T, SMTError>
Implementors
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>