mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

A few changes based on previous reviews

Browse source 
Tested the optimization procedure with:
- unbounded objectives
- bounded with rational solutions
- bounded with irrational solutions
This commit is contained in:
Anh-Dung Phan 2013-10-21 17:25:34 -07:00
parent 3dd72f8f16
commit 3441fc2942
8 changed files with 24 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_context.cpp
View file

@ -68,7 +68,7 @@ namespace opt {
}
if (!m_objectives.empty()) {
vector<inf_eps_rational<rational> > values;
vector<inf_eps_rational<inf_rational> > values;
for (unsigned i = 0; i < fmls_copy.size(); ++i) {
s->assert_expr(fmls_copy[i].get());
}
@ -76,6 +76,7 @@ namespace opt {
// if (!instsanceof ...) { throw ... invalid usage ..}
is_sat = optimize_objectives(dynamic_cast<opt_solver&>(*s), m_objectives, m_is_max, values);
std::cout << "is-sat: " << is_sat << "\n";
if (is_sat != l_true) {
return;
}

4
src/opt/opt_solver.cpp
View file

@ -70,7 +70,7 @@ namespace opt {
if (is_bounded) {
m_objective_value = get_optimizer().get_objective_value(m_objective_var);
} else {
inf_eps_rational<rational> r(rational(1), rational(0));
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
m_objective_value = r;
}
}
@ -131,7 +131,7 @@ namespace opt {
m_objective_enabled = enable;
}
inf_eps_rational<rational> opt_solver::get_objective_value() {
inf_eps_rational<inf_rational> opt_solver::get_objective_value() {
return m_objective_value;
}

5
src/opt/opt_solver.h
View file

@ -20,6 +20,7 @@ Notes:
#ifndef _OPT_SOLVER_H_
#define _OPT_SOLVER_H_
#include"inf_rational.h"
#include"inf_eps_rational.h"
#include"ast.h"
#include"params.h"
@ -38,7 +39,7 @@ namespace opt {
symbol m_logic;
bool m_objective_enabled;
smt::theory_var m_objective_var;
inf_eps_rational<rational> m_objective_value;
inf_eps_rational<inf_rational> m_objective_value;
public:
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
virtual ~opt_solver();
@ -64,7 +65,7 @@ namespace opt {
void set_objective(app* term);
void toggle_objective(bool enable);
inf_eps_rational<rational> get_objective_value();
inf_eps_rational<inf_rational> get_objective_value();
private:
smt::theory_opt& get_optimizer();
};

24
src/opt/optimize_objectives.cpp
View file

@ -33,23 +33,20 @@ namespace opt {
opt_solver& s,
app_ref_vector& objectives,
svector<bool> const& is_max,
vector<inf_eps_rational<rational> >& values)
vector<inf_eps_rational<inf_rational> >& values)
{
SASSERT(is_max.size() == objectives.size());
enable_trace("maximize"); // NSB review: OK for now for debugging. Otherwise, use command-line /tr:maximize
// First check_sat call for initialize theories
lbool is_sat = s.check_sat(0, 0);
if (is_sat != l_false) {
if (is_sat == l_false) {
return is_sat;
}
s.push();
// Assume there is only one objective function
SASSERT(is_max.size() == 1);
// Temporarily ignore the assertion to run the first objective function
//SASSERT(is_max.size() == 1);
ast_manager& m = objectives.get_manager();
arith_util autil(m);
bool ismax = is_max[0];
@ -62,20 +59,19 @@ namespace opt {
s.set_objective(objective_var); // NSB review: I would change signature of set_objective to take is_max and decide whether to add equation.
// Otherwise, the difference logic backends will not work.
s.toggle_objective(true);
is_sat = s.check_sat(0, 0);
is_sat = s.check_sat(0, 0);
while (is_sat == l_true) {
// Extract values for objectives
inf_eps_rational<rational> val;
val = is_max[0] ? s.get_objective_value() : -s.get_objective_value();
inf_eps_rational<inf_rational> val;
val = ismax ? s.get_objective_value() : -s.get_objective_value();
// Check whether objective is unbounded
// NSB: review: what if optimal is 1-epsilon. Then the check also fails.
values.reset();
values.push_back(val);
if (!val.is_rational()) {
if (!val.get_infinity().is_zero()) {
break;
}
@ -90,7 +86,7 @@ namespace opt {
if (is_sat == l_undef) {
return is_sat;
}
SASSERT(is_sat == l_false); // NSB review: not really water-tight with cancellation and with infinitesimal solutions.
//SASSERT(is_sat == l_false); // NSB review: not really water-tight with cancellation and with infinitesimal solutions.
return l_true;
}
@ -101,7 +97,7 @@ namespace opt {
lbool optimize_objectives(opt_solver& s,
app_ref_vector& objectives, svector<bool> const& is_max,
vector<inf_eps_rational<rational> >& values) {
vector<inf_eps_rational<inf_rational> >& values) {
return mathsat_style_opt(s, objectives, is_max, values);
}
}

2
src/opt/optimize_objectives.h
View file

@ -29,7 +29,7 @@ namespace opt {
lbool optimize_objectives(opt_solver& s,
app_ref_vector& objectives, svector<bool> const& is_max,
vector<inf_eps_rational<rational> >& values);
vector<inf_eps_rational<inf_rational> >& values);
};
#endif

2
src/smt/theory_arith.h
View file

@ -994,7 +994,7 @@ namespace smt {
// -----------------------------------
virtual bool maximize(theory_var v) { return max_min(v, true); }
virtual theory_var add_objective(app* term);
virtual inf_eps_rational<rational> get_objective_value(theory_var v);
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
inf_rational m_objective;
// -----------------------------------

5
src/smt/theory_arith_aux.h
View file

@ -961,9 +961,8 @@ namespace smt {
}
template<typename Ext>
inf_eps_rational<rational> theory_arith<Ext>::get_objective_value(theory_var v) {
inf_eps_rational<rational> val;
val = m_objective.get_rational();
inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
inf_eps_rational<inf_rational> val(m_objective);
return val;
}

5
src/smt/theory_opt.h
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include "inf_rational.h"
#include "inf_eps_rational.h"
#ifndef _THEORY_OPT_H_
@ -28,9 +29,9 @@ namespace smt {
public:
virtual bool maximize(theory_var v) { UNREACHABLE(); return false; };
virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
virtual inf_eps_rational<rational> get_objective_value(theory_var v) {
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v) {
UNREACHABLE();
inf_eps_rational<rational> r(rational(1), rational(0));
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
return r;
}
};