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

don't rename uint_set but keep the original name

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-18 17:18:33 -07:00
parent bd4db4c41f
commit 9a987237d5
2 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_lookahead.h
View file

@ -353,7 +353,7 @@ namespace sat {
candidate(bool_var v, double r): m_var(v), m_rating(r) {} candidate(bool_var v, double r): m_var(v), m_rating(r) {}
}; };
svector<candidate> m_candidates; svector<candidate> m_candidates;
uint_set m_select_lookahead_vars; tracked_uint_set m_select_lookahead_vars;
double get_rating(bool_var v) const { return m_rating[v]; } double get_rating(bool_var v) const { return m_rating[v]; }
double get_rating(literal l) const { return get_rating(l.var()); } double get_rating(literal l) const { return get_rating(l.var()); }

10
src/util/sat_literal.h
View file

@ -110,12 +110,10 @@ namespace sat {
inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
typedef tracked_uint_set uint_set; typedef tracked_uint_set bool_var_set;
typedef uint_set bool_var_set;
class literal_set { class literal_set {
uint_set m_set; tracked_uint_set m_set;
public: public:
literal_set(literal_vector const& v) { literal_set(literal_vector const& v) {
for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
@ -141,9 +139,9 @@ namespace sat {
void reset() { m_set.reset(); } void reset() { m_set.reset(); }
void finalize() { m_set.finalize(); } void finalize() { m_set.finalize(); }
class iterator { class iterator {
uint_set::iterator m_it; tracked_uint_set::iterator m_it;
public: public:
iterator(uint_set::iterator it):m_it(it) {} iterator(tracked_uint_set::iterator it):m_it(it) {}
literal operator*() const { return to_literal(*m_it); } literal operator*() const { return to_literal(*m_it); }
iterator& operator++() { ++m_it; return *this; } iterator& operator++() { ++m_it; return *this; }
iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; } iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }