#include "util/gparams.h"
#include "ast/for_each_expr.h"
#include "ast/ast_pp.h"
#include "ast/ast_translation.h"
#include "ast/bv_decl_plugin.h"
#include "ast/pb_decl_plugin.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
#include "ast/ast_ll_pp.h"
#include "ast/display_dimacs.h"
#include "ast/occurs.h"
#include "model/model_smt2_pp.h"
#include "tactic/goal.h"
#include "tactic/tactic.h"
#include "tactic/arith/lia2card_tactic.h"
#include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/simplify_tactic.h"
#include "tactic/core/propagate_values_tactic.h"
#include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/elim_uncnstr_tactic.h"
#include "tactic/tactical.h"
#include "tactic/arith/card2bv_tactic.h"
#include "tactic/arith/eq2bv_tactic.h"
#include "tactic/bv/dt2bv_tactic.h"
#include "ast/converters/generic_model_converter.h"
#include "ackermannization/ackermannize_bv_tactic.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "params/sat_params.hpp"
#include "solver/tactic2solver.h"
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
#include "opt/opt_context.h"
#include "opt/opt_solver.h"
#include "opt/opt_nlsat.h"
#include "opt/opt_pareto_solver.h"
#include "opt/opt_params.hpp"
namespace opt {
void context::scoped_state::push() {
m_asms_lim.push_back(m_asms.size());
m_hard_lim.push_back(m_hard.size());
m_values_lim.push_back(m_values.size());
m_objectives_lim.push_back(m_objectives.size());
m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size());
}
void context::scoped_state::pop() {
m_hard.shrink(m_hard_lim.back());
m_asms.shrink(m_asms_lim.back());
m_values.shrink(m_values_lim.back());
unsigned k = m_objectives_term_trail_lim.back();
while (m_objectives_term_trail.size() > k) {
unsigned idx = m_objectives_term_trail.back();
m_objectives[idx].m_terms.pop_back();
m_objectives[idx].m_weights.pop_back();
m_objectives_term_trail.pop_back();
}
m_objectives_term_trail_lim.pop_back();
k = m_objectives_lim.back();
while (m_objectives.size() > k) {
objective& obj = m_objectives.back();
if (obj.m_type == O_MAXSMT) {
m_indices.erase(obj.m_id);
}
m_objectives.pop_back();
}
m_objectives_lim.pop_back();
m_hard_lim.pop_back();
m_asms_lim.pop_back();
m_values_lim.pop_back();
}
void context::scoped_state::add(expr* hard) {
m_hard.push_back(hard);
}
bool context::scoped_state::set(expr_ref_vector const & hard) {
bool eq = hard.size() == m_hard.size();
for (unsigned i = 0; eq && i < hard.size(); ++i) {
eq = hard.get(i) == m_hard.get(i);
}
m_hard.reset();
m_hard.append(hard);
return !eq;
}
unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) {
if (!m.is_bool(f)) {
throw default_exception("Soft constraint should be Boolean");
}
if (!m_indices.contains(id)) {
m_objectives.push_back(objective(m, id));
m_indices.insert(id, m_objectives.size() - 1);
}
SASSERT(m_indices.contains(id));
unsigned idx = m_indices[id];
if (!w.is_zero()) {
m_objectives[idx].m_terms.push_back(f);
m_objectives[idx].m_weights.push_back(w);
m_objectives_term_trail.push_back(idx);
}
return idx;
}
unsigned context::scoped_state::add(app* t, bool is_max) {
app_ref tr(t, m);
if (!m_bv.is_bv(t) && !m_arith.is_int_real(t)) {
throw default_exception("Objective must be bit-vector, integer or real");
}
unsigned index = m_objectives.size();
m_objectives.push_back(objective(is_max, tr, index));
return index;
}
context::context(ast_manager& m):
opt_wrapper(m),
m_arith(m),
m_bv(m),
m_hard_constraints(m),
m_solver(nullptr),
m_pareto1(false),
m_box_index(UINT_MAX),
m_optsmt(m, *this),
m_scoped_state(m),
m_fm(alloc(generic_model_converter, m, "opt")),
m_model_fixed(),
m_objective_refs(m),
m_core(m),
m_unknown("unknown")
{
params_ref p;
p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("elim_to_real", true);
updt_params(p);
m_model_counter = 0;
}
context::~context() {
reset_maxsmts();
}
context* context::translate(ast_manager& target_m) {
ast_translation translator(m, target_m);
context* result = alloc(context, target_m);
result->updt_params(m_params);
if (m_logic != symbol::null) {
result->set_logic(m_logic);
}
for (expr* e : m_scoped_state.m_hard) {
result->add_hard_constraint(translator(e));
}
for (auto const& obj : m_scoped_state.m_objectives) {
if (obj.m_type == O_MAXIMIZE || obj.m_type == O_MINIMIZE) {
app_ref translated_term(to_app(translator(obj.m_term.get())), target_m);
result->add_objective(translated_term, obj.m_type == O_MAXIMIZE);
}
else if (obj.m_type == O_MAXSMT) {
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
result->add_soft_constraint(
translator(obj.m_terms.get(i)),
obj.m_weights[i],
obj.m_id
);
}
}
}
result->m_enable_sat = m_enable_sat;
result->m_enable_sls = m_enable_sls;
result->m_is_clausal = m_is_clausal;
result->m_pp_neat = m_pp_neat;
result->m_pp_wcnf = m_pp_wcnf;
result->m_incremental = m_incremental;
result->m_maxsat_engine = m_maxsat_engine;
return result;
}
void context::reset_maxsmts() {
for (auto& kv : m_maxsmts) {
dealloc(kv.m_value);
}
m_maxsmts.reset();
}
void context::push() {
m_scoped_state.push();
}
void context::pop(unsigned n) {
n = std::min(n, m_scoped_state.num_scopes());
for (unsigned i = 0; i < n; ++i) {
m_scoped_state.pop();
}
clear_state();
reset_maxsmts();
m_optsmt.reset();
m_hard_constraints.reset();
}
void context::get_labels(svector<symbol> & r) {
r.append(m_labels);
}
void context::get_unsat_core(expr_ref_vector & r) {
r.append(m_core);
}
void context::set_hard_constraints(expr_ref_vector const& fmls) {
if (m_calling_on_model) {
for (expr* f : fmls)
add_hard_constraint(f);
return;
}
if (m_scoped_state.set(fmls))
clear_state();
}
void context::add_hard_constraint(expr* f) {
if (m_calling_on_model) {
if (!m_incremental)
throw default_exception("Set opt.incremental = true to allow adding constraints during search");
get_solver().assert_expr(f);
for (auto const& [k, v] : m_maxsmts)
v->reset_upper();
for (unsigned i = 0; i < num_objectives(); ++i) {
auto const& o = m_scoped_state.m_objectives[i];
if (o.m_type != O_MAXSMT)
m_optsmt.update_upper(o.m_index, inf_eps::infinity());
}
}
else {
m_scoped_state.add(f);
clear_state();
}
}
void context::add_hard_constraint(expr* f, expr* t) {
if (m_calling_on_model)
throw default_exception("adding hard constraints is not supported during callbacks");
m_scoped_state.m_asms.push_back(t);
m_scoped_state.add(m.mk_implies(t, f));
clear_state();
}
void context::get_hard_constraints(expr_ref_vector& hard) {
hard.append(m_scoped_state.m_hard);
}
expr_ref context::get_objective(unsigned i) {
SASSERT(i < num_objectives());
objective const& o = m_scoped_state.m_objectives[i];
expr_ref result(m), zero(m);
expr_ref_vector args(m);
switch (o.m_type) {
case O_MAXSMT:
zero = m_arith.mk_numeral(rational(0), false);
for (unsigned i = 0; i < o.m_terms.size(); ++i) {
args.push_back(m.mk_ite(o.m_terms[i], zero, m_arith.mk_numeral(o.m_weights[i], false)));
}
result = m_arith.mk_add(args.size(), args.data());
break;
case O_MAXIMIZE:
result = o.m_term;
if (m_arith.is_int_real(result)) {
result = m_arith.mk_uminus(result);
}
else if (m_bv.is_bv(result)) {
result = m_bv.mk_bv_neg(result);
}
else {
UNREACHABLE();
}
break;
case O_MINIMIZE:
result = o.m_term;
break;
}
return result;
}
unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
clear_state();
return m_scoped_state.add(f, w, id);
}
unsigned context::add_objective(app* t, bool is_max) {
clear_state();
return m_scoped_state.add(t, is_max);
}
void context::import_scoped_state() {
m_optsmt.reset();
reset_maxsmts();
m_objectives.reset();
m_hard_constraints.reset();
scoped_state& s = m_scoped_state;
for (unsigned i = 0; i < s.m_objectives.size(); ++i) {
objective& obj = s.m_objectives[i];
m_objectives.push_back(obj);
if (obj.m_type == O_MAXSMT) {
add_maxsmt(obj.m_id, i);
}
}
m_hard_constraints.append(s.m_hard);
}
lbool context::optimize(expr_ref_vector const& _asms) {
scoped_time _st(*this);
if (m_pareto) {
return execute_pareto();
}
if (m_box_index != UINT_MAX) {
return execute_box();
}
clear_state();
init_solver();
import_scoped_state();
expr_ref_vector asms(_asms);
asms.append(m_scoped_state.m_asms);
m_has_assumptions = !asms.empty();
normalize(asms);
if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) {
return l_false;
}
internalize();
update_solver();
if (contains_quantifiers()) {
warning_msg("optimization with quantified constraints is not supported");
}
solver& s = get_solver();
s.assert_expr(m_hard_constraints);
if (m_model_converter)
m_model_converter->convert_initialize_value(m_scoped_state.m_values);
for (auto & [var, value] : m_scoped_state.m_values)
s.user_propagate_initialize_value(var, value);
if (m_preferred) {
auto p = m_preferred;
s.user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
s.user_propagate_register_decide(p->decide_eh);
}
opt_params optp(m_params);
symbol pri = optp.priority();
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n");
lbool is_sat = s.check_sat(asms.size(), asms.data());
TRACE(opt, s.display(tout << "initial search result: " << is_sat << "\n"););
if (is_sat != l_false) {
s.get_model(m_model);
s.get_labels(m_labels);
model_updated(m_model.get());
if (!m_model) {
is_sat = l_undef;
}
}
if (is_sat != l_true) {
TRACE(opt, tout << m_hard_constraints << " " << asms << "\n";);
if (!asms.empty()) {
s.get_unsat_core(m_core);
}
return is_sat;
}
s.assert_expr(asms);
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n");
TRACE(opt, model_smt2_pp(tout, m, *m_model, 0););
m_optsmt.setup(*m_opt_solver.get());
update_lower();
switch (m_objectives.size()) {
case 0:
break;
case 1:
if (m_pareto1) {
is_sat = l_false;
m_pareto1 = false;
}
else {
m_pareto1 = (pri == symbol("pareto"));
is_sat = execute(m_objectives[0], true, false);
}
break;
default: {
opt_params optp(m_params);
symbol pri = optp.priority();
if (pri == symbol("pareto")) {
is_sat = execute_pareto();
}
else if (pri == symbol("box")) {
is_sat = execute_box();
}
else {
is_sat = execute_lex();
}
}
}
if (is_sat == l_true) validate_model();
return adjust_unknown(is_sat);
}
lbool context::adjust_unknown(lbool r) {
if (r == l_true && m_opt_solver.get() && m_opt_solver->was_unknown()) {
r = l_undef;
}
return r;
}
void context::get_base_model(model_ref& mdl) {
mdl = m_model;
}
void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed.contains(mdl.get())) {
TRACE(opt, m_fm->display(tout << "fix-model\n");
tout << *mdl << "\n";
if (m_model_converter) m_model_converter->display(tout););
(*m_fm)(mdl);
apply(m_model_converter, mdl);
m_model_fixed.push_back(mdl.get());
}
}
void context::set_model(model_ref& m) {
m_model = m;
m_model_available = true;
opt_params optp(m_params);
symbol prefix = optp.solution_prefix();
bool model2console = optp.dump_models();
bool model2file = prefix != symbol::null && prefix != symbol("");
if ((model2console || model2file) && m) {
model_ref md = m->copy();
fix_model(md);
if (model2file) {
std::ostringstream buffer;
buffer << prefix << (m_model_counter++) << ".smt2";
std::ofstream out(buffer.str());
if (out) {
out << *md;
out.close();
}
}
if (model2console)
std::cout << *md;
}
if (m_on_model_eh && m) {
model_ref md = m->copy();
if (!m_model_fixed.contains(md.get()))
fix_model(md);
flet<bool> _calling(m_calling_on_model, true);
m_on_model_eh(m_on_model_ctx, md);
m_model_fixed.pop_back();
}
}
void context::get_model_core(model_ref& mdl) {
if (!m_model_available)
throw default_exception("model is not available");
mdl = m_model;
CTRACE(opt, mdl, tout << *mdl;);
fix_model(mdl);
if (mdl) mdl->set_model_completion(true);
CTRACE(opt, mdl, tout << *mdl;);
}
void context::get_box_model(model_ref& mdl, unsigned index) {
if (index >= m_box_models.size()) {
throw default_exception("index into models is out of bounds");
}
mdl = m_box_models[index];
fix_model(mdl);
}
bool context::contains_quantifiers() const {
for (expr* f : m_hard_constraints) {
if (has_quantifiers(f)) return true;
}
return false;
}
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
inf_eps lower0 = m_optsmt.get_lower(index).rational_bound();
inf_eps upper0 = m_optsmt.get_upper(index).rational_bound();
if (scoped) get_solver().push();
lbool result = m_optsmt.lex(index, is_max);
if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
if (scoped) get_solver().pop(1);
m_optsmt.update_lower(index, lower0);
m_optsmt.update_upper(index, upper0);
warning_msg("unbounded objectives on quantified constraints is not supported");
return l_undef;
}
if (result == l_true && m_optsmt.has_open_bound(index)) {
if (committed && m_objectives.size() > 1) {
m_opt_solver->set_reason_unknown("later lexicographic objectives after an unattained nonlinear optimum are not supported");
result = l_undef;
}
committed = false;
}
if (result == l_true) { m_optsmt.get_model(m_model, m_labels); SASSERT(m_model); }
if (result == l_undef) {
model_ref mdl;
svector<symbol> labels;
m_optsmt.get_model(mdl, labels);
if (mdl) {
m_model = mdl;
m_labels = labels;
}
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) m_optsmt.commit_assignment(index);
return result;
}
lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) {
model_ref tmp;
maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push();
lbool result = ms(committed);
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) {
ms.get_model(m_model, m_labels);
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
DEBUG_CODE(if (result == l_true) validate_maxsat(id););
return result;
}
lbool context::execute(objective const& obj, bool committed, bool scoped) {
switch(obj.m_type) {
case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped, true);
case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped, false);
case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped);
}
UNREACHABLE();
return l_undef;
}
bool context::scoped_lex() {
if (m_maxsat_engine == symbol("maxres")) {
for (auto const& o : m_objectives) {
if (o.m_type != O_MAXSMT) return true;
}
return false;
}
return true;
}
lbool context::execute_lex() {
lbool r = l_true;
bool sc = scoped_lex();
IF_VERBOSE(1, verbose_stream() << "(opt :lex)\n";);
unsigned sz = m_objectives.size();
for (unsigned i = 0; r == l_true && i < sz; ++i) {
objective const& o = m_objectives[i];
bool is_last = i + 1 == sz;
r = execute(o, i + 1 < sz, sc && !is_last);
bool unbounded =
(o.m_type == O_MINIMIZE && !get_lower_value(i).is_finite()) ||
(o.m_type == O_MAXIMIZE && !get_upper_value(i).is_finite());
if (r == l_true && unbounded) {
if (!is_last)
r = execute_lex_after_unbounded(i);
return r;
}
if (r == l_true && i + 1 < sz) {
update_lower();
}
}
DEBUG_CODE(if (r == l_true) validate_lex(););
return r;
}
lbool context::execute_lex_after_unbounded(unsigned unbounded_index) {
unsigned sz = m_objectives.size();
unsigned u = m_objectives[unbounded_index].m_index;
for (unsigned j = unbounded_index + 1; j < sz; ++j) {
objective const& o = m_objectives[j];
if (o.m_type == O_MAXSMT)
return l_true;
lbool r = m_optsmt.lex_after_unbounded(u, o.m_index, o.m_type == O_MAXIMIZE);
model_ref mdl;
svector<symbol> labels;
m_optsmt.get_model(mdl, labels);
if (mdl) {
m_model = mdl;
m_labels = labels;
}
if (r != l_true)
return r;
if (j + 1 < sz) {
if (get_lower_value(j) != get_upper_value(j))
return l_true;
m_optsmt.commit_assignment(o.m_index);
}
}
return l_true;
}
lbool context::execute_box() {
if (m_box_index < m_box_models.size()) {
m_model = m_box_models[m_box_index];
CTRACE(opt, m_model, tout << *m_model << "\n";);
++m_box_index;
return l_true;
}
if (m_box_index < m_objectives.size()) {
m_model = nullptr;
++m_box_index;
return l_undef;
}
if (m_box_index != UINT_MAX && m_box_index >= m_objectives.size()) {
m_box_index = UINT_MAX;
return l_false;
}
m_box_index = 1;
m_box_models.reset();
lbool r = m_optsmt.box();
for (unsigned i = 0, j = 0; r == l_true && i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
if (obj.m_type == O_MAXSMT) {
solver::scoped_push _sp(get_solver());
r = execute(obj, false, false);
m_box_models.push_back(m_model.get());
}
else {
model* mdl = m_optsmt.get_model(j);
if (!mdl) mdl = m_model.get();
m_box_models.push_back(mdl);
++j;
}
}
if (r == l_true && !m_box_models.empty()) {
m_model = m_box_models[0];
CTRACE(opt, m_model, tout << *m_model << "\n";);
}
return r;
}
expr_ref context::mk_le(unsigned i, model_ref& mdl) {
objective const& obj = m_objectives[i];
return mk_cmp(false, mdl, obj);
}
expr_ref context::mk_ge(unsigned i, model_ref& mdl) {
objective const& obj = m_objectives[i];
return mk_cmp(true, mdl, obj);
}
expr_ref context::mk_gt(unsigned i, model_ref& mdl) {
expr_ref result = mk_le(i, mdl);
result = mk_not(m, result);
return result;
}
expr_ref context::mk_cmp(bool is_ge, model_ref& mdl, objective const& obj) {
rational k(0);
expr_ref val(m), result(m);
switch (obj.m_type) {
case O_MINIMIZE:
is_ge = !is_ge;
Z3_fallthrough;
case O_MAXIMIZE:
val = (*mdl)(obj.m_term);
if (m_pareto_exact_comparison && m_arith.is_irrational_algebraic_numeral(val)) {
result = is_ge ? mk_ge(obj.m_term, val) : mk_ge(val, obj.m_term);
break;
}
if (!is_numeral(val, k) && model_value_bound(m_arith, val, is_ge, k))
val = m_arith.mk_numeral(k, false);
if (is_numeral(val, k)) {
if (is_ge) {
result = mk_ge(obj.m_term, val);
}
else {
result = mk_ge(val, obj.m_term);
}
}
else {
IF_VERBOSE(5, verbose_stream() << "(opt.pareto :unhandled-objective-value "
<< val << ")\n");
result = m.mk_true();
}
break;
case O_MAXSMT: {
pb_util pb(m);
unsigned sz = obj.m_terms.size();
ptr_vector<expr> terms;
vector<rational> coeffs;
for (unsigned i = 0; i < sz; ++i) {
terms.push_back(obj.m_terms[i]);
coeffs.push_back(obj.m_weights[i]);
if (mdl->is_true(obj.m_terms[i])) {
k += obj.m_weights[i];
}
else {
TRACE(opt, tout << (*mdl)(obj.m_terms[i]) << "\n";);
}
}
if (is_ge) {
result = pb.mk_ge(sz, coeffs.data(), terms.data(), k);
}
else {
result = pb.mk_le(sz, coeffs.data(), terms.data(), k);
}
break;
}
}
TRACE(opt,
tout << (is_ge?">= ":"<= ") << k << "\n";
display_objective(tout, obj);
tout << "\n";
tout << result << "\n";);
return result;
}
expr_ref context::mk_ge(expr* t, expr* s) {
expr_ref result(m);
if (m_bv.is_bv(t)) {
result = m_bv.mk_ule(s, t);
}
else {
result = m_arith.mk_ge(t, s);
}
return result;
}
void context::publish_pareto_result() {
SASSERT (m_pareto);
m_pareto->get_model(m_model, m_labels);
update_bound(true);
update_bound(false);
TRACE(opt, model_smt2_pp(tout, m, *m_model.get(), 0););
}
solver* context::mk_pareto_solver() {
opt_params optp(m_params);
m_pareto_exact_comparison = false;
if (!optp.pareto_nlsat() || m_has_assumptions)
return m_solver.get();
expr_ref_vector terms(m_hard_constraints);
for (objective const& obj : m_objectives) {
if (obj.m_type != O_MAXIMIZE && obj.m_type != O_MINIMIZE)
return m_solver.get();
if (!m_arith.is_real(obj.m_term))
return m_solver.get();
if (!in_nra_fragment(m, m_arith, m_hard_constraints, obj.m_term))
return m_solver.get();
terms.push_back(obj.m_term);
}
solver* s;
bool reuse_nlsat_solver = optp.pareto_nlsat_reuse() && can_reuse_nlsat_solver(terms);
if (reuse_nlsat_solver)
s = mk_pareto_nlsat_solver(m, m_params);
else {
tactic_ref t = mk_qfnra_nlsat_tactic(m, m_params);
s = mk_tactic2solver(m, t.get(), m_params);
}
for (expr* f : m_hard_constraints)
s->assert_expr(f);
m_pareto_exact_comparison = true;
IF_VERBOSE(2, verbose_stream() << "(opt.pareto :solver " << (reuse_nlsat_solver ? "incremental-nlsat" : "qfnra-nlsat") << ")\n");
return s;
}
lbool context::execute_pareto() {
if (!m_pareto) {
m_pareto_unknown.clear();
set_pareto(alloc(gia_pareto, m, *this, mk_pareto_solver(), m_params));
}
lbool is_sat = (*(m_pareto.get()))();
if (is_sat != l_true) {
if (is_sat == l_undef)
m_pareto_unknown = m_pareto->reason_unknown();
if (m_pareto_exact_comparison) {
statistics stats;
m_pareto->collect_statistics(stats);
add_statistics(stats);
}
set_pareto(nullptr);
}
if (is_sat == l_true) {
publish_pareto_result();
}
return is_sat;
}
std::string context::reason_unknown() const {
if (!m.inc()) {
return Z3_CANCELED_MSG;
}
if (!m_pareto_unknown.empty())
return m_pareto_unknown;
if (m_solver.get()) {
return m_solver->reason_unknown();
}
return m_unknown;
}
void context::display_bounds(std::ostream& out, bounds_t const& b) const {
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
display_objective(out, obj);
auto [lower, upper] = b[i];
if (obj.m_type == O_MAXIMIZE) {
out << " |-> [" << lower << ":" << upper << "]\n";
}
else {
out << " |-> [" << -upper << ":" << -lower << "]\n";
}
}
}
solver& context::get_solver() {
return *m_solver.get();
}
void context::init_solver() {
setup_arith_solver();
m_sat_solver = nullptr;
m_opt_solver = alloc(opt_solver, m, m_params, *m_fm);
m_opt_solver->set_logic(m_logic);
m_solver = m_opt_solver.get();
m_opt_solver->ensure_pb();
}
void context::setup_arith_solver() {
opt_params p(m_params);
if (p.optsmt_engine() == symbol("symba") ||
p.optsmt_engine() == symbol("farkas")) {
m_params.set_uint("arith.solver", static_cast<unsigned>(arith_solver_id::AS_OPTINF));
}
}
void context::initialize_value(expr* var, expr* value) {
m_scoped_state.m_values.push_back({expr_ref(var, m), expr_ref(value, m)});
}
void context::update_solver() {
sat_params p(m_params);
if (!p.euf() && (!m_enable_sat || !probe_fd()))
return;
if (!is_maxsat_query())
return;
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("maxresw") &&
m_maxsat_engine != symbol("rc2") &&
m_maxsat_engine != symbol("rc2tot") &&
m_maxsat_engine != symbol("rc2bin") &&
m_maxsat_engine != symbol("maxres-bin") &&
m_maxsat_engine != symbol("maxres-bin-delay") &&
m_maxsat_engine != symbol("pd-maxres") &&
m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) {
return;
}
if (opt_params(m_params).priority() == symbol("pareto"))
return;
if (m.proofs_enabled())
return;
m_params.set_bool("minimize_core_partial", true);
m_params.set_bool("minimize_core", true);
m_sat_solver = mk_inc_sat_solver(m, m_params);
expr_ref_vector fmls(m);
get_solver().get_assertions(fmls);
m_sat_solver->assert_expr(fmls);
m_solver = m_sat_solver.get();
}
void context::enable_sls(bool force) {
if ((force || m_enable_sls) && m_sat_solver.get()) {
m_params.set_bool("optimize_model", true);
m_sat_solver->updt_params(m_params);
}
}
struct context::is_fd {
struct found_fd {};
ast_manager& m;
pb_util pb;
bv_util bv;
is_fd(ast_manager& m): m(m), pb(m), bv(m) {}
void operator()(var *) { throw found_fd(); }
void operator()(quantifier *) { throw found_fd(); }
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != m.get_basic_family_id() &&
fid != pb.get_family_id() &&
fid != bv.get_family_id() &&
(!is_uninterp_const(n) || (!m.is_bool(n) && !bv.is_bv(n)))) {
throw found_fd();
}
}
};
bool context::is_maxsat_query() {
for (objective& obj : m_objectives)
if (obj.m_type != O_MAXSMT)
return false;
return true;
}
bool context::probe_fd() {
expr_fast_mark1 visited;
is_fd proc(m);
if (!is_maxsat_query())
return false;
try {
for (objective& obj : m_objectives) {
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < ms.size(); ++j)
quick_for_each_expr(proc, visited, ms[j]);
}
unsigned sz = get_solver().get_num_assertions();
for (unsigned i = 0; i < sz; ++i)
quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
for (expr* f : m_hard_constraints)
quick_for_each_expr(proc, visited, f);
}
catch (const is_fd::found_fd &) {
return false;
}
return true;
}
struct context::is_propositional_fn {
struct found {};
ast_manager& m;
is_propositional_fn(ast_manager& m): m(m) {}
void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); }
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != m.get_basic_family_id() &&
!is_uninterp_const(n)) {
throw found();
}
}
};
bool context::is_propositional(expr* p) {
expr* np;
if (is_uninterp_const(p) || (m.is_not(p, np) && is_uninterp_const(np))) {
return true;
}
is_propositional_fn proc(m);
expr_fast_mark1 visited;
try {
quick_for_each_expr(proc, visited, p);
}
catch (const is_propositional_fn::found &) {
return false;
}
return true;
}
void context::add_maxsmt(symbol const& id, unsigned index) {
maxsmt* ms = alloc(maxsmt, *this, index);
ms->updt_params(m_params);
m_maxsmts.insert(id, ms);
}
bool context::is_numeral(expr* e, rational & n) const {
unsigned sz;
return m_arith.is_numeral(e, n) || m_bv.is_numeral(e, n, sz);
}
void context::normalize(expr_ref_vector const& asms) {
expr_ref_vector fmls(m);
m_model_converter = nullptr;
to_fmls(fmls);
simplify_fmls(fmls, asms);
while (asms.empty() && simplify_min_max_of_sums(fmls))
simplify_fmls(fmls, asms);
from_fmls(fmls);
}
void context::simplify_fmls(expr_ref_vector& fmls, expr_ref_vector const& asms) {
if (m_is_clausal) {
return;
}
goal_ref g(alloc(goal, m, true, !asms.empty()));
for (expr* fml : fmls)
g->assert_expr(fml);
for (expr * a : asms)
g->assert_expr(a, a);
params_ref som_params(m_params);
som_params.set_bool("som", true);
tactic_ref tac0 =
and_then(mk_simplify_tactic(m, som_params),
mk_propagate_values_tactic(m),
m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
mk_simplify_tactic(m));
opt_params optp(m_params);
tactic_ref tac1, tac2, tac3, tac4;
bool has_dep = false;
for (unsigned i = 0; !has_dep && i < g->size(); ++i) {
ptr_vector<expr> deps;
expr_dependency_ref core(g->dep(i), m);
m.linearize(core, deps);
has_dep |= !deps.empty();
}
if (optp.elim_01() && m_logic.is_null() && !has_dep && !m_incremental) {
tac1 = mk_dt2bv_tactic(m);
tac2 = mk_lia2card_tactic(m);
tac3 = mk_eq2bv_tactic(m);
params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac2->updt_params(lia_p);
set_simplify(and_then(tac0.get(), tac1.get(), tac2.get(), tac3.get(), mk_simplify_tactic(m)));
}
else {
set_simplify(tac0.get());
}
goal_ref_buffer result;
TRACE(opt, g->display(tout););
(*m_simplify)(g, result);
SASSERT(result.size() == 1);
goal* r = result[0];
m_model_converter = r->mc();
CTRACE(opt, r->mc(), r->mc()->display(tout););
fmls.reset();
expr_ref tmp(m);
for (unsigned i = 0; i < r->size(); ++i) {
if (asms.empty()) {
fmls.push_back(r->form(i));
continue;
}
ptr_vector<expr> deps;
expr_dependency_ref core(r->dep(i), m);
m.linearize(core, deps);
if (deps.empty())
fmls.push_back(r->form(i));
else if (deps.size() == 1 && deps[0] == r->form(i))
continue;
else if (is_objective(r->form(i)))
fmls.push_back(r->form(i));
else
fmls.push_back(m.mk_implies(mk_and(m, deps), r->form(i)));
}
if (r->inconsistent()) {
ptr_vector<expr> core_elems;
expr_dependency_ref core(r->dep(0), m);
m.linearize(core, core_elems);
m_core.append(core_elems.size(), core_elems.data());
}
}
bool context::is_objective(expr* fml) {
return is_app(fml) && m_objective_fns.contains(to_app(fml)->get_decl());
}
bool context::is_maximize(expr* fml, app_ref& term, expr_ref& 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, expr_ref& 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;
}
bool context::simplify_min_max_of_sums(expr_ref_vector& fmls) {
bool simplified = false;
bool progress = true;
while (progress) {
progress = false;
for (auto f : fmls) {
if (is_min_max_of_sums(f, fmls)) {
progress = true;
simplified = true;
break;
}
}
}
return simplified;
}
bool context::is_min_max_of_sums(expr* fml, expr_ref_vector& fmls) {
app_ref term(m);
expr_ref orig_term(m);
unsigned index = 0;
bool is_max = is_maximize(fml, term, orig_term, index);
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
if (!is_max && !is_min)
return false;
if (!is_uninterp(term)) return false;
ptr_vector<expr> _fmls(fmls.size(), fmls.data());
expr_mark mark;
mark_occurs(_fmls, term, mark);
unsigned max_cardinality = 0, min_cardinality = UINT_MAX;
expr_ref_vector cardinalities(m);
arith_util a(m);
expr *x = nullptr, *y = nullptr, *cnd = nullptr, *th = nullptr, *el = nullptr;
rational n;
auto is_zero_one = [&](expr *t) -> bool {
return m.is_ite(t, cnd, th, el) && a.is_numeral(th, n) &&
(n == 1 || n == 0) && a.is_numeral(el, n) &&
(n == 1 || n == 0);
};
auto is_lower_bound = [&](expr *f) {
if (!a.is_le(f, x, y))
return false;
if (x != term)
return false;
if (mark.is_marked(y))
return false;
bool is_zo = is_zero_one(y);
if (!a.is_add(y) && !is_zo)
return false;
if (!is_zo && !all_of(*to_app(y), is_zero_one))
return false;
cardinalities.push_back(y);
max_cardinality = std::max(max_cardinality, is_zo ? 1 : to_app(y)->get_num_args());
min_cardinality = std::min(min_cardinality, is_zo ? 1 : to_app(y)->get_num_args());
return true;
};
auto is_upper_bound = [&](expr *f) {
if (!a.is_ge(f, x, y))
return false;
if (x != term)
return false;
bool is_zo = is_zero_one(y);
if (!is_zo && !a.is_add(y))
return false;
if (!is_zo && !all_of(*to_app(y), is_zero_one))
return false;
cardinalities.push_back(x);
max_cardinality = std::max(max_cardinality, is_zo ? 1 : to_app(x)->get_num_args());
min_cardinality = std::min(min_cardinality, is_zo ? 1 : to_app(y)->get_num_args());
return true;
};
for (auto f : fmls) {
if (fml == f)
continue;
if (!mark.is_marked(f))
continue;
if (is_max && is_lower_bound(f))
continue;
if (!is_max && is_upper_bound(f))
continue;
return false;
}
if (min_cardinality == UINT_MAX)
return false;
expr_ref_vector new_fmls(m);
expr_ref_vector soft(m);
for (unsigned k = 1; k <= min_cardinality; ++k) {
auto p_k = m.mk_fresh_const("p", m.mk_bool_sort());
expr_ref one(a.mk_int(1), m);
soft.push_back(m.mk_ite(p_k, one, a.mk_int(0)));
for (auto c : cardinalities)
if (is_max)
new_fmls.push_back(m.mk_implies(p_k, a.mk_ge(c, a.mk_int(k))));
else
new_fmls.push_back(m.mk_implies(a.mk_ge(c, a.mk_int(k)), p_k));
}
app_ref sum(a.mk_add(soft.size(), soft.data()), m);
if (is_max)
new_fmls.push_back(mk_maximize(index, sum));
else
new_fmls.push_back(mk_minimize(index, sum));
unsigned j = 0;
for (auto f : fmls)
if (!mark.is_marked(f))
fmls[j++] = f;
fmls.shrink(j);
fmls.append(new_fmls);
return true;
}
bool context::is_maxsat(expr* fml, expr_ref_vector& terms,
vector<rational>& weights, rational& offset,
bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
if (!is_app(fml))
return false;
neg = false;
orig_term = nullptr;
index = 0;
app* a = to_app(fml);
if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) {
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr_ref arg(a->get_arg(i), m);
rational weight = m_objectives[index].m_weights[i];
if (weight.is_neg()) {
weight.neg();
arg = mk_not(m, arg);
offset -= weight;
}
if (m.is_true(arg)) {
IF_VERBOSE(5, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> true\n";);
}
else if (weight.is_zero()) {
}
else if (m.is_false(arg)) {
IF_VERBOSE(5, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> false\n";);
offset += weight;
}
else {
terms.push_back(arg);
weights.push_back(weight);
}
}
id = m_objectives[index].m_id;
return true;
}
app_ref term(m);
offset = rational::zero();
bool is_max = is_maximize(fml, term, orig_term, index);
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
if (!is_max && !is_min)
return false;
if (is_min && get_pb_sum(term, terms, weights, offset)) {
TRACE(opt, tout << "try to convert minimization\n" << mk_pp(term, m) << "\n";);
for (unsigned i = 0; i < weights.size(); ++i) {
if (weights[i].is_neg()) {
offset += weights[i];
weights[i].neg();
}
else {
terms[i] = mk_not(m, terms[i].get());
}
}
TRACE(opt,
tout << "Convert minimization " << orig_term << "\n";
tout << "to maxsat: " << term << "\n";
for (unsigned i = 0; i < weights.size(); ++i) {
tout << mk_pp(terms.get(i), m) << ": " << weights[i] << "\n";
}
tout << "offset: " << offset << "\n";
);
std::ostringstream out;
out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
id = symbol(out.str());
return true;
}
if (is_max && get_pb_sum(term, terms, weights, offset)) {
TRACE(opt, tout << "try to convert maximization " << mk_pp(term, m) << "\n";);
for (unsigned i = 0; i < weights.size(); ++i) {
if (weights[i].is_neg()) {
weights[i].neg();
terms[i] = mk_not(m, terms[i].get());
}
offset += weights[i];
}
neg = true;
std::ostringstream out;
out << mk_bounded_pp(orig_term, m) << ':' << index;
id = symbol(out.str());
return true;
}
if ((is_max || is_min) && m_bv.is_bv(term)) {
offset.reset();
unsigned bv_size = m_bv.get_bv_size(term);
expr_ref val(m);
val = m_bv.mk_numeral(is_max, 1);
for (unsigned i = 0; i < bv_size; ++i) {
rational w = power(rational(2),i);
weights.push_back(w);
terms.push_back(m.mk_eq(val, m_bv.mk_extract(i, i, term)));
if (is_max) {
offset += w;
}
}
neg = is_max;
std::ostringstream out;
out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
id = symbol(out.str());
return true;
}
return false;
}
expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) {
ptr_vector<sort> domain;
for (unsigned i = 0; i < sz; ++i) {
domain.push_back(args[i]->get_sort());
}
char const* name = "";
switch(ty) {
case O_MAXIMIZE: name = "maximize"; break;
case O_MINIMIZE: name = "minimize"; break;
case O_MAXSMT: name = "maxsat"; break;
}
func_decl* f = m.mk_fresh_func_decl(name,"", domain.size(), domain.data(), m.mk_bool_sort());
m_objective_fns.insert(f, index);
m_objective_refs.push_back(f);
m_objective_orig.insert(f, sz > 0 ? args[0] : nullptr);
return m.mk_app(f, sz, args);
}
expr* context::mk_maximize(unsigned index, app* t) {
expr* t_ = t;
return mk_objective_fn(index, O_MAXIMIZE, 1, &t_);
}
expr* context::mk_minimize(unsigned index, app* t) {
expr* t_ = t;
return mk_objective_fn(index, O_MINIMIZE, 1, &t_);
}
expr* context::mk_maxsat(unsigned index, unsigned num_fmls, expr* const* fmls) {
return mk_objective_fn(index, O_MAXSMT, num_fmls, fmls);
}
void context::from_fmls(expr_ref_vector const& fmls) {
TRACE(opt, tout << fmls << "\n";);
m_hard_constraints.reset();
for (expr * fml : fmls) {
app_ref tr(m);
expr_ref orig_term(m);
expr_ref_vector terms(m);
vector<rational> weights;
rational offset(0);
unsigned index = 0;
symbol id;
bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) {
objective& obj = m_objectives[index];
if (obj.m_type != O_MAXSMT) {
obj.m_id = id;
obj.m_type = O_MAXSMT;
SASSERT(!m_maxsmts.contains(id));
add_maxsmt(id, index);
}
mk_atomic(terms);
SASSERT(obj.m_id == id);
obj.m_term = orig_term?to_app(orig_term):nullptr;
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_weights.reset();
obj.m_weights.append(weights);
obj.m_adjust_value.set_offset(offset);
obj.m_adjust_value.set_negate(neg);
TRACE(opt, tout << "maxsat: " << neg << " " << id << " offset: " << offset << "\n";
tout << terms << "\n";);
}
else if (is_maximize(fml, tr, orig_term, index)) {
purify(tr);
m_objectives[index].m_term = tr;
}
else if (is_minimize(fml, tr, orig_term, index)) {
purify(tr);
m_objectives[index].m_term = tr;
m_objectives[index].m_adjust_value.set_negate(true);
}
else {
m_hard_constraints.push_back(fml);
}
}
for (objective & obj : m_objectives) {
expr* t = obj.m_term;
switch(obj.m_type) {
case O_MINIMIZE:
case O_MAXIMIZE:
if (!m_arith.is_int(t) && !m_arith.is_real(t)) {
obj.m_term = m_arith.mk_numeral(rational(0), true);
}
break;
default:
break;
}
}
}
void context::model_updated(model* md) {
model_ref mdl = md;
set_model(mdl);
}
rational context::adjust(unsigned id, rational const& v) {
return m_objectives[id].m_adjust_value(v);
}
void context::add_offset(unsigned id, rational const& o) {
m_objectives[id].m_adjust_value.add_offset(o);
}
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
app_ref term = m_objectives[index].m_term;
if (!term) {
return true;
}
rational v = m_objectives[index].m_adjust_value(_v);
expr_ref val(m);
model_ref mdl = md->copy();
fix_model(mdl);
mdl->set_model_completion(true);
val = (*mdl)(term);
unsigned bvsz;
if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
TRACE(opt, tout << "model does not evaluate objective to a value but instead " << val << "\n";
tout << *mdl << "\n";
);
return false;
}
if (r != v) {
TRACE(opt, tout << "Out of bounds: " << term << " " << val << " != " << v << "\n";);
return false;
}
else {
TRACE(opt, tout << "validated: " << term << " = " << val << "\n";);
}
return true;
}
void context::purify(app_ref& term) {
generic_model_converter_ref fm;
if (m_arith.is_add(term)) {
expr_ref_vector args(m);
for (expr* arg : *term) {
if (is_mul_const(arg)) {
args.push_back(arg);
}
else {
args.push_back(purify(fm, arg));
}
}
term = m_arith.mk_add(args.size(), args.data());
}
else if (m.is_ite(term) || !is_mul_const(term)) {
TRACE(opt, tout << "Purifying " << term << "\n";);
term = purify(fm, term);
}
if (fm) {
m_model_converter = concat(m_model_converter.get(), fm.get());
}
}
bool context::is_mul_const(expr* e) {
expr* e1, *e2;
return
is_uninterp_const(e) ||
m_arith.is_numeral(e) ||
(m_arith.is_mul(e, e1, e2) && m_arith.is_numeral(e1) && is_uninterp_const(e2)) ||
(m_arith.is_mul(e, e2, e1) && m_arith.is_numeral(e1) && is_uninterp_const(e2));
}
app* context::purify(generic_model_converter_ref& fm, expr* term) {
std::ostringstream out;
out << mk_bounded_pp(term, m, 3);
app* q = m.mk_fresh_const(out.str(), term->get_sort());
if (!fm) fm = alloc(generic_model_converter, m, "opt");
if (m_arith.is_int_real(term)) {
m_hard_constraints.push_back(m_arith.mk_ge(q, term));
m_hard_constraints.push_back(m_arith.mk_le(q, term));
}
else {
m_hard_constraints.push_back(m.mk_eq(q, term));
}
fm->hide(q);
return q;
}
void context::mk_atomic(expr_ref_vector& terms) {
generic_model_converter_ref fm;
for (unsigned i = 0; i < terms.size(); ++i) {
expr_ref p(terms[i].get(), m);
app_ref q(m);
if (is_propositional(p)) {
terms[i] = p;
}
else {
terms[i] = purify(fm, p);
}
}
if (fm) {
m_model_converter = concat(m_model_converter.get(), fm.get());
}
}
void context::to_fmls(expr_ref_vector& fmls) {
m_objective_fns.reset();
fmls.append(m_hard_constraints);
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
switch(obj.m_type) {
case O_MINIMIZE:
fmls.push_back(mk_minimize(i, obj.m_term));
break;
case O_MAXIMIZE:
fmls.push_back(mk_maximize(i, obj.m_term));
break;
case O_MAXSMT:
fmls.push_back(mk_maxsat(i, obj.m_terms.size(), obj.m_terms.data()));
break;
}
}
TRACE(opt, tout << fmls << "\n";);
}
void context::internalize() {
for (objective & obj : m_objectives) {
switch(obj.m_type) {
case O_MINIMIZE: {
app_ref tmp(m);
tmp = obj.m_term;
if (m_arith.is_int(tmp) || m_arith.is_real(tmp)) {
tmp = m_arith.mk_uminus(obj.m_term);
}
obj.m_index = m_optsmt.add(tmp);
break;
}
case O_MAXIMIZE:
obj.m_index = m_optsmt.add(obj.m_term);
break;
case O_MAXSMT: {
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
ms.add(obj.m_terms.get(j), obj.m_weights[j]);
}
break;
}
}
}
}
void context::update_bound(bool is_lower) {
expr_ref val(m);
if (!m_model.get()) return;
for (objective const& obj : m_objectives) {
rational r;
switch(obj.m_type) {
case O_MINIMIZE: {
val = (*m_model)(obj.m_term);
TRACE(opt, tout << obj.m_term << " " << val << "\n";);
if (model_value_bound(m_arith, val, is_lower != obj.m_adjust_value.get_negate(), r) || m_bv.is_numeral(val, r)) {
inf_eps val = inf_eps(obj.m_adjust_value(r));
TRACE(opt, tout << "adjusted value: " << val << "\n";);
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val);
}
else {
m_optsmt.update_upper(obj.m_index, val);
}
}
break;
}
case O_MAXIMIZE: {
val = (*m_model)(obj.m_term);
TRACE(opt, tout << obj.m_term << " " << val << "\n";);
if (model_value_bound(m_arith, val, is_lower != obj.m_adjust_value.get_negate(), r) || m_bv.is_numeral(val, r)) {
inf_eps val = inf_eps(obj.m_adjust_value(r));
TRACE(opt, tout << "adjusted value: " << val << "\n";);
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val);
}
else {
m_optsmt.update_upper(obj.m_index, val);
}
}
break;
}
case O_MAXSMT: {
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
val = (*m_model)(obj.m_terms[j]);
TRACE(opt, tout << mk_pp(obj.m_terms[j], m) << " " << val << "\n";);
if (!m.is_true(val))
r += obj.m_weights[j];
}
maxsmt& ms = *m_maxsmts.find(obj.m_id);
if (is_lower) {
ms.update_upper(r);
TRACE(opt, tout << "update upper from " << r << " to " << ms.get_upper() << "\n";);
}
else {
ms.update_lower(r);
TRACE(opt, tout << "update lower from " << r << " to " << ms.get_lower() << "\n";);
}
break;
}
}
}
}
void context::display_benchmark() {
display(verbose_stream());
return;
if (opt_params(m_params).dump_benchmarks() &&
sat_enabled() &&
m_objectives.size() == 1 &&
m_objectives[0].m_type == O_MAXSMT
) {
objective& o = m_objectives[0];
unsigned sz = o.m_terms.size();
inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.data(), o.m_weights.data());
}
}
void context::display(std::ostream& out) {
display_assignment(out);
}
void context::display_assignment(std::ostream& out) {
if (m_scoped_state.m_objectives.size() != m_objectives.size()) {
throw default_exception("check-sat has not been called with latest objectives");
}
out << "(objectives\n";
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_scoped_state.m_objectives[i];
out << " (";
display_objective(out, obj);
objective_value lower = get_lower_value(i);
objective_value upper = get_upper_value(i);
if (lower != upper) {
out << " (interval " << lower.to_expr() << " " << upper.to_expr() << ")";
}
else if (lower.exact_finite() && !lower.has_infinitesimal()) {
out << " " << expr_ref(lower.exact_finite(), m);
}
else {
out << " " << lower.to_expr();
}
out << ")\n";
}
out << ")\n";
}
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;
}
}
objective_value context::get_lower_value(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 objective_value(m, inf_eps(m_maxsmts.find(obj.m_id)->get_lower()));
case O_MINIMIZE:
return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
case O_MAXIMIZE:
return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
}
UNREACHABLE();
return objective_value(m);
}
objective_value context::get_upper_value(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 objective_value(m, inf_eps(m_maxsmts.find(obj.m_id)->get_upper()));
case O_MINIMIZE:
return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
case O_MAXIMIZE:
return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
}
UNREACHABLE();
return objective_value(m);
}
expr_ref context::get_lower(unsigned idx) {
return get_lower_value(idx).to_expr();
}
expr_ref context::get_upper(unsigned idx) {
return get_upper_value(idx).to_expr();
}
void context::set_simplify(tactic* tac) {
m_simplify = tac;
}
void context::clear_state() {
m_pareto = nullptr;
m_pareto_unknown.clear();
m_pareto1 = false;
m_box_index = UINT_MAX;
m_box_models.reset();
m_model.reset();
m_model_fixed.reset();
m_core.reset();
m_model_available = false;
}
void context::set_pareto(pareto_base* p) {
m_pareto = p;
m_pareto1 = p != nullptr;
}
void context::collect_statistics_core(statistics& stats) const {
if (m_solver)
m_solver->collect_statistics(stats);
if (m_pareto && m_pareto_exact_comparison)
m_pareto->collect_statistics(stats);
if (m_simplify)
m_simplify->collect_statistics(stats);
for (auto const& kv : m_maxsmts)
kv.m_value->collect_statistics(stats);
get_memory_statistics(stats);
get_rlimit_statistics(m.limit(), stats);
}
void context::collect_param_descrs(param_descrs & r) {
opt_params::collect_param_descrs(r);
smt::kernel::collect_param_descrs(r);
insert_timeout(r);
insert_ctrl_c(r);
}
void context::updt_params(params_ref const& p) {
m_params.append(p);
if (m_solver) {
m_solver->updt_params(m_params);
}
if (m_sat_solver) {
m_sat_solver->updt_params(m_params);
}
m_optsmt.updt_params(m_params);
for (auto & kv : m_maxsmts) {
kv.m_value->updt_params(m_params);
}
opt_params _p(p);
m_enable_sat = _p.enable_sat();
m_enable_sls = _p.enable_sls();
m_maxsat_engine = _p.maxsat_engine();
m_pp_neat = _p.pp_neat();
m_pp_wcnf = _p.pp_wcnf();
m_incremental = _p.incremental();
}
std::string context::to_string() {
if (m_pp_wcnf)
return to_wcnf();
return to_string(false, m_scoped_state.m_hard, m_scoped_state.m_objectives);
}
std::string context::to_string_internal() const {
return to_string(true, m_hard_constraints, m_objectives);
}
std::string context::to_wcnf() {
import_scoped_state();
expr_ref_vector asms(m);
normalize(asms);
auto const& objectives = m_objectives;
if (objectives.size() > 1)
throw default_exception("only single objective weighted MaxSAT wcnf output is supported");
ptr_vector<expr> soft_f;
vector<rational> soft_w;
svector<std::pair<expr*, unsigned>> soft;
if (objectives.size() == 1) {
auto const& obj = objectives[0];
if (obj.m_type != O_MAXSMT)
throw default_exception("only single objective weighted MaxSAT wcnf output is supported");
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
rational w = obj.m_weights[j];
if (!w.is_unsigned())
throw default_exception("only single objective weighted MaxSAT wcnf output is supported");
soft_f.push_back(obj.m_terms[j]);
soft_w.push_back(w);
}
}
std::ostringstream strm;
m_sat_solver = mk_inc_sat_solver(m, m_params);
m_sat_solver->assert_expr(m_hard_constraints);
inc_sat_display(strm, *m_sat_solver.get(), soft_f.size(), soft_f.data(), soft_w.data());
return strm.str();
}
std::string context::to_string(bool is_internal, expr_ref_vector const& hard, vector<objective> const& objectives) const {
smt2_pp_environment_dbg env(m);
ast_pp_util visitor(m);
std::ostringstream out;
visitor.collect(hard);
model_converter_ref mc = concat(m_model_converter.get(), m_fm.get());
for (objective const& obj : objectives) {
switch(obj.m_type) {
case O_MAXIMIZE:
case O_MINIMIZE:
visitor.collect(obj.m_term);
break;
case O_MAXSMT:
visitor.collect(obj.m_terms);
break;
}
}
if (is_internal && mc) {
mc->set_env(&visitor);
}
param_descrs descrs;
collect_param_descrs(descrs);
m_params.display_smt2(out, "opt", descrs);
visitor.display_decls(out);
visitor.display_asserts(out, hard, m_pp_neat);
for (objective const& obj : objectives) {
switch(obj.m_type) {
case O_MAXIMIZE:
out << "(maximize ";
ast_smt2_pp(out, obj.m_term, env);
out << ")\n";
break;
case O_MINIMIZE:
out << "(minimize ";
ast_smt2_pp(out, obj.m_term, env);
out << ")\n";
break;
case O_MAXSMT:
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
out << "(assert-soft ";
ast_smt2_pp(out, obj.m_terms[j], env);
rational w = obj.m_weights[j];
w.display_decimal(out << " :weight ", 3, true);
if (obj.m_id != symbol::null) {
if (is_smt2_quoted_symbol(obj.m_id)) {
out << " :id " << mk_smt2_quoted_symbol(obj.m_id);
}
else {
out << " :id " << obj.m_id;
}
}
out << ")\n";
}
break;
}
}
if (is_internal && mc) {
mc->display(out);
}
if (is_internal && mc) {
mc->set_env(nullptr);
}
out << "(check-sat)\n";
return out.str();
}
void context::validate_model() {
return;
if (!gparams::get_ref().get_bool("model_validate", false)) return;
expr_ref_vector fmls(m);
get_hard_constraints(fmls);
expr_ref tmp(m);
model_ref mdl;
get_model(mdl);
mdl->set_model_completion(true);
for (expr * f : fmls) {
if (!mdl->is_true(f)) {
IF_VERBOSE(0,
verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n";
m_fm->display(verbose_stream() << "fm\n");
m_model_converter->display(verbose_stream() << "mc\n");
model_smt2_pp(verbose_stream(), m, *mdl, 0);
verbose_stream() << to_string_internal() << "\n");
}
}
}
void context::validate_maxsat(symbol const& id) {
maxsmt& ms = *m_maxsmts.find(id);
TRACE(opt, tout << "Validate: " << id << "\n";);
for (objective const& obj : m_objectives) {
if (obj.m_id == id && obj.m_type == O_MAXSMT) {
SASSERT(obj.m_type == O_MAXSMT);
rational value(0);
expr_ref val(m);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
auto const& t = obj.m_terms[i];
if (!m_model->is_true(t)) {
value += obj.m_weights[i];
}
}
value = obj.m_adjust_value(value);
rational value0 = ms.get_lower();
TRACE(opt, tout << "value " << value << " " << value0 << "\n";);
}
}
}
void context::validate_lex() {
rational r1;
expr_ref val(m);
SASSERT(m_model);
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
switch(obj.m_type) {
case O_MINIMIZE:
case O_MAXIMIZE:
break;
case O_MAXSMT: {
rational value(0);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
if (!m_model->is_true(obj.m_terms[i])) {
value += obj.m_weights[i];
}
}
maxsmt& ms = *m_maxsmts.find(obj.m_id);
rational value0 = ms.get_lower();
TRACE(opt, tout << "value " << value << " other " << value0 << "\n";);
break;
}
}
}
}
}