mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fixes to model generation of weighted maxsat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-14 09:37:42 +02:00
parent 5225ea18b7
commit 04824d86df
8 changed files with 45 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/opt/fu_malik.cpp
View file

@ -43,7 +43,7 @@ namespace opt {
struct fu_malik::imp {
ast_manager& m;
solver & m_original_solver;
opt_solver & m_opt_solver;
ref<solver> 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() {

4
src/opt/fu_malik.h
View file

@ -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;

2
src/opt/maxsmt.cpp
View file

@ -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;

5
src/opt/maxsmt.h
View file

@ -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);

31
src/opt/opt_context.cpp
View file

@ -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 {

6
src/opt/opt_context.h
View file

@ -86,6 +86,8 @@ namespace opt {
model_ref m_model;
model_converter_ref m_model_converter;
obj_map<func_decl, unsigned> m_objective_fns;
obj_map<func_decl, expr*> 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<rational>& weights, rational& offset, bool& neg,
symbol& id, unsigned& index);

2
src/opt/opt_solver.h
View file

@ -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();

12
src/opt/weighted_maxsat.cpp
View file

@ -35,7 +35,6 @@ namespace smt {
rational m_min_cost; // current maximal cost assignment.
u_map<theory_var> m_bool2var; // bool_var -> theory_var
svector<bool_var> 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);
}
}
};