mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#7033

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-03 10:34:16 -08:00
parent 965bee5801
commit a8f3396b24
1 changed files with 14 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/qe/qsat.cpp
View file

@ -85,8 +85,10 @@ namespace qe {
if (m_flevel.find(a->get_decl(), lvl)) { if (m_flevel.find(a->get_decl(), lvl)) {
lvl0.merge(lvl); lvl0.merge(lvl);
} }
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (expr* f : *a) {
app* arg = to_app(a->get_arg(i)); if (!is_app(f))
throw tactic_exception("atom is non-ground");
app* arg = to_app(f);
if (m_elevel.find(arg, lvl)) { if (m_elevel.find(arg, lvl)) {
lvl0.merge(lvl); lvl0.merge(lvl);
} }
@ -265,12 +267,9 @@ namespace qe {
continue; continue;
} }
unsigned sz = a->get_num_args(); for (expr* f : *a) {
for (unsigned i = 0; i < sz; ++i) { if (!mark.is_marked(f))
expr* f = a->get_arg(i); todo.push_back(f);
if (!mark.is_marked(f)) {
todo.push_back(f);
}
} }
bool is_boolop = bool is_boolop =
@ -324,8 +323,8 @@ namespace qe {
unsigned sz = a->get_num_args(); unsigned sz = a->get_num_args();
bool diff = false; bool diff = false;
args.reset(); args.reset();
for (unsigned i = 0; i < sz; ++i) { for (expr* f : *a) {
expr* f = a->get_arg(i), *f1; expr *f1;
if (cache.find(f, f1)) { if (cache.find(f, f1)) {
args.push_back(f1); args.push_back(f1);
diff |= f != f1; diff |= f != f1;
@ -413,8 +412,8 @@ namespace qe {
unsigned sz = a->get_num_args(); unsigned sz = a->get_num_args();
args.reset(); args.reset();
bool diff = false; bool diff = false;
for (unsigned i = 0; i < sz; ++i) { for (expr* f : *a) {
expr* f = a->get_arg(i), *f1; expr *f1;
if (cache.find(f, f1)) { if (cache.find(f, f1)) {
args.push_back(f1); args.push_back(f1);
diff |= f != f1; diff |= f != f1;
@ -1018,12 +1017,12 @@ namespace qe {
expr_ref_vector args(m); expr_ref_vector args(m);
unsigned num_args = a->get_num_args(); unsigned num_args = a->get_num_args();
bool all_visited = true; bool all_visited = true;
for (unsigned i = 0; i < num_args; ++i) { for (expr* arg : *a) {
if (visited.find(a->get_arg(i), r)) { if (visited.find(arg, r)) {
args.push_back(r); args.push_back(r);
} }
else { else {
todo.push_back(a->get_arg(i)); todo.push_back(arg);
all_visited = false; all_visited = false;
} }
} }