mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-13 04:13:01 +00:00
Code Activity

fix build warnings and scoop up after Nuno's leaks

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-02-10 09:25:37 -08:00
parent bcca975d2d
commit a7b9df14f4
6 changed files with 14 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sat_ddfw.h
View file

@ -72,7 +72,7 @@ namespace sat {
double m_reward = 0;
double m_last_reward = 0;
unsigned m_make_count = 0;
unsigned m_timestamp = 0;
uint64_t m_timestamp = 0;
int m_bias = 0;
ema m_reward_avg = 1e-5;
};
@ -282,7 +282,7 @@ namespace sat {
inline int& bias(bool_var v) { return m_vars[v].m_bias; }
unsigned timestamp(bool_var v) { return m_vars[v].m_timestamp; }
uint64_t timestamp(bool_var v) { return m_vars[v].m_timestamp; }
void reserve_vars(unsigned n);

4
src/ast/sls/sls_context.h
View file

@ -86,7 +86,7 @@ namespace sls {
virtual void force_restart() = 0;
virtual std::ostream& display(std::ostream& out) = 0;
virtual reslimit& rlimit() = 0;
virtual unsigned timestamp(sat::bool_var v) = 0;
virtual uint64_t timestamp(sat::bool_var v) = 0;
};
class context {
@ -196,7 +196,7 @@ namespace sls {
void shift_weights() { s.shift_weights(); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) { return s.reward(v); }
unsigned timestamp(sat::bool_var v) { return s.timestamp(v); }
uint64_t timestamp(sat::bool_var v) { return s.timestamp(v); }
indexed_uint_set const& unsat() const { return s.unsat(); }
indexed_uint_set const& unsat_vars() const { return s.unsat_vars(); }
unsigned num_external_in_unsat_vars() const { return s.num_external_in_unsat_vars(); }

2
src/ast/sls/sls_smt_plugin.h
View file

@ -186,6 +186,6 @@ namespace sls {
m_new_clause_added = true;
}
void force_restart() override { m_ddfw->force_restart(); }
unsigned timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
uint64_t timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
};
}

2
src/ast/sls/sls_smt_solver.cpp
View file

@ -102,7 +102,7 @@ namespace sls {
void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
reslimit& rlimit() override { return m_ddfw.rlimit(); }
void shift_weights() override { m_ddfw.shift_weights(); }
unsigned timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
uint64_t timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
void force_restart() override { m_ddfw.force_restart(); }

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

@ -301,7 +301,8 @@ namespace upolynomial {
void core_manager::sub(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) {
sub_core(sz1, p1, sz2, p2, m_basic_tmp);
buffer = std::move(m_basic_tmp);
// buffer = std::move(m_basic_tmp);
buffer.swap(m_basic_tmp);
}
// buffer := p1 * p2
@ -342,7 +343,8 @@ namespace upolynomial {
void core_manager::mul(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) {
mul_core(sz1, p1, sz2, p2, m_basic_tmp);
buffer = std::move(m_basic_tmp);
// buffer = std::move(m_basic_tmp);
buffer.swap(m_basic_tmp);
}
// buffer := dp/dx

8
src/nlsat/levelwise.cpp
View file

@ -155,7 +155,7 @@ namespace nlsat {
// Every root function on each side must be connected to the boundary through edges.
bool relation_invariant() const {
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
auto n = rfs.size();
if (n == 0) return true;
// Build adjacency list from pairs (using ps_idx)
@ -602,7 +602,7 @@ namespace nlsat {
void fill_relation_pairs_for_section_biggest_cell() {
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
auto n = rfs.size();
if (n == 0)
return;
SASSERT(is_set(m_l_rf));
@ -624,7 +624,7 @@ namespace nlsat {
// K = lower rfunc positions, f = upper rfunc positions
void build_both_side_spanning_tree() {
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
auto n = rfs.size();
SASSERT(n > 0 && is_set(m_l_rf) && is_set(m_u_rf));
SASSERT(!is_section());
SASSERT(!same_boundary_poly());
@ -695,7 +695,7 @@ namespace nlsat {
// Check arborescence invariants (used in debug via SASSERT)
DEBUG_CODE(
unsigned lower_root_idx = both.size() - 1;
auto lower_root_idx = both.size() - 1;
auto arb_invariant = [&]() {
// Reconstruct parent[] from the algorithm logic
std_vector<unsigned> parent(both.size(), UINT_MAX);