pub trait SMTBackend {
type Idx: Debug + Clone;
type Logic: Logic;
// Required methods
fn set_logic<S: SMTProc>(&mut self, _: &mut S);
fn new_var<T, P>(&mut self, _: Option<T>, _: P) -> Self::Idx
where T: AsRef<str>,
P: Into<<<Self as SMTBackend>::Logic as Logic>::Sorts>;
fn assert<T: Into<<<Self as SMTBackend>::Logic as Logic>::Fns>>(
&mut self,
_: T,
_: &[Self::Idx],
) -> Self::Idx;
fn check_sat<S: SMTProc>(&mut self, _: &mut S, _: bool) -> SMTRes;
fn solve<S: SMTProc>(
&mut self,
_: &mut S,
_: bool,
) -> (SMTResult<HashMap<Self::Idx, u64>>, SMTRes);
}
Expand description
Trait a backend should implement to support SMT solving.
This is a minimalistic API and has to be expanded in the future to support more SMT operations and to grow this into a full SMTLib Crate.
All functions names are analogous in meaning to their usage in the original SMT-LIB2 sense. TODO:
- define_fun
- declare_sort
- define_sort
- get_proof
- get_unsat_core
- get_value
- get_assignment
- push
- pop
- get_option
- set_option
- get_info
- set_info
- exit
Required Associated Types§
Required Methods§
fn set_logic<S: SMTProc>(&mut self, _: &mut S)
fn new_var<T, P>(&mut self, _: Option<T>, _: P) -> Self::Idx
fn assert<T: Into<<<Self as SMTBackend>::Logic as Logic>::Fns>>( &mut self, _: T, _: &[Self::Idx], ) -> Self::Idx
fn check_sat<S: SMTProc>(&mut self, _: &mut S, _: bool) -> SMTRes
fn solve<S: SMTProc>( &mut self, _: &mut S, _: bool, ) -> (SMTResult<HashMap<Self::Idx, u64>>, SMTRes)
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.