[−][src]Enum smt2::Command

pub enum Command<E: Environment> {
    Assert(Typed<Term<E>>),
    CheckSat,
    DeclareConst(E::Ident, GroundSort<E::Sort>),
    DeclareDatatypes(Vec<SortDeclaration<E>>, Vec<UnresolvedDataTypeDeclaration<E>>),
    DeclareFun(E::Ident, Vec<GroundSort<E::Sort>>, GroundSort<E::Sort>),
    Exit,
    GetModel,
    SetLogic(E::Logic),
}

SMT2-lib command.

Variants

Assert(Typed<Term<E>>)

Assertion.

CheckSat

Check sat.

DeclareConst(E::Ident, GroundSort<E::Sort>)

Declare a cosntant.

Declare new datatypes. The declare-datatype is desigarized into declare-datatypes.

DeclareFun(E::Ident, Vec<GroundSort<E::Sort>>, GroundSort<E::Sort>)

Declare a new uninterpreted function.

Exit

Exit the program.

GetModel

Get a model.

SetLogic(E::Logic)

Set the solver logic.

Implementations

impl<E: Server> Command<E> where
    E::Constant: Display,
    E::Ident: Display,
    E::Function: Display,
    E::Sort: Display, [src]

pub fn exec(self, env: &mut E) -> ExecResult<(), E::Error>[src]

Execute the command on the given environment.

Trait Implementations

impl<E: Environment> Untypable for Command<E>[src]

type Sort = E::Sort

type Environment = E

Auto Trait Implementations

impl<E> RefUnwindSafe for Command<E> where
    <E as Environment>::Constant: RefUnwindSafe,
    <E as Environment>::Function: RefUnwindSafe,
    <E as Environment>::Ident: RefUnwindSafe,
    <E as Environment>::Logic: RefUnwindSafe,
    <E as Environment>::Sort: RefUnwindSafe, 

impl<E> Send for Command<E> where
    <E as Environment>::Constant: Send,
    <E as Environment>::Function: Send,
    <E as Environment>::Ident: Send,
    <E as Environment>::Logic: Send,
    <E as Environment>::Sort: Send, 

impl<E> Sync for Command<E> where
    <E as Environment>::Constant: Sync,
    <E as Environment>::Function: Sync,
    <E as Environment>::Ident: Sync,
    <E as Environment>::Logic: Sync,
    <E as Environment>::Sort: Sync, 

impl<E> Unpin for Command<E> where
    <E as Environment>::Constant: Unpin,
    <E as Environment>::Function: Unpin,
    <E as Environment>::Ident: Unpin,
    <E as Environment>::Logic: Unpin,
    <E as Environment>::Sort: Unpin, 

impl<E> UnwindSafe for Command<E> where
    <E as Environment>::Constant: UnwindSafe,
    <E as Environment>::Function: UnwindSafe,
    <E as Environment>::Ident: UnwindSafe,
    <E as Environment>::Logic: UnwindSafe,
    <E as Environment>::Sort: UnwindSafe, 

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized, [src]

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.