/********************* */
/*! \file bitvector.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean
- ** Minor contributors (to current version): lianah, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief A fixed-size bit-vector.
**
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** A fixed-size bit-vector, implemented as a wrapper around Integer.
**/
#include "cvc4_public.h"
-#ifndef __CVC4__BITVECTOR_H
-#define __CVC4__BITVECTOR_H
+#ifndef CVC4__BITVECTOR_H
+#define CVC4__BITVECTOR_H
-#include <iostream>
-#include "util/exception.h"
+#include <cstdint>
+#include <iosfwd>
+
+#include "base/exception.h"
#include "util/integer.h"
namespace CVC4 {
-class CVC4_PUBLIC BitVector {
+class CVC4_PUBLIC BitVector
+{
+ public:
+ BitVector(unsigned size, const Integer& val)
+ : d_size(size), d_value(val.modByPow2(size))
+ {
+ }
-private:
+ BitVector(unsigned size = 0) : d_size(size), d_value(0) {}
- /*
- Class invariants:
- * no overflows: 2^d_size < d_value
- * no negative numbers: d_value >= 0
+ /**
+ * BitVector constructor using a 32-bit unsigned integer for the value.
+ *
+ * Note: we use an explicit bit-width here to be consistent across
+ * platforms (long is 32-bit when compiling 64-bit binaries on
+ * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
*/
- unsigned d_size;
- Integer d_value;
-
- Integer toSignedInt() const {
- // returns Integer corresponding to two's complement interpretation of bv
- unsigned size = d_size;
- Integer sign_bit = d_value.extractBitRange(1,size-1);
- Integer val = d_value.extractBitRange(size-1, 0);
- Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
- return res;
- }
-
-
-public:
-
- BitVector(unsigned size, const Integer& val):
- d_size(size),
- d_value(val.modByPow2(size))
- {}
-
- BitVector(unsigned size = 0)
- : d_size(size), d_value(0) {}
-
- BitVector(unsigned size, unsigned int z)
- : d_size(size), d_value(z) {
+ BitVector(unsigned size, uint32_t z) : d_size(size), d_value(z)
+ {
d_value = d_value.modByPow2(size);
}
-
- BitVector(unsigned size, unsigned long int z)
- : d_size(size), d_value(z) {
+
+ /**
+ * BitVector constructor using a 64-bit unsigned integer for the value.
+ *
+ * Note: we use an explicit bit-width here to be consistent across
+ * platforms (long is 32-bit when compiling 64-bit binaries on
+ * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
+ */
+ BitVector(unsigned size, uint64_t z) : d_size(size), d_value(z)
+ {
d_value = d_value.modByPow2(size);
}
BitVector(unsigned size, const BitVector& q)
- : d_size(size), d_value(q.d_value) {}
-
- BitVector(const std::string& num, unsigned base = 2);
+ : d_size(size), d_value(q.d_value)
+ {
+ }
+
+ /**
+ * BitVector constructor.
+ *
+ * The value of the bit-vector is passed in as string of base 2, 10 or 16.
+ * The size of resulting bit-vector is
+ * - base 2: the size of the binary string
+ * - base 10: the min. size required to represent the decimal as a bit-vector
+ * - base 16: the max. size required to represent the hexadecimal as a
+ * bit-vector (4 * size of the given value string)
+ *
+ * @param num The value of the bit-vector in string representation.
+ * @param base The base of the string representation.
+ */
+ BitVector(const std::string& num, unsigned base = 2)
+ {
+ CheckArgument(base == 2 || base == 10 || base == 16, base);
+ d_value = Integer(num, base);
+ switch (base)
+ {
+ case 10: d_size = d_value.length(); break;
+ case 16: d_size = num.size() * 4; break;
+ default: d_size = num.size();
+ }
+ }
~BitVector() {}
- Integer toInteger() const {
- return d_value;
- }
-
- BitVector& operator =(const BitVector& x) {
- if(this == &x)
- return *this;
+ BitVector& operator=(const BitVector& x)
+ {
+ if (this == &x) return *this;
d_size = x.d_size;
d_value = x.d_value;
return *this;
}
- bool operator ==(const BitVector& y) const {
- if (d_size != y.d_size) return false;
- return d_value == y.d_value;
- }
+ /* Get size (bit-width). */
+ unsigned getSize() const;
+ /* Get value. */
+ const Integer& getValue() const;
- bool operator !=(const BitVector& y) const {
- if (d_size != y.d_size) return true;
- return d_value != y.d_value;
- }
+ /* Return value. */
+ Integer toInteger() const;
+ /* Return Integer corresponding to two's complement interpretation of this. */
+ Integer toSignedInteger() const;
+ /* Return (binary) string representation. */
+ std::string toString(unsigned int base = 2) const;
- BitVector concat (const BitVector& other) const {
- return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
- }
+ /* Return hash value. */
+ size_t hash() const;
- BitVector extract(unsigned high, unsigned low) const {
- return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
- }
+ /* Set bit at index 'i'. */
+ BitVector setBit(uint32_t i) const;
+ /* Return true if bit at index 'i' is set. */
+ bool isBitSet(uint32_t i) const;
- /*
- Bitwise operations on BitVectors
- */
+ /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
+ unsigned isPow2() const;
- // xor
- BitVector operator ^(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseXor(y.d_value));
- }
-
- // or
- BitVector operator |(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseOr(y.d_value));
- }
-
- // and
- BitVector operator &(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
- }
+ /* -----------------------------------------------------------------------
+ ** Operators
+ * ----------------------------------------------------------------------- */
- // not
- BitVector operator ~() const {
- return BitVector(d_size, d_value.bitwiseNot());
- }
+ /* String Operations ----------------------------------------------------- */
- /*
- Arithmetic operations on BitVectors
- */
+ /* Return the concatenation of this and bit-vector 'other'. */
+ BitVector concat(const BitVector& other) const;
+ /* Return the bit range from index 'high' to index 'low'. */
+ BitVector extract(unsigned high, unsigned low) const;
- bool operator <(const BitVector& y) const {
- return d_value < y.d_value;
- }
+ /* (Dis)Equality --------------------------------------------------------- */
- bool operator >(const BitVector& y) const {
- return d_value > y.d_value ;
- }
+ /* Return true if this is equal to 'y'. */
+ bool operator==(const BitVector& y) const;
- bool operator <=(const BitVector& y) const {
- return d_value <= y.d_value;
- }
-
- bool operator >=(const BitVector& y) const {
- return d_value >= y.d_value ;
- }
+ /* Return true if this is not equal to 'y'. */
+ bool operator!=(const BitVector& y) const;
-
- BitVector operator +(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- Integer sum = d_value + y.d_value;
- return BitVector(d_size, sum);
- }
+ /* Unsigned Inequality --------------------------------------------------- */
- BitVector operator -(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- // to maintain the invariant that we are only adding BitVectors of the
- // same size
- BitVector one(d_size, Integer(1));
- return *this + ~y + one;
- }
+ /* Return true if this is unsigned less than bit-vector 'y'. */
+ bool operator<(const BitVector& y) const;
- BitVector operator -() const {
- BitVector one(d_size, Integer(1));
- return ~(*this) + one;
- }
+ /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
+ bool operator<=(const BitVector& y) const;
- BitVector operator *(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- Integer prod = d_value * y.d_value;
- return BitVector(d_size, prod);
- }
+ /* Return true if this is unsigned greater than bit-vector 'y'. */
+ bool operator>(const BitVector& y) const;
- BitVector setBit(uint32_t i) const {
- CheckArgument(i < d_size, i);
- Integer res = d_value.setBit(i);
- return BitVector(d_size, res);
- }
+ /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
+ bool operator>=(const BitVector& y) const;
- bool isBitSet(uint32_t i) const {
- CheckArgument(i < d_size, i);
- return d_value.isBitSet(i);
- }
-
- /**
- * Total division function that returns 0 when the denominator is 0.
- */
- BitVector unsignedDivTotal (const BitVector& y) const {
+ /* Return true if this is unsigned less than bit-vector 'y'.
+ * This function is a synonym for operator < but performs additional
+ * argument checks.*/
+ bool unsignedLessThan(const BitVector& y) const;
- CheckArgument(d_size == y.d_size, y);
- if (y.d_value == 0) {
- return BitVector(d_size, 0u);
- }
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value > 0, y);
- return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
- }
-
- /**
- * Total division function that returns 0 when the denominator is 0.
- */
- BitVector unsignedRemTotal(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- if (y.d_value == 0) {
- return BitVector(d_size, 0u);
- }
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value > 0, y);
- return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
- }
-
-
- bool signedLessThan(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- Integer a = (*this).toSignedInt();
- Integer b = y.toSignedInt();
-
- return a < b;
- }
+ /* Return true if this is unsigned less than or equal to bit-vector 'y'.
+ * This function is a synonym for operator >= but performs additional
+ * argument checks.*/
+ bool unsignedLessThanEq(const BitVector& y) const;
- bool unsignedLessThan(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- return d_value < y.d_value;
- }
+ /* Signed Inequality ----------------------------------------------------- */
- bool signedLessThanEq(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- Integer a = (*this).toSignedInt();
- Integer b = y.toSignedInt();
-
- return a <= b;
- }
+ /* Return true if this is signed less than bit-vector 'y'. */
+ bool signedLessThan(const BitVector& y) const;
- bool unsignedLessThanEq(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, this);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- return d_value <= y.d_value;
- }
+ /* Return true if this is signed less than or equal to bit-vector 'y'. */
+ bool signedLessThanEq(const BitVector& y) const;
-
- /*
- Extend operations
- */
+ /* Bit-wise operations --------------------------------------------------- */
- BitVector zeroExtend(unsigned amount) const {
- return BitVector(d_size + amount, d_value);
- }
+ /* Return a bit-vector representing the bit-wise xor (this ^ y). */
+ BitVector operator^(const BitVector& y) const;
- BitVector signExtend(unsigned amount) const {
- Integer sign_bit = d_value.extractBitRange(1, d_size -1);
- if(sign_bit == Integer(0)) {
- return BitVector(d_size + amount, d_value);
- } else {
- Integer val = d_value.oneExtend(d_size, amount);
- return BitVector(d_size+ amount, val);
- }
- }
-
- /*
- Shifts on BitVectors
- */
+ /* Return a bit-vector representing the bit-wise or (this | y). */
+ BitVector operator|(const BitVector& y) const;
- BitVector leftShift(const BitVector& y) const {
- if (y.d_value > Integer(d_size)) {
- return BitVector(d_size, Integer(0));
- }
- if (y.d_value == 0) {
- return *this;
- }
+ /* Return a bit-vector representing the bit-wise and (this & y). */
+ BitVector operator&(const BitVector& y) const;
- // making sure we don't lose information casting
- CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
- uint32_t amount = y.d_value.toUnsignedInt();
- Integer res = d_value.multiplyByPow2(amount);
- return BitVector(d_size, res);
- }
+ /* Return a bit-vector representing the bit-wise not of this. */
+ BitVector operator~() const;
- BitVector logicalRightShift(const BitVector& y) const {
- if(y.d_value > Integer(d_size)) {
- return BitVector(d_size, Integer(0));
- }
+ /* Arithmetic operations ------------------------------------------------- */
- // making sure we don't lose information casting
- CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
- uint32_t amount = y.d_value.toUnsignedInt();
- Integer res = d_value.divByPow2(amount);
- return BitVector(d_size, res);
- }
+ /* Return a bit-vector representing the addition (this + y). */
+ BitVector operator+(const BitVector& y) const;
- BitVector arithRightShift(const BitVector& y) const {
- Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
- if(y.d_value > Integer(d_size)) {
- if(sign_bit == Integer(0)) {
- return BitVector(d_size, Integer(0));
- } else {
- return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
- }
- }
-
- if (y.d_value == 0) {
- return *this;
- }
+ /* Return a bit-vector representing the subtraction (this - y). */
+ BitVector operator-(const BitVector& y) const;
- // making sure we don't lose information casting
- CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
-
- uint32_t amount = y.d_value.toUnsignedInt();
- Integer rest = d_value.divByPow2(amount);
-
- if(sign_bit == Integer(0)) {
- return BitVector(d_size, rest);
- }
- Integer res = rest.oneExtend(d_size - amount, amount);
- return BitVector(d_size, res);
- }
-
+ /* Return a bit-vector representing the negation of this. */
+ BitVector operator-() const;
- /*
- Convenience functions
- */
-
- size_t hash() const {
- return d_value.hash() + d_size;
- }
+ /* Return a bit-vector representing the multiplication (this * y). */
+ BitVector operator*(const BitVector& y) const;
- std::string toString(unsigned int base = 2) const {
- std::string str = d_value.toString(base);
- if( base == 2 && d_size > str.size() ) {
- std::string zeroes;
- for( unsigned int i=0; i < d_size - str.size(); ++i ) {
- zeroes.append("0");
- }
- return zeroes + str;
- } else {
- return str;
- }
- }
+ /* Total division function.
+ * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
+ * denominator is zero, and a bit-vector representing the unsigned division
+ * (this / y), otherwise. */
+ BitVector unsignedDivTotal(const BitVector& y) const;
- unsigned getSize() const {
- return d_size;
- }
+ /* Total remainder function.
+ * Returns this when the denominator is zero, and the unsigned remainder
+ * (this % y), otherwise. */
+ BitVector unsignedRemTotal(const BitVector& y) const;
- const Integer& getValue() const {
- return d_value;
- }
+ /* Extend operations ----------------------------------------------------- */
- /**
- Returns k is the integer is equal to 2^{k-1} and zero
- otherwise
- @return k if the integer is equal to 2^{k-1} and zero otherwise
- */
- unsigned isPow2() {
- return d_value.isPow2();
- }
+ /* Return a bit-vector representing this extended by 'n' zero bits. */
+ BitVector zeroExtend(unsigned n) const;
-};/* class BitVector */
+ /* Return a bit-vector representing this extended by 'n' bits of the value
+ * of the signed bit. */
+ BitVector signExtend(unsigned n) const;
+ /* Shift operations ------------------------------------------------------ */
+ /* Return a bit-vector representing a left shift of this by 'y'. */
+ BitVector leftShift(const BitVector& y) const;
-inline BitVector::BitVector(const std::string& num, unsigned base) {
- CheckArgument(base == 2 || base == 16, base);
+ /* Return a bit-vector representing a logical right shift of this by 'y'. */
+ BitVector logicalRightShift(const BitVector& y) const;
- if( base == 2 ) {
- d_size = num.size();
- } else {
- d_size = num.size() * 4;
- }
+ /* Return a bit-vector representing an arithmetic right shift of this
+ * by 'y'.*/
+ BitVector arithRightShift(const BitVector& y) const;
- d_value = Integer(num, base);
-}/* BitVector::BitVector() */
+ /* -----------------------------------------------------------------------
+ ** Static helpers.
+ * ----------------------------------------------------------------------- */
+ /* Create bit-vector of ones of given size. */
+ static BitVector mkOnes(unsigned size);
-/**
- * Hash function for the BitVector constants.
- */
-struct CVC4_PUBLIC BitVectorHashFunction {
- inline size_t operator()(const BitVector& bv) const {
- return bv.hash();
- }
-};/* struct BitVectorHashFunction */
+ /* Create bit-vector representing the minimum signed value of given size. */
+ static BitVector mkMinSigned(unsigned size);
+
+ /* Create bit-vector representing the maximum signed value of given size. */
+ static BitVector mkMaxSigned(unsigned size);
+
+ private:
+ /**
+ * Class invariants:
+ * - no overflows: 2^d_size < d_value
+ * - no negative numbers: d_value >= 0
+ */
+
+ unsigned d_size;
+ Integer d_value;
+
+}; /* class BitVector */
+
+/* -----------------------------------------------------------------------
+ ** BitVector structs
+ * ----------------------------------------------------------------------- */
/**
* The structure representing the extraction operation for bit-vectors. The
- * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
+ * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
* by taking the bits at indices <code>high ... low</code>
*/
-struct CVC4_PUBLIC BitVectorExtract {
+struct CVC4_PUBLIC BitVectorExtract
+{
/** The high bit of the range for this extract */
unsigned high;
/** The low bit of the range for this extract */
unsigned low;
- BitVectorExtract(unsigned high, unsigned low)
- : high(high), low(low) {}
+ BitVectorExtract(unsigned high, unsigned low) : high(high), low(low) {}
- bool operator == (const BitVectorExtract& extract) const {
+ bool operator==(const BitVectorExtract& extract) const
+ {
return high == extract.high && low == extract.low;
}
-};/* struct BitVectorExtract */
-
-/**
- * Hash function for the BitVectorExtract objects.
- */
-struct CVC4_PUBLIC BitVectorExtractHashFunction {
- size_t operator()(const BitVectorExtract& extract) const {
- size_t hash = extract.low;
- hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
- return hash;
- }
-};/* struct BitVectorExtractHashFunction */
-
+}; /* struct BitVectorExtract */
/**
- * The structure representing the extraction of one Boolean bit.
+ * The structure representing the extraction of one Boolean bit.
*/
-struct CVC4_PUBLIC BitVectorBitOf {
+struct CVC4_PUBLIC BitVectorBitOf
+{
/** The index of the bit */
unsigned bitIndex;
- BitVectorBitOf(unsigned i)
- : bitIndex(i) {}
+ BitVectorBitOf(unsigned i) : bitIndex(i) {}
- bool operator == (const BitVectorBitOf& other) const {
- return bitIndex == other.bitIndex;
+ bool operator==(const BitVectorBitOf& other) const
+ {
+ return bitIndex == other.bitIndex;
}
-};/* struct BitVectorBitOf */
+}; /* struct BitVectorBitOf */
-/**
- * Hash function for the BitVectorBitOf objects.
- */
-struct CVC4_PUBLIC BitVectorBitOfHashFunction {
- size_t operator()(const BitVectorBitOf& b) const {
- return b.bitIndex;
- }
-};/* struct BitVectorBitOfHashFunction */
-
-
-
-struct CVC4_PUBLIC BitVectorSize {
+struct CVC4_PUBLIC BitVectorSize
+{
unsigned size;
- BitVectorSize(unsigned size)
- : size(size) {}
- operator unsigned () const { return size; }
-};/* struct BitVectorSize */
+ BitVectorSize(unsigned size) : size(size) {}
+ operator unsigned() const { return size; }
+}; /* struct BitVectorSize */
-struct CVC4_PUBLIC BitVectorRepeat {
+struct CVC4_PUBLIC BitVectorRepeat
+{
unsigned repeatAmount;
- BitVectorRepeat(unsigned repeatAmount)
- : repeatAmount(repeatAmount) {}
- operator unsigned () const { return repeatAmount; }
-};/* struct BitVectorRepeat */
+ BitVectorRepeat(unsigned repeatAmount) : repeatAmount(repeatAmount) {}
+ operator unsigned() const { return repeatAmount; }
+}; /* struct BitVectorRepeat */
-struct CVC4_PUBLIC BitVectorZeroExtend {
+struct CVC4_PUBLIC BitVectorZeroExtend
+{
unsigned zeroExtendAmount;
BitVectorZeroExtend(unsigned zeroExtendAmount)
- : zeroExtendAmount(zeroExtendAmount) {}
- operator unsigned () const { return zeroExtendAmount; }
-};/* struct BitVectorZeroExtend */
+ : zeroExtendAmount(zeroExtendAmount)
+ {
+ }
+ operator unsigned() const { return zeroExtendAmount; }
+}; /* struct BitVectorZeroExtend */
-struct CVC4_PUBLIC BitVectorSignExtend {
+struct CVC4_PUBLIC BitVectorSignExtend
+{
unsigned signExtendAmount;
BitVectorSignExtend(unsigned signExtendAmount)
- : signExtendAmount(signExtendAmount) {}
- operator unsigned () const { return signExtendAmount; }
-};/* struct BitVectorSignExtend */
+ : signExtendAmount(signExtendAmount)
+ {
+ }
+ operator unsigned() const { return signExtendAmount; }
+}; /* struct BitVectorSignExtend */
-struct CVC4_PUBLIC BitVectorRotateLeft {
+struct CVC4_PUBLIC BitVectorRotateLeft
+{
unsigned rotateLeftAmount;
BitVectorRotateLeft(unsigned rotateLeftAmount)
- : rotateLeftAmount(rotateLeftAmount) {}
- operator unsigned () const { return rotateLeftAmount; }
-};/* struct BitVectorRotateLeft */
+ : rotateLeftAmount(rotateLeftAmount)
+ {
+ }
+ operator unsigned() const { return rotateLeftAmount; }
+}; /* struct BitVectorRotateLeft */
-struct CVC4_PUBLIC BitVectorRotateRight {
+struct CVC4_PUBLIC BitVectorRotateRight
+{
unsigned rotateRightAmount;
BitVectorRotateRight(unsigned rotateRightAmount)
- : rotateRightAmount(rotateRightAmount) {}
- operator unsigned () const { return rotateRightAmount; }
-};/* struct BitVectorRotateRight */
+ : rotateRightAmount(rotateRightAmount)
+ {
+ }
+ operator unsigned() const { return rotateRightAmount; }
+}; /* struct BitVectorRotateRight */
-template <typename T>
-struct CVC4_PUBLIC UnsignedHashFunction {
- inline size_t operator()(const T& x) const {
- return (size_t)x;
+struct CVC4_PUBLIC IntToBitVector
+{
+ unsigned size;
+ IntToBitVector(unsigned size) : size(size) {}
+ operator unsigned() const { return size; }
+}; /* struct IntToBitVector */
+
+/* -----------------------------------------------------------------------
+ ** Hash Function structs
+ * ----------------------------------------------------------------------- */
+
+/*
+ * Hash function for the BitVector constants.
+ */
+struct CVC4_PUBLIC BitVectorHashFunction
+{
+ inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
+}; /* struct BitVectorHashFunction */
+
+/**
+ * Hash function for the BitVectorExtract objects.
+ */
+struct CVC4_PUBLIC BitVectorExtractHashFunction
+{
+ size_t operator()(const BitVectorExtract& extract) const
+ {
+ size_t hash = extract.low;
+ hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+ return hash;
}
-};/* struct UnsignedHashFunction */
+}; /* struct BitVectorExtractHashFunction */
-inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+/**
+ * Hash function for the BitVectorBitOf objects.
+ */
+struct CVC4_PUBLIC BitVectorBitOfHashFunction
+{
+ size_t operator()(const BitVectorBitOf& b) const { return b.bitIndex; }
+}; /* struct BitVectorBitOfHashFunction */
+
+template <typename T>
+struct CVC4_PUBLIC UnsignedHashFunction
+{
+ inline size_t operator()(const T& x) const { return (size_t)x; }
+}; /* struct UnsignedHashFunction */
+
+/* -----------------------------------------------------------------------
+ ** Output stream
+ * ----------------------------------------------------------------------- */
+
+inline std::ostream& operator<<(std::ostream& os,
+ const BitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
+{
return os << bv.toString();
}
-inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+ const BitVectorExtract& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
+{
return os << "[" << bv.high << ":" << bv.low << "]";
}
-inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+ const BitVectorBitOf& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
+{
return os << "[" << bv.bitIndex << "]";
}
-}/* CVC4 namespace */
+inline std::ostream& operator<<(std::ostream& os,
+ const IntToBitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
+{
+ return os << "[" << bv.size << "]";
+}
+
+} // namespace CVC4
-#endif /* __CVC4__BITVECTOR_H */
+#endif /* CVC4__BITVECTOR_H */
projects / cvc5.git / blobdiff