mirror of
https://github.com/Z3Prover/z3
synced 2025-08-08 12:11:23 +00:00
working on pb pre-processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
0c2ec6951a
commit
70c4432bb4
2 changed files with 139 additions and 66 deletions
|
|
@ -61,25 +61,34 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
|
||||||
// sort and coalesce arguments:
|
// sort and coalesce arguments:
|
||||||
PBU::compare cmp;
|
PBU::compare cmp;
|
||||||
std::sort(args.begin(), args.end(), cmp);
|
std::sort(args.begin(), args.end(), cmp);
|
||||||
|
|
||||||
unsigned i = 0, j = 1;
|
// coallesce
|
||||||
for (; j < args.size(); ++i) {
|
unsigned i, j;
|
||||||
SASSERT(j > i);
|
for (i = 0, j = 1; j < args.size(); ++j) {
|
||||||
for (; j < args.size() && args[j].first == args[i].first; ++j) {
|
if (args[i].first == args[j].first) {
|
||||||
args[i].second += args[j].second;
|
args[i].second += args[j].second;
|
||||||
}
|
}
|
||||||
if (args[i].second.is_zero()) {
|
else {
|
||||||
--i;
|
++i;
|
||||||
}
|
args[i] = args[j];
|
||||||
if (j < args.size()) {
|
|
||||||
args[i+1].first = args[j].first;
|
|
||||||
args[i+1].second = args[j].second;
|
|
||||||
++j;
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (i + 1 < args.size()) {
|
if (i + 1 < args.size()) {
|
||||||
args.resize(i+1);
|
args.resize(i+1);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// remove 0s.
|
||||||
|
for (i = 0, j = 0; j < args.size(); ++j) {
|
||||||
|
if (!args[j].second.is_zero()) {
|
||||||
|
if (i != j) {
|
||||||
|
args[i] = args[j];
|
||||||
|
}
|
||||||
|
++i;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (i < args.size()) {
|
||||||
|
args.resize(i);
|
||||||
|
}
|
||||||
TRACE("pb", display(tout << "post-unique:", args, k););
|
TRACE("pb", display(tout << "post-unique:", args, k););
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -87,6 +96,12 @@ template<typename PBU>
|
||||||
lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k) {
|
lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k) {
|
||||||
TRACE("pb", display(tout << "pre-normalize:", args, k););
|
TRACE("pb", display(tout << "pre-normalize:", args, k););
|
||||||
|
|
||||||
|
bool found = false;
|
||||||
|
for (unsigned i = 0; !found && i < args.size(); ++i) {
|
||||||
|
found = args[i].second.is_zero();
|
||||||
|
}
|
||||||
|
if (found) display(std::cout, args, k);
|
||||||
|
SASSERT(!found);
|
||||||
//
|
//
|
||||||
// Ensure all coefficients are positive:
|
// Ensure all coefficients are positive:
|
||||||
// c*l + y >= k
|
// c*l + y >= k
|
||||||
|
|
@ -223,6 +238,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
|
||||||
if (args[i].second < min) min = args[i].second;
|
if (args[i].second < min) min = args[i].second;
|
||||||
if (args[i].second > max) max = args[i].second;
|
if (args[i].second > max) max = args[i].second;
|
||||||
}
|
}
|
||||||
|
SASSERT(min.is_pos());
|
||||||
PBU::numeral n0 = k/max;
|
PBU::numeral n0 = k/max;
|
||||||
PBU::numeral n1 = floor(n0);
|
PBU::numeral n1 = floor(n0);
|
||||||
PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
|
PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
|
||||||
|
|
@ -259,6 +275,7 @@ void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::nume
|
||||||
--i;
|
--i;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
unique(args, k);
|
||||||
normalize(args, k);
|
normalize(args, k);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -31,8 +31,8 @@ class pb_preprocess_tactic : public tactic {
|
||||||
ast_manager& m;
|
ast_manager& m;
|
||||||
pb_util pb;
|
pb_util pb;
|
||||||
var_map m_vars;
|
var_map m_vars;
|
||||||
app_ref_vector m_ge;
|
unsigned_vector m_ge;
|
||||||
expr_ref_vector m_other;
|
unsigned_vector m_other;
|
||||||
th_rewriter m_r;
|
th_rewriter m_r;
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -51,7 +51,7 @@ class pb_preprocess_tactic : public tactic {
|
||||||
|
|
||||||
public:
|
public:
|
||||||
pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()):
|
pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()):
|
||||||
m(m), pb(m), m_ge(m), m_other(m), m_r(m) {}
|
m(m), pb(m), m_r(m) {}
|
||||||
|
|
||||||
virtual ~pb_preprocess_tactic() {}
|
virtual ~pb_preprocess_tactic() {}
|
||||||
|
|
||||||
|
|
@ -70,7 +70,7 @@ public:
|
||||||
|
|
||||||
reset();
|
reset();
|
||||||
for (unsigned i = 0; i < g->size(); ++i) {
|
for (unsigned i = 0; i < g->size(); ++i) {
|
||||||
process_vars(g->form(i));
|
process_vars(i, g->form(i));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (m_ge.empty()) {
|
if (m_ge.empty()) {
|
||||||
|
|
@ -78,15 +78,14 @@ public:
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < m_ge.size(); ++i) {
|
for (unsigned i = 0; i < m_ge.size(); ++i) {
|
||||||
classify_vars(i, m_ge[i].get());
|
classify_vars(i, to_app(g->form(m_ge[i])));
|
||||||
}
|
}
|
||||||
|
|
||||||
declassifier dcl(m_vars);
|
declassifier dcl(m_vars);
|
||||||
expr_mark visited;
|
expr_mark visited;
|
||||||
for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) {
|
for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) {
|
||||||
for_each_expr(dcl, visited, m_other[i].get());
|
for_each_expr(dcl, visited, g->form(m_other[i]));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (m_vars.empty()) {
|
if (m_vars.empty()) {
|
||||||
|
|
@ -95,38 +94,37 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
g->inc_depth();
|
g->inc_depth();
|
||||||
|
// first eliminate variables
|
||||||
var_map::iterator it = next_resolvent(m_vars.begin());
|
var_map::iterator it = next_resolvent(m_vars.begin());
|
||||||
while (it != m_vars.end()) {
|
while (it != m_vars.end()) {
|
||||||
expr * e = it->m_key;
|
expr * e = it->m_key;
|
||||||
if (it->m_value.pos.empty()) {
|
rec const& r = it->m_value;
|
||||||
replace(it->m_value.neg, e, m.mk_false());
|
if (r.pos.empty()) {
|
||||||
|
replace(r.neg, e, m.mk_false(), g);
|
||||||
}
|
}
|
||||||
else if (it->m_value.neg.empty()) {
|
else if (r.neg.empty()) {
|
||||||
replace(it->m_value.pos, e, m.mk_true());
|
replace(r.pos, e, m.mk_true(), g);
|
||||||
}
|
|
||||||
else if (it->m_value.pos.size() == 1) {
|
|
||||||
resolve(it->m_value.pos[0], it->m_value.neg, e, true);
|
|
||||||
}
|
|
||||||
else if (it->m_value.neg.size() == 1) {
|
|
||||||
resolve(it->m_value.neg[0], it->m_value.pos, e, false);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
|
|
||||||
}
|
}
|
||||||
++it;
|
++it;
|
||||||
it = next_resolvent(it);
|
it = next_resolvent(it);
|
||||||
// FIXME: some but not all indices are invalidated.
|
|
||||||
}
|
}
|
||||||
|
// now resolve clauses.
|
||||||
g->reset();
|
it = next_resolvent(m_vars.begin());
|
||||||
for (unsigned i = 0; i < m_ge.size(); ++i) {
|
while (it != m_vars.end()) {
|
||||||
g->assert_expr(m_ge[i].get());
|
expr * e = it->m_key;
|
||||||
|
rec const& r = it->m_value;
|
||||||
|
if (r.pos.size() == 1) {
|
||||||
|
resolve(r.pos[0], r.neg, e, true, g);
|
||||||
|
}
|
||||||
|
else if (r.neg.size() == 1) {
|
||||||
|
resolve(r.neg[0], r.pos, e, false, g);
|
||||||
|
}
|
||||||
|
++it;
|
||||||
|
it = next_resolvent(it);
|
||||||
}
|
}
|
||||||
|
|
||||||
for (unsigned i = 0; i < m_other.size(); ++i) {
|
|
||||||
g->assert_expr(m_other[i].get());
|
|
||||||
}
|
|
||||||
|
|
||||||
|
g->elim_true();
|
||||||
|
|
||||||
result.push_back(g.get());
|
result.push_back(g.get());
|
||||||
}
|
}
|
||||||
|
|
@ -148,22 +146,23 @@ private:
|
||||||
m_vars.reset();
|
m_vars.reset();
|
||||||
}
|
}
|
||||||
|
|
||||||
void process_vars(expr* e) {
|
|
||||||
|
void process_vars(unsigned i, expr* e) {
|
||||||
expr* r;
|
expr* r;
|
||||||
if (is_uninterp_const(e)) {
|
if (is_uninterp_const(e)) {
|
||||||
m_ge.push_back(to_app(e));
|
m_ge.push_back(i);
|
||||||
}
|
}
|
||||||
else if (pb.is_ge(e) && pure_args(to_app(e))) {
|
else if (pb.is_ge(e) && pure_args(to_app(e))) {
|
||||||
m_ge.push_back(to_app(e));
|
m_ge.push_back(i);
|
||||||
}
|
}
|
||||||
else if (m.is_or(e) && pure_args(to_app(e))) {
|
else if (m.is_or(e) && pure_args(to_app(e))) {
|
||||||
m_ge.push_back(to_app(e));
|
m_ge.push_back(i);
|
||||||
}
|
}
|
||||||
else if (m.is_not(e, r) && is_uninterp_const(r)) {
|
else if (m.is_not(e, r) && is_uninterp_const(r)) {
|
||||||
m_ge.push_back(to_app(e));
|
m_ge.push_back(i);
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
m_other.push_back(e);
|
m_other.push_back(i);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -231,11 +230,43 @@ private:
|
||||||
return rational::zero();
|
return rational::zero();
|
||||||
}
|
}
|
||||||
|
|
||||||
void resolve(unsigned idx, unsigned_vector const& positions, expr* e, bool pos) {
|
//
|
||||||
app* fml = m_ge[idx].get();
|
// one of the formulas are replaced by T after resolution
|
||||||
|
// so if there is a pointer into that formula, we can no
|
||||||
|
// longer assume variables have unique occurrences.
|
||||||
|
//
|
||||||
|
bool is_valid(unsigned_vector const& positions, goal_ref const& g) const {
|
||||||
|
for (unsigned i = 0; i < positions.size(); ++i) {
|
||||||
|
unsigned idx = positions[i];
|
||||||
|
if (m.is_true(g->form(idx))) return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool is_reduction(unsigned_vector const& pos, app* fml, goal_ref const& g) {
|
||||||
|
unsigned sz = fml->get_num_args();
|
||||||
|
for (unsigned i = 0; i < pos.size(); ++i) {
|
||||||
|
if (!is_app(g->form(pos[i]))) return false;
|
||||||
|
if (to_app(g->form(pos[i]))->get_num_args() < sz) return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
void resolve(unsigned idx1, unsigned_vector const& positions, expr* e, bool pos, goal_ref const& g) {
|
||||||
|
if (!is_app(g->form(idx1))) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
app* fml = to_app(g->form(idx1));
|
||||||
if (m.is_true(fml)) {
|
if (m.is_true(fml)) {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
if (!is_valid(positions, g)) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
if (positions.size() > 1 && !is_reduction(positions, fml, g)) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
IF_VERBOSE(1, verbose_stream() << "resolving: " << mk_pp(fml, m) << "\n";);
|
||||||
m_r.set_substitution(0);
|
m_r.set_substitution(0);
|
||||||
expr_ref tmp1(m), tmp2(m), e1(m), e2(m);
|
expr_ref tmp1(m), tmp2(m), e1(m), e2(m);
|
||||||
ptr_vector<expr> args;
|
ptr_vector<expr> args;
|
||||||
|
|
@ -251,26 +282,49 @@ private:
|
||||||
}
|
}
|
||||||
VERIFY(to_ge(fml, args, coeffs, k1));
|
VERIFY(to_ge(fml, args, coeffs, k1));
|
||||||
c1 = get_coeff(args.size(), args.c_ptr(), coeffs.c_ptr(), e1);
|
c1 = get_coeff(args.size(), args.c_ptr(), coeffs.c_ptr(), e1);
|
||||||
|
if (c1.is_zero()) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
unsigned sz = coeffs.size();
|
unsigned sz = coeffs.size();
|
||||||
for (unsigned i = 0; i < positions.size(); ++i) {
|
for (unsigned i = 0; i < positions.size(); ++i) {
|
||||||
SASSERT(positions[i] != idx); // rely on simplification
|
unsigned idx2 = positions[i];
|
||||||
app* fml2 = m_ge[positions[i]].get();
|
if (idx2 == idx1) {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
app* fml2 = to_app(g->form(idx2));
|
||||||
if (m.is_true(fml2)) continue;
|
if (m.is_true(fml2)) continue;
|
||||||
VERIFY(to_ge(fml2, args, coeffs, k2));
|
VERIFY(to_ge(fml2, args, coeffs, k2));
|
||||||
c2 = get_coeff(args.size()-sz, args.c_ptr()+sz, coeffs.c_ptr()+sz, e2);
|
c2 = get_coeff(args.size()-sz, args.c_ptr()+sz, coeffs.c_ptr()+sz, e2);
|
||||||
std::cout << "coeffs: " << c1 << " " << c2 << "\n";
|
if (!c2.is_zero()) {
|
||||||
tmp1 = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), k1 + k2);
|
rational m1(1), m2(1);
|
||||||
m_r(tmp1, tmp2);
|
if (c1 != c2) {
|
||||||
TRACE("pb", tout << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
|
rational lc = lcm(c1, c2);
|
||||||
IF_VERBOSE(1, verbose_stream() << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
|
m1 = lc/c1;
|
||||||
#if 0
|
m2 = lc/c2;
|
||||||
m_ge[positions[i]] = tmp2;
|
for (unsigned j = 0; j < sz; ++j) {
|
||||||
#endif
|
coeffs[j] *= m1;
|
||||||
|
}
|
||||||
|
for (unsigned j = sz; j < args.size(); ++j) {
|
||||||
|
coeffs[j] *= m2;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
tmp1 = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), m1*k1 + m2*k2);
|
||||||
|
m_r(tmp1, tmp2);
|
||||||
|
TRACE("pb", tout << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
|
||||||
|
IF_VERBOSE(1, verbose_stream() << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
|
||||||
|
|
||||||
|
g->update(idx2, tmp2); // proof & dependencies
|
||||||
|
|
||||||
|
if (!m1.is_one()) {
|
||||||
|
for (unsigned j = 0; j < sz; ++j) {
|
||||||
|
coeffs[j] /= m1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
args.resize(sz);
|
args.resize(sz);
|
||||||
coeffs.resize(sz);
|
coeffs.resize(sz);
|
||||||
}
|
}
|
||||||
|
g->update(idx1, m.mk_true()); // proof & dependencies
|
||||||
// m_ge[idx] = m.mk_true();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
bool to_ge(app* e, ptr_vector<expr>& args, vector<rational>& coeffs, rational& k) {
|
bool to_ge(app* e, ptr_vector<expr>& args, vector<rational>& coeffs, rational& k) {
|
||||||
|
|
@ -307,18 +361,20 @@ private:
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
void replace(unsigned_vector const& positions, expr* e, expr* v) {
|
void replace(unsigned_vector const& positions, expr* e, expr* v, goal_ref const& g) {
|
||||||
|
if (!is_valid(positions, g)) return;
|
||||||
expr_substitution sub(m);
|
expr_substitution sub(m);
|
||||||
sub.insert(e, v);
|
sub.insert(e, v);
|
||||||
expr_ref tmp(m);
|
expr_ref tmp(m);
|
||||||
m_r.set_substitution(&sub);
|
m_r.set_substitution(&sub);
|
||||||
for (unsigned i = 0; i < positions.size(); ++i) {
|
for (unsigned i = 0; i < positions.size(); ++i) {
|
||||||
unsigned idx = positions[i];
|
unsigned idx = positions[i];
|
||||||
if (!m.is_true(m_ge[idx].get())) {
|
expr* f = g->form(idx);
|
||||||
m_r(m_ge[idx].get(), tmp);
|
if (!m.is_true(f)) {
|
||||||
TRACE("pb", tout << mk_pp(m_ge[idx].get(), m) << " -> " << tmp
|
m_r(f, tmp);
|
||||||
|
TRACE("pb", tout << mk_pp(f, m) << " -> " << tmp
|
||||||
<< " by " << mk_pp(e, m) << " |-> " << mk_pp(v, m) << "\n";);
|
<< " by " << mk_pp(e, m) << " |-> " << mk_pp(v, m) << "\n";);
|
||||||
m_ge[idx] = to_app(tmp);
|
g->update(idx, tmp); // proof & dependencies.
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue