mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-22 23:44:34 +00:00
Code Activity

build fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-19 20:55:45 +02:00
parent d65c0fbcd6
commit aaaa32b4a0
2 changed files with 33 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/sls/sls_bv_tracker.h
View file

@ -42,8 +42,37 @@ class sls_tracker {
struct value_score { struct value_score {
value_score() : value(unsynch_mpz_manager::mk_z(0)) {}; value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
value_score(value_score&&) noexcept = default; value_score(value_score&&) noexcept = default;
value_score(const value_score &other) {
m = other.m;
if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
m->set(value, other.value);
}
score = other.score;
score_prune = other.score_prune;
has_pos_occ = other.has_pos_occ;
has_neg_occ = other.has_neg_occ;
distance = other.distance;
touched = other.touched;
}
~value_score() { if (m) m->del(value); } ~value_score() { if (m) m->del(value); }
value_score& operator=(value_score&&) = default; value_score& operator=(value_score&&) = default;
value_score &operator=(const value_score &other) {
if (this != &other) {
if (m)
m->del(value);
m = other.m;
if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
m->set(value, other.value);
}
score = other.score;
score_prune = other.score_prune;
has_pos_occ = other.has_pos_occ;
has_neg_occ = other.has_neg_occ;
distance = other.distance;
touched = other.touched;
}
return *this;
}
unsynch_mpz_manager * m = nullptr; unsynch_mpz_manager * m = nullptr;
mpz value; mpz value;
double score = 0.0; double score = 0.0;

4
src/util/obj_hashtable.h
View file

@ -61,6 +61,10 @@ public:
key_data() {} key_data() {}
key_data(Key *key) : m_key(key) {} key_data(Key *key) : m_key(key) {}
key_data(Key *k, Value const &v) : m_key(k), m_value(v) {} key_data(Key *k, Value const &v) : m_key(k), m_value(v) {}
key_data(key_data &&kd) noexcept = default;
key_data(key_data const &kd) noexcept = default;
key_data &operator=(key_data const &kd) = default;
key_data &operator=(key_data &&kd) = default;
Value const & get_value() const { return m_value; } Value const & get_value() const { return m_value; }
Key & get_key () const { return *m_key; } Key & get_key () const { return *m_key; }
unsigned hash() const { return m_key->hash(); } unsigned hash() const { return m_key->hash(); }