diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index cac12413e..232e7b6d0 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2254,9 +2254,10 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const } else { string_buffer<64> buffer; - buffer << prefix; if (prefix == symbol::null) buffer << "sk"; + else + buffer << prefix; buffer << "!"; if (suffix != symbol::null) buffer << suffix << "!"; diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index fcf9a9f8f..fd176c1e0 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -717,7 +717,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT)); op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT)); - if (logic == symbol::null) { + if (logic == symbol::null || logic == "QF_FD") { op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL)); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 59210a266..5dd3ed1f7 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -302,17 +302,16 @@ namespace sat{ } bdd elim_vars::make_clauses(clause_use_list & occs) { - bdd result = m.mk_true(); - clause_use_list::iterator it = occs.mk_iterator(); - while (!it.at_end()) { + bdd result = m.mk_true(); + for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) { clause const& c = it.curr(); - if (c.is_blocked()) continue; - bdd cl = m.mk_false(); - for (literal l : c) { - cl |= mk_literal(l); + if (!c.is_blocked()) { + bdd cl = m.mk_false(); + for (literal l : c) { + cl |= mk_literal(l); + } + result &= cl; } - it.next(); - result &= cl; } return result; } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 347800d19..2cc1a7f09 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -418,8 +418,7 @@ namespace sat { literal target) { if (c1.is_blocked()) return; clause_use_list const & cs = m_use_list.get(target); - clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { + for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { clause & c2 = it.curr(); CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";); SASSERT(!c2.was_removed()); @@ -433,7 +432,6 @@ namespace sat { out_lits.push_back(l); } } - it.next(); } } @@ -532,7 +530,7 @@ namespace sat { if (c1.is_blocked()) return; clause_use_list const & cs = m_use_list.get(target); clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { + for (; !it.at_end(); it.next()) { clause & c2 = it.curr(); SASSERT(!c2.was_removed()); if (&c2 != &c1 && @@ -543,7 +541,6 @@ namespace sat { out.push_back(&c2); } } - it.next(); } } @@ -652,29 +649,16 @@ namespace sat { unsigned new_trail_sz = s.m_trail.size(); for (unsigned i = old_trail_sz; i < new_trail_sz; i++) { literal l = s.m_trail[i]; - { - // put clauses with literals assigned to false back into todo-list - clause_use_list & cs = m_use_list.get(~l); - clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { - clause & c = it.curr(); - it.next(); - m_sub_todo.insert(c); - } + // put clauses with literals assigned to false back into todo-list + for (auto it = m_use_list.get(~l).mk_iterator(); !it.at_end(); it.next()) { + m_sub_todo.insert(it.curr()); } - { - // erase satisfied clauses - clause_use_list & cs = m_use_list.get(l); - { - clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { - clause & c = it.curr(); - it.next(); - remove_clause(c, l); - } - } - cs.reset(); + clause_use_list& cs = m_use_list.get(l); + for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { + clause & c = it.curr(); + remove_clause(c, l); } + cs.reset(); } } @@ -1338,12 +1322,8 @@ namespace sat { } if (!found) { IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";); - watched w(l2, false); - w.set_blocked(); - s.get_wlist(~l).push_back(w); - w = watched(l, false); - w.set_blocked(); - s.get_wlist(~l2).push_back(w); + s.get_wlist(~l).push_back(watched(l2, true)); + s.get_wlist(~l2).push_back(watched(l, true)); ++s.m_num_bca; } } @@ -1473,29 +1453,18 @@ namespace sat { void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) { clause_use_list const & cs = m_use_list.get(l); clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { + for (; !it.at_end(); it.next()) { if (!it.curr().is_blocked() || include_blocked) { r.push_back(clause_wrapper(it.curr())); SASSERT(r.back().size() == it.curr().size()); } - it.next(); } watch_list & wlist = get_wlist(~l); - if (include_blocked) { - for (auto & w : wlist) { - if (w.is_binary_non_learned_clause2()) { - r.push_back(clause_wrapper(l, w.get_literal())); - SASSERT(r.back().size() == 2); - } - } - } - else { - for (auto & w : wlist) { - if (w.is_binary_unblocked_clause()) { - r.push_back(clause_wrapper(l, w.get_literal())); - SASSERT(r.back().size() == 2); - } + for (auto & w : wlist) { + if (include_blocked ? w.is_binary_non_learned_clause() : w.is_binary_unblocked_clause()) { + r.push_back(clause_wrapper(l, w.get_literal())); + SASSERT(r.back().size() == 2); } } } @@ -1607,8 +1576,7 @@ namespace sat { \brief Eliminate the clauses where the variable being eliminated occur. */ void simplifier::remove_clauses(clause_use_list const & cs, literal l) { - clause_use_list::iterator it = cs.mk_iterator(); - while (!it.at_end()) { + for (auto it = cs.mk_iterator(); !it.at_end(); ) { clause & c = it.curr(); it.next(); SASSERT(c.contains(l)); @@ -1641,22 +1609,14 @@ namespace sat { unsigned before_lits = num_bin_pos*2 + num_bin_neg*2; - { - clause_use_list::iterator it = pos_occs.mk_iterator(); - while (!it.at_end()) { - if (!it.curr().is_blocked()) - before_lits += it.curr().size(); - it.next(); - } + for (auto it = pos_occs.mk_iterator(); !it.at_end(); it.next()) { + if (!it.curr().is_blocked()) + before_lits += it.curr().size(); } - { - clause_use_list::iterator it2 = neg_occs.mk_iterator(); - while (!it2.at_end()) { - if (!it2.curr().is_blocked()) - before_lits += it2.curr().size(); - it2.next(); - } + for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { + if (!it.curr().is_blocked()) + before_lits += it.curr().size(); } TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";); diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index f18e08999..8d7924c6f 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -88,7 +88,7 @@ namespace sat { bool is_binary_unblocked_clause() const { return m_val2 == 0; } bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); } - bool is_binary_non_learned_clause2() const { return is_binary_clause() && !is_learned(); } + bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); } void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast(BINARY); SASSERT(!is_learned()); } void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index fe8135368..208d60386 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1110,7 +1110,6 @@ struct sat2goal::imp { r.assert_expr(m.mk_false()); return; } - IF_VERBOSE(1, verbose_stream() << "solver2goal " << s.num_vars() << " " << s.clauses().size() << "\n";); init_lit2expr(s, map, mc, r.models_enabled()); // collect units unsigned num_vars = s.num_vars();