mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-27 14:37:55 +00:00
Code Activity

shortcircuit stats functions on ground terms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-28 21:48:49 -07:00
parent b303fd59c0
commit 8aee7129f6
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/mam.cpp
View file

@ -879,6 +879,9 @@ namespace smt {
*/ */
void get_stats_core(app * n, unsigned & sz, unsigned & num_unbound_vars) { void get_stats_core(app * n, unsigned & sz, unsigned & num_unbound_vars) {
sz++; sz++;
if (n->is_ground()) {
return;
}
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i); expr * arg = n->get_arg(i);
@ -901,7 +904,7 @@ namespace smt {
void get_stats(app * n, unsigned & sz, unsigned & num_unbound_vars) { void get_stats(app * n, unsigned & sz, unsigned & num_unbound_vars) {
sz = 0; sz = 0;
num_unbound_vars = 0; num_unbound_vars = 0;
return get_stats_core(n, sz, num_unbound_vars); get_stats_core(n, sz, num_unbound_vars);
} }
/** /**
@ -1032,6 +1035,9 @@ namespace smt {
*/ */
unsigned get_num_bound_vars_core(app * n, bool & has_unbound_vars) { unsigned get_num_bound_vars_core(app * n, bool & has_unbound_vars) {
unsigned r = 0; unsigned r = 0;
if (n->is_ground()) {
return 0;
}
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i); expr * arg = n->get_arg(i);