mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Replace the use of optional<rational> by inf_eps_rational<rational>

Browse source 
Also handle composite objectives correctly.
This commit is contained in:
Phan Anh Dung 2013-10-19 06:03:21 +02:00
parent a44044fb15
commit 53f78f7d19
9 changed files with 50 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/opt_context.cpp
View file

@ -16,7 +16,6 @@ Notes:
--*/
#include "opt_context.h"
#include "fu_malik.h"
#include "weighted_maxsat.h"
@ -62,7 +61,7 @@ namespace opt {
}
if (!m_objectives.empty()) {
vector<optional<rational> > values;
vector<inf_eps_rational<rational> > values;
for (unsigned i = 0; i < fmls_copy.size(); ++i) {
s->assert_expr(fmls_copy[i].get());
}
@ -75,11 +74,7 @@ namespace opt {
}
for (unsigned i = 0; i < values.size(); ++i) {
if (values[i]) {
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << *values[i] << "\n";
} else {
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> unbounded\n";
}
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << values[i].to_string() << "\n";
}
}

1
src/opt/opt_context.h
View file

@ -66,7 +66,6 @@ namespace opt {
};
}
#endif

11
src/opt/opt_solver.cpp
View file

@ -7,7 +7,6 @@ namespace opt {
opt_solver::opt_solver(ast_manager & m, params_ref const & p, symbol const & l):
solver_na2as(m),
m_manager(m),
m_params(p),
m_context(m, m_params),
m_objective_enabled(false) {
@ -15,7 +14,7 @@ namespace opt {
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
}
opt_solver::~opt_solver() {
}
@ -64,14 +63,14 @@ namespace opt {
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt_solver_na2as", tout << "smt_opt_solver::check_sat_core: " << num_assumptions << "\n";);
TRACE("opt_solver_na2as", tout << "opt_opt_solver::check_sat_core: " << num_assumptions << "\n";);
lbool r = m_context.check(num_assumptions, assumptions);
if (r == l_true && m_objective_enabled) {
bool is_bounded = get_optimizer().max(m_objective_var);
bool is_bounded = get_optimizer().maximize(m_objective_var);
if (is_bounded) {
m_objective_value = get_optimizer().get_objective_value(m_objective_var);
} else {
optional<rational> r;
inf_eps_rational<rational> r(rational(1), rational(0));
m_objective_value = r;
}
}
@ -132,7 +131,7 @@ namespace opt {
m_objective_enabled = enable;
}
optional<rational> opt_solver::get_objective_value() {
inf_eps_rational<rational> opt_solver::get_objective_value() {
return m_objective_value;
}

6
src/opt/opt_solver.h
View file

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

39
src/opt/optimize_objectives.cpp
View file

@ -31,7 +31,7 @@ namespace opt {
*/
lbool mathsat_style_opt(opt_solver& s,
expr_ref_vector& objectives, svector<bool> const& is_max,
vector<optional<rational> >& values) {
vector<inf_eps_rational<rational> >& values) {
enable_trace("maximize");
// First check_sat call for initialize theories
lbool is_sat = s.check_sat(0, 0);
@ -39,38 +39,47 @@ namespace opt {
return l_false;
}
s.push();
// Assume there is only one objective function
ast_manager& m = objectives.get_manager();
arith_util autil(m);
app* objective = is_max[0] ? (app*) objectives[0].get() : autil.mk_uminus(objectives[0].get());
app* objective = m.mk_fresh_const("objective", autil.mk_real());
if (is_max[0]) {
s.assert_expr(autil.mk_eq(objective, objectives[0].get()));
} else {
s.assert_expr(autil.mk_eq(objective, autil.mk_uminus(objectives[0].get())));
};
s.set_objective(objective);
s.toggle_objective(true);
is_sat = s.check_sat(0, 0);
while (is_sat != l_false) {
// Extract values for objectives.
optional<rational> rat;
rat = s.get_objective_value();
// Extract values for objectives
inf_eps_rational<rational> val;
val = is_max[0] ? s.get_objective_value() : -s.get_objective_value();
// Unbounded objective
if (!rat) {
// Check whether objective is unbounded
if (!val.is_rational()) {
values.reset();
values.push_back(rat);
return l_true;
values.push_back(val);
break;
}
// If values have initial data, they will be dropped.
// If values have initial data, they will be dropped
values.reset();
values.push_back(rat);
values.push_back(val);
// Assert there must be something better.
// Assert there must be something better
expr_ref_vector assumptions(m);
expr* bound = m.mk_fresh_const("bound", m.mk_bool_sort());
assumptions.push_back(bound);
expr* r = autil.mk_numeral(*rat, false);
expr* r = autil.mk_numeral(val.get_rational(), false);
s.assert_expr(m.mk_eq(bound, is_max[0] ? autil.mk_gt(objectives[0].get(), r) : autil.mk_lt(objectives[0].get(), r)));
is_sat = s.check_sat(1, assumptions.c_ptr());
}
}
s.pop(1);
return l_true;
}
@ -82,7 +91,7 @@ namespace opt {
lbool optimize_objectives(opt_solver& s,
expr_ref_vector& objectives, svector<bool> const& is_max,
vector<optional<rational> >& values) {
vector<inf_eps_rational<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,
expr_ref_vector& objectives, svector<bool> const& is_max,
vector<optional<rational> >& values);
vector<inf_eps_rational<rational> >& values);
};
#endif

4
src/smt/theory_arith.h
View file

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

11
src/smt/theory_arith_aux.h
View file

@ -19,6 +19,7 @@ Revision History:
#ifndef _THEORY_ARITH_AUX_H_
#define _THEORY_ARITH_AUX_H_
#include"inf_eps_rational.h"
#include"theory_arith.h"
namespace smt {
@ -960,12 +961,10 @@ namespace smt {
}
template<typename Ext>
optional<rational> theory_arith<Ext>::get_objective_value(theory_var v) {
optional<rational> rat;
if (m_objective.is_rational()) {
rat = m_objective.get_rational();
};
return rat;
inf_eps_rational<rational> theory_arith<Ext>::get_objective_value(theory_var v) {
inf_eps_rational<rational> val;
val = m_objective.get_rational();
return val;
}
/**

10
src/smt/theory_opt.h
View file

@ -18,15 +18,21 @@ Notes:
--*/
#include "inf_eps_rational.h"
#ifndef _THEORY_OPT_H_
#define _THEORY_OPT_H_
namespace smt {
class theory_opt {
public:
virtual bool max(theory_var v) { UNREACHABLE(); return false; };
virtual bool maximize(theory_var v) { UNREACHABLE(); return false; };
virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
virtual optional<rational> get_objective_value(theory_var v) { UNREACHABLE(); optional<rational> r; return r;}
virtual inf_eps_rational<rational> get_objective_value(theory_var v) {
UNREACHABLE();
inf_eps_rational<rational> r(rational(1), rational(0));
return r;
}
};
}