Added native support for shift operations to ezSAT

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4c0b624be852265f132a9101b24d99cf2b662059..13ed112ed231a506272a29e23920d683b973c887 100644 (file)
--- 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)

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 83e1b23c57a257b6e1ac3926ff48954f914dafee..c5ef6b0a2c298cd2a89617bd54f671e63aa9473a 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -237,7 +237,7 @@ public:
 
        std::vector<int> vec_iff(const std::vector<int> &vec1, const std::vector<int> &vec2);
        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_ite(int sel, const std::vector<int> &vec1, const std::vector<int> &vec2);
 
        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);
@@ -265,6 +265,10 @@ public:
        std::vector<int> vec_shr(const std::vector<int> &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); }
        std::vector<int> vec_srr(const std::vector<int> &vec1, int shift) { return vec_srl(vec1, -shift); }
 
+       std::vector<int> vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right);
+       std::vector<int> vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
+       std::vector<int> vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
+
        void vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const;
        void vec_append_signed(std::vector<int> &vec, const std::vector<int> &vec1, int64_t value);
        void vec_append_unsigned(std::vector<int> &vec, const std::vector<int> &vec1, uint64_t value);