Struct smt2parser::stats::Smt2Counters [−][src]
pub struct Smt2Counters {Show 62 fields
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>,
}
Expand description
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
Trait Implementations
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_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_set_info(
&mut self,
_keyword: (),
_value: AttributeValue<(), (), ()>
) -> Result<Self::T, Self::E>
fn visit_set_option(
&mut self,
_keyword: (),
_value: AttributeValue<(), (), ()>
) -> Result<Self::T, Self::E>
Returns the “default value” for a type. Read more
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
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>
type QualIdentifier = ()
fn visit_parameterized_sort(
&mut self,
_identifier: Identifier<()>,
_parameters: Vec<Self::T>
) -> Result<Self::T, Self::E>
fn visit_fresh_symbol(
&mut self,
_value: String,
_kind: SymbolKind
) -> 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>
Auto Trait Implementations
impl RefUnwindSafe for Smt2Counters
impl Send for Smt2Counters
impl Sync for Smt2Counters
impl Unpin for Smt2Counters
impl UnwindSafe for Smt2Counters
Blanket Implementations
Mutably borrows from an owned value. Read more