Enum smt2parser::concrete::Command

pub enum Command<Term = Term, Symbol = Symbol, Sort = Sort, Keyword = Keyword, Constant = Constant, SExpr = SExpr> {
    Assert {
        term: Term,
    },
    CheckSat,
    CheckSatAssuming {
        literals: Vec<(Symbol, bool)>,
    },
    DeclareConst {
        symbol: Symbol,
        sort: Sort,
    },
    DeclareDatatype {
        symbol: Symbol,
        datatype: DatatypeDec<Symbol, Sort>,
    },
    DeclareDatatypes {
        datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>,
    },
    DeclareFun {
        symbol: Symbol,
        parameters: Vec<Sort>,
        sort: Sort,
    },
    DeclareSort {
        symbol: Symbol,
        arity: Numeral,
    },
    DefineFun {
        sig: FunctionDec<Symbol, Sort>,
        term: Term,
    },
    DefineFunRec {
        sig: FunctionDec<Symbol, Sort>,
        term: Term,
    },
    DefineFunsRec {
        funs: Vec<(FunctionDec<Symbol, Sort>, Term)>,
    },
    DefineSort {
        symbol: Symbol,
        parameters: Vec<Symbol>,
        sort: Sort,
    },
    Echo {
        message: String,
    },
    Exit,
    GetAssertions,
    GetAssignment,
    GetInfo {
        flag: Keyword,
    },
    GetModel,
    GetOption {
        keyword: Keyword,
    },
    GetProof,
    GetUnsatAssumptions,
    GetUnsatCore,
    GetValue {
        terms: Vec<Term>,
    },
    Pop {
        level: Numeral,
    },
    Push {
        level: Numeral,
    },
    Reset,
    ResetAssertions,
    SetInfo {
        keyword: Keyword,
        value: AttributeValue<Constant, Symbol, SExpr>,
    },
    SetLogic {
        symbol: Symbol,
    },
    SetOption {
        keyword: Keyword,
        value: AttributeValue<Constant, Symbol, SExpr>,
    },
}

Concrete syntax for a command.

Variants

Assert

Fields of Assert

term: Term

CheckSat

CheckSatAssuming

Fields of CheckSatAssuming

literals: Vec<(Symbol, bool)>

DeclareConst

Fields of DeclareConst

symbol: Symbolsort: Sort

DeclareDatatype

Fields of DeclareDatatype

symbol: Symboldatatype: DatatypeDec<Symbol, Sort>

DeclareDatatypes

Fields of DeclareDatatypes

datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>

DeclareFun

Fields of DeclareFun

symbol: Symbolparameters: Vec<Sort>sort: Sort

DeclareSort

Fields of DeclareSort

symbol: Symbolarity: Numeral

DefineFun

Fields of DefineFun

sig: FunctionDec<Symbol, Sort>term: Term

DefineFunRec

Fields of DefineFunRec

sig: FunctionDec<Symbol, Sort>term: Term

DefineFunsRec

Fields of DefineFunsRec

funs: Vec<(FunctionDec<Symbol, Sort>, Term)>

DefineSort

Fields of DefineSort

symbol: Symbolparameters: Vec<Symbol>sort: Sort

Echo

Fields of Echo

message: String

Exit

GetAssertions

GetAssignment

GetInfo

Fields of GetInfo

flag: Keyword

GetModel

GetOption

Fields of GetOption

keyword: Keyword

GetProof

GetUnsatAssumptions

GetUnsatCore

GetValue

Fields of GetValue

terms: Vec<Term>

Pop

Fields of Pop

level: Numeral

Push

Fields of Push

level: Numeral

Reset

ResetAssertions

SetInfo

Fields of SetInfo

keyword: Keywordvalue: AttributeValue<Constant, Symbol, SExpr>

SetLogic

Fields of SetLogic

symbol: Symbol

SetOption

Fields of SetOption

keyword: Keywordvalue: AttributeValue<Constant, Symbol, SExpr>

Implementations

impl Command

pub fn accept<V, T, E, S1, S2, S3, S4, S5, S6, S7>(
    self,
    visitor: &mut V
) -> Result<T, E> where
    V: SortVisitor<S1, T = S2, E = E> + SymbolVisitor<T = S1, E = E> + QualIdentifierVisitor<Identifier<S1>, S2, T = S3, E = E> + ConstantVisitor<T = S4, E = E> + KeywordVisitor<T = S5, E = E> + SExprVisitor<S4, S1, S5, T = S6, E = E> + TermVisitor<S4, S3, S5, S6, S1, S2, T = S7, E = E> + CommandVisitor<S7, S1, S2, S5, S4, S6, T = T, E = E>, 

Visit a concrete command.

Trait Implementations

impl<Term: Clone, Symbol: Clone, Sort: Clone, Keyword: Clone, Constant: Clone, SExpr: Clone> Clone for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

fn clone(&self) -> Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Term: Debug, Symbol: Debug, Sort: Debug, Keyword: Debug, Constant: Debug, SExpr: Debug> Debug for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

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

Formats the value using the given formatter.

impl<'de, Term, Symbol, Sort, Keyword, Constant, SExpr> Deserialize<'de> for Command<Term, Symbol, Sort, Keyword, Constant, SExpr> where
    Term: Deserialize<'de>,
    Symbol: Deserialize<'de>,
    Sort: Deserialize<'de>,
    Keyword: Deserialize<'de>,
    Constant: Deserialize<'de>,
    SExpr: Deserialize<'de>, 

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
    __D: Deserializer<'de>, 

Deserialize this value from the given Serde deserializer.

impl<Term, Symbol, Sort, Keyword, Constant, SExpr> Display for Command<Term, Symbol, Sort, Keyword, Constant, SExpr> where
    Term: Display,
    Symbol: Display,
    Sort: Display,
    Keyword: Display,
    Constant: Display,
    SExpr: Display, 

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

Formats the value using the given formatter.

impl<Term: Hash, Symbol: Hash, Sort: Hash, Keyword: Hash, Constant: Hash, SExpr: Hash> Hash for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

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, 

Feeds a slice of this type into the given Hasher.

impl<Term: PartialEq, Symbol: PartialEq, Sort: PartialEq, Keyword: PartialEq, Constant: PartialEq, SExpr: PartialEq> PartialEq<Command<Term, Symbol, Sort, Keyword, Constant, SExpr>> for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

fn eq(
    &self,
    other: &Command<Term, Symbol, Sort, Keyword, Constant, SExpr>
) -> bool

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

fn ne(
    &self,
    other: &Command<Term, Symbol, Sort, Keyword, Constant, SExpr>
) -> bool

This method tests for !=.

impl<Term, Symbol, Sort, Keyword, Constant, SExpr> Serialize for Command<Term, Symbol, Sort, Keyword, Constant, SExpr> where
    Term: Serialize,
    Symbol: Serialize,
    Sort: Serialize,
    Keyword: Serialize,
    Constant: Serialize,
    SExpr: Serialize, 

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

Serialize this value into the given Serde serializer.

impl<Term: Eq, Symbol: Eq, Sort: Eq, Keyword: Eq, Constant: Eq, SExpr: Eq> Eq for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

impl<Term, Symbol, Sort, Keyword, Constant, SExpr> StructuralEq for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>

impl<Term, Symbol, Sort, Keyword, Constant, SExpr> StructuralPartialEq for Command<Term, Symbol, Sort, Keyword, Constant, SExpr>