fix bug in sls

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

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);

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) {

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());

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);
+
     };
 
     /**

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; }
 
 

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;
+                    }
                 }
             }
         }