mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
debugging lia2maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
370a4b66de
commit
ddb30c51b5
5 changed files with 104 additions and 65 deletions
|
|
@ -32,6 +32,7 @@ namespace opt {
|
|||
m_msolver = 0;
|
||||
m_s = &s;
|
||||
if (m_soft_constraints.empty()) {
|
||||
TRACE("opt", tout << "no constraints\n";);
|
||||
m_msolver = 0;
|
||||
is_sat = s.check_sat(0, 0);
|
||||
m_answer.reset();
|
||||
|
|
@ -75,29 +76,29 @@ namespace opt {
|
|||
return m_answer;
|
||||
}
|
||||
|
||||
inf_eps maxsmt::get_value() const {
|
||||
rational maxsmt::get_value() const {
|
||||
if (m_msolver) {
|
||||
return inf_eps(m_msolver->get_value());
|
||||
return m_msolver->get_value();
|
||||
}
|
||||
return inf_eps(m_upper);
|
||||
return m_upper;
|
||||
}
|
||||
|
||||
inf_eps maxsmt::get_lower() const {
|
||||
rational maxsmt::get_lower() const {
|
||||
rational r = m_lower;
|
||||
if (m_msolver) {
|
||||
rational q = m_msolver->get_lower();
|
||||
if (r < q) r = q;
|
||||
}
|
||||
return inf_eps(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
inf_eps maxsmt::get_upper() const {
|
||||
rational maxsmt::get_upper() const {
|
||||
rational r = m_upper;
|
||||
if (m_msolver) {
|
||||
rational q = m_msolver->get_upper();
|
||||
if (r > q) r = q;
|
||||
}
|
||||
return inf_eps(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
void maxsmt::update_lower(rational const& r) {
|
||||
|
|
|
|||
|
|
@ -74,9 +74,9 @@ namespace opt {
|
|||
rational weight(unsigned idx) const { return m_weights[idx]; }
|
||||
|
||||
void commit_assignment();
|
||||
inf_eps get_value() const;
|
||||
inf_eps get_lower() const;
|
||||
inf_eps get_upper() const;
|
||||
rational get_value() const;
|
||||
rational get_lower() const;
|
||||
rational get_upper() const;
|
||||
void update_lower(rational const& r);
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -209,8 +209,10 @@ namespace opt {
|
|||
}
|
||||
|
||||
bool context::is_maxsat(expr* fml, expr_ref_vector& terms,
|
||||
vector<rational>& weights, symbol& id, unsigned& index) {
|
||||
vector<rational>& weights, rational& offset,
|
||||
bool& neg, symbol& id, unsigned& index) {
|
||||
if (!is_app(fml)) return false;
|
||||
neg = false;
|
||||
app* a = to_app(fml);
|
||||
if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) {
|
||||
terms.append(a->get_num_args(), a->get_args());
|
||||
|
|
@ -219,25 +221,46 @@ namespace opt {
|
|||
return true;
|
||||
}
|
||||
app_ref term(m);
|
||||
if (is_minimize(fml, term, index)) {
|
||||
offset = rational::zero();
|
||||
if (is_minimize(fml, term, index) &&
|
||||
get_pb_sum(term, terms, weights, offset)) {
|
||||
TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";);
|
||||
rational coeff(0);
|
||||
// minimize 2*x + 3*y
|
||||
// <=>
|
||||
// (assert-soft (not x) 2)
|
||||
// (assert-soft (not y) 3)
|
||||
//
|
||||
if (get_pb_sum(term, terms, weights, coeff) && coeff.is_zero()) {
|
||||
for (unsigned i = 0; i < weights.size(); ++i) {
|
||||
if (!weights[i].is_pos()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < weights.size(); ++i) {
|
||||
if (weights[i].is_neg()) {
|
||||
offset += weights[i];
|
||||
weights[i].neg();
|
||||
}
|
||||
for (unsigned i = 0; i < terms.size(); ++i) {
|
||||
else {
|
||||
terms[i] = m.mk_not(terms[i].get());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
if (is_maximize(fml, term, index) &&
|
||||
get_pb_sum(term, terms, weights, offset)) {
|
||||
TRACE("opt", tout << "try to convert maximization" << mk_pp(term, m) << "\n";);
|
||||
// maximize 2*x + 3*y - z
|
||||
// <=>
|
||||
// (assert-soft x 2)
|
||||
// (assert-soft y 3)
|
||||
// (assert-soft (not z) 1)
|
||||
// offset := 6
|
||||
// maximize = offset - penalty
|
||||
//
|
||||
for (unsigned i = 0; i < weights.size(); ++i) {
|
||||
if (weights[i].is_neg()) {
|
||||
weights[i].neg();
|
||||
terms[i] = m.mk_not(terms[i].get());
|
||||
}
|
||||
offset += weights[i];
|
||||
}
|
||||
neg = true;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
|
@ -281,9 +304,11 @@ namespace opt {
|
|||
app_ref tr(m);
|
||||
expr_ref_vector terms(m);
|
||||
vector<rational> weights;
|
||||
rational offset;
|
||||
unsigned index;
|
||||
symbol id;
|
||||
if (is_maxsat(fml, terms, weights, id, index)) {
|
||||
bool neg;
|
||||
if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
|
||||
objective& obj = m_objectives[index];
|
||||
if (obj.m_type != O_MAXSMT) {
|
||||
// change from maximize/minimize.
|
||||
|
|
@ -298,6 +323,9 @@ namespace opt {
|
|||
SASSERT(obj.m_id == id);
|
||||
obj.m_terms.reset();
|
||||
obj.m_terms.append(terms);
|
||||
obj.m_offset = offset;
|
||||
obj.m_neg = neg;
|
||||
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
|
||||
}
|
||||
else if (is_maximize(fml, tr, index)) {
|
||||
m_objectives[index].m_term = tr;
|
||||
|
|
@ -390,51 +418,47 @@ namespace opt {
|
|||
void context::display_assignment(std::ostream& out) {
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
switch(obj.m_type) {
|
||||
case O_MAXSMT: {
|
||||
symbol s = obj.m_id;
|
||||
if (s != symbol::null) {
|
||||
out << s << " : ";
|
||||
}
|
||||
maxsmt* ms = m_maxsmts.find(s);
|
||||
out << ms->get_value() << "\n";
|
||||
break;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
display_objective(out, obj);
|
||||
out << get_upper(i) << "\n";
|
||||
}
|
||||
m_optsmt.display_assignment(out);
|
||||
}
|
||||
|
||||
void context::display_range_assignment(std::ostream& out) {
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
switch(obj.m_type) {
|
||||
case O_MAXSMT: {
|
||||
symbol s = obj.m_id;
|
||||
if (s != symbol::null) {
|
||||
out << s << " : ";
|
||||
}
|
||||
maxsmt* ms = m_maxsmts.find(s);
|
||||
out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n";
|
||||
break;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
display_objective(out, obj);
|
||||
out << " [" << get_lower(i) << ":" << get_upper(i) << "]\n";
|
||||
}
|
||||
m_optsmt.display_range_assignment(out);
|
||||
}
|
||||
|
||||
void context::display_objective(std::ostream& out, objective const& obj) const {
|
||||
switch(obj.m_type) {
|
||||
case O_MAXSMT: {
|
||||
symbol s = obj.m_id;
|
||||
if (s != symbol::null) {
|
||||
out << s << " : ";
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
out << obj.m_term << " ";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
expr_ref context::get_lower(unsigned idx) {
|
||||
if (idx > m_objectives.size()) {
|
||||
throw default_exception("index out of bounds");
|
||||
}
|
||||
objective const& obj = m_objectives[idx];
|
||||
switch(obj.m_type) {
|
||||
case O_MAXSMT:
|
||||
return to_expr(m_maxsmts.find(obj.m_id)->get_lower());
|
||||
case O_MAXSMT: {
|
||||
rational r = m_maxsmts.find(obj.m_id)->get_lower();
|
||||
if (obj.m_neg) r.neg();
|
||||
r += obj.m_offset;
|
||||
return to_expr(inf_eps(r));
|
||||
}
|
||||
case O_MINIMIZE:
|
||||
case O_MAXIMIZE:
|
||||
return to_expr(m_optsmt.get_lower(obj.m_index));
|
||||
|
|
@ -450,8 +474,12 @@ namespace opt {
|
|||
}
|
||||
objective const& obj = m_objectives[idx];
|
||||
switch(obj.m_type) {
|
||||
case O_MAXSMT:
|
||||
return to_expr(m_maxsmts.find(obj.m_id)->get_upper());
|
||||
case O_MAXSMT: {
|
||||
rational r = m_maxsmts.find(obj.m_id)->get_upper();
|
||||
if (obj.m_neg) r.neg();
|
||||
r += obj.m_offset;
|
||||
return to_expr(inf_eps(r));
|
||||
}
|
||||
case O_MINIMIZE:
|
||||
case O_MAXIMIZE:
|
||||
return to_expr(m_optsmt.get_upper(obj.m_index));
|
||||
|
|
|
|||
|
|
@ -49,6 +49,8 @@ namespace opt {
|
|||
app_ref m_term; // for maximize, minimize term
|
||||
expr_ref_vector m_terms; // for maxsmt
|
||||
vector<rational> m_weights; // for maxsmt
|
||||
rational m_offset; // for maxsmt
|
||||
bool m_neg; // negate
|
||||
symbol m_id; // for maxsmt
|
||||
unsigned m_index; // for maximize/minimize index
|
||||
|
||||
|
|
@ -56,6 +58,8 @@ namespace opt {
|
|||
m_type(is_max?O_MAXIMIZE:O_MINIMIZE),
|
||||
m_term(t),
|
||||
m_terms(t.get_manager()),
|
||||
m_offset(0),
|
||||
m_neg(false),
|
||||
m_id(),
|
||||
m_index(idx)
|
||||
{}
|
||||
|
|
@ -64,6 +68,8 @@ namespace opt {
|
|||
m_type(O_MAXSMT),
|
||||
m_term(m),
|
||||
m_terms(m),
|
||||
m_offset(0),
|
||||
m_neg(false),
|
||||
m_id(id),
|
||||
m_index(0)
|
||||
{}
|
||||
|
|
@ -119,7 +125,8 @@ namespace opt {
|
|||
bool is_maximize(expr* fml, app_ref& term, unsigned& index);
|
||||
bool is_minimize(expr* fml, app_ref& term, unsigned& index);
|
||||
bool is_maxsat(expr* fml, expr_ref_vector& terms,
|
||||
vector<rational>& weights, symbol& id, unsigned& index);
|
||||
vector<rational>& weights, rational& offset, bool& neg,
|
||||
symbol& id, unsigned& index);
|
||||
expr* mk_maximize(unsigned index, app* t);
|
||||
expr* mk_minimize(unsigned index, app* t);
|
||||
expr* mk_maxsat(unsigned index, unsigned num_fmls, expr* const* fmls);
|
||||
|
|
@ -132,6 +139,8 @@ namespace opt {
|
|||
|
||||
opt_solver& get_solver();
|
||||
|
||||
void display_objective(std::ostream& out, objective const& obj) const;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -218,12 +218,15 @@ namespace smt {
|
|||
if (m_min_cost_atom) {
|
||||
lits.push_back(~literal(m_min_cost_bv));
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "block: " << m_costs.size() << " " << lits.size() << " " << m_min_cost << "\n";);
|
||||
IF_VERBOSE(2, for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
verbose_stream() << lits[i] << " ";
|
||||
}
|
||||
verbose_stream() << "\n";
|
||||
);
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "block: ";
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
ctx.literal2expr(lits[i], tmp);
|
||||
verbose_stream() << tmp << " ";
|
||||
}
|
||||
verbose_stream() << "\n";
|
||||
);
|
||||
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (is_final && m_cost < m_min_cost) {
|
||||
|
|
@ -312,6 +315,7 @@ namespace opt {
|
|||
*/
|
||||
|
||||
lbool operator()() {
|
||||
TRACE("opt", tout << "weighted maxsat\n";);
|
||||
smt::theory_weighted_maxsat& wth = ensure_theory();
|
||||
lbool result;
|
||||
{
|
||||
|
|
@ -319,11 +323,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
wth.assert_weighted(m_soft[i].get(), m_weights[i]);
|
||||
}
|
||||
#if 1
|
||||
result = s.check_sat_core(0,0);
|
||||
#else
|
||||
result = iterative_weighted_maxsat(s, *wth);
|
||||
#endif
|
||||
|
||||
wth.get_assignment(m_assignment);
|
||||
if (!m_assignment.empty() && result == l_false) {
|
||||
|
|
@ -331,6 +331,7 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
m_upper = wth.get_min_cost();
|
||||
TRACE("opt", tout << "min cost: " << m_upper << "\n";);
|
||||
wth.reset();
|
||||
return result;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue