pub trait SmtEngine {
type Bool: Clone;
type BitVec: Clone;
type Error;
Show 36 methods
// Required methods
fn build_bool_lit(&self, value: bool) -> Self::Bool;
fn build_bool_eq(&self, arg1: Self::Bool, arg2: Self::Bool) -> Self::Bool;
fn build_bool_ite(
&self,
cond: Self::Bool,
if_true: Self::Bool,
if_false: Self::Bool,
) -> Self::Bool;
fn build_bool_let(
&self,
var: &str,
expr: Self::Bool,
body: impl FnOnce(Self::Bool) -> Self::Bool,
) -> Self::Bool;
fn build_not(&self, arg: Self::Bool) -> Self::Bool;
fn build_and(&self, args: &[Self::Bool]) -> Self::Bool;
fn build_or(&self, args: &[Self::Bool]) -> Self::Bool;
fn build_xor(&self, args: &[Self::Bool]) -> Self::Bool;
fn build_bitvec_lit(&self, value: &Const) -> Self::BitVec;
fn build_bitvec_eq(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::Bool;
fn build_bitvec_ite(
&self,
cond: Self::Bool,
if_true: Self::BitVec,
if_false: Self::BitVec,
) -> Self::BitVec;
fn build_bitvec_let(
&self,
var: &str,
expr: Self::BitVec,
body: impl FnOnce(Self::BitVec) -> Self::BitVec,
) -> Self::BitVec;
fn build_concat(
&self,
arg_msb: Self::BitVec,
arg_lsb: Self::BitVec,
) -> Self::BitVec;
fn build_extract(
&self,
index_msb: usize,
index_lsb: usize,
arg: Self::BitVec,
) -> Self::BitVec;
fn build_bvnot(&self, arg1: Self::BitVec) -> Self::BitVec;
fn build_bvand(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvor(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec;
fn build_bvxor(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvadd(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvcomp(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvult(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool;
fn build_bvslt(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool;
fn build_bvshl(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvlshr(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvashr(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvmul(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvudiv(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvurem(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvsdiv(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn build_bvsrem(
&self,
arg1: Self::BitVec,
arg2: Self::BitVec,
) -> Self::BitVec;
fn declare_bool_const(&self, name: &str) -> Result<Self::Bool, Self::Error>;
fn declare_bitvec_const(
&self,
name: &str,
width: usize,
) -> Result<Self::BitVec, Self::Error>;
fn assert(&mut self, term: Self::Bool) -> Result<(), Self::Error>;
fn check(&mut self) -> Result<SmtResponse, Self::Error>;
fn get_bool(&self, term: &Self::Bool) -> Result<bool, Self::Error>;
fn get_bitvec(&self, term: &Self::BitVec) -> Result<Const, Self::Error>;
}
Required Associated Types§
Required Methods§
fn build_bool_lit(&self, value: bool) -> Self::Bool
fn build_bool_eq(&self, arg1: Self::Bool, arg2: Self::Bool) -> Self::Bool
fn build_bool_ite( &self, cond: Self::Bool, if_true: Self::Bool, if_false: Self::Bool, ) -> Self::Bool
fn build_bool_let( &self, var: &str, expr: Self::Bool, body: impl FnOnce(Self::Bool) -> Self::Bool, ) -> Self::Bool
fn build_not(&self, arg: Self::Bool) -> Self::Bool
fn build_and(&self, args: &[Self::Bool]) -> Self::Bool
fn build_or(&self, args: &[Self::Bool]) -> Self::Bool
fn build_xor(&self, args: &[Self::Bool]) -> Self::Bool
fn build_bitvec_lit(&self, value: &Const) -> Self::BitVec
fn build_bitvec_eq(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool
fn build_bitvec_ite( &self, cond: Self::Bool, if_true: Self::BitVec, if_false: Self::BitVec, ) -> Self::BitVec
fn build_bitvec_let( &self, var: &str, expr: Self::BitVec, body: impl FnOnce(Self::BitVec) -> Self::BitVec, ) -> Self::BitVec
fn build_concat( &self, arg_msb: Self::BitVec, arg_lsb: Self::BitVec, ) -> Self::BitVec
fn build_extract( &self, index_msb: usize, index_lsb: usize, arg: Self::BitVec, ) -> Self::BitVec
fn build_bvnot(&self, arg1: Self::BitVec) -> Self::BitVec
fn build_bvand(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvor(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvxor(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvadd(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvcomp(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvult(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool
fn build_bvslt(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool
fn build_bvshl(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvlshr(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvashr(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvmul(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvudiv(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvurem(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvsdiv(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn build_bvsrem(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec
fn declare_bool_const(&self, name: &str) -> Result<Self::Bool, Self::Error>
fn declare_bitvec_const( &self, name: &str, width: usize, ) -> Result<Self::BitVec, Self::Error>
fn assert(&mut self, term: Self::Bool) -> Result<(), Self::Error>
fn check(&mut self) -> Result<SmtResponse, Self::Error>
fn get_bool(&self, term: &Self::Bool) -> Result<bool, Self::Error>
fn get_bitvec(&self, term: &Self::BitVec) -> Result<Const, Self::Error>
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.