[−][src]Trait smt2::Environment

pub trait Environment: Sized {
    type Logic;
    type Constant: Clone + PartialEq + SortedWith<GroundSort<Self::Sort>>;
    type Ident: Clone + PartialEq;
    type Sort: Sort;
    type Function;
    type Error;
    fn sort(&self, id: &Self::Ident) -> Option<Self::Sort>;

    fn sort_bool(&self) -> GroundSort<Self::Sort>;

    fn typecheck_function(
        &self, 
        checker: &mut TypeChecker<Self::Sort>, 
        f: &Self::Function, 
        args: &[TypeRef<Self::Sort>], 
        return_sort: TypeRef<Self::Sort>
    );
}

SMT2-lib solver environment.

Associated Types

type Logic

type Constant: Clone + PartialEq + SortedWith<GroundSort<Self::Sort>>

type Ident: Clone + PartialEq

type Sort: Sort

type Function

type Error

Loading content...

Required methods

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

Find a sort.

fn sort_bool(&self) -> GroundSort<Self::Sort>

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

fn typecheck_function(
    &self,
    checker: &mut TypeChecker<Self::Sort>,
    f: &Self::Function,
    args: &[TypeRef<Self::Sort>],
    return_sort: TypeRef<Self::Sort>
)

Loading content...

Implementors

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

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>[src]

Find a sort.

fn sort_bool(&self) -> GroundSort<S>[src]

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

Loading content...