aboutsummaryrefslogtreecommitdiffstats
path: root/libs
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-02-13 16:52:16 +0100
committerClifford Wolf <clifford@clifford.at>2016-02-13 16:52:16 +0100
commit0d7fd2585e8daec77870f19264644a204e0a8ed4 (patch)
tree680308c755ff95dde092e26d4e0e33eccc249f62 /libs
parenta75f94ec4ae411d98d9882e423e0ae02eda4bd37 (diff)
downloadyosys-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.cc24
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());