Merge branch 'master' of https://github.com/z3prover/z3

src/api/python/z3/z3.py

@@ -5340,7 +5340,7 @@ class Goal(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
+    def __deepcopy__(self, memo={}):
         return self.translate(self.ctx)
 
     def simplify(self, *arguments, **keywords):
@@ -5528,7 +5528,7 @@ class AstVector(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
+    def __deepcopy__(self, memo={}):
         return self.translate(self.ctx)
 
     def __repr__(self):
@@ -5872,7 +5872,7 @@ class FuncInterp(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
+    def __deepcopy__(self, memo={}):
         return self.translate(self.ctx)
 
     def as_list(self):
@@ -6168,7 +6168,7 @@ class ModelRef(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
+    def __deepcopy__(self, memo={}):
         return self.translate(self.ctx)
 
 def Model(ctx = None):
@@ -6786,7 +6786,7 @@ class Solver(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
+    def __deepcopy__(self, memo={}):
         return self.translate(self.ctx)
 
     def sexpr(self):

src/opt/maxlex.cpp

@@ -26,10 +26,6 @@ Author:
 namespace opt {
 
     bool is_maxlex(weights_t & _ws) {
-        // disable for now
-#if true
-        return false;
-#else
         vector<rational> ws(_ws);
         std::sort(ws.begin(), ws.end());
         ws.reverse();
@@ -42,7 +38,6 @@ namespace opt {
             sum -= w;
         }
         return true;
-#endif
     }
 
     class maxlex : public maxsmt_solver_base {
@@ -85,21 +80,23 @@ namespace opt {
         }
 
         void update_assignment(model_ref & mdl) {
-            bool prefix_defined = true;
+            bool first_undef = true, second_undef = false;
             for (auto & soft : m_soft) {
-                if (!prefix_defined) {
+                if (first_undef && soft.value != l_undef) {
-                    set_value(soft, l_undef);
                     continue;
                 }
-                switch (soft.value) {
+                first_undef = false;
-                case l_undef:
+                if (soft.value != l_false) {
-                    prefix_defined = mdl->is_true(soft.s);
+                    lbool v = mdl->is_true(soft.s) ? l_true : l_undef;;
-                    set_value(soft, prefix_defined ? l_true : l_undef);
+                    if (v == l_undef) {
-                    break;
+                        second_undef = true;
-                case l_true:
+                    }
-                    break;
+                    if (second_undef) {
-                case l_false:
+                        soft.set_value(v);
-                    break;
+                    }
+                    else {
+                        set_value(soft, v); // also update constraints
+                    }
                 }
             }
             update_bounds();
@@ -108,15 +105,9 @@ namespace opt {
         void update_bounds() {
             m_lower.reset();
             m_upper.reset();
-            bool prefix_defined = true;
             for (auto & soft : m_soft) {
-                if (!prefix_defined) {
-                    m_upper += soft.weight;
-                    continue;
-                }
                 switch (soft.value) {
                 case l_undef:
-                    prefix_defined = false;
                     m_upper += soft.weight;
                     break;
                 case l_true:
@@ -131,6 +122,9 @@ namespace opt {
         }
 
         void init() {
+            for (auto & soft : m_soft) {
+                soft.set_value(l_undef);
+            }
             model_ref mdl;
             s().get_model(mdl);
             update_assignment(mdl);           
@@ -216,9 +210,20 @@ namespace opt {
                                 // a, b is unsat, a, not b is unsat -> a is unsat
                                 // b is unsat, a, not b is unsat -> not a, not b
                                 set_value(soft, l_false);
+                                // core1 = { b }
+                                // core2 = { a, not b }
                                 if (!core.contains(a)) {
                                     set_value(soft2, l_false);
                                 }
+                                else {
+                                    // core1 = { a, b}
+                                    // core2 = { not_b }
+                                    core.reset();
+                                    s().get_unsat_core(core);
+                                    if (!core.contains(a)) {
+                                        set_value(soft2, l_true);
+                                    }
+                                }
                                 update_bounds();
                                 break;
                             case l_undef:
@@ -238,6 +243,47 @@ namespace opt {
             return l_true;
         }
 
+        // every time probing whether to include soft_i, 
+        // include suffix that is known to be assignable to T
+        lbool maxlexN() {
+            unsigned sz = m_soft.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                auto& soft = m_soft[i];
+                if (soft.value != l_undef) {
+                    continue;
+                }
+                expr_ref_vector asms(m);
+                asms.push_back(soft.s);
+                for (unsigned j = i + 1; j < sz; ++j) {
+                    auto& soft2 = m_soft[j];
+                    if (soft2.value == l_true) {
+                        asms.push_back(soft2.s);                    
+                    }
+                }
+                lbool is_sat = s().check_sat(asms);
+                switch (is_sat) {
+                case l_true:
+                    update_assignment();
+                    SASSERT(soft.value == l_true);
+                    break;
+                case l_false:
+                    set_value(soft, l_false);
+                    for (unsigned j = i + 1; j < sz; ++j) {
+                        auto& soft2 = m_soft[j];
+                        if (soft2.value != l_true) {
+                            break;
+                        }                        
+                        assert_value(soft2);
+                    }
+                    update_bounds();
+                    break;
+                case l_undef:
+                    return l_undef;
+                }
+            }
+            return l_true;
+        }
+
     public:
 
         maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
@@ -251,7 +297,7 @@ namespace opt {
         
         lbool operator()() override {
             init();            
-            return maxlex1();
+            return maxlexN();
         }
 
 

src/opt/maxsmt.cpp

@@ -232,10 +232,11 @@ namespace opt {
     lbool maxsmt::operator()() {
         lbool is_sat = l_undef;
         m_msolver = nullptr;
+        opt_params optp(m_params);
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
-        if (is_maxlex(m_weights)) {
+        if (optp.maxlex_enable() && is_maxlex(m_weights)) {
             m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
         }
         else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            

src/opt/opt_params.pyg

@@ -14,6 +14,7 @@ def_module_params('opt',
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
                           ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
+                          ('maxlex.enable', BOOL, False, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
                           ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
                           ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
                           ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),