mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add extra fields to nlsat-clause

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-30 17:00:05 -07:00
parent 39dc8861ee
commit 4c070f9e76
2 changed files with 17 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_clause.cpp
View file

@ -25,7 +25,10 @@ namespace nlsat {
m_size(sz),
m_capacity(sz),
m_learned(learned),
m_activity(0),
m_active(false),
m_removed(false),
m_marked(false),
m_var_hash(0),
m_assumptions(as) {
for (unsigned i = 0; i < sz; i++) {
m_lits[i] = lits[i];

17
src/nlsat/nlsat_clause.h
View file

@ -29,7 +29,10 @@ namespace nlsat {
unsigned m_size;
unsigned m_capacity:31;
unsigned m_learned:1;
unsigned m_activity;
unsigned m_active:1;
unsigned m_removed:1;
unsigned m_marked:1;
unsigned m_var_hash;
assumption_set m_assumptions;
literal m_lits[0];
static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
@ -46,9 +49,15 @@ namespace nlsat {
literal const * begin() const { return m_lits; }
literal const * end() const { return m_lits + m_size; }
literal const * data() const { return m_lits; }
void inc_activity() { m_activity++; }
void set_activity(unsigned v) { m_activity = v; }
unsigned get_activity() const { return m_activity; }
void set_active(bool b) { m_active = b; }
bool is_active() const { return m_active; }
void set_removed() { m_removed = true; }
bool is_removed() const { return m_removed; }
unsigned var_hash() const { return m_var_hash; }
void set_var_hash(unsigned h) { m_var_hash = h; }
bool is_marked() const { return m_marked; }
void mark() { m_marked = true; }
void unmark() { m_marked = false; }
bool contains(literal l) const;
bool contains(bool_var v) const;
void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; } }