Struct SMTLib2

pub struct SMTLib2<T: Logic> { /* private fields */ }

Implementations

impl<L: Logic> SMTLib2<L>

pub fn new(logic: Option<L>) -> SMTLib2<L>

pub fn expand_assertion(&self, ni: NodeIndex) -> String

pub fn new_const<T: Into<L::Fns>>(&mut self, cval: T) -> NodeIndex

Trait Implementations

impl<T: Clone + Logic> Clone for SMTLib2<T>

where T::Fns: Clone, T::Sorts: Clone,

fn clone(&self) -> SMTLib2<T>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: Debug + Logic> Debug for SMTLib2<T>

where T::Fns: Debug, T::Sorts: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<L: Logic> SMTBackend for SMTLib2<L>

type Idx = NodeIndex

type Logic = L

fn new_var<T, P>(&mut self, var_name: Option<T>, ty: P) -> Self::Idx

where T: AsRef<str>, P: Into<<<Self as SMTBackend>::Logic as Logic>::Sorts>,

fn set_logic<S: SMTProc>(&mut self, smt_proc: &mut S)

fn assert<T: Into<L::Fns>>(&mut self, assert: T, ops: &[Self::Idx]) -> Self::Idx

fn check_sat<S: SMTProc>(&mut self, smt_proc: &mut S, debug: bool) -> SMTRes

fn solve<S: SMTProc>( &mut self, smt_proc: &mut S, debug: bool, ) -> (SMTResult<HashMap<Self::Idx, u64>>, SMTRes)