summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezsat.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-07-30 17:17:31 +0200
committerClifford Wolf <clifford@clifford.at>2014-07-30 18:37:17 +0200
commit9b566a7efa9813b0dd343bc96fe145f9e3e68d4f (patch)
tree27c18c759118f3578cf78da902ae130c380c7ab5 /libs/ezsat/ezsat.cc
parent45fd26b76e1ca72927ab0a8ce207aab0d024eba3 (diff)
Added native support for shift operations to ezSAT
Diffstat (limited to 'libs/ezsat/ezsat.cc')
-rw-r--r--libs/ezsat/ezsat.cc90
1 files changed, 90 insertions, 0 deletions
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<int> ezSAT::vec_srl(const std::vector<int> &vec1, int shift)
return vec;
}
+std::vector<int> ezSAT::vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right)
+{
+ std::vector<int> 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<int> ezSAT::vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &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<int> 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<int> buffer = vec1;
+
+ if (vec2_signed)
+ while (buffer.size() < vec1.size() + (1 << vec2_bits))
+ buffer.push_back(extend_left);
+
+ std::vector<int> overflow_pattern_left(buffer.size(), extend_left);
+ std::vector<int> 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<int> 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<int> ezSAT::vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &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<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
+ int overflow = vec_reduce_or(overflow_bits);
+
+ std::vector<int> buffer = vec1;
+ std::vector<int> 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<int> 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<int> &vec, const std::vector<int> &vec1) const
{
for (auto bit : vec1)