mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

working on maxres

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-31 23:35:41 -07:00
parent 39414d8b8d
commit 6438c477b3
2 changed files with 22 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/opt/dual_maxres.cpp
View file

@ -64,6 +64,7 @@ class dual_maxres : public maxsmt_solver_base {
expr_ref_vector m_B; expr_ref_vector m_B;
expr_ref_vector m_asms; expr_ref_vector m_asms;
obj_map<expr, rational> m_asm2weight; obj_map<expr, rational> m_asm2weight;
obj_map<expr, expr*> m_soft2asm;
ptr_vector<expr> m_new_core; ptr_vector<expr> m_new_core;
mus m_mus; mus m_mus;
expr_ref_vector m_trail; expr_ref_vector m_trail;
@ -89,6 +90,11 @@ public:
void add_soft(expr* e, rational const& w) { void add_soft(expr* e, rational const& w) {
TRACE("opt", tout << mk_pp(e, m) << "\n";); TRACE("opt", tout << mk_pp(e, m) << "\n";);
expr_ref asum(m), fml(m); expr_ref asum(m), fml(m);
expr* f;
if (m_soft2asm.find(e, f)) {
m_asm2weight.find(f) += w;
return;
}
if (is_literal(e)) { if (is_literal(e)) {
asum = e; asum = e;
} }
@ -97,6 +103,7 @@ public:
fml = m.mk_iff(asum, e); fml = m.mk_iff(asum, e);
m_s->assert_expr(fml); m_s->assert_expr(fml);
} }
m_soft2asm.insert(e, asum);
new_assumption(asum, w); new_assumption(asum, w);
m_upper += w; m_upper += w;
} }
@ -461,6 +468,7 @@ public:
m_upper.reset(); m_upper.reset();
m_lower.reset(); m_lower.reset();
m_asm2weight.reset(); m_asm2weight.reset();
m_soft2asm.reset();
m_trail.reset(); m_trail.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
add_soft(m_soft[i].get(), m_weights[i]); add_soft(m_soft[i].get(), m_weights[i]);

16
src/opt/maxres.cpp
View file

@ -63,6 +63,12 @@ public:
TRACE("opt", tout << mk_pp(e, m) << "\n";); TRACE("opt", tout << mk_pp(e, m) << "\n";);
expr_ref asum(m), fml(m); expr_ref asum(m), fml(m);
app_ref cls(m); app_ref cls(m);
info inf(0,rational(0));
if (m_asm2info.find(e, inf)) {
inf.m_weight += w;
m_asm2info.insert(e, inf);
return;
}
cls = mk_cls(e); cls = mk_cls(e);
m_trail.push_back(cls); m_trail.push_back(cls);
if (is_literal(e)) { if (is_literal(e)) {
@ -104,15 +110,21 @@ public:
return l_undef; return l_undef;
} }
switch (is_sat) { switch (is_sat) {
case l_true: case l_true: {
m_s->get_model(m_model); m_s->get_model(m_model);
expr_ref tmp(m);
DEBUG_CODE(
for (unsigned i = 0; i < m_asms.size(); ++i) {
VERIFY(m_model->eval(m_asms[i].get(), tmp));
SASSERT(m.is_true(tmp));
});
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref tmp(m);
VERIFY(m_model->eval(m_soft[i].get(), tmp)); VERIFY(m_model->eval(m_soft[i].get(), tmp));
m_assignment[i] = m.is_true(tmp); m_assignment[i] = m.is_true(tmp);
} }
m_upper = m_lower; m_upper = m_lower;
return l_true; return l_true;
}
case l_undef: case l_undef:
return l_undef; return l_undef;
default: default: