From 736d43c084600c10045e6d429ecf4d270217c2b6 Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Fri, 1 Nov 2013 08:05:29 +0100
Subject: [PATCH] Block lower bound of difference logic objectives

---
 src/smt/network_flow_def.h      |  7 +++----
 src/smt/theory_diff_logic.h     |  5 +++--
 src/smt/theory_diff_logic_def.h | 34 ++++++++++++++++++++++++++++++---
 3 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h
index 5d7f5018b..e4fb13f37 100644
--- a/src/smt/network_flow_def.h
+++ b/src/smt/network_flow_def.h
@@ -308,7 +308,7 @@ namespace smt {
         m_thread[z] = y;
         n = q;
         last = m_final[q];
-        while (n != last) {
+        while (n != last && n != -1) {
             m_depth[n] += 1 + m_depth[p];
             n = m_pred[n];
         }
@@ -495,7 +495,7 @@ namespace smt {
         // m_pred is predecessor link
         // m_depth depth counting from a root note.
         // m_graph
-
+#if 0
         node root = m_pred.size()-1;
         for (unsigned i = 0; i < m_upwards.size(); ++i) {
             if (m_upwards[i]) {
@@ -509,8 +509,7 @@ namespace smt {
         // m_thread forms a spanning tree over [0..root]
         // union-find structure:
         svector<int> roots(root+1, -1);
-
-#if 0              
+              
         for (unsigned i = 0; i < m_thread.size(); ++i) {
             if (m_states[i] == BASIS) {
                 node x = m_thread[i];
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 3b566d8c2..ecb512bda 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -189,8 +189,9 @@ namespace smt {
 
         // For optimization purpose
         typedef vector <std::pair<theory_var, rational> > objective_term;
-        vector<objective_term>          m_objectives;
-        vector<rational>                m_objective_consts;
+        vector<objective_term>         m_objectives;
+        vector<rational>               m_objective_consts;
+        vector<vector<numeral> >       m_objective_assignments;
         numeral                        m_objective_value;
 
         // Set a conflict due to a negative cycle.
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index df78a2763..98bd2268e 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -778,6 +778,7 @@ void theory_diff_logic<Ext>::reset_eh() {
     m_non_diff_logic_exprs  = false;
     m_objectives      .reset();
     m_objective_consts.reset();
+    m_objective_assignments.reset();
     theory::reset_eh();
 }
 
@@ -1023,7 +1024,7 @@ 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 potentials
+        m_objective_assignments[v] = potentials;
         TRACE("network_flow",
             for (unsigned i = 0; i < potentials.size(); ++i) {
                 tout << "v" << i << " -> " << potentials[i] << "\n";
@@ -1041,9 +1042,11 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
     objective_term objective;
     theory_var result = m_objectives.size();
     rational q(1), r(0);
+    vector<numeral> vr;
     if (internalize_objective(term, q, r, objective)) {
         m_objectives.push_back(objective);
         m_objective_consts.push_back(r);
+        m_objective_assignments.push_back(vr);
     }
     else {
         result = null_theory_var;
@@ -1063,7 +1066,6 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
     ast_manager& m = get_manager();
     objective_term const& t = m_objectives[v];
     expr_ref e(m), f(m), f2(m);
-    // hacky implementation for now.
     if (t.size() == 1 && t[0].second.is_one()) {
         f = get_enode(t[0].first)->get_owner();
     }
@@ -1081,8 +1083,34 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
         f = m_util.mk_sub(f, f2);
     }
     else {
-        NOT_IMPLEMENTED_YET();
+        expr_ref_vector disj(m);
+        vector<numeral> const & ns = m_objective_assignments[v];
+        inf_rational val;
+        rational r, s;
+        for (unsigned i = 0; i < t.size(); ++i) {
+            r = ns[i].get_rational().to_rational();
+            s = ns[i].get_infinitesimal().to_rational(); 
+            val = inf_rational(r, s);
+            f = get_enode(t[i].first)->get_owner();
+            e = m_util.mk_numeral(val.get_rational(), m.get_sort(f));
+            if (t[i].second.is_neg() && val.get_infinitesimal().is_pos()) {
+                disj.push_back(m_util.mk_le(f, e));
+            }
+            else if (t[i].second.is_neg()) {
+                disj.push_back(m_util.mk_lt(f, e));
+            }
+            else if (t[i].second.is_pos() && val.get_infinitesimal().is_neg()) {
+                disj.push_back(m_util.mk_ge(f, e));
+            }
+            else if (t[i].second.is_pos()) {
+                disj.push_back(m_util.mk_gt(f, e));
+            }
+            else {
+            }
+        }
+        return m.mk_or(disj.size(), disj.c_ptr());
     }
+
     inf_rational new_val = val - inf_rational(m_objective_consts[v]);
     e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));