From 898609a3ef4e923f6041cfc0f0ad5306ce30bb6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Oct 2013 20:50:33 -0700 Subject: [PATCH] cleanup macro usage Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 30 +++++++++++++++++------------- src/opt/opt_solver.h | 3 +++ src/smt/theory_arith.h | 11 +++++------ src/smt/theory_arith_aux.h | 21 +++++++-------------- src/smt/theory_opt.h | 32 ++++++++++++++++++++++++++++++++ 5 files changed, 64 insertions(+), 33 deletions(-) create mode 100644 src/smt/theory_opt.h diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 4989993b4..8f041e9c2 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -43,17 +43,21 @@ namespace opt { m_context.pop(n); } -#define ACCESS_ARITHMETIC_CLASS(_code_) \ - smt::context& ctx = m_context.get_context(); \ - smt::theory_id arith_id = m_context.m().get_family_id("arith"); \ - smt::theory* arith_theory = ctx.get_theory(arith_id); \ - if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) { \ - smt::theory_mi_arith& th = dynamic_cast(*arith_theory); \ - _code_; \ - } \ - else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) { \ - smt::theory_i_arith& th = dynamic_cast(*arith_theory); \ - _code_; \ + + smt::theory_opt& opt_solver::get_optimizer() { + smt::context& ctx = m_context.get_context(); + smt::theory_id arith_id = m_context.m().get_family_id("arith"); + smt::theory* arith_theory = ctx.get_theory(arith_id); + if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } + else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } + else { + UNREACHABLE(); + return dynamic_cast(*arith_theory); + } } @@ -61,7 +65,7 @@ namespace opt { TRACE("opt_solver_na2as", tout << "smt_opt_solver::check_sat_core: " << num_assumptions << "\n";); lbool r = m_context.check(num_assumptions, assumptions); if (r == l_true &&& m_objective_enabled) { - ACCESS_ARITHMETIC_CLASS(th.min(m_objective_var);); + VERIFY(get_optimizer().max_min(m_objective_var, false)); } return r; } @@ -113,7 +117,7 @@ namespace opt { } void opt_solver::set_objective(app* term) { - ACCESS_ARITHMETIC_CLASS(m_objective_var = th.set_objective(term);); + m_objective_var = get_optimizer().add_objective(term); } void opt_solver::toggle_objective(bool enable) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index a6a48d3f9..c9fd48ed2 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -26,6 +26,7 @@ Notes: #include"smt_kernel.h" #include"smt_params.h" #include"smt_types.h" +#include"theory_opt.h" namespace opt { @@ -60,6 +61,8 @@ namespace opt { void set_objective(app* term); void toggle_objective(bool enable); + private: + smt::theory_opt& get_optimizer(); }; } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index d9c0efb72..f007492a7 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -36,6 +36,7 @@ Revision History: #include"grobner.h" #include"arith_simplifier_plugin.h" #include"arith_eq_solver.h" +#include"theory_opt.h" namespace smt { @@ -80,7 +81,7 @@ namespace smt { */ template - class theory_arith : public theory, private Ext { + class theory_arith : public theory, public theory_opt, private Ext { public: typedef typename Ext::numeral numeral; typedef typename Ext::inf_numeral inf_numeral; @@ -855,7 +856,6 @@ namespace smt { template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); bool max_min(row & r, bool max); - bool max_min(theory_var v, bool max); bool max_min(svector const & vars); // ----------------------------------- @@ -985,15 +985,14 @@ namespace smt { // ----------------------------------- virtual bool get_value(enode * n, expr_ref & r); + // ----------------------------------- // // Optimization // // ----------------------------------- - - void min(theory_var v); - theory_var set_objective(app* term); - + virtual bool max_min(theory_var v, bool max); + virtual theory_var add_objective(app* term); // ----------------------------------- // diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index e668997fc..12658a979 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -948,22 +948,15 @@ namespace smt { return x_i; } - /** - \brief minimize the given variable. - TODO: max_min returns a bool. What does this do? - */ - template - void theory_arith::min(theory_var v) { - max_min(v, false); - } - + // // set_objective(expr* term) internalizes the arithmetic term and creates - // a row for it if it is not already internalized. Then return the variable - // corresponding to the term. - // TODO handle case where internalize fails. e.g., check for this in a suitable way. + // a row for it if it is not already internalized. + // Then return the variable corresponding to the term. + // + template - theory_var theory_arith::set_objective(app* term) { - return internalize_term_core(term); + theory_var theory_arith::add_objective(app* term) { + return internalize_term(term); } /** diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h new file mode 100644 index 000000000..f0759e9fc --- /dev/null +++ b/src/smt/theory_opt.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_opt.h + +Abstract: + + Interface utilities used by optimization providing + theory solvers. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-10-18 + +Notes: + +--*/ + +#ifndef _THEORY_OPT_H_ +#define _THEORY_OPT_H_ + +namespace smt { + class theory_opt { + public: + virtual bool max_min(theory_var v, bool max) { UNREACHABLE(); return false; }; + virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } + }; +} + +#endif