exposing lower/upper

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

src/opt/opt_context.cpp

@@ -108,7 +108,7 @@ namespace opt {
     lbool context::execute_lex() {
         lbool r = l_true;
         for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
-            r = execute(m_objectives[i], true);
+            r = execute(m_objectives[i], i + 1 < m_objectives.size());
         }
         return r;
     }    
@@ -180,6 +180,31 @@ namespace opt {
         m_optsmt.display_range_assignment(out);
     }
 
+    expr_ref context::get_lower(unsigned idx) {
+        NOT_IMPLEMENTED_YET();
+        if (idx > m_objectives.size()) {
+            throw default_exception("index out of bounds"); 
+        }
+        objective const& obj = m_objectives[idx];
+        switch(obj.m_type) {
+        case O_MAXSMT: {
+            maxsmt* ms = m_maxsmts.find(obj.m_id);
+            inf_eps l = ms->get_lower();
+            break;
+        }
+        case O_MAXIMIZE:
+        case O_MINIMIZE:
+            break;
+        }
+
+        return expr_ref(0,m);
+    }
+
+    expr_ref context::get_upper(unsigned idx) {
+        NOT_IMPLEMENTED_YET();
+        return expr_ref(0, m);
+    }
+        
     void context::set_cancel(bool f) {
         if (m_solver) {
             m_solver->set_cancel(f);

src/opt/opt_context.h

@@ -80,6 +80,10 @@ namespace opt {
         void display_range_assignment(std::ostream& out);
         static void collect_param_descrs(param_descrs & r);
         void updt_params(params_ref& p);
+
+        expr_ref get_lower(unsigned idx);
+        expr_ref get_upper(unsigned idx);
+
     private:
         void validate_feasibility(maxsmt& ms);