Enum smt2parser::concrete::Command

pub enum Command {
    Assert {
        term: Term,
    },
    CheckSat,
    CheckSatAssuming {
        literals: Vec<(Symbol, bool)>,
    },
    DeclareConst {
        symbol: Symbol,
        sort: Sort,
    },
    DeclareDatatype {
        symbol: Symbol,
        datatype: DatatypeDec,
    },
    DeclareDatatypes {
        datatypes: Vec<(Symbol, Numeral, DatatypeDec)>,
    },
    DeclareFun {
        symbol: Symbol,
        parameters: Vec<Sort>,
        sort: Sort,
    },
    DeclareSort {
        symbol: Symbol,
        arity: Numeral,
    },
    DefineFun {
        sig: FunctionDec,
        term: Term,
    },
    DefineFunRec {
        sig: FunctionDec,
        term: Term,
    },
    DefineFunsRec {
        funs: Vec<(FunctionDec, 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,
    },
    SetLogic {
        symbol: Symbol,
    },
    SetOption {
        keyword: Keyword,
        value: AttributeValue,
    },
}

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

DeclareDatatypes

Fields of DeclareDatatypes

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

DeclareFun

Fields of DeclareFun

symbol: Symbolparameters: Vec<Sort>sort: Sort

DeclareSort

Fields of DeclareSort

symbol: Symbolarity: Numeral

DefineFun

Fields of DefineFun

sig: FunctionDecterm: Term

DefineFunRec

Fields of DefineFunRec

sig: FunctionDecterm: Term

DefineFunsRec

Fields of DefineFunsRec

funs: Vec<(FunctionDec, 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

SetLogic

Fields of SetLogic

symbol: Symbol

SetOption

Fields of SetOption

keyword: Keywordvalue: AttributeValue

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 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, 

Feeds a slice of this type into the given Hasher.

impl PartialEq<Command> 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: &Command) -> bool

This method tests for !=.

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

impl StructuralPartialEq for Command