Trait SmtEngine

Source

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>;
}