Struct Rewriter

pub struct Rewriter { /* private fields */ }

State of the SMT2 rewriter.

Implementations

impl Rewriter

pub fn new(config: RewriterConfig, discarded_options: HashSet<String>) -> Self

Trait Implementations

impl Debug for Rewriter

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Rewriter for Rewriter

type V = SyntaxBuilder

fn visitor(&mut self) -> &mut SyntaxBuilder

Delegate visitor

fn process_symbol(&mut self, symbol: Symbol) -> Symbol

fn visit_forall(&mut self, vars: Vec<(Symbol, Sort)>, term: Term) -> Term

fn visit_assert(&mut self, term: Term) -> Command

fn visit_set_option( &mut self, keyword: Keyword, value: AttributeValue, ) -> Command

fn visit_get_unsat_core(&mut self) -> Command

fn process_constant( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> <Self::V as Smt2Visitor>::Constant

fn process_keyword( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> <Self::V as Smt2Visitor>::Keyword

fn process_s_expr( &mut self, value: <Self::V as Smt2Visitor>::SExpr, ) -> <Self::V as Smt2Visitor>::SExpr

fn process_sort( &mut self, value: <Self::V as Smt2Visitor>::Sort, ) -> <Self::V as Smt2Visitor>::Sort

fn process_qual_identifier( &mut self, value: <Self::V as Smt2Visitor>::QualIdentifier, ) -> <Self::V as Smt2Visitor>::QualIdentifier

fn process_term( &mut self, value: <Self::V as Smt2Visitor>::Term, ) -> <Self::V as Smt2Visitor>::Term

fn process_command( &mut self, value: <Self::V as Smt2Visitor>::Command, ) -> <Self::V as Smt2Visitor>::Command

fn visit_numeral_constant( &mut self, value: BigUint, ) -> <Self::V as Smt2Visitor>::Constant

fn visit_decimal_constant( &mut self, value: Ratio<BigInt>, ) -> <Self::V as Smt2Visitor>::Constant

fn visit_hexadecimal_constant( &mut self, value: Vec<u8>, ) -> <Self::V as Smt2Visitor>::Constant

fn visit_binary_constant( &mut self, value: Vec<bool>, ) -> <Self::V as Smt2Visitor>::Constant

fn visit_string_constant( &mut self, value: String, ) -> <Self::V as Smt2Visitor>::Constant

fn visit_bound_symbol( &mut self, value: String, ) -> Result<<Self::V as Smt2Visitor>::Symbol, String>

fn visit_fresh_symbol( &mut self, value: String, ) -> <Self::V as Smt2Visitor>::Symbol

fn visit_any_symbol( &mut self, value: String, ) -> <Self::V as Smt2Visitor>::Symbol

fn bind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol)

fn unbind_symbol(&mut self, symbol: &<Self::V as Smt2Visitor>::Symbol)

fn visit_keyword(&mut self, value: String) -> <Self::V as Smt2Visitor>::Keyword

fn visit_constant_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Constant, ) -> <Self::V as Smt2Visitor>::SExpr

fn visit_symbol_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Symbol, ) -> <Self::V as Smt2Visitor>::SExpr

fn visit_keyword_s_expr( &mut self, value: <Self::V as Smt2Visitor>::Keyword, ) -> <Self::V as Smt2Visitor>::SExpr

fn visit_application_s_expr( &mut self, values: Vec<<Self::V as Smt2Visitor>::SExpr>, ) -> <Self::V as Smt2Visitor>::SExpr

fn visit_simple_sort( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> <Self::V as Smt2Visitor>::Sort

fn visit_parameterized_sort( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, parameters: Vec<<Self::V as Smt2Visitor>::Sort>, ) -> <Self::V as Smt2Visitor>::Sort

fn visit_simple_identifier( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, ) -> <Self::V as Smt2Visitor>::QualIdentifier

fn visit_sorted_identifier( &mut self, identifier: Identifier<<Self::V as Smt2Visitor>::Symbol>, sort: <Self::V as Smt2Visitor>::Sort, ) -> <Self::V as Smt2Visitor>::QualIdentifier

fn visit_constant( &mut self, constant: <Self::V as Smt2Visitor>::Constant, ) -> <Self::V as Smt2Visitor>::Term

fn visit_qual_identifier( &mut self, qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier, ) -> <Self::V as Smt2Visitor>::Term

fn visit_application( &mut self, qual_identifier: <Self::V as Smt2Visitor>::QualIdentifier, arguments: Vec<<Self::V as Smt2Visitor>::Term>, ) -> <Self::V as Smt2Visitor>::Term

fn visit_let( &mut self, var_bindings: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Term)>, term: <Self::V as Smt2Visitor>::Term, ) -> <Self::V as Smt2Visitor>::Term

fn visit_exists( &mut self, vars: Vec<(<Self::V as Smt2Visitor>::Symbol, <Self::V as Smt2Visitor>::Sort)>, term: <Self::V as Smt2Visitor>::Term, ) -> <Self::V as Smt2Visitor>::Term

fn visit_match( &mut self, term: <Self::V as Smt2Visitor>::Term, cases: Vec<(Vec<<Self::V as Smt2Visitor>::Symbol>, <Self::V as Smt2Visitor>::Term)>, ) -> <Self::V as Smt2Visitor>::Term

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>)>, ) -> <Self::V as Smt2Visitor>::Term

fn visit_check_sat(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_check_sat_assuming( &mut self, literals: Vec<(<Self::V as Smt2Visitor>::Symbol, bool)>, ) -> <Self::V as Smt2Visitor>::Command

fn visit_declare_const( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, sort: <Self::V as Smt2Visitor>::Sort, ) -> <Self::V as Smt2Visitor>::Command

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

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>)>, ) -> <Self::V as Smt2Visitor>::Command

fn visit_declare_fun( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, parameters: Vec<<Self::V as Smt2Visitor>::Sort>, sort: <Self::V as Smt2Visitor>::Sort, ) -> <Self::V as Smt2Visitor>::Command

fn visit_declare_sort( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, arity: BigUint, ) -> <Self::V as Smt2Visitor>::Command

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

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

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)>, ) -> <Self::V as Smt2Visitor>::Command

fn visit_define_sort( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, parameters: Vec<<Self::V as Smt2Visitor>::Symbol>, sort: <Self::V as Smt2Visitor>::Sort, ) -> <Self::V as Smt2Visitor>::Command

fn visit_echo(&mut self, message: String) -> <Self::V as Smt2Visitor>::Command

fn visit_exit(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_assertions(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_assignment(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_info( &mut self, flag: <Self::V as Smt2Visitor>::Keyword, ) -> <Self::V as Smt2Visitor>::Command

fn visit_get_model(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_option( &mut self, keyword: <Self::V as Smt2Visitor>::Keyword, ) -> <Self::V as Smt2Visitor>::Command

fn visit_get_proof(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_unsat_assumptions(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_get_value( &mut self, terms: Vec<<Self::V as Smt2Visitor>::Term>, ) -> <Self::V as Smt2Visitor>::Command

fn visit_pop(&mut self, level: BigUint) -> <Self::V as Smt2Visitor>::Command

fn visit_push(&mut self, level: BigUint) -> <Self::V as Smt2Visitor>::Command

fn visit_reset(&mut self) -> <Self::V as Smt2Visitor>::Command

fn visit_reset_assertions(&mut self) -> <Self::V as Smt2Visitor>::Command

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

fn visit_set_logic( &mut self, symbol: <Self::V as Smt2Visitor>::Symbol, ) -> <Self::V as Smt2Visitor>::Command