mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix bug in handling of repeated soft constraints. #815

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-11 10:19:57 +01:00
parent 0765eea486
commit 2307a7ffa7
5 changed files with 40 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/opt/maxres.cpp
View file

@ -805,8 +805,9 @@ public:
lbool init_local() {
m_lower.reset();
m_trail.reset();
lbool is_sat = l_true;
obj_map<expr, rational> new_soft;
lbool is_sat = find_mutexes(new_soft);
is_sat = find_mutexes(new_soft);
if (is_sat != l_true) {
return is_sat;
}

11
src/opt/maxsmt.cpp
View file

@ -333,8 +333,15 @@ namespace opt {
TRACE("opt", tout << mk_pp(f, m) << " weight: " << w << "\n";);
SASSERT(m.is_bool(f));
SASSERT(w.is_pos());
m_soft_constraints.push_back(f);
m_weights.push_back(w);
unsigned index = 0;
if (m_soft_constraint_index.find(f, index)) {
m_weights[index] += w;
}
else {
m_soft_constraint_index.insert(f, m_weights.size());
m_soft_constraints.push_back(f);
m_weights.push_back(w);
}
m_upper += w;
}

2
src/opt/maxsmt.h
View file

@ -120,6 +120,7 @@ namespace opt {
unsigned m_index;
scoped_ptr<maxsmt_solver_base> m_msolver;
expr_ref_vector m_soft_constraints;
obj_map<expr, unsigned> m_soft_constraint_index;
expr_ref_vector m_answer;
vector<rational> m_weights;
rational m_lower;
@ -138,7 +139,6 @@ namespace opt {
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }
void commit_assignment();
rational get_value() const;
rational get_lower() const;
rational get_upper() const;
void update_lower(rational const& r);

27
src/opt/opt_context.cpp
View file

@ -360,6 +360,7 @@ namespace opt {
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
DEBUG_CODE(if (result == l_true) validate_maxsat(id););
return result;
}
@ -1448,6 +1449,32 @@ namespace opt {
return out.str();
}
void context::validate_maxsat(symbol const& id) {
maxsmt& ms = *m_maxsmts.find(id);
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
if (obj.m_id == id) {
SASSERT(obj.m_type == O_MAXSMT);
rational value(0);
expr_ref val(m);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
bool evaluated = m_model->eval(obj.m_terms[i], val);
SASSERT(evaluated);
CTRACE("opt", evaluated && !m.is_true(val) && !m.is_false(val), tout << mk_pp(obj.m_terms[i], m) << " " << val << "\n";);
CTRACE("opt", !evaluated, tout << mk_pp(obj.m_terms[i], m) << "\n";);
if (evaluated && !m.is_true(val)) {
value += obj.m_weights[i];
}
// TBD: check that optimal was not changed.
}
value = obj.m_adjust_value(value);
rational value0 = ms.get_lower();
TRACE("opt", tout << "value " << value << " " << value0 << "\n";);
SASSERT(value == value0);
}
}
}
void context::validate_lex() {
rational r1;
expr_ref val(m);

1
src/opt/opt_context.h
View file

@ -291,6 +291,7 @@ namespace opt {
void validate_lex();
void validate_maxsat(symbol const& id);
void display_benchmark();