From 1c56d6ee95608f05106d66e21f6f6492067a5d48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Aug 2014 01:17:26 -0700
Subject: [PATCH] align lengths of weights and soft constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp | 12 ++++++++++--
 src/opt/maxsls.cpp |  2 +-
 src/opt/maxsmt.cpp |  4 ++--
 src/opt/maxsmt.h   |  2 +-
 4 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 8a4f07b18..a8b21436e 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -179,7 +179,7 @@ public:
     lbool mus_mss_solver() {
         init();
         init_local();
-        enable_sls(m_asms);
+        sls();
         ptr_vector<expr> mcs;
         vector<ptr_vector<expr> > cores;
         while (m_lower < m_upper) {            
@@ -221,7 +221,7 @@ public:
     lbool mss_solver() {
         init();
         init_local();
-        enable_sls(m_asms);
+        sls();
         set_mus(false);
         ptr_vector<expr> mcs;
         lbool is_sat = l_true;
@@ -383,6 +383,14 @@ public:
         return m_asm2weight.find(e);
     }
 
+    void sls() {
+        vector<rational> ws;
+        for (unsigned i = 0; i < m_asms.size(); ++i) {
+            ws.push_back(get_weight(m_asms[i].get()));
+        }
+        enable_sls(m_asms, ws);
+    }
+
     rational split_core(ptr_vector<expr> const& core) {
 
         // find the minimal weight:
diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp
index be8e99c3a..6145d1e71 100644
--- a/src/opt/maxsls.cpp
+++ b/src/opt/maxsls.cpp
@@ -33,7 +33,7 @@ namespace opt {
         lbool operator()() {
             IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
             init();
-            enable_sls(m_soft);
+            enable_sls(m_soft, m_weights);
             lbool is_sat = s().check_sat(0, 0);
             if (is_sat == l_true) {
                 s().get_model(m_model);
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 44f898443..d084dc5b5 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -94,8 +94,8 @@ namespace opt {
         m_s.updt_params(p);
     }
 
-    void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft) {
-        m_c.enable_sls(soft, m_weights);
+    void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft, vector<rational> const& ws) {
+        m_c.enable_sls(soft, ws);
     }
 
     app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index ee275e7f6..54b2110b3 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -81,7 +81,7 @@ namespace opt {
         void set_mus(bool f);
         app* mk_fresh_bool(char const* name);
     protected:
-        void enable_sls(expr_ref_vector const& soft);
+        void enable_sls(expr_ref_vector const& soft, vector<rational> const& ws);
     };
 
     /**