diff options
-rw-r--r-- | libs/ezsat/ezsat.cc | 32 | ||||
-rw-r--r-- | libs/ezsat/ezsat.h | 11 |
2 files changed, 26 insertions, 17 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 27e74e010..dccc00555 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -651,34 +651,42 @@ bool ezSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> & return false; } -std::vector<int> ezSAT::vec_const_signed(int64_t value, int bits) +std::vector<int> ezSAT::vec_const(const std::vector<bool> &bits) { std::vector<int> vec; - for (int i = 0; i < bits; i++) + for (auto bit : bits) + vec.push_back(bit ? TRUE : FALSE); + return vec; +} + +std::vector<int> ezSAT::vec_const_signed(int64_t value, int numBits) +{ + std::vector<int> vec; + for (int i = 0; i < numBits; i++) vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); return vec; } -std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int bits) +std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int numBits) { std::vector<int> vec; - for (int i = 0; i < bits; i++) + for (int i = 0; i < numBits; i++) vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); return vec; } -std::vector<int> ezSAT::vec_var(int bits) +std::vector<int> ezSAT::vec_var(int numBits) { std::vector<int> vec; - for (int i = 0; i < bits; i++) + for (int i = 0; i < numBits; i++) vec.push_back(literal()); return vec; } -std::vector<int> ezSAT::vec_var(std::string name, int bits) +std::vector<int> ezSAT::vec_var(std::string name, int numBits) { std::vector<int> vec; - for (int i = 0; i < bits; i++) + for (int i = 0; i < numBits; i++) vec.push_back(VAR(name + "[" + std::to_string(i) + "]")); return vec; } @@ -782,21 +790,21 @@ static void halfadder(ezSAT *that, int a, int b, int &y, int &x) x = new_x, y = new_y; } -std::vector<int> ezSAT::vec_count(const std::vector<int> &vec, int bits, bool clip) +std::vector<int> ezSAT::vec_count(const std::vector<int> &vec, int numBits, bool clip) { - std::vector<int> sum = vec_const_unsigned(0, bits); + std::vector<int> sum = vec_const_unsigned(0, numBits); std::vector<int> carry_vector; for (auto bit : vec) { int carry = bit; - for (int i = 0; i < bits; i++) + for (int i = 0; i < numBits; i++) halfadder(this, carry, sum[i], carry, sum[i]); carry_vector.push_back(carry); } if (clip) { int overflow = vec_reduce_or(carry_vector); - sum = vec_ite(overflow, vec_const_unsigned(~0, bits), sum); + sum = vec_ite(overflow, vec_const_unsigned(~0, numBits), sum); } #if 0 diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index abec0b239..547edb93b 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -203,10 +203,11 @@ public: // simple helpers for building expressions with bit vectors - std::vector<int> vec_const_signed(int64_t value, int bits); - std::vector<int> vec_const_unsigned(uint64_t value, int bits); - std::vector<int> vec_var(int bits); - std::vector<int> vec_var(std::string name, int bits); + std::vector<int> vec_const(const std::vector<bool> &bits); + std::vector<int> vec_const_signed(int64_t value, int numBits); + std::vector<int> vec_const_unsigned(uint64_t value, int numBits); + std::vector<int> vec_var(int numBits); + std::vector<int> vec_var(std::string name, int numBits); std::vector<int> vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend = false); std::vector<int> vec_not(const std::vector<int> &vec1); @@ -218,7 +219,7 @@ public: std::vector<int> vec_ite(const std::vector<int> &vec1, const std::vector<int> &vec2, const std::vector<int> &vec3); std::vector<int> vec_ite(int sel, const std::vector<int> &vec2, const std::vector<int> &vec3); - std::vector<int> vec_count(const std::vector<int> &vec, int bits, bool clip = true); + std::vector<int> vec_count(const std::vector<int> &vec, int numBits, bool clip = true); std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2); std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2); std::vector<int> vec_neg(const std::vector<int> &vec); |