mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

allow negative weights for weighted maxsat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-02 10:21:58 -07:00
parent 57ebf7bd38
commit b2db2f1eb6
2 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -6712,7 +6712,7 @@ class Optimize(Z3PPObject):
""" """
if _is_int(weight): if _is_int(weight):
weight = "%d" % weight weight = "%d" % weight
elif isinstance(weight, (float, double)): elif isinstance(weight, float):
weight = "%f" % weight weight = "%f" % weight
if not isinstance(weight, str): if not isinstance(weight, str):
raise Z3Exception("weight should be a string or an integer") raise Z3Exception("weight should be a string or an integer")

19
src/opt/opt_context.cpp
View file

@ -90,9 +90,6 @@ namespace opt {
} }
unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) { unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) {
if (w.is_neg()) {
throw default_exception("Negative weight supplied. Weight should be non-negative");
}
if (!m.is_bool(f)) { if (!m.is_bool(f)) {
throw default_exception("Soft constraint should be Boolean"); throw default_exception("Soft constraint should be Boolean");
} }
@ -102,7 +99,7 @@ namespace opt {
} }
SASSERT(m_indices.contains(id)); SASSERT(m_indices.contains(id));
unsigned idx = m_indices[id]; unsigned idx = m_indices[id];
if (w.is_pos()) { if (!w.is_zero()) {
m_objectives[idx].m_terms.push_back(f); m_objectives[idx].m_terms.push_back(f);
m_objectives[idx].m_weights.push_back(w); m_objectives[idx].m_weights.push_back(w);
m_objectives_term_trail.push_back(idx); m_objectives_term_trail.push_back(idx);
@ -743,16 +740,22 @@ namespace opt {
app* a = to_app(fml); app* a = to_app(fml);
if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) { if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) {
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* arg = a->get_arg(i); expr_ref arg(a->get_arg(i), m);
if (m.is_true(arg)) { rational weight = m_objectives[index].m_weights[i];
if (weight.is_neg()) {
weight.neg();
arg = mk_not(m, arg);
offset -= weight;
}
if (m.is_true(arg) || weight.is_zero()) {
// skip // skip
} }
else if (m.is_false(arg)) { else if (m.is_false(arg)) {
offset += m_objectives[index].m_weights[i]; offset += weight;
} }
else { else {
terms.push_back(arg); terms.push_back(arg);
weights.push_back(m_objectives[index].m_weights[i]); weights.push_back(weight);
} }
} }
id = m_objectives[index].m_id; id = m_objectives[index].m_id;