Added native support for shift operations to ezSAT

2 files changed, 95 insertions, 1 deletions

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4c0b624be..13ed112ed 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)
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 83e1b23c5..c5ef6b0a2 100644
--- 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);