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

adding pre-processing of BP constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-23 01:33:24 -08:00
parent 670f56e5e4
commit 24f2fd380c
9 changed files with 679 additions and 281 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/pb_decl_plugin.h
View file

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

113
src/ast/rewriter/pb_rewriter.cpp
View file

@ -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<expr*, rational> arg_t;
typedef vector<arg_t> 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<expr*,rational> const& a,
std::pair<expr*,rational> 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<std::pair<expr*,rational> > 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<pb_ast_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;
}

15
src/ast/rewriter/pb_rewriter.h
View file

@ -22,12 +22,27 @@ Notes:
#include"pb_decl_plugin.h"
#include"rewriter_types.h"
#include"params.h"
#include"lbool.h"
template<typename PBU>
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<rational> m_coeffs;
ptr_vector<expr> m_args;
public:
pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {

263
src/ast/rewriter/pb_rewriter_def.h Normal file
View file

@ -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<typename PBU>
void pb_rewriter_util<PBU>::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<typename PBU>
void pb_rewriter_util<PBU>::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<typename PBU>
lbool pb_rewriter_util<PBU>::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<typename PBU>
void pb_rewriter_util<PBU>::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

60
src/opt/weighted_maxsat.cpp
View file

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

3
src/smt/theory_arith_int.h
View file

@ -473,7 +473,8 @@ namespace smt {
*/
template<typename Ext>
bool theory_arith<Ext>::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));

279
src/smt/theory_pb.cpp
View file

@ -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<literal, rational> arg_t;
typedef vector<arg_t> 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<pb_lit_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<pb_lit_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<pb_lit_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;

185
src/tactic/core/pb_preprocess_tactic.cpp Normal file
View file

@ -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<expr, rec> var_map;
ast_manager& m;
pb_util pb;
var_map m_vars;
ptr_vector<app> m_ge;
ptr_vector<expr> m_other;
struct declassifier {
obj_map<expr, rec>& m_vars;
declassifier(obj_map<expr, rec>& 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);
}

34
src/tactic/core/pb_preprocess_tactic.h Normal file
View file

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