mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
separate out file for objectives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
759d80dfe3
commit
401fced400
|
|
@ -132,6 +132,8 @@ namespace opt {
|
|||
}
|
||||
|
||||
};
|
||||
|
||||
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
|
||||
|
||||
lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) {
|
||||
ast_manager& m = soft_constraints.get_manager();
|
||||
|
|
|
|||
|
|
@ -21,8 +21,6 @@ Notes:
|
|||
--*/
|
||||
|
||||
#include "opt_context.h"
|
||||
#include "fu_malik.h"
|
||||
#include "weighted_maxsat.h"
|
||||
#include "ast_pp.h"
|
||||
#include "opt_solver.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
|
|
@ -37,7 +35,8 @@ namespace opt {
|
|||
m_hard_constraints(m),
|
||||
m_soft_constraints(m),
|
||||
m_objectives(m),
|
||||
m_opt_objectives(m)
|
||||
m_opt_objectives(m),
|
||||
m_maxsmt(m)
|
||||
{
|
||||
m_params.set_bool("model", true);
|
||||
m_params.set_bool("unsat_core", true);
|
||||
|
|
@ -45,57 +44,30 @@ namespace opt {
|
|||
|
||||
void context::optimize() {
|
||||
|
||||
expr_ref_vector const& fmls = m_soft_constraints;
|
||||
|
||||
if (!m_solver) {
|
||||
symbol logic;
|
||||
set_solver(alloc(opt_solver, m, m_params, logic));
|
||||
}
|
||||
solver* s = m_solver.get();
|
||||
|
||||
// really just works for opt_solver now.
|
||||
solver* s = m_solver.get();
|
||||
opt_solver::scoped_push _sp(get_opt_solver(*s));
|
||||
|
||||
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
|
||||
s->assert_expr(m_hard_constraints[i].get());
|
||||
}
|
||||
|
||||
expr_ref_vector fmls_copy(fmls);
|
||||
|
||||
lbool is_sat;
|
||||
if (!fmls.empty()) {
|
||||
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
|
||||
if (is_maxsat_problem()) {
|
||||
is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
|
||||
}
|
||||
else {
|
||||
is_sat = weighted_maxsat(get_opt_solver(*s), fmls_copy, m_weights);
|
||||
}
|
||||
std::cout << "is-sat: " << is_sat << "\n";
|
||||
if (is_sat != l_true) {
|
||||
return;
|
||||
}
|
||||
std::cout << "Satisfying soft constraints\n";
|
||||
for (unsigned i = 0; i < fmls_copy.size(); ++i) {
|
||||
std::cout << mk_pp(fmls_copy[i].get(), m) << "\n";
|
||||
}
|
||||
|
||||
is_sat = m_maxsmt(get_opt_solver(*s), m_soft_constraints, m_weights);
|
||||
|
||||
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
|
||||
s->assert_expr(m_soft_constraints[i].get());
|
||||
}
|
||||
|
||||
if (!m_objectives.empty()) {
|
||||
vector<inf_eps_rational<inf_rational> > values;
|
||||
for (unsigned i = 0; i < fmls_copy.size(); ++i) {
|
||||
s->assert_expr(fmls_copy[i].get());
|
||||
}
|
||||
is_sat = m_opt_objectives(get_opt_solver(*s), m_objectives, values);
|
||||
std::cout << "is-sat: " << is_sat << std::endl;
|
||||
|
||||
if (is_sat != l_true) {
|
||||
return;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < values.size(); ++i) {
|
||||
if (!m_is_max[i]) {
|
||||
values[i].neg();
|
||||
}
|
||||
std::cout << "objective value: " << mk_pp(m_objectives[i].get(), m) << " -> " << values[i].to_string() << std::endl;
|
||||
}
|
||||
}
|
||||
if (is_sat == l_true) {
|
||||
is_sat = m_opt_objectives(get_opt_solver(*s), m_objectives);
|
||||
}
|
||||
|
||||
if (m_objectives.empty() && m_soft_constraints.empty()) {
|
||||
is_sat = s->check_sat(0,0);
|
||||
|
|
@ -103,15 +75,6 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
bool context::is_maxsat_problem() const {
|
||||
vector<rational> const& ws = m_weights;
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
if (!ws[i].is_one()) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
opt_solver& context::get_opt_solver(solver& s) {
|
||||
if (typeid(opt_solver) != typeid(s)) {
|
||||
|
|
@ -125,6 +88,7 @@ namespace opt {
|
|||
m_solver->cancel();
|
||||
}
|
||||
m_opt_objectives.set_cancel(true);
|
||||
m_maxsmt.set_cancel(true);
|
||||
}
|
||||
|
||||
void context::reset_cancel() {
|
||||
|
|
@ -132,6 +96,7 @@ namespace opt {
|
|||
m_solver->reset_cancel();
|
||||
}
|
||||
m_opt_objectives.set_cancel(false);
|
||||
m_maxsmt.set_cancel(false);
|
||||
}
|
||||
|
||||
void context::add_objective(app* t, bool is_max) {
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@ Notes:
|
|||
#include "ast.h"
|
||||
#include "solver.h"
|
||||
#include "optimize_objectives.h"
|
||||
#include "opt_maxsmt.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
|
|
@ -43,6 +44,7 @@ namespace opt {
|
|||
ref<solver> m_solver;
|
||||
params_ref m_params;
|
||||
optimize_objectives m_opt_objectives;
|
||||
maxsmt m_maxsmt;
|
||||
public:
|
||||
context(ast_manager& m);
|
||||
|
||||
|
|
|
|||
66
src/opt/opt_maxsmt.cpp
Normal file
66
src/opt/opt_maxsmt.cpp
Normal file
|
|
@ -0,0 +1,66 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
opt_maxsmt.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
MaxSMT optimization context.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-7
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#include "opt_maxsmt.h"
|
||||
#include "fu_malik.h"
|
||||
#include "weighted_maxsat.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
lbool maxsmt::operator()(opt_solver& s, expr_ref_vector& fmls, vector<rational> const& ws) {
|
||||
lbool is_sat;
|
||||
|
||||
if (fmls.empty()) {
|
||||
is_sat = s.check_sat(0, 0);
|
||||
}
|
||||
else if (is_maxsat_problem(ws)) {
|
||||
is_sat = opt::fu_malik_maxsat(s, fmls);
|
||||
}
|
||||
else {
|
||||
is_sat = weighted_maxsat(s, fmls, ws);
|
||||
}
|
||||
|
||||
// Infrastructure for displaying and storing solution is TBD.
|
||||
std::cout << "is-sat: " << is_sat << "\n";
|
||||
if (is_sat == l_true) {
|
||||
std::cout << "Satisfying soft constraints\n";
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
std::cout << mk_pp(fmls[i].get(), m) << "\n";
|
||||
}
|
||||
}
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
void maxsmt::set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
}
|
||||
|
||||
bool maxsmt::is_maxsat_problem(vector<rational> const& ws) const {
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
if (!ws[i].is_one()) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
52
src/opt/opt_maxsmt.h
Normal file
52
src/opt/opt_maxsmt.h
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
opt_maxsmt.h
|
||||
|
||||
Abstract:
|
||||
|
||||
MaxSMT optimization context.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-7
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _OPT_MAXSMT_H_
|
||||
#define _OPT_MAXSMT_H_
|
||||
|
||||
#include "opt_solver.h"
|
||||
|
||||
namespace opt {
|
||||
/**
|
||||
Takes solver with hard constraints added.
|
||||
Returns modified soft constraints that are maximal assignments.
|
||||
*/
|
||||
|
||||
class maxsmt {
|
||||
ast_manager& m;
|
||||
opt_solver* s;
|
||||
volatile bool m_cancel;
|
||||
symbol m_engine;
|
||||
public:
|
||||
maxsmt(ast_manager& m): m(m), s(0), m_cancel(false) {}
|
||||
|
||||
lbool operator()(opt_solver& s, expr_ref_vector& soft, vector<rational> const& weights);
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
void set_engine(symbol const& e) { m_engine = e; }
|
||||
|
||||
private:
|
||||
|
||||
bool is_maxsat_problem(vector<rational> const& ws) const;
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -204,23 +204,25 @@ namespace opt {
|
|||
Takes solver with hard constraints added.
|
||||
Returns an optimal assignment to objective functions.
|
||||
*/
|
||||
lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector<inf_eps>& values) {
|
||||
lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector const& objectives) {
|
||||
s = &solver;
|
||||
s->reset_objectives();
|
||||
m_lower.reset();
|
||||
m_upper.reset();
|
||||
m_objs.reset();
|
||||
for (unsigned i = 0; i < objectives.size(); ++i) {
|
||||
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
|
||||
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
|
||||
m_objs.push_back(objectives[i]);
|
||||
}
|
||||
|
||||
// First check_sat call to initialize theories
|
||||
lbool is_sat = s->check_sat(0, 0);
|
||||
if (is_sat == l_true) {
|
||||
if (is_sat == l_true && !objectives.empty()) {
|
||||
opt_solver::scoped_push _push(*s);
|
||||
|
||||
for (unsigned i = 0; i < objectives.size(); ++i) {
|
||||
m_vars.push_back(s->add_objective(objectives[i].get()));
|
||||
m_vars.push_back(s->add_objective(objectives[i]));
|
||||
}
|
||||
|
||||
if (m_engine == symbol("basic")) {
|
||||
|
|
@ -235,12 +237,31 @@ namespace opt {
|
|||
NOT_IMPLEMENTED_YET();
|
||||
UNREACHABLE();
|
||||
}
|
||||
values.reset();
|
||||
values.append(m_lower);
|
||||
}
|
||||
|
||||
std::cout << "is-sat: " << is_sat << std::endl;
|
||||
display(std::cout);
|
||||
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
inf_eps optimize_objectives::get_value(bool as_positive, unsigned index) const {
|
||||
if (as_positive) {
|
||||
return m_lower[index];
|
||||
}
|
||||
else {
|
||||
return -m_lower[index];
|
||||
}
|
||||
}
|
||||
|
||||
void optimize_objectives::display(std::ostream& out) const {
|
||||
unsigned sz = m_objs.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
out << "objective value: " << mk_pp(m_objs[i], m) << " -> " << get_value(true, i).to_string() << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -33,17 +33,22 @@ namespace opt {
|
|||
volatile bool m_cancel;
|
||||
vector<inf_eps> m_lower;
|
||||
vector<inf_eps> m_upper;
|
||||
app_ref_vector m_objs;
|
||||
svector<smt::theory_var> m_vars;
|
||||
symbol m_engine;
|
||||
public:
|
||||
optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}
|
||||
optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
|
||||
|
||||
lbool operator()(opt_solver& s, app_ref_vector& objectives, vector<inf_eps>& values);
|
||||
lbool operator()(opt_solver& s, app_ref_vector const& objectives);
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
void set_engine(symbol const& e) { m_engine = e; }
|
||||
|
||||
void display(std::ostream& out) const;
|
||||
|
||||
inf_eps get_value(bool as_positive, unsigned index) const;
|
||||
|
||||
private:
|
||||
|
||||
lbool basic_opt();
|
||||
|
|
|
|||
|
|
@ -66,10 +66,13 @@ namespace smt {
|
|||
SASSERT(m_util.is_at_most_k(atom));
|
||||
unsigned k = m_util.get_k(atom);
|
||||
|
||||
|
||||
if (ctx.b_internalized(atom)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
m_stats.m_num_predicates++;
|
||||
|
||||
TRACE("card", tout << "internalize: " << mk_pp(atom, m) << "\n";);
|
||||
|
||||
SASSERT(!ctx.b_internalized(atom));
|
||||
|
|
@ -210,7 +213,10 @@ namespace smt {
|
|||
m_cards_trail.push_back(abv);
|
||||
}
|
||||
|
||||
|
||||
void theory_card::collect_statistics(::statistics& st) const {
|
||||
st.update("pb axioms", m_stats.m_num_axioms);
|
||||
st.update("pb predicates", m_stats.m_num_predicates);
|
||||
}
|
||||
|
||||
void theory_card::reset_eh() {
|
||||
|
||||
|
|
@ -229,6 +235,7 @@ namespace smt {
|
|||
m_cards_lim.reset();
|
||||
m_watch_trail.reset();
|
||||
m_watch_lim.reset();
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void theory_card::update_min_max(bool_var v, bool is_true, card* c) {
|
||||
|
|
@ -470,8 +477,16 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_card::add_clause(literal_vector const& lits) {
|
||||
m_stats.m_num_axioms++;
|
||||
context& ctx = get_context();
|
||||
TRACE("card", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
justification* js = 0;
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
|
||||
IF_VERBOSE(0,
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
verbose_stream() << lits[i] << " ";
|
||||
}
|
||||
verbose_stream() << "\n";);
|
||||
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -28,6 +28,13 @@ namespace smt {
|
|||
|
||||
typedef svector<std::pair<bool_var, int> > arg_t;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_axioms;
|
||||
unsigned m_num_predicates;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
stats() { reset(); }
|
||||
};
|
||||
|
||||
struct card {
|
||||
int m_k;
|
||||
bool_var m_bv;
|
||||
|
|
@ -49,6 +56,7 @@ namespace smt {
|
|||
unsigned_vector m_watch_lim;
|
||||
literal_vector m_literals;
|
||||
card_util m_util;
|
||||
stats m_stats;
|
||||
|
||||
void add_watch(bool_var bv, card* c);
|
||||
void add_card(card* c);
|
||||
|
|
@ -84,6 +92,7 @@ namespace smt {
|
|||
virtual void init_search_eh();
|
||||
virtual void push_scope_eh();
|
||||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
virtual void collect_statistics(::statistics & st) const;
|
||||
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -92,6 +92,7 @@ class lia2card_tactic : public tactic {
|
|||
it = m_01s.begin(), end = m_01s.end();
|
||||
for (; it != end; ++it) {
|
||||
if (!validate_uses(m_uses.find(*it))) {
|
||||
std::cout << "did not validate: " << mk_pp(*it, m) << "\n";
|
||||
m_uses.remove(*it);
|
||||
m_01s.remove(*it);
|
||||
it = m_01s.begin();
|
||||
|
|
|
|||
Loading…
Reference in a new issue