Enum 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.

DeclareDatatypes(Vec<SortDeclaration<E>>, Vec<UnresolvedDataTypeDeclaration<E>>)

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,

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

Execute the command on the given environment.

Trait Implementations

impl<E: Environment> Untypable for Command<E>

type Sort = <E as Environment>::Sort

type Environment = E

fn type_decoration( &mut self, checker: &mut TypeChecker<Self::Sort>, env: &Self::Environment, )