Struct smt2parser::concrete::SyntaxBuilder [−][src]
pub struct SyntaxBuilder;
Expand description
An implementation of Smt2Visitor
that returns concrete syntax values.
Trait Implementations
impl<Term, Symbol, Sort, Keyword, Constant, SExpr> CommandVisitor<Term, Symbol, Sort, Keyword, Constant, SExpr> for SyntaxBuilder
impl<Term, Symbol, Sort, Keyword, Constant, SExpr> CommandVisitor<Term, Symbol, Sort, Keyword, Constant, SExpr> for SyntaxBuilder
fn visit_declare_datatype(
&mut self,
symbol: Symbol,
datatype: DatatypeDec<Symbol, Sort>
) -> Result<Self::T, Self::E>
fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>
) -> Result<Self::T, Self::E>
fn visit_declare_fun(
&mut self,
symbol: Symbol,
parameters: Vec<Sort>,
sort: Sort
) -> Result<Self::T, Self::E>
fn visit_define_fun(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Result<Self::T, Self::E>
fn visit_define_fun_rec(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Result<Self::T, Self::E>
fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec<Symbol, Sort>, Term)>
) -> Result<Self::T, Self::E>
fn visit_define_sort(
&mut self,
symbol: Symbol,
parameters: Vec<Symbol>,
sort: Sort
) -> Result<Self::T, Self::E>
fn visit_set_info(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Result<Self::T, Self::E>
fn visit_set_option(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Result<Self::T, Self::E>
Returns the “default value” for a type. Read more
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
type T = QualIdentifier<Identifier, Sort>
fn visit_sorted_identifier(
&mut self,
identifier: Identifier,
sort: Sort
) -> Result<Self::T, Self::E>
type QualIdentifier = QualIdentifier
type T = Sort<Identifier<Symbol>>
fn visit_parameterized_sort(
&mut self,
identifier: Identifier<Symbol>,
parameters: Vec<Self::T>
) -> Result<Self::T, Self::E>
fn visit_fresh_symbol(
&mut self,
value: String,
_kind: SymbolKind
) -> Result<Self::T, Self::E>
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> for SyntaxBuilder
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> for SyntaxBuilder
fn visit_qual_identifier(
&mut self,
qual_identifier: QualIdentifier
) -> Result<Self::T, Self::E>
fn visit_application(
&mut self,
qual_identifier: QualIdentifier,
arguments: Vec<Self::T>
) -> Result<Self::T, Self::E>
fn visit_let(
&mut self,
var_bindings: Vec<(Symbol, Self::T)>,
term: Self::T
) -> Result<Self::T, Self::E>
fn visit_match(
&mut self,
term: Self::T,
cases: Vec<(Vec<Symbol>, Self::T)>
) -> Result<Self::T, Self::E>
fn visit_attributes(
&mut self,
term: Self::T,
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>
) -> Result<Self::T, Self::E>
Auto Trait Implementations
impl RefUnwindSafe for SyntaxBuilder
impl Send for SyntaxBuilder
impl Sync for SyntaxBuilder
impl Unpin for SyntaxBuilder
impl UnwindSafe for SyntaxBuilder
Blanket Implementations
Mutably borrows from an owned value. Read more