1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     smt_quantifier_stat.cpp
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-02-20.
15 
16 Revision History:
17 
18 --*/
19 #include "ast/quantifier_stat.h"
20 
21 namespace q {
22 
quantifier_stat(unsigned generation)23     quantifier_stat::quantifier_stat(unsigned generation):
24         m_size(0),
25         m_depth(0),
26         m_generation(generation),
27         m_case_split_factor(1),
28         m_num_nested_quantifiers(0),
29         m_num_instances(0),
30         m_num_instances_checker_sat(0),
31         m_num_instances_simplify_true(0),
32         m_num_instances_curr_search(0),
33         m_num_instances_curr_branch(0),
34         m_max_generation(0),
35         m_max_cost(0.0f) {
36     }
37 
quantifier_stat_gen(ast_manager & m,region & r)38     quantifier_stat_gen::quantifier_stat_gen(ast_manager & m, region & r):
39         m_manager(m),
40         m_region(r) {
41     }
42 
reset()43     void quantifier_stat_gen::reset() {
44         m_already_found.reset();
45         m_todo.reset();
46         m_case_split_factor = 1;
47     }
48 
operator ()(quantifier * q,unsigned generation)49     quantifier_stat * quantifier_stat_gen::operator()(quantifier * q, unsigned generation) {
50         reset();
51         quantifier_stat * r = new (m_region) quantifier_stat(generation);
52         m_todo.push_back(entry(q->get_expr()));
53         while (!m_todo.empty()) {
54             entry & e       = m_todo.back();
55             expr * n        = e.m_expr;
56             unsigned depth  = e.m_depth;
57             bool depth_only = e.m_depth_only;
58             m_todo.pop_back();
59             unsigned old_depth;
60             if (m_already_found.find(n, old_depth)) {
61                 if (old_depth >= depth)
62                     continue;
63                 depth_only  = true;
64             }
65             m_already_found.insert(n, depth);
66             if (depth >= r->m_depth)
67                 r->m_depth = depth;
68             if (!depth_only) {
69                 r->m_size++;
70                 if (is_quantifier(n))
71                     r->m_num_nested_quantifiers ++;
72                 if (is_app(n) && to_app(n)->get_family_id() == m_manager.get_basic_family_id()) {
73                     unsigned num_args = to_app(n)->get_num_args();
74                     // Remark: I'm approximating the case_split factor.
75                     // I'm also ignoring the case split factor due to theories.
76                     switch (to_app(n)->get_decl_kind()) {
77                     case OP_OR:
78                         if (depth == 0)
79                             m_case_split_factor *= num_args;
80                         else
81                             m_case_split_factor *= (num_args + 1);
82                         break;
83                     case OP_AND:
84                         if (depth > 0)
85                             m_case_split_factor *= (num_args + 1);
86                         break;
87                     case OP_EQ:
88                         if (m_manager.is_iff(n)) {
89                             if (depth == 0)
90                                 m_case_split_factor *= 4;
91                             else
92                                 m_case_split_factor *= 9;
93                         }
94                         break;
95                     case OP_ITE:
96                         if (depth == 0)
97                             m_case_split_factor *= 4;
98                         else
99                             m_case_split_factor *= 9;
100                         break;
101                     default:
102                         break;
103                     }
104                 }
105             }
106             if (is_app(n)) {
107                 unsigned j = to_app(n)->get_num_args();
108                 while (j > 0) {
109                     --j;
110                     m_todo.push_back(entry(to_app(n)->get_arg(j), depth + 1, depth_only));
111                 }
112             }
113         }
114         r->m_case_split_factor = m_case_split_factor.get_value();
115         return r;
116     }
117 
118 };
119 
120