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

merge with current master

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-10 10:46:42 -08:00
parent 08a925323c
commit bf39b2b103
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.h
View file

@ -353,8 +353,10 @@ namespace sat {
void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); } void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); }
bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); } bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); }
bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); } bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); }
unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); }
void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); } void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); }
void mark_visited(bool_var v) { mark_visited(literal(v, false)); } void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
void inc_visited(bool_var v) { m_visited.inc_visited(v); }
bool all_distinct(literal_vector const& lits); bool all_distinct(literal_vector const& lits);
bool all_distinct(clause const& cl); bool all_distinct(clause const& cl);

4
src/util/visit_helper.h
View file

@ -45,5 +45,5 @@ public:
m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1); m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1);
} }
bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; } bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; }
unsigned num_visited(unsigned v) { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; } unsigned num_visited(unsigned v) const { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; }
}; };