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

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-07 14:08:33 -07:00
parent 1589e7dafa
commit f41769cdcf
3 changed files with 42 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polynomial/polynomial.cpp
View file

@ -6181,9 +6181,11 @@ namespace polynomial {
} }
return false; return false;
} }
if (!m_manager.ge(a1, a2)) if (m_manager.eq(a1, a2) || (m1->is_square() && m_manager.ge(a1, a2))) {
return false;
++i, ++j; ++i, ++j;
continue;
}
return false;
} }
return i == sz1 && j == sz2; return i == sz1 && j == sz2;
} }

33
src/nlsat/nlsat_solver.cpp
View file

@ -1733,7 +1733,7 @@ namespace nlsat {
if (!simplify()) if (!simplify())
return l_false; return l_false;
} }
IF_VERBOSE(3, verbose_stream() << "search\n");
sort_watched_clauses(); sort_watched_clauses();
lbool r = search_check(); lbool r = search_check();
CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout););
@ -2792,6 +2792,7 @@ namespace nlsat {
vector<ptr_vector<clause>> m_var_occurs; vector<ptr_vector<clause>> m_var_occurs;
bool simplify() { bool simplify() {
IF_VERBOSE(3, display(verbose_stream() << "before\n"));
unsigned sz = m_clauses.size(); unsigned sz = m_clauses.size();
while (true) { while (true) {
@ -2815,7 +2816,7 @@ namespace nlsat {
sz = m_clauses.size(); sz = m_clauses.size();
} }
IF_VERBOSE(3, display(verbose_stream())); IF_VERBOSE(3, display(verbose_stream() << "after\n"));
return true; return true;
} }
@ -2957,7 +2958,8 @@ namespace nlsat {
continue; continue;
lits.push_back(l); lits.push_back(l);
if (a.m_bool_var != l.var()) { if (a.m_bool_var != l.var()) {
IF_VERBOSE(3, display(verbose_stream() << "simplify ", l) << "\n"); IF_VERBOSE(3, display(verbose_stream() << "simplify ", a) << " -> ";
display(verbose_stream(), l) << "\n");
b2l.insert(a.m_bool_var, l); b2l.insert(a.m_bool_var, l);
} }
} }
@ -3182,6 +3184,8 @@ namespace nlsat {
} }
break; break;
case atom::EQ: { case atom::EQ: {
if (sign)
continue;
all_solved = false; all_solved = false;
if (!m_pm.is_const(B)) if (!m_pm.is_const(B))
continue; continue;
@ -3212,6 +3216,13 @@ namespace nlsat {
if (lo.empty() && hi.empty()) if (lo.empty() && hi.empty())
return false; return false;
if (apply_fm_equality(x, clauses, lo, hi))
return true;
if (!all_solved)
return false;
IF_VERBOSE(3, IF_VERBOSE(3,
verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n";
for (auto c : clauses) for (auto c : clauses)
@ -3219,14 +3230,6 @@ namespace nlsat {
display(verbose_stream(), *c) << "\n"; display(verbose_stream(), *c) << "\n";
); );
if (apply_fm_equality(x, clauses, lo, hi))
return true;
// return false;
if (!all_solved)
return false;
auto num_lo = lo.size(), num_hi = hi.size(); auto num_lo = lo.size(), num_hi = hi.size();
if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2)) if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2))
return false; return false;
@ -3310,6 +3313,7 @@ namespace nlsat {
auto a1 = static_cast<_assumption_set>(l.c->assumptions()); auto a1 = static_cast<_assumption_set>(l.c->assumptions());
auto a2 = static_cast<_assumption_set>(h.c->assumptions()); auto a2 = static_cast<_assumption_set>(h.c->assumptions());
a1 = m_asm.mk_join(a1, a2); a1 = m_asm.mk_join(a1, a2);
inc_ref(a1);
polynomial_ref A(l.A), B(l.B); polynomial_ref A(l.A), B(l.B);
@ -3347,6 +3351,7 @@ namespace nlsat {
if (cls) if (cls)
compute_occurs(*cls); compute_occurs(*cls);
} }
dec_ref(a1);
// track updates for model reconstruction // track updates for model reconstruction
m_bounds.push_back(l); m_bounds.push_back(l);
m_bounds.push_back(h); m_bounds.push_back(h);
@ -3508,7 +3513,7 @@ namespace nlsat {
continue; continue;
TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";); TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";);
m_bounds.push_back(bound_constraint(v, p, q, false, nullptr)); m_bounds.push_back(bound_constraint(v, p, q, false, nullptr));
IF_VERBOSE(3, display(verbose_stream(), *c) << "\n");
if (!substitute_var(v, p, q, *c)) if (!substitute_var(v, p, q, *c))
return false; return false;
del_clause(c, m_clauses); del_clause(c, m_clauses);
@ -4303,12 +4308,14 @@ namespace nlsat {
} }
std::ostream& display_assumptions(std::ostream & out, _assumption_set s) const { std::ostream& display_assumptions(std::ostream & out, _assumption_set s) const {
if (!m_display_assumption)
return out;
vector<assumption, false> deps; vector<assumption, false> deps;
m_asm.linearize(s, deps); m_asm.linearize(s, deps);
bool first = true; bool first = true;
for (auto dep : deps) { for (auto dep : deps) {
if (first) first = false; else out << " "; if (first) first = false; else out << " ";
if (m_display_assumption) (*m_display_assumption)(out, dep); (*m_display_assumption)(out, dep);
} }
return out; return out;
} }

15
src/util/small_object_allocator.cpp
View file

@ -28,6 +28,8 @@ Revision History:
# include <iostream> # include <iostream>
#endif #endif
#define DEBUG_SMALL_ALLOC(_x_) {}
small_object_allocator::small_object_allocator(char const * id) { small_object_allocator::small_object_allocator(char const * id) {
for (unsigned i = 0; i < NUM_SLOTS; i++) { for (unsigned i = 0; i < NUM_SLOTS; i++) {
m_chunks[i] = nullptr; m_chunks[i] = nullptr;
@ -75,6 +77,7 @@ void small_object_allocator::reset() {
void small_object_allocator::deallocate(size_t size, void * p) { void small_object_allocator::deallocate(size_t size, void * p) {
if (size == 0) return; if (size == 0) return;
DEBUG_SMALL_ALLOC(verbose_stream() << "deallocate " << size << " " << p << " bytes\n");
#if defined(Z3DEBUG) && !defined(_WINDOWS) #if defined(Z3DEBUG) && !defined(_WINDOWS)
// Valgrind friendly // Valgrind friendly
memory::deallocate(p); memory::deallocate(p);
@ -98,7 +101,9 @@ void small_object_allocator::deallocate(size_t size, void * p) {
void * small_object_allocator::allocate(size_t size) { void * small_object_allocator::allocate(size_t size) {
if (size == 0) return nullptr; if (size == 0)
return nullptr;
#if defined(Z3DEBUG) && !defined(_WINDOWS) #if defined(Z3DEBUG) && !defined(_WINDOWS)
@ -109,6 +114,11 @@ void * small_object_allocator::allocate(size_t size) {
if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
return memory::allocate(size); return memory::allocate(size);
} }
DEBUG_SMALL_ALLOC(
static unsigned count = 0;
++count);
#ifdef Z3DEBUG #ifdef Z3DEBUG
size_t osize = size; size_t osize = size;
#endif #endif
@ -120,6 +130,7 @@ void * small_object_allocator::allocate(size_t size) {
if (m_free_list[slot_id] != nullptr) { if (m_free_list[slot_id] != nullptr) {
void * r = m_free_list[slot_id]; void * r = m_free_list[slot_id];
m_free_list[slot_id] = *(reinterpret_cast<void **>(r)); m_free_list[slot_id] = *(reinterpret_cast<void **>(r));
DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n");
return r; return r;
} }
chunk * c = m_chunks[slot_id]; chunk * c = m_chunks[slot_id];
@ -130,6 +141,7 @@ void * small_object_allocator::allocate(size_t size) {
if (new_curr < c->m_data + CHUNK_SIZE) { if (new_curr < c->m_data + CHUNK_SIZE) {
void * r = c->m_curr; void * r = c->m_curr;
c->m_curr = new_curr; c->m_curr = new_curr;
DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n");
return r; return r;
} }
} }
@ -138,6 +150,7 @@ void * small_object_allocator::allocate(size_t size) {
m_chunks[slot_id] = new_c; m_chunks[slot_id] = new_c;
void * r = new_c->m_curr; void * r = new_c->m_curr;
new_c->m_curr += size; new_c->m_curr += size;
DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n");
return r; return r;
} }