mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

utils

Browse source
This commit is contained in:
Jakob Rath 2023-07-17 13:40:52 +02:00
parent 8c17e231ad
commit 82b1f9297b
3 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_egraph.cpp
View file

@ -919,6 +919,11 @@ namespace euf {
} }
} }
template void euf::egraph::explain(ptr_vector<void>& justifications, cc_justification*);
template void euf::egraph::explain_todo(ptr_vector<void>& justifications, cc_justification*);
template void euf::egraph::explain_eq(ptr_vector<void>& justifications, cc_justification*, enode* a, enode* b);
template unsigned euf::egraph::explain_diseq(ptr_vector<void>& justifications, cc_justification*, enode* a, enode* b);
template void euf::egraph::explain(ptr_vector<int>& justifications, cc_justification*); template void euf::egraph::explain(ptr_vector<int>& justifications, cc_justification*);
template void euf::egraph::explain_todo(ptr_vector<int>& justifications, cc_justification*); template void euf::egraph::explain_todo(ptr_vector<int>& justifications, cc_justification*);
template void euf::egraph::explain_eq(ptr_vector<int>& justifications, cc_justification*, enode* a, enode* b); template void euf::egraph::explain_eq(ptr_vector<int>& justifications, cc_justification*, enode* a, enode* b);

6
src/ast/euf/euf_egraph.h
View file

@ -178,8 +178,8 @@ namespace euf {
enode_vector m_empty_enodes; enode_vector m_empty_enodes;
unsigned m_num_scopes = 0; unsigned m_num_scopes = 0;
bool m_inconsistent = false; bool m_inconsistent = false;
enode *m_n1 = nullptr; enode* m_n1 = nullptr;
enode *m_n2 = nullptr; enode* m_n2 = nullptr;
justification m_justification; justification m_justification;
unsigned m_new_th_eqs_qhead = 0; unsigned m_new_th_eqs_qhead = 0;
svector<th_eq> m_new_th_eqs; svector<th_eq> m_new_th_eqs;
@ -305,7 +305,7 @@ namespace euf {
void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; } void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; } void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; } void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; } void set_display_justification(std::function<void(std::ostream&, void*)> d) { m_display_justification = std::move(d); }
void begin_explain(); void begin_explain();
void end_explain(); void end_explain();

11
src/util/tptr.h
View file

@ -43,4 +43,15 @@ Revision History:
#define UNBOXINT(PTR) static_cast<int>(reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) #define UNBOXINT(PTR) static_cast<int>(reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT)
template <typename U, typename T>
U unbox(T* ptr) {
return static_cast<U>(reinterpret_cast<std::uintptr_t>(ptr) >> PTR_ALIGNMENT);
}
template <typename T, typename U>
T* box(U val) {
static_assert( sizeof(T*) >= sizeof(U) + PTR_ALIGNMENT );
T* ptr = reinterpret_cast<T*>(static_cast<std::uintptr_t>(val) << PTR_ALIGNMENT);
SASSERT_EQ(val, unbox<U>(ptr)); // roundtrip of conversion integer -> pointer -> integer is not actually guaranteed by the C++ standard (but seems fine in practice, as indicated by previous usage of BOXINT/UNBOXINT)
return ptr;
}