RetroSearch Browse

Showing content from https://z3prover.github.io/api/html/classz3_1_1stats.html below:

Definition at line 2686 of file z3++.h.

◆ stats() [1/3] ◆ stats() [2/3] ◆ stats() [3/3] ◆ ~stats()

Definition at line 2696 of file z3++.h.

void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)

Decrement the reference counter of the given statistics object.

◆ double_value() double double_value ( unsigned i ) const inline

Definition at line 2710 of file z3++.h.

Z3_error_code check_error() const

double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)

Return the double value of the given statistical data.

◆ is_double() bool is_double ( unsigned i ) const inline

Definition at line 2708 of file z3++.h.

bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)

Return true if the given statistical data is a double.

◆ is_uint() bool is_uint ( unsigned i ) const inline

Definition at line 2707 of file z3++.h.

bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)

Return true if the given statistical data is a unsigned integer.

◆ key() std::string key ( unsigned i ) const inline

Definition at line 2706 of file z3++.h.

const char * Z3_string

Z3 string type. It is just an alias for const char *.

Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)

Return the key (a string) for a particular statistical data.

◆ operator Z3_stats() operator Z3_stats ( ) const inline ◆ operator=()

Definition at line 2698 of file z3++.h.

2701

object::operator=(s);

2702

m_stats = s.m_stats;

void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)

Increment the reference counter of the given statistics object.

◆ size() ◆ uint_value() unsigned uint_value ( unsigned i ) const inline

Definition at line 2709 of file z3++.h.

unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)

Return the unsigned value of the given statistical data.

◆ operator<< std::ostream& operator<< ( std::ostream & out, stats const & s ) friend

Definition at line 2713 of file z3++.h.

Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)

Convert a statistics into a string.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4