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