Struct smt2patch::Rewriter

pub struct Rewriter { /* fields omitted */ }

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

pub fn process_constant(
    &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

pub fn process_s_expr(
    &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

pub fn process_qual_identifier(
    &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

pub fn process_command(
    &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

pub fn visit_decimal_constant(
    &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

pub fn visit_binary_constant(
    &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

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

pub fn visit_keyword(
    &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

pub fn visit_symbol_s_expr(
    &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

pub fn visit_application_s_expr(
    &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

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

pub fn visit_simple_identifier(
    &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

pub fn visit_constant(
    &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

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

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

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

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

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

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

pub fn visit_check_sat_assuming(
    &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

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

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

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

pub fn visit_declare_sort(
    &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

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

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

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

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

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

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

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

pub fn visit_get_info(
    &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

pub fn visit_get_option(
    &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

pub fn visit_get_unsat_assumptions(
    &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

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

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

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

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

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

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