Struct Term 

pub struct Term {
    pub tree_depth: usize,
    pub tree_size: usize,
}

Statistics about a term.

Fields

tree_depth: usize

tree_size: usize

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate 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 Debug for Term

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

Formats the value using the given formatter.

impl Default for Term

fn default() -> Term

Returns the “default value” for a type.

impl PartialEq for Term

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Term

impl StructuralPartialEq for Term