diff options
Diffstat (limited to 'libs/ezsat/ezsat.cc')
| -rw-r--r-- | libs/ezsat/ezsat.cc | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 8d232f335..177bcd8a3 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -2,11 +2,11 @@ * ezSAT -- A simple and easy to use CNF generator for SAT solvers * * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -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()); @@ -1373,7 +1395,7 @@ int ezSAT::manyhot(const std::vector<int> &vec, int min_hot, int max_hot) if (max_hot < 0) max_hot = min_hot; - + std::vector<int> formula; int M = max_hot+1, N = vec.size(); std::map<std::pair<int,int>, int> x; |