Struct smt2parser::stats::Smt2Counters

pub struct Smt2Counters {

    pub numeral_constant_count: usize,
    pub decimal_constant_count: usize,
    pub hexadecimal_constant_count: usize,
    pub binary_constant_count: usize,
    pub string_constant_count: usize,
    pub fresh_symbol_count: usize,
    pub bound_symbol_count: usize,
    pub any_symbol_count: usize,
    pub keyword_count: usize,
    pub constant_s_expr_count: usize,
    pub symbol_s_expr_count: usize,
    pub keyword_s_expr_count: usize,
    pub application_s_expr_count: usize,
    pub simple_sort_count: usize,
    pub parameterized_sort_count: usize,
    pub simple_identifier_count: usize,
    pub sorted_identifier_count: usize,
    pub constant_count: usize,
    pub qual_identifier_count: usize,
    pub application_count: usize,
    pub let_count: usize,
    pub forall_count: usize,
    pub exists_count: usize,
    pub match_count: usize,
    pub attributes_count: usize,
    pub assert_count: usize,
    pub check_sat_count: usize,
    pub check_sat_assuming_count: usize,
    pub declare_const_count: usize,
    pub declare_datatype_count: usize,
    pub declare_datatypes_count: usize,
    pub declare_fun_count: usize,
    pub declare_sort_count: usize,
    pub define_fun_count: usize,
    pub define_fun_rec_count: usize,
    pub define_funs_rec_count: usize,
    pub define_sort_count: usize,
    pub echo_count: usize,
    pub exit_count: usize,
    pub get_assertions_count: usize,
    pub get_assignment_count: usize,
    pub get_info_count: usize,
    pub get_model_count: usize,
    pub get_option_count: usize,
    pub get_proof_count: usize,
    pub get_unsat_assumptions_count: usize,
    pub get_unsat_core_count: usize,
    pub get_value_count: usize,
    pub pop_count: usize,
    pub push_count: usize,
    pub reset_count: usize,
    pub reset_assertions_count: usize,
    pub set_info_count: usize,
    pub set_logic_count: usize,
    pub set_option_count: usize,
    pub term_count: usize,
    pub term_max_depth: usize,
    pub term_max_size: usize,
    pub term_sum_depth: usize,
    pub term_sum_size: usize,
    pub keyword_counts: BTreeMap<String, usize>,
    pub symbol_counts: BTreeMap<String, usize>,
}

An implementation of Smt2Visitor that returns simple statistics on the SMT2 inputs.

Fields

numeral_constant_count: usize

decimal_constant_count: usize

hexadecimal_constant_count: usize

binary_constant_count: usize

string_constant_count: usize

fresh_symbol_count: usize

bound_symbol_count: usize

any_symbol_count: usize

keyword_count: usize

constant_s_expr_count: usize

symbol_s_expr_count: usize

keyword_s_expr_count: usize

application_s_expr_count: usize

simple_sort_count: usize

parameterized_sort_count: usize

simple_identifier_count: usize

sorted_identifier_count: usize

constant_count: usize

qual_identifier_count: usize

application_count: usize

let_count: usize

forall_count: usize

exists_count: usize

match_count: usize

attributes_count: usize

assert_count: usize

check_sat_count: usize

check_sat_assuming_count: usize

declare_const_count: usize

declare_datatype_count: usize

declare_datatypes_count: usize

declare_fun_count: usize

declare_sort_count: usize

define_fun_count: usize

define_fun_rec_count: usize

define_funs_rec_count: usize

define_sort_count: usize

echo_count: usize

exit_count: usize

get_assertions_count: usize

get_assignment_count: usize

get_info_count: usize

get_model_count: usize

get_option_count: usize

get_proof_count: usize

get_unsat_assumptions_count: usize

get_unsat_core_count: usize

get_value_count: usize

pop_count: usize

push_count: usize

reset_count: usize

reset_assertions_count: usize

set_info_count: usize

set_logic_count: usize

set_option_count: usize

term_count: usize

term_max_depth: usize

term_max_size: usize

term_sum_depth: usize

term_sum_size: usize

keyword_counts: BTreeMap<String, usize>

symbol_counts: BTreeMap<String, usize>

Implementations

impl Smt2Counters

pub fn new(keywords: Vec<String>, symbols: Vec<String>) -> Self

Build a Smt2Visitor that holds statistics, including some interesting keywords and symbols.

Trait Implementations

impl Clone for Smt2Counters

fn clone(&self) -> Smt2Counters

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl CommandVisitor<Term, (), (), (), (), ()> for Smt2Counters

type T = ()

type E = Error

fn visit_assert(&mut self, term: Term) -> Result<Self::T, Self::E>

fn visit_check_sat(&mut self) -> Result<Self::T, Self::E>

fn visit_check_sat_assuming(
    &mut self,
    _literals: Vec<((), bool)>
) -> Result<Self::T, Self::E>

fn visit_declare_const(
    &mut self,
    _symbol: (),
    _sort: ()
) -> Result<Self::T, Self::E>

fn visit_declare_datatype(
    &mut self,
    _symbol: (),
    _datatype: DatatypeDec<(), ()>
) -> Result<Self::T, Self::E>

fn visit_declare_datatypes(
    &mut self,
    _datatypes: Vec<((), Numeral, DatatypeDec<(), ()>)>
) -> Result<Self::T, Self::E>

fn visit_declare_fun(
    &mut self,
    _symbol: (),
    _parameters: Vec<()>,
    _sort: ()
) -> Result<Self::T, Self::E>

fn visit_declare_sort(
    &mut self,
    _symbol: (),
    _arity: Numeral
) -> Result<Self::T, Self::E>

fn visit_define_fun(
    &mut self,
    _sig: FunctionDec<(), ()>,
    term: Term
) -> Result<Self::T, Self::E>

fn visit_define_fun_rec(
    &mut self,
    _sig: FunctionDec<(), ()>,
    term: Term
) -> Result<Self::T, Self::E>

fn visit_define_funs_rec(
    &mut self,
    funs: Vec<(FunctionDec<(), ()>, Term)>
) -> Result<Self::T, Self::E>

fn visit_define_sort(
    &mut self,
    _symbol: (),
    _parameters: Vec<()>,
    _sort: ()
) -> Result<Self::T, Self::E>

fn visit_echo(&mut self, _message: String) -> Result<Self::T, Self::E>

fn visit_exit(&mut self) -> Result<Self::T, Self::E>

fn visit_get_assertions(&mut self) -> Result<Self::T, Self::E>

fn visit_get_assignment(&mut self) -> Result<Self::T, Self::E>

fn visit_get_info(&mut self, _flag: ()) -> Result<Self::T, Self::E>

fn visit_get_model(&mut self) -> Result<Self::T, Self::E>

fn visit_get_option(&mut self, _keyword: ()) -> Result<Self::T, Self::E>

fn visit_get_proof(&mut self) -> Result<Self::T, Self::E>

fn visit_get_unsat_assumptions(&mut self) -> Result<Self::T, Self::E>

fn visit_get_unsat_core(&mut self) -> Result<Self::T, Self::E>

fn visit_get_value(&mut self, terms: Vec<Term>) -> Result<Self::T, Self::E>

fn visit_pop(&mut self, _level: Numeral) -> Result<Self::T, Self::E>

fn visit_push(&mut self, _level: Numeral) -> Result<Self::T, Self::E>

fn visit_reset(&mut self) -> Result<Self::T, Self::E>

fn visit_reset_assertions(&mut self) -> Result<Self::T, Self::E>

fn visit_set_info(
    &mut self,
    _keyword: (),
    _value: AttributeValue<(), (), ()>
) -> Result<Self::T, Self::E>

fn visit_set_logic(&mut self, _symbol: ()) -> Result<Self::T, Self::E>

fn visit_set_option(
    &mut self,
    _keyword: (),
    _value: AttributeValue<(), (), ()>
) -> Result<Self::T, Self::E>

impl ConstantVisitor for Smt2Counters

type T = ()

type E = Error

fn visit_numeral_constant(
    &mut self,
    _value: Numeral
) -> Result<Self::T, Self::E>

fn visit_decimal_constant(
    &mut self,
    _value: Decimal
) -> Result<Self::T, Self::E>

fn visit_hexadecimal_constant(
    &mut self,
    _value: Hexadecimal
) -> Result<Self::T, Self::E>

fn visit_binary_constant(&mut self, _value: Binary) -> Result<Self::T, Self::E>

fn visit_string_constant(&mut self, _value: String) -> Result<Self::T, Self::E>

impl Debug for Smt2Counters

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

Formats the value using the given formatter.

impl Default for Smt2Counters

fn default() -> Smt2Counters

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Smt2Counters

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
    __D: Deserializer<'de>, 

Deserialize this value from the given Serde deserializer.

impl KeywordVisitor for Smt2Counters

type T = ()

type E = Error

fn visit_keyword(&mut self, value: String) -> Result<Self::T, Self::E>

impl PartialEq<Smt2Counters> for Smt2Counters

fn eq(&self, other: &Smt2Counters) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Smt2Counters) -> bool

This method tests for !=.

impl QualIdentifierVisitor<Identifier<()>, ()> for Smt2Counters

type T = ()

type E = Error

fn visit_simple_identifier(
    &mut self,
    _identifier: Identifier<()>
) -> Result<Self::T, Self::E>

fn visit_sorted_identifier(
    &mut self,
    _identifier: Identifier<()>,
    _sort: ()
) -> Result<Self::T, Self::E>

impl SExprVisitor<(), (), ()> for Smt2Counters

type T = ()

type E = Error

fn visit_constant_s_expr(&mut self, _value: ()) -> Result<Self::T, Self::E>

fn visit_symbol_s_expr(&mut self, _value: ()) -> Result<Self::T, Self::E>

fn visit_keyword_s_expr(&mut self, _value: ()) -> Result<Self::T, Self::E>

fn visit_application_s_expr(
    &mut self,
    _values: Vec<Self::T>
) -> Result<Self::T, Self::E>

impl Serialize for Smt2Counters

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error> where
    __S: Serializer, 

Serialize this value into the given Serde serializer.

impl Smt2Visitor for Smt2Counters

type Error = Error

type Constant = ()

type QualIdentifier = ()

type Keyword = ()

type Sort = ()

type SExpr = ()

type Symbol = ()

type Term = Term

type Command = ()

fn syntax_error(&mut self, position: Position, s: String) -> Self::Error

fn parsing_error(&mut self, position: Position, s: String) -> Self::Error

impl SortVisitor<()> for Smt2Counters

type T = ()

type E = Error

fn visit_simple_sort(
    &mut self,
    _identifier: Identifier<()>
) -> Result<Self::T, Self::E>

fn visit_parameterized_sort(
    &mut self,
    _identifier: Identifier<()>,
    _parameters: Vec<Self::T>
) -> Result<Self::T, Self::E>

impl SymbolVisitor for Smt2Counters

type T = ()

type E = Error

fn visit_fresh_symbol(
    &mut self,
    _value: String,
    _kind: SymbolKind
) -> Result<Self::T, Self::E>

fn visit_bound_symbol(&mut self, value: String) -> Result<Self::T, Self::E>

fn visit_any_symbol(&mut self, _value: String) -> Result<Self::T, Self::E>

fn bind_symbol(&mut self, _symbol: &Self::T)

fn unbind_symbol(&mut self, _symbol: &Self::T)

impl TermVisitor<(), (), (), (), (), ()> for Smt2Counters

type T = Term

type E = Error

fn visit_constant(&mut self, _constant: ()) -> Result<Self::T, Self::E>

fn visit_qual_identifier(
    &mut self,
    _qual_identifier: ()
) -> Result<Self::T, Self::E>

fn visit_application(
    &mut self,
    _qual_identifier: (),
    arguments: Vec<Self::T>
) -> Result<Self::T, Self::E>

fn visit_let(
    &mut self,
    var_bindings: Vec<((), Self::T)>,
    term: Self::T
) -> Result<Self::T, Self::E>

fn visit_forall(
    &mut self,
    _vars: Vec<((), ())>,
    term: Self::T
) -> Result<Self::T, Self::E>

fn visit_exists(
    &mut self,
    _vars: Vec<((), ())>,
    term: Self::T
) -> Result<Self::T, Self::E>

fn visit_match(
    &mut self,
    term: Self::T,
    cases: Vec<(Vec<()>, Self::T)>
) -> Result<Self::T, Self::E>

fn visit_attributes(
    &mut self,
    term: Self::T,
    _attributes: Vec<((), AttributeValue<(), (), ()>)>
) -> Result<Self::T, Self::E>

impl Eq for Smt2Counters

impl StructuralEq for Smt2Counters

impl StructuralPartialEq for Smt2Counters