diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index bc186433e..c590f8320 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -83,18 +83,18 @@ public: app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); bool is_at_most_k(func_decl *a) const; - bool is_at_most_k(app *a) const { return is_at_most_k(a->get_decl()); } + bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); } bool is_at_most_k(app *a, rational& k) const; bool is_at_least_k(func_decl *a) const; - bool is_at_least_k(app *a) const { return is_at_most_k(a->get_decl()); } + bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); } bool is_at_least_k(app *a, rational& k) const; rational get_k(func_decl *a) const; rational get_k(app *a) const { return get_k(a->get_decl()); } bool is_le(func_decl *a) const; - bool is_le(app *a) const { return is_le(a->get_decl()); } + bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); } bool is_le(app* a, rational& k) const; bool is_ge(func_decl* a) const; - bool is_ge(app* a) const { return is_ge(a->get_decl()); } + bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); } bool is_ge(app* a, rational& k) const; rational get_coeff(app* a, unsigned index) const { return get_coeff(a->get_decl(), index); } rational get_coeff(func_decl* a, unsigned index) const; diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 462944943..5b1b37120 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -18,6 +18,60 @@ Notes: --*/ #include "pb_rewriter.h" +#include "pb_rewriter_def.h" +#include "ast_pp.h" + + +class pb_ast_rewriter_util { + ast_manager& m; + expr_ref_vector m_refs; +public: + + typedef std::pair arg_t; + typedef vector args_t; + typedef rational numeral; + + pb_ast_rewriter_util(ast_manager& m): m(m), m_refs(m) {} + + expr* negate(expr* e) { + if (m.is_true(e)) { + return m.mk_false(); + } + if (m.is_false(e)) { + return m.mk_true(); + } + if (m.is_not(e, e)) { + return e; + } + m_refs.push_back(m.mk_not(e)); + return m_refs.back(); + } + + void display(std::ostream& out, expr* e) { + out << mk_pp(e, m); + } + + bool is_negated(expr* e) const { + return m.is_not(e); + } + + bool is_true(expr* e) const { + return m.is_true(e); + } + + bool is_false(expr* e) const { + return m.is_false(e); + } + + struct compare { + bool operator()(std::pair const& a, + std::pair const& b) { + return a.first->get_id() < b.first->get_id(); + } + + }; +}; + br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { ast_manager& m = result.get_manager(); @@ -32,34 +86,59 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons } } rational k = m_util.get_k(f); + + vector > vec; + for (unsigned i = 0; i < num_args; ++i) { + vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i))); + } switch(f->get_decl_kind()) { case OP_AT_MOST_K: case OP_PB_LE: - if (sum > k) { - result = m.mk_false(); - return BR_DONE; + for (unsigned i = 0; i < num_args; ++i) { + vec[i].second.neg(); } - if (maxsum <= k) { - result = m.mk_true(); - return BR_DONE; - } - return BR_FAILED; + k.neg(); + break; case OP_AT_LEAST_K: case OP_PB_GE: - if (sum >= k) { - result = m.mk_true(); - return BR_DONE; - } - if (maxsum < k) { - result = m.mk_false(); - return BR_DONE; - } - return BR_FAILED; + break; default: UNREACHABLE(); return BR_FAILED; } + + + pb_ast_rewriter_util pbu(m); + pb_rewriter_util util(pbu); + + util.unique(vec, k); + lbool is_sat = util.normalize(vec, k); + util.prune(vec, k); + switch (is_sat) { + case l_true: + result = m.mk_true(); + break; + case l_false: + result = m.mk_false(); + break; + default: + m_args.reset(); + m_coeffs.reset(); + for (unsigned i = 0; i < vec.size(); ++i) { + m_args.push_back(vec[i].first); + m_coeffs.push_back(vec[i].second); + } + result = m_util.mk_ge(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k); + break; + } + TRACE("pb", + expr_ref tmp(m); + tmp = m.mk_app(f, num_args, args); + tout << tmp << "\n"; + tout << result << "\n";); + + return BR_DONE; } diff --git a/src/ast/rewriter/pb_rewriter.h b/src/ast/rewriter/pb_rewriter.h index da020cb7c..8ea41b668 100644 --- a/src/ast/rewriter/pb_rewriter.h +++ b/src/ast/rewriter/pb_rewriter.h @@ -22,12 +22,27 @@ Notes: #include"pb_decl_plugin.h" #include"rewriter_types.h" #include"params.h" +#include"lbool.h" + + +template +class pb_rewriter_util { + PBU& m_util; + void display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k); +public: + pb_rewriter_util(PBU& u) : m_util(u) {} + void unique(typename PBU::args_t& args, typename PBU::numeral& k); + lbool normalize(typename PBU::args_t& args, typename PBU::numeral& k); + void prune(typename PBU::args_t& args, typename PBU::numeral& k); +}; /** \brief Cheap rewrite rules for PB constraints */ class pb_rewriter { pb_util m_util; + vector m_coeffs; + ptr_vector m_args; public: pb_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h new file mode 100644 index 000000000..a6a37f73d --- /dev/null +++ b/src/ast/rewriter/pb_rewriter_def.h @@ -0,0 +1,263 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + pb_rewriter_def.h + +Abstract: + + Basic rewriting rules for PB constraints. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-14-12 + +Notes: + +--*/ +#ifndef _PB_REWRITER_DEF_H_ +#define _PB_REWRITER_DEF_H_ + +#include"pb_rewriter.h" + + +template +void pb_rewriter_util::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k) { + for (unsigned i = 0; i < args.size(); ++i) { + out << args[i].second << " * "; + m_util.display(out, args[i].first); + out << " "; + if (i+1 < args.size()) out << "+ "; + } + out << " >= " << k << "\n"; +} + +template +void pb_rewriter_util::unique(typename PBU::args_t& args, typename PBU::numeral& k) { + + TRACE("pb", display(tout << "pre-unique:", args, k);); + for (unsigned i = 0; i < args.size(); ++i) { + if (m_util.is_negated(args[i].first)) { + args[i].first = m_util.negate(args[i].first); + k -= args[i].second; + args[i].second = -args[i].second; + } + } + // remove constants + for (unsigned i = 0; i < args.size(); ++i) { + if (m_util.is_true(args[i].first)) { + k -= args[i].second; + std::swap(args[i], args[args.size()-1]); + args.pop_back(); + --i; + } + else if (m_util.is_false(args[i].first)) { + std::swap(args[i], args[args.size()-1]); + args.pop_back(); + --i; + } + } + // sort and coalesce arguments: + PBU::compare cmp; + std::sort(args.begin(), args.end(), cmp); + + unsigned i = 0, j = 1; + for (; j < args.size(); ++i) { + SASSERT(j > i); + for (; j < args.size() && args[j].first == args[i].first; ++j) { + args[i].second += args[j].second; + } + if (j < args.size()) { + args[i+1].first = args[j].first; + args[i+1].second = args[j].second; + ++j; + } + } + if (i + 1 < args.size()) { + args.resize(i+1); + } + TRACE("pb", display(tout << "post-unique:", args, k);); +} + +template +lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU::numeral& k) { + TRACE("pb", display(tout << "pre-normalize:", args, k);); + + // + // Ensure all coefficients are positive: + // c*l + y >= k + // <=> + // c*(1-~l) + y >= k + // <=> + // c - c*~l + y >= k + // <=> + // -c*~l + y >= k - c + // + PBU::numeral sum(0); + for (unsigned i = 0; i < args.size(); ++i) { + PBU::numeral c = args[i].second; + if (c.is_neg()) { + args[i].second = -c; + args[i].first = m_util.negate(args[i].first); + k -= c; + } + sum += args[i].second; + } + // detect tautologies: + if (k <= PBU::numeral::zero()) { + args.reset(); + k = PBU::numeral::zero(); + return l_true; + } + // detect infeasible constraints: + if (sum < k) { + args.reset(); + k = PBU::numeral::one(); + return l_false; + } + + bool all_int = true; + for (unsigned i = 0; all_int && i < args.size(); ++i) { + all_int = args[i].second.is_int(); + } + + if (!all_int) { + // normalize to integers. + PBU::numeral d(denominator(k)); + for (unsigned i = 0; i < args.size(); ++i) { + d = lcm(d, denominator(args[i].second)); + } + SASSERT(!d.is_one()); + k *= d; + for (unsigned i = 0; i < args.size(); ++i) { + args[i].second *= d; + } + } + + // Ensure the largest coefficient is not larger than k: + sum = PBU::numeral::zero(); + for (unsigned i = 0; i < args.size(); ++i) { + PBU::numeral c = args[i].second; + if (c > k) { + args[i].second = k; + } + sum += args[i].second; + } + SASSERT(!args.empty()); + + // normalize tight inequalities to unit coefficients. + if (sum == k) { + for (unsigned i = 0; i < args.size(); ++i) { + args[i].second = PBU::numeral::one(); + } + k = PBU::numeral(args.size()); + } + + // apply cutting plane reduction: + PBU::numeral g(0); + for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) { + PBU::numeral c = args[i].second; + if (c != k) { + if (g.is_zero()) { + g = c; + } + else { + g = gcd(g, c); + } + } + } + if (g.is_zero()) { + // all coefficients are equal to k. + for (unsigned i = 0; i < args.size(); ++i) { + SASSERT(args[i].second == k); + args[i].second = PBU::numeral::one(); + } + k = PBU::numeral::one(); + } + else if (g > PBU::numeral::one()) { + IF_VERBOSE(3, verbose_stream() << "cut " << g << "\n"; + display(verbose_stream(), args, k); + ); + + // + // Example 5x + 5y + 2z + 2u >= 5 + // becomes 3x + 3y + z + u >= 3 + // + PBU::numeral k_new = div(k, g); + if (!(k % g).is_zero()) { // k_new is the ceiling of k / g. + k_new++; + } + for (unsigned i = 0; i < args.size(); ++i) { + SASSERT(args[i].second.is_pos()); + PBU::numeral c = args[i].second; + if (c == k) { + c = k_new; + } + else { + c = div(c, g); + } + args[i].second = c; + SASSERT(args[i].second.is_pos()); + } + k = k_new; + } + // + // normalize coefficients that fall within a range + // k/n <= ... < k/(n-1) for some n = 1,2,... + // + // e.g, k/n <= min <= max < k/(n-1) + // k/min <= n, n-1 < k/max + // . floor(k/max) = ceil(k/min) - 1 + // . floor(k/max) < k/max + // + // example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2 + // replace all coefficients by 1, and k by 2. + // + if (!k.is_one()) { + PBU::numeral min = args[0].second, max = args[0].second; + for (unsigned i = 1; i < args.size(); ++i) { + if (args[i].second < min) min = args[i].second; + if (args[i].second > max) max = args[i].second; + } + PBU::numeral n0 = k/max; + PBU::numeral n1 = floor(n0); + PBU::numeral n2 = ceil(k/min) - PBU::numeral::one(); + if (n1 == n2 && !n0.is_int()) { + IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k);); + + for (unsigned i = 0; i < args.size(); ++i) { + args[i].second = PBU::numeral::one(); + } + k = n1 + PBU::numeral::one(); + } + } + return l_undef; +} + + +template +void pb_rewriter_util::prune(typename PBU::args_t& args, typename PBU::numeral& k) { + + PBU::numeral nlt(0); + unsigned occ = 0; + for (unsigned i = 0; nlt < k && i < args.size(); ++i) { + if (args[i].second < k) { + nlt += args[i].second; + ++occ; + } + } + if (0 < occ && nlt < k) { + + for (unsigned i = 0; i < args.size(); ++i) { + if (args[i].second < k) { + args[i] = args.back(); + args.pop_back(); + --i; + } + } + normalize(args, k); + } +} + +#endif diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index b9a9cfbcc..6fae39bad 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -374,7 +374,7 @@ namespace opt { } } - smt::theory_weighted_maxsat& ensure_theory() { + smt::theory_weighted_maxsat* ensure_theory() { smt::theory_weighted_maxsat* wth = get_theory(); if (wth) { wth->reset(); @@ -383,7 +383,7 @@ namespace opt { wth = alloc(smt::theory_weighted_maxsat, m, s); s.get_context().register_plugin(wth); } - return *wth; + return wth; } /** @@ -420,16 +420,26 @@ namespace opt { mdl = m_model.get(); } - + class scoped_ensure_theory { + smt::theory_weighted_maxsat* m_wth; + public: + scoped_ensure_theory(imp& i) { + m_wth = i.ensure_theory(); + } + ~scoped_ensure_theory() { + m_wth->reset(); + } + smt::theory_weighted_maxsat& operator()() { return *m_wth; } + }; lbool incremental_solve() { TRACE("opt", tout << "weighted maxsat\n";); - smt::theory_weighted_maxsat& wth = ensure_theory(); + scoped_ensure_theory wth(*this); solver::scoped_push _s(s); lbool is_sat = l_true; bool was_sat = false; for (unsigned i = 0; i < m_soft.size(); ++i) { - wth.assert_weighted(m_soft[i].get(), m_weights[i]); + wth().assert_weighted(m_soft[i].get(), m_weights[i]); } solver::scoped_push __s(s); while (l_true == is_sat) { @@ -438,27 +448,27 @@ namespace opt { is_sat = l_undef; } if (is_sat == l_true) { - if (wth.is_optimal()) { + if (wth().is_optimal()) { s.get_model(m_model); } - expr_ref fml = wth.mk_block(); + expr_ref fml = wth().mk_block(); s.assert_expr(fml); was_sat = true; } } if (was_sat) { - wth.get_assignment(m_assignment); + wth().get_assignment(m_assignment); } if (is_sat == l_false && was_sat) { is_sat = l_true; } - m_upper = wth.get_min_cost(); + m_upper = wth().get_min_cost(); if (is_sat == l_true) { m_lower = m_upper; } TRACE("opt", tout << "min cost: " << m_upper << "\n";); - return is_sat; - } + return is_sat; + } /** Iteratively increase cost until there is an assignment during @@ -468,13 +478,13 @@ namespace opt { */ lbool iterative_solve() { - smt::theory_weighted_maxsat& wth = ensure_theory(); + scoped_ensure_theory wth(*this); solver::scoped_push _s(s); for (unsigned i = 0; i < m_soft.size(); ++i) { - wth.assert_weighted(m_soft[i].get(), m_weights[i]); + wth().assert_weighted(m_soft[i].get(), m_weights[i]); } solver::scoped_push __s(s); - rational cost = wth.get_min_cost(); + rational cost = wth().get_min_cost(); rational log_cost(1), tmp(1); while (tmp < cost) { ++log_cost; @@ -486,7 +496,7 @@ namespace opt { unsigned nsc = 0; m_upper = cost; while (log_cost <= cost && result == l_false) { - bound = wth.set_min_cost(log_cost); + bound = wth().set_min_cost(log_cost); s.push_core(); ++nsc; IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";); @@ -538,32 +548,32 @@ namespace opt { lbool bisection_solve() { TRACE("opt", tout << "weighted maxsat\n";); - smt::theory_weighted_maxsat& wth = ensure_theory(); + scoped_ensure_theory wth(*this); solver::scoped_push _s(s); lbool is_sat = l_true; bool was_sat = false; expr_ref_vector bounds(m); for (unsigned i = 0; i < m_soft.size(); ++i) { - wth.assert_weighted(m_soft[i].get(), m_weights[i]); + wth().assert_weighted(m_soft[i].get(), m_weights[i]); } solver::scoped_push __s(s); m_lower = rational::zero(); - m_upper = wth.get_min_cost(); - while (m_lower < m_upper) { + m_upper = wth().get_min_cost(); + while (m_lower < m_upper && is_sat != l_undef) { rational cost = div(m_upper + m_lower, rational(2)); - bounds.push_back(wth.set_min_cost(cost)); + bounds.push_back(wth().set_min_cost(cost)); is_sat = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1); if (m_cancel) { is_sat = l_undef; } switch(is_sat) { case l_true: { - if (wth.is_optimal()) { + if (wth().is_optimal()) { s.get_model(m_model); } - expr_ref fml = wth.mk_block(); + expr_ref fml = wth().mk_block(); s.assert_expr(fml); - m_upper = wth.get_min_cost(); + m_upper = wth().get_min_cost(); break; } case l_false: { @@ -572,8 +582,8 @@ namespace opt { break; } case l_undef: - return l_undef; - } + break; + } } if (was_sat) { is_sat = l_true; diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index a80f55de8..4fa9e75c7 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -473,7 +473,8 @@ namespace smt { */ template bool theory_arith::mk_gomory_cut(row const & r) { - SASSERT(!all_coeff_int(r)); + // The following assertion is wrong. It may be violated in mixed-integer problems. + // SASSERT(!all_coeff_int(r)); theory_var x_i = r.get_base_var(); SASSERT(is_int(x_i)); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index df71ce969..8c9be4659 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -24,9 +24,43 @@ Notes: #include "sorting_network.h" #include "uint_set.h" #include "smt_model_generator.h" +#include "pb_rewriter_def.h" namespace smt { + class pb_lit_rewriter_util { + public: + typedef std::pair arg_t; + typedef vector args_t; + typedef rational numeral; + + literal negate(literal l) { + return ~l; + } + + void display(std::ostream& out, literal l) { + out << l; + } + + bool is_negated(literal l) const { + return l.sign(); + } + + bool is_true(literal l) const { + return l == true_literal; + } + + bool is_false(literal l) const { + return l == false_literal; + } + + struct compare { + bool operator()(arg_t const& a, arg_t const& b) { + return a.first < b.first; + } + }; + }; + void theory_pb::ineq::negate() { m_lit.neg(); numeral sum(0); @@ -52,245 +86,21 @@ namespace smt { void theory_pb::ineq::unique() { - numeral& k = m_k; - arg_t& args = m_args; - // normalize first all literals to be positive: - // then we can compare them more easily. - for (unsigned i = 0; i < size(); ++i) { - if (lit(i).sign()) { - args[i].first.neg(); - k -= coeff(i); - args[i].second = -coeff(i); - } - } - // remove constants - for (unsigned i = 0; i < size(); ++i) { - if (lit(i) == true_literal) { - k += coeff(i); - std::swap(args[i], args[size()-1]); - args.pop_back(); - } - else if (lit(i) == false_literal) { - std::swap(args[i], args[size()-1]); - args.pop_back(); - } - } - // sort and coalesce arguments: - std::sort(args.begin(), args.end()); - - unsigned i = 0, j = 1; - for (; j < size(); ++i) { - SASSERT(j > i); - literal l = lit(i); - for (; j < size() && lit(j) == lit(i); ++j) { - args[i].second += coeff(j); - } - if (j < size()) { - args[i+1].first = lit(j); - args[i+1].second = coeff(j); - ++j; - } - } - if (i + 1 < size()) { - args.resize(i+1); - } + pb_lit_rewriter_util pbu; + pb_rewriter_util util(pbu); + util.unique(m_args, m_k); } void theory_pb::ineq::prune() { - numeral& k = m_k; - arg_t& args = m_args; - numeral nlt(0); - unsigned occ = 0; - for (unsigned i = 0; nlt < k && i < size(); ++i) { - if (coeff(i) < k) { - nlt += coeff(i); - ++occ; - } - } - if (0 < occ && nlt < k) { - IF_VERBOSE(2, verbose_stream() << "prune\n"; - for (unsigned i = 0; i < size(); ++i) { - verbose_stream() << coeff(i) << "*" << lit(i) << " "; - } - verbose_stream() << " >= " << k << "\n"; - ); - - for (unsigned i = 0; i < size(); ++i) { - if (coeff(i) < k) { - args[i] = args.back(); - args.pop_back(); - --i; - } - } - normalize(); - - } + pb_lit_rewriter_util pbu; + pb_rewriter_util util(pbu); + util.prune(m_args, m_k); } lbool theory_pb::ineq::normalize() { - - numeral& k = m_k; - arg_t& args = m_args; - - // - // Ensure all coefficients are positive: - // c*l + y >= k - // <=> - // c*(1-~l) + y >= k - // <=> - // c - c*~l + y >= k - // <=> - // -c*~l + y >= k - c - // - numeral sum(0); - for (unsigned i = 0; i < size(); ++i) { - numeral c = coeff(i); - if (c.is_neg()) { - args[i].second = -c; - args[i].first = ~lit(i); - k -= c; - } - sum += coeff(i); - } - // detect tautologies: - if (k <= numeral::zero()) { - args.reset(); - k = numeral::zero(); - return l_true; - } - // detect infeasible constraints: - if (sum < k) { - args.reset(); - k = numeral::one(); - return l_false; - } - - bool all_int = true; - for (unsigned i = 0; all_int && i < size(); ++i) { - all_int = coeff(i).is_int(); - } - - if (!all_int) { - // normalize to integers. - numeral d(denominator(k)); - for (unsigned i = 0; i < size(); ++i) { - d = lcm(d, denominator(coeff(i))); - } - SASSERT(!d.is_one()); - k *= d; - for (unsigned i = 0; i < size(); ++i) { - args[i].second *= d; - } - } - - // Ensure the largest coefficient is not larger than k: - sum = numeral::zero(); - for (unsigned i = 0; i < size(); ++i) { - numeral c = coeff(i); - if (c > k) { - args[i].second = k; - } - sum += coeff(i); - } - SASSERT(!args.empty()); - - // normalize tight inequalities to unit coefficients. - if (sum == k) { - for (unsigned i = 0; i < size(); ++i) { - args[i].second = numeral::one(); - } - k = numeral(size()); - } - - // apply cutting plane reduction: - numeral g(0); - for (unsigned i = 0; !g.is_one() && i < size(); ++i) { - numeral c = coeff(i); - if (c != k) { - if (g.is_zero()) { - g = c; - } - else { - g = gcd(g, c); - } - } - } - if (g.is_zero()) { - // all coefficients are equal to k. - for (unsigned i = 0; i < size(); ++i) { - SASSERT(coeff(i) == k); - args[i].second = numeral::one(); - } - k = numeral::one(); - } - else if (g > numeral::one()) { - IF_VERBOSE(2, verbose_stream() << "cut " << g << "\n"; - for (unsigned i = 0; i < size(); ++i) { - verbose_stream() << coeff(i) << "*" << lit(i) << " "; - } - verbose_stream() << " >= " << k << "\n"; - ); - - // - // Example 5x + 5y + 2z + 2u >= 5 - // becomes 3x + 3y + z + u >= 3 - // - numeral k_new = div(k, g); - if (!(k % g).is_zero()) { // k_new is the ceiling of k / g. - k_new++; - } - for (unsigned i = 0; i < size(); ++i) { - SASSERT(coeff(i).is_pos()); - numeral c = coeff(i); - if (c == k) { - c = k_new; - } - else { - c = div(c, g); - } - args[i].second = c; - SASSERT(coeff(i).is_pos()); - } - k = k_new; - } - // - // normalize coefficients that fall within a range - // k/n <= ... < k/(n-1) for some n = 1,2,... - // - // e.g, k/n <= min <= max < k/(n-1) - // k/min <= n, n-1 < k/max - // . floor(k/max) = ceil(k/min) - 1 - // . floor(k/max) < k/max - // - // example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2 - // replace all coefficients by 1, and k by 2. - // - if (!k.is_one()) { - numeral min = coeff(0), max = coeff(0); - for (unsigned i = 1; i < size(); ++i) { - if (coeff(i) < min) min = coeff(i); - if (coeff(i) > max) max = coeff(i); - } - numeral n0 = k/max; - numeral n1 = floor(n0); - numeral n2 = ceil(k/min) - numeral::one(); - if (n1 == n2 && !n0.is_int()) { - IF_VERBOSE(2, verbose_stream() << "set cardinality\n"; - for (unsigned i = 0; i < size(); ++i) { - verbose_stream() << coeff(i) << "*" << lit(i) << " "; - } - verbose_stream() << " >= " << k << "\n"; - ); - - for (unsigned i = 0; i < size(); ++i) { - args[i].second = numeral::one(); - } - k = n1 + numeral::one(); - } - } - - SASSERT(well_formed()); - return l_undef; + pb_lit_rewriter_util pbu; + pb_rewriter_util util(pbu); + return util.normalize(m_args, m_k); } app_ref theory_pb::ineq::to_expr(context& ctx, ast_manager& m) { @@ -403,6 +213,7 @@ namespace smt { break; } +#if 0 // TBD: special cases: k == 1, or args.size() == 1 if (c->k().is_one()) { @@ -416,7 +227,7 @@ namespace smt { ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); return true; } - +#endif // maximal coefficient: numeral& max_watch = c->m_max_watch; diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp new file mode 100644 index 000000000..60bda3c18 --- /dev/null +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -0,0 +1,185 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + pb_preprocess_tactic.cpp + +Abstract: + + Pre-process pseudo-Boolean inequalities using + generalized Davis Putnam (resolution) to eliminate variables. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-23 + +Notes: + +--*/ +#include "pb_preprocess_tactic.h" +#include "tactical.h" +#include "for_each_expr.h" +#include "pb_decl_plugin.h" + +class pb_preprocess_tactic : public tactic { + struct rec { unsigned pos, neg; rec() { pos = neg = 0; } }; + typedef obj_map var_map; + ast_manager& m; + pb_util pb; + var_map m_vars; + ptr_vector m_ge; + ptr_vector m_other; + + struct declassifier { + obj_map& m_vars; + declassifier(obj_map& v): m_vars(v) {} + + void operator()(app* e) { + if (m_vars.contains(e)) { + m_vars.remove(e); + } + } + void operator()(var* e) {} + void operator()(quantifier* q) {} + }; + +public: + pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): + m(m), pb(m) {} + + virtual ~pb_preprocess_tactic() {} + + virtual tactic * translate(ast_manager & m) { + return alloc(pb_preprocess_tactic, m); + } + + 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; + + reset(); + for (unsigned i = 0; i < g->size(); i++) { + process_vars(g->form(i)); + } + + if (m_ge.empty()) { + result.push_back(g.get()); + return; + } + + for (unsigned i = 0; i < m_ge.size(); ++i) { + classify_vars(m_ge[i]); + } + + declassifier dcl(m_vars); + expr_mark visited; + for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) { + for_each_expr(dcl, visited, m_other[i]); + } + + if (m_vars.empty()) { + result.push_back(g.get()); + return; + } + + var_map::iterator it = next_resolvent(m_vars.begin()); + while (it != m_vars.end()) { + expr * e = it->m_key; + it->m_value.pos; + it->m_value.neg; + + it = next_resolvent(it); + } + + g->inc_depth(); + result.push_back(g.get()); + } + + virtual void set_cancel(bool f) { + } + + virtual void updt_params(params_ref const & p) { + } + + virtual void cleanup() { + } + +private: + + void reset() { + m_ge.reset(); + m_other.reset(); + m_vars.reset(); + } + + void process_vars(expr* e) { + if (pb.is_ge(e) && pure_args(to_app(e))) { + m_ge.push_back(to_app(e)); + } + else if (m.is_or(e) && pure_args(to_app(e))) { + m_ge.push_back(to_app(e)); + } + else { + m_other.push_back(e); + } + } + + void classify_vars(app* e) { + expr* r; + for (unsigned i = 0; i < e->get_num_args(); ++i) { + if (m.is_true(e) || m.is_false(e)) { + // no-op + } + else if (m.is_not(e, r)) { + insert(r, false); + } + else { + insert(e, true); + } + } + } + + void insert(expr* e, bool pos) { + if (!m_vars.contains(e)) { + m_vars.insert(e, rec()); + } + if (pos) { + m_vars.find(e).pos++; + } + else { + m_vars.find(e).neg++; + } + } + + bool pure_args(app* a) const { + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* e = a->get_arg(i); + m.is_not(e, e); + if (!is_uninterp_const(e) && !m.is_true(e) && !m.is_false(e)) { + return false; + } + } + return true; + } + + var_map::iterator next_resolvent(var_map::iterator it) { + if (it == m_vars.end()) { + return it; + } + while (it != m_vars.end() && it->m_value.pos != 1 && it->m_value.neg != 1) { + ++it; + } + return it; + } +}; + + +tactic * mk_pb_preprocess_tactic(ast_manager & m, params_ref const & p) { + return alloc(pb_preprocess_tactic, m); +} diff --git a/src/tactic/core/pb_preprocess_tactic.h b/src/tactic/core/pb_preprocess_tactic.h new file mode 100644 index 000000000..5746779b7 --- /dev/null +++ b/src/tactic/core/pb_preprocess_tactic.h @@ -0,0 +1,34 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + pb_preprocess_tactic.h + +Abstract: + + Pre-process pseudo-Boolean inequalities using + generalized Davis Putnam (resolution) to eliminate variables. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-23 + +Notes: + +--*/ +#ifndef _PB_PREPROCESS_TACTIC_H_ +#define _PB_PREPROCESS_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_pb_preprocess_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("pb-preprocess", "pre-process pseudo-Boolean constraints a la Davis Putnam.", "mk_pb_preprocess_tactic(m, p)") +*/ + + +#endif