diff --git a/.github/workflows/test_cmake.yml b/.github/workflows/test_cmake.yml
new file mode 100644
index 00000000..4a1866a5
--- /dev/null
+++ b/.github/workflows/test_cmake.yml
@@ -0,0 +1,53 @@
+name: CMake Test
+
+on:
+    pull_request:
+    push:
+        branches:
+            - main
+
+jobs:
+  cmake-test:
+    runs-on: ubuntu-24.04
+    strategy:
+      fail-fast: false
+      matrix:
+        cmake-version: 
+          - '3.18' # debian11
+          - '3.22' # ubuntu22.04
+          - '3.25' # debian12
+          - '3.26' # rhel8, rhel9
+          - '3.28' # ubuntu24.04, leap15.6
+          - '3.30' # rhel10
+          - '3.31' # debian13
+          - 'latest'
+        build_shared_libs: ['ON', 'OFF']
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Setup cmake
+        uses: jwlawson/actions-setup-cmake@v2
+        with:
+          cmake-version: ${{ matrix.cmake-version }}
+
+      - name: Check version
+        run: cmake --version
+
+      - name: Configure
+        run: |
+          cmake -S . -B /tmp/build \
+            -DCUDD_BUILD_WITH_STATS=ON \
+            -DCUDD_BUILD_DDDMP=ON \
+            -DCUDD_BUILD_TESTS=ON \
+            -DCUDD_BUILD_SHARED_LIBS=${{ matrix.build_shared_libs }}
+
+      - name: Build
+        run: cmake --build /tmp/build
+
+      - name: Test 
+        run: ctest --test-dir /tmp/build --output-on-failure
+
+      - name: Install
+        run: cmake --install /tmp/build --prefix /tmp/install
diff --git a/.github/workflows/test_toolset.yml b/.github/workflows/test_toolset.yml
new file mode 100644
index 00000000..6e2f6b9b
--- /dev/null
+++ b/.github/workflows/test_toolset.yml
@@ -0,0 +1,52 @@
+name: Toolset Test
+
+on:
+    pull_request:
+    push:
+        branches:
+            - main
+
+jobs:
+  cmake-test:
+    runs-on: ubuntu-24.04
+    container:
+      image: docker.io/gcc:${{ matrix.toolset-version }}
+    strategy:
+      fail-fast: false
+      matrix:
+        toolset-version: ['10', '11', '12', '13', '14', '15']
+        build_shared_libs: ['ON', 'OFF']
+
+    env:
+        CMAKE_C_COMPILER: gcc
+        CMAKE_CXX_COMPILER: g++
+        CMAKE_GENERATOR: Ninja
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Setup cmake
+        run: |
+          apt-get update
+          apt-get install -y cmake ninja-build
+
+      - name: Check version
+        run: cmake --version
+
+      - name: Configure
+        run: |
+          cmake -S . -B /tmp/build \
+            -DCUDD_BUILD_WITH_STATS=ON \
+            -DCUDD_BUILD_DDDMP=ON \
+            -DCUDD_BUILD_TESTS=ON \
+            -DCUDD_BUILD_SHARED_LIBS=${{ matrix.build_shared_libs }}
+
+      - name: Build
+        run: cmake --build /tmp/build
+
+      - name: Test 
+        run: ctest --test-dir /tmp/build --output-on-failure
+
+      - name: Install
+        run: cmake --install /tmp/build --prefix /tmp/install
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..47add18b
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,32 @@
+# Build directories
+build/
+install/
+out/
+bin/
+lib/
+
+# CMake-generated files and folders
+CMakeCache.txt
+CMakeFiles/
+CMakeScripts/
+cmake_install.cmake
+CTestTestfile.cmake
+install_manifest.txt
+compile_commands.json
+CMakeLists.txt.user
+Testing/
+
+# Compilation database (common typo fixed)
+compile_commands.json
+
+# OS or editor-specific files (optional, but recommended)
+*.swp
+*.swo
+*.bak
+*.tmp
+*.log
+.DS_Store
+Thumbs.db
+
+# Optional: Ignore all top-level build/ variants
+[Bb]uild*/
\ No newline at end of file
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 00000000..ff7eeba3
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,375 @@
+cmake_minimum_required(VERSION 3.10)
+
+project(cudd
+  VERSION 3.0.0
+  DESCRIPTION "CUDD: University of Colorado at Boulder Decision Diagrams"
+  HOMEPAGE_URL "https://github.com/bounverif/cudd"
+  LANGUAGES C CXX
+)
+
+if(PROJECT_SOURCE_DIR STREQUAL PROJECT_BINARY_DIR)
+  message(FATAL_ERROR "In-source builds not allowed.")
+endif()
+
+if(NOT CMAKE_BUILD_TYPE)
+  set(CMAKE_BUILD_TYPE Release)
+endif()
+
+set(CMAKE_C_STANDARD 11)
+set(CMAKE_C_STANDARD_REQUIRED ON)
+set(CMAKE_C_EXTENSIONS OFF)
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+set(CMAKE_CXX_EXTENSIONS OFF)
+set(CMAKE_POSITION_INDEPENDENT_CODE ON)
+set(CMAKE_CXX_VISIBILITY_PRESET hidden)
+set(CMAKE_VISIBILITY_INLINES_HIDDEN ON)
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
+# ============================================================================ #
+# Settings
+# ============================================================================ #
+
+option(CUDD_BUILD_CPP_API "Build C++ API" ON)
+option(CUDD_BUILD_SHARED_LIBS "Build CUDD as a shared library" OFF)
+option(CUDD_BUILD_WITH_STATS "Build CUDD with statistics" OFF)
+option(CUDD_BUILD_DDDMP "Build DDDMP Library" OFF)
+option(CUDD_BUILD_TESTS "Build CUDD tests" OFF)
+option(CUDD_BUILD_WITH_SYSTEM_QSORT "Build with system qsort" OFF)
+
+# option(BUILD_API_DOCS "Build API documentation with Doxygen" OFF)
+# option(BUILD_USER_GUIDES "Build user guides with LaTeX" OFF)
+# option(BUILD_NANOTRAV_EXAMPLE "Build Nanotrav Example" OFF)
+
+if(CUDD_BUILD_CPP_API)
+  include(CheckCXXCompilerFlag)
+  CHECK_CXX_COMPILER_FLAG("-std=c++11" COMPILER_SUPPORTS_CXX11)
+  if(NOT COMPILER_SUPPORTS_CXX11)
+    message(FATAL_ERROR "${CMAKE_CXX_COMPILER} has no C++11 support.")
+  endif()
+  include(CheckCXXSourceCompiles)
+  set(HAVE_MODERN_CXX TRUE)
+  set(HAVE_WORKING_THREAD TRUE)
+endif()
+
+# ============================================================================ #
+# Compiler Settings
+# ============================================================================ #
+
+include(CheckCXXCompilerFlag)
+
+if(CUDD_BUILD_WITH_SYSTEM_QSORT)
+  set(USE_SYSTEM_QSORT TRUE)
+endif()
+
+# set(__USE_MINGW_ANSI_STDIO ON) # TODO: Test.
+
+find_package(Threads)
+if(CMAKE_USE_PTHREADS_INIT)
+  add_definitions(-DHAVE_PTHREADS=1)
+  set(HAVE_PTHREADS TRUE)
+  add_definitions("-pthread")
+  # target_link_libraries(${name} ${CMAKE_THREAD_LIBS_INIT})
+endif()
+
+include(CheckIncludeFile)
+
+CHECK_INCLUDE_FILE("float.h" HAVE_FLOAT_H)
+if(NOT (HAVE_FLOAT_H))
+  message(FATAL_ERROR "'float.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("inttypes.h" HAVE_INTTYPES_H)
+if(NOT (HAVE_INTTYPES_H))
+  message(FATAL_ERROR "'inttypes.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("limits.h" HAVE_LIMITS_H)
+if(NOT (HAVE_LIMITS_H))
+  message(FATAL_ERROR "'limits.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("stddef.h" HAVE_STDDEF_H)
+if(NOT (HAVE_STDDEF_H))
+  message(FATAL_ERROR "'stddef.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("stdlib.h" HAVE_STDLIB_H)
+if(NOT (HAVE_STDLIB_H))
+  message(FATAL_ERROR "'stdlib.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("string.h" HAVE_STRING_H)
+if(NOT (HAVE_STRING_H))
+  message(FATAL_ERROR "'string.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("assert.h" HAVE_ASSERT_H)
+if(NOT (HAVE_ASSERT_H))
+  message(FATAL_ERROR "'assert.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("math.h" HAVE_MATH_H)
+if(NOT (HAVE_MATH_H))
+  message(FATAL_ERROR "'math.h' missing.")
+endif()
+
+CHECK_INCLUDE_FILE("unistd.h" HAVE_UNISTD_H)
+CHECK_INCLUDE_FILE("sys/time.h" HAVE_SYS_TIME_H)
+CHECK_INCLUDE_FILE("sys/times.h" HAVE_SYS_TIMES_H)
+CHECK_INCLUDE_FILE("sys/resource.h" HAVE_SYS_RESOURCE_H)
+CHECK_INCLUDE_FILE("sys/wait.h" HAVE_SYS_WAIT_H)
+CHECK_INCLUDE_FILE("sys/stat.h" HAVE_SYS_STAT_H)
+CHECK_INCLUDE_FILE("dlfcn.h" HAVE_DLFCN_H) # libtool
+CHECK_INCLUDE_FILE("memory.h" HAVE_MEMORY_H)
+CHECK_INCLUDE_FILE("strings.h" HAVE_STRINGS_H)
+
+set(STDC_HEADERS TRUE) # TODO: Test
+
+CHECK_INCLUDE_FILE("stdbool.h" HAVE__BOOL)
+
+include(CheckTypeSize)
+CHECK_TYPE_SIZE(size_t SIZE_T)
+CHECK_TYPE_SIZE(uint16_t UINT16_T)
+CHECK_TYPE_SIZE(uint32_t UINT32_T)
+CHECK_TYPE_SIZE(ptrdiff_t PTRDIFF_T)
+CHECK_TYPE_SIZE(int SIZEOF_INT)
+CHECK_TYPE_SIZE(long SIZEOF_LONG)
+CHECK_TYPE_SIZE("void*" SIZEOF_VOID_P)
+CHECK_TYPE_SIZE("long double" SIZEOF_LONG_DOUBLE)
+
+include(CheckFunctionExists)
+
+set(CMAKE_REQUIRED_INCLUDES "math.h")
+set(CMAKE_REQUIRED_LIBRARIES m)
+
+CHECK_FUNCTION_EXISTS(pow HAVE_POW)
+if(NOT (HAVE_POW))
+  message(FATAL_ERROR "'pow' function missing.")
+endif()
+
+CHECK_FUNCTION_EXISTS(sqrt HAVE_SQRT)
+if(NOT (HAVE_SQRT))
+  message(FATAL_ERROR "'sqrt' function missing.")
+endif()
+
+CHECK_FUNCTION_EXISTS(strchr HAVE_STRCHR)
+if(NOT (HAVE_STRCHR))
+  message(FATAL_ERROR "'strchr' function missing.")
+endif()
+
+CHECK_FUNCTION_EXISTS(strstr HAVE_STRSTR)
+if(NOT (HAVE_STRSTR))
+  message(FATAL_ERROR "'strstr' function missing.")
+endif()
+
+CHECK_FUNCTION_EXISTS(powl HAVE_POWL)
+CHECK_FUNCTION_EXISTS(gethostname HAVE_GETHOSTNAME)
+CHECK_FUNCTION_EXISTS(getrlimit HAVE_GETRLIMIT)
+CHECK_FUNCTION_EXISTS(getrusage HAVE_GETRUSAGE)
+CHECK_FUNCTION_EXISTS(sysconf HAVE_SYSCONF)
+
+include(CheckCSourceCompiles)
+CHECK_C_SOURCE_COMPILES(
+  "#include <math.h>
+  int main() { double x = INFINITY; }
+  " HAVE_IEEE_754)
+
+
+### ============================================================================ #
+# CUDD Library
+### ============================================================================ #
+
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/config.h.in
+               ${CMAKE_CURRENT_BINARY_DIR}/config.h)
+
+# Public header directories
+set(CUDD_PUBLIC_HEADERS
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cudd.h"
+)
+set(CUDD_SOURCES
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddAbs.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddBddCorr.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddGenetic.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddReorder.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddGroup.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddApply.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddBddIte.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddGroup.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSat.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddIsop.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddFind.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddBridge.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddHarwell.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSign.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddLin.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddInv.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddCache.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddInit.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSolve.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddMisc.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddIte.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddCheck.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddInteract.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSplit.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddPort.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddNeg.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddClip.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddLCache.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSubsetHB.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddReord.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAddWalsh.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddCof.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddLevelQ.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSubsetSP.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddSetop.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAndAbs.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddCompose.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddLinear.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddSymmetry.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddSymm.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAnneal.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddDecomp.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddLiteral.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddTable.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddUtil.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddApa.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddEssent.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddMatMult.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddUtil.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddAPI.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddExact.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddPriority.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddWindow.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddApprox.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddExport.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddRead.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddCount.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddBddAbs.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddGenCof.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddRef.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/cudd/cuddZddFuncs.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/epd/epd.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/mtr/mtrBasic.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/mtr/mtrGroup.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/st/st.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/cpu_stats.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/cpu_time.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/cstringstream.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/datalimit.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/pathsearch.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/pipefork.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/prtime.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/safe_mem.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/strsav.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/texpand.c"
+  "${CMAKE_CURRENT_SOURCE_DIR}/util/ucbqsort.c"
+)
+
+if(CUDD_BUILD_CPP_API)
+  add_subdirectory(cplusplus)
+endif()
+
+###
+### CUDD Target
+###
+
+# Define the cudd library target
+if(CUDD_BUILD_SHARED_LIBS)
+  add_library(cudd SHARED ${CUDD_SOURCES})
+else()
+  add_library(cudd STATIC ${CUDD_SOURCES})
+endif()
+
+# Link the math library (libm)
+find_library(MATH_LIBRARY m REQUIRED)
+target_link_libraries(cudd PUBLIC ${MATH_LIBRARY})
+
+# Include directories (build and install time)
+target_include_directories(cudd PUBLIC
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/cudd>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/cplusplus>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/epd>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/mtr>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/st>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/util>
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>
+  $<INSTALL_INTERFACE:include/cudd>
+)
+
+# Define properties for the library
+set_target_properties(cudd PROPERTIES
+  VERSION ${PROJECT_VERSION}
+  SOVERSION ${PROJECT_VERSION_MAJOR}
+  POSITION_INDEPENDENT_CODE ON
+  CXX_VISIBILITY_PRESET hidden
+  VISIBILITY_INLINES_HIDDEN ON
+  PUBLIC_HEADER "${CUDD_PUBLIC_HEADERS}"
+)
+
+# Optional compilation flags
+if(CUDD_BUILD_WITH_STATS)
+  target_compile_definitions(cudd PUBLIC DD_STATS)
+endif()
+
+###
+### Export and Install
+###
+
+include(GNUInstallDirs)
+include(GenerateExportHeader)
+include(CMakePackageConfigHelpers)
+
+generate_export_header(cudd
+  EXPORT_MACRO_NAME CUDD_API
+)
+
+# Install the cudd library
+install(TARGETS cudd
+  EXPORT cuddTargets
+  RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR} COMPONENT Runtime
+  LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} COMPONENT Runtime 
+  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} COMPONENT Development
+  INCLUDES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}
+  PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cudd COMPONENT Development
+)
+
+# Install version/config files for find_package
+write_basic_package_version_file(
+  "${CMAKE_CURRENT_BINARY_DIR}/cuddConfigVersion.cmake"
+  VERSION ${PROJECT_VERSION}
+  COMPATIBILITY SameMajorVersion
+)
+
+configure_package_config_file(
+  "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cuddConfig.cmake.in"
+  "${CMAKE_CURRENT_BINARY_DIR}/cuddConfig.cmake"
+  INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cudd
+)
+
+install(FILES
+  "${CMAKE_CURRENT_BINARY_DIR}/cuddConfig.cmake"
+  "${CMAKE_CURRENT_BINARY_DIR}/cuddConfigVersion.cmake"
+  DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cudd
+)
+
+# DDDMP Target
+if(CUDD_BUILD_DDDMP)
+  add_subdirectory(dddmp)
+endif()
+
+# Test Build
+include(CTest)
+if(CUDD_BUILD_TESTS)
+  add_subdirectory(nanotrav)
+endif()
+
+# Compile Commands
+if (PROJECT_IS_TOP_LEVEL AND UNIX)
+    # Create symlink to compile_commands.json for IDE to pick it up
+    execute_process(
+        COMMAND ${CMAKE_COMMAND} -E create_symlink
+            ${CMAKE_BINARY_DIR}/compile_commands.json
+            ${CMAKE_CURRENT_SOURCE_DIR}/compile_commands.json
+    )
+endif()
\ No newline at end of file
diff --git a/cmake/config.h.in b/cmake/config.h.in
new file mode 100644
index 00000000..42e6f337
--- /dev/null
+++ b/cmake/config.h.in
@@ -0,0 +1,186 @@
+/* Configurations to be filled by CMake. */
+
+/* Define if building universal (internal helper macro) */
+#cmakedefine AC_APPLE_UNIVERSAL_BUILD
+
+/* Define to 1 if you have the <assert.h> header file. */
+#cmakedefine01 HAVE_ASSERT_H
+
+/* Define to 1 if you have the <dlfcn.h> header file. */
+#cmakedefine01 HAVE_DLFCN_H
+
+/* Define to 1 if you have the <float.h> header file. */
+#cmakedefine01 HAVE_FLOAT_H
+
+/* Define to 1 if you have the `gethostname' function. */
+#cmakedefine01 HAVE_GETHOSTNAME
+
+/* Define to 1 if you have the `getrlimit' function. */
+#cmakedefine01 HAVE_GETRLIMIT
+
+/* Define to 1 if you have the `getrusage' function. */
+#cmakedefine01 HAVE_GETRUSAGE
+
+/* Define if you have working floating-point infinities */
+#cmakedefine HAVE_IEEE_754
+
+/* Define to 1 if you have the <inttypes.h> header file. */
+#cmakedefine01 HAVE_INTTYPES_H
+
+/* Define to 1 if you have the <limits.h> header file. */
+#cmakedefine01 HAVE_LIMITS_H
+
+/* Define to 1 if you have the <math.h> header file. */
+#cmakedefine01 HAVE_MATH_H
+
+/* Define to 1 if you have the <memory.h> header file. */
+#cmakedefine01 HAVE_MEMORY_H
+
+/* Define to 1 if your compiler supports enough C++11 */
+#cmakedefine01 HAVE_MODERN_CXX
+
+/* Define to 1 if you have the `pow' function. */
+#cmakedefine01 HAVE_POW
+
+/* Define to 1 if you have the `powl' function. */
+#cmakedefine01 HAVE_POWL
+
+/* Define to 1 if the system has the type `ptrdiff_t'. */
+#cmakedefine01 HAVE_PTRDIFF_T
+
+/* Define to 1 if you have the `sqrt' function. */
+#cmakedefine01 HAVE_SQRT
+
+/* Define to 1 if you have the <stddef.h> header file. */
+#cmakedefine01 HAVE_STDDEF_H
+
+/* Define to 1 if you have the <stdint.h> header file. */
+#cmakedefine01 HAVE_STDINT_H
+
+/* Define to 1 if you have the <stdlib.h> header file. */
+#cmakedefine01 HAVE_STDLIB_H
+
+/* Define to 1 if you have the `strchr' function. */
+#cmakedefine01 HAVE_STRCHR
+
+/* Define to 1 if you have the <strings.h> header file. */
+#cmakedefine01 HAVE_STRINGS_H
+
+/* Define to 1 if you have the <string.h> header file. */
+#cmakedefine01 HAVE_STRING_H
+
+/* Define to 1 if you have the `strstr' function. */
+#cmakedefine01 HAVE_STRSTR
+
+/* Define to 1 if you have the `sysconf' function. */
+#cmakedefine01 HAVE_SYSCONF
+
+/* Define to 1 if you have the <sys/resource.h> header file. */
+#cmakedefine01 HAVE_SYS_RESOURCE_H
+
+/* Define to 1 if you have the <sys/stat.h> header file. */
+#cmakedefine01 HAVE_SYS_STAT_H
+
+/* Define to 1 if you have the <sys/times.h> header file. */
+#cmakedefine01 HAVE_SYS_TIMES_H
+
+/* Define to 1 if you have the <sys/time.h> header file. */
+#cmakedefine01 HAVE_SYS_TIME_H
+
+/* Define to 1 if you have the <sys/types.h> header file. */
+#cmakedefine01 HAVE_SYS_TYPES_H
+
+/* Define to 1 if you have the <sys/wait.h> header file. */
+#cmakedefine01 HAVE_SYS_WAIT_H
+
+/* Define to 1 if you have the <unistd.h> header file. */
+#cmakedefine01 HAVE_UNISTD_H
+
+/* Define to 1 if C++ thread header is usable */
+#cmakedefine01 HAVE_WORKING_THREAD
+
+/* Define to 1 if the system has the type `_Bool'. */
+#cmakedefine01 HAVE__BOOL
+
+/* Define to the sub-directory in which libtool stores uninstalled libraries.
+   */
+#cmakedefine LT_OBJDIR "@LT_OBJDIR@"
+
+/* Name of package */
+#define PACKAGE "@CMAKE_PROJECT_NAME@"
+
+/* Define to the address where bug reports for this package should be sent. */
+#define PACKAGE_BUGREPORT "Fabio@Colorado.EDU"
+
+/* Define to the full name of this package. */
+#define PACKAGE_NAME "@CMAKE_PROJECT_NAME@"
+
+/* Define to the full name and version of this package. */
+#define PACKAGE_STRING "@CMAKE_PROJECT_NAME@ @VERSION@"
+
+/* Define to the one symbol short name of this package. */
+#define PACKAGE_TARNAME "@CMAKE_PROJECT_NAME@"
+
+/* Define to the home page for this package. */
+#define PACKAGE_URL "@PACKAGE_URL@"
+
+/* Define to the version of this package. */
+#define PACKAGE_VERSION "@PROJECT_VERSION@"
+
+/* The size of `int', as computed by sizeof. */
+#define SIZEOF_INT @SIZEOF_INT@
+
+/* The size of `long', as computed by sizeof. */
+#define SIZEOF_LONG @SIZEOF_LONG@
+
+/* The size of `long double', as computed by sizeof. */
+#define SIZEOF_LONG_DOUBLE @SIZEOF_LONG_DOUBLE@
+
+/* The size of `void *', as computed by sizeof. */
+#define SIZEOF_VOID_P @SIZEOF_VOID_P@
+
+/* Define to 1 if you have the ANSI C header files. */
+#cmakedefine01 STDC_HEADERS
+
+/* Define to use system qsort */
+#cmakedefine USE_SYSTEM_QSORT
+
+/* Version number of package */
+#define VERSION "@VERSION@"
+
+/* Define WORDS_BIGENDIAN to 1 if your processor stores words with the most
+   significant byte first (like Motorola and SPARC, unlike Intel). */
+#if defined AC_APPLE_UNIVERSAL_BUILD
+# if defined __BIG_ENDIAN__
+#  define WORDS_BIGENDIAN 1
+# endif
+#else
+# ifndef WORDS_BIGENDIAN
+#cmakedefine WORDS_BIGENDIAN
+# endif
+#endif
+
+/* Define for Solaris 2.5.1 so the uint32_t typedef from <sys/synch.h>,
+   <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
+   #define below would cause a syntax error. */
+#cmakedefine _UINT32_T
+
+/* Define to 1 to enable C99-compliant printf on MinGW-w64 */
+#cmakedefine __USE_MINGW_ANSI_STDIO
+
+/* Define to `__inline__' or `__inline' if that's what the C compiler
+   calls it, or to nothing if 'inline' is not supported under any name.  */
+#ifndef __cplusplus
+#cmakedefine inline
+#endif
+
+/* Define to `unsigned int' if <sys/types.h> does not define. */
+#cmakedefine size_t
+
+/* Define to the type of an unsigned integer type of width exactly 16 bits if
+   such a type exists and the standard includes do not define it. */
+#cmakedefine uint16_t
+
+/* Define to the type of an unsigned integer type of width exactly 32 bits if
+   such a type exists and the standard includes do not define it. */
+#cmakedefine uint32_t
diff --git a/cmake/cuddConfig.cmake.in b/cmake/cuddConfig.cmake.in
new file mode 100644
index 00000000..5f5449c8
--- /dev/null
+++ b/cmake/cuddConfig.cmake.in
@@ -0,0 +1,15 @@
+@PACKAGE_INIT@
+
+if(@COMPONET_TARGETS_ENABLED@)
+  set(_supported_components Runtime Development)
+
+  foreach(_comp ${MathFunctions_FIND_COMPONENTS})
+    if(NOT _comp IN_LIST _supported_components)
+      set(CUDD_FOUND False)
+      set(CUDD_NOT_FOUND_MESSAGE "Unsupported component: ${_comp}")
+    endif()
+    include("${CMAKE_CURRENT_LIST_DIR}/cudd${_comp}Targets.cmake")
+  endforeach()
+else()
+  include("${CMAKE_CURRENT_LIST_DIR}/cuddTargets.cmake")
+endif()
\ No newline at end of file
diff --git a/cplusplus/CMakeLists.txt b/cplusplus/CMakeLists.txt
new file mode 100644
index 00000000..0a57c63e
--- /dev/null
+++ b/cplusplus/CMakeLists.txt
@@ -0,0 +1,9 @@
+set(CUDD_PUBLIC_HEADERS
+"${CUDD_PUBLIC_HEADERS}"
+"${CMAKE_CURRENT_SOURCE_DIR}/cuddObj.hh"
+)
+
+set(CUDD_SOURCES
+"${CUDD_SOURCES}"
+"${CMAKE_CURRENT_SOURCE_DIR}/cuddObj.cc"
+)
diff --git a/cplusplus/cuddObj.cc b/cplusplus/cuddObj.cc
index 35256123..81cd34ab 100644
--- a/cplusplus/cuddObj.cc
+++ b/cplusplus/cuddObj.cc
@@ -916,6 +916,28 @@ ADD::operator|=(
 
 } // ADD::operator|=
 
+ADD
+ADD::operator^(
+  const ADD& other) const
+{
+  DdManager *mgr = checkSameManager(other);
+  DdNode *result = Cudd_addApply(mgr,Cudd_addXor,node,other.node);
+  checkReturnValue(result);
+  return ADD(p, result);
+} // ADD::operator^
+
+ADD
+ADD::operator^=(
+  const ADD& other)
+{
+  DdManager *mgr = checkSameManager(other);
+  DdNode *result = Cudd_addApply(mgr,Cudd_addXor,node,other.node);
+  checkReturnValue(result);
+  Cudd_Ref(result);
+  Cudd_RecursiveDeref(mgr,node);
+  node = result;
+  return *this;
+} // ADD::operator^=
 
 bool
 ADD::IsZero() const
@@ -1181,6 +1203,15 @@ ZDD::operator-=(
 } // ZDD::operator-=
 
 
+ZDD
+ZDD::operator~() const
+{
+  DdNode *result = Cudd_zddDiff(p->manager, p->manager->univ[0], node);
+  checkReturnValue(result);
+  return ZDD(p, result);
+} // ZDD::operator~
+
+
 // ---------------------------------------------------------------------------
 // Members of class Cudd
 // ---------------------------------------------------------------------------
@@ -1468,6 +1499,27 @@ Cudd::bddZero() const
 } // Cudd::bddZero
 
 
+BDD
+Cudd::makeBddNode(
+  int index,
+  BDD T,
+  BDD E) const
+{
+  // Reduction Rule 1
+  if (T == E) { return T; }
+
+  // Use of Complemented Edge
+  const bool comple = Cudd_IsComplement(T.node);
+  DdNode *r1 = cuddUniqueInter(p->manager, index,
+                               comple ? Cudd_Not(T.node) : T.node,
+                               comple ? Cudd_Not(E.node) : E.node);
+
+  DdNode *r2 = comple ? Cudd_Complement(r1) : r1;
+  checkReturnValue(r2);
+  return BDD(p, r2);
+} // Cudd::makeBddNode
+
+
 ADD
 Cudd::addVar() const
 {
@@ -1509,6 +1561,20 @@ Cudd::addZero() const
 } // Cudd::addZero
 
 
+ADD
+Cudd::makeAddNode(
+  int index,
+  ADD T,
+  ADD E) const
+{
+  // Reduction Rule 1
+  if (T == E) { return T; }
+  DdNode *r = cuddUniqueInter(p->manager, index, T.node, E.node);
+  checkReturnValue(r);
+  return ADD(p, r);
+} // Cudd::makeAddNode
+
+
 ADD
 Cudd::constant(
   CUDD_VALUE_TYPE c) const
@@ -1572,6 +1638,19 @@ Cudd::zddZero() const
 } // Cudd::zddZero
 
 
+ZDD
+Cudd::makeZddNode(
+  int index,
+  ZDD T,
+  ZDD E) const
+{
+  if (T == zddZero()) { return E;}
+  DdNode *result = cuddUniqueInterZdd(p->manager, index, T.node, E.node);
+  checkReturnValue(result);
+  return ZDD(p, result);
+} // Cudd::makeZddNode
+
+
 void
 defaultError(
   string message)
@@ -5655,6 +5734,26 @@ BDD::PickOneMinterm(
 } // BDD::PickOneMinterm
 
 
+void
+ADD::PickOneCube(
+  char * string) const
+{
+  DdManager *mgr = p->manager;
+  int result = Cudd_addPickOneCube(mgr, node, string);
+  checkReturnValue(result);
+} // ADD::PickOneCube
+
+
+ADD
+ADD::PickOneMintermSet(
+  const ADD& choice) const
+{
+  DdNode *result = Cudd_addPickOneMintermSet(p->manager, node, choice.node);
+  checkReturnValue(result);
+  return ADD(p, result);
+} // ADD::PickOneMintermSet
+
+
 BDD
 Cudd::bddComputeCube(
   BDD * vars,
@@ -5882,6 +5981,15 @@ ZDD::DivideF(
 } // ZDD::DivideF
 
 
+ZDD
+ZDD::Complement() const
+{
+  DdNode *result = Cudd_zddComplement(p->manager, node);
+  checkReturnValue(result);
+  return ZDD(p, result);
+} // ZDD::Complement
+
+
 MtrNode *
 Cudd::MakeZddTreeNode(
   unsigned int low,
diff --git a/cplusplus/cuddObj.hh b/cplusplus/cuddObj.hh
index c9b02e89..c07e798a 100644
--- a/cplusplus/cuddObj.hh
+++ b/cplusplus/cuddObj.hh
@@ -323,6 +323,8 @@ public:
     ADD operator&=(const ADD& other);
     ADD operator|(const ADD& other) const;
     ADD operator|=(const ADD& other);
+    ADD operator^(const ADD& other) const;
+    ADD operator^=(const ADD& other);
     bool IsZero() const;
     ADD ExistAbstract(const ADD& cube) const;
     ADD UnivAbstract(const ADD& cube) const;
@@ -373,6 +375,8 @@ public:
     ADD Triangle(const ADD& g, std::vector<ADD> z) const;
     ADD Eval(int * inputs) const;
     bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const;
+    void PickOneCube(char * string) const;
+    ADD PickOneMintermSet(const ADD& choice) const;
 
 }; // ADD
 
@@ -408,6 +412,7 @@ public:
     ZDD operator|=(const ZDD& other);
     ZDD operator-(const ZDD& other) const;
     ZDD operator-=(const ZDD& other);
+    ZDD operator~() const;
     int Count() const;
     double CountDouble() const;
     ZDD Product(const ZDD& g) const;
@@ -416,6 +421,7 @@ public:
     ZDD Divide(const ZDD& g) const;
     ZDD WeakDivF(const ZDD& g) const;
     ZDD DivideF(const ZDD& g) const;
+    ZDD Complement() const;
     double CountMinterm(int path) const;
     BDD PortToBdd() const;
     ZDD Ite(const ZDD& g, const ZDD& h) const;
@@ -485,16 +491,19 @@ public:
     BDD bddVar(int index) const;
     BDD bddOne(void) const;
     BDD bddZero(void) const;
+    BDD makeBddNode(int index, BDD low, BDD high) const;
     ADD addVar(void) const;
     ADD addVar(int index) const;
     ADD addOne(void) const;
     ADD addZero(void) const;
+    ADD makeAddNode(int index, ADD T, ADD E) const;
     ADD constant(CUDD_VALUE_TYPE c) const;
     ADD plusInfinity(void) const;
     ADD minusInfinity(void) const;
     ZDD zddVar(int index) const;
     ZDD zddOne(int i) const;
     ZDD zddZero(void) const;
+    ZDD makeZddNode(int index, ZDD low, ZDD high) const;
     ADD addNewVarAtLevel(int level) const;
     BDD bddNewVarAtLevel(int level) const;
     void zddVarsFromBddVars(int multiplicity) const;
diff --git a/cudd/cudd.h b/cudd/cudd.h
index 7d6f10e5..4c9caf2a 100644
--- a/cudd/cudd.h
+++ b/cudd/cudd.h
@@ -58,6 +58,7 @@
 /*---------------------------------------------------------------------------*/
 
 #include <inttypes.h>
+#include <stdio.h>
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -695,6 +696,8 @@ extern DdNode * Cudd_addNegate(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addRoundOff(DdManager *dd, DdNode *f, int N);
 extern DdNode * Cudd_addWalsh(DdManager *dd, DdNode **x, DdNode **y, int n);
 extern DdNode * Cudd_addResidue(DdManager *dd, int n, int m, int options, int top);
+extern int Cudd_addPickOneCube(DdManager *ddm, DdNode *node, char *string);
+extern DdNode * Cudd_addPickOneMintermSet(DdManager *dd, DdNode *f, DdNode *choice);
 extern DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
 extern DdNode * Cudd_bddAndAbstractLimit(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit);
 extern int Cudd_ApaNumberOfDigits(int binaryDigits);
diff --git a/cudd/cuddUtil.c b/cudd/cuddUtil.c
index facaf488..a82de9e0 100644
--- a/cudd/cuddUtil.c
+++ b/cudd/cuddUtil.c
@@ -1301,7 +1301,7 @@ Cudd_CountLeaves(
 
   @sideeffect None
 
-  @see Cudd_bddPickOneMinterm
+  @see Cudd_addPickOneCube Cudd_bddPickOneMinterm
 
 */
 int
@@ -1354,6 +1354,63 @@ Cudd_bddPickOneCube(
 } /* end of Cudd_bddPickOneCube */
 
 
+/**
+  @brief Picks one on-set cube randomly from the given %DD.
+
+  @details The cube corresponds to a path to a non-zero terminal. The cube is
+  written into an array of characters.  The array must have at least as many
+  entries as there are variables.
+
+  @return 1 if successful; 0 otherwise.
+
+  @sideeffect None
+
+  @see Cudd_bddPickOneCube
+
+*/
+int
+Cudd_addPickOneCube(
+  DdManager * ddm,
+  DdNode * node,
+  char * string)
+{
+    DdNode *T, *E;
+    DdNode *zero;
+    char   dir;
+    int    i;
+
+    if (string == NULL || node == NULL) return(0);
+
+    /* The constant 0 function has no on-set cubes. */
+    zero = DD_ZERO(ddm);
+    if (node == zero) {
+        ddm->errorCode = CUDD_INVALID_ARG;
+        return(0);
+    }
+
+    for (i = 0; i < ddm->size; i++) string[i] = 2;
+
+    for (;;) {
+        if (Cudd_IsConstant(node)) break;
+
+        T = cuddT(node); E = cuddE(node);
+        if (T == zero) {
+          string[node->index] = 0;
+          node = E;
+        } else if (E == zero) {
+            string[node->index] = 1;
+            node = T;
+        } else {
+            dir = (char) ((Cudd_Random(ddm) & 0x2000) >> 13);
+            string[node->index] = dir;
+            node = dir ? T : E;
+        }
+    }
+    return(1);
+
+} /* end of Cudd_addPickOneCube */
+
+
 /**
   @brief Picks one on-set minterm randomly from the given %DD.
 
@@ -1454,6 +1511,94 @@ Cudd_bddPickOneMinterm(
 }  /* end of Cudd_bddPickOneMinterm */
 
 
+/**
+
+
+  @brief Picks one on-set minterm from the given %DD.
+
+
+
+
+
+  @details The minterm is represented as a decision diagram. Whenever there is
+
+
+  a choice for a variable (i.e., neither of the children is the 0-terminal), the
+
+
+  value taken from the cube <code>choice</code>, or it is false if
+
+
+  <code>choice</code> is independent of that variable. If <code>f</code> is the
+
+
+  constant function 0 (i.e., there is no cube), this function simply returns the
+
+
+  0-terminal.
+
+
+
+
+
+  @return a pointer to the %BDD for the minterm if successful; NULL if the
+
+
+  procedure ran out of memory.
+
+
+
+
+
+  @sideeffect None
+
+
+
+
+
+  @see Cudd_bddPickOneCube Cudd_bddPickOneMinterm
+
+
+
+
+
+*/
+
+
+DdNode *
+Cudd_addPickOneMintermSet(
+  DdManager * dd /**< manager */,
+  DdNode * f /**< function from which to pick one minterm */,
+  DdNode * choice /**< cube describing the choice */)
+{
+    if (f->index == CUDD_CONST_INDEX) return f;
+
+    DdNode *T = cuddT(f), *E = cuddE(f);
+    DdNode *zero = DD_ZERO(dd);
+
+    while (choice->index < f->index) {
+      choice = cuddT(choice) != zero ? cuddT(choice) : cuddE(choice);
+    }
+
+    int this_choice = 0;
+
+    if (T != zero) {
+        if (E == zero || (choice->index == f->index && cuddT(choice) == zero)) {
+            this_choice = 1;
+        }
+    }
+
+    DdNode *sub = Cudd_addPickOneMintermSet(dd, this_choice ? T : E, choice);
+
+    if (sub == NULL) return NULL;
+
+    DdNode *new_T = this_choice ? sub : zero;
+    DdNode *new_E = this_choice ? zero : sub;
+    return cuddUniqueInter(dd, f->index, new_T, new_E);
+
+}  /* end of Cudd_addPickOneMintermSet */
+
+
 /**
   @brief Picks k on-set minterms evenly distributed from given %DD.
 
diff --git a/dddmp/CMakeLists.txt b/dddmp/CMakeLists.txt
new file mode 100644
index 00000000..11dba713
--- /dev/null
+++ b/dddmp/CMakeLists.txt
@@ -0,0 +1,55 @@
+set(DDDMP_PUBLIC_HEADERS
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmp.h"
+)
+
+set(DDDMP_SOURCES
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpInt.h"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpBinary.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpNodeAdd.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpStoreCnf.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpConvert.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpNodeBdd.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpStoreMisc.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpDbg.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpNodeCnf.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpUtil.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpLoad.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpStoreAdd.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpLoadCnf.c"
+"${CMAKE_CURRENT_SOURCE_DIR}/dddmpStoreBdd.c"
+)
+
+if(CUDD_BUILD_SHARED_LIBS)
+  add_library(dddmp SHARED ${DDDMP_SOURCES})
+else()
+  add_library(dddmp STATIC ${DDDMP_SOURCES})
+endif()
+
+target_include_directories(dddmp PUBLIC
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/cudd>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/epd>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/mtr>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/st>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/util>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/dddmp>
+  $<BUILD_INTERFACE:${CMAKE_BINARY_DIR}>
+  $<INSTALL_INTERFACE:include/cudd>
+)
+
+set_target_properties(cudd PROPERTIES
+  VERSION ${PROJECT_VERSION}
+  SOVERSION ${PROJECT_VERSION_MAJOR}
+  POSITION_INDEPENDENT_CODE ON
+  CXX_VISIBILITY_PRESET hidden
+  VISIBILITY_INLINES_HIDDEN ON
+  PUBLIC_HEADER "${DDDMP_PUBLIC_HEADERS}"
+)
+
+install(TARGETS dddmp
+  EXPORT cuddTargets
+  RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR} COMPONENT Runtime
+  LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} COMPONENT Runtime 
+  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} COMPONENT Development
+  INCLUDES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}
+  PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cudd COMPONENT Development
+)
\ No newline at end of file
diff --git a/nanotrav/CMakeLists.txt b/nanotrav/CMakeLists.txt
new file mode 100644
index 00000000..09a6ef9e
--- /dev/null
+++ b/nanotrav/CMakeLists.txt
@@ -0,0 +1,85 @@
+set(NANOTRAV_SOURCES
+  bnet.c
+  chkMterm.c
+  ntr.c
+  ntrBddTest.c
+  ntrHeap.c
+  ntrMflow.c
+  ntrShort.c
+  ntrZddTest.c
+  main.c
+)
+
+add_executable(nanotrav ${NANOTRAV_SOURCES})
+
+target_link_libraries(nanotrav PRIVATE cudd dddmp)
+target_include_directories(nanotrav PUBLIC
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/nanotrav>
+  $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/nanotrav>
+  $<INSTALL_INTERFACE:include/cudd>
+)
+
+add_test(
+  NAME test_C17
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -cover ${CMAKE_CURRENT_SOURCE_DIR}/C17.blif
+)
+
+add_test(
+  NAME test_C880
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -ordering dfs -autodyn -automethod sifting -reordering sifting -drop ${CMAKE_CURRENT_SOURCE_DIR}/C880.blif
+)
+
+add_test(
+  NAME test_s27
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -ordering hw -reordering annealing -trav ${CMAKE_CURRENT_SOURCE_DIR}/s27.blif
+)
+
+add_test(
+  NAME test_s27b
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -ordering dfs -reordering win4 -verify ${CMAKE_CURRENT_SOURCE_DIR}/s27.blif ${CMAKE_CURRENT_SOURCE_DIR}/s27b.blif
+)
+
+add_test(
+  NAME test_s27c
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -trav -image depend -depend ${CMAKE_CURRENT_SOURCE_DIR}/s27c.blif
+)
+
+add_test(
+  NAME test_mult32a
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -autodyn -reordering sifting -trav ${CMAKE_CURRENT_SOURCE_DIR}/mult32a.blif
+)
+
+add_test(
+  NAME test_s382
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -trav -image part -autodyn -automethod sifting -drop -scc -shortpaths bellman ${CMAKE_CURRENT_SOURCE_DIR}/s382.blif
+)
+
+add_test(
+  NAME test_s641
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -trav -autodyn -automethod group -drop -clauses -density -decomp -zdd ${CMAKE_CURRENT_SOURCE_DIR}/s641.blif
+)
+
+add_test(
+  NAME test_closest
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -reordering genetic -drop -closest ${CMAKE_CURRENT_SOURCE_DIR}/closest.blif
+)
+
+add_test(
+  NAME test_adj49
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -ordering dfs -reordering cogroup -drop -char2vect -cofest ${CMAKE_CURRENT_SOURCE_DIR}/adj49.blif
+)
+
+add_test(
+  NAME test_ham01
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -reordering linear ${CMAKE_CURRENT_SOURCE_DIR}/ham01.blif
+)
+
+add_test(
+  NAME test_miniFirst
+  COMMAND $<TARGET_FILE:nanotrav> -p 1 -second ${CMAKE_CURRENT_SOURCE_DIR}/miniSecond.blif ${CMAKE_CURRENT_SOURCE_DIR}/miniFirst.blif
+)
+
+add_test(
+  NAME test_rcn25
+  COMMAND $<TARGET_FILE:nanotrav>  -p 1 -envelope ${CMAKE_CURRENT_SOURCE_DIR}/rcn25.blif
+)