From 70bcf0b51da6917bf9d3e4a418e5744c601767a8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 17 Jun 2022 12:07:15 +0100 Subject: [PATCH] reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields Yes, those 8 bytes are yours now, use responsibly. --- src/smt/smt_enode.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 196d28396..b3a3bbf69 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -78,6 +78,8 @@ namespace smt { unsigned m_merge_tf:1; //!< True if the enode should be merged with true/false when the associated boolean variable is assigned. unsigned m_cgc_enabled:1; //!< True if congruence closure is enabled for this enode. unsigned m_iscope_lvl; //!< When the enode was internalized + bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log. + signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern /* The following property is valid for m_parents @@ -96,8 +98,6 @@ namespace smt { enode_vector m_parents; //!< Parent enodes of the equivalence class. id_var_list<> m_th_var_list; //!< List of theories that 'care' about this enode. trans_justification m_trans; //!< A justification for the enode being equal to its root. - bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log. - signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern approx_set m_lbls; approx_set m_plbls; enode * m_args[0]; //!< Cached args