From 04824d86dfc45988293ca551f01771b79fb5b589 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Dec 2013 09:37:42 +0200 Subject: [PATCH] fixes to model generation of weighted maxsat Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 21 +++++++++++---------- src/opt/fu_malik.h | 4 ++-- src/opt/maxsmt.cpp | 2 +- src/opt/maxsmt.h | 5 ++--- src/opt/opt_context.cpp | 31 ++++++++++++++++++++----------- src/opt/opt_context.h | 6 ++++-- src/opt/opt_solver.h | 2 +- src/opt/weighted_maxsat.cpp | 12 ++++-------- 8 files changed, 45 insertions(+), 38 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 7877ec7b0..af700168f 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -43,7 +43,7 @@ namespace opt { struct fu_malik::imp { ast_manager& m; - solver & m_original_solver; + opt_solver & m_opt_solver; ref m_s; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; @@ -55,9 +55,9 @@ namespace opt { bool m_use_new_bv_solver; - imp(ast_manager& m, solver& s, expr_ref_vector const& soft): + imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft): m(m), - m_original_solver(s), + m_opt_solver(s), m_s(&s), m_soft(soft), m_orig_soft(soft), @@ -98,7 +98,7 @@ namespace opt { } void collect_statistics(statistics& st) const { - if (m_s != &m_original_solver) { + if (m_s != &m_opt_solver) { m_s->collect_statistics(st); } } @@ -215,9 +215,11 @@ namespace opt { if (!found) { continue; } - expr_ref block_var(m), tmp(m); + app_ref block_var(m), tmp(m); block_var = m.mk_fresh_const("block_var", m.mk_bool_sort()); m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); + m_opt_solver.mc().insert(block_var->get_decl()); + m_opt_solver.mc().insert(to_app(m_aux[i].get())->get_decl()); m_soft[i] = m.mk_or(m_soft[i].get(), block_var); block_vars.push_back(block_var); tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); @@ -253,8 +255,7 @@ namespace opt { } void set_solver() { - opt_solver & opt_s = opt_solver::to_opt(m_original_solver); - if (opt_s.dump_benchmarks()) + if (m_opt_solver.dump_benchmarks()) return; solver& current_solver = s(); @@ -268,11 +269,11 @@ namespace opt { probe_ref p = mk_is_qfbv_probe(); bool all_bv = (*p)(g).is_true(); if (all_bv) { - smt::context & ctx = opt_s.get_context(); + smt::context & ctx = m_opt_solver.get_context(); tactic_ref t = mk_qfbv_tactic(m, ctx.get_params()); // The new SAT solver hasn't supported unsat core yet m_s = mk_tactic2solver(m, t.get()); - SASSERT(m_s != &m_original_solver); + SASSERT(m_s != &m_opt_solver); for (unsigned i = 0; i < num_assertions; ++i) { m_s->assert_expr(current_solver.get_assertion(i)); } @@ -327,7 +328,7 @@ namespace opt { }; - fu_malik::fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) { + fu_malik::fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints) { m_imp = alloc(imp, m, s, soft_constraints); } fu_malik::~fu_malik() { diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h index 2cd4e146d..df6c14a55 100644 --- a/src/opt/fu_malik.h +++ b/src/opt/fu_malik.h @@ -24,7 +24,7 @@ Notes: #ifndef _OPT_FU_MALIK_H_ #define _OPT_FU_MALIK_H_ -#include "solver.h" +#include "opt_solver.h" #include "maxsmt.h" namespace opt { @@ -33,7 +33,7 @@ namespace opt { struct imp; imp* m_imp; public: - fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints); + fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints); virtual ~fu_malik(); virtual lbool operator()(); virtual rational get_lower() const; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 1d1a65e5c..369b26782 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -26,7 +26,7 @@ Notes: namespace opt { - lbool maxsmt::operator()(solver& s) { + lbool maxsmt::operator()(opt_solver& s) { lbool is_sat; m_answer.reset(); m_msolver = 0; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 92744baaf..b6d27f379 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -19,7 +19,6 @@ Notes: #ifndef _OPT_MAXSMT_H_ #define _OPT_MAXSMT_H_ -#include "solver.h" #include "opt_solver.h" #include "statistics.h" @@ -44,7 +43,7 @@ namespace opt { class maxsmt { ast_manager& m; - solver* m_s; + opt_solver* m_s; volatile bool m_cancel; expr_ref_vector m_soft_constraints; expr_ref_vector m_answer; @@ -57,7 +56,7 @@ namespace opt { public: maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {} - lbool operator()(solver& s); + lbool operator()(opt_solver& s); void set_cancel(bool f); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 453af018e..be0e6010d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -35,7 +35,8 @@ namespace opt { context::context(ast_manager& m): m(m), m_hard_constraints(m), - m_optsmt(m) + m_optsmt(m), + m_objective_refs(m) { m_params.set_bool("model", true); m_params.set_bool("unsat_core", true); @@ -119,16 +120,16 @@ namespace opt { lbool context::execute_min_max(unsigned index, bool committed) { lbool result = m_optsmt.lex(index); - if (result == l_true) m_optsmt.get_model(m_model); if (committed) m_optsmt.commit_assignment(index); + if (committed && result == l_true) m_optsmt.get_model(m_model); return result; } lbool context::execute_maxsat(symbol const& id, bool committed) { maxsmt& ms = *m_maxsmts.find(id); lbool result = ms(get_solver()); - if (result == l_true) ms.get_model(m_model); if (committed) ms.commit_assignment(); + if (committed && result == l_true) ms.get_model(m_model); return result; } @@ -202,19 +203,21 @@ namespace opt { } } - bool context::is_maximize(expr* fml, app_ref& term, unsigned& index) { + bool context::is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) { if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && m_objectives[index].m_type == O_MAXIMIZE) { term = to_app(to_app(fml)->get_arg(0)); + orig_term = m_objective_orig.find(to_app(fml)->get_decl()); return true; } return false; } - bool context::is_minimize(expr* fml, app_ref& term, unsigned& index) { + bool context::is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) { if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && m_objectives[index].m_type == O_MINIMIZE) { term = to_app(to_app(fml)->get_arg(0)); + orig_term = m_objective_orig.find(to_app(fml)->get_decl()); return true; } return false; @@ -233,8 +236,9 @@ namespace opt { return true; } app_ref term(m); + expr* orig_term; offset = rational::zero(); - if (is_minimize(fml, term, index) && + if (is_minimize(fml, term, orig_term, index) && get_pb_sum(term, terms, weights, offset)) { TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";); // minimize 2*x + 3*y @@ -252,11 +256,11 @@ namespace opt { } } std::ostringstream out; - out << term; + out << mk_pp(orig_term, m); id = symbol(out.str().c_str()); return true; } - if (is_maximize(fml, term, index) && + if (is_maximize(fml, term, orig_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 @@ -276,7 +280,7 @@ namespace opt { } neg = true; std::ostringstream out; - out << term; + out << mk_pp(orig_term, m); id = symbol(out.str().c_str()); return true; } @@ -297,6 +301,10 @@ namespace opt { } func_decl* f = m.mk_fresh_func_decl(name,"", domain.size(), domain.c_ptr(), m.mk_bool_sort()); m_objective_fns.insert(f, index); + m_objective_refs.push_back(f); + if (sz > 0) { + m_objective_orig.insert(f, args[0]); + } return m.mk_app(f, sz, args); } @@ -317,6 +325,7 @@ namespace opt { void context::from_fmls(expr_ref_vector const& fmls) { m_hard_constraints.reset(); + expr* orig_term; for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i]; app_ref tr(m); @@ -345,10 +354,10 @@ namespace opt { obj.m_neg = neg; TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";); } - else if (is_maximize(fml, tr, index)) { + else if (is_maximize(fml, tr, orig_term, index)) { m_objectives[index].m_term = tr; } - else if (is_minimize(fml, tr, index)) { + else if (is_minimize(fml, tr, orig_term, index)) { m_objectives[index].m_term = tr; } else { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 50f69d59e..ebf6eed0a 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -86,6 +86,8 @@ namespace opt { model_ref m_model; model_converter_ref m_model_converter; obj_map m_objective_fns; + obj_map m_objective_orig; + func_decl_ref_vector m_objective_refs; public: context(ast_manager& m); ~context(); @@ -124,8 +126,8 @@ namespace opt { void normalize(); void internalize(); - bool is_maximize(expr* fml, app_ref& term, unsigned& index); - bool is_minimize(expr* fml, app_ref& term, unsigned& index); + bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index); + bool is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index); bool is_maxsat(expr* fml, expr_ref_vector& terms, vector& weights, rational& offset, bool& neg, symbol& id, unsigned& index); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 844e276ba..9d452193e 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -83,7 +83,7 @@ namespace opt { expr_ref mk_gt(unsigned obj_index, inf_eps const& val); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); - model_converter& mc() { return m_fm; } + filter_model_converter& mc() { return m_fm; } static opt_solver& to_opt(solver& s); bool dump_benchmarks(); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 97de77219..787625136 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -35,7 +35,6 @@ namespace smt { rational m_min_cost; // current maximal cost assignment. u_map m_bool2var; // bool_var -> theory_var svector m_var2bool; // theory_var -> bool_var - model_ref m_model; public: theory_weighted_maxsat(ast_manager& m): theory(m.mk_family_id("weighted_maxsat")), @@ -187,7 +186,6 @@ namespace smt { m_bool2var.reset(); m_var2bool.reset(); m_min_cost_atom = 0; - m_model = 0; } virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_weighted_maxsat, new_ctx->get_manager()); } @@ -196,9 +194,6 @@ namespace smt { virtual void new_eq_eh(theory_var v1, theory_var v2) { } virtual void new_diseq_eh(theory_var v1, theory_var v2) { } - void get_model(model_ref& mdl) { - mdl = m_model.get(); - } private: @@ -244,7 +239,6 @@ namespace smt { m_min_cost = weight; m_cost_save.reset(); m_cost_save.append(m_costs); - ctx.get_model(m_model); } return false; } @@ -349,7 +343,6 @@ namespace opt { if (result == l_true) { m_lower = m_upper; } - wth.get_model(m_model); TRACE("opt", tout << "min cost: " << m_upper << "\n";); wth.reset(); return result; @@ -364,7 +357,10 @@ namespace opt { } void get_model(model_ref& mdl) { - mdl = m_model.get(); + lbool is_sat = s.check_sat_core(0,0); + if (is_sat == l_true) { + s.get_model(mdl); + } } };