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

port updates from poly/polysat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-09 13:00:43 -08:00
parent e580c384b8
commit 70d4f32ffd
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/util/dlist.h
View file

@ -223,6 +223,16 @@ public:
} }
}; };
template <typename T>
class dll_elements {
T const* m_list;
public:
dll_elements(T const* list) : m_list(list) {}
dll_iterator<T> begin() const { return dll_iterator<T>::mk_begin(m_list); }
dll_iterator<T> end() const { return dll_iterator<T>::mk_end(m_list); }
};
template < typename T template < typename T
, typename U = std::enable_if_t<std::is_base_of_v<dll_base<T>, T>> // should only match if T actually inherits from dll_base<T> , typename U = std::enable_if_t<std::is_base_of_v<dll_base<T>, T>> // should only match if T actually inherits from dll_base<T>
> >

2
src/util/var_queue.h
View file

@ -69,6 +69,8 @@ public:
m_queue.reset(); m_queue.reset();
} }
bool contains(var v) const { return m_queue.contains(v); }
bool empty() const { return m_queue.empty(); } bool empty() const { return m_queue.empty(); }
var next_var() { SASSERT(!empty()); return m_queue.erase_min(); } var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }