mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

removing iterators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-20 13:30:31 -07:00
parent 936c22a00b
commit 320105c714
2 changed files with 6 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/mam.cpp
View file

@ -2016,26 +2016,20 @@ namespace smt {
void execute(code_tree * t) {
TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
init(t);
enode_vector::const_iterator it = t->get_candidates().begin();
enode_vector::const_iterator end = t->get_candidates().end();
if (t->filter_candidates()) {
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
if (!app->is_marked() && app->is_cgr()) {
execute_core(t, app);
app->set_mark();
}
}
it = t->get_candidates().begin();
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
if (app->is_marked())
app->unset_mark();
}
}
else {
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (app->is_cgr()) {
TRACE("trigger_bug", tout << "is_cgr\n";);
@ -2821,15 +2815,13 @@ namespace smt {
} // end of execute_core
void display_trees(std::ostream & out, const ptr_vector<code_tree> & trees) {
ptr_vector<code_tree>::const_iterator it = trees.begin();
ptr_vector<code_tree>::const_iterator end = trees.end();
unsigned lbl = 0;
for (; it != end; ++it, ++lbl) {
code_tree * tree = *it;
for (code_tree* tree : trees) {
if (tree) {
out << "tree for f" << lbl << "\n";
out << *tree;
}
++lbl;
}
}

5
src/smt/qi_queue.cpp
View file

@ -148,11 +148,8 @@ namespace smt {
}
void qi_queue::instantiate() {
svector<entry>::iterator it = m_new_entries.begin();
svector<entry>::iterator end = m_new_entries.end();
unsigned since_last_check = 0;
for (; it != end; ++it) {
entry & curr = *it;
for (entry & curr : m_new_entries) {
fingerprint * f = curr.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());