mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

attempt to fix build

Browse source
This commit is contained in:
Nuno Lopes 2020-02-01 10:52:16 +00:00
parent 9fab72b3ef
commit 3ec7146ec8
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_parallel.cpp
View file

@ -20,6 +20,7 @@ Author:
#include "ast/ast_translation.h" #include "ast/ast_translation.h"
#include "smt/smt_parallel.h" #include "smt/smt_parallel.h"
#include "smt/smt_lookahead.h" #include "smt/smt_lookahead.h"
#include <thread>
namespace smt { namespace smt {
@ -57,7 +58,7 @@ namespace smt {
pasms.push_back(tr(asms)); pasms.push_back(tr(asms));
} }
std::function<void(context&,expr_ref_vector&,expr_ref&)> cube = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) { auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
lookahead lh(ctx); lookahead lh(ctx);
c = lh.choose(); c = lh.choose();
if (c) lasms.push_back(c); if (c) lasms.push_back(c);
@ -100,6 +101,8 @@ namespace smt {
}; };
std::mutex mux; std::mutex mux;
unsigned num_iterations = 0;
auto worker_thread = [&](int i) { auto worker_thread = [&](int i) {
try { try {
IF_VERBOSE(0, verbose_stream() << "thread " << i << "\n";); IF_VERBOSE(0, verbose_stream() << "thread " << i << "\n";);
@ -109,7 +112,7 @@ namespace smt {
expr_ref c(pm); expr_ref c(pm);
pctx.get_fparams().m_max_conflicts = max_conflicts; pctx.get_fparams().m_max_conflicts = max_conflicts;
if (num_iterations > 0) { if (num_iterations++ > 0) {
cube(pctx, lasms, c); cube(pctx, lasms, c);
} }
lbool r = pctx.check(lasms.size(), lasms.c_ptr()); lbool r = pctx.check(lasms.size(), lasms.c_ptr());
@ -132,8 +135,8 @@ namespace smt {
result = r; result = r;
done = true; done = true;
} }
if (!first) return;
} }
if (!first) return;
for (ast_manager* m : pms) { for (ast_manager* m : pms) {
if (m != &pm) m->limit().cancel(); if (m != &pm) m->limit().cancel();