From 9b566a7efa9813b0dd343bc96fe145f9e3e68d4f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 30 Jul 2014 17:17:31 +0200 Subject: Added native support for shift operations to ezSAT --- libs/ezsat/ezsat.cc | 90 +++++++++++++++++++++++++++++++++++++++++++++++++++++ libs/ezsat/ezsat.h | 6 +++- 2 files changed, 95 insertions(+), 1 deletion(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 4c0b624b..13ed112e 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -977,6 +977,96 @@ std::vector ezSAT::vec_srl(const std::vector &vec1, int shift) return vec; } +std::vector ezSAT::vec_shift(const std::vector &vec1, int shift, int extend_left, int extend_right) +{ + std::vector vec; + for (int i = 0; i < int(vec1.size()); i++) { + int j = i+shift; + if (j < 0) + vec.push_back(extend_right); + else if (j >= int(vec1.size())) + vec.push_back(extend_left); + else + vec.push_back(vec1[j]); + } + return vec; +} + +static int my_clog2(int x) +{ + int result = 0; + for (x--; x > 0; result++) + x >>= 1; + return result; +} + +std::vector ezSAT::vec_shift_right(const std::vector &vec1, const std::vector &vec2, bool vec2_signed, int extend_left, int extend_right) +{ + int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size())); + + std::vector overflow_bits(vec2.begin() + vec2_bits, vec2.end()); + int overflow_left = FALSE, overflow_right = FALSE; + + if (vec2_signed) { + int overflow = FALSE; + for (auto bit : overflow_bits) + overflow = OR(overflow, XOR(bit, vec2[vec2_bits-1])); + overflow_left = AND(overflow, NOT(vec2.back())); + overflow_right = AND(overflow, vec2.back()); + } else + overflow_left = vec_reduce_or(overflow_bits); + + std::vector buffer = vec1; + + if (vec2_signed) + while (buffer.size() < vec1.size() + (1 << vec2_bits)) + buffer.push_back(extend_left); + + std::vector overflow_pattern_left(buffer.size(), extend_left); + std::vector overflow_pattern_right(buffer.size(), extend_right); + + buffer = vec_ite(overflow_left, overflow_pattern_left, buffer); + + if (vec2_signed) + buffer = vec_ite(overflow_right, overflow_pattern_left, buffer); + + for (int i = vec2_bits-1; i >= 0; i--) { + std::vector shifted_buffer; + if (vec2_signed && i == vec2_bits-1) + shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right); + else + shifted_buffer = vec_shift(buffer, 1 << i, extend_left, extend_right); + buffer = vec_ite(vec2[i], shifted_buffer, buffer); + } + + buffer.resize(vec1.size()); + return buffer; +} + +std::vector ezSAT::vec_shift_left(const std::vector &vec1, const std::vector &vec2, bool vec2_signed, int extend_left, int extend_right) +{ + // vec2_signed is not implemented in vec_shift_left() yet + assert(vec2_signed == false); + + int vec2_bits = std::min(my_clog2(vec1.size()), int(vec2.size())); + + std::vector overflow_bits(vec2.begin() + vec2_bits, vec2.end()); + int overflow = vec_reduce_or(overflow_bits); + + std::vector buffer = vec1; + std::vector overflow_pattern_right(buffer.size(), extend_right); + buffer = vec_ite(overflow, overflow_pattern_right, buffer); + + for (int i = 0; i < vec2_bits; i++) { + std::vector shifted_buffer; + shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right); + buffer = vec_ite(vec2[i], shifted_buffer, buffer); + } + + buffer.resize(vec1.size()); + return buffer; +} + void ezSAT::vec_append(std::vector &vec, const std::vector &vec1) const { for (auto bit : vec1) diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 83e1b23c..c5ef6b0a 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -237,7 +237,7 @@ public: std::vector vec_iff(const std::vector &vec1, const std::vector &vec2); std::vector vec_ite(const std::vector &vec1, const std::vector &vec2, const std::vector &vec3); - std::vector vec_ite(int sel, const std::vector &vec2, const std::vector &vec3); + std::vector vec_ite(int sel, const std::vector &vec1, const std::vector &vec2); std::vector vec_count(const std::vector &vec, int numBits, bool clip = true); std::vector vec_add(const std::vector &vec1, const std::vector &vec2); @@ -265,6 +265,10 @@ public: std::vector vec_shr(const std::vector &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); } std::vector vec_srr(const std::vector &vec1, int shift) { return vec_srl(vec1, -shift); } + std::vector vec_shift(const std::vector &vec1, int shift, int extend_left, int extend_right); + std::vector vec_shift_right(const std::vector &vec1, const std::vector &vec2, bool vec2_signed, int extend_left, int extend_right); + std::vector vec_shift_left(const std::vector &vec1, const std::vector &vec2, bool vec2_signed, int extend_left, int extend_right); + void vec_append(std::vector &vec, const std::vector &vec1) const; void vec_append_signed(std::vector &vec, const std::vector &vec1, int64_t value); void vec_append_unsigned(std::vector &vec, const std::vector &vec1, uint64_t value); -- cgit v1.2.3