mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
parallelizing ccc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
07fe45e923
commit
d052155f6e
8 changed files with 284 additions and 281 deletions
|
|
@ -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<decision> const& v) {
|
||||
|
|
@ -35,9 +52,9 @@ std::ostream& ccc::pp(std::ostream& out, svector<decision> 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<decision> 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<decision>& decisions, lookahead& lh) {
|
||||
lbool ccc::cube(svector<decision>& 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<decision>& 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<decision>& decisions, lookahead& l
|
|||
return r;
|
||||
}
|
||||
|
||||
bool ccc::contains_branch(svector<decision> 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<decision> 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<decision> 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<decision>& decisions) {
|
||||
void ccc::replay_decisions(solver& s, svector<decision>& 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<decision>& decisions) {
|
|||
}
|
||||
}
|
||||
|
||||
bool ccc::push_decision(solver& s, decision const& d) {
|
||||
literal lit = d.m_last;
|
||||
bool ccc::get_solved(svector<decision>& 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<decision>& decisions) {
|
||||
bool ccc::cube_decision(solver& s, svector<decision>& 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<decision>& 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<decision>& decisions) {
|
||||
lbool ccc::bounded_search(solver& s, svector<decision>& 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<decision>& 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<decision> 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<decision>());
|
||||
}
|
||||
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<decision> 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
|
||||
|
|
|
|||
|
|
@ -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<unsigned> m_solved;
|
||||
queue<decision> m_decisions;
|
||||
queue<solution> m_solved;
|
||||
vector<queue<decision> > 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<bool> m_values;
|
||||
lbool conquer(solver& s, unsigned thread_id);
|
||||
bool cube_decision(solver& s, svector<decision>& 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<decision>& decisions);
|
||||
|
||||
lbool bounded_search(solver& s, svector<decision>& decisions);
|
||||
lbool bounded_search(solver& s, svector<decision>& 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<decision>& decisions, lookahead& lh);
|
||||
void put_decision(decision const& d);
|
||||
bool get_decision(unsigned thread_id, decision& d);
|
||||
bool get_solved(svector<decision>& decisions);
|
||||
|
||||
lbool cube2();
|
||||
lbool cube2(unsigned& branch_id, svector<decision>& decisions, lookahead& lh);
|
||||
|
||||
void replay_decisions(solver& s, svector<decision>& decisions);
|
||||
void replay_decisions(solver& s, svector<decision>& decisions, unsigned thread_id);
|
||||
|
||||
static std::ostream& pp(std::ostream& out, svector<decision> const& v);
|
||||
|
||||
|
|
@ -76,7 +84,8 @@ namespace sat {
|
|||
|
||||
void check_non_model(char const* fn, svector<decision> const& decisions);
|
||||
|
||||
bool contains_branch(svector<decision> const& decisions, unsigned branch_id) const;
|
||||
unsigned spawn_conquer(svector<decision> 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); }
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
||||
// -----------------------
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
#include<iostream>
|
||||
#include<climits>
|
||||
#include<limits>
|
||||
#include"z3_omp.h"
|
||||
|
||||
#ifndef SIZE_MAX
|
||||
#define SIZE_MAX std::numeric_limits<std::size_t>::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<typename T>
|
||||
struct default_eq {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue