mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity

for now, disable FI-lemma if we have to introduce extract-terms

Browse source
This commit is contained in:
Jakob Rath 2023-12-07 14:25:45 +01:00
parent 02ff7efe25
commit 110c62963f
2 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/polysat/viable.cpp
View file

@ -279,8 +279,7 @@ namespace polysat {
// unsigned const lo_parity = ne->interval.lo_val().parity(w); // unsigned const lo_parity = ne->interval.lo_val().parity(w);
// unsigned const hi_parity = ne->interval.hi_val().parity(w); // unsigned const hi_parity = ne->interval.hi_val().parity(w);
// display_one(std::cerr << "try to reduce entry: ", v, ne) << "\n"; display_one(std::cerr << "try to reduce entry: ", v, ne) << "\n";
// std::cerr << "coeff_parity " << k << " lo_parity " << lo_parity << " hi_parity " << hi_parity << "\n";
if (k > 0 && ne->coeff.is_power_of_two()) { if (k > 0 && ne->coeff.is_power_of_two()) {
// reduction of coeff gives us a unit entry // reduction of coeff gives us a unit entry
@ -293,6 +292,8 @@ namespace polysat {
// new_hi = hi[w-1:k] if hi[k-1:0] = 0 // new_hi = hi[w-1:k] if hi[k-1:0] = 0
// hi[w-1:k] + 1 otherwise // hi[w-1:k] + 1 otherwise
// //
// Reference: Fig. 1 (dtrim) in BitvectorsMCSAT
//
pdd const& pdd_lo = ne->interval.lo(); pdd const& pdd_lo = ne->interval.lo();
pdd const& pdd_hi = ne->interval.hi(); pdd const& pdd_hi = ne->interval.hi();
rational const& lo = ne->interval.lo_val(); rational const& lo = ne->interval.lo_val();
@ -317,6 +318,7 @@ namespace polysat {
// we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly // we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly
// new_lo = lo[:k] etc. // new_lo = lo[:k] etc.
// TODO: for now just disable the FI-lemma if this case occurs // TODO: for now just disable the FI-lemma if this case occurs
ne->valid_for_lemma = false;
if (new_lo == new_hi) { if (new_lo == new_hi) {
// empty or full // empty or full
@ -327,7 +329,8 @@ namespace polysat {
ne->coeff = machine_div2k(ne->coeff, k); ne->coeff = machine_div2k(ne->coeff, k);
ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi); ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi);
ne->bit_width -= k; ne->bit_width -= k;
LOG("reduced entry to unit in width " << ne->bit_width); display_one(std::cerr << "reduced entry: ", v, ne) << "\n";
LOG("reduced entry to unit in bitwidth " << ne->bit_width);
return intersect(v, ne); return intersect(v, ne);
} }
@ -382,6 +385,9 @@ namespace polysat {
}; };
if (ne->interval.is_full()) { if (ne->interval.is_full()) {
// for (auto const& l : m_units[v].get_layers())
// while (l.entries)
// remove_entry(l.entries);
while (entries) while (entries)
remove_entry(entries); remove_entry(entries);
entries = create_entry(); entries = create_entry();

2
src/math/polysat/viable.h
View file

@ -54,6 +54,7 @@ namespace polysat {
bool refined = false; bool refined = false;
/// whether the entry is part of the current set of intervals, or stashed away for backtracking /// whether the entry is part of the current set of intervals, or stashed away for backtracking
bool active = true; bool active = true;
bool valid_for_lemma = true;
pvar var = null_var; pvar var = null_var;
void reset() { void reset() {
@ -61,6 +62,7 @@ namespace polysat {
fi_record::reset(); fi_record::reset();
refined = false; refined = false;
active = true; active = true;
valid_for_lemma = true;
var = null_var; var = null_var;
} }
}; };