Enhancement for Valentin #332

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

src/opt/opt_context.cpp

@@ -241,27 +241,37 @@ namespace opt {
         TRACE("opt", model_smt2_pp(tout, m, *m_model, 0););
         m_optsmt.setup(*m_opt_solver.get());
         update_lower();
+        
         switch (m_objectives.size()) {
         case 0:
-            return is_sat;
+            break;
         case 1:
-            return execute(m_objectives[0], true, false);
+            is_sat = execute(m_objectives[0], true, false);
+            break;
         default: {
             opt_params optp(m_params);
             symbol pri = optp.priority();
             if (pri == symbol("pareto")) {
-                return execute_pareto();
+                is_sat = execute_pareto();
             }
             else if (pri == symbol("box")) {
-                return execute_box();
+                is_sat = execute_box();
             }
             else {
-                return execute_lex();
+                is_sat = execute_lex();
             }
+            break;
         }
         }
+        return adjust_unknown(is_sat);
     }
 
+    lbool context::adjust_unknown(lbool r) {
+        if (r == l_true && m_opt_solver.get() && m_opt_solver->was_unknown()) {
+            r = l_undef;
+        }
+        return r;
+    }
 
     bool context::print_model() const {
         opt_params optp(m_params);

src/opt/opt_context.h

@@ -229,6 +229,7 @@ namespace opt {
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();
+        lbool adjust_unknown(lbool r);
         bool scoped_lex();
         expr_ref to_expr(inf_eps const& n);
 

src/opt/opt_solver.cpp

@@ -44,7 +44,8 @@ namespace opt {
         m_fm(fm),
         m_objective_terms(m),
         m_dump_benchmarks(false),
-        m_first(true) {
+        m_first(true),
+        m_was_unknown(false) {
         m_params.updt_params(p);
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
             m_params.m_relevancy_lvl = 0;
@@ -173,6 +174,7 @@ namespace opt {
         else {
             r = m_context.check(num_assumptions, assumptions);
         }
+        r = adjust_result(r);
         m_first = false;
         if (dump_benchmarks()) {
             w.stop();
@@ -242,6 +244,7 @@ namespace opt {
         TRACE("opt", tout << ge << "\n";);
         assert_expr(ge);
         lbool is_sat = m_context.check(0, 0);
+        is_sat = adjust_result(is_sat);
         if (is_sat == l_true) {
             set_model(i);
         }
@@ -261,6 +264,13 @@ namespace opt {
 
     }
 
+    lbool opt_solver::adjust_result(lbool r) {
+        if (r == l_undef && m_context.last_failure() == smt::QUANTIFIERS) {
+            r = l_true;
+            m_was_unknown = true;
+        }
+        return r;
+    }
     
     void opt_solver::get_unsat_core(ptr_vector<expr> & r) {
         unsigned sz = m_context.get_unsat_core_size();

src/opt/opt_solver.h

@@ -82,6 +82,7 @@ namespace opt {
         static unsigned     m_dump_count;
         statistics          m_stats;
         bool                m_first;
+        bool                m_was_unknown;
     public:
         opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
         virtual ~opt_solver();
@@ -117,6 +118,8 @@ namespace opt {
             return m_valid_objectives[obj_index];
         }
 
+        bool was_unknown() const { return m_was_unknown; }
+
         vector<inf_eps> const& get_objective_values();
         expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
 
@@ -136,6 +139,7 @@ namespace opt {
     private:
         lbool decrement_value(unsigned i, inf_eps& val);
         void set_model(unsigned i);
+        lbool adjust_result(lbool r);
     };
 }