From 5ed8a48ac2ca8815edaf0926b511772307bc310f Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Tue, 26 Nov 2013 14:16:59 -0800
Subject: [PATCH] Add push/pop to box optimization

---
 src/opt/opt_cmds.cpp            |  4 ++--
 src/opt/opt_context.cpp         | 28 +++++++++++++++++++++-------
 src/opt/opt_context.h           |  3 +++
 src/smt/theory_diff_logic_def.h |  3 +++
 4 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 803d38295..6bf45daee 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -249,8 +249,8 @@ private:
 };
 
 static expr* sexpr2expr(cmd_context & ctx, sexpr * s) {
-    NOT_IMPLEMENTED_YET();
-    return 0;
+    NOT_IMPLEMENTED_YET();    
+    return ctx.m().mk_true();
 }
 
 static opt::objective* sexpr2objective(cmd_context & ctx, sexpr * s) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 13680c16a..198ed918b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -90,20 +90,24 @@ namespace opt {
     
     lbool context::execute_lex(compound_objective & obj) {
         ptr_vector<objective> children(obj.num_children(), obj.children());
+        lbool result = l_true;
         for (unsigned i = 0; i < children.size(); ++i) {
-            lbool result = execute(*children[i], true);
-            if (result != l_true) return result;
+            result = execute(*children[i], true);
+            if (result != l_true) break;
         }
-        return l_true;
-    }
+        return result;
+    }    
 
     lbool context::execute_box(compound_objective & obj) {
         ptr_vector<objective> children(obj.num_children(), obj.children());
+        lbool result = l_true;
         for (unsigned i = 0; i < children.size(); ++i) {
-            lbool result = execute(*children[i], false);
-            if (result != l_true) return result;
+            push();
+            result = execute(*children[i], false);
+            pop(1);
+            if (result != l_true) break;
         }
-        return l_true;
+        return result;
     }
 
     lbool context::execute_pareto(compound_objective & obj) {
@@ -111,6 +115,16 @@ namespace opt {
         return execute_lex(obj);
     }
 
+    void context::push() {
+        opt_solver& s = *m_solver.get();
+        s.push();
+    }
+
+    void context::pop(unsigned sz) {
+        opt_solver& s = *m_solver.get();
+        s.pop(sz);
+    }
+
     lbool context::optimize(objective & objective) {
         opt_solver& s = *m_solver.get(); 
         solver::scoped_push _sp(s);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 68cf61d80..f70440de6 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -59,6 +59,9 @@ namespace opt {
         lbool execute_box(compound_objective & obj);
         lbool execute_pareto(compound_objective & obj);
 
+        void push();
+        void pop(unsigned sz);
+
         lbool optimize(objective & objective);
         lbool optimize();
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index a3f1930c1..7472edd8b 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1028,6 +1028,7 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
 
     network_flow<GExt> net_flow(m_graph, balances);
     min_flow_result result = net_flow.min_cost();
+    SASSERT(result != UNBOUNDED);
     if (result == OPTIMAL) {
         numeral objective_value = net_flow.get_optimal_solution(m_objective_assignments[v], true) + numeral(m_objective_consts[v]);
         IF_VERBOSE(1, verbose_stream() << "Optimal value of objective " << v << ": " << objective_value << std::endl;);
@@ -1059,6 +1060,8 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
         return inf_eps_rational<inf_rational>(inf_rational(r, i));
     } 
     else {
+        // Dual problem is infeasible, primal problem is unbounded
+        SASSERT(result == INFEASIBLE);
         IF_VERBOSE(1, verbose_stream() << "Unbounded objective" << std::endl;);
         return inf_eps_rational<inf_rational>::infinity();
     }