From 0d7fd2585e8daec77870f19264644a204e0a8ed4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 13 Feb 2016 16:52:16 +0100 Subject: Added "int ceil_log2(int)" function --- libs/ezsat/ezsat.cc | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) (limited to 'libs') 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 &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 &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 bits; for (int k = 0; k < num_bits; k++) bits.push_back(literal()); -- cgit v1.2.3