From 6c4cadd22384985ce8e429e7dafef8ecd4ccf364 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Sep 2017 00:33:56 -0700 Subject: [PATCH] tidy Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 19 ++--- src/sat/sat_lookahead.h | 6 +- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 53 +++----------- src/sat/tactic/atom2bool_var.cpp | 15 ++-- src/sat/tactic/goal2sat.cpp | 100 +++++++++++--------------- 6 files changed, 70 insertions(+), 124 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 74b54e283..f3a0c9d9c 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -463,10 +463,8 @@ namespace sat { } } - static unsigned counter = 0; void lookahead::heule_schur_scores() { - if (counter % 10 != 0) return; - ++counter; + if (m_rating_throttle++ % 10 != 0) return; for (bool_var x : m_freevars) { literal l(x, false); m_rating[l.var()] = heule_schur_score(l) * heule_schur_score(~l); @@ -536,8 +534,7 @@ namespace sat { } void lookahead::heule_unit_scores() { - if (counter % 10 != 0) return; - ++counter; + if (m_rating_throttle++ % 10 != 0) return; for (bool_var x : m_freevars) { literal l(x, false); m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l); @@ -614,7 +611,6 @@ namespace sat { double neg = l_score(~l, h, factor, sqfactor, afactor); hp[l.index()] = pos; hp[(~l).index()] = neg; - // std::cout << "h_scores: " << pos << " " << neg << "\n"; m_rating[l.var()] = pos * neg; } } @@ -930,8 +926,6 @@ namespace sat { return out; } - static unsigned last_prefix_length = 0; - void lookahead::display_search_string() { printf("\r"); uint64 q = m_prefix; @@ -945,10 +939,10 @@ namespace sat { printf(" d: %d", depth); new_prefix_length += 10; } - for (unsigned i = new_prefix_length; i < last_prefix_length; ++i) { + for (unsigned i = new_prefix_length; i < m_last_prefix_length; ++i) { printf(" "); } - last_prefix_length = new_prefix_length; + m_last_prefix_length = new_prefix_length; fflush(stdout); } @@ -2105,7 +2099,6 @@ namespace sat { l = diff1 < diff2 ? lit : ~lit; } } - // if (count > 1) std::cout << count << "\n"; TRACE("sat", tout << "selected: " << l << "\n";); return l; } @@ -2276,8 +2269,8 @@ namespace sat { if (m_search_mode == lookahead_mode::searching) { m_stats.m_propagations++; TRACE("sat", tout << "removing free var v" << l.var() << "\n";); - if (l.var() > m_freevars.max_var()) std::cout << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n"; - if (!m_freevars.contains(l.var())) std::cout << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n"; + if (l.var() > m_freevars.max_var()) IF_VERBOSE(0, verbose_stream() << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n";); + if (!m_freevars.contains(l.var())) IF_VERBOSE(0, verbose_stream() << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n";); if (m_freevars.contains(l.var())) { m_freevars.remove(l.var()); } validate_assign(l); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index c64f265c0..be6070014 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -194,8 +194,10 @@ namespace sat { #endif double m_lookahead_reward; // metric associated with current lookahead1 literal. literal_vector m_wstack; // windofall stack that is populated in lookahead1 mode + unsigned m_last_prefix_length; uint64 m_prefix; // where we are in search tree svector m_vprefix; // var: prefix where variable participates in propagation + unsigned m_rating_throttle; // throttle to recompute rating indexed_uint_set m_freevars; lookahead_mode m_search_mode; // mode of search stats m_stats; @@ -507,7 +509,9 @@ namespace sat { m_drat(s), m_num_tc1(0), m_level(2), - m_prefix(0) { + m_last_prefix_length(0), + m_prefix(0), + m_rating_throttle(0) { m_s.rlimit().push_child(&m_rlimit); init_config(); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index fd8de1ad3..53e8e12dc 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -597,6 +597,7 @@ namespace sat { clause * const * begin_learned() const { return m_learned.begin(); } clause * const * end_learned() const { return m_learned.end(); } clause_vector const& learned() const { return m_learned; } + clause_vector const& clauses() const { return m_clauses; } void collect_bin_clauses(svector & r, bool learned, bool learned_only = false) const; // ----------------------- diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 1fbabcf13..7c3c9643e 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -17,27 +17,6 @@ Notes: --*/ -/* -#include "solver.h" -#include "tactical.h" -#include "sat_solver.h" -#include "ba_solver.h" -#include "tactic2solver.h" -#include "aig_tactic.h" -#include "propagate_values_tactic.h" -#include "max_bv_sharing_tactic.h" -#include "card2bv_tactic.h" -#include "bit_blaster_tactic.h" -#include "simplify_tactic.h" -#include "goal2sat.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" -#include "filter_model_converter.h" -#include "bit_blaster_model_converter.h" -#include "ast_translation.h" -#include "ast_util.h" -#include "propagate_values_tactic.h" -*/ #include "solver/solver.h" #include "tactic/tactical.h" @@ -133,17 +112,6 @@ public: if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr); result->m_internalized = m_internalized; result->m_internalized_converted = m_internalized_converted; -#if 0 - static unsigned file_no = 0; - #pragma omp critical (print_sat) - { - ++file_no; - std::ostringstream ostrm; - ostrm << "s" << file_no << ".txt"; - std::ofstream ous(ostrm.str()); - result->m_solver.display(ous); - } -#endif return result; } @@ -660,9 +628,9 @@ private: } sat::literal_vector value; sat::literal_set premises; - for (unsigned i = 0; i < bvars.size(); ++i) { + for (sat::bool_var bv : bvars) { unsigned index; - if (bool_var2conseq.find(bvars[i], index)) { + if (bool_var2conseq.find(bv, index)) { value.push_back(lconseq[index][0]); for (unsigned j = 1; j < lconseq[index].size(); ++j) { premises.insert(lconseq[index][j]); @@ -754,10 +722,8 @@ private: } void extract_asm2dep(dep2asm_t const& dep2asm, u_map& asm2dep) { - dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); - for (; it != end; ++it) { - expr* e = it->m_key; - asm2dep.insert(it->m_value.index(), e); + for (auto const& kv : dep2asm) { + asm2dep.insert(kv.m_value.index(), kv.m_key); } } @@ -777,9 +743,9 @@ private: ); m_core.reset(); - for (unsigned i = 0; i < core.size(); ++i) { + for (sat::literal c : core) { expr* e = 0; - VERIFY(asm2dep.find(core[i].index(), e)); + VERIFY(asm2dep.find(c.index(), e)); if (asm2fml.contains(e)) { e = asm2fml.find(e); } @@ -789,11 +755,10 @@ private: void check_assumptions(dep2asm_t& dep2asm) { sat::model const & ll_m = m_solver.get_model(); - dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); - for (; it != end; ++it) { - sat::literal lit = it->m_value; + for (auto const& kv : dep2asm) { + sat::literal lit = kv.m_value; if (sat::value_at(lit, ll_m) != l_true) { - IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " does not evaluate to true\n"; + IF_VERBOSE(0, verbose_stream() << mk_pp(kv.m_key, m) << " does not evaluate to true\n"; verbose_stream() << m_asms << "\n"; m_solver.display_assignment(verbose_stream()); m_solver.display(verbose_stream());); diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index 26f3448d3..d8827fe66 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -16,19 +16,18 @@ Author: Notes: --*/ -#include "sat/tactic/atom2bool_var.h" -#include "ast/ast_smt2_pp.h" + #include "util/ref_util.h" +#include "ast/ast_smt2_pp.h" #include "tactic/goal.h" +#include "sat/tactic/atom2bool_var.h" void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const { - obj_map::iterator it = m_mapping.begin(); - obj_map::iterator end = m_mapping.end(); - for (; it != end; ++it) { - sat::literal l(static_cast(it->m_value), false); - lit2expr.set(l.index(), it->m_key); + for (auto const& kv : m_mapping) { + sat::literal l(static_cast(kv.m_value), false); + lit2expr.set(l.index(), kv.m_key); l.neg(); - lit2expr.set(l.index(), m().mk_not(it->m_key)); + lit2expr.set(l.index(), m().mk_not(kv.m_key)); } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index fc061a2e7..75561ed86 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -26,19 +26,19 @@ Author: Notes: --*/ -#include "sat/tactic/goal2sat.h" -#include "ast/ast_smt2_pp.h" #include "util/ref_util.h" #include "util/cooperate.h" -#include "tactic/filter_model_converter.h" -#include "model/model_evaluator.h" -#include "ast/for_each_expr.h" -#include "model/model_v2_pp.h" -#include "tactic/tactic.h" +#include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" -#include "sat/ba_solver.h" #include "ast/pb_decl_plugin.h" #include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "sat/tactic/goal2sat.h" +#include "sat/ba_solver.h" +#include "model/model_evaluator.h" +#include "model/model_v2_pp.h" +#include "tactic/tactic.h" +#include "tactic/filter_model_converter.h" #include struct goal2sat::imp { @@ -412,15 +412,7 @@ struct goal2sat::imp { for (unsigned i = 0; i < num_args; ++i) { sat::literal lit(m_result_stack[sz - num_args + i]); if (!m_solver.is_external(lit.var())) { -#if 1 m_solver.set_external(lit.var()); -#else - sat::bool_var w = m_solver.mk_var(true); - sat::literal lit2(w, false); - mk_clause(lit, ~lit2); - mk_clause(~lit, lit2); - lit = lit2; -#endif } lits.push_back(lit); } @@ -473,9 +465,9 @@ struct goal2sat::imp { k.neg(); svector wlits; convert_pb_args(t, wlits); - for (unsigned i = 0; i < wlits.size(); ++i) { - wlits[i].second.neg(); - k += rational(wlits[i].first); + for (wliteral& wl : wlits) { + wl.second.neg(); + k += rational(wl.first); } check_unsigned(k); unsigned sz = m_result_stack.size(); @@ -502,9 +494,9 @@ struct goal2sat::imp { sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true); m_ext->add_pb_ge(v1, wlits, k.get_unsigned()); k.neg(); - for (unsigned i = 0; i < wlits.size(); ++i) { - wlits[i].second.neg(); - k += rational(wlits[i].first); + for (wliteral& wl : wlits) { + wl.second.neg(); + k += rational(wl.first); } check_unsigned(k); m_ext->add_pb_ge(v2, wlits, k.get_unsigned()); @@ -547,8 +539,8 @@ struct goal2sat::imp { sat::literal_vector lits; unsigned sz = m_result_stack.size(); convert_pb_args(t->get_num_args(), lits); - for (unsigned i = 0; i < lits.size(); ++i) { - lits[i].neg(); + for (sat::literal& l : lits) { + l.neg(); } if (root) { m_result_stack.reset(); @@ -570,8 +562,8 @@ struct goal2sat::imp { sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true); sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true); m_ext->add_at_least(v1, lits, k.get_unsigned()); - for (unsigned i = 0; i < lits.size(); ++i) { - lits[i].neg(); + for (sat::literal& l : lits) { + l.neg(); } m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned()); if (root) { @@ -782,8 +774,7 @@ struct goal2sat::imp { fmls.reset(); m.linearize(g.dep(idx), deps); fmls.push_back(f); - for (unsigned i = 0; i < deps.size(); ++i) { - expr * d = deps[i]; + for (expr * d : deps) { expr * d1 = d; SASSERT(m.is_bool(d)); bool sign = m.is_not(d, d1); @@ -935,10 +926,8 @@ struct sat2goal::imp { // create a SAT model using md sat::model sat_md; - unsigned sz = m_var2expr.size(); expr_ref val(m()); - for (sat::bool_var v = 0; v < sz; v++) { - expr * atom = m_var2expr.get(v); + for (expr * atom : m_var2expr) { ev(atom, val); if (m().is_true(val)) sat_md.push_back(l_true); @@ -952,7 +941,7 @@ struct sat2goal::imp { m_mc(sat_md); // register value of non-auxiliary boolean variables back into md - sz = m_var2expr.size(); + unsigned sz = m_var2expr.size(); for (sat::bool_var v = 0; v < sz; v++) { expr * atom = m_var2expr.get(v); if (is_uninterp_const(atom)) { @@ -973,9 +962,8 @@ struct sat2goal::imp { virtual model_converter * translate(ast_translation & translator) { sat_model_converter * res = alloc(sat_model_converter, translator.to()); res->m_fmc = static_cast(m_fmc->translate(translator)); - unsigned sz = m_var2expr.size(); - for (unsigned i = 0; i < sz; i++) - res->m_var2expr.push_back(translator(m_var2expr.get(i))); + for (expr* e : m_var2expr) + res->m_var2expr.push_back(translator(e)); return res; } @@ -1056,9 +1044,9 @@ struct sat2goal::imp { pb_util pb(m); ptr_buffer lits; vector coeffs; - for (unsigned i = 0; i < p.size(); ++i) { - lits.push_back(lit2expr(p[i].second)); - coeffs.push_back(rational(p[i].first)); + for (auto const& wl : p) { + lits.push_back(lit2expr(wl.second)); + coeffs.push_back(rational(wl.first)); } rational k(p.k()); expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m); @@ -1072,8 +1060,8 @@ struct sat2goal::imp { void assert_card(goal& r, sat::ba_solver::card const& c) { pb_util pb(m); ptr_buffer lits; - for (unsigned i = 0; i < c.size(); ++i) { - lits.push_back(lit2expr(c[i])); + for (sat::literal l : c) { + lits.push_back(lit2expr(l)); } expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m); @@ -1085,8 +1073,8 @@ struct sat2goal::imp { void assert_xor(goal & r, sat::ba_solver::xor const& x) { ptr_buffer lits; - for (unsigned i = 0; i < x.size(); ++i) { - lits.push_back(lit2expr(x[i])); + for (sat::literal l : x) { + lits.push_back(lit2expr(l)); } expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m); @@ -1096,16 +1084,16 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) { + void assert_clauses(sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { ptr_buffer lits; - for (sat::clause * const * it = begin; it != end; it++) { + for (sat::clause* cp : clauses) { checkpoint(); lits.reset(); - sat::clause const & c = *(*it); + sat::clause const & c = *cp; unsigned sz = c.size(); if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) { - for (unsigned i = 0; i < sz; i++) { - lits.push_back(lit2expr(c[i])); + for (sat::literal l : c) { + lits.push_back(lit2expr(l)); } r.assert_expr(m.mk_or(lits.size(), lits.c_ptr())); } @@ -1141,15 +1129,13 @@ struct sat2goal::imp { // collect binary clauses svector bin_clauses; s.collect_bin_clauses(bin_clauses, m_learned); - svector::iterator it = bin_clauses.begin(); - svector::iterator end = bin_clauses.end(); - for (; it != end; ++it) { + for (sat::solver::bin_clause const& bc : bin_clauses) { checkpoint(); - r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second))); + r.assert_expr(m.mk_or(lit2expr(bc.first), lit2expr(bc.second))); } // collect clauses - assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true); - assert_clauses(s, s.begin_learned(), s.end_learned(), r, false); + assert_clauses(s, s.clauses(), r, true); + assert_clauses(s, s.learned(), r, false); sat::ba_solver* ext = get_ba_solver(s); if (ext) { @@ -1220,13 +1206,11 @@ struct sat2goal::imp { // collect learned binary clauses svector bin_clauses; s.collect_bin_clauses(bin_clauses, true, true); - svector::iterator it = bin_clauses.begin(); - svector::iterator end = bin_clauses.end(); - for (; it != end; ++it) { + for (sat::solver::bin_clause const& bc : bin_clauses) { checkpoint(); lits.reset(); - lits.push_back(it->first); - lits.push_back(it->second); + lits.push_back(bc.first); + lits.push_back(bc.second); add_clause(lits, lemmas); } // collect clauses