CBMC
|
Stats about sharing between several sharing map instances. More...
#include <sharing_map.h>
Public Attributes | |
std::size_t | num_nodes = 0 |
std::size_t | num_unique_nodes = 0 |
std::size_t | num_leafs = 0 |
std::size_t | num_unique_leafs = 0 |
Stats about sharing between several sharing map instances.
An instance of this class is returned by the get_sharing_map_stats_* functions.
The num_nodes field gives the total number of nodes in the given maps. Nodes that are part of n of the maps are counted n times.
The num_unique_nodes field gives the number of unique nodes in the given maps. A node that is part of several of the maps is only counted once.
The num_leafs and num_unique_leafs fields are similar to the above but only leafs are counted.
Definition at line 535 of file sharing_map.h.
std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statst::num_leafs = 0 |
Definition at line 539 of file sharing_map.h.
std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statst::num_nodes = 0 |
Definition at line 537 of file sharing_map.h.
std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statst::num_unique_leafs = 0 |
Definition at line 540 of file sharing_map.h.
std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statst::num_unique_nodes = 0 |
Definition at line 538 of file sharing_map.h.