mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

#5447

Browse source 
That the bug went away is a fluke. It wasnt fixed.
It is in pb-preprocess, an essentially unused tactic. The special subsumption resolution rule wasn't accounting for membership of all variables.
This commit is contained in:
Nikolaj Bjorner 2021-08-02 09:03:15 -07:00
parent e3be25dad6
commit da8530e2db
1 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -199,7 +199,7 @@ public:
expr* fml = g->form(m_ge[i]); expr* fml = g->form(m_ge[i]);
if (!to_ge(fml, args1, coeffs1, k1)) continue; if (!to_ge(fml, args1, coeffs1, k1)) continue;
if (args1.empty()) continue; if (args1.empty()) continue;
expr* arg = args1[0].get(); expr* arg = args1.get(0);
bool neg = m.is_not(arg, arg); bool neg = m.is_not(arg, arg);
if (!is_uninterp_const(arg)) continue; if (!is_uninterp_const(arg)) continue;
if (!m_vars.contains(to_app(arg))) continue; if (!m_vars.contains(to_app(arg))) continue;
@ -478,24 +478,28 @@ private:
expr_ref_vector args1(m), args2(m); expr_ref_vector args1(m), args2(m);
vector<rational> coeffs1, coeffs2; vector<rational> coeffs1, coeffs2;
rational k1, k2; rational k1, k2;
if (!to_ge(fml1, args1, coeffs1, k1)) return; if (!to_ge(fml1, args1, coeffs1, k1) || !k1.is_one())
if (!k1.is_one()) return; return;
if (!to_ge(g->form(idx2), args2, coeffs2, k2)) return; if (!to_ge(fml2, args2, coeffs2, k2))
return;
// check that each variable in idx1 occurs only in idx2 // check that each variable in idx1 occurs only in idx2
unsigned min_index = 0; unsigned min_index = 0;
rational min_coeff(0); rational min_coeff(0);
unsigned_vector indices; unsigned_vector indices;
for (unsigned i = 0; i < args1.size(); ++i) { for (unsigned i = 0; i < args1.size(); ++i) {
expr* x = args1[i].get(); expr* x = args1.get(i);
m.is_not(x, x); m.is_not(x, x);
if (!is_app(x)) return; if (!is_app(x) || !m_vars.contains(to_app(x)))
if (!m_vars.contains(to_app(x))) return; return;
TRACE("pb", tout << mk_pp(x, m) << "\n";); TRACE("pb", tout << mk_pp(x, m) << "\n";);
rec const& r = m_vars.find(to_app(x)); rec const& r = m_vars.find(to_app(x));
if (r.pos.size() != 1 || r.neg.size() != 1) return; if (r.pos.size() != 1 || r.neg.size() != 1)
if (r.pos[0] != idx2 && r.neg[0] != idx2) return; return;
if (r.pos[0] != idx2 && r.neg[0] != idx2)
return;
bool found = false;
for (unsigned j = 0; j < args2.size(); ++j) { for (unsigned j = 0; j < args2.size(); ++j) {
if (is_complement(args1[i].get(), args2[j].get())) { if (is_complement(args1.get(i), args2.get(j))) {
if (i == 0) { if (i == 0) {
min_coeff = coeffs2[j]; min_coeff = coeffs2[j];
} }
@ -504,12 +508,15 @@ private:
min_index = j; min_index = j;
} }
indices.push_back(j); indices.push_back(j);
found = true;
} }
} }
if (!found)
return;
} }
for (unsigned i = 0; i < indices.size(); ++i) { for (unsigned i = 0; i < indices.size(); ++i) {
unsigned j = indices[i]; unsigned j = indices[i];
expr* arg = args2[j].get(); expr* arg = args2.get(j);
if (j == min_index) { if (j == min_index) {
args2[j] = m.mk_false(); args2[j] = m.mk_false();
} }
@ -521,9 +528,7 @@ private:
tmp1 = pb.mk_ge(args2.size(), coeffs2.data(), args2.data(), k2); tmp1 = pb.mk_ge(args2.size(), coeffs2.data(), args2.data(), k2);
IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n"; IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n";
for (unsigned i = 0; i < args2.size(); ++i) { verbose_stream() << args2 << "\n";
verbose_stream() << mk_pp(args2[i].get(), m) << " ";
}
verbose_stream() << "\n"; verbose_stream() << "\n";
); );
m_r(tmp1, tmp2); m_r(tmp1, tmp2);