Trait SMTBackend

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

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

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)

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

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

type Idx = NodeIndex

type Logic = L