mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Add getter for target and justification to enode

Browse source
This commit is contained in:
Jakob Rath 2023-07-12 15:47:33 +02:00
parent f61bf0843b
commit 1d3a31c323
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/euf/euf_enode.h
View file

@ -211,6 +211,9 @@ namespace euf {
bool children_are_roots() const;
enode* get_next() const { return m_next; }
enode* get_target() const { return m_target; }
justification get_justification() const { return m_justification; }
bool has_lbl_hash() const { return m_lbl_hash >= 0; }
unsigned char get_lbl_hash() const {
SASSERT(m_lbl_hash >= 0 && static_cast<unsigned>(m_lbl_hash) < approx_set_traits<unsigned long long>::capacity);