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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-16 11:23:03 -07:00
commit 66e6dc78a3
251 changed files with 14282 additions and 16741 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/opt/maxres.cpp
View file

@ -88,7 +88,7 @@ private:
expr_ref_vector m_asms;
expr_ref_vector m_defs;
obj_map<expr, rational> m_asm2weight;
ptr_vector<expr> m_new_core;
expr_ref_vector m_new_core;
mus m_mus;
expr_ref_vector m_trail;
strategy_t m_st;
@ -119,6 +119,7 @@ public:
maxsmt_solver_base(c, ws, soft),
m_index(index),
m_B(m), m_asms(m), m_defs(m),
m_new_core(m),
m_mus(c.get_solver()),
m_trail(m),
m_st(st),
@ -351,11 +352,13 @@ public:
exprs core;
while (is_sat == l_false) {
core.reset();
s().get_unsat_core(core);
// verify_core(core);
expr_ref_vector _core(m);
s().get_unsat_core(_core);
model_ref mdl;
get_mus_model(mdl);
is_sat = minimize_core(core);
is_sat = minimize_core(_core);
core.append(_core.size(), _core.c_ptr());
// verify_core(core);
++m_stats.m_num_cores;
if (is_sat != l_true) {
IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
@ -380,8 +383,8 @@ public:
}
TRACE("opt",
tout << "num cores: " << cores.size() << "\n";
for (unsigned i = 0; i < cores.size(); ++i) {
display_vec(tout, cores[i]);
for (auto const& c : cores) {
display_vec(tout, c);
}
tout << "num satisfying: " << asms.size() << "\n";);
@ -473,8 +476,8 @@ public:
}
void process_unsat(vector<exprs> const& cores) {
for (unsigned i = 0; i < cores.size(); ++i) {
process_unsat(cores[i]);
for (auto const & c : cores) {
process_unsat(c);
}
}
@ -538,7 +541,7 @@ public:
return nullptr != mdl.get();
}
lbool minimize_core(exprs& core) {
lbool minimize_core(expr_ref_vector& core) {
if (core.empty()) {
return l_true;
}
@ -599,8 +602,7 @@ public:
}
void display(std::ostream& out) {
for (unsigned i = 0; i < m_asms.size(); ++i) {
expr* a = m_asms[i].get();
for (expr * a : m_asms) {
out << mk_pp(a, m) << " : " << get_weight(a) << "\n";
}
}
@ -707,8 +709,8 @@ public:
void update_assignment(model* mdl) {
unsigned correction_set_size = 0;
for (unsigned i = 0; i < m_asms.size(); ++i) {
if (is_false(mdl, m_asms[i].get())) {
for (expr* a : m_asms) {
if (is_false(mdl, a)) {
++correction_set_size;
}
}
@ -719,10 +721,12 @@ public:
rational upper(0);
expr_ref tmp(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
if (!is_true(mdl, m_soft[i])) {
unsigned i = 0;
for (expr* s : m_soft) {
if (!is_true(mdl, s)) {
upper += m_weights[i];
}
++i;
}
if (upper > m_upper) {
@ -738,8 +742,9 @@ public:
TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0););
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);
i = 0;
for (expr* s : m_soft) {
m_assignment[i++] = is_true(s);
}
// DEBUG_CODE(verify_assignment(););
@ -756,8 +761,8 @@ public:
pb_util u(m);
expr_ref_vector nsoft(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
nsoft.push_back(mk_not(m, m_soft[i]));
for (expr* s : m_soft) {
nsoft.push_back(mk_not(m, s));
}
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
TRACE("opt", tout << "block upper bound " << fml << "\n";);;

56
src/opt/maxsmt.cpp
View file

@ -21,6 +21,7 @@ Notes:
#include "opt/maxsmt.h"
#include "opt/maxres.h"
#include "opt/wmax.h"
#include "opt/opt_params.hpp"
#include "ast/ast_pp.h"
#include "util/uint_set.h"
#include "opt/opt_context.h"
@ -409,6 +410,59 @@ namespace opt {
m_c.model_updated(mdl);
}
class solver_maxsat_context : public maxsat_context {
params_ref m_params;
solver_ref m_solver;
model_ref m_model;
ref<generic_model_converter> m_fm;
symbol m_maxsat_engine;
public:
solver_maxsat_context(params_ref& p, solver* s, model * m):
m_params(p),
m_solver(s),
m_model(m),
m_fm(alloc(generic_model_converter, s->get_manager(), "maxsmt")) {
opt_params _p(p);
m_maxsat_engine = _p.maxsat_engine();
}
generic_model_converter& fm() override { return *m_fm.get(); }
bool sat_enabled() const override { return false; }
solver& get_solver() override { return *m_solver.get(); }
ast_manager& get_manager() const override { return m_solver->get_manager(); }
params_ref& params() override { return m_params; }
void enable_sls(bool force) override { } // no op
symbol const& maxsat_engine() const override { return m_maxsat_engine; }
void get_base_model(model_ref& _m) override { _m = m_model; };
smt::context& smt_context() override {
throw default_exception("stand-alone maxsat context does not support wmax");
}
unsigned num_objectives() override { return 1; }
bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; };
void set_model(model_ref& _m) override { m_model = _m; }
void model_updated(model* mdl) override { } // no-op
};
lbool maxsmt_wrapper::operator()(vector<std::pair<expr*,rational>>& soft) {
solver_maxsat_context ctx(m_params, m_solver.get(), m_model.get());
maxsmt maxsmt(ctx, 0);
for (auto const& p : soft) {
maxsmt.add(p.first, p.second);
}
lbool r = maxsmt();
if (r == l_true) {
ast_manager& m = m_solver->get_manager();
svector<symbol> labels;
maxsmt.get_model(m_model, labels);
// TBD: is m_fm applied or not?
unsigned j = 0;
expr_ref tmp(m);
for (unsigned i = 0; i < soft.size(); ++i) {
if (m_model->eval(soft[i].first, tmp) && m.is_true(tmp)) {
soft[j++] = soft[i];
}
}
soft.shrink(j);
}
return r;
}
};

42
src/opt/maxsmt.h
View file

@ -153,6 +153,48 @@ namespace opt {
solver& s();
};
/**
\brief Standalone MaxSMT solver.
It takes as input a solver object and provides a MaxSAT solver routine.
It assumes the solver state is satisfiable and therefore there is a model
associated with the constraints asserted to the solver. A model of the
solver state must be supplied as a last argument.
It assumes that the caller manages scope on the solver such that
the solver can be left in a stronger or inconsistent state upon return.
Callers should therefore use this feature under a push/pop.
*/
class maxsmt_wrapper {
params_ref m_params;
ref<solver> m_solver;
model_ref m_model;
public:
maxsmt_wrapper(params_ref & p, solver* s, model* m):
m_params(p),
m_solver(s),
m_model(m) {}
lbool operator()(expr_ref_vector& soft) {
vector<std::pair<expr*, rational>> _soft;
for (expr* e : soft) _soft.push_back(std::make_pair(e, rational::one()));
lbool r = (*this)(_soft);
soft.reset();
for (auto const& p : _soft) soft.push_back(p.first);
return r;
}
/**
\brief takes a vector of weighted soft constraints.
Returns a modified list of soft constraints that are
satisfied in the maximal satisfying assignment.
*/
lbool operator()(vector<std::pair<expr*,rational>> & soft);
model_ref get_model() { return m_model; }
};
};
#endif

2
src/opt/opt_context.cpp
View file

@ -172,7 +172,7 @@ namespace opt {
r.append(m_labels);
}
void context::get_unsat_core(ptr_vector<expr> & r) {
void context::get_unsat_core(expr_ref_vector & r) {
throw default_exception("Unsat cores are not supported with optimization");
}

2
src/opt/opt_context.h
View file

@ -195,7 +195,7 @@ namespace opt {
void collect_statistics(statistics& stats) const override;
proof* get_proof() override { return nullptr; }
void get_labels(svector<symbol> & r) override;
void get_unsat_core(ptr_vector<expr> & r) override;
void get_unsat_core(expr_ref_vector & r) override;
std::string reason_unknown() const override;
void set_reason_unknown(char const* msg) override { m_unknown = msg; }

3
src/opt/opt_solver.cpp
View file

@ -294,7 +294,8 @@ namespace opt {
return r;
}
void opt_solver::get_unsat_core(ptr_vector<expr> & r) {
void opt_solver::get_unsat_core(expr_ref_vector & r) {
r.reset();
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++) {
r.push_back(m_context.get_unsat_core_expr(i));

2
src/opt/opt_solver.h
View file

@ -96,7 +96,7 @@ namespace opt {
void push_core() override;
void pop_core(unsigned n) override;
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
void get_unsat_core(ptr_vector<expr> & r) override;
void get_unsat_core(expr_ref_vector & r) override;
void get_model_core(model_ref & _m) override;
proof * get_proof() override;
std::string reason_unknown() const override;