diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-02-13 16:52:16 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-02-13 16:52:16 +0100 |
| commit | 0d7fd2585e8daec77870f19264644a204e0a8ed4 (patch) | |
| tree | 680308c755ff95dde092e26d4e0e33eccc249f62 /libs | |
| parent | a75f94ec4ae411d98d9882e423e0ae02eda4bd37 (diff) | |
| download | yosys-0d7fd2585e8daec77870f19264644a204e0a8ed4.tar.gz yosys-0d7fd2585e8daec77870f19264644a204e0a8ed4.tar.bz2 yosys-0d7fd2585e8daec77870f19264644a204e0a8ed4.zip | |
Added "int ceil_log2(int)" function
Diffstat (limited to 'libs')
| -rw-r--r-- | libs/ezsat/ezsat.cc | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index da36fb74e..177bcd8a3 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1337,6 +1337,28 @@ void ezSAT::printInternalState(FILE *f) const fprintf(f, "--8<-- snap --8<--\n"); } +static int clog2(int x) +{ + int y = (x & (x - 1)); + y = (y | -y) >> 31; + + x |= (x >> 1); + x |= (x >> 2); + x |= (x >> 4); + x |= (x >> 8); + x |= (x >> 16); + + x >>= 1; + x -= ((x >> 1) & 0x55555555); + x = (((x >> 2) & 0x33333333) + (x & 0x33333333)); + x = (((x >> 4) + x) & 0x0f0f0f0f); + x += (x >> 8); + x += (x >> 16); + x = x & 0x0000003f; + + return x - y; +} + int ezSAT::onehot(const std::vector<int> &vec, bool max_only) { // Mixed one-hot/binary encoding as described by Claessen in Sec. 4.2 of @@ -1350,7 +1372,7 @@ int ezSAT::onehot(const std::vector<int> &vec, bool max_only) formula.push_back(expression(OpOr, vec)); // create binary vector - int num_bits = ceil(log2(vec.size())); + int num_bits = clog2(vec.size()); std::vector<int> bits; for (int k = 0; k < num_bits; k++) bits.push_back(literal()); |