Add push/pop to box optimization

src/opt/opt_cmds.cpp

@@ -249,8 +249,8 @@ private:
 };
 
 static expr* sexpr2expr(cmd_context & ctx, sexpr * s) {
-    NOT_IMPLEMENTED_YET();
+    NOT_IMPLEMENTED_YET();    
-    return 0;
+    return ctx.m().mk_true();
 }
 
 static opt::objective* sexpr2objective(cmd_context & ctx, sexpr * s) {

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);
+            result = execute(*children[i], true);
-            if (result != l_true) return result;
+            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);
+            push();
-            if (result != l_true) return result;
+            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);

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();
 

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();
     }