Commit 73cdc963 authored by Peter Navrátil's avatar Peter Navrátil
Browse files

changed some static to nonstatic

parent 17a0746c

bvec_cudd.cpp

+47 −56
Original line number Diff line number Diff line
@@ -116,21 +116,19 @@ namespace cudd { 
    }



    Bvec

    Bvec::bvec_coerce(size_t bitnum, const Bvec& vec) {

    	Cudd& manager = vec.m_manager;

    	Bvec res = bvec_false(manager, bitnum);

        size_t minnum = std::min(bitnum, vec.bitnum());

    Bvec::bvec_coerce(size_t bits) const {

    	Bvec res = bvec_false(m_manager, bits);

        size_t minnum = std::min(bits, bitnum());

    	for (size_t i = 0; i < minnum; ++i) {

    		res[i] = vec[i];

    		res[i] = m_bitvec[i];

    	}

    	return res;

    }



    bool

    Bvec::bvec_isConst(const Bvec& src) {

    	Cudd& manager = src.m_manager;

    	for (size_t i = 0; i < src.bitnum(); ++i) {

    		if (src[i].IsVar()) {

    Bvec::bvec_isConst() const {

    	for (size_t i = 0; i < bitnum(); ++i) {

    		if (m_bitvec[i].IsVar()) {

    			return false;

    		}

    	}
@@ -138,12 +136,12 @@ namespace cudd { 
    }



    int

    Bvec::bvec_val(const Bvec& src) {

    Bvec::bvec_val() const {

    	int val = 0;

    	for (size_t i = src.bitnum(); i >= 1U; --i) {

    		if (src[i - 1U].IsOne())

    	for (size_t i = bitnum(); i >= 1U; --i) {

    		if (m_bitvec[i - 1U].IsOne())

    			val = (val << 1) | 1;

    		else if (src[i - 1U].IsZero())

    		else if (m_bitvec[i - 1U].IsZero())

    			val = val << 1;

    		else

    			return 0;
@@ -266,29 +264,27 @@ namespace cudd { 
    }



    Bvec

    Bvec::bvec_mulfixed(const Bvec& src, size_t con) {

    	Cudd& manager = src.m_manager;

    	Bvec res(manager);

    Bvec::bvec_mulfixed(size_t con) const {

    	Bvec res(m_manager);



    	if (src.bitnum() == 0) {

    	if (bitnum() == 0) {

    		//DEFAULT(res);

    		return res;

    	}



    	if (con == 0) {

    		return bvec_false(manager, src.bitnum()); /* return false array (base case) */

    		return bvec_false(m_manager, bitnum()); /* return false array (base case) */

    	}



    	//Bvec next = bvec_false(manager, src.bitnum());

    	Bvec next = reserve(manager, src.bitnum());

    	for (size_t i = 1; i < src.bitnum(); ++i) {

    		next.m_bitvec.push_back(src[i - 1]);

    	Bvec next = reserve(m_manager, bitnum());

    	for (size_t i = 1; i < bitnum(); ++i) {

    		next.m_bitvec.push_back(m_bitvec[i - 1]);

    	}



    	Bvec rest = bvec_mulfixed(next, con >> 1);

    	Bvec rest = next.bvec_mulfixed(con >> 1);



    	if (con & 0x1) {

    		res = bvec_add(src, rest);

    		res = bvec_add(*this, rest);

    	} else {

    		res = rest;

    	}
@@ -306,7 +302,7 @@ namespace cudd { 
            return res;

        }

        Bvec leftshifttmp = Bvec(left);

        Bvec leftshift = bvec_coerce(bitnum, leftshifttmp);

        Bvec leftshift = leftshifttmp.bvec_coerce(bitnum);



        for (size_t i = 0; i < right.bitnum(); ++i) {

    		Bvec added = bvec_add(res, leftshift);
@@ -330,18 +326,16 @@ namespace cudd { 
    Bvec::bvec_div_rec(Bvec& divisor, Bvec& remainder, Bvec& result, size_t step) {

    	Cudd& manager = result.m_manager;

    	BDD isSmaller = bvec_lte(divisor, remainder);

    	Bvec newResult = bvec_shlfixed(result, 1, isSmaller);

    	Bvec newResult = result.bvec_shlfixed(1, isSmaller);

    	Bvec zero = bvec_build(manager, divisor.bitnum(), false);

    	//Bvec sub = bvec_build(manager,divisor.bitnum(), false);

    	Bvec sub = reserve(manager, divisor.bitnum());



    	for (size_t i = 0; i < divisor.bitnum(); ++i) {

    		//sub[i] = isSmaller.Ite(divisor[i], zero[i]);

    		sub.m_bitvec.push_back(isSmaller.Ite(divisor[i], zero[i]));

    	}



    	Bvec tmp = remainder - sub;

    	Bvec newRemainder = bvec_shlfixed(tmp, 1, result[divisor.bitnum() - 1]);

    	Bvec newRemainder = tmp.bvec_shlfixed(1, result[divisor.bitnum() - 1]);



    	if (step > 1) {

    		bvec_div_rec(divisor, newRemainder, newResult, step - 1);
@@ -352,16 +346,15 @@ namespace cudd { 
    }



    int

    Bvec::bvec_divfixed(const Bvec& src, size_t con, Bvec& result, Bvec& rem) {

    Bvec::bvec_divfixed(size_t con, Bvec& result, Bvec& rem) const {

    	if (con > 0) {

    		Cudd& manager = src.m_manager;

    		Bvec divisor = bvec_con(manager, src.bitnum(), con);

    		Bvec tmp = bvec_false(manager, src.bitnum());

    		Bvec tmpremainder = bvec_shlfixed(tmp, 1, src[src.bitnum() - 1]);

    		Bvec res = bvec_shlfixed(src, 1, manager.bddZero());

    		Bvec divisor = bvec_con(m_manager, bitnum(), con);

    		Bvec tmp = bvec_false(m_manager, bitnum());

    		Bvec tmpremainder = tmp.bvec_shlfixed(1, m_bitvec[bitnum() - 1]);

    		Bvec res = bvec_shlfixed(1, m_manager.bddZero());



    		bvec_div_rec(divisor, tmpremainder, result, divisor.bitnum());

    		Bvec remainder = bvec_shrfixed(tmpremainder, 1, manager.bddZero());

    		Bvec remainder = tmpremainder.bvec_shrfixed(1, m_manager.bddZero());



    		result = res;

    		rem = remainder;
@@ -380,9 +373,9 @@ namespace cudd { 
            return 1;

    	}



    	Bvec rem = bvec_coerce(bitnum, left);

    	Bvec divtmp = bvec_coerce(bitnum, right);

    	Bvec div = bvec_shlfixed(divtmp, left.bitnum(), manager.bddZero());

    	Bvec rem = left.bvec_coerce(bitnum);

    	Bvec divtmp = right.bvec_coerce(bitnum);

    	Bvec div = divtmp.bvec_shlfixed(left.bitnum(), manager.bddZero());



    	Bvec res = bvec_false(manager, right.bitnum());
@@ -406,7 +399,7 @@ namespace cudd { 
    	}



    	result = res;

    	remainder = bvec_coerce(right.bitnum(), rem);

    	remainder = rem.bvec_coerce(right.bitnum());

    	return 0;

    }
@@ -444,27 +437,26 @@ namespace cudd { 
    }



    Bvec

    Bvec::bvec_shlfixed(const Bvec& src, int pos, const BDD& con) {

    	Cudd& manager = src.m_manager;

    	Bvec res(manager);

    	size_t min = src.bitnum() < pos ? src.bitnum() : pos;

    Bvec::bvec_shlfixed(int pos, const BDD& con) const {

    	Bvec res(m_manager);

    	size_t min = bitnum() < pos ? bitnum() : pos;



    	if (pos < 0U) {

    		//bdd_error(BVEC_SHIFT);

    		//DEFAULT(res);

    		return res;

    	}

    	if (src.bitnum() == 0) {

    	if (bitnum() == 0) {

    		//DEFAULT(res);

    		return res;

    	}



    	res = reserve(manager, src.bitnum());

    	res = reserve(m_manager, bitnum());

    	for (size_t i = 0; i < min; ++i) {

    		res.m_bitvec.push_back(con);

    	}

    	for (size_t i = min; i < src.bitnum(); i++) {

    		res.m_bitvec.push_back(src[i - pos]);

    	for (size_t i = min; i < bitnum(); i++) {

    		res.m_bitvec.push_back(m_bitvec[i - pos]);

    	}

    	return res;

    }
@@ -507,9 +499,8 @@ namespace cudd { 
    }



    Bvec

    Bvec::bvec_shrfixed(const Bvec& src, int pos, const BDD& con) {

    	Cudd& manager = src.m_manager;

    	Bvec res(manager);

    Bvec::bvec_shrfixed(int pos, const BDD& con) const {

    	Bvec res(m_manager);



    	if (pos < 0) {

    		//bdd_error(BVEC_SHIFT);
@@ -517,19 +508,19 @@ namespace cudd { 
    		return res;

    	}



    	if (src.bitnum() == 0) {

    	if (bitnum() == 0) {

    		//DEFAULT(res);

    		return res;

    	}

    	size_t maxnum = std::max(static_cast<int>(src.bitnum() - pos), 0);

    	res = bvec_false(manager, src.bitnum());

    	size_t maxnum = std::max(static_cast<int>(bitnum() - pos), 0);

    	res = bvec_false(m_manager, bitnum());



    	for (size_t i = maxnum; i < src.bitnum(); ++i) {

    	for (size_t i = maxnum; i < bitnum(); ++i) {

    		res[i] = con;

    	}



    	for (size_t i = 0; i < maxnum; ++i) {

    		res[i] = src[i + pos];

    		res[i] = m_bitvec[i + pos];

    	}

    	return res;

    }

bvec_cudd.h

+14 −14
Original line number Diff line number Diff line
@@ -63,13 +63,13 @@ namespace cudd { 
    	bvec_varvec(Cudd& manager, size_t bitnum, int *var);



    	Bvec

    	bvec_coerce(size_t bitnum);

    	bvec_coerce(size_t bitnum) const;



    	bool

    	bvec_isConst();

    	bvec_isConst() const;



    	int

    	bvec_val();

    	bvec_val() const;



    	static Bvec

    	bvec_copy(const Bvec& other);
@@ -89,14 +89,14 @@ namespace cudd { 
    	static Bvec

    	bvec_sub(const Bvec& left, const Bvec& right);



    	static Bvec

    	bvec_mulfixed(const Bvec& src, size_t con);

    	Bvec

    	bvec_mulfixed(size_t con) const;



    	static Bvec

    	bvec_mul(const Bvec& left, const Bvec& right);



    	static int

    	bvec_divfixed(const Bvec& src, size_t con, Bvec& result, Bvec& rem);

    	int

    	bvec_divfixed(size_t con, Bvec& result, Bvec& rem) const;



    	static int

    	bvec_div(const Bvec& left, const Bvec& right, Bvec& result, Bvec& rem);
@@ -107,14 +107,14 @@ namespace cudd { 
    	static Bvec

    	bvec_ite(const BDD& val, const Bvec& left, const Bvec& right);



    	static Bvec

    	bvec_shlfixed(const Bvec& src, int pos, const BDD& con);

    	Bvec

    	bvec_shlfixed(int pos, const BDD& con) const;



    	static Bvec

    	bvec_shl(const Bvec& left, const Bvec& right, const BDD& con);



    	static Bvec

    	bvec_shrfixed(const Bvec& src, int pos, const BDD& con);

    	Bvec

    	bvec_shrfixed(int pos, const BDD& con) const;



    	static Bvec

    	bvec_shr(const Bvec& left, const Bvec& right, const BDD& con);
@@ -159,13 +159,13 @@ namespace cudd { 
    	operator!(void) const { return bvec_map1(*this, bdd_not); }



    	Bvec

    	operator<<(size_t con) const { return bvec_shlfixed(*this, con, m_manager.bddZero()); }

    	operator<<(size_t con) const { return bvec_shlfixed(con, m_manager.bddZero()); }



    	Bvec

    	operator<<(const Bvec& other) const { return bvec_shl(*this, other, m_manager.bddZero()); }



    	Bvec

    	operator>>(size_t con) const { return bvec_shrfixed(*this, con, m_manager.bddZero()); }

    	operator>>(size_t con) const { return bvec_shrfixed(con, m_manager.bddZero()); }



    	Bvec

    	operator>>(const Bvec& other) const { return bvec_shr(*this, other, m_manager.bddZero()); }
@@ -177,7 +177,7 @@ namespace cudd { 
    	operator-(const Bvec& other) { return bvec_sub(*this, other); }



    	Bvec

    	operator*(size_t con) const { return bvec_mulfixed(*this, con); }

    	operator*(size_t con) const { return bvec_mulfixed(con); }



    	Bvec

    	operator*(const Bvec& other) const { return bvec_mul(*this, other); }

bvec_sylvan.cpp

+48 −55
Original line number Diff line number Diff line
@@ -45,7 +45,7 @@ namespace sylvan { 
        return m_bitvec.size();

    }



    int

    bool

    Bvec::empty() const {

        return m_bitvec.empty();

    }
@@ -101,41 +101,35 @@ namespace sylvan { 
	}



	Bvec

    Bvec::bvec_coerce(size_t bitnum, const Bvec& vec) {

    Bvec::bvec_coerce(size_t bits) const {

		LACE_ME;

        Bvec res = bvec_false(bitnum);

		size_t minnum = std::min(bitnum, vec.bitnum());

        Bvec res = bvec_false(bits);

		size_t minnum = std::min(bits, bitnum());

		for (size_t i = 0; i < minnum; ++i) {

			res[i] = vec[i];

			res[i] = m_bitvec[i];

		}

		return res;

	}



	int

    Bvec::bvec_isConst(const Bvec& src) {

	//bool Bvec::bvec_isConst(const Bvec& src) {

	//Bdd Bvec::bvec_isConst(const Bvec& src) {

	bool

    Bvec::bvec_isConst() const {

		LACE_ME;

		for (size_t i = 0; i < src.bitnum(); ++i) {

			if (!src[i].isConstant()) {

				return 0;

				//return false;

				//return Bdd::bddZero();

		for (size_t i = 0; i < bitnum(); ++i) {

			if (!m_bitvec[i].isConstant()) {

				return false;

			}

		}

		return 1;

		//return true;

		//return Bdd::bddOne();

		return true;

	}



	int

    Bvec::bvec_val(const Bvec& src) {

    Bvec::bvec_val() const {

		LACE_ME;

		int val = 0;

		for (size_t i = src.bitnum(); i >= 1U; --i) {

			if (src[i - 1U].isOne())

		for (size_t i = bitnum(); i >= 1U; --i) {

			if (m_bitvec[i - 1U].isOne())

				val = (val << 1) | 1;

			else if (src[i - 1U].isZero())

			else if (m_bitvec[i - 1U].isZero())

				val = val << 1;

			else

				return 0;
@@ -251,28 +245,27 @@ namespace sylvan { 
	}



	Bvec

    Bvec::bvec_mulfixed(const Bvec& src, size_t con) {

    Bvec::bvec_mulfixed(size_t con) const {

		LACE_ME;

		Bvec res;



		if (src.bitnum() == 0) {

		if (bitnum() == 0) {

			//DEFAULT(res);

			return res;

		}



		if (con == 0) {

			return bvec_false(src.bitnum());  /* return false array (base case) */

			return bvec_false(bitnum());  /* return false array (base case) */

		}



		//Bvec next = bvec_false(src.bitnum());

		Bvec next = reserve(src.bitnum());

		for (size_t i = 1; i < src.bitnum(); ++i) {

			next.m_bitvec.push_back(src[i - 1]);

		Bvec next = reserve(bitnum());

		for (size_t i = 1; i < bitnum(); ++i) {

			next.m_bitvec.push_back(m_bitvec[i - 1]);

		}

		Bvec rest = bvec_mulfixed(next, con >> 1);

		Bvec rest = next.bvec_mulfixed(con >> 1);



		if (con & 0x1) {

			res = bvec_add(src, rest);

			res = bvec_add(*this, rest);

		} else {

			res = rest;

		}
@@ -290,7 +283,7 @@ namespace sylvan { 
			return res;

		}

		Bvec leftshifttmp = Bvec(left);

		Bvec leftshift = bvec_coerce(bitnum, leftshifttmp);

		Bvec leftshift = leftshifttmp.bvec_coerce(bitnum);



		for (size_t i = 0; i < right.bitnum(); ++i) {

			Bvec added = bvec_add(res, leftshift);
@@ -315,7 +308,7 @@ namespace sylvan { 
    Bvec::bvec_div_rec(Bvec divisor, Bvec& remainder, Bvec& result, size_t step) {

		LACE_ME;

		Bdd isSmaller = bvec_lte(divisor, remainder);

		Bvec newResult = bvec_shlfixed(result, 1, isSmaller);

		Bvec newResult = result.bvec_shlfixed(1, isSmaller);

		Bvec zero = bvec_false(divisor.bitnum());

		Bvec sub = reserve(divisor.bitnum());
@@ -324,7 +317,7 @@ namespace sylvan { 
		}



		Bvec tmp = remainder - sub;

		Bvec newRemainder = bvec_shlfixed(tmp, 1, result[divisor.bitnum() - 1]);

		Bvec newRemainder = tmp.bvec_shlfixed(1, result[divisor.bitnum() - 1]);



		if (step > 1) {

			bvec_div_rec(divisor, newRemainder, newResult, step - 1);
@@ -335,16 +328,16 @@ namespace sylvan { 
	}



	int

    Bvec::bvec_divfixed(const Bvec& src, size_t con, Bvec& result, Bvec& rem) {

    Bvec::bvec_divfixed(size_t con, Bvec& result, Bvec& rem) {

		LACE_ME;

		if (con > 0) {

			Bvec divisor = bvec_con(src.bitnum(), con);

			Bvec tmp = bvec_false(src.bitnum());

			Bvec tmpremainder = bvec_shlfixed(tmp, 1, src[src.bitnum() - 1]);

			Bvec res = bvec_shlfixed(src, 1, Bdd::bddZero());

			Bvec divisor = bvec_con(bitnum(), con);

			Bvec tmp = bvec_false(bitnum());

			Bvec tmpremainder = tmp.bvec_shlfixed(1, m_bitvec[bitnum() - 1]);

			Bvec res = bvec_shlfixed(1, Bdd::bddZero());



			bvec_div_rec(divisor, tmpremainder, result, divisor.bitnum());

			Bvec remainder = bvec_shrfixed(tmpremainder, 1, Bdd::bddZero());

			Bvec remainder = tmpremainder.bvec_shrfixed(1, Bdd::bddZero());



			result = res;

			rem = remainder;
@@ -362,9 +355,9 @@ namespace sylvan { 
			//return bdd_error(BVEC_SIZE);

		}



		Bvec rem = bvec_coerce(bitnum, left);

		Bvec divtmp = bvec_coerce(bitnum, right);

		Bvec div = bvec_shlfixed(divtmp, left.bitnum(), Bdd::bddZero());

		Bvec rem = left.bvec_coerce(bitnum);

		Bvec divtmp = right.bvec_coerce(bitnum);

		Bvec div = divtmp.bvec_shlfixed(left.bitnum(), Bdd::bddZero());



		Bvec res = bvec_false(right.bitnum());
@@ -388,7 +381,7 @@ namespace sylvan { 
		}



		result = res;

		remainder = bvec_coerce(right.bitnum(), rem);

		remainder = rem.bvec_coerce(right.bitnum());

		return 0;

	}
@@ -425,27 +418,27 @@ namespace sylvan { 
	}



	Bvec

    Bvec::bvec_shlfixed(const Bvec& src, int pos, const Bdd& con) {

    Bvec::bvec_shlfixed(int pos, const Bdd& con) const {

		LACE_ME;

		Bvec res;

		size_t min = src.bitnum() < pos ? src.bitnum() : pos;

		size_t min = bitnum() < pos ? bitnum() : pos;



		if (pos < 0) {

			//bdd_error(BVEC_SHIFT);

			//DEFAULT(res);

			return res;

		}

		if (src.bitnum() == 0) {

		if (bitnum() == 0) {

			//DEFAULT(res);

			return res;

		}



		res = reserve(src.bitnum());

		res = reserve(bitnum());

		for (size_t i = 0; i < min; ++i) {

			res.m_bitvec.push_back(con);

		}

		for (size_t i = min; i < src.bitnum(); i++) {

			res.m_bitvec.push_back(src[i - pos]);

		for (size_t i = min; i < bitnum(); i++) {

			res.m_bitvec.push_back(m_bitvec[i - pos]);

		}



		return res;
@@ -490,7 +483,7 @@ namespace sylvan { 
	}



	Bvec

    Bvec::bvec_shrfixed(const Bvec& src, int pos, const Bdd& con) {

    Bvec::bvec_shrfixed(int pos, const Bdd& con) const {

		LACE_ME;

		Bvec res;

		if (pos < 0) {
@@ -499,20 +492,20 @@ namespace sylvan { 
			return res;

		}



		if (src.bitnum() == 0) {

		if (bitnum() == 0) {

			//DEFAULT(res);

			return res;

		}



		size_t maxnum = std::max(static_cast<int>(src.bitnum() - pos), 0);

		res = bvec_false(src.bitnum());

		size_t maxnum = std::max(static_cast<int>(bitnum() - pos), 0);

		res = bvec_false(bitnum());



		for (size_t i = maxnum; i < src.bitnum(); ++i) {

		for (size_t i = maxnum; i < bitnum(); ++i) {

			res[i] = con;

		}



		for (size_t i = 0; i < maxnum; ++i) {

			res[i] = src[i + pos];

			res[i] = m_bitvec[i + pos];

		}

		return res;

	}

bvec_sylvan.h

+18 −18
Original line number Diff line number Diff line
@@ -45,7 +45,7 @@ public: 
	size_t

    bitnum() const;



	int

	bool

    empty() const;



	static Bvec
@@ -66,14 +66,14 @@ public: 
	static Bvec

    bvec_varvec(size_t bitnum, int *var);



	static Bvec

    bvec_coerce(size_t bitnum, const Bvec& vec);

	Bvec

    bvec_coerce(size_t bitnum) const;



	static int

    bvec_isConst(const Bvec& src);

	bool

    bvec_isConst() const;



	static int

    bvec_val(const Bvec& src);

	int

    bvec_val() const;



	//Bvec

    //bvec_copy(const Bvec& v);
@@ -94,14 +94,14 @@ public: 
	static Bvec

    bvec_sub(const Bvec& left, const Bvec& right);



	static Bvec

    bvec_mulfixed(const Bvec& src, size_t con);

	Bvec

    bvec_mulfixed(size_t con) const;



	static Bvec

    bvec_mul(const Bvec& left, const Bvec& right);



	static int

    bvec_divfixed(const Bvec& src, size_t con, Bvec& result, Bvec& rem);

	int

    bvec_divfixed(size_t con, Bvec& result, Bvec& rem);



	static int

    bvec_div(const Bvec& left, const Bvec& right, Bvec& result, Bvec& rem);
@@ -112,14 +112,14 @@ public: 
	static Bvec

    bvec_ite(const Bdd& a, const Bvec& left, const Bvec& right);



	static Bvec

    bvec_shlfixed(const Bvec& src, int pos, const Bdd& con);

	Bvec

    bvec_shlfixed(int pos, const Bdd& con) const;



	static Bvec

    bvec_shl(const Bvec& left, const Bvec& right, const Bdd& con);



	static Bvec

    bvec_shrfixed(const Bvec& src, int pos, const Bdd& con);

	Bvec

    bvec_shrfixed(int pos, const Bdd& con) const;



	static Bvec

    bvec_shr(const Bvec& left, const Bvec& right, const Bdd& con);
@@ -164,13 +164,13 @@ public: 
    operator!(void) const { return bvec_map1(*this, bdd_not); }



	Bvec

    operator<<(size_t con) const { return bvec_shlfixed(*this, con, Bdd::bddZero()); }

    operator<<(size_t con) const { return bvec_shlfixed(con, Bdd::bddZero()); }



	Bvec

    operator<<(const Bvec& other) const { return bvec_shl(*this, other,Bdd::bddZero()); }



	Bvec

    operator>>(size_t con) const { return bvec_shrfixed(*this, con, Bdd::bddZero()); }

    operator>>(size_t con) const { return bvec_shrfixed(con, Bdd::bddZero()); }



	Bvec

    operator>>(const Bvec& other) const { return bvec_shr(*this, other, Bdd::bddZero()); }
@@ -182,7 +182,7 @@ public: 
    operator-(const Bvec& other) { return bvec_sub(*this, other); }



	Bvec

    operator*(size_t con) const { return bvec_mulfixed(*this, con); }

    operator*(size_t con) const { return bvec_mulfixed(con); }



	Bvec

    operator*(const Bvec other) const { return bvec_mul(*this, other); }

tests.cpp

+6 −6
Original line number Diff line number Diff line
@@ -237,8 +237,8 @@ TEST_CASE("Manipulation tests") { 
        bvec buddy_val = bvec_con_buddy(size, val);



        REQUIRE(isEqual(cudd_val, sylvan_val, buddy_val));

        REQUIRE(cudd::Bvec::bvec_isConst(cudd_val) == 1);

        REQUIRE(sylvan::Bvec::bvec_isConst(sylvan_val) == 1);

        REQUIRE(cudd_val.bvec_isConst() == 1);

        REQUIRE(sylvan_val.bvec_isConst() == 1);

        REQUIRE(bvec_isconst(buddy_val) == 1);



        int offset = 1;
@@ -247,8 +247,8 @@ TEST_CASE("Manipulation tests") { 
        sylvan::Bvec sylvan_var = sylvan::Bvec::bvec_var(size, offset, step);

        bvec buddy_var = bvec_var_buddy(size, offset, step);

        //TODO isequalvar

        REQUIRE(cudd::Bvec::bvec_isConst(cudd_var) == 0);

        REQUIRE(sylvan::Bvec::bvec_isConst(sylvan_var) == 0);

        REQUIRE(cudd_var.bvec_isConst() == 0);

        REQUIRE(sylvan_var.bvec_isConst() == 0);

        REQUIRE(bvec_isconst(buddy_var) == 0);

    }
@@ -261,8 +261,8 @@ TEST_CASE("Manipulation tests") { 


        REQUIRE(isEqual(bvec_cudd, bvec_sylvan, bvec_buddy));



        int cudd_val = cudd::Bvec::bvec_val(bvec_cudd);

        int sylvan_val = sylvan::Bvec::bvec_val(bvec_sylvan);

        int cudd_val = bvec_cudd.bvec_val();

        int sylvan_val = bvec_sylvan.bvec_val();

        int buddy_val = bvec_val(bvec_buddy);

        REQUIRE(cudd_val == sylvan_val);

        REQUIRE(cudd_val == buddy_val);