3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

enable propagation when there are changed columns

- to fix bug reported by Nikhil Swamy/F*
- deal with some compiler warnings by adding annotations
This commit is contained in:
Nikolaj Bjorner 2025-01-12 13:30:31 -08:00
parent 558758fcf1
commit 85356c5548
3 changed files with 9 additions and 2 deletions

View file

@ -1800,10 +1800,12 @@ namespace lp {
switch (k) {
case LT:
k = LE;
Z3_fallthrough;
case LE:
return floor(bound);
case GT:
k = GE;
Z3_fallthrough;
case GE:
return ceil(bound);
case EQ:
@ -2028,6 +2030,7 @@ namespace lp {
switch (kind) {
case LT:
y_of_bound = -1;
Z3_fallthrough;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
@ -2043,6 +2046,7 @@ namespace lp {
}
case GT:
y_of_bound = 1;
Z3_fallthrough;
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
@ -2145,6 +2149,7 @@ namespace lp {
switch (kind) {
case LT:
y_of_bound = -1;
Z3_fallthrough;
case LE:
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
@ -2156,6 +2161,7 @@ namespace lp {
break;
case GT:
y_of_bound = 1;
Z3_fallthrough;
case GE:
{
auto low = numeric_pair<mpq>(right_side, y_of_bound);
@ -2198,6 +2204,7 @@ namespace lp {
switch (kind) {
case LT:
y_of_bound = -1;
Z3_fallthrough;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;

View file

@ -25,7 +25,7 @@ template < typename B> class stacked_vector {
struct log_entry {
unsigned m_i; unsigned m_ts; B b;
log_entry(unsigned i, unsigned t, B const& b): m_i(i), m_ts(t), b(b) {}
log_entry():m_i(UINT_MAX), m_ts(0) {}
log_entry():m_i(UINT_MAX), m_ts(0), b() {}
};
svector<unsigned> m_stack_of_vector_sizes;
svector<unsigned> m_stack_of_change_sizes;

View file

@ -2131,7 +2131,7 @@ public:
}
bool can_propagate_core() {
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def;
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def || lp().has_changed_columns();
}
bool propagate() {