From 3441fc29427242dc334204d36c2861623d4d4941 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Mon, 21 Oct 2013 17:25:34 -0700 Subject: [PATCH] A few changes based on previous reviews Tested the optimization procedure with: - unbounded objectives - bounded with rational solutions - bounded with irrational solutions --- src/opt/opt_context.cpp | 3 ++- src/opt/opt_solver.cpp | 4 ++-- src/opt/opt_solver.h | 5 +++-- src/opt/optimize_objectives.cpp | 24 ++++++++++-------------- src/opt/optimize_objectives.h | 2 +- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 5 ++--- src/smt/theory_opt.h | 5 +++-- 8 files changed, 24 insertions(+), 26 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 45b945d73..ff49a5c8d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -68,7 +68,7 @@ namespace opt { } if (!m_objectives.empty()) { - vector > values; + vector > 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(*s), m_objectives, m_is_max, values); std::cout << "is-sat: " << is_sat << "\n"; + if (is_sat != l_true) { return; } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index c2a01f92f..220ae0143 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -70,7 +70,7 @@ namespace opt { if (is_bounded) { m_objective_value = get_optimizer().get_objective_value(m_objective_var); } else { - inf_eps_rational r(rational(1), rational(0)); + inf_eps_rational r(rational(1), inf_rational(0)); m_objective_value = r; } } @@ -131,7 +131,7 @@ namespace opt { m_objective_enabled = enable; } - inf_eps_rational opt_solver::get_objective_value() { + inf_eps_rational opt_solver::get_objective_value() { return m_objective_value; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 3904a3646..9b59bf93b 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -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 m_objective_value; + inf_eps_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 get_objective_value(); + inf_eps_rational get_objective_value(); private: smt::theory_opt& get_optimizer(); }; diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index f7bcb362c..e167922cc 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -33,23 +33,20 @@ namespace opt { opt_solver& s, app_ref_vector& objectives, svector const& is_max, - vector >& values) + vector >& 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 val; - val = is_max[0] ? s.get_objective_value() : -s.get_objective_value(); + inf_eps_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 const& is_max, - vector >& values) { + vector >& values) { return mathsat_style_opt(s, objectives, is_max, values); } } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index 94a6f591a..fcf388fc9 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -29,7 +29,7 @@ namespace opt { lbool optimize_objectives(opt_solver& s, app_ref_vector& objectives, svector const& is_max, - vector >& values); + vector >& values); }; #endif diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 99b7e34f3..e0e535189 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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 get_objective_value(theory_var v); + virtual inf_eps_rational get_objective_value(theory_var v); inf_rational m_objective; // ----------------------------------- diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index da56f8b0f..8d010be71 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -961,9 +961,8 @@ namespace smt { } template - inf_eps_rational theory_arith::get_objective_value(theory_var v) { - inf_eps_rational val; - val = m_objective.get_rational(); + inf_eps_rational theory_arith::get_objective_value(theory_var v) { + inf_eps_rational val(m_objective); return val; } diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index c3765a1fc..9b013612b 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -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 get_objective_value(theory_var v) { + virtual inf_eps_rational get_objective_value(theory_var v) { UNREACHABLE(); - inf_eps_rational r(rational(1), rational(0)); + inf_eps_rational r(rational(1), inf_rational(0)); return r; } };