Struct Client 

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

SMT2-lib solver environment.

Implementations

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

where L: Display, C: Display + Constant,

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>

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.

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 typecheck_function( &self, _checker: &mut TypeChecker<S>, _f: &F, _args: &[TypeRef<S>], _return_sort: TypeRef<S>, )