more updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/opt_cmds.cpp

@@ -138,7 +138,10 @@ public:
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
 
     virtual void set_next_arg(cmd_context & ctx, expr * t) {
-        m_opt_ctx().add_objective(t, m_is_max);
+        if (!is_app(t)) {
+            throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
+        }
+        m_opt_ctx().add_objective(to_app(t), m_is_max);
     }
 
     virtual void failure_cleanup(cmd_context & ctx) {

src/opt/opt_context.h

@@ -32,13 +32,12 @@ namespace opt {
 
     class context {
         ast_manager& m;
-        expr_ref_vector m_hard_constraints;
+        expr_ref_vector  m_hard_constraints;
         expr_ref_vector  m_soft_constraints;
         vector<rational> m_weights;
-
+        app_ref_vector   m_objectives;
-        expr_ref_vector m_objectives;
+        svector<bool>    m_is_max;
-        svector<bool>   m_is_max;
+        ref<solver>      m_solver;
-        ref<solver>     m_solver;
 
     public:
         context(ast_manager& m):
@@ -53,7 +52,7 @@ namespace opt {
             m_weights.push_back(w);
         }
 
-        void add_objective(expr* t, bool is_max) {
+        void add_objective(app* t, bool is_max) {
             m_objectives.push_back(t);
             m_is_max.push_back(is_max);
         }

src/opt/optimize_objectives.cpp

@@ -29,58 +29,68 @@ namespace opt {
     /*
         Enumerate locally optimal assignments until fixedpoint.
     */
-    lbool mathsat_style_opt(opt_solver& s, 
+    lbool mathsat_style_opt(
-                          expr_ref_vector& objectives, svector<bool> const& is_max,
+        opt_solver& s, 
-                          vector<inf_eps_rational<rational> >& values) {
+        app_ref_vector& objectives, 
-        enable_trace("maximize");        
+        svector<bool> const& is_max,
+        vector<inf_eps_rational<rational> >& values) 
+    {
+        SASSERT(is_max.size() == objectives.size());
+
+        enable_trace("maximize");        // NSB review: OK for now for debugging. Otherwise, use command-line /tr:maximize
+
         // First check_sat call for initialize theories
         lbool is_sat = s.check_sat(0, 0);
-        if (is_sat == l_false) {
+        if (is_sat != l_false) {
-            return l_false;
+            return is_sat;
         }
 
         s.push();
 
+
         // Assume there is only one objective function
+        SASSERT(is_max.size() == 1);
         ast_manager& m = objectives.get_manager();
         arith_util autil(m);
-        app* objective = m.mk_fresh_const("objective", autil.mk_real());
+        bool ismax = is_max[0];
-        if (is_max[0]) {
+        app_ref objective_var(m), objective_term(m), obj_eq(m);
-	        s.assert_expr(autil.mk_eq(objective, objectives[0].get()));
+        objective_term = ismax?objectives[0].get():autil.mk_uminus(objectives[0].get());
-        } else {
+        sort* srt = m.get_sort(objective_term);
-	        s.assert_expr(autil.mk_eq(objective, autil.mk_uminus(objectives[0].get())));
+        objective_var = m.mk_fresh_const("objective", srt);
-        };
+        obj_eq = autil.mk_eq(objective_var, objective_term);
-        s.set_objective(objective);
+        s.assert_expr(obj_eq);
+        s.set_objective(objective_var);  // NSB review: I would change signature of set_objective to take is_max and decide whether to add equation.
+                                         // Otherwise, the difference logic backends will not work.
         s.toggle_objective(true);
         is_sat = s.check_sat(0, 0);        
                 
-        while (is_sat != l_false) {
+        while (is_sat == l_true) {
             // Extract values for objectives
             inf_eps_rational<rational> val;
-			val = is_max[0] ? s.get_objective_value() : -s.get_objective_value();
+            val = is_max[0] ? s.get_objective_value() : -s.get_objective_value();
 
             // Check whether objective is unbounded
-            if (!val.is_rational()) {
+            // NSB: review: what if optimal is 1-epsilon. Then the check also fails.
-                values.reset();
-                values.push_back(val);
-                break;
-            }
 
-            // If values have initial data, they will be dropped
             values.reset();
             values.push_back(val);
 
-            // Assert there must be something better            
+            if (!val.is_rational()) {
-            expr_ref_vector assumptions(m);
+                break;
-            expr* bound = m.mk_fresh_const("bound", m.mk_bool_sort());
+            }
-            assumptions.push_back(bound);
+ 
-            expr* r = autil.mk_numeral(val.get_rational(), false);
+            expr_ref constraint(m);                       
-            s.assert_expr(m.mk_eq(bound, is_max[0] ? autil.mk_gt(objectives[0].get(), r) : autil.mk_lt(objectives[0].get(), r)));
+            constraint = autil.mk_gt(objective_term, autil.mk_numeral(val.get_rational(), srt));
-            is_sat = s.check_sat(1, assumptions.c_ptr());            
+            s.assert_expr(constraint);
+            is_sat = s.check_sat(0, 0);
         }      
 
         s.pop(1);
        
+        if (is_sat == l_undef) {
+            return is_sat;
+        }
+        SASSERT(is_sat == l_false); // NSB review: not really water-tight with cancellation and with infinitesimal solutions.
         return l_true;
     }
 
@@ -90,7 +100,7 @@ namespace opt {
     */
     
     lbool optimize_objectives(opt_solver& s, 
-                          expr_ref_vector& objectives, svector<bool> const& is_max,
+                          app_ref_vector& objectives, svector<bool> const& is_max,
                           vector<inf_eps_rational<rational> >& values) {
         return mathsat_style_opt(s, objectives, is_max, values);
     }

src/opt/optimize_objectives.h

@@ -28,8 +28,8 @@ namespace opt {
     */
     
     lbool optimize_objectives(opt_solver& s, 
-                          expr_ref_vector& objectives, svector<bool> const& is_max,
+                              app_ref_vector& objectives, svector<bool> const& is_max,
-                          vector<inf_eps_rational<rational> >& values);
+                              vector<inf_eps_rational<rational> >& values);
 };
 
 #endif