cleanup macro usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<smt::theory_mi_arith&>(*arith_theory); \
-        _code_;                                                         \
-    }                                                                   \
-    else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) {   \
-        smt::theory_i_arith& th = dynamic_cast<smt::theory_i_arith&>(*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<smt::theory_mi_arith&>(*arith_theory); 
+        }                                                                   
+        else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) {   
+            return dynamic_cast<smt::theory_i_arith&>(*arith_theory); 
+        }
+        else {
+            UNREACHABLE();
+            return dynamic_cast<smt::theory_mi_arith&>(*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) {

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();
     };
 }
 

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<typename Ext>
-    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<bool invert>
         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<theory_var> 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);
 
         // -----------------------------------
         //

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<typename Ext>
-    void theory_arith<Ext>::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<typename Ext>
-    theory_var theory_arith<Ext>::set_objective(app* term) {
-        return internalize_term_core(term);
+    theory_var theory_arith<Ext>::add_objective(app* term) {
+        return internalize_term(term);
     }
 
     /**

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