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

preparing for inf extension of arithmetic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-31 02:02:37 -07:00
parent acc7aa1636
commit 0b65aa83e8
6 changed files with 83 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/opt/optimize_objectives.cpp
View file

@ -43,9 +43,11 @@ Notes:
#include "optimize_objectives.h"
#include "opt_solver.h"
#include "arith_decl_plugin.h"
#include "smt_context.h"
namespace opt {
void optimize_objectives::set_cancel(bool f) {
m_cancel = true;
}
@ -62,50 +64,29 @@ namespace opt {
/*
Enumerate locally optimal assignments until fixedpoint.
*/
lbool optimize_objectives::basic_opt(app_ref_vector& objectives, vector<inf_eps>& values)
{
ast_manager& m = objectives.get_manager();
lbool optimize_objectives::basic_opt(app_ref_vector& objectives) {
arith_util autil(m);
s->reset_objectives();
values.reset();
m_lower.reset();
m_upper.reset();
// First check_sat call to initialize theories
lbool is_sat = s->check_sat(0, 0);
if (is_sat == l_false) {
if (is_sat != l_true) {
return is_sat;
}
opt_solver::scoped_push _push(*s);
opt_solver::toggle_objective _t(*s, true);
for (unsigned i = 0; i < objectives.size(); ++i) {
s->add_objective(objectives[i].get());
values.push_back(inf_eps(rational(-1),inf_rational(0)));
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
}
is_sat = s->check_sat(0, 0);
while (is_sat == l_true && !m_cancel) {
set_max(values, s->get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < values.size(); ++i) {
verbose_stream() << values[i] << " ";
}
verbose_stream() << "\n";);
expr_ref_vector disj(m);
expr_ref constraint(m);
for (unsigned i = 0; i < objectives.size(); ++i) {
inf_eps const& v = values[i];
disj.push_back(s->block_lower_bound(i, v));
}
constraint = m.mk_or(disj.size(), disj.c_ptr());
s->assert_expr(constraint);
is_sat = s->check_sat(0, 0);
is_sat = update_lower();
}
if (m_cancel || is_sat == l_undef) {
return l_undef;
@ -113,13 +94,40 @@ namespace opt {
return l_true;
}
lbool optimize_objectives::update_lower() {
lbool is_sat = s->check_sat(0, 0);
set_max(m_lower, s->get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < m_lower.size(); ++i) {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << "\n";);
expr_ref_vector disj(m);
expr_ref constraint(m);
for (unsigned i = 0; i < m_lower.size(); ++i) {
inf_eps const& v = m_lower[i];
disj.push_back(s->block_lower_bound(i, v));
}
constraint = m.mk_or(disj.size(), disj.c_ptr());
s->assert_expr(constraint);
return is_sat;
}
lbool optimize_objectives::update_upper() {
return l_undef;
}
/**
Takes solver with hard constraints added.
Returns an optimal assignment to objective functions.
*/
lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector<inf_eps>& values) {
s = &solver;
return basic_opt(objectives, values);
lbool result = basic_opt(objectives);
values.reset();
values.append(m_lower);
return result;
}
}

8
src/opt/optimize_objectives.h
View file

@ -31,6 +31,8 @@ namespace opt {
ast_manager& m;
opt_solver* s;
volatile bool m_cancel;
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
public:
optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}
@ -40,10 +42,14 @@ namespace opt {
private:
lbool basic_opt(app_ref_vector& objectives, vector<inf_eps>& values);
lbool basic_opt(app_ref_vector& objectives);
void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src);
lbool update_lower();
lbool update_upper();
};
};

3
src/smt/theory_arith.cpp
View file

@ -25,5 +25,6 @@ namespace smt {
template class theory_arith<i_ext>;
// template class theory_arith<si_ext>;
// template class theory_arith<smi_ext>;
// TBD: template class smt::theory_arith<inf_ext>;
};

22
src/smt/theory_arith.h
View file

@ -1121,11 +1121,33 @@ namespace smt {
}
smi_ext() : m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(0), true) {}
};
class inf_ext {
public:
typedef rational numeral;
typedef inf_eps_rational<inf_rational> inf_numeral;
inf_numeral m_int_epsilon;
inf_numeral m_real_epsilon;
numeral fractional_part(inf_numeral const& n) {
SASSERT(n.is_rational());
return n.get_rational() - floor(n);
}
static numeral fractional_part(numeral const & n) {
return n - floor(n);
}
static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
return inf_numeral(inf_rational(n, r));
}
inf_ext() : m_int_epsilon(inf_rational(rational(1))), m_real_epsilon(inf_rational(rational(0), true)) {}
};
typedef theory_arith<mi_ext> theory_mi_arith;
typedef theory_arith<i_ext> theory_i_arith;
typedef smt::theory_arith<inf_ext> theory_inf_arith;
// typedef theory_arith<si_ext> theory_si_arith;
// typedef theory_arith<smi_ext> theory_smi_arith;
};

16
src/util/inf_eps_rational.h
View file

@ -143,16 +143,28 @@ class inf_eps_rational {
return m_infty;
}
static const inf_eps_rational & zero() {
return inf_eps_rational(Numeral::zero());
}
static const inf_eps_rational & one() {
return inf_eps_rational(Numeral::one());
}
static const inf_eps_rational & minus_one() {
return inf_eps_rational(Numeral::minus_one());
}
inf_eps_rational & operator=(const inf_eps_rational & r) {
m_infty = r.m_infty;
m_r = r.m_r;
return *this;
}
inf_eps_rational & operator=(const rational & r) {
inf_eps_rational & operator=(const Numeral & r) {
m_infty.reset();
m_r = r;
return *this;
return *this;
}
inf_eps_rational & operator+=(const inf_eps_rational & r) {

2
src/util/inf_rational.h
View file

@ -88,7 +88,7 @@ class inf_rational {
m_second(pos_inf?rational(1):rational(-1))
{}
explicit inf_rational(rational const& r):
inf_rational(rational const& r):
m_first(r)
{
m_second.reset();