summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-08-11 16:27:15 +0200
committerClifford Wolf <clifford@clifford.at>2013-08-11 16:27:15 +0200
commitccf36cb7d81a9513db15b8a36c240d2c7ec9f5b5 (patch)
treea81d36a260ad19154cb160da0aba95aa0d3444d1 /libs
parenta5836af172a154bc0b8f9fdea34e140a5662bc99 (diff)
Added SAT support for $div and $mod cells
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/ezsat.cc6
-rw-r--r--libs/ezsat/ezsat.h3
2 files changed, 9 insertions, 0 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 00918f62..4258fb6f 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -852,6 +852,12 @@ std::vector<int> ezSAT::vec_sub(const std::vector<int> &vec1, const std::vector<
return vec;
}
+std::vector<int> ezSAT::vec_neg(const std::vector<int> &vec)
+{
+ std::vector<int> zero(vec.size(), FALSE);
+ return vec_sub(zero, vec);
+}
+
void ezSAT::vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero)
{
assert(vec1.size() == vec2.size());
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 2d0307d5..4a6a7278 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -223,6 +223,7 @@ public:
std::vector<int> vec_count(const std::vector<int> &vec, int bits, 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);
void vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero);
@@ -305,6 +306,8 @@ struct ezSATvec
ezSATvec(ezSAT &sat, const std::vector<int> &vec) : sat(sat), vec(vec) { }
ezSATvec operator ~() { return ezSATvec(sat, sat.vec_not(vec)); }
+ ezSATvec operator -() { return ezSATvec(sat, sat.vec_neg(vec)); }
+
ezSATvec operator &(const ezSATvec &other) { return ezSATvec(sat, sat.vec_and(vec, other.vec)); }
ezSATvec operator |(const ezSATvec &other) { return ezSATvec(sat, sat.vec_or(vec, other.vec)); }
ezSATvec operator ^(const ezSATvec &other) { return ezSATvec(sat, sat.vec_xor(vec, other.vec)); }