Enum Command

pub enum Command<'st> {
    Assert(&'st Term<'st>),
    CheckSat,
    CheckSatAssuming(&'st [PropLiteral<'st>]),
    DeclareConst(Symbol<'st>, Sort<'st>),
    DeclareDatatype(Symbol<'st>, DatatypeDec<'st>),
    DeclareDatatypes(&'st [SortDec<'st>], &'st [DatatypeDec<'st>]),
    DeclareFun(Symbol<'st>, &'st [Sort<'st>], Sort<'st>),
    DeclareSort(Symbol<'st>, Numeral<'st>),
    DefineFun(FunctionDef<'st>),
    DefineFunRec(FunctionDef<'st>),
    DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>]),
    DefineSort(Symbol<'st>, &'st [Symbol<'st>], Sort<'st>),
    Echo(&'st str),
    Exit,
    GetAssertions,
    GetAssignment,
    GetInfo(InfoFlag<'st>),
    GetModel,
    GetOption(Keyword<'st>),
    GetProof,
    GetUnsatAssumptions,
    GetUnsatCore,
    GetValue(&'st [&'st Term<'st>]),
    Pop(Numeral<'st>),
    Push(Numeral<'st>),
    Reset,
    ResetAssertions,
    SetInfo(Attribute<'st>),
    SetLogic(Symbol<'st>),
    SetOption(Option<'st>),
    Simplify(&'st Term<'st>),
}

Variants

Assert(&'st Term<'st>)

(assert <term>)

CheckSat

(check-sat)

CheckSatAssuming(&'st [PropLiteral<'st>])

(check-sat-assuming (<prop_literal>*))

DeclareConst(Symbol<'st>, Sort<'st>)

(declare-const <symbol> <sort>)

DeclareDatatype(Symbol<'st>, DatatypeDec<'st>)

(declare-datatype <symbol> <datatype_dec>)

DeclareDatatypes(&'st [SortDec<'st>], &'st [DatatypeDec<'st>])

(declare-datatypes (<sort_dec>n+1) (<datatype_dec>n+1))

DeclareFun(Symbol<'st>, &'st [Sort<'st>], Sort<'st>)

(declare-fun <symbol> (<sort>*) <sort>)

DeclareSort(Symbol<'st>, Numeral<'st>)

(declare-sort <symbol> <numeral>)

DefineFun(FunctionDef<'st>)

(define-fun <function_def>)

DefineFunRec(FunctionDef<'st>)

(define-fun-rec <function_def>)

DefineFunsRec(&'st [FunctionDec<'st>], &'st [&'st Term<'st>])

(define-funs-rec (<function_dec>n+1) (<term>n+1))

DefineSort(Symbol<'st>, &'st [Symbol<'st>], Sort<'st>)

(define-sort <symbol> (<symbol>*) <sort>)

Echo(&'st str)

(echo <string>)

Exit

(exit)

GetAssertions

(get-assertions)

GetAssignment

(get-assignment)

GetInfo(InfoFlag<'st>)

(get-info <info_flag>)

GetModel

(get-model)

GetOption(Keyword<'st>)

(get-option <keyword>)

GetProof

(get-proof)

GetUnsatAssumptions

(get-unsat-assumptions)

GetUnsatCore

(get-unsat-core)

GetValue(&'st [&'st Term<'st>])

(get-value (<term>+))

Pop(Numeral<'st>)

(pop <numeral>)

Push(Numeral<'st>)

(push <numeral>)

Reset

(reset)

ResetAssertions

(reset-assertions)

SetInfo(Attribute<'st>)

(set-info <attribute>)

SetLogic(Symbol<'st>)

(set-logic <symbol>)

SetOption(Option<'st>)

(set-option <option>)

Simplify(&'st Term<'st>)

(simplify <term>)

Implementations

impl<'st> Command<'st>

pub fn parse(st: &'st Storage, src: &str) -> Result<Command<'st>, ParseError>

impl<'st> Command<'st>

pub fn has_response(&self) -> bool

pub fn parse_response( &self, st: &'st Storage, response: &str, ) -> Result<Option<SpecificSuccessResponse<'st>>, ParseError>

Trait Implementations

impl<'st> Clone for Command<'st>

fn clone(&self) -> Command<'st>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'st> Debug for Command<'st>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Command<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'st> Hash for Command<'st>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<'st> PartialEq for Command<'st>

fn eq(&self, other: &Command<'st>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'st> Copy for Command<'st>

impl<'st> Eq for Command<'st>

impl<'st> StructuralPartialEq for Command<'st>