mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update lower bounds from feasible solutiosn
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e307c5fdda
commit
370a4b66de
|
@ -147,5 +147,9 @@ namespace opt {
|
|||
void core_maxsat::set_cancel(bool f) {
|
||||
|
||||
}
|
||||
void core_maxsat::collect_statistics(statistics& st) const {
|
||||
// nothing specific
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
|
|
@ -40,6 +40,7 @@ namespace opt {
|
|||
virtual rational get_value() const;
|
||||
virtual expr_ref_vector get_assignment() const;
|
||||
virtual void set_cancel(bool f);
|
||||
virtual void collect_statistics(statistics& st) const;
|
||||
|
||||
private:
|
||||
void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
|
||||
|
|
|
@ -93,6 +93,12 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
void collect_statistics(statistics& st) const {
|
||||
if (m_s != &m_original_solver) {
|
||||
m_s->collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
|
||||
set.reset();
|
||||
expr_set::iterator it = set1.begin(), end = set1.end();
|
||||
|
@ -307,11 +313,6 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
}
|
||||
statistics st;
|
||||
s().collect_statistics(st);
|
||||
SASSERT(st.size() > 0);
|
||||
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
|
||||
opt_s.set_interim_stats(st);
|
||||
// We are done and soft_constraints has
|
||||
// been updated with the max-sat assignment.
|
||||
return is_sat;
|
||||
|
@ -344,6 +345,9 @@ namespace opt {
|
|||
void fu_malik::set_cancel(bool f) {
|
||||
// no-op
|
||||
}
|
||||
void fu_malik::collect_statistics(statistics& st) const {
|
||||
m_imp->collect_statistics(st);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -41,6 +41,7 @@ namespace opt {
|
|||
virtual rational get_value() const;
|
||||
virtual expr_ref_vector get_assignment() const;
|
||||
virtual void set_cancel(bool f);
|
||||
virtual void collect_statistics(statistics& st) const;
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -79,21 +79,29 @@ namespace opt {
|
|||
if (m_msolver) {
|
||||
return inf_eps(m_msolver->get_value());
|
||||
}
|
||||
return inf_eps();
|
||||
return inf_eps(m_upper);
|
||||
}
|
||||
|
||||
inf_eps maxsmt::get_lower() const {
|
||||
rational r = m_lower;
|
||||
if (m_msolver) {
|
||||
return inf_eps(m_msolver->get_lower());
|
||||
rational q = m_msolver->get_lower();
|
||||
if (r < q) r = q;
|
||||
}
|
||||
return inf_eps();
|
||||
return inf_eps(r);
|
||||
}
|
||||
|
||||
inf_eps maxsmt::get_upper() const {
|
||||
rational r = m_upper;
|
||||
if (m_msolver) {
|
||||
return inf_eps(m_msolver->get_upper());
|
||||
rational q = m_msolver->get_upper();
|
||||
if (r > q) r = q;
|
||||
}
|
||||
return inf_eps(rational(m_soft_constraints.size()));
|
||||
return inf_eps(r);
|
||||
}
|
||||
|
||||
void maxsmt::update_lower(rational const& r) {
|
||||
if (m_lower > r) m_lower = r;
|
||||
}
|
||||
|
||||
void maxsmt::commit_assignment() {
|
||||
|
@ -130,5 +138,11 @@ namespace opt {
|
|||
m_maxsat_engine = _p.maxsat_engine();
|
||||
}
|
||||
|
||||
void maxsmt::collect_statistics(statistics& st) const {
|
||||
if (m_msolver) {
|
||||
m_msolver->collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
|
|
@ -21,6 +21,7 @@ Notes:
|
|||
|
||||
#include "solver.h"
|
||||
#include "opt_solver.h"
|
||||
#include "statistics.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
|
@ -33,6 +34,7 @@ namespace opt {
|
|||
virtual rational get_value() const = 0;
|
||||
virtual expr_ref_vector get_assignment() const = 0;
|
||||
virtual void set_cancel(bool f) = 0;
|
||||
virtual void collect_statistics(statistics& st) const = 0;
|
||||
};
|
||||
/**
|
||||
Takes solver with hard constraints added.
|
||||
|
@ -46,6 +48,8 @@ namespace opt {
|
|||
expr_ref_vector m_soft_constraints;
|
||||
expr_ref_vector m_answer;
|
||||
vector<rational> m_weights;
|
||||
rational m_lower;
|
||||
rational m_upper;
|
||||
scoped_ptr<maxsmt_solver> m_msolver;
|
||||
symbol m_maxsat_engine;
|
||||
public:
|
||||
|
@ -58,8 +62,11 @@ namespace opt {
|
|||
void updt_params(params_ref& p);
|
||||
|
||||
void add(expr* f, rational const& w) {
|
||||
SASSERT(m.is_bool(f));
|
||||
SASSERT(w.is_pos());
|
||||
m_soft_constraints.push_back(f);
|
||||
m_weights.push_back(w);
|
||||
m_upper += w;
|
||||
}
|
||||
|
||||
unsigned size() const { return m_soft_constraints.size(); }
|
||||
|
@ -70,10 +77,15 @@ namespace opt {
|
|||
inf_eps get_value() const;
|
||||
inf_eps get_lower() const;
|
||||
inf_eps get_upper() const;
|
||||
void update_lower(rational const& r);
|
||||
|
||||
|
||||
expr_ref_vector get_assignment() const;
|
||||
|
||||
void display_answer(std::ostream& out) const;
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
|
||||
private:
|
||||
|
||||
|
|
|
@ -85,6 +85,7 @@ namespace opt {
|
|||
return is_sat;
|
||||
}
|
||||
s.get_model(m_model);
|
||||
update_lower();
|
||||
switch (m_objectives.size()) {
|
||||
case 0:
|
||||
return is_sat;
|
||||
|
@ -223,11 +224,15 @@ namespace opt {
|
|||
rational coeff(0);
|
||||
// minimize 2*x + 3*y
|
||||
// <=>
|
||||
// (assret-soft (not x) 2)
|
||||
// (assert-soft (not x) 2)
|
||||
// (assert-soft (not y) 3)
|
||||
//
|
||||
if (get_pb_sum(term, terms, weights, coeff) && coeff.is_zero()) {
|
||||
// TBD: and weights are positive?
|
||||
for (unsigned i = 0; i < weights.size(); ++i) {
|
||||
if (!weights[i].is_pos()) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < terms.size(); ++i) {
|
||||
terms[i] = m.mk_not(terms[i].get());
|
||||
}
|
||||
|
@ -348,6 +353,40 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::update_lower() {
|
||||
arith_util a(m);
|
||||
expr_ref val(m);
|
||||
rational r(0);
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
switch(obj.m_type) {
|
||||
case O_MINIMIZE:
|
||||
case O_MAXIMIZE:
|
||||
if (m_model->eval(obj.m_term, val) && a.is_numeral(val, r)) {
|
||||
m_optsmt.update_lower(obj.m_index, r);
|
||||
}
|
||||
break;
|
||||
case O_MAXSMT: {
|
||||
bool ok = true;
|
||||
for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) {
|
||||
if (m_model->eval(obj.m_terms[j], val)) {
|
||||
if (!m.is_true(val)) {
|
||||
r += obj.m_weights[j];
|
||||
}
|
||||
}
|
||||
else {
|
||||
ok = false;
|
||||
}
|
||||
}
|
||||
if (ok) {
|
||||
m_maxsmts.find(obj.m_id)->update_lower(r);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void context::display_assignment(std::ostream& out) {
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
|
@ -459,6 +498,10 @@ namespace opt {
|
|||
if (m_solver) {
|
||||
m_solver->collect_statistics(stats);
|
||||
}
|
||||
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
|
||||
for (; it != end; ++it) {
|
||||
it->m_value->collect_statistics(stats);
|
||||
}
|
||||
}
|
||||
|
||||
void context::collect_param_descrs(param_descrs & r) {
|
||||
|
|
|
@ -128,6 +128,8 @@ namespace opt {
|
|||
void from_fmls(expr_ref_vector const& fmls);
|
||||
void simplify_fmls(expr_ref_vector& fmls);
|
||||
|
||||
void update_lower();
|
||||
|
||||
opt_solver& get_solver();
|
||||
|
||||
};
|
||||
|
|
|
@ -55,14 +55,8 @@ namespace opt {
|
|||
m_context.collect_param_descrs(r);
|
||||
}
|
||||
|
||||
void opt_solver::collect_statistics(statistics & st) const {
|
||||
// HACK: display fu_malik statistics
|
||||
if (m_stats.size() > 0) {
|
||||
st.copy(m_stats);
|
||||
}
|
||||
else {
|
||||
m_context.collect_statistics(st);
|
||||
}
|
||||
void opt_solver::collect_statistics(statistics & st) const {
|
||||
m_context.collect_statistics(st);
|
||||
}
|
||||
|
||||
void opt_solver::assert_expr(expr * t) {
|
||||
|
@ -241,9 +235,6 @@ namespace opt {
|
|||
return dynamic_cast<opt_solver&>(s);
|
||||
}
|
||||
|
||||
void opt_solver::set_interim_stats(statistics & st) {
|
||||
m_stats.copy(st);
|
||||
}
|
||||
|
||||
void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic,
|
||||
char const * status, char const * attributes) {
|
||||
|
|
|
@ -79,7 +79,6 @@ namespace opt {
|
|||
expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
|
||||
|
||||
static opt_solver& to_opt(solver& s);
|
||||
void set_interim_stats(statistics & st);
|
||||
bool dump_benchmarks();
|
||||
|
||||
class toggle_objective {
|
||||
|
|
|
@ -105,6 +105,13 @@ namespace opt {
|
|||
return l_true;
|
||||
}
|
||||
|
||||
void optsmt::update_lower(unsigned idx, rational const& r) {
|
||||
inf_eps v(r);
|
||||
if (m_lower[idx] < v) {
|
||||
m_lower[idx] = v;
|
||||
}
|
||||
}
|
||||
|
||||
void optsmt::update_lower() {
|
||||
model_ref md;
|
||||
s->get_model(md);
|
||||
|
@ -202,30 +209,26 @@ namespace opt {
|
|||
Returns an optimal assignment to objective functions.
|
||||
*/
|
||||
lbool optsmt::operator()(opt_solver& solver) {
|
||||
if (m_objs.empty()) {
|
||||
return l_true;
|
||||
}
|
||||
lbool is_sat = l_true;
|
||||
s = &solver;
|
||||
s->reset_objectives();
|
||||
solver.reset_objectives();
|
||||
m_vars.reset();
|
||||
|
||||
// First check_sat call to initialize theories
|
||||
lbool is_sat = s->check_sat(0, 0);
|
||||
solver::scoped_push _push(*s);
|
||||
if (is_sat == l_true && !m_objs.empty()) {
|
||||
for (unsigned i = 0; i < m_objs.size(); ++i) {
|
||||
m_vars.push_back(s->add_objective(m_objs[i].get()));
|
||||
}
|
||||
solver::scoped_push _push(solver);
|
||||
|
||||
if (m_engine == symbol("basic")) {
|
||||
is_sat = basic_opt();
|
||||
}
|
||||
else if (m_engine == symbol("farkas")) {
|
||||
is_sat = farkas_opt();
|
||||
}
|
||||
else {
|
||||
// TODO: implement symba engine
|
||||
// report error on bad configuration.
|
||||
NOT_IMPLEMENTED_YET();
|
||||
UNREACHABLE();
|
||||
}
|
||||
for (unsigned i = 0; i < m_objs.size(); ++i) {
|
||||
m_vars.push_back(solver.add_objective(m_objs[i].get()));
|
||||
}
|
||||
|
||||
if (m_engine == symbol("farkas")) {
|
||||
is_sat = farkas_opt();
|
||||
}
|
||||
else {
|
||||
is_sat = basic_opt();
|
||||
}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl;
|
||||
|
|
|
@ -56,6 +56,8 @@ namespace opt {
|
|||
inf_eps get_value(unsigned index) const;
|
||||
inf_eps get_lower(unsigned index) const;
|
||||
inf_eps get_upper(unsigned index) const;
|
||||
|
||||
void update_lower(unsigned idx, rational const& r);
|
||||
|
||||
private:
|
||||
|
||||
|
|
|
@ -370,7 +370,9 @@ namespace opt {
|
|||
void wmaxsmt::set_cancel(bool f) {
|
||||
// no-op
|
||||
}
|
||||
|
||||
void wmaxsmt::collect_statistics(statistics& st) const {
|
||||
// no-op
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -39,6 +39,7 @@ namespace opt {
|
|||
virtual rational get_value() const;
|
||||
virtual expr_ref_vector get_assignment() const;
|
||||
virtual void set_cancel(bool f);
|
||||
virtual void collect_statistics(statistics& st) const;
|
||||
};
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue