Struct smt2::client::Client

pub struct Client<L, C: Clone + PartialEq, S: Sort, F: Function> { /* fields omitted */ }

SMT2-lib solver environment.

Implementations

impl<L, C: Constant, S: Sort, F: Function> Client<L, C, S, F> where
    L: Display,
    C: Display, 

pub fn new(
    cmd: Command,
    sort_bool: S,
    cst_true: F,
    cst_false: F
) -> ExecResult<Client<L, C, S, F>, Error<L, C, S, F>>

pub fn new_id(&mut self) -> Ident

pub fn new_sort_id(&mut self) -> Ident

pub fn assert(
    &mut self,
    term: &Typed<Term<Self>>
) -> ExecResult<(), Error<L, C, S, F>>

Assert.

pub fn check_sat(&mut self) -> ExecResult<CheckSat, Error<L, C, S, F>>

Check satifiability.

pub fn declare_const(
    &mut self,
    cst: F,
    sort: &GroundSort<S>
) -> ExecResult<(), Error<L, C, S, F>>

Declare a new constant.

pub fn declare_sort(&mut self, sort: S) -> ExecResult<(), Error<L, C, S, F>>

Declare new sort.

pub fn predefined_fun<Id: ToString>(
    &mut self,
    id: Id,
    function: F,
    sig: FunctionSignature<S>
) -> ExecResult<(), Error<L, C, S, F>>

Set the function object for the given predefined function.

pub fn declare_fun(
    &mut self,
    function: F,
    args: &Vec<GroundSort<S>>,
    return_sort: &GroundSort<S>
) -> ExecResult<(), Error<L, C, S, F>>

Declare new function.

pub fn define_sort(
    &mut self,
    _def: &DataTypeDeclaration<Self>
) -> ExecResult<(), Error<L, C, S, F>>

Define previously declared sort.

pub fn exit(&mut self) -> ExecResult<(), Error<L, C, S, F>>

Exit the solver.

pub fn get_model(&mut self) -> ExecResult<Model<Self>, Error<L, C, S, F>>

pub fn set_logic(&mut self, logic: &L) -> ExecResult<(), Error<L, C, S, F>>

Set the solver's logic.

Trait Implementations

impl<L, C: Clone + PartialEq, S: Sort, F: Function> Environment for Client<L, C, S, F>

type Logic = L

type Ident = Ident

type Constant = Sorted<C, GroundSort<S>>

type Sort = S

type Function = F

type Error = Error<L, C, S, F>

fn sort(&self, id: &Ident) -> Option<S>

Find a sort.

fn sort_bool(&self) -> GroundSort<S>

Get the Bool sort, which is the only required sort.

fn typecheck_function(
    &self,
    _checker: &mut TypeChecker<S>,
    _f: &F,
    _args: &[TypeRef<S>],
    _return_sort: TypeRef<S>
)