mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
pareto take 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8883234647
commit
a307bd67e0
|
@ -205,12 +205,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < bounds.size(); ++i) {
|
||||
for (unsigned j = 0; j < bounds.size(); ++j) {
|
||||
objective const& obj = m_objectives[j];
|
||||
if (obj.m_type == O_MAXIMIZE) {
|
||||
bounds[i][j].second = bounds[j][j].second;
|
||||
}
|
||||
else {
|
||||
bounds[i][j].first = bounds[j][j].first;
|
||||
}
|
||||
bounds[i][j].second = bounds[j][j].second;
|
||||
}
|
||||
display_bounds(verbose_stream() << "new bound\n", bounds[i]);
|
||||
}
|
||||
|
@ -253,7 +248,7 @@ namespace opt {
|
|||
if (j > 0) {
|
||||
b2[j-1].second = b[j-1].second;
|
||||
}
|
||||
display_bounds(verbose_stream() << "new bound\n", b2);
|
||||
display_bounds(verbose_stream() << "refined bound\n", b2);
|
||||
bounds.push_back(b2);
|
||||
}
|
||||
break;
|
||||
|
@ -268,7 +263,12 @@ namespace opt {
|
|||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
display_objective(out, obj);
|
||||
out << " |-> [" << b[i].first << ":" << b[i].second << "]\n";
|
||||
if (obj.m_type == O_MAXIMIZE) {
|
||||
out << " |-> [" << b[i].first << ":" << b[i].second << "]\n";
|
||||
}
|
||||
else {
|
||||
out << " |-> [" << -b[i].second << ":" << -b[i].first << "]\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -506,11 +506,15 @@ namespace opt {
|
|||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective & obj = m_objectives[i];
|
||||
switch(obj.m_type) {
|
||||
case O_MINIMIZE:
|
||||
obj.m_index = m_optsmt.add(obj.m_term, false);
|
||||
case O_MINIMIZE: {
|
||||
app_ref tmp(m);
|
||||
arith_util a(m);
|
||||
tmp = a.mk_uminus(obj.m_term);
|
||||
obj.m_index = m_optsmt.add(tmp);
|
||||
break;
|
||||
}
|
||||
case O_MAXIMIZE:
|
||||
obj.m_index = m_optsmt.add(obj.m_term, true);
|
||||
obj.m_index = m_optsmt.add(obj.m_term);
|
||||
break;
|
||||
case O_MAXSMT: {
|
||||
maxsmt& ms = *m_maxsmts.find(obj.m_id);
|
||||
|
@ -604,6 +608,7 @@ namespace opt {
|
|||
return inf_eps(r);
|
||||
}
|
||||
case O_MINIMIZE:
|
||||
return -m_optsmt.get_upper(obj.m_index);
|
||||
case O_MAXIMIZE:
|
||||
return m_optsmt.get_lower(obj.m_index);
|
||||
default:
|
||||
|
@ -626,6 +631,7 @@ namespace opt {
|
|||
return inf_eps(r);
|
||||
}
|
||||
case O_MINIMIZE:
|
||||
return -m_optsmt.get_lower(obj.m_index);
|
||||
case O_MAXIMIZE:
|
||||
return m_optsmt.get_upper(obj.m_index);
|
||||
default:
|
||||
|
|
|
@ -340,19 +340,16 @@ namespace opt {
|
|||
is_sat = basic_opt();
|
||||
}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl;
|
||||
display_assignment(verbose_stream()););
|
||||
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
||||
inf_eps optsmt::get_lower(unsigned i) const {
|
||||
return m_is_max[i]?m_lower[i]:-m_upper[i];
|
||||
return m_lower[i];
|
||||
}
|
||||
|
||||
inf_eps optsmt::get_upper(unsigned i) const {
|
||||
return m_is_max[i]?m_upper[i]:-m_lower[i];
|
||||
return m_upper[i];
|
||||
}
|
||||
|
||||
void optsmt::get_model(model_ref& mdl) {
|
||||
|
@ -362,7 +359,7 @@ namespace opt {
|
|||
// force lower_bound(i) <= objective_value(i)
|
||||
void optsmt::commit_assignment(unsigned i) {
|
||||
inf_eps lo = m_lower[i];
|
||||
TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << lo << "\n";
|
||||
TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs[i].get(), m) << " to: " << lo << "\n";
|
||||
tout << get_lower(i) << ":" << get_upper(i) << "\n";);
|
||||
// Only assert bounds for bounded objectives
|
||||
if (lo.is_finite()) {
|
||||
|
@ -370,42 +367,12 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {
|
||||
bool is_max = m_is_max[i];
|
||||
expr_ref obj(m_objs[i], m);
|
||||
if (!is_max) {
|
||||
arith_util a(m);
|
||||
th_rewriter rw(m);
|
||||
obj = a.mk_uminus(obj);
|
||||
rw(obj, obj);
|
||||
}
|
||||
return out << obj;
|
||||
}
|
||||
|
||||
void optsmt::display_assignment(std::ostream& out) const {
|
||||
unsigned sz = m_objs.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (get_lower(i) != get_upper(i)) {
|
||||
display_objective(out, i) << " |-> [" << get_lower(i)
|
||||
<< ":" << get_upper(i) << "]" << std::endl;
|
||||
}
|
||||
else {
|
||||
display_objective(out, i) << " |-> " << get_lower(i) << std::endl;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
unsigned optsmt::add(app* t, bool is_max) {
|
||||
unsigned optsmt::add(app* t) {
|
||||
expr_ref t1(t, m), t2(m);
|
||||
th_rewriter rw(m);
|
||||
if (!is_max) {
|
||||
arith_util a(m);
|
||||
t1 = a.mk_uminus(t);
|
||||
}
|
||||
rw(t1, t2);
|
||||
SASSERT(is_app(t2));
|
||||
m_objs.push_back(to_app(t2));
|
||||
m_is_max.push_back(is_max);
|
||||
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
|
||||
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
|
||||
return m_objs.size()-1;
|
||||
|
|
|
@ -34,7 +34,6 @@ namespace opt {
|
|||
vector<inf_eps> m_lower;
|
||||
vector<inf_eps> m_upper;
|
||||
app_ref_vector m_objs;
|
||||
svector<bool> m_is_max;
|
||||
svector<smt::theory_var> m_vars;
|
||||
symbol m_engine;
|
||||
model_ref m_model;
|
||||
|
@ -49,15 +48,12 @@ namespace opt {
|
|||
|
||||
lbool pareto(unsigned obj_index);
|
||||
|
||||
unsigned add(app* t, bool is_max);
|
||||
unsigned add(app* t);
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
void updt_params(params_ref& p);
|
||||
|
||||
void display_assignment(std::ostream& out) const;
|
||||
void display_range_assignment(std::ostream& out) const;
|
||||
|
||||
unsigned get_num_objectives() const { return m_objs.size(); }
|
||||
void commit_assignment(unsigned index);
|
||||
inf_eps get_lower(unsigned index) const;
|
||||
|
@ -68,8 +64,6 @@ namespace opt {
|
|||
|
||||
private:
|
||||
|
||||
std::ostream& display_objective(std::ostream& out, unsigned i) const;
|
||||
|
||||
lbool basic_opt();
|
||||
|
||||
lbool basic_lex(unsigned idx);
|
||||
|
|
|
@ -152,8 +152,12 @@ public:
|
|||
SASSERT(g->is_well_sorted());
|
||||
pc = 0; core = 0;
|
||||
|
||||
// TBD: bail out if cores are enabled.
|
||||
// TBD: bail out if proofs are enabled/add proofs.
|
||||
if (g->unsat_core_enabled()) {
|
||||
throw tactic_exception("pb-preprocess does not support cores");
|
||||
}
|
||||
if (g->proofs_enabled()) {
|
||||
throw tactic_exception("pb-preprocess does not support proofs");
|
||||
}
|
||||
|
||||
pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
|
||||
mc = pp;
|
||||
|
@ -166,6 +170,7 @@ public:
|
|||
bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
|
||||
reset();
|
||||
normalize(g);
|
||||
decompose(g);
|
||||
if (g->inconsistent()) {
|
||||
return false;
|
||||
}
|
||||
|
@ -300,6 +305,14 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
void decompose(goal_ref const& g) {
|
||||
for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) {
|
||||
expr* e = g->form(i);
|
||||
if (pb.is_ge(e) && to_app(e)->get_num_args() > 20) {
|
||||
// TBD: decompose inequality int smaller ones.
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void process_vars(unsigned i, goal_ref const& g) {
|
||||
expr* r, *e;
|
||||
|
|
Loading…
Reference in a new issue