mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

don't need marks in bool_var_manager anymore

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 04:35:37 +02:00
parent 7b9726a95c
commit 71e97a4098
2 changed files with 6 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/math/polysat/boolean.cpp
View file

@ -25,20 +25,20 @@ namespace polysat {
m_lemma.push_back(nullptr); m_lemma.push_back(nullptr);
return var; return var;
} }
else { else {
sat::bool_var var = m_unused.back(); sat::bool_var var = m_unused.back();
m_unused.pop_back(); m_unused.pop_back();
SASSERT_EQ(m_level[var], UINT_MAX); SASSERT_EQ(m_level[var], UINT_MAX);
SASSERT_EQ(m_value[2*var], l_undef); SASSERT_EQ(m_value[2*var], l_undef);
SASSERT_EQ(m_value[2*var+1], l_undef); SASSERT_EQ(m_value[2*var+1], l_undef);
SASSERT_EQ(m_reason[var], nullptr); SASSERT_EQ(m_reason[var], nullptr);
SASSERT_EQ(m_lemma[var], nullptr); SASSERT_EQ(m_lemma[var], nullptr);
return var; return var;
} }
} }
void bool_var_manager::del_var(sat::bool_var var) { void bool_var_manager::del_var(sat::bool_var var) {
SASSERT(std::all_of(m_unused.begin(), m_unused.end(), [var](unsigned unused_var) { return var != unused_var; })); SASSERT(std::count(m_unused.begin(), m_unused.end(), var) == 0);
auto lit = sat::literal(var); auto lit = sat::literal(var);
m_value[lit.index()] = l_undef; m_value[lit.index()] = l_undef;
m_value[(~lit).index()] = l_undef; m_value[(~lit).index()] = l_undef;
@ -67,22 +67,6 @@ namespace polysat {
m_lemma[lit.var()] = nullptr; m_lemma[lit.var()] = nullptr;
} }
void bool_var_manager::reset_marks() {
LOG_V("-------------------------- (reset boolean marks)");
m_marks.reserve(size());
m_clock++;
if (m_clock != 0)
return;
m_clock++;
m_marks.fill(0);
}
void bool_var_manager::set_mark(sat::bool_var var) {
LOG_V("Marking: b" << var);
SASSERT(var != sat::null_bool_var);
m_marks[var] = m_clock;
}
std::ostream& bool_var_manager::display(std::ostream& out) const { std::ostream& bool_var_manager::display(std::ostream& out) const {
for (sat::bool_var v = 0; v < size(); ++v) { for (sat::bool_var v = 0; v < size(); ++v) {
sat::literal lit{v}; sat::literal lit{v};

7
src/math/polysat/boolean.h
View file

@ -27,9 +27,6 @@ namespace polysat {
// For enumerative backtracking we store the lemma we're handling with a certain decision // For enumerative backtracking we store the lemma we're handling with a certain decision
svector<clause*> m_lemma; svector<clause*> m_lemma;
unsigned_vector m_marks;
unsigned m_clock = 0;
public: public:
// allocated size (not the number of active variables) // allocated size (not the number of active variables)
unsigned size() const { return m_level.size(); } unsigned size() const { return m_level.size(); }
@ -37,10 +34,6 @@ namespace polysat {
sat::bool_var new_var(); sat::bool_var new_var();
void del_var(sat::bool_var var); void del_var(sat::bool_var var);
void reset_marks();
bool is_marked(sat::bool_var var) const { return m_clock == m_marks[var]; }
void set_mark(sat::bool_var var);
bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; } bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; }
bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; } bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
bool is_decision(sat::bool_var var) const { return is_assigned(var) && !reason(var); } bool is_decision(sat::bool_var var) const { return is_assigned(var) && !reason(var); }