From f41769cdcfb20f8f3b123e17f35d47c3797f81c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 May 2024 14:08:33 -0700 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/polynomial.cpp | 8 +++--- src/nlsat/nlsat_solver.cpp | 39 +++++++++++++++++------------ src/util/small_object_allocator.cpp | 15 ++++++++++- 3 files changed, 42 insertions(+), 20 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index c78269057..b90f4995a 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -6181,9 +6181,11 @@ namespace polynomial { } return false; } - if (!m_manager.ge(a1, a2)) - return false; - ++i, ++j; + if (m_manager.eq(a1, a2) || (m1->is_square() && m_manager.ge(a1, a2))) { + ++i, ++j; + continue; + } + return false; } return i == sz1 && j == sz2; } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 345dfa754..7fb657e9b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -343,10 +343,10 @@ namespace nlsat { void dec_ref(assumption) {} - void inc_ref(_assumption_set a) { + void inc_ref(_assumption_set a) { if (a != nullptr) m_asm.inc_ref(a); } - + void dec_ref(_assumption_set a) { if (a != nullptr) m_asm.dec_ref(a); } @@ -1733,7 +1733,7 @@ namespace nlsat { if (!simplify()) return l_false; } - + IF_VERBOSE(3, verbose_stream() << "search\n"); sort_watched_clauses(); lbool r = search_check(); CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); @@ -2792,6 +2792,7 @@ namespace nlsat { vector> m_var_occurs; bool simplify() { + IF_VERBOSE(3, display(verbose_stream() << "before\n")); unsigned sz = m_clauses.size(); while (true) { @@ -2815,7 +2816,7 @@ namespace nlsat { sz = m_clauses.size(); } - IF_VERBOSE(3, display(verbose_stream())); + IF_VERBOSE(3, display(verbose_stream() << "after\n")); return true; } @@ -2957,7 +2958,8 @@ namespace nlsat { continue; lits.push_back(l); 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); } } @@ -3182,6 +3184,8 @@ namespace nlsat { } break; case atom::EQ: { + if (sign) + continue; all_solved = false; if (!m_pm.is_const(B)) continue; @@ -3212,21 +3216,20 @@ namespace nlsat { if (lo.empty() && hi.empty()) return false; - IF_VERBOSE(3, - verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; - for (auto c : clauses) - if (!c->is_removed()) - display(verbose_stream(), *c) << "\n"; - ); - if (apply_fm_equality(x, clauses, lo, hi)) return true; - // return false; if (!all_solved) return false; + IF_VERBOSE(3, + verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; + for (auto c : clauses) + if (!c->is_removed()) + display(verbose_stream(), *c) << "\n"; + ); + auto num_lo = lo.size(), num_hi = hi.size(); if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2)) return false; @@ -3310,6 +3313,7 @@ namespace nlsat { auto a1 = static_cast<_assumption_set>(l.c->assumptions()); auto a2 = static_cast<_assumption_set>(h.c->assumptions()); a1 = m_asm.mk_join(a1, a2); + inc_ref(a1); polynomial_ref A(l.A), B(l.B); @@ -3347,6 +3351,7 @@ namespace nlsat { if (cls) compute_occurs(*cls); } + dec_ref(a1); // track updates for model reconstruction m_bounds.push_back(l); m_bounds.push_back(h); @@ -3482,7 +3487,7 @@ namespace nlsat { // // Equality simplificadtion (TODO, this should is deprecated by fm) // - bool solve_eqs() { + bool solve_eqs() { polynomial_ref p(m_pm), q(m_pm); var v; init_var_signs(); @@ -3508,7 +3513,7 @@ namespace nlsat { continue; TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";); 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)) return false; del_clause(c, m_clauses); @@ -4303,12 +4308,14 @@ namespace nlsat { } std::ostream& display_assumptions(std::ostream & out, _assumption_set s) const { + if (!m_display_assumption) + return out; vector deps; m_asm.linearize(s, deps); bool first = true; for (auto dep : deps) { if (first) first = false; else out << " "; - if (m_display_assumption) (*m_display_assumption)(out, dep); + (*m_display_assumption)(out, dep); } return out; } diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp index bd980df34..3fa92613d 100644 --- a/src/util/small_object_allocator.cpp +++ b/src/util/small_object_allocator.cpp @@ -28,6 +28,8 @@ Revision History: # include #endif +#define DEBUG_SMALL_ALLOC(_x_) {} + small_object_allocator::small_object_allocator(char const * id) { for (unsigned i = 0; i < NUM_SLOTS; i++) { m_chunks[i] = nullptr; @@ -75,6 +77,7 @@ void small_object_allocator::reset() { void small_object_allocator::deallocate(size_t size, void * p) { if (size == 0) return; + DEBUG_SMALL_ALLOC(verbose_stream() << "deallocate " << size << " " << p << " bytes\n"); #if defined(Z3DEBUG) && !defined(_WINDOWS) // Valgrind friendly 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) { - if (size == 0) return nullptr; + if (size == 0) + return nullptr; + #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)) { return memory::allocate(size); } +DEBUG_SMALL_ALLOC( + static unsigned count = 0; + ++count); + + #ifdef Z3DEBUG size_t osize = size; #endif @@ -120,6 +130,7 @@ void * small_object_allocator::allocate(size_t size) { if (m_free_list[slot_id] != nullptr) { void * r = m_free_list[slot_id]; m_free_list[slot_id] = *(reinterpret_cast(r)); + DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n"); return r; } 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) { void * r = c->m_curr; c->m_curr = new_curr; + DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n"); return r; } } @@ -138,6 +150,7 @@ void * small_object_allocator::allocate(size_t size) { m_chunks[slot_id] = new_c; void * r = new_c->m_curr; new_c->m_curr += size; + DEBUG_SMALL_ALLOC(verbose_stream() << "allocate " << size << " " << r << " " << count << " bytes\n"); return r; }