From 03f5020d0b599e03e2fc8b3ffabc06cb74274c39 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Dec 2013 22:06:15 -0800
Subject: [PATCH] Nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 36 +++++++++++++++++-------------------
 src/opt/opt_context.h   | 21 ++++++++++++---------
 2 files changed, 29 insertions(+), 28 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index f9f6def15..710d8a739 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -84,8 +84,7 @@ namespace opt {
         // HACK: reuse m_optsmt but add only a single objective each round
         bool is_max = (obj->get_decl_kind() == OP_MAXIMIZE);
         m_optsmt.add(to_app(obj->get_arg(0)), is_max);
-        opt_solver& s = *m_solver.get();
-        lbool result = m_optsmt(s);
+        lbool result = m_optsmt(get_solver());
         if (committed) m_optsmt.commit_assignment(0);
         return result;
     }
@@ -93,30 +92,27 @@ namespace opt {
     lbool context::execute_maxsat(app* obj, bool committed) {
         maxsmt* ms;
         VERIFY(m_maxsmts.find(obj->get_decl()->get_name(), ms));
-        opt_solver& s = *m_solver.get();
-        lbool result = (*ms)(s);
+        lbool result = (*ms)(get_solver());
         if (committed) ms->commit_assignment();
         return result;
     }
     
     lbool context::execute_lex(app* obj) {
-        lbool result = l_true;
-        for (unsigned i = 0; i < obj->get_num_args(); ++i) {
-            result = execute(obj->get_arg(i), true);
-            if (result != l_true) break;
+        lbool r = l_true;
+        for (unsigned i = 0; r == l_true && i < obj->get_num_args(); ++i) {
+            r = execute(obj->get_arg(i), true);
         }
-        return result;
+        return r;
     }    
 
     lbool context::execute_box(app* obj) {
-        lbool result = l_true;
-        for (unsigned i = 0; i < obj->get_num_args(); ++i) {
+        lbool r = l_true;
+        for (unsigned i = 0; r == l_true && i < obj->get_num_args(); ++i) {
             push();
-            result = execute(obj->get_arg(i), false);
+            r = execute(obj->get_arg(i), false);
             pop(1);
-            if (result != l_true) break;
         }
-        return result;
+        return r;
     }
 
     lbool context::execute_pareto(app* obj) {
@@ -124,18 +120,20 @@ namespace opt {
         return execute_lex(obj);
     }
 
+    opt_solver& context::get_solver() { 
+        return *m_solver.get(); 
+    }
+
     void context::push() {
-        opt_solver& s = *m_solver.get();
-        s.push();
+        get_solver().push();
     }
 
     void context::pop(unsigned sz) {
-        opt_solver& s = *m_solver.get();
-        s.pop(sz);
+        get_solver().pop(sz);
     }
 
     lbool context::optimize(expr* objective) {
-        opt_solver& s = *m_solver.get(); 
+        opt_solver& s = get_solver();
         solver::scoped_push _sp(s);
 
         for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index bc2cc713a..30308f0d9 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -53,15 +53,6 @@ namespace opt {
         void add_objective(app* t, bool is_max) { m_objs.push_back(t); m_ismaxs.push_back(is_max); }
         void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
 
-        lbool execute(expr* obj, bool committed);
-        lbool execute_min_max(app* obj, bool committed);
-        lbool execute_maxsat(app* obj, bool committed);
-        lbool execute_lex(app* obj);
-        lbool execute_box(app* obj);
-        lbool execute_pareto(app* obj);
-
-        void push();
-        void pop(unsigned sz);
 
         lbool optimize(expr* objective);
         lbool optimize();
@@ -76,6 +67,18 @@ namespace opt {
         void updt_params(params_ref& p);
     private:
         void validate_feasibility(maxsmt& ms);
+
+        lbool execute(expr* obj, bool committed);
+        lbool execute_min_max(app* obj, bool committed);
+        lbool execute_maxsat(app* obj, bool committed);
+        lbool execute_lex(app* obj);
+        lbool execute_box(app* obj);
+        lbool execute_pareto(app* obj);
+
+        void push();
+        void pop(unsigned sz);
+        opt_solver& get_solver();
+
     };
 
 }