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

working on maxsat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-14 10:00:21 +02:00
parent 04824d86df
commit 5f72325e99
2 changed files with 21 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/opt/fu_malik.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include "probe.h"
#include "tactic.h"
#include "smt_context.h"
#include "ast_pp.h"
/**
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
@ -290,8 +291,14 @@ namespace opt {
if (!m_soft.empty() && is_sat == l_true) {
solver::scoped_push _sp(s());
expr_ref tmp(m);
TRACE("opt",
tout << "soft constraints:\n";
for (unsigned i = 0; i < m_soft.size(); ++i) {
tout << mk_pp(m_soft[i].get(), m) << "\n";
});
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl());
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
@ -304,7 +311,7 @@ namespace opt {
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list of satisfying m_soft
// Get a list satisfying m_soft
s().get_model(m_model);
m_lower = m_upper;
m_assignment.reset();
@ -315,6 +322,7 @@ namespace opt {
m_assignment.push_back(m_orig_soft[i].get());
}
}
TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";);
}
}
// We are done and soft_constraints has

15
src/opt/opt_context.cpp
View file

@ -255,6 +255,14 @@ namespace opt {
terms[i] = m.mk_not(terms[i].get());
}
}
TRACE("opt",
tout << "Convert minimization " << mk_pp(orig_term, m) << "\n";
tout << "to maxsat: " << term << "\n";
for (unsigned i = 0; i < weights.size(); ++i) {
tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n";
}
tout << "offset: " << offset << "\n";
);
std::ostringstream out;
out << mk_pp(orig_term, m);
id = symbol(out.str().c_str());
@ -448,7 +456,7 @@ namespace opt {
out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
}
else {
out << "|-> " << get_lower(i) << "\n";
out << " |-> " << get_lower(i) << "\n";
}
}
}
@ -459,12 +467,12 @@ namespace opt {
case O_MAXSMT: {
symbol s = obj.m_id;
if (s != symbol::null) {
out << s << " : ";
out << s;
}
break;
}
default:
out << obj.m_term << " ";
out << obj.m_term;
break;
}
}
@ -477,6 +485,7 @@ namespace opt {
switch(obj.m_type) {
case O_MAXSMT: {
rational r = m_maxsmts.find(obj.m_id)->get_lower();
TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
if (obj.m_neg) r.neg();
r += obj.m_offset;
return inf_eps(r);