Struct smt2patch::Rewriter [−][src]
pub struct Rewriter { /* fields omitted */ }
Expand description
State of the SMT2 rewriter.
Implementations
Trait Implementations
type V = SyntaxBuilder
Delegate visitor
fn process_constant(
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Constant
[src]fn process_keyword(
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Keyword
[src]fn process_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::SExpr
) -> <Self::V as Smt2Visitor>::SExpr
[src]fn process_sort(
&mut self,
value: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Sort
[src]fn process_qual_identifier(
&mut self,
value: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::QualIdentifier
[src]fn process_term(
&mut self,
value: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Term
[src]fn process_command(
&mut self,
value: <Self::V as Smt2Visitor>::Command
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_decimal_constant(
&mut self,
value: Ratio<BigInt>
) -> <Self::V as Smt2Visitor>::Constant
[src]fn visit_hexadecimal_constant(
&mut self,
value: Vec<u8, Global>
) -> <Self::V as Smt2Visitor>::Constant
[src]fn visit_binary_constant(
&mut self,
value: Vec<bool, Global>
) -> <Self::V as Smt2Visitor>::Constant
[src]fn visit_bound_symbol(
&mut self,
value: String
) -> Result<<Self::V as Smt2Visitor>::Symbol, String>
[src]fn visit_constant_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::SExpr
[src]fn visit_symbol_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::SExpr
[src]fn visit_keyword_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::SExpr
[src]fn visit_application_s_expr(
&mut self,
values: Vec<<Self::V as Smt2Visitor>::SExpr, Global>
) -> <Self::V as Smt2Visitor>::SExpr
[src]fn visit_simple_sort(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::Sort
[src]fn visit_parameterized_sort(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
parameters: Vec<<Self::V as Smt2Visitor>::Sort, Global>
) -> <Self::V as Smt2Visitor>::Sort
[src]fn visit_simple_identifier(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::QualIdentifier
[src]fn visit_sorted_identifier(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::QualIdentifier
[src]fn visit_constant(
&mut self,
constant: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_qual_identifier(
&mut self,
qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_application(
&mut self,
qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier,
arguments: Vec<<Self::V as Smt2Visitor>::Term, Global>
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_let(
&mut self,
var_bindings: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Term), Global>,
term: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_exists(
&mut self,
vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort), Global>,
term: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_match(
&mut self,
term: <Self::V as Smt2Visitor>::Term,
cases: Vec<(Vec<<Self::V as Smt2Visitor>::Symbol, Global>, <Self::V as Smt2Visitor>::Term), Global>
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_attributes(
&mut self,
term: <Self::V as Smt2Visitor>::Term,
attributes: Vec<(<Self::V as Smt2Visitor>::Keyword, AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>), Global>
) -> <Self::V as Smt2Visitor>::Term
[src]fn visit_check_sat_assuming(
&mut self,
literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool), Global>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_declare_const(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_declare_datatype(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
datatype: DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_declare_datatypes(
&mut self,
datatypes: Vec<(<Self::V as Smt2Visitor>::Symbol, BigUint, DatatypeDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>), Global>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_declare_fun(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
parameters: Vec<<Self::V as Smt2Visitor>::Sort, Global>,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_declare_sort(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
arity: BigUint
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_define_fun(
&mut self,
sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>,
term: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_define_fun_rec(
&mut self,
sig: FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>,
term: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_define_funs_rec(
&mut self,
funs: Vec<(FunctionDec<<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort>, <Self::V as Smt2Visitor>::Term), Global>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_define_sort(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
parameters: Vec<<Self::V as Smt2Visitor>::Symbol, Global>,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_get_info(
&mut self,
flag: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_get_option(
&mut self,
keyword: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_get_value(
&mut self,
terms: Vec<<Self::V as Smt2Visitor>::Term, Global>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_set_info(
&mut self,
keyword: <Self::V as Smt2Visitor>::Keyword,
value: AttributeValue<<Self::V as Smt2Visitor>::Constant, <Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::SExpr>
) -> <Self::V as Smt2Visitor>::Command
[src]fn visit_set_logic(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::Command
[src]Auto Trait Implementations
impl RefUnwindSafe for Rewriter
impl UnwindSafe for Rewriter
Blanket Implementations
Mutably borrows from an owned value. Read more
type T = <V as Smt2Visitor>::Constant
pub fn visit_hexadecimal_constant(
&mut self,
value: Vec<u8, Global>
) -> <R as ConstantVisitor>::T
[src]pub fn visit_binary_constant(
&mut self,
value: Vec<bool, Global>
) -> <R as ConstantVisitor>::T
[src]type T = <V as Smt2Visitor>::Keyword
type Constant = <V as Smt2Visitor>::Constant
type QualIdentifier = <V as Smt2Visitor>::QualIdentifier
type Keyword = <V as Smt2Visitor>::Keyword
type Sort = <V as Smt2Visitor>::Sort
type SExpr = <V as Smt2Visitor>::SExpr
type Symbol = <V as Smt2Visitor>::Symbol
type Term = <V as Smt2Visitor>::Term
type Command = <V as Smt2Visitor>::Command
type T = <V as Smt2Visitor>::Symbol
pub fn visit_bound_symbol(
&mut self,
value: String
) -> Result<<R as SymbolVisitor>::T, String>
[src]