mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-17 08:42:15 +00:00
Code Activity

fix LUT synthesis

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-04 15:34:15 -08:00
parent c562a1f883
commit fcfb76960f
1 changed files with 12 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/sat/sat_lut_finder.cpp
View file

@ -239,27 +239,20 @@ namespace sat {
v = vars[i]; v = vars[i];
vars.erase(v); vars.erase(v);
uint64_t r = 0; uint64_t r = 0;
unsigned stride_sz = (1u << i); uint64_t m = m_masks[vars.size()];
unsigned num_strides = (1u << vars.size()) / (stride_sz * 2); unsigned offset = 0;
// example, if i = 2, then we are examining
switch (i) { // how m_combination evaluates at position xy0uv
case 0: // If it evaluates to 0, then it has to evaluate to 1 on position xy1uv
for (unsigned j = 0; j < (1u << vars.size()); ++j) { // Offset keeps track of the value of xyuv
if (0 == (m_combination & (1ull << 2*j))) { //
r |= (1ull << j); for (unsigned j = 0; j < 64; ++j) {
if (0 != (m & (1ull << j))) {
if (0 == (m_combination & (1ull << j))) {
r |= 1ull << offset;
} }
++offset;
} }
break;
case 1:
// (0, 2) (1, 3), (4, 6), (5, 7)
for (unsigned j = 0; j < (1u << vars.size()); ++j) {
}
// TBD
break;
default:
// TBD
break;
} }
return r; return r;
} }