fix sls based on pkb120

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

src/opt/opt_sls_solver.h

@@ -194,8 +194,13 @@ namespace opt {
         void pbsls_opt() {
             #pragma omp critical (sls_solver)
             {
+                if (m_pbsls) {
+                    m_pbsls->reset();
+                }
+                else {
                     m_pbsls = alloc(smt::pb_sls, m);
                 }
+            }
             m_pbsls->set_model(m_model);
             m_pbsls->updt_params(m_params);
             for (unsigned i = 0; i < m_solver->get_num_assertions(); ++i) {

src/opt/pb_sls.cpp

@@ -130,7 +130,24 @@ namespace smt {
             one(mgr)
         {
             init_max_flips();
+        }
+
+        ~imp() {
+        }
+
+        void reset() {
+            init_max_flips();
             m_non_greedy_percent = 30;
+            m_decl2var.reset();
+            m_var2decl.reset();
+            m_assignment.reset();
+            m_hard_occ.reset();
+            m_soft_occ.reset();
+            m_clauses.reset();
+            m_orig_clauses.reset();
+            m_soft.reset();
+            m_weights.reset();
+            m_trail.reset();
             m_decl2var.insert(m.mk_true(), 0);
             m_var2decl.push_back(m.mk_true());
             m_assignment.push_back(true);
@@ -139,9 +156,6 @@ namespace smt {
             one = mpz(1);
         }
 
-        ~imp() {
-        }
-
         void init_max_flips() {
             m_max_flips = 200;
         }
@@ -635,11 +649,36 @@ namespace smt {
             m_rewrite(_f, tmp);
             if (!is_app(tmp)) return false;            
             app* f = to_app(tmp);
+            expr* f2;
             unsigned sz = f->get_num_args();
             expr* const* args = f->get_args();
             literal lit;
             rational coeff, k;
-            if (pb.is_ge(f) || pb.is_eq(f)) {
+            if (m.is_not(f, f2) && pb.is_ge(f2)) {
+                // ~(ax+by >= k) 
+                // <=>
+                // ax + by < k
+                // <=>
+                // -ax - by >= -k + 1
+                // <=>
+                // a(1-x) + b(1-y) >= -k + a + b + 1
+                sz = to_app(f2)->get_num_args();
+                args = to_app(f2)->get_args();
+                k = pb.get_k(f2);
+                SASSERT(k.is_int());
+                k.neg();
+                k += rational::one();
+                expr_ref_vector args(m);
+                vector<rational> coeffs;
+                for (unsigned i = 0; i < sz; ++i) {
+                    args.push_back(m.mk_not(to_app(f2)->get_arg(i)));
+                    coeffs.push_back(pb.get_coeff(f2, i));
+                    k += pb.get_coeff(f2, i);
+                }
+                tmp = pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
+                return compile_clause(tmp, cls);
+            }
+            else if (pb.is_ge(f) || pb.is_eq(f)) {
                 k = pb.get_k(f);
                 SASSERT(k.is_int());
                 cls.m_k = k.to_mpq().numerator();
@@ -720,6 +759,9 @@ namespace smt {
     void pb_sls::get_model(model_ref& mdl) {
         m_imp->get_model(mdl);
     }
+    void pb_sls::reset() {
+        m_imp->reset();
+    }
     bool pb_sls::soft_holds(unsigned index) {
         return m_imp->soft_holds(index);
     }

src/opt/pb_sls.h

@@ -42,6 +42,7 @@ namespace smt {
         void collect_statistics(::statistics& st) const;
         void get_model(model_ref& mdl);
         void updt_params(params_ref& p);
+        void reset();
     };
 
 

src/opt/weighted_maxsat.cpp

@@ -621,6 +621,7 @@ namespace opt {
                     }                     
                     TRACE("opt", tout << "new upper: " << m_upper << "\n";);
                     IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";);
+                    
                     fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
                     was_sat = true;
                 }