mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

moving to resource managed cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 13:13:11 -08:00
parent 61dbb6168e
commit 32b6b2da44
41 changed files with 55 additions and 280 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/bcd2.cpp
View file

@ -118,7 +118,7 @@ namespace opt {
expr_ref_vector asms(m);
init();
init_bcd();
if (m_cancel) {
if (m.canceled()) {
normalize_bounds();
return l_undef;
}
@ -130,7 +130,7 @@ namespace opt {
TRACE("opt", display(tout););
assert_cores();
set2asms(m_asm_set, asms);
if (m_cancel) {
if (m.canceled()) {
normalize_bounds();
return l_undef;
}

6
src/opt/maxhs.cpp
View file

@ -83,10 +83,6 @@ namespace opt {
}
virtual ~maxhs() {}
virtual void set_cancel(bool f) {
maxsmt_solver_base::set_cancel(f);
}
virtual void collect_statistics(statistics& st) const {
maxsmt_solver_base::collect_statistics(st);
m_hs.collect_statistics(st);
@ -113,7 +109,7 @@ namespace opt {
++m_stats.m_num_iterations;
trace_bounds("maxhs");
TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}

9
src/opt/maxres.cpp
View file

@ -200,7 +200,7 @@ public:
display(tout);
);
is_sat = check_sat_hill_climb(m_asms);
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
switch (is_sat) {
@ -233,7 +233,7 @@ public:
exprs cs;
while (m_lower < m_upper) {
lbool is_sat = check_sat_hill_climb(m_asms);
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
switch (is_sat) {
@ -786,11 +786,6 @@ public:
remove_soft(core, m_asms);
}
virtual void set_cancel(bool f) {
maxsmt_solver_base::set_cancel(f);
m_mus.set_cancel(f);
}
virtual void updt_params(params_ref& p) {
maxsmt_solver_base::updt_params(p);
opt_params _p(p);

10
src/opt/maxsmt.cpp
View file

@ -39,7 +39,6 @@ namespace opt {
maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& soft):
m(c.get_manager()),
m_c(c),
m_cancel(false),
m_soft(soft),
m_weights(ws),
m_assertions(m) {
@ -150,7 +149,7 @@ namespace opt {
maxsmt::maxsmt(maxsat_context& c):
m(c.get_manager()), m_c(c), m_cancel(false),
m(c.get_manager()), m_c(c),
m_soft_constraints(m), m_answer(m) {}
lbool maxsmt::operator()() {
@ -274,13 +273,6 @@ namespace opt {
}
}
void maxsmt::set_cancel(bool f) {
m_cancel = f;
if (m_msolver) {
m_msolver->set_cancel(f);
}
}
bool maxsmt::is_maxsat_problem(vector<rational> const& ws) const {
for (unsigned i = 0; i < ws.size(); ++i) {

5
src/opt/maxsmt.h
View file

@ -44,7 +44,6 @@ namespace opt {
virtual rational get_lower() const = 0;
virtual rational get_upper() const = 0;
virtual bool get_assignment(unsigned index) const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
virtual void updt_params(params_ref& p) = 0;
@ -60,7 +59,6 @@ namespace opt {
protected:
ast_manager& m;
maxsat_context& m_c;
volatile bool m_cancel;
const expr_ref_vector m_soft;
vector<rational> m_weights;
expr_ref_vector m_assertions;
@ -78,7 +76,6 @@ namespace opt {
virtual rational get_lower() const { return m_lower; }
virtual rational get_upper() const { return m_upper; }
virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
virtual void collect_statistics(statistics& st) const { }
virtual void get_model(model_ref& mdl, svector<symbol>& labels) { mdl = m_model.get(); labels = m_labels;}
virtual void commit_assignment();
@ -115,7 +112,6 @@ namespace opt {
ast_manager& m;
maxsat_context& m_c;
scoped_ptr<maxsmt_solver_base> m_msolver;
volatile bool m_cancel;
expr_ref_vector m_soft_constraints;
expr_ref_vector m_answer;
vector<rational> m_weights;
@ -128,7 +124,6 @@ namespace opt {
public:
maxsmt(maxsat_context& c);
lbool operator()();
void set_cancel(bool f);
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }

4
src/opt/mss.cpp
View file

@ -26,7 +26,7 @@ Notes:
namespace opt {
mss::mss(solver& s, ast_manager& m): m_s(s), m(m), m_cancel(false) {
mss::mss(solver& s, ast_manager& m): m_s(s), m(m) {
}
mss::~mss() {
@ -191,7 +191,7 @@ namespace opt {
if (core.empty()) {
return l_true;
}
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {

2
src/opt/mss.h
View file

@ -23,7 +23,6 @@ namespace opt {
class mss {
solver& m_s;
ast_manager& m;
volatile bool m_cancel;
typedef ptr_vector<expr> exprs;
typedef obj_hashtable<expr> expr_set;
exprs m_mss;
@ -38,7 +37,6 @@ namespace opt {
lbool operator()(model* initial_model, vector<exprs> const& cores, exprs& literals, exprs& mcs);
void set_cancel(bool f) { m_cancel = f; }
void get_model(model_ref& mdl) { mdl = m_model; }

20
src/opt/opt_context.cpp
View file

@ -1259,26 +1259,6 @@ namespace opt {
}
}
void context::set_cancel(bool f) {
#pragma omp critical (opt_context)
{
if (m_solver) {
if (f) m_solver->cancel(); else m_solver->reset_cancel();
}
if (m_pareto) {
m_pareto->set_cancel(f);
}
if (m_simplify) {
if (f) m_simplify->cancel(); else m_solver->reset_cancel();
}
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
it->m_value->set_cancel(f);
}
}
m_optsmt.set_cancel(f);
}
void context::collect_statistics(statistics& stats) const {
if (m_solver) {
m_solver->collect_statistics(stats);

3
src/opt/opt_context.h
View file

@ -174,9 +174,6 @@ namespace opt {
virtual void push();
virtual void pop(unsigned n);
virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
virtual void set_cancel(bool f);
virtual void reset_cancel() { set_cancel(false); }
virtual void cancel() { set_cancel(true); }
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;

4
src/opt/opt_pareto.cpp
View file

@ -34,7 +34,7 @@ namespace opt {
{
solver::scoped_push _s(*m_solver.get());
while (is_sat == l_true) {
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
m_solver->get_model(m_model);
@ -92,7 +92,7 @@ namespace opt {
lbool oia_pareto::operator()() {
solver::scoped_push _s(*m_solver.get());
lbool is_sat = m_solver->check_sat(0, 0);
if (m_cancel) {
if (m.canceled()) {
is_sat = l_undef;
}
if (is_sat == l_true) {

9
src/opt/opt_pareto.h
View file

@ -37,7 +37,6 @@ namespace opt {
protected:
ast_manager& m;
pareto_callback& cb;
volatile bool m_cancel;
ref<solver> m_solver;
params_ref m_params;
model_ref m_model;
@ -50,7 +49,6 @@ namespace opt {
params_ref & p):
m(m),
cb(cb),
m_cancel(false),
m_solver(s),
m_params(p) {
}
@ -65,13 +63,6 @@ namespace opt {
virtual void collect_statistics(statistics & st) const {
m_solver->collect_statistics(st);
}
virtual void set_cancel(bool f) {
if (f)
m_solver->cancel();
else
m_solver->reset_cancel();
m_cancel = f;
}
virtual void display(std::ostream & out) const {
m_solver->display(out);
}

29
src/opt/optsmt.cpp
View file

@ -41,11 +41,6 @@ Notes:
namespace opt {
void optsmt::set_cancel(bool f) {
TRACE("opt", tout << "set cancel: " << f << "\n";);
m_cancel = f;
}
void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls) {
for (unsigned i = 0; i < src.size(); ++i) {
if (src[i] >= dst[i]) {
@ -74,7 +69,7 @@ namespace opt {
expr* vars[1];
solver::scoped_push _push(*m_s);
while (is_sat == l_true && !m_cancel) {
while (is_sat == l_true && !m.canceled()) {
tmp = m.mk_fresh_const("b", m.mk_bool_sort());
vars[0] = tmp;
@ -86,7 +81,7 @@ namespace opt {
}
}
if (m_cancel || is_sat == l_undef) {
if (m.canceled() || is_sat == l_undef) {
return l_undef;
}
@ -110,11 +105,11 @@ namespace opt {
lbool is_sat = l_true;
while (is_sat == l_true && !m_cancel) {
while (is_sat == l_true && !m.canceled()) {
is_sat = update_upper();
}
if (m_cancel || is_sat == l_undef) {
if (m.canceled() || is_sat == l_undef) {
return l_undef;
}
@ -150,7 +145,7 @@ namespace opt {
lbool is_sat = l_true;
solver::scoped_push _push(*m_s);
while (!m_cancel) {
while (!m.canceled()) {
m_s->assert_expr(fml);
TRACE("opt", tout << fml << "\n";);
is_sat = m_s->check_sat(1,vars);
@ -185,7 +180,7 @@ namespace opt {
bound = m.mk_or(m_lower_fmls.size(), m_lower_fmls.c_ptr());
m_s->assert_expr(bound);
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
return basic_opt();
@ -242,7 +237,7 @@ namespace opt {
vector<inf_eps> mid;
for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
if (m_lower[i] < m_upper[i]) {
mid.push_back((m_upper[i]+m_lower[i])/rational(2));
bound = m_s->mk_ge(i, mid[i]);
@ -254,7 +249,7 @@ namespace opt {
}
}
bool progress = false;
for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) {
th.enable_record_conflict(bounds[i].get());
lbool is_sat = m_s->check_sat(1, bounds.c_ptr() + i);
@ -284,7 +279,7 @@ namespace opt {
progress = true;
}
}
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
if (!progress) {
@ -328,7 +323,7 @@ namespace opt {
for (unsigned i = 0; i < obj_index; ++i) {
commit_assignment(i);
}
while (is_sat == l_true && !m_cancel) {
while (is_sat == l_true && !m.canceled()) {
is_sat = m_s->check_sat(0, 0);
if (is_sat != l_true) break;
@ -357,8 +352,8 @@ namespace opt {
// on current state.
}
if (m_cancel || is_sat == l_undef) {
TRACE("opt", tout << "undef: " << m_cancel << " " << is_sat << "\n";);
if (m.canceled() || is_sat == l_undef) {
TRACE("opt", tout << "undef: " << m.canceled() << " " << is_sat << "\n";);
return l_undef;
}

5
src/opt/optsmt.h
View file

@ -30,7 +30,6 @@ namespace opt {
class optsmt {
ast_manager& m;
opt_solver* m_s;
volatile bool m_cancel;
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
app_ref_vector m_objs;
@ -42,7 +41,7 @@ namespace opt {
sref_vector<model> m_models;
public:
optsmt(ast_manager& m):
m(m), m_s(0), m_cancel(false), m_objs(m), m_lower_fmls(m) {}
m(m), m_s(0), m_objs(m), m_lower_fmls(m) {}
void setup(opt_solver& solver);
@ -52,8 +51,6 @@ namespace opt {
unsigned add(app* t);
void set_cancel(bool f);
void updt_params(params_ref& p);
unsigned get_num_objectives() const { return m_objs.size(); }

10
src/opt/pb_sls.cpp
View file

@ -60,7 +60,6 @@ namespace smt {
pb_util pb;
unsynch_mpz_manager mgr;
th_rewriter m_rewrite;
volatile bool m_cancel;
vector<clause> m_clauses; // clauses to be satisfied
expr_ref_vector m_orig_clauses; // for debugging
model_ref m_orig_model; // for debugging
@ -86,7 +85,6 @@ namespace smt {
m(m),
pb(m),
m_rewrite(m),
m_cancel(false),
m_orig_clauses(m),
m_trail(m),
one(mgr)
@ -157,7 +155,7 @@ namespace smt {
while (m_max_flips > 0) {
--m_max_flips;
literal lit = flip();
if (m_cancel) {
if (m.canceled()) {
return l_undef;
}
IF_VERBOSE(3, verbose_stream()
@ -203,9 +201,6 @@ namespace smt {
bool get_value(literal l) {
return l.sign() ^ m_assignment[l.var()];
}
void set_cancel(bool f) {
m_cancel = f;
}
void get_model(model_ref& mdl) {
mdl = alloc(model, m);
for (unsigned i = 1; i < m_var2decl.size(); ++i) {
@ -719,9 +714,6 @@ namespace smt {
lbool pb_sls::operator()() {
return (*m_imp)();
}
void pb_sls::set_cancel(bool f) {
m_imp->set_cancel(f);
}
void pb_sls::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}

1
src/opt/pb_sls.h
View file

@ -38,7 +38,6 @@ namespace smt {
bool soft_holds(unsigned index);
void set_model(model_ref& mdl);
lbool operator()();
void set_cancel(bool f);
void collect_statistics(::statistics& st) const;
void get_model(model_ref& mdl);
void updt_params(params_ref& p);

2
src/opt/wmax.cpp
View file

@ -47,7 +47,7 @@ namespace opt {
}
while (l_true == is_sat) {
is_sat = s().check_sat(0,0);
if (m_cancel) {
if (m.canceled()) {
is_sat = l_undef;
}
if (is_sat == l_true) {