prjunnamed_netlist

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

Required Associated Types§

Required Methods§

Source

fn build_bool_lit(&self, value: bool) -> Self::Bool

Source

fn build_bool_eq(&self, arg1: Self::Bool, arg2: Self::Bool) -> Self::Bool

Source

fn build_bool_ite( &self, cond: Self::Bool, if_true: Self::Bool, if_false: Self::Bool, ) -> Self::Bool

Source

fn build_bool_let( &self, var: &str, expr: Self::Bool, body: impl FnOnce(Self::Bool) -> Self::Bool, ) -> Self::Bool

Source

fn build_not(&self, arg: Self::Bool) -> Self::Bool

Source

fn build_and(&self, args: &[Self::Bool]) -> Self::Bool

Source

fn build_or(&self, args: &[Self::Bool]) -> Self::Bool

Source

fn build_xor(&self, args: &[Self::Bool]) -> Self::Bool

Source

fn build_bitvec_lit(&self, value: &Const) -> Self::BitVec

Source

fn build_bitvec_eq(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool

Source

fn build_bitvec_ite( &self, cond: Self::Bool, if_true: Self::BitVec, if_false: Self::BitVec, ) -> Self::BitVec

Source

fn build_bitvec_let( &self, var: &str, expr: Self::BitVec, body: impl FnOnce(Self::BitVec) -> Self::BitVec, ) -> Self::BitVec

Source

fn build_concat( &self, arg_msb: Self::BitVec, arg_lsb: Self::BitVec, ) -> Self::BitVec

Source

fn build_extract( &self, index_msb: usize, index_lsb: usize, arg: Self::BitVec, ) -> Self::BitVec

Source

fn build_bvnot(&self, arg1: Self::BitVec) -> Self::BitVec

Source

fn build_bvand(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvor(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvxor(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvadd(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvcomp(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvult(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool

Source

fn build_bvslt(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::Bool

Source

fn build_bvshl(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvlshr(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvashr(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvmul(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvudiv(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvurem(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvsdiv(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn build_bvsrem(&self, arg1: Self::BitVec, arg2: Self::BitVec) -> Self::BitVec

Source

fn declare_bool_const(&self, name: &str) -> Result<Self::Bool, Self::Error>

Source

fn declare_bitvec_const( &self, name: &str, width: usize, ) -> Result<Self::BitVec, Self::Error>

Source

fn assert(&mut self, term: Self::Bool) -> Result<(), Self::Error>

Source

fn check(&mut self) -> Result<SmtResponse, Self::Error>

Source

fn get_bool(&self, term: &Self::Bool) -> Result<bool, Self::Error>

Source

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.

Implementors§