From d052155f6eb817fbd1e915da001653bcf230b946 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Apr 2017 14:46:46 -0700 Subject: [PATCH] parallelizing ccc Signed-off-by: Nikolaj Bjorner --- src/sat/sat_ccc.cpp | 397 ++++++++++++++++------------------ src/sat/sat_ccc.h | 74 ++++--- src/sat/sat_lookahead.h | 6 +- src/sat/sat_solver.cpp | 11 +- src/sat/sat_solver.h | 2 +- src/smt/asserted_formulas.cpp | 32 +-- src/util/util.cpp | 16 ++ src/util/util.h | 27 ++- 8 files changed, 284 insertions(+), 281 deletions(-) diff --git a/src/sat/sat_ccc.cpp b/src/sat/sat_ccc.cpp index 141869f11..a282397be 100644 --- a/src/sat/sat_ccc.cpp +++ b/src/sat/sat_ccc.cpp @@ -15,6 +15,16 @@ Author: Notes: + The cube process spawns conquer threads to search parts of the + state space. + The conquer threads have two modes: + - emulation mode - where they try to outpace the cuber on the same search tree + - complement mode - where they solve a sub-branch not yet explored by the cuber. + When the conquer thread returns a solved cube it is processed in the following ways: + - ignore if solved_id \not\in decisions + - mark d as closed if d \in decisions, such that d is marked by solved id + - backjump otherwise, conquer thread has solved a branch attempted by the cuber + --*/ #include "sat_solver.h" @@ -23,9 +33,16 @@ Notes: using namespace sat; - std::ostream& ccc::decision::pp(std::ostream& out) const { - return out << "(" << m_id << " " << m_last << " d:" << m_depth << ") "; + out << "(" + << " id:" << m_id + << " l:" << m_literal + << " d:" << m_depth; + if (m_spawn_id != 0) { + out << " s:" << m_spawn_id; + } + out << ") "; + return out; } std::ostream& ccc::pp(std::ostream& out, svector const& v) { @@ -35,9 +52,9 @@ std::ostream& ccc::pp(std::ostream& out, svector const& v) { return out; } -lbool ccc::cube2() { - unsigned branch_id = 0; - unsigned_vector id_trail; +lbool ccc::cube() { + m_branch_id = 0; + m_last_closure_level = UINT_MAX; lookahead lh(m_s); lh.init_search(); @@ -47,41 +64,26 @@ lbool ccc::cube2() { literal_vector trail; svector decisions; lh.m_search_mode = lookahead_mode::searching; - lh.m_blocked_literal = null_literal; - lbool r = cube2(branch_id, decisions, lh); + lbool r = cube(decisions, lh); if (r == l_true) { m_model = lh.get_model(); } + lh.collect_statistics(m_stats); return r; } -lbool ccc::cube2(unsigned& branch_id, svector& decisions, lookahead& lh) { +lbool ccc::cube(svector& decisions, lookahead& lh) { m_s.checkpoint(); if (lh.inconsistent()) { return l_false; } - lh.inc_istamp(); - - // check if CDCL solver got ahead. - bool repeat = false; - #pragma omp critical (ccc_solved) - { - while (!m_solved.empty()) { - unsigned solved_id = m_solved.top(); - if (contains_branch(decisions, solved_id)) { - IF_VERBOSE(1, verbose_stream() << "conquer " << decisions.size() << "\n";); - repeat = true; - break; - } - else { - m_solved.pop(); - } - } + if (get_solved(decisions)) { + return l_false; } - if (repeat) return l_false; - + + lh.inc_istamp(); literal l = lh.choose(); if (lh.inconsistent()) { return l_false; @@ -92,34 +94,38 @@ lbool ccc::cube2(unsigned& branch_id, svector& decisions, lookahead& l } if (!decisions.empty()) { - #pragma omp critical (ccc_decisions) - { - m_decisions.push(decisions.back()); - } + put_decision(decisions.back()); } - // update trail and set of ids + // update trail and decisions - ++branch_id; ++lh.m_stats.m_decisions; unsigned parent_id = decisions.empty() ? 0 : decisions.back().m_id; - decision d(branch_id, decisions.size() + 1, l, null_literal, parent_id); + unsigned spawn_id = spawn_conquer(decisions); + unsigned branch_id = ++m_branch_id; + decision d(branch_id, decisions.size() + 1, l, parent_id, spawn_id); decisions.push_back(d); - #pragma omp critical (ccc_log) - { - IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";); - IF_VERBOSE(2, pp(verbose_stream(), decisions) << "\n"; ); - } - TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); + IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";); + IF_VERBOSE(2, pp(verbose_stream(), decisions) << "\n"; ); + + TRACE("sat", tout << "choose: " << l << "\n";); lh.push(l, lh.c_fixed_truth); - lbool r = cube2(branch_id, decisions, lh); + lbool r = cube(decisions, lh); if (r == l_false) { lh.pop(); - lh.flip_prefix(); - lh.push(~l, lh.c_fixed_truth); - decisions.back().m_last = ~l; - r = cube2(branch_id, decisions, lh); + if (decisions.back().is_closed()) { + // branch was solved by a spawned conquer process + IF_VERBOSE(1, verbose_stream() << "closed " << decisions.back().m_id << "\n";); + + r = l_false; + } + else { + lh.flip_prefix(); + lh.push(~l, lh.c_fixed_truth); + decisions.back().negate(); + r = cube(decisions, lh); + } if (r == l_false) { lh.pop(); decisions.pop_back(); @@ -128,106 +134,26 @@ lbool ccc::cube2(unsigned& branch_id, svector& decisions, lookahead& l return r; } -bool ccc::contains_branch(svector const& decisions, unsigned branch_id) const { - for (unsigned i = 0; i < decisions.size(); ++i) { - if (branch_id == decisions[i].m_id) return true; +unsigned ccc::spawn_conquer(svector const& decisions) { + unsigned result = 0; + // + // decisions must have been solved at a higher level by a conquer thread + // + if (!m_free_threads.empty() && m_last_closure_level <= 1 + decisions.size() + m_free_threads.size()) { + result = m_free_threads.back(); + m_free_threads.pop_back(); + IF_VERBOSE(1, verbose_stream() << "spawn " << result << "\n";); } - return false; + return result; +} + +void ccc::free_conquer(unsigned thread_id) { + m_free_threads.push_back(thread_id); } -lbool ccc::cube() { - unsigned branch_id = 0; - unsigned_vector id_trail; - - lookahead lh(m_s); - lh.init_search(); - lh.m_model.reset(); - - lookahead::scoped_level _sl(lh, lh.c_fixed_truth); - literal_vector trail; - svector decisions; - lh.m_search_mode = lookahead_mode::searching; - lh.m_blocked_literal = null_literal; - while (!m_cancel) { - - m_s.checkpoint(); - - SASSERT(trail.size() <= decisions.size()); - while (trail.size() < decisions.size()) { - //check_non_model("lh inconsistent ", decisions); - decisions.pop_back(); - id_trail.pop_back(); - } - SASSERT(id_trail.size() == trail.size()); - SASSERT(id_trail.size() == decisions.size()); - - TRACE("sat", lh.display(tout);); - - if (lh.inconsistent()) { - if (!lh.backtrack(trail)) return l_false; - continue; - } - - lh.inc_istamp(); - - // check if CDCL solver got ahead. - bool repeat = false; - #pragma omp critical (ccc_solved) - { - if (!m_solved.empty()) { - unsigned solved_id = m_solved.top(); - if (id_trail.contains(solved_id)) { - IF_VERBOSE(1, verbose_stream() << "cconquer " << decisions.size() << "\n";); - lh.set_conflict(); - } - else { - m_solved.pop(); - } - repeat = true; - } - } - if (repeat) continue; - - literal l = lh.choose(); - if (lh.inconsistent()) { - if (!lh.backtrack(trail)) return l_false; - continue; - } - if (l == null_literal) { - m_model = lh.get_model(); - return l_true; - } - - // update trail and set of ids - - ++branch_id; - ++lh.m_stats.m_decisions; - unsigned parent_id = id_trail.empty() ? 0 : id_trail.back(); - decision d(branch_id, trail.size() + 1, l, lh.m_blocked_literal, parent_id); - id_trail.push_back(branch_id); - trail.push_back(l); - decisions.push_back(d); - SASSERT(id_trail.size() == trail.size()); - lh.m_blocked_literal = null_literal; - - #pragma omp critical (ccc_log) - { - IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";); - IF_VERBOSE(2, verbose_stream() << " " << trail << "\n"; pp(verbose_stream(), decisions) << "\n"; ); - } - #pragma omp critical (ccc_decisions) - { - m_decisions.push(d); - } - TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); - lh.push(l, lh.c_fixed_truth); - SASSERT(lh.inconsistent() || !lh.is_unsat()); - } - return l_undef; -} - -lbool ccc::conquer(solver& s) { +lbool ccc::conquer(solver& s, unsigned thread_id) { + SASSERT(thread_id > 0); try { if (s.inconsistent()) return l_false; s.init_search(); @@ -242,7 +168,7 @@ lbool ccc::conquer(solver& s) { while (true) { SASSERT(!s.inconsistent()); - lbool r = bounded_search(s, decisions); + lbool r = bounded_search(s, decisions, thread_id); if (r != l_undef) return r; @@ -257,17 +183,13 @@ lbool ccc::conquer(solver& s) { } } -void ccc::replay_decisions(solver& s, svector& decisions) { +void ccc::replay_decisions(solver& s, svector& decisions, unsigned thread_id) { s.propagate(true); for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < decisions.size(); ++i) { - decision d = decisions[i]; - literal lit = d.m_last; - lbool val = s.value(lit); - #pragma omp critical (ccc_log) - { - IF_VERBOSE(2, verbose_stream() << "replay " << lit << " " << val << "\n";); - } - if (!push_decision(s, d)) { + decision const& d = decisions[i]; + IF_VERBOSE(2, verbose_stream() << "replay " << d.get_literal(thread_id) << " " << s.value(d.get_literal(thread_id)) << "\n";); + + if (!push_decision(s, d, thread_id)) { // negation of decision is implied. // check_non_model("replay", decisions); decisions.resize(i); @@ -276,13 +198,73 @@ void ccc::replay_decisions(solver& s, svector& decisions) { } } -bool ccc::push_decision(solver& s, decision const& d) { - literal lit = d.m_last; +bool ccc::get_solved(svector& decisions) { + // check if CDCL solver got ahead. + bool found = false; + #pragma omp critical (ccc_solved) + { + while (!m_solved.empty()) { + solution const& sol = m_solved.top(); + unsigned branch_id = sol.m_branch_id; + unsigned thread_id = sol.m_thread_id; + SASSERT(thread_id > 0); + for (unsigned i = decisions.size(); i > 0; ) { + --i; + decision& d = decisions[i]; + if (branch_id == d.m_id) { + if (d.m_spawn_id == thread_id) { + SASSERT(d.m_spawn_id > 0); + free_conquer(thread_id); + IF_VERBOSE(1, verbose_stream() << "close " << i << "\n";); + d.close(); + } + else { + // IF_VERBOSE(1, verbose_stream() << "conquer " << branch_id << " " << i << " " << d.get_literal(thread_id) << "\n";); + found = true; + } + m_last_closure_level = d.m_depth; + break; + } + } + if (found) { + break; + } + // IF_VERBOSE(1, verbose_stream() << "not found: " << branch_id << " " << decisions.size() << "\n";); + m_solved.pop(); + } + } + return found; +} + +void ccc::put_decision(decision const& d) { + #pragma omp critical (ccc_decisions) + { + for (unsigned i = 0; i < m_num_conquer; ++i) { + m_decisions[i].push(d); + } + } +} + +bool ccc::get_decision(unsigned thread_id, decision& d) { + SASSERT(0 < thread_id && thread_id <= m_decisions.size()); + bool result = false; + #pragma omp critical (ccc_decisions) + { + if (!m_decisions[thread_id - 1].empty()) { + d = m_decisions[thread_id - 1].pop(); + result = true; + } + } + return result; +} + +bool ccc::push_decision(solver& s, decision const& d, unsigned thread_id) { + literal lit = d.get_literal(thread_id); switch (s.value(lit)) { case l_false: #pragma omp critical (ccc_solved) { - m_solved.push(d.m_id); + m_solved.push(solution(thread_id, d.m_id)); } //TBD: s.m_restart_threshold = s.m_config.m_restart_initial; @@ -297,40 +279,16 @@ bool ccc::push_decision(solver& s, decision const& d) { s.propagate(true); break; } - literal blocked = d.m_blocked; - if (false && blocked != null_literal) { - switch (s.value(blocked)) { - case l_false: - #pragma omp critical (ccc_solved) - { - m_solved.push(d.m_id); - } - return false; - case l_true: - break; - case l_undef: - //s.assign(blocked, justification()); - //s.propagate(true); - break; - } - } return true; } -bool ccc::cube_decision(solver& s, svector& decisions) { +bool ccc::cube_decision(solver& s, svector& decisions, unsigned thread_id) { decision d; bool use_cube_decision = false; SASSERT(s.m_qhead == s.m_trail.size()); - get_cube: - #pragma omp critical (ccc_decisions) - { - if (!m_decisions.empty()) { - d = m_decisions.pop(); - use_cube_decision = true; - } - } - if (!use_cube_decision) { + get_cube: + if (!get_decision(thread_id, d)) { return false; } @@ -338,42 +296,45 @@ bool ccc::cube_decision(solver& s, svector& decisions) { goto get_cube; } + if (!decisions.empty() && decisions.back().m_spawn_id == thread_id && decisions.back().m_depth < d.m_depth) { + goto get_cube; + } + while (!decisions.empty() && decisions.back().m_depth >= d.m_depth) { // check_non_model("cube decision", decisions); decisions.pop_back(); } + SASSERT(decisions.empty() || decisions.back().m_depth + 1 == d.m_depth); SASSERT(decisions.empty() || decisions.back().m_id == d.m_parent); s.pop_reinit(s.scope_lvl() - decisions.size()); SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.scope_lvl() == decisions.size()); - #pragma omp critical (ccc_log) - { - literal lit = d.m_last; - IF_VERBOSE(1, verbose_stream() << "cube " << decisions.size() << "\n";); - IF_VERBOSE(2, pp(verbose_stream() << "push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n"; - if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";); - } - if (push_decision(s, d)) { + literal lit = d.get_literal(thread_id); + IF_VERBOSE(1, verbose_stream() << "cube " << decisions.size() << " " << d.get_literal(thread_id) << "\n";); + IF_VERBOSE(2, pp(verbose_stream() << "push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n"; + if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";); + + if (push_decision(s, d, thread_id)) { decisions.push_back(d); } return true; } -lbool ccc::bounded_search(solver& s, svector& decisions) { +lbool ccc::bounded_search(solver& s, svector& decisions, unsigned thread_id) { while (true) { s.checkpoint(); bool done = false; while (!done) { - replay_decisions(s, decisions); + replay_decisions(s, decisions, thread_id); lbool is_sat = s.propagate_and_backjump_step(done); if (is_sat != l_true) return is_sat; } s.gc(); - if (!cube_decision(s, decisions) && !s.decide()) { + if (!cube_decision(s, decisions, thread_id) && !s.decide()) { lbool is_sat = s.final_check(); if (is_sat != l_undef) { return is_sat; @@ -383,26 +344,6 @@ lbool ccc::bounded_search(solver& s, svector& decisions) { } -void ccc::push_model(unsigned v, bool sign) { - if (m_values.size() <= v) { - m_values.resize(v + 1); - } - m_values[v] = sign; -} - -void ccc::check_non_model(char const* fn, svector const& decisions) { - for (unsigned i = 0; i < decisions.size(); ++i) { - decision d = decisions[i]; - literal lit = d.m_last; - if (m_values[lit.var()] != lit.sign()) return; - } - - #pragma omp critical (ccc_log) - { - pp(verbose_stream() << "backtracking from model " << fn << " ", decisions) << "\n"; - } -} - lbool ccc::search() { enum par_exception_kind { DEFAULT_EX, @@ -421,8 +362,10 @@ lbool ccc::search() { par_exception_kind ex_kind; unsigned error_code = 0; lbool result = l_undef; + m_decisions.reset(); - int num_threads = 2; // for ccc-infinity only two threads. s.m_config.m_num_threads + 1; + m_num_conquer = m_s.m_config.m_num_threads; + int num_threads = 1 + m_num_conquer; // for ccc-infinity only two threads. for (int i = 1; i < num_threads; ++i) { limits.push_back(reslimit()); @@ -431,6 +374,10 @@ lbool ccc::search() { solvers.push_back(s1); s1->copy(m_s); scoped_rlimit.push_child(&s1->rlimit()); + m_decisions.push_back(queue()); + } + for (unsigned i = 1; i < m_num_conquer; ++i) { + m_free_threads.push_back(i); } #pragma omp parallel for @@ -438,10 +385,10 @@ lbool ccc::search() { try { lbool r = l_undef; if (i == 0) { - r = cube2(); + r = cube(); } else { - r = conquer(*solvers[i-1]); + r = conquer(*solvers[i-1], i); } bool first = false; #pragma omp critical (par_solver) @@ -476,6 +423,7 @@ lbool ccc::search() { } for (unsigned i = 0; i < solvers.size(); ++i) { + solvers[i]->collect_statistics(m_stats); dealloc(solvers[i]); } @@ -497,3 +445,22 @@ lbool ccc::search() { return result; } + +#if 0 +void ccc::push_model(unsigned v, bool sign) { + if (m_values.size() <= v) { + m_values.resize(v + 1); + } + m_values[v] = sign; +} + +void ccc::check_non_model(char const* fn, svector const& decisions) { + for (unsigned i = 0; i < decisions.size(); ++i) { + decision d = decisions[i]; + literal lit = d.m_literal; + if (m_values[lit.var()] != lit.sign()) return; + } + + IF_VERBOSE(1, pp(verbose_stream() << "backtracking from model " << fn << " ", decisions) << "\n";); +} +#endif diff --git a/src/sat/sat_ccc.h b/src/sat/sat_ccc.h index 7d6000c93..21291c1aa 100644 --- a/src/sat/sat_ccc.h +++ b/src/sat/sat_ccc.h @@ -26,47 +26,55 @@ namespace sat { class ccc { struct decision { - unsigned m_id; - unsigned m_depth; - literal m_last; - literal m_blocked; - unsigned m_parent; - decision(unsigned id, unsigned d, literal last, literal blocked, unsigned parent_id): - m_id(id), m_depth(d), m_last(last), m_blocked(blocked), m_parent(parent_id) {} - decision(): m_id(0), m_depth(0), m_last(null_literal), m_parent(0) {} - + unsigned m_id; // unique identifier for decision + unsigned m_depth; // depth of decision + literal m_literal; // decision literal + unsigned m_parent; // id of parent + int m_spawn_id; // thread id of conquer thread processing complented branch. + // = 0 if not spawned. + // > 0 if active spawn is in progress + // < 0 if thread has closed the branch + decision(unsigned id, unsigned d, literal last, unsigned parent_id, unsigned spawn): + m_id(id), m_depth(d), m_literal(last), m_parent(parent_id), m_spawn_id(spawn) {} + decision(): + m_id(0), m_depth(0), m_literal(null_literal), m_parent(0), m_spawn_id(0) {} + + void close() { SASSERT(m_spawn_id > 0); m_spawn_id = -m_spawn_id; } + bool is_closed() const { return m_spawn_id < 0; } + void negate() { m_literal.neg(); m_spawn_id = 0; } + literal get_literal(unsigned thread_id) const { return thread_id == m_spawn_id ? ~m_literal : m_literal; } std::ostream& pp(std::ostream& out) const; }; + struct solution { + unsigned m_thread_id; + unsigned m_branch_id; + solution(unsigned t, unsigned s): m_thread_id(t), m_branch_id(s) {} + }; + solver& m_s; - queue m_solved; - queue m_decisions; + queue m_solved; + vector > m_decisions; + unsigned m_num_conquer; model m_model; volatile bool m_cancel; + unsigned m_branch_id; + unsigned_vector m_free_threads; + unsigned m_last_closure_level; + ::statistics m_stats; - svector m_values; + lbool conquer(solver& s, unsigned thread_id); + bool cube_decision(solver& s, svector& decisions, unsigned thread_id); - struct config { - config() { - } - }; - - struct stats { - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - lbool conquer(solver& s); - bool cube_decision(solver& s, svector& decisions); - - lbool bounded_search(solver& s, svector& decisions); + lbool bounded_search(solver& s, svector& decisions, unsigned thread_id); + bool push_decision(solver& s, decision const& d, unsigned thread_id); lbool cube(); - bool push_decision(solver& s, decision const& d); + lbool cube(svector& decisions, lookahead& lh); + void put_decision(decision const& d); + bool get_decision(unsigned thread_id, decision& d); + bool get_solved(svector& decisions); - lbool cube2(); - lbool cube2(unsigned& branch_id, svector& decisions, lookahead& lh); - - void replay_decisions(solver& s, svector& decisions); + void replay_decisions(solver& s, svector& decisions, unsigned thread_id); static std::ostream& pp(std::ostream& out, svector const& v); @@ -76,7 +84,8 @@ namespace sat { void check_non_model(char const* fn, svector const& decisions); - bool contains_branch(svector const& decisions, unsigned branch_id) const; + unsigned spawn_conquer(svector const& decisions); + void free_conquer(unsigned thread_id); public: @@ -86,6 +95,7 @@ namespace sat { model const& get_model() const { return m_model; } + void collect_statistics(::statistics& st) { st.copy(m_stats); } }; } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index a0b82cf45..0cc4678dd 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -161,8 +161,7 @@ namespace sat { lookahead_mode m_search_mode; // mode of search stats m_stats; model m_model; - literal m_blocked_literal; - + // --------------------------------------- // truth values @@ -1713,8 +1712,7 @@ namespace sat { if (trail.empty()) return false; pop(); flip_prefix(); - m_blocked_literal = trail.back(); - assign(~m_blocked_literal); + assign(~trail.back()); trail.pop_back(); propagate(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4647ddb36..fa8663db8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -874,7 +874,7 @@ namespace sat { scoped_rl.push_child(&srch.rlimit()); lbool r = srch.check(num_lits, lits, 0); m_model = srch.get_model(); - // srch.collect_statistics(m_lookahead_stats); + // srch.collect_statistics(m_aux_stats); return r; } @@ -882,6 +882,7 @@ namespace sat { ccc c(*this); lbool r = c.search(); m_model = c.get_model(); + c.collect_statistics(m_aux_stats); return r; } @@ -893,10 +894,10 @@ namespace sat { m_model = lh.get_model(); } catch (z3_exception&) { - lh.collect_statistics(m_lookahead_stats); + lh.collect_statistics(m_aux_stats); throw; } - lh.collect_statistics(m_lookahead_stats); + lh.collect_statistics(m_aux_stats); return r; } @@ -2808,7 +2809,7 @@ namespace sat { m_asymm_branch.collect_statistics(st); m_probing.collect_statistics(st); if (m_ext) m_ext->collect_statistics(st); - st.copy(m_lookahead_stats); + st.copy(m_aux_stats); } void solver::reset_statistics() { @@ -2817,7 +2818,7 @@ namespace sat { m_simplifier.reset_statistics(); m_asymm_branch.reset_statistics(); m_probing.reset_statistics(); - m_lookahead_stats.reset(); + m_aux_stats.reset(); } // ----------------------- diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index fda8362ca..dec32f11a 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -141,7 +141,7 @@ namespace sat { unsigned m_par_num_vars; bool m_par_syncing_clauses; - statistics m_lookahead_stats; + statistics m_aux_stats; void del_clauses(clause * const * begin, clause * const * end); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26395f9ab..6598c3a05 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -288,7 +288,7 @@ void asserted_formulas::reduce() { } void asserted_formulas::eliminate_and() { - IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";); set_eliminate_and(true); reduce_asserted_formulas(); TRACE("after_elim_and", display(tout);); @@ -393,19 +393,19 @@ void asserted_formulas::find_macros_core() { } void asserted_formulas::find_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.find-macros)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.find-macros)\n";); TRACE("before_find_macros", display(tout);); find_macros_core(); TRACE("after_find_macros", display(tout);); } void asserted_formulas::expand_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";); find_macros_core(); } void asserted_formulas::apply_quasi_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";); TRACE("before_quasi_macros", display(tout);); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); @@ -423,7 +423,7 @@ void asserted_formulas::apply_quasi_macros() { } void asserted_formulas::nnf_cnf() { - IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.nnf)\n";); nnf apply_nnf(m_manager, m_defined_names); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); @@ -473,7 +473,7 @@ void asserted_formulas::nnf_cnf() { #define MK_SIMPLE_SIMPLIFIER(NAME, FUNCTOR_DEF, LABEL, MSG) \ void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(LABEL, tout << "before:\n"; display(tout);); \ FUNCTOR_DEF; \ expr_ref_vector new_exprs(m_manager); \ @@ -508,13 +508,13 @@ void asserted_formulas::NAME() { MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall"); void asserted_formulas::reduce_and_solve() { - IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";); flush_cache(); // collect garbage reduce_asserted_formulas(); } void asserted_formulas::infer_patterns() { - IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";); TRACE("before_pattern_inference", display(tout);); pattern_inference infer(m_manager, m_params); expr_ref_vector new_exprs(m_manager); @@ -552,7 +552,7 @@ void asserted_formulas::commit(unsigned new_qhead) { } void asserted_formulas::eliminate_term_ite() { - IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";); TRACE("before_elim_term_ite", display(tout);); elim_term_ite elim(m_manager, m_defined_names); expr_ref_vector new_exprs(m_manager); @@ -589,7 +589,7 @@ void asserted_formulas::eliminate_term_ite() { } void asserted_formulas::propagate_values() { - IF_IVERBOSE(10, verbose_stream() << "(smt.constant-propagation)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.constant-propagation)\n";); TRACE("propagate_values", tout << "before:\n"; display(tout);); flush_cache(); bool found = false; @@ -673,7 +673,7 @@ void asserted_formulas::propagate_booleans() { flush_cache(); while (cont) { TRACE("propagate_booleans", tout << "before:\n"; display(tout);); - IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-booleans)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.propagate-booleans)\n";); cont = false; unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); @@ -716,7 +716,7 @@ void asserted_formulas::propagate_booleans() { #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ bool asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ FUNCTOR; \ bool changed = false; \ @@ -773,7 +773,7 @@ proof * asserted_formulas::get_inconsistency_proof() const { } void asserted_formulas::refine_inj_axiom() { - IF_IVERBOSE(10, verbose_stream() << "(smt.refine-injectivity)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.refine-injectivity)\n";); TRACE("inj_axiom", display(tout);); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); @@ -805,7 +805,7 @@ MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_el #define LIFT_ITE(NAME, FUNCTOR, MSG) \ void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE("lift_ite", display(tout);); \ FUNCTOR; \ unsigned i = m_asserted_qhead; \ @@ -817,7 +817,7 @@ void asserted_formulas::NAME() { proof_ref new_pr(m_manager); \ functor(n, new_n, new_pr); \ TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \ - IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ + IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ m_asserted_formulas.set(i, new_n); \ if (m_manager.proofs_enabled()) { \ new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ @@ -841,7 +841,7 @@ unsigned asserted_formulas::get_total_size() const { } void asserted_formulas::max_bv_sharing() { - IF_IVERBOSE(10, verbose_stream() << "(smt.maximizing-bv-sharing)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.maximizing-bv-sharing)\n";); TRACE("bv_sharing", display(tout);); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); diff --git a/src/util/util.cpp b/src/util/util.cpp index bfd4923a8..50d93913a 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -17,6 +17,9 @@ Revision History: --*/ +#ifdef _WINDOWS +#include "windows.h" +#endif #include"util.h" static unsigned g_verbosity_level = 0; @@ -35,6 +38,19 @@ void set_verbose_stream(std::ostream& str) { g_verbose_stream = &str; } +static int g_thread_id = 0; +static bool g_is_threaded = false; + +bool is_threaded() { + if (g_is_threaded) return true; +#ifdef _WINDOWS + int thid = GetCurrentThreadId(); + g_is_threaded = g_thread_id != thid && g_thread_id != 0; + g_thread_id = thid; +#endif + return g_is_threaded; +} + std::ostream& verbose_stream() { return *g_verbose_stream; } diff --git a/src/util/util.h b/src/util/util.h index a040a79ae..e62f24e44 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -24,6 +24,7 @@ Revision History: #include #include #include +#include"z3_omp.h" #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -182,16 +183,26 @@ void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str); +bool is_threaded(); -#define IF_VERBOSE(LVL, CODE) { if (get_verbosity_level() >= LVL) { CODE } } ((void) 0) - -#ifdef _EXTERNAL_RELEASE -#define IF_IVERBOSE(LVL, CODE) ((void) 0) -#else -#define IF_IVERBOSE(LVL, CODE) { if (get_verbosity_level() >= LVL) { CODE } } ((void) 0) -#endif - + +#define IF_VERBOSE(LVL, CODE) { \ + if (get_verbosity_level() >= LVL) { \ + if (is_threaded()) { \ + LOCK_CODE(CODE); \ + } \ + else { \ + CODE; \ + } \ + } } ((void) 0) +#define LOCK_CODE(CODE) \ + { \ + __pragma(omp critical (verbose_lock)) \ + { \ + CODE; \ + } \ + } template struct default_eq {