1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
expr_stat.h
Abstract:
Expression statistics (symbol count, var count, depth, ...)
All functions in these module assume expressions do not contain
nested quantifiers.
Author:
Leonardo de Moura (leonardo) 2008-02-05.
Revision History:
--*/
#pragma once
class expr;
struct expr_stat {
unsigned m_sym_count = 0; // symbol count
unsigned m_depth = 0; // depth
unsigned m_const_count = 0; // constant count
unsigned m_max_var_idx = 0;
bool m_ground = true;
};
/**
\brief Collect statistics regarding the given expression.
\warning This function traverses the dag as a tree.
*/
void get_expr_stat(expr * n, expr_stat & r);
/**
\brief Return the number of symbols in \c n.
\warning This function traverses the dag as a tree.
*/
unsigned get_symbol_count(expr * n);