Struct smt2patch::Rewriter [−][src]
pub struct Rewriter { /* fields omitted */ }
State of the SMT2 rewriter.
Implementations
impl Rewriter
[src]
pub fn new(config: RewriterConfig, discarded_options: HashSet<String>) -> Self
[src]
Trait Implementations
impl Debug for Rewriter
[src]
impl Rewriter for Rewriter
[src]
type V = SyntaxBuilder
fn visitor(&mut self) -> &mut SyntaxBuilder
[src]
fn process_symbol(&mut self, symbol: Symbol) -> Symbol
[src]
fn visit_forall(&mut self, vars: Vec<(Symbol, Sort)>, term: Term) -> Term
[src]
fn visit_assert(&mut self, term: Term) -> Command
[src]
fn visit_set_option(
&mut self,
keyword: Keyword,
value: AttributeValue
) -> Command
[src]
&mut self,
keyword: Keyword,
value: AttributeValue
) -> Command
fn visit_get_unsat_core(&mut self) -> Command
[src]
pub fn process_constant(
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Constant
pub fn process_keyword(
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Keyword
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Keyword
pub fn process_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::SExpr
) -> <Self::V as Smt2Visitor>::SExpr
[src]
&mut self,
value: <Self::V as Smt2Visitor>::SExpr
) -> <Self::V as Smt2Visitor>::SExpr
pub fn process_sort(
&mut self,
value: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Sort
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Sort
pub fn process_qual_identifier(
&mut self,
value: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::QualIdentifier
[src]
&mut self,
value: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::QualIdentifier
pub fn process_term(
&mut self,
value: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Term
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Term
) -> <Self::V as Smt2Visitor>::Term
pub fn process_command(
&mut self,
value: <Self::V as Smt2Visitor>::Command
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Command
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_numeral_constant(
&mut self,
value: BigUint
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: BigUint
) -> <Self::V as Smt2Visitor>::Constant
pub fn visit_decimal_constant(
&mut self,
value: Ratio<BigInt>
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: Ratio<BigInt>
) -> <Self::V as Smt2Visitor>::Constant
pub fn visit_hexadecimal_constant(
&mut self,
value: Vec<u8, Global>
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: Vec<u8, Global>
) -> <Self::V as Smt2Visitor>::Constant
pub fn visit_binary_constant(
&mut self,
value: Vec<bool, Global>
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: Vec<bool, Global>
) -> <Self::V as Smt2Visitor>::Constant
pub fn visit_string_constant(
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Constant
[src]
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Constant
pub fn visit_symbol(
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Symbol
[src]
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Symbol
pub fn visit_keyword(
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Keyword
[src]
&mut self,
value: String
) -> <Self::V as Smt2Visitor>::Keyword
pub fn visit_constant_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::SExpr
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::SExpr
pub fn visit_symbol_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::SExpr
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::SExpr
pub fn visit_keyword_s_expr(
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::SExpr
[src]
&mut self,
value: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::SExpr
pub fn visit_application_s_expr(
&mut self,
values: Vec<<Self::V as Smt2Visitor>::SExpr, Global>
) -> <Self::V as Smt2Visitor>::SExpr
[src]
&mut self,
values: Vec<<Self::V as Smt2Visitor>::SExpr, Global>
) -> <Self::V as Smt2Visitor>::SExpr
pub fn visit_simple_sort(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::Sort
[src]
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::Sort
pub 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]
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
parameters: Vec<<Self::V as Smt2Visitor>::Sort, Global>
) -> <Self::V as Smt2Visitor>::Sort
pub fn visit_simple_identifier(
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::QualIdentifier
[src]
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>
) -> <Self::V as Smt2Visitor>::QualIdentifier
pub 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]
&mut self,
identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::QualIdentifier
pub fn visit_constant(
&mut self,
constant: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Term
[src]
&mut self,
constant: <Self::V as Smt2Visitor>::Constant
) -> <Self::V as Smt2Visitor>::Term
pub fn visit_qual_identifier(
&mut self,
qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::Term
[src]
&mut self,
qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier
) -> <Self::V as Smt2Visitor>::Term
pub 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]
&mut self,
qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier,
arguments: Vec<<Self::V as Smt2Visitor>::Term, Global>
) -> <Self::V as Smt2Visitor>::Term
pub 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]
&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
pub 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]
&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
pub 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]
&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
pub 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]
&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
pub fn visit_check_sat(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_check_sat_assuming(
&mut self,
literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool), Global>
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool), Global>
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_declare_const(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
sort: <Self::V as Smt2Visitor>::Sort
) -> <Self::V as Smt2Visitor>::Command
pub 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]
&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
pub 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]
&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
pub 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]
&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
pub fn visit_declare_sort(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
arity: BigUint
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol,
arity: BigUint
) -> <Self::V as Smt2Visitor>::Command
pub 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]
&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
pub 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]
&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
pub 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]
&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
pub 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]
&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
pub fn visit_echo(
&mut self,
message: String
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
message: String
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_exit(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_get_assertions(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_get_assignment(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_get_info(
&mut self,
flag: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
flag: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_get_model(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_get_option(
&mut self,
keyword: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
keyword: <Self::V as Smt2Visitor>::Keyword
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_get_proof(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_get_unsat_assumptions(
&mut self
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_get_value(
&mut self,
terms: Vec<<Self::V as Smt2Visitor>::Term, Global>
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
terms: Vec<<Self::V as Smt2Visitor>::Term, Global>
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_pop(&mut self, level: BigUint) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_push(
&mut self,
level: BigUint
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
level: BigUint
) -> <Self::V as Smt2Visitor>::Command
pub fn visit_reset(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub fn visit_reset_assertions(&mut self) -> <Self::V as Smt2Visitor>::Command
[src]
pub 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]
&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
pub fn visit_set_logic(
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::Command
[src]
&mut self,
symbol: <Self::V as Smt2Visitor>::Symbol
) -> <Self::V as Smt2Visitor>::Command
Auto Trait Implementations
impl RefUnwindSafe for Rewriter
impl Send for Rewriter
impl Sync for Rewriter
impl Unpin for Rewriter
impl UnwindSafe for Rewriter
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<R, V> ConstantVisitor for R where
V: Smt2Visitor,
R: Rewriter<V = V>,
[src]
V: Smt2Visitor,
R: Rewriter<V = V>,
type T = <V as Smt2Visitor>::Constant
pub fn visit_numeral_constant(
&mut self,
value: BigUint
) -> <R as ConstantVisitor>::T
[src]
&mut self,
value: BigUint
) -> <R as ConstantVisitor>::T
pub fn visit_decimal_constant(
&mut self,
value: Ratio<BigInt>
) -> <R as ConstantVisitor>::T
[src]
&mut self,
value: Ratio<BigInt>
) -> <R as ConstantVisitor>::T
pub fn visit_hexadecimal_constant(
&mut self,
value: Vec<u8, Global>
) -> <R as ConstantVisitor>::T
[src]
&mut self,
value: Vec<u8, Global>
) -> <R as ConstantVisitor>::T
pub fn visit_binary_constant(
&mut self,
value: Vec<bool, Global>
) -> <R as ConstantVisitor>::T
[src]
&mut self,
value: Vec<bool, Global>
) -> <R as ConstantVisitor>::T
pub fn visit_string_constant(
&mut self,
value: String
) -> <R as ConstantVisitor>::T
[src]
&mut self,
value: String
) -> <R as ConstantVisitor>::T
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<R, V> KeywordVisitor for R where
V: Smt2Visitor,
R: Rewriter<V = V>,
[src]
V: Smt2Visitor,
R: Rewriter<V = V>,
type T = <V as Smt2Visitor>::Keyword
pub fn visit_keyword(&mut self, value: String) -> <R as KeywordVisitor>::T
[src]
impl<R, V> Smt2Visitor for R where
V: Smt2Visitor,
R: Rewriter<V = V>,
[src]
V: Smt2Visitor,
R: Rewriter<V = V>,
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
impl<R, V> SymbolVisitor for R where
V: Smt2Visitor,
R: Rewriter<V = V>,
[src]
V: Smt2Visitor,
R: Rewriter<V = V>,
type T = <V as Smt2Visitor>::Symbol
pub fn visit_symbol(&mut self, value: String) -> <R as SymbolVisitor>::T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,