From ccf36cb7d81a9513db15b8a36c240d2c7ec9f5b5 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 11 Aug 2013 16:27:15 +0200 Subject: Added SAT support for $div and $mod cells --- libs/ezsat/ezsat.cc | 6 ++++++ libs/ezsat/ezsat.h | 3 +++ 2 files changed, 9 insertions(+) (limited to 'libs') 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 ezSAT::vec_sub(const std::vector &vec1, const std::vector< return vec; } +std::vector ezSAT::vec_neg(const std::vector &vec) +{ + std::vector zero(vec.size(), FALSE); + return vec_sub(zero, vec); +} + void ezSAT::vec_cmp(const std::vector &vec1, const std::vector &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 vec_count(const std::vector &vec, int bits, bool clip = true); std::vector vec_add(const std::vector &vec1, const std::vector &vec2); std::vector vec_sub(const std::vector &vec1, const std::vector &vec2); + std::vector vec_neg(const std::vector &vec); void vec_cmp(const std::vector &vec1, const std::vector &vec2, int &carry, int &overflow, int &sign, int &zero); @@ -305,6 +306,8 @@ struct ezSATvec ezSATvec(ezSAT &sat, const std::vector &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)); } -- cgit v1.2.3