Enum smtlib_lowlevel::ast::Command

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

Variants

Assert(Term)

(assert <term>)

CheckSat

(check-sat)

CheckSatAssuming(Vec<PropLiteral>)

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

DeclareConst(Symbol, Sort)

(declare-const <symbol> <sort>)

DeclareDatatype(Symbol, DatatypeDec)

(declare-datatype <symbol> <datatype_dec>)

DeclareDatatypes(Vec<SortDec>, Vec<DatatypeDec>)

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

DeclareFun(Symbol, Vec<Sort>, Sort)

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

DeclareSort(Symbol, Numeral)

(declare-sort <symbol> <numeral>)

DefineFun(FunctionDef)

(define-fun <function_def>)

DefineFunRec(FunctionDef)

(define-fun-rec <function_def>)

DefineFunsRec(Vec<FunctionDec>, Vec<Term>)

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

DefineSort(Symbol, Vec<Symbol>, Sort)

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

Echo(String)

(echo <string>)

Exit

(exit)

GetAssertions

(get-assertions)

GetAssignment

(get-assignment)

GetInfo(InfoFlag)

(get-info <info_flag>)

GetModel

(get-model)

GetOption(Keyword)

(get-option <keyword>)

GetProof

(get-proof)

GetUnsatAssumptions

(get-unsat-assumptions)

GetUnsatCore

(get-unsat-core)

GetValue(Vec<Term>)

(get-value (<term>+))

Pop(Numeral)

(pop <numeral>)

Push(Numeral)

(push <numeral>)

Reset

(reset)

ResetAssertions

(reset-assertions)

SetInfo(Attribute)

(set-info <attribute>)

SetLogic(Symbol)

(set-logic <symbol>)

SetOption(Option)

(set-option <option>)

Simplify(Term)

(simplify <term>)

Implementations

impl Command

pub fn parse(src: &str) -> Result<Self, ParseError>

impl Command

pub fn has_response(&self) -> bool

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

Trait Implementations

impl Clone for Command

fn clone(&self) -> Command

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Command

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Command

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for Command

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

Formats the value using the given formatter.

impl Hash for Command

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 PartialEq for Command

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

This method tests for self and other values to be equal, and is used by ==.

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

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

impl Serialize for Command

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for Command

impl StructuralPartialEq for Command