diff options
Diffstat (limited to 'src/theory/bv/bitblast/bitblast_utils.h')
-rw-r--r-- | src/theory/bv/bitblast/bitblast_utils.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h index f2bee22e5..03e0aa349 100644 --- a/src/theory/bv/bitblast/bitblast_utils.h +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -81,7 +81,7 @@ Node mkOr<Node>(Node a, Node b) { template <> inline Node mkOr<Node>(const std::vector<Node>& children) { - Assert (children.size()); + Assert(children.size()); if (children.size() == 1) return children[0]; return NodeManager::currentNM()->mkNode(kind::OR, children); @@ -95,7 +95,7 @@ Node mkAnd<Node>(Node a, Node b) { template <> inline Node mkAnd<Node>(const std::vector<Node>& children) { - Assert (children.size()); + Assert(children.size()); if (children.size() == 1) return children[0]; return NodeManager::currentNM()->mkNode(kind::AND, children); @@ -123,7 +123,7 @@ Node mkIte<Node>(Node cond, Node a, Node b) { template <class T> void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) { - Assert ( lo < b.size() && hi < b.size() && lo <= hi); + Assert(lo < b.size() && hi < b.size() && lo <= hi); for (unsigned i = lo; i <= hi; ++i) { dest.push_back(b[i]); } @@ -168,7 +168,7 @@ void inline lshift(std::vector<T>& bits, unsigned amount) { template <class T> void inline makeZero(std::vector<T>& bits, unsigned width) { - Assert(bits.size() == 0); + Assert(bits.size() == 0); for(unsigned i = 0; i < width; ++i) { bits.push_back(mkFalse<T>()); } @@ -188,7 +188,7 @@ void inline makeZero(std::vector<T>& bits, unsigned width) { template <class T> T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) { Assert(a.size() == b.size() && res.size() == 0); - + for (unsigned i = 0 ; i < a.size(); ++i) { T sum = mkXor(mkXor(a[i], b[i]), carry); carry = mkOr( mkAnd(a[i], b[i]), @@ -222,8 +222,8 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s template <class T> T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) { - Assert (a.size() && b.size()); - + Assert(a.size() && b.size()); + T res = mkAnd(mkNot(a[0]), b[0]); if(orEqual) { @@ -240,7 +240,7 @@ T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu template <class T> T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) { - Assert (a.size() && b.size()); + Assert(a.size() && b.size()); if (a.size() == 1) { if(orEqual) { return mkOr(mkIff(a[0], b[0]), |