diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index 07153e1ac..cb68b2c0b 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -59,11 +59,18 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } vector params; for (unsigned i = 0; i < num_parameters; ++i) { - if (parameters[i].is_int()) { - params.push_back(parameter(rational(parameters[i].get_int()))); + parameter const& p = parameters[i]; + if (p.is_int()) { + params.push_back(p); } - else if (parameters[i].is_rational()) { - params.push_back(parameter(parameters[i].get_rational())); + else if (p.is_rational()) { + // HACK: ast pretty printer does not work with rationals. + if (p.get_rational().is_int32()) { + params.push_back(parameter(p.get_rational().get_int32())); + } + else { + params.push_back(p); + } } else { m.raise_exception("function 'pble' expects arity+1 integer parameters"); @@ -148,11 +155,11 @@ bool pb_util::is_at_least_k(app *a, rational& k) const { rational pb_util::get_k(app *a) const { parameter const& p = a->get_decl()->get_parameter(0); if (is_at_most_k(a) || is_at_least_k(a)) { - return rational(p.get_int()); + return to_rational(p); } else { SASSERT(is_le(a) || is_ge(a)); - return p.get_rational(); + return to_rational(p); } } @@ -191,7 +198,13 @@ rational pb_util::get_coeff(app* a, unsigned index) { } SASSERT(is_le(a) || is_ge(a)); SASSERT(1 + index < a->get_decl()->get_num_parameters()); - return a->get_decl()->get_parameter(index + 1).get_rational(); + return to_rational(a->get_decl()->get_parameter(index + 1)); } - +rational pb_util::to_rational(parameter const& p) const { + if (p.is_int()) { + return rational(p.get_int()); + } + SASSERT(p.is_rational()); + return p.get_rational(); +} diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index 4b768ff11..103f74115 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -92,6 +92,8 @@ public: bool is_ge(app* a) const; bool is_ge(app* a, rational& k) const; rational get_coeff(app* a, unsigned index); +private: + rational to_rational(parameter const& p) const; }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e3d4a555e..52ae1e38e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -23,6 +23,11 @@ Notes: #include "opt_params.hpp" #include "arith_decl_plugin.h" #include "for_each_expr.h" +#include "goal.h" +#include "tactic.h" +#include "lia2card_tactic.h" +#include "elim01_tactic.h" +#include "tactical.h" namespace opt { @@ -51,21 +56,24 @@ namespace opt { m_objectives.push_back(objective(m, id)); m_indices.insert(id, m_objectives.size() - 1); } - ms->add(f, w); SASSERT(m_indices.contains(id)); - return m_indices[id]; + unsigned idx = m_indices[id]; + m_objectives[idx].m_terms.push_back(f); + m_objectives[idx].m_weights.push_back(w); + return idx; } unsigned context::add_objective(app* t, bool is_max) { app_ref tr(t, m); - unsigned index = m_optsmt.get_num_objectives(); - m_optsmt.add(t, is_max); + unsigned index = m_objectives.size(); m_objectives.push_back(objective(is_max, tr, index)); return index; } lbool context::optimize() { - opt_solver& s = get_solver(); + opt_solver& s = get_solver(); + normalize(); + internalize(); solver::scoped_push _sp(s); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { s.assert_expr(m_hard_constraints[i].get()); @@ -137,9 +145,9 @@ namespace opt { lbool context::execute_box() { lbool r = l_true; for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { - push(); + get_solver().push(); r = execute(m_objectives[i], false); - pop(1); + get_solver().pop(1); } return r; } @@ -153,12 +161,180 @@ namespace opt { return *m_solver.get(); } - void context::push() { - get_solver().push(); + void context::normalize() { + expr_ref_vector fmls(m); + to_fmls(fmls); + simplify_fmls(fmls); + from_fmls(fmls); } - void context::pop(unsigned sz) { - get_solver().pop(sz); + void context::simplify_fmls(expr_ref_vector& fmls) { + goal_ref g(alloc(goal, m, true, false)); + for (unsigned i = 0; i < fmls.size(); ++i) { + g->assert_expr(fmls[i].get()); + } + tactic_ref tac1 = mk_elim01_tactic(m); + tactic_ref tac2 = mk_lia2card_tactic(m); + tactic_ref tac = and_then(tac1.get(), tac2.get()); + model_converter_ref mc; // TBD: expose model converter upwards and apply to returned model. + proof_converter_ref pc; + expr_dependency_ref core(m); + goal_ref_buffer result; + (*tac)(g, result, mc, pc, core); // TBD: have this an attribute so we can cancel. + SASSERT(result.size() == 1); + goal* r = result[0]; + fmls.reset(); + for (unsigned i = 0; i < r->size(); ++i) { + fmls.push_back(r->form(i)); + } + } + + bool context::is_maximize(expr* fml, app_ref& 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)); + return true; + } + return false; + } + + bool context::is_minimize(expr* fml, app_ref& 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)); + return true; + } + return false; + } + + bool context::is_maxsat(expr* fml, expr_ref_vector& terms, + vector& weights, symbol& id, unsigned& index) { + if (!is_app(fml)) return 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()); + weights.append(m_objectives[index].m_weights); + id = m_objectives[index].m_id; + return true; + } + app_ref term(m); + if (is_minimize(fml, term, index)) { + TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";); + rational coeff(0); + return get_pb_sum(term, terms, weights, coeff); + } + return false; + } + + expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) { + ptr_vector domain; + for (unsigned i = 0; i < sz; ++i) { + domain.push_back(m.get_sort(args[i])); + } + char const* name = ""; + switch(ty) { + case O_MAXIMIZE: name = "maximize"; break; + case O_MINIMIZE: name = "minimize"; break; + case O_MAXSMT: name = "maxsat"; break; + default: break; + } + func_decl* f = m.mk_fresh_func_decl(name,"", domain.size(), domain.c_ptr(), m.mk_bool_sort()); + m_objective_fns.insert(f, index); + 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) { + m_hard_constraints.reset(); + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* fml = fmls[i]; + app_ref tr(m); + expr_ref_vector terms(m); + vector weights; + unsigned index; + symbol id; + if (is_maxsat(fml, terms, weights, id, index)) { + objective& obj = m_objectives[index]; + if (obj.m_type != O_MAXSMT) { + // change from maximize/minimize. + obj.m_id = id; + obj.m_type = O_MAXSMT; + obj.m_weights.append(weights); + SASSERT(!m_maxsmts.contains(id)); + maxsmt* ms = alloc(maxsmt, m); + m_maxsmts.insert(id, ms); + m_indices.insert(id, index); + } + SASSERT(obj.m_id == id); + obj.m_terms.reset(); + obj.m_terms.append(terms); + } + else if (is_maximize(fml, tr, index)) { + m_objectives[index].m_term = tr; + } + else if (is_minimize(fml, tr, index)) { + m_objectives[index].m_term = tr; + } + else { + m_hard_constraints.push_back(fml); + } + } + } + + 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.c_ptr())); + break; + } + } + } + + void context::internalize() { + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective & obj = m_objectives[i]; + switch(obj.m_type) { + case O_MINIMIZE: + obj.m_index = m_optsmt.get_num_objectives(); + m_optsmt.add(obj.m_term, false); + break; + case O_MAXIMIZE: + obj.m_index = m_optsmt.get_num_objectives(); + m_optsmt.add(obj.m_term, true); + 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[j].get(), obj.m_weights[j]); + } + break; + } + } + } } void context::display_assignment(std::ostream& out) { @@ -333,13 +509,11 @@ namespace opt { case O_MINIMIZE: visitor.collect(obj.m_term); break; - case O_MAXSMT: { - maxsmt& ms = *m_maxsmts.find(obj.m_id); - for (unsigned j = 0; j < ms.size(); ++j) { - visitor.collect(ms[j]); + case O_MAXSMT: + for (unsigned j = 0; j < obj.m_terms.size(); ++j) { + visitor.collect(obj.m_terms[j]); } break; - } default: UNREACHABLE(); break; @@ -375,17 +549,16 @@ namespace opt { PP(obj.m_term); out << ")\n"; break; - case O_MAXSMT: { - maxsmt& ms = *m_maxsmts.find(obj.m_id); - for (unsigned j = 0; j < ms.size(); ++j) { + case O_MAXSMT: + for (unsigned j = 0; j < obj.m_terms.size(); ++j) { out << "(assert-soft "; - PP(ms[j]); - rational w = ms.weight(j); + PP(obj.m_terms[j]); + rational w = obj.m_weights[j]; if (w.is_int()) { - out << " :weight " << ms.weight(j); + out << " :weight " << w; } else { - out << " :dweight " << ms.weight(j); + out << " :dweight " << w; } if (obj.m_id != symbol::null) { out << " :id " << obj.m_id; @@ -393,7 +566,6 @@ namespace opt { out << ")\n"; } break; - } default: UNREACHABLE(); break; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 7ab30ec71..9bc1007de 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -43,20 +43,27 @@ namespace opt { O_MINIMIZE, O_MAXSMT }; + struct objective { objective_t m_type; - app_ref m_term; // for maximize, minimize - symbol m_id; // for maxsmt - unsigned m_index; + app_ref m_term; // for maximize, minimize term + expr_ref_vector m_terms; // for maxsmt + vector m_weights; // for maxsmt + symbol m_id; // for maxsmt + unsigned m_index; // for maximize/minimize index + objective(bool is_max, app_ref& t, unsigned idx): m_type(is_max?O_MAXIMIZE:O_MINIMIZE), m_term(t), + m_terms(t.get_manager()), m_id(), m_index(idx) {} + objective(ast_manager& m, symbol id): m_type(O_MAXSMT), m_term(m), + m_terms(m), m_id(id), m_index(0) {} @@ -70,6 +77,7 @@ namespace opt { map_id m_indices; vector m_objectives; model_ref m_model; + obj_map m_objective_fns; public: context(ast_manager& m); ~context(); @@ -106,8 +114,20 @@ namespace opt { lbool execute_pareto(); expr_ref to_expr(inf_eps const& n); - void push(); - void pop(unsigned sz); + 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_maxsat(expr* fml, expr_ref_vector& terms, + vector& weights, 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); + expr* mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args); + void to_fmls(expr_ref_vector& fmls); + void from_fmls(expr_ref_vector const& fmls); + void simplify_fmls(expr_ref_vector& fmls); + opt_solver& get_solver(); }; diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index ebad310d3..91a421adb 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -208,13 +208,12 @@ namespace opt { // First check_sat call to initialize theories lbool is_sat = s->check_sat(0, 0); + solver::scoped_push _push(*s); if (is_sat == l_true && !m_objs.empty()) { for (unsigned i = 0; i < m_objs.size(); ++i) { m_vars.push_back(s->add_objective(m_objs[i].get())); } - solver::scoped_push _push(*s); - if (m_engine == symbol("basic")) { is_sat = basic_opt(); } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 96245165f..48b4a4583 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -927,7 +927,7 @@ namespace smt { */ template theory_var theory_arith::pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain) { - TRACE("maximize", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); + TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); theory_var x_i = null_theory_var; inf_numeral curr_gain; column & c = m_columns[x_j]; @@ -951,7 +951,7 @@ namespace smt { x_i = s; a_ij = coeff; gain = curr_gain; - TRACE("maximize", + TRACE("opt", tout << "x_i: v" << x_i << ", gain: " << gain << "\n"; tout << "value(s): (" << get_value(s) << " - " << b->get_value() << ")/" << coeff << "\n"; display_row(tout, r, true); @@ -959,10 +959,10 @@ namespace smt { } } } - TRACE("maximize", tout << "x_i: v" << x_i << ", gain: " << gain << "\n";); + TRACE("opt", tout << "x_i: v" << x_i << ", gain: " << gain << "\n";); } } - TRACE("maximize", tout << "x_i v" << x_i << "\n";); + TRACE("opt", tout << "x_i v" << x_i << "\n";); return x_i; } @@ -1017,11 +1017,15 @@ namespace smt { if (get_theory_vars(term, vars)) { m_objective_theory_vars.insert(v, vars); } + TRACE("opt", tout << mk_pp(term, get_manager()) << " |-> v" << v << "\n";); + TRACE("opt", tout << "data-size: " << m_data.size() << "\n";); + SASSERT(!is_quasi_base(v)); return v; } template inf_eps_rational theory_arith::maximize(theory_var v) { + TRACE("opt", tout << "data-size: " << m_data.size() << "\n";); bool r = max_min(v, true); if (r || at_upper(v)) { if (m_objective_theory_vars.contains(v)) { @@ -1250,7 +1254,7 @@ namespace smt { x_j = null_theory_var; x_i = null_theory_var; gain.reset(); - TRACE("maximize", tout << "i: " << i << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout); i++;); + TRACE("opt", tout << "i: " << i << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout); i++;); typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { @@ -1288,10 +1292,10 @@ namespace smt { } } } - TRACE("maximize", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";); + TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";); if (x_j == null_theory_var) { - TRACE("maximize", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); + TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); return true; @@ -1301,14 +1305,14 @@ namespace smt { // can increase/decrease x_j as much as we want. if (inc && upper(x_j)) { update_value(x_j, upper_bound(x_j) - get_value(x_j)); - TRACE("maximize", tout << "moved v" << x_j << " to upper bound\n";); + TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); continue; } if (!inc && lower(x_j)) { update_value(x_j, lower_bound(x_j) - get_value(x_j)); - TRACE("maximize", tout << "moved v" << x_j << " to lower bound\n";); + TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); continue; @@ -1320,18 +1324,18 @@ namespace smt { // can increase/decrease x_j up to upper/lower bound. if (inc) { update_value(x_j, upper_bound(x_j) - get_value(x_j)); - TRACE("maximize", tout << "moved v" << x_j << " to upper bound\n";); + TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); } else { update_value(x_j, lower_bound(x_j) - get_value(x_j)); - TRACE("maximize", tout << "moved v" << x_j << " to lower bound\n";); + TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); } SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); continue; } - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; + TRACE("opt", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; tout << "value x_i: " << get_value(x_i) << "\n"; @@ -1379,7 +1383,7 @@ namespace smt { SASSERT(!delta.is_neg()); } - TRACE("maximize", tout << "Original delta: " << delta << "\n";); + TRACE("opt", tout << "Original delta: " << delta << "\n";); delta_abs = abs(delta); // @@ -1415,7 +1419,7 @@ namespace smt { delta = delta_abs; } - TRACE("maximize", tout << "Safe delta: " << delta << "\n";); + TRACE("opt", tout << "Safe delta: " << delta << "\n";); update_value(x_i, delta); } @@ -1441,7 +1445,7 @@ namespace smt { */ template bool theory_arith::max_min(theory_var v, bool max) { - TRACE("maximize", tout << (max ? "maximizing" : "minimizing") << " v" << v << "...\n";); + TRACE("opt", tout << (max ? "maximizing" : "minimizing") << " v" << v << "...\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); SASSERT(!is_quasi_base(v)); @@ -1461,7 +1465,7 @@ namespace smt { } } if (max_min(m_tmp_row, max)) { - TRACE("maximize", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; + TRACE("opt", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row);); mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row); @@ -1489,7 +1493,7 @@ namespace smt { if (succ) { // process new bounds bool r = propagate_core(); - TRACE("maximize", tout << "after max/min round:\n"; display(tout);); + TRACE("opt", tout << "after max/min round:\n"; display(tout);); return r; } return true; diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp new file mode 100644 index 000000000..de76b5e62 --- /dev/null +++ b/src/tactic/arith/elim01_tactic.cpp @@ -0,0 +1,177 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + elim01_tactic.cpp + +Abstract: + + Replace 0-1 integer variables by Booleans. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-7 + +Notes: + +--*/ +#include"tactical.h" +#include"cooperate.h" +#include"bound_manager.h" +#include"ast_pp.h" +#include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version. +#include"arith_decl_plugin.h" +#include"elim01_tactic.h" + +class bool2int_model_converter : public model_converter { + ast_manager& m; + arith_util a; + func_decl_ref_vector m_refs; + obj_map m_bool2int; +public: + + bool2int_model_converter(ast_manager& m): + m(m), + a(m), + m_refs(m) + {} + + virtual void operator()(model_ref & old_model, unsigned goal_idx) { + SASSERT(goal_idx == 0); + model * new_model = alloc(model, m); + unsigned num = old_model->get_num_constants(); + for (unsigned i = 0; i < num; ++i) { + func_decl* f = old_model->get_constant(i); + expr* fi = old_model->get_const_interp(f); + func_decl* f_old; + if (m_bool2int.find(f, f_old)) { + if (!fi) { + // no-op + } + else if (m.is_false(fi)) { + fi = a.mk_numeral(rational(0), true); + } + else if (m.is_true(fi)) { + fi = a.mk_numeral(rational(1), true); + } + else { + fi = 0; + } + new_model->register_decl(f_old, fi); + } + else { + new_model->register_decl(f, fi); + } + num = old_model->get_num_functions(); + for (unsigned i = 0; i < num; i++) { + func_decl * f = old_model->get_function(i); + func_interp * fi = old_model->get_func_interp(f); + new_model->register_decl(f, fi->copy()); + } + new_model->copy_usort_interps(*old_model); + old_model = new_model; + } + } + + void insert(func_decl* x_new, func_decl* x_old) { + m_refs.push_back(x_new); + m_refs.push_back(x_old); + m_bool2int.insert(x_new, x_old); + } + + + virtual model_converter * translate(ast_translation & translator) { + bool2int_model_converter* mc = alloc(bool2int_model_converter, translator.to()); + obj_map::iterator it = m_bool2int.begin(), end = m_bool2int.end(); + for (; it != end; ++it) { + mc->insert(translator(it->m_key), translator(it->m_value)); + } + return mc; + } +}; + + +class elim01_tactic : public tactic { +public: + typedef obj_hashtable expr_set; + ast_manager & m; + arith_util a; + params_ref m_params; + + elim01_tactic(ast_manager & _m, params_ref const & p): + m(_m), + a(m) { + } + + virtual ~elim01_tactic() { + } + + void set_cancel(bool f) { + } + + void updt_params(params_ref const & p) { + m_params = p; + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + + tactic_report report("elim01", *g); + + expr_safe_replace sub(m); + bool2int_model_converter* b2i = alloc(bool2int_model_converter, m); + mc = b2i; + bound_manager bounds(m); + bounds(*g); + + bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); + for (; bit != bend; ++bit) { + if (!is_app(*bit)) continue; + app* x = to_app(*bit); + bool s1, s2; + rational lo, hi; + if (a.is_int(x) && + bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && + bounds.has_upper(x, hi, s2) && !s2 && hi.is_one()) { + app* x_new = m.mk_fresh_const(x->get_decl()->get_name().str().c_str(), m.mk_bool_sort()); + sub.insert(x, m.mk_ite(x_new, a.mk_numeral(rational(1), true), + a.mk_numeral(rational(0), true))); + b2i->insert(x_new->get_decl(), x->get_decl()); + } + } + + expr_ref new_curr(m); + proof_ref new_pr(m); + + for (unsigned i = 0; i < g->size(); i++) { + expr * curr = g->form(i); + sub(curr, new_curr); + g->update(i, new_curr, new_pr, g->dep(i)); + } + g->inc_depth(); + result.push_back(g.get()); + TRACE("pb", g->display(tout);); + SASSERT(g->is_well_sorted()); + + // TBD: support proof conversion (or not..) + } + + virtual tactic * translate(ast_manager & m) { + return alloc(elim01_tactic, m, m_params); + } + + virtual void collect_param_descrs(param_descrs & r) {} + + virtual void cleanup() {} +}; + +tactic * mk_elim01_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(elim01_tactic, m, p)); +} + diff --git a/src/tactic/arith/elim01_tactic.h b/src/tactic/arith/elim01_tactic.h new file mode 100644 index 000000000..867013ed0 --- /dev/null +++ b/src/tactic/arith/elim01_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + elim01_tactic.h + +Abstract: + + Replace 0-1 integer variables by Booleans. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-7 + +Notes: + +--*/ +#ifndef _ELIM01_TACTIC_H_ +#define _ELIM01_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_elim01_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("elim01", "eliminate 0-1 integer variables, replace them by Booleans.", "mk_elim01_tactic(m, p)") +*/ + + +#endif diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 4212b8e4d..347d4749f 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -143,24 +143,44 @@ public: if ((a.is_le(fml, x, y) || a.is_ge(fml, y, x)) && get_pb_sum(x, rational::one(), args, coeffs, coeff) && get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { - result = m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff); + result = mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff); return true; } else if ((a.is_lt(fml, y, x) || a.is_gt(fml, x, y)) && get_pb_sum(x, rational::one(), args, coeffs, coeff) && get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { - result = m.mk_not(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); + result = m.mk_not(mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); return true; } else if (m.is_eq(fml, x, y) && get_pb_sum(x, rational::one(), args, coeffs, coeff) && get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { - result = m.mk_and(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff), - m_pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); + result = m.mk_and(mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff), + mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); return true; } return false; } + + expr* mk_le(unsigned sz, rational const* weights, expr* const* args, rational const& w) { + if (sz == 1 && weights[0].is_one() && w >= rational::one()) { + return m.mk_true(); + } + if (sz == 1 && weights[0].is_one() && w.is_zero()) { + return m.mk_not(args[0]); + } + return m_pb.mk_le(sz, weights, args, w); + } + + expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) { + if (sz == 1 && weights[0].is_one() && w.is_one()) { + return args[0]; + } + if (sz == 1 && weights[0].is_one() && w.is_zero()) { + return m.mk_not(args[0]); + } + return m_pb.mk_ge(sz, weights, args, w); + } bool get_pb_sum(expr* x, rational const& mul, expr_ref_vector& args, vector& coeffs, rational& coeff) { expr *y, *z, *u; @@ -179,31 +199,53 @@ public: else if (a.is_uminus(x, y)) { ok = get_pb_sum(y, -mul, args, coeffs, coeff); } - else if (a.is_mul(x, y, z) && a.is_numeral(y, r)) { + else if (a.is_mul(x, y, z) && is_numeral(y, r)) { ok = get_pb_sum(z, r*mul, args, coeffs, coeff); } - else if (a.is_mul(x, z, y) && a.is_numeral(y, r)) { + else if (a.is_mul(x, z, y) && is_numeral(y, r)) { ok = get_pb_sum(z, r*mul, args, coeffs, coeff); } - else if (m.is_ite(x, y, z, u) && a.is_numeral(z, r) && a.is_numeral(u, q)) { - args.push_back(y); - coeffs.push_back(r*mul); - args.push_back(m.mk_not(y)); - coeffs.push_back(q*mul); + else if (m.is_ite(x, y, z, u) && is_numeral(z, r) && is_numeral(u, q)) { + insert_arg(r*mul, y, args, coeffs, coeff); + // q*(1-y) = -q*y + q + coeff += q*mul; + insert_arg(-q*mul, y, args, coeffs, coeff); } else if (is_01var(x)) { - args.push_back(mk_01(x)); - coeffs.push_back(mul); + insert_arg(mul, mk_01(x), args, coeffs, coeff); } - else if (a.is_numeral(x, r)) { + else if (is_numeral(x, r)) { coeff += mul*r; } else { + TRACE("pb", tout << "Can't handle " << mk_pp(x, m) << "\n";); ok = false; } return ok; } + + bool is_numeral(expr* e, rational& r) { + if (a.is_uminus(e, e) && is_numeral(e, r)) { + r.neg(); + return true; + } + return a.is_numeral(e, r); + } + void insert_arg(rational const& p, expr* x, + expr_ref_vector& args, vector& coeffs, rational& coeff) { + if (p.is_neg()) { + // p*x = -p*(1-x) + p + args.push_back(m.mk_not(x)); + coeffs.push_back(-p); + coeff += p; + } + else if (p.is_pos()) { + args.push_back(x); + coeffs.push_back(p); + } + } + virtual tactic * translate(ast_manager & m) { return alloc(lia2card_tactic, m, m_params); } @@ -224,6 +266,9 @@ tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(lia2card_tactic, m, p)); } -void convert_objectives() { - +bool get_pb_sum(expr* term, expr_ref_vector& args, vector& coeffs, rational& coeff) { + params_ref p; + ast_manager& m = args.get_manager(); + lia2card_tactic tac(m, p); + return tac.get_pb_sum(term, rational::one(), args, coeffs, coeff); } diff --git a/src/tactic/arith/lia2card_tactic.h b/src/tactic/arith/lia2card_tactic.h index 69a5f3f60..de25ce409 100644 --- a/src/tactic/arith/lia2card_tactic.h +++ b/src/tactic/arith/lia2card_tactic.h @@ -30,4 +30,6 @@ tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p = params_ref() ADD_TACTIC("lia2card", "introduce cardinality constraints from 0-1 integer.", "mk_lia2card_tactic(m, p)") */ +bool get_pb_sum(expr* term, expr_ref_vector& args, vector& coeffs, rational& coeff); + #endif