improved templated version (218b1db4) · Commits · Martin Jonáš / BDD

CMakeLists.txt

+2 −0

Original line number	Diff line number	Diff line
		@@ -13,7 +13,9 @@ set(SOURCE_FILES bvec_cudd.h bvec_cudd.cpp bvec_sylvan.cpp bvec_sylvan.h)
		add_executable(bdd ${SOURCE_FILES} bdd.cpp)
		add_executable(validation_tests ${SOURCE_FILES} validation_tests.cpp main.cpp)
		add_executable(unit_tests ${SOURCE_FILES} unit_tests.cpp main.cpp)
		add_executable(bdd_template templateExample.cpp)

		TARGET_LINK_LIBRARIES(bdd ${LIBRARIES})
		TARGET_LINK_LIBRARIES(validation_tests ${LIBRARIES})
		TARGET_LINK_LIBRARIES(unit_tests ${LIBRARIES})
		TARGET_LINK_LIBRARIES(bdd_template ${LIBRARIES})

0 → 100644

+58 −0

Original line number	Diff line number	Diff line
		#include <cuddObj.hh>
		#include <sylvan_obj.hpp>

		class CuddManager {
		private:

		const cudd::Cudd& m_manager;

		public:
		CuddManager(const cudd::Cudd& manager) : m_manager(manager) {}

		cudd::BDD
		bddOne() const {
		return m_manager.bddOne();
		}

		cudd::BDD
		bddZero() const {
		return m_manager.bddZero();
		}

		cudd::BDD
		bddVar(int pos) const {
		return m_manager.bddVar(pos);
		}

		bool
		isConst(const cudd::BDD& bdd) {
		return (bdd.IsOne() \|\| bdd.IsZero());
		}

		};

		class SylvanManager {
		public:
		SylvanManager() = default;

		sylvan::Bdd
		bddOne() const {
		return sylvan::Bdd::bddOne();
		}

		sylvan::Bdd
		bddZero() const {
		return sylvan::Bdd::bddZero();
		}

		sylvan::Bdd
		bddVar(int pos) const {
		return sylvan::Bdd::bddVar(pos);
		}

		bool
		isConst(const sylvan::Bdd& bdd) {
		return bdd.isConstant();
		}

		};

+10 −23

Original line number	Diff line number	Diff line
		#include "bvec_cudd.h"
		#include "templatedBvec.hpp"
		#include "managers.h"

		int main(int argc, char ** argv) {
		using namespace cudd;
		Cudd manager;
		auto createConst = [&](bool isTrue) {
		if (isTrue) {
		return manager.bddOne();
		}
		return manager.bddZero();
		};
		auto createVal = [&](int pos) {
		return manager.bddVar(pos);
		};
		auto checkVal = [&](const cudd::BDD& bdd, int choice) {
		if (choice == 0) {
		return bdd.IsZero();
		} else if (choice == 1) {
		return bdd.IsOne();
		} else {
		return (bdd.IsOne() \|\| bdd.IsZero());
		}
		};
		using Tconst = decltype(createConst);
		using Tval = decltype(createVal);
		using Tcheck = decltype(checkVal);
		Bvec<cudd::BDD, Tconst, Tval, Tcheck> bvec(8, true, createConst, createVal, checkVal);
		CuddManager cudd_manager(manager);

		using CuddManagerT = decltype(cudd_manager);
		Bvec<cudd::BDD, CuddManagerT> cudd_bvec(8, true, cudd_manager);

		SylvanManager sylvan_manager{};
		using SylvanManagerT = decltype(sylvan_manager);
		Bvec<sylvan::Bdd, SylvanManagerT> sylvan_bvec(8, true, sylvan_manager);

		return 0;
		}

+96 −102

File changed.

Preview size limit exceeded, changes collapsed.