Skip to content

Commit 3ccf7a6

Browse files
NikolajBjornerNikolajBjorner
committed
make concurrent collect_statistics in a timeout thread safe
1 parent 951554e commit 3ccf7a6

File tree

1 file changed

+52
-45
lines changed

1 file changed

+52
-45
lines changed

‎src/smt/tactic/smt_tactic_core.cpp‎

Lines changed: 52 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ Module Name:
3232
#include "solver/mus.h"
3333
#include "solver/parallel_tactical.h"
3434
#include "solver/parallel_params.hpp"
35+
#include <mutex>
3536

3637
typedef obj_map<expr, expr *> expr2expr_map;
3738

@@ -43,11 +44,12 @@ class smt_tactic : public tactic {
4344
expr_ref_vector m_vars;
4445
vector<std::pair<expr_ref, expr_ref>> m_values;
4546
statistics m_stats;
46-
smt::kernel* m_ctx = nullptr;
47+
std::atomic<smt::kernel*> m_ctx = nullptr;
4748
symbol m_logic;
4849
progress_callback* m_callback = nullptr;
4950
bool m_candidate_models = false;
5051
bool m_fail_if_inconclusive = false;
52+
mutable std::mutex m_mutex;
5153

5254
public:
5355
smt_tactic(ast_manager& m, params_ref const & p):
@@ -63,7 +65,7 @@ class smt_tactic : public tactic {
6365
}
6466

6567
~smt_tactic() override {
66-
SASSERT(m_ctx == nullptr);
68+
SASSERT(m_ctx.load() == nullptr);
6769
}
6870

6971
char const* name() const override { return "smt"; }
@@ -88,8 +90,8 @@ class smt_tactic : public tactic {
8890
fparams().updt_params(p);
8991
m_params_ref.copy(p);
9092
m_logic = p.get_sym(symbol("logic"), m_logic);
91-
if (m_logic != symbol::null && m_ctx) {
92-
m_ctx->set_logic(m_logic);
93+
if (m_logic != symbol::null && m_ctx.load()) {
94+
m_ctx.load()->set_logic(m_logic);
9395
}
9496
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
9597
}
@@ -99,12 +101,15 @@ class smt_tactic : public tactic {
99101
smt_params_helper::collect_param_descrs(r);
100102
}
101103

102-
103104
void collect_statistics(statistics & st) const override {
104-
if (m_ctx)
105-
m_ctx->collect_statistics(st); // ctx is still running...
106-
else
107-
st.copy(m_stats);
105+
if (m_ctx.load()) {
106+
std::scoped_lock lock(m_mutex);
107+
if (m_ctx.load()) {
108+
m_ctx.load()->collect_statistics(st); // ctx is still running...
109+
return;
110+
}
111+
}
112+
st.copy(m_stats);
108113
}
109114

110115
void cleanup() override {
@@ -141,10 +146,13 @@ class smt_tactic : public tactic {
141146
}
142147

143148
~scoped_init_ctx() {
144-
smt::kernel * d = m_owner.m_ctx;
145-
m_owner.m_ctx = nullptr;
146-
m_owner.m_user_ctx = nullptr;
147-
149+
smt::kernel* d = nullptr;
150+
{
151+
std::scoped_lock lock(m_owner.m_mutex);
152+
d = m_owner.m_ctx.load();
153+
m_owner.m_ctx = nullptr;
154+
m_owner.m_user_ctx = nullptr;
155+
}
148156
if (d)
149157
dealloc(d);
150158
}
@@ -169,7 +177,7 @@ class smt_tactic : public tactic {
169177
TRACE(smt_tactic_detail, in->display(tout););
170178
TRACE(smt_tactic_memory, tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
171179
scoped_init_ctx init(*this, m);
172-
SASSERT(m_ctx);
180+
SASSERT(m_ctx.load());
173181

174182
expr_ref_vector clauses(m);
175183
expr2expr_map bool2dep;
@@ -182,41 +190,40 @@ class smt_tactic : public tactic {
182190
if (in->proofs_enabled() && !assumptions.empty())
183191
throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
184192
for (unsigned i = 0; i < clauses.size(); ++i) {
185-
m_ctx->assert_expr(clauses[i].get());
193+
m_ctx.load()->assert_expr(clauses[i].get());
186194
}
187195
}
188196
else if (in->proofs_enabled()) {
189197
unsigned sz = in->size();
190198
for (unsigned i = 0; i < sz; i++) {
191-
m_ctx->assert_expr(in->form(i), in->pr(i));
199+
m_ctx.load()->assert_expr(in->form(i), in->pr(i));
192200
}
193201
}
194202
else {
195203
unsigned sz = in->size();
196204
for (unsigned i = 0; i < sz; i++) {
197-
m_ctx->assert_expr(in->form(i));
205+
m_ctx.load()->assert_expr(in->form(i));
198206
}
199207
}
200-
if (m_ctx->canceled()) {
208+
if (m_ctx.load()->canceled()) {
201209
throw tactic_exception(Z3_CANCELED_MSG);
202210
}
203211
user_propagate_delay_init();
204212

205213
lbool r;
206214
try {
207215
if (assumptions.empty() && !m_user_ctx)
208-
r = m_ctx->setup_and_check();
216+
r = m_ctx.load()->setup_and_check();
209217
else
210-
r = m_ctx->check(assumptions.size(), assumptions.data());
218+
r = m_ctx.load()->check(assumptions.size(), assumptions.data());
211219
}
212220
catch(...) {
213221
TRACE(smt_tactic, tout << "exception\n";);
214-
m_ctx->collect_statistics(m_stats);
222+
m_ctx.load()->collect_statistics(m_stats);
215223
throw;
216224
}
217-
SASSERT(m_ctx);
218-
m_ctx->collect_statistics(m_stats);
219-
proof_ref pr(m_ctx->get_proof(), m);
225+
m_ctx.load()->collect_statistics(m_stats);
226+
proof_ref pr(m_ctx.load()->get_proof(), m);
220227
TRACE(smt_tactic, tout << r << " " << pr << "\n";);
221228
switch (r) {
222229
case l_true: {
@@ -228,17 +235,17 @@ class smt_tactic : public tactic {
228235
// store the model in a no-op model converter, and filter fresh Booleans
229236
if (in->models_enabled()) {
230237
model_ref md;
231-
m_ctx->get_model(md);
238+
m_ctx.load()->get_model(md);
232239
buffer<symbol> r;
233-
m_ctx->get_relevant_labels(nullptr, r);
240+
m_ctx.load()->get_relevant_labels(nullptr, r);
234241
labels_vec rv;
235242
rv.append(r.size(), r.data());
236243
model_converter_ref mc;
237244
mc = model_and_labels2model_converter(md.get(), rv);
238245
mc = concat(fmc.get(), mc.get());
239246
in->add(mc.get());
240247
}
241-
if (m_ctx->canceled())
248+
if (m_ctx.load()->canceled())
242249
throw tactic_exception(Z3_CANCELED_MSG);
243250
return;
244251
}
@@ -251,9 +258,9 @@ class smt_tactic : public tactic {
251258
in->reset();
252259
expr_dependency * lcore = nullptr;
253260
if (in->unsat_core_enabled()) {
254-
unsigned sz = m_ctx->get_unsat_core_size();
261+
unsigned sz = m_ctx.load()->get_unsat_core_size();
255262
for (unsigned i = 0; i < sz; i++) {
256-
expr * b = m_ctx->get_unsat_core_expr(i);
263+
expr * b = m_ctx.load()->get_unsat_core_expr(i);
257264
SASSERT(is_uninterp_const(b) && m.is_bool(b));
258265
expr * d = bool2dep.find(b);
259266
lcore = m.mk_join(lcore, m.mk_leaf(d));
@@ -269,13 +276,13 @@ class smt_tactic : public tactic {
269276
}
270277
case l_undef:
271278

272-
if (m_ctx->canceled() && !pr) {
279+
if (m_ctx.load()->canceled() && !pr) {
273280
throw tactic_exception(Z3_CANCELED_MSG);
274281
}
275282

276283
if (m_fail_if_inconclusive && !m_candidate_models && !pr) {
277284
std::stringstream strm;
278-
strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string();
285+
strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx.load()->last_failure_as_string();
279286
throw tactic_exception(strm.str());
280287
}
281288
result.push_back(in.get());
@@ -285,15 +292,15 @@ class smt_tactic : public tactic {
285292
in->updt_prec(goal::UNDER_OVER);
286293
}
287294
if (m_candidate_models) {
288-
switch (m_ctx->last_failure()) {
295+
switch (m_ctx.load()->last_failure()) {
289296
case smt::NUM_CONFLICTS:
290297
case smt::THEORY:
291298
case smt::QUANTIFIERS:
292299
if (in->models_enabled()) {
293300
model_ref md;
294-
m_ctx->get_model(md);
301+
m_ctx.load()->get_model(md);
295302
buffer<symbol> r;
296-
m_ctx->get_relevant_labels(nullptr, r);
303+
m_ctx.load()->get_relevant_labels(nullptr, r);
297304
labels_vec rv;
298305
rv.append(r.size(), r.data());
299306
in->add(model_and_labels2model_converter(md.get(), rv));
@@ -306,7 +313,7 @@ class smt_tactic : public tactic {
306313
if (pr) {
307314
return;
308315
}
309-
throw tactic_exception(m_ctx->last_failure_as_string());
316+
throw tactic_exception(m_ctx.load()->last_failure_as_string());
310317
}
311318
}
312319
catch (rewriter_exception & ex) {
@@ -329,24 +336,24 @@ class smt_tactic : public tactic {
329336

330337
void on_clause_delay_init() {
331338
if (m_on_clause_eh)
332-
m_ctx->register_on_clause(m_on_clause_ctx, m_on_clause_eh);
339+
m_ctx.load()->register_on_clause(m_on_clause_ctx, m_on_clause_eh);
333340
}
334341

335342
void user_propagate_delay_init() {
336343
if (!m_user_ctx)
337344
return;
338-
m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
339-
if (m_fixed_eh) m_ctx->user_propagate_register_fixed(m_fixed_eh);
340-
if (m_final_eh) m_ctx->user_propagate_register_final(m_final_eh);
341-
if (m_eq_eh) m_ctx->user_propagate_register_eq(m_eq_eh);
342-
if (m_diseq_eh) m_ctx->user_propagate_register_diseq(m_diseq_eh);
343-
if (m_created_eh) m_ctx->user_propagate_register_created(m_created_eh);
344-
if (m_decide_eh) m_ctx->user_propagate_register_decide(m_decide_eh);
345+
m_ctx.load()->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
346+
if (m_fixed_eh) m_ctx.load()->user_propagate_register_fixed(m_fixed_eh);
347+
if (m_final_eh) m_ctx.load()->user_propagate_register_final(m_final_eh);
348+
if (m_eq_eh) m_ctx.load()->user_propagate_register_eq(m_eq_eh);
349+
if (m_diseq_eh) m_ctx.load()->user_propagate_register_diseq(m_diseq_eh);
350+
if (m_created_eh) m_ctx.load()->user_propagate_register_created(m_created_eh);
351+
if (m_decide_eh) m_ctx.load()->user_propagate_register_decide(m_decide_eh);
345352

346353
for (expr* v : m_vars)
347-
m_ctx->user_propagate_register_expr(v);
354+
m_ctx.load()->user_propagate_register_expr(v);
348355
for (auto& [var, value] : m_values)
349-
m_ctx->user_propagate_initialize_value(var, value);
356+
m_ctx.load()->user_propagate_initialize_value(var, value);
350357
}
351358

352359
void user_propagate_clear() override {

0 commit comments

Comments
 (0)