From 0b65aa83e801c68b8159b892af282f60ac02d547 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 31 Oct 2013 02:02:37 -0700 Subject: [PATCH] preparing for inf extension of arithmetic Signed-off-by: Nikolaj Bjorner --- src/opt/optimize_objectives.cpp | 66 ++++++++++++++++++--------------- src/opt/optimize_objectives.h | 8 +++- src/smt/theory_arith.cpp | 3 +- src/smt/theory_arith.h | 22 +++++++++++ src/util/inf_eps_rational.h | 16 +++++++- src/util/inf_rational.h | 2 +- 6 files changed, 83 insertions(+), 34 deletions(-) diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index d310abba6..ffba96a9e 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -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& 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& values) { s = &solver; - return basic_opt(objectives, values); + lbool result = basic_opt(objectives); + values.reset(); + values.append(m_lower); + return result; } } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index bacc27b09..cb3176d0d 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -31,6 +31,8 @@ namespace opt { ast_manager& m; opt_solver* s; volatile bool m_cancel; + vector m_lower; + vector 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& values); + lbool basic_opt(app_ref_vector& objectives); void set_max(vector& dst, vector const& src); + lbool update_lower(); + + lbool update_upper(); + }; }; diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp index 0bb356b95..6c18b66c3 100644 --- a/src/smt/theory_arith.cpp +++ b/src/smt/theory_arith.cpp @@ -25,5 +25,6 @@ namespace smt { template class theory_arith; // template class theory_arith; // template class theory_arith; - + + // TBD: template class smt::theory_arith; }; diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 20631ea27..80731ab1d 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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_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 theory_mi_arith; typedef theory_arith theory_i_arith; + typedef smt::theory_arith theory_inf_arith; // typedef theory_arith theory_si_arith; // typedef theory_arith theory_smi_arith; + }; diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index 1d6d04818..a8d32e2b2 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -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) { diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index 5cdfe9e93..2da99cca5 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -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();