From b25e8e2288b77a74cc8f9ef8c913271d27123e31 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 13 Sep 2015 16:00:45 +0200
Subject: [PATCH] tune lexicographic products, avoid push/pop and ensure
 correction sets are not used for multiple objectives

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp      |  2 +-
 src/opt/opt_context.cpp | 17 ++++++++++++++++-
 src/opt/opt_context.h   |  2 ++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index f57d33c95..7c470f552 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -507,7 +507,7 @@ public:
             --m_correction_set_size;
         }
         trace();
-        if (m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
+        if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
             exprs cs;
             get_current_correction_set(m_csmodel.get(), cs);
             m_correction_set_size = cs.size();
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index f3d0e9bd0..0264ea70f 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -314,12 +314,27 @@ namespace opt {
         }
     }
     
+    /**
+       \brief there is no need to use push/pop when all objectives are maxsat and engine
+       is maxres.
+    */
+    bool context::scoped_lex() {
+        if (m_maxsat_engine == symbol("maxres")) {
+            for (unsigned i = 0; i < m_objectives.size(); ++i) {
+                if (m_objectives[i].m_type != O_MAXSMT) return true;
+            }
+            return false;
+        }
+        return true;
+    }
+
     lbool context::execute_lex() {
         lbool r = l_true;
+        bool sc = scoped_lex();
         IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
         for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
             bool is_last = i + 1 == m_objectives.size();
-            r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last);
+            r = execute(m_objectives[i], i + 1 < m_objectives.size(), sc && !is_last);
             if (r == l_true && !get_lower_as_num(i).is_finite()) {
                 return r;
             }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index aa8c0a69a..735dc6905 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -54,6 +54,7 @@ namespace opt {
         virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter.
         virtual void get_base_model(model_ref& _m) = 0;  // retrieve model from initial satisfiability call.
         virtual smt::context& smt_context() = 0;    // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
+        virtual unsigned num_objectives() = 0;
     };
 
     /**
@@ -228,6 +229,7 @@ namespace opt {
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();
+        bool scoped_lex();
         expr_ref to_expr(inf_eps const& n);
 
         void reset_maxsmts();