mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

pleay nice with alignment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-26 23:29:42 -07:00
parent d818233063
commit a0de244487
1 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/muz/rel/dl_sparse_table.h
View file

@ -338,17 +338,20 @@ namespace datalog {
SASSERT(length + m_small_offset <= 64); SASSERT(length + m_small_offset <= 64);
} }
table_element get(const char * rec) const { table_element get(const char * rec) const {
const uint64_t * ptr = reinterpret_cast<const uint64_t*>(rec + m_big_offset);
uint64_t res = *ptr; uint64_t res;
memcpy(&res, rec + m_big_offset, sizeof(res));
res >>= m_small_offset; res >>= m_small_offset;
res &= m_mask; res &= m_mask;
return res; return res;
} }
void set(char * rec, table_element val) const { void set(char * rec, table_element val) const {
SASSERT( (val&~m_mask)==0 ); //the value fits into the column SASSERT( (val&~m_mask)==0 ); //the value fits into the column
uint64_t * ptr = reinterpret_cast<uint64_t*>(rec + m_big_offset); uint64_t cell;
*ptr &= m_write_mask; memcpy(&cell, rec + m_big_offset, sizeof(cell));
*ptr |= val << m_small_offset; cell &= m_write_mask;
cell |= val << m_small_offset;
memcpy(rec + m_big_offset, &cell, sizeof(cell));
} }
unsigned next_ofs() const { return m_offset+m_length; } unsigned next_ofs() const { return m_offset+m_length; }
}; };