mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields

Browse source 
Yes, those 8 bytes are yours now, use responsibly.
This commit is contained in:
Nuno Lopes 2022-06-17 12:07:15 +01:00
parent 08c44bc6f6
commit 70bcf0b51d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_enode.h
View file

@ -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