From a785ffe0bae5c22454b638045310a78954f3b16a Mon Sep 17 00:00:00 2001 From: Alcides Fonseca Date: Fri, 25 Jan 2019 14:42:22 +0000 Subject: [PATCH 1/3] Updated deepcopy to the latest Python API --- src/api/python/z3/z3.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 65f634b6b..556c920f6 100644 --- a/src/api/python/z3/z3.py +++ b/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): From 1ed68906faab97f8022e61b41caf24b71cb4d7b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jan 2019 08:23:41 -0800 Subject: [PATCH 2/3] fix debug assertion code, make maxlex optional Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 9 ++------- src/opt/maxsmt.cpp | 3 ++- src/opt/opt_params.pyg | 1 + 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 1604db161..30b4dbfc6 100644 --- a/src/opt/maxlex.cpp +++ b/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 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 { @@ -141,7 +136,7 @@ namespace opt { if (soft.value == l_true) { continue; } - SASSERT(soft.value() == l_undef); + SASSERT(soft.value == l_undef); expr* a = soft.s; lbool is_sat = s().check_sat(1, &a); switch (is_sat) { @@ -169,7 +164,7 @@ namespace opt { if (soft.value != l_undef) { continue; } - SASSERT(soft.value() == l_undef); + SASSERT(soft.value == l_undef); if (i + 1 == sz) { expr* a = soft.s; lbool is_sat = s().check_sat(1, &a); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 329e7979c..5441c4def 100644 --- a/src/opt/maxsmt.cpp +++ b/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) { diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 623eefea3..4235deb3d 100644 --- a/src/opt/opt_params.pyg +++ b/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'), From 121211a51cec7bf67dcbd87e8c99658b80856d8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jan 2019 20:01:38 -0800 Subject: [PATCH 3/3] maxlexN Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 89 ++++++++++++++++++++++++++++++++++++---------- 1 file changed, 70 insertions(+), 19 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 30b4dbfc6..1ee9db090 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -80,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) { - set_value(soft, l_undef); + if (first_undef && soft.value != l_undef) { continue; } - switch (soft.value) { - case l_undef: - prefix_defined = mdl->is_true(soft.s); - set_value(soft, prefix_defined ? l_true : l_undef); - break; - case l_true: - break; - case l_false: - break; + first_undef = false; + if (soft.value != l_false) { + lbool v = mdl->is_true(soft.s) ? l_true : l_undef;; + if (v == l_undef) { + second_undef = true; + } + if (second_undef) { + soft.set_value(v); + } + else { + set_value(soft, v); // also update constraints + } } } update_bounds(); @@ -103,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: @@ -126,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); @@ -211,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: @@ -233,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): @@ -246,7 +297,7 @@ namespace opt { lbool operator()() override { init(); - return maxlex1(); + return maxlexN(); }