Trait smt2parser::visitors::CommandVisitor [−][src]
pub trait CommandVisitor<Term, Symbol, Sort, Keyword, Constant, SExpr> { type T;}Show methods
fn visit_assert(&mut self, term: Term) -> Self::T; fn visit_check_sat(&mut self) -> Self::T; fn visit_check_sat_assuming(
&mut self,
literals: Vec<(Symbol, bool)>
) -> Self::T; fn visit_declare_const(&mut self, symbol: Symbol, sort: Sort) -> Self::T; fn visit_declare_datatype(
&mut self,
symbol: Symbol,
datatype: DatatypeDec<Symbol, Sort>
) -> Self::T; fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>
) -> Self::T; fn visit_declare_fun(
&mut self,
symbol: Symbol,
parameters: Vec<Sort>,
sort: Sort
) -> Self::T; fn visit_declare_sort(&mut self, symbol: Symbol, arity: Numeral) -> Self::T; fn visit_define_fun(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Self::T; fn visit_define_fun_rec(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Self::T; fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec<Symbol, Sort>, Term)>
) -> Self::T; fn visit_define_sort(
&mut self,
symbol: Symbol,
parameters: Vec<Symbol>,
sort: Sort
) -> Self::T; fn visit_echo(&mut self, message: String) -> Self::T; fn visit_exit(&mut self) -> Self::T; fn visit_get_assertions(&mut self) -> Self::T; fn visit_get_assignment(&mut self) -> Self::T; fn visit_get_info(&mut self, flag: Keyword) -> Self::T; fn visit_get_model(&mut self) -> Self::T; fn visit_get_option(&mut self, keyword: Keyword) -> Self::T; fn visit_get_proof(&mut self) -> Self::T; fn visit_get_unsat_assumptions(&mut self) -> Self::T; fn visit_get_unsat_core(&mut self) -> Self::T; fn visit_get_value(&mut self, terms: Vec<Term>) -> Self::T; fn visit_pop(&mut self, level: Numeral) -> Self::T; fn visit_push(&mut self, level: Numeral) -> Self::T; fn visit_reset(&mut self) -> Self::T; fn visit_reset_assertions(&mut self) -> Self::T; fn visit_set_info(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Self::T; fn visit_set_logic(&mut self, symbol: Symbol) -> Self::T; fn visit_set_option(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Self::T;
Associated Types
Required methods
fn visit_assert(&mut self, term: Term) -> Self::T
[src]fn visit_check_sat(&mut self) -> Self::T
[src]fn visit_declare_const(&mut self, symbol: Symbol, sort: Sort) -> Self::T
[src]fn visit_declare_datatype(
&mut self,
symbol: Symbol,
datatype: DatatypeDec<Symbol, Sort>
) -> Self::T
[src]fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(Symbol, Numeral, DatatypeDec<Symbol, Sort>)>
) -> Self::T
[src]fn visit_declare_fun(
&mut self,
symbol: Symbol,
parameters: Vec<Sort>,
sort: Sort
) -> Self::T
[src]fn visit_declare_sort(&mut self, symbol: Symbol, arity: Numeral) -> Self::T
[src]fn visit_define_fun(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Self::T
[src]fn visit_define_fun_rec(
&mut self,
sig: FunctionDec<Symbol, Sort>,
term: Term
) -> Self::T
[src]fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec<Symbol, Sort>, Term)>
) -> Self::T
[src]fn visit_define_sort(
&mut self,
symbol: Symbol,
parameters: Vec<Symbol>,
sort: Sort
) -> Self::T
[src]fn visit_echo(&mut self, message: String) -> Self::T
[src]fn visit_exit(&mut self) -> Self::T
[src]fn visit_get_assertions(&mut self) -> Self::T
[src]fn visit_get_assignment(&mut self) -> Self::T
[src]fn visit_get_info(&mut self, flag: Keyword) -> Self::T
[src]fn visit_get_model(&mut self) -> Self::T
[src]fn visit_get_option(&mut self, keyword: Keyword) -> Self::T
[src]fn visit_get_proof(&mut self) -> Self::T
[src]fn visit_get_unsat_assumptions(&mut self) -> Self::T
[src]fn visit_get_unsat_core(&mut self) -> Self::T
[src]fn visit_get_value(&mut self, terms: Vec<Term>) -> Self::T
[src]fn visit_push(&mut self, level: Numeral) -> Self::T
[src]fn visit_reset(&mut self) -> Self::T
[src]fn visit_reset_assertions(&mut self) -> Self::T
[src]fn visit_set_info(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Self::T
[src]fn visit_set_logic(&mut self, symbol: Symbol) -> Self::T
[src]fn visit_set_option(
&mut self,
keyword: Keyword,
value: AttributeValue<Constant, Symbol, SExpr>
) -> Self::T
[src]Implementors
impl<R, V> CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
[src]
impl<R, V> CommandVisitor<<V as Smt2Visitor>::Term, <V as Smt2Visitor>::Symbol, <V as Smt2Visitor>::Sort, <V as Smt2Visitor>::Keyword, <V as Smt2Visitor>::Constant, <V as Smt2Visitor>::SExpr> for R where
R: Rewriter<V = V>,
V: Smt2Visitor,
[src]fn visit_declare_datatype(
&mut self,
symbol: V::Symbol,
datatype: DatatypeDec<V::Symbol, V::Sort>
) -> Self::T
[src]fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(V::Symbol, Numeral, DatatypeDec<V::Symbol, V::Sort>)>
) -> Self::T
[src]fn visit_declare_fun(
&mut self,
symbol: V::Symbol,
parameters: Vec<V::Sort>,
sort: V::Sort
) -> Self::T
[src]fn visit_define_fun(
&mut self,
sig: FunctionDec<V::Symbol, V::Sort>,
term: V::Term
) -> Self::T
[src]fn visit_define_fun_rec(
&mut self,
sig: FunctionDec<V::Symbol, V::Sort>,
term: V::Term
) -> Self::T
[src]fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec<V::Symbol, V::Sort>, V::Term)>
) -> Self::T
[src]fn visit_define_sort(
&mut self,
symbol: V::Symbol,
parameters: Vec<V::Symbol>,
sort: V::Sort
) -> Self::T
[src]fn visit_set_info(
&mut self,
keyword: V::Keyword,
value: AttributeValue<V::Constant, V::Symbol, V::SExpr>
) -> Self::T
[src]fn visit_set_option(
&mut self,
keyword: V::Keyword,
value: AttributeValue<V::Constant, V::Symbol, V::SExpr>
) -> Self::T
[src]