Added ezsat vec_const() api

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 27e74e010a1ccee773106ca28da49d3a72219a7c..dccc00555aae8a89a4c966a4d12fe0ec8c9a96a3 100644 (file)
--- 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 abec0b239a84818be0d073c6001dd2ec5766c6b7..547edb93bcc2d1262e784d3a2ae83c78835c84e9 100644 (file)
--- 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);