fix lack of warning/error for unbounded objectives in context of quantifiers #1382

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

src/opt/opt_context.cpp

@@ -345,12 +345,24 @@ namespace opt {
         fix_model(mdl);
     }
 
+    bool context::contains_quantifiers() const {
+        for (expr* f : m_hard_constraints) {
+            if (has_quantifiers(f)) return true;
+        }
+        return false;
+    }
+
+
     lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
         if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index, is_max);
         if (result == l_true) m_optsmt.get_model(m_model, m_labels);
         if (scoped) get_solver().pop(1);        
         if (result == l_true && committed) m_optsmt.commit_assignment(index);
+        if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
+            throw default_exception("unbounded objectives on quantified constraints is not supported");
+            result = l_undef;
+        }
         return result;
     }
     
@@ -646,8 +658,7 @@ namespace opt {
         expr_fast_mark1 visited;
         is_bv proc(m);
         try {
-            for (unsigned i = 0; i < m_objectives.size(); ++i) {
+            for (objective& obj : m_objectives) {
-                objective & obj = m_objectives[i];
                 if (obj.m_type != O_MAXSMT) return false;
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
                 for (unsigned j = 0; j < ms.size(); ++j) {
@@ -658,8 +669,8 @@ namespace opt {
             for (unsigned i = 0; i < sz; i++) {
                 quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
             }
-            for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+            for (expr* f : m_hard_constraints) {
-                quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
+                quick_for_each_expr(proc, visited, f);
             }
         }
         catch (is_bv::found) {

src/opt/opt_context.h

@@ -233,13 +233,14 @@ namespace opt {
 
     private:
         lbool execute(objective const& obj, bool committed, bool scoped);
-        lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
+        lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);        
         lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();
         lbool adjust_unknown(lbool r);
         bool scoped_lex();
+        bool contains_quantifiers() const;
         expr_ref to_expr(inf_eps const& n);
         void to_exprs(inf_eps const& n, expr_ref_vector& es);
 

src/opt/optsmt.cpp

@@ -161,6 +161,14 @@ namespace opt {
         return l_true;        
     }
 
+    bool optsmt::is_unbounded(unsigned obj_index, bool is_maximize) {
+        if (is_maximize) {
+            return !m_upper[obj_index].is_finite();
+        }
+        else {
+            return !m_lower[obj_index].is_finite();
+        }
+    }
 
     lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
         arith_util arith(m);

src/opt/optsmt.h

@@ -49,6 +49,8 @@ namespace opt {
 
         lbool lex(unsigned obj_index, bool is_maximize);
 
+        bool is_unbounded(unsigned obj_index, bool is_maximize);
+
         unsigned add(app* t);
 
         void updt_params(params_ref& p);