From b82a68f4d465d056392f344d681dd1c78eff8bc7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 24 Aug 2014 19:53:55 -0700
Subject: [PATCH] fix bug in sls

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/inc_sat_solver.cpp | 16 +++++++++++++++-
 src/opt/maxsls.cpp         |  1 +
 src/opt/maxsmt.cpp         |  4 ++++
 src/opt/maxsmt.h           |  2 ++
 src/opt/opt_context.h      |  1 +
 src/sat/sat_sls.cpp        |  6 ++++--
 6 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp
index 89f9e79fd..49315a895 100644
--- a/src/opt/inc_sat_solver.cpp
+++ b/src/opt/inc_sat_solver.cpp
@@ -228,11 +228,25 @@ private:
         r = internalize_assumptions(soft.size(), soft.c_ptr(), dep2asm);
         sat::literal_vector lits;
         svector<double> weights;
+        sat::literal lit;
 
         if (r == l_true) {
             for (unsigned i = 0; i < soft.size(); ++i) {
                 weights.push_back(m_weights[i].get_double());
-                lits.push_back(dep2asm.find(soft[i].get()));
+                expr* s = soft[i].get();
+                bool is_neg = m.is_not(s, s);
+                if (!dep2asm.find(s, lit)) {
+                    std::cout << "not found: " << mk_pp(s, m) << "\n";
+                    dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
+                    for (; it != end; ++it) {
+                        std::cout << mk_pp(it->m_key, m) << " " << it->m_value << "\n";
+                    }
+                    UNREACHABLE();
+                }
+                if (is_neg) {
+                    lit.neg();
+                }                        
+                lits.push_back(lit);
             }
             m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr());
             m_params.set_bool("optimize_model", true);
diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp
index 48fa48821..c679a6929 100644
--- a/src/opt/maxsls.cpp
+++ b/src/opt/maxsls.cpp
@@ -33,6 +33,7 @@ namespace opt {
         lbool operator()() {
             IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
             init();
+            set_enable_sls(true);
             enable_sls(m_soft, m_weights);
             lbool is_sat = s().check_sat(0, 0);
             if (is_sat == l_true) {
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index d084dc5b5..9fe704942 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -98,6 +98,10 @@ namespace opt {
         m_c.enable_sls(soft, ws);
     }
 
+    void maxsmt_solver_base::set_enable_sls(bool f) {
+        m_c.set_enable_sls(f);
+    }
+
     app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
         app* result = m.mk_fresh_const(name, m.mk_bool_sort());
         m_c.fm().insert(result->get_decl());
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index b3e17ad71..47b903e17 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -84,6 +84,8 @@ namespace opt {
         app* mk_fresh_bool(char const* name);
     protected:
         void enable_sls(expr_ref_vector const& soft, weights_t& ws);
+        void set_enable_sls(bool f);
+
     };
 
     /**
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 63ac13edc..5f3bd88cb 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -177,6 +177,7 @@ namespace opt {
         ast_manager& get_manager() { return this->m; }
         params_ref& params() { return m_params; }
         void enable_sls(expr_ref_vector const& soft, weights_t& weights);
+        void set_enable_sls(bool f) { m_enable_sls = f; }
         symbol const& maxsat_engine() const { return m_maxsat_engine; }
 
 
diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp
index 8f4e09173..3a520742e 100644
--- a/src/sat/sat_sls.cpp
+++ b/src/sat/sat_sls.cpp
@@ -387,8 +387,10 @@ namespace sat {
                     m_best_value = val;
                     m_best_model.reset();
                     m_best_model.append(m_model);
-                    IF_VERBOSE(0, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
-                    m_max_tries *= 2;
+                    IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";);
+                    if (i*2 > m_max_tries) {
+                        m_max_tries *= 2;
+                    }
                 }
             }
         }