From a6e103dd36f989b7d6d32cd3eb68e01838bcefff Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Wed, 30 Oct 2013 06:30:51 +0100
Subject: [PATCH] Make a few variables private

---
 src/smt/network_flow_def.h      |  4 ++--
 src/smt/theory_arith.h          |  5 +++--
 src/smt/theory_arith_aux.h      |  5 ++---
 src/smt/theory_diff_logic.h     | 16 +++++++---------
 src/smt/theory_diff_logic_def.h | 15 ++++++++++-----
 5 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h
index 2950a77c3..b3be85a2f 100644
--- a/src/smt/network_flow_def.h
+++ b/src/smt/network_flow_def.h
@@ -125,10 +125,10 @@ namespace smt {
             edge_id e_id;
             get_edge_id(u, v, e_id);
             if (m_upwards[u]) {
-                m_potentials[u] = m_potentials[v] + m_graph.get_weight(e_id);
+                m_potentials[u] = m_potentials[v] - m_graph.get_weight(e_id);
             }
             else {
-                m_potentials[u] = m_potentials[v] - m_graph.get_weight(e_id);
+                m_potentials[u] = m_potentials[v] + m_graph.get_weight(e_id);
             }
             u = m_thread[u];
         }
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index a434c2e83..20631ea27 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -432,6 +432,8 @@ namespace smt {
         bool                    m_eager_gcd; // true if gcd should be applied at every add_row
         unsigned                m_final_check_idx;
 
+        inf_rational            m_objective_value;
+
         // backtracking
         svector<bound_trail>    m_bound_trail;
         svector<unsigned>       m_unassigned_atoms_trail;
@@ -997,8 +999,7 @@ namespace smt {
         virtual theory_var add_objective(app* term);
         virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
         virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
-        inf_rational m_objective_value;
-
+        
         // -----------------------------------
         //
         // Pretty Printing
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 86b2ff28a..d43d1ef24 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -998,9 +998,8 @@ namespace smt {
     }
 
     template<typename Ext>
-    inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) { 
-        inf_eps_rational<inf_rational> val(m_objective_value);     
-        return val; 
+    inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
+        return inf_eps_rational<inf_rational>(m_objective_value); 
     }
 
     /**
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 158ea3209..3b566d8c2 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -185,7 +185,13 @@ namespace smt {
 
         arith_factory *                m_factory;
         rational                       m_delta;
-        nc_functor                     m_nc_functor;        
+        nc_functor                     m_nc_functor;   
+
+        // For optimization purpose
+        typedef vector <std::pair<theory_var, rational> > objective_term;
+        vector<objective_term>          m_objectives;
+        vector<rational>                m_objective_consts;
+        numeral                        m_objective_value;
 
         // Set a conflict due to a negative cycle.
         void set_neg_cycle_conflict();
@@ -309,14 +315,6 @@ namespace smt {
         virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
         virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
 
-        // TBD: why are these public?:
-        numeral                        m_objective_value;
-
-
-        typedef vector <std::pair<theory_var, rational> > objective_term;
-        vector<objective_term> m_objectives;
-        vector<rational>       m_objective_consts;
-
         bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
 
     private:        
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 46565b0e6..bcf22a2de 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1004,10 +1004,10 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
     objective_term const& objective = m_objectives[v];
 
     IF_VERBOSE(1,
-               for (unsigned i = 0; i < objective.size(); ++i) {
-                   verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
-               }
-               verbose_stream() << m_objective_consts[v] << "\n";);
+        for (unsigned i = 0; i < objective.size(); ++i) {
+            verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
+        }
+        verbose_stream() << m_objective_consts[v] << "\n";);
 
     // Objective coefficients now become balances
     vector<fin_numeral> balances(m_graph.get_num_nodes());
@@ -1023,7 +1023,12 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
         vector<numeral> potentials;
         m_objective_value = net_flow.get_optimal_solution(potentials, true);
         std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl;
-        // TODO: return the model of the optimal solution from potential        
+        // TODO: return the model of the optimal solution from potentials
+        IF_VERBOSE(1,
+            for (unsigned i = 0; i < potentials.size(); ++i) {
+                verbose_stream() << "v" << i << " -> " << potentials[i] << "\n";
+            });
+
     } 
     else {
         std::cout << "Unbounded objective" << std::endl;