From 929c68e403353ff4e2be6c80ee0f7cc53a040b50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 12:06:04 +0200
Subject: [PATCH 01/15] Upgraded libraries and compilers

---
 cmake/clang-tidy.cmake                        |  2 +-
 cmake/toolchain/i686-linux-gcc14.cmake        | 19 +++++++++++++++++++
 .../toolchain/x86_64-darwin-brew-gcc14.cmake  | 19 +++++++++++++++++++
 cmake/toolchain/x86_64-linux-gcc14.cmake      | 19 +++++++++++++++++++
 compile.sh                                    |  9 +++++++++
 getlibs.sh                                    | 10 ++++++++--
 6 files changed, 75 insertions(+), 3 deletions(-)
 create mode 100644 cmake/toolchain/i686-linux-gcc14.cmake
 create mode 100644 cmake/toolchain/x86_64-darwin-brew-gcc14.cmake
 create mode 100644 cmake/toolchain/x86_64-linux-gcc14.cmake

diff --git a/cmake/clang-tidy.cmake b/cmake/clang-tidy.cmake
index b93e6f8..83792e8 100644
--- a/cmake/clang-tidy.cmake
+++ b/cmake/clang-tidy.cmake
@@ -1,4 +1,4 @@
-find_program(CLANG_TIDY_PROGRAM clang-tidy-14 clang-tidy)
+find_program(CLANG_TIDY_PROGRAM NAMES clang-tidy-14 clang-tidy)
 if(CLANG_TIDY_PROGRAM)
     execute_process(COMMAND ${CLANG_TIDY_PROGRAM} --version OUTPUT_VARIABLE CLANG_TIDY_VERSION_STRING)
     string(REGEX MATCH "LLVM version ([0-9A-Za-z]+)\\.([0-9A-Za-z\\.]+)" TIDY_VERSION "${CLANG_TIDY_VERSION_STRING}")
diff --git a/cmake/toolchain/i686-linux-gcc14.cmake b/cmake/toolchain/i686-linux-gcc14.cmake
new file mode 100644
index 0000000..e8e5bca
--- /dev/null
+++ b/cmake/toolchain/i686-linux-gcc14.cmake
@@ -0,0 +1,19 @@
+# the name of the target operating system
+set(CMAKE_SYSTEM_NAME Linux)
+
+# which compilers to use for C and C++
+set(CMAKE_C_COMPILER gcc-14)
+set(CMAKE_C_FLAGS -m32)
+set(CMAKE_CXX_COMPILER g++-14)
+set(CMAKE_CXX_FLAGS -m32)
+set(CMAKE_ASM_FLAGS -m32)
+
+# here is the target environment located
+set(CMAKE_FIND_ROOT_PATH "${CMAKE_PREFIX_PATH}")
+
+# adjust the default behaviour of the FIND_XXX() commands:
+# search headers and libraries in the target environment,
+# search programs in both target and host environments
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
diff --git a/cmake/toolchain/x86_64-darwin-brew-gcc14.cmake b/cmake/toolchain/x86_64-darwin-brew-gcc14.cmake
new file mode 100644
index 0000000..d0f50fd
--- /dev/null
+++ b/cmake/toolchain/x86_64-darwin-brew-gcc14.cmake
@@ -0,0 +1,19 @@
+# the name of the target operating system
+set(CMAKE_SYSTEM_NAME Darwin)
+
+# which compilers to use for C and C++
+set(CMAKE_C_COMPILER gcc-14)
+set(CMAKE_C_FLAGS -m64)
+set(CMAKE_CXX_COMPILER g++-14)
+set(CMAKE_CXX_FLAGS -m64)
+set(CMAKE_ASM_FLAGS -m64)
+
+# here is the target environment located
+set(CMAKE_FIND_ROOT_PATH "${CMAKE_PREFIX_PATH}")
+
+# adjust the default behaviour of the FIND_XXX() commands:
+# search headers and libraries in the target environment,
+# search programs in both target and host environments
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
diff --git a/cmake/toolchain/x86_64-linux-gcc14.cmake b/cmake/toolchain/x86_64-linux-gcc14.cmake
new file mode 100644
index 0000000..10bf9fe
--- /dev/null
+++ b/cmake/toolchain/x86_64-linux-gcc14.cmake
@@ -0,0 +1,19 @@
+# the name of the target operating system
+set(CMAKE_SYSTEM_NAME Linux)
+
+# which compilers to use for C and C++
+set(CMAKE_C_COMPILER gcc-14)
+set(CMAKE_C_FLAGS -m64)
+set(CMAKE_CXX_COMPILER g++-14)
+set(CMAKE_CXX_FLAGS -m64)
+set(CMAKE_ASM_FLAGS -m64)
+
+# here is the target environment located
+set(CMAKE_FIND_ROOT_PATH "${CMAKE_PREFIX_PATH}")
+
+# adjust the default behaviour of the FIND_XXX() commands:
+# search headers and libraries in the target environment,
+# search programs in both target and host environments
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
diff --git a/compile.sh b/compile.sh
index 8c8f4cc..48e8d35 100755
--- a/compile.sh
+++ b/compile.sh
@@ -13,9 +13,15 @@ for target in $targets ; do
     unset BUILD_EXTRA
     unset CMAKE_BUILD_TYPE
     case $target in
+        x86_64-linux-gcc14*)
+            PLATFORM=x86_64-linux-gcc14
+            ;;
         linux64*|x86_64-linux*)
             PLATFORM=x86_64-linux
             ;;
+        i686-linux-gcc14*)
+            PLATFORM=i686-linux-gcc14
+            ;;
         linux32*|i686-linux*)
             PLATFORM=i686-linux
             ;;
@@ -25,6 +31,9 @@ for target in $targets ; do
         win32*|i686-w64-mingw32*)
             PLATFORM=i686-w64-mingw32
             ;;
+        x86_64-darwin-brew-gcc14*)
+            PLATFORM=x86_64-darwin-brew-gcc14
+            ;;
         macos*|x86_64-darwin*)
             PLATFORM=x86_64-darwin
             ;;
diff --git a/getlibs.sh b/getlibs.sh
index 7c8b4f1..feab846 100755
--- a/getlibs.sh
+++ b/getlibs.sh
@@ -9,6 +9,12 @@ if [ $# -eq 0 ]; then
   kernel=$(uname --kernel-name)
   targets=${machine,,}-${kernel,,}
   echo "Expects targets as arguments, for example: $targets"
+  echo "The following are supported:"
+  for file in "$PROJECT_DIR/cmake/toolchain"/*.cmake ; do
+      cmake=$(basename "$file")
+      toolchain=${cmake%.cmake}
+      echo -e "\t${toolchain}"
+  done
   exit 1
 else
   targets="$@"
@@ -61,13 +67,13 @@ for target in $targets ; do
 
     # UUtils various low level Uppaal utilities
     NAME=UUtils
-    VERSION=2.0.5
+    VERSION=2.0.7
     LIBRARY="${NAME}-${VERSION}"
     if [ -r "$PREFIX/include/base/Enumerator.h" ]; then
       echo "$LIBRARY is already installed in $PREFIX"
     else
       ARCHIVE="${LIBRARY}.tar.gz"
-      SHA256=e213f936af73344de071a7794233a328028045c08df58ac9c637a0e6a2ad7b3f
+      SHA256=52a823768398707eee42392182c320141662e74e6bd8eaac1a0eca22d8a27bcd
       SOURCE="${SOURCES}/${LIBRARY}"
       BUILD="${PREFIX}/build-${LIBRARY}"
       pushd "$SOURCES"

From 72a094c4f890f0ac0d48e8fce5b6c0ff72b6af4c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 13:33:58 +0200
Subject: [PATCH 02/15] Upgraded C++ standard to C++23 and refactored reference
 counting using std::shared_ptr

---
 CMakeLists.txt       |   4 +-
 include/dbm/pfed.h   | 107 ++++++--------------------
 include/dbm/priced.h | 152 +++++++++++++++----------------------
 src/pfed.cpp         |  66 +++-------------
 src/priced.cpp       | 175 +++++++++++++++++++------------------------
 5 files changed, 174 insertions(+), 330 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index f4815d9..2c13597 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,5 +1,5 @@
 cmake_minimum_required(VERSION 3.16)
-project(UDBM VERSION 2.0.14 LANGUAGES CXX C)
+project(UDBM VERSION 2.0.15 LANGUAGES CXX C)
 include(CMakePackageConfigHelpers)
 include(GNUInstallDirs)
 
@@ -8,7 +8,7 @@ option(UDBM_STATIC "Static linking" OFF)
 option(FIND_FATAL "Stop upon find_package errors" OFF)
 
 cmake_policy(SET CMP0048 NEW) # project() command manages VERSION variables
-set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD 23)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS OFF)
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
diff --git a/include/dbm/pfed.h b/include/dbm/pfed.h
index a2880f1..5ac1e33 100644
--- a/include/dbm/pfed.h
+++ b/include/dbm/pfed.h
@@ -39,8 +39,8 @@ namespace dbm
     class pdbm_t
     {
     protected:
-        PDBM pdbm;
-        cindex_t dim;
+        PDBMPtr pdbm{nullptr};
+        cindex_t dim{0};
 
     public:
         /**
@@ -48,7 +48,7 @@ namespace dbm
          * dimension zero.  This must not be assigned to another
          * pdbm_t.
          */
-        pdbm_t();
+        pdbm_t() = default;
 
         /**
          * Allocates a new empty priced DBM of the given
@@ -56,41 +56,24 @@ namespace dbm
          *
          * @see pdbm_allocate()
          */
-        explicit pdbm_t(cindex_t);
+        explicit pdbm_t(cindex_t dim): dim{dim} {}
 
         /**
          * Makes a reference to the given priced DBM.
          */
-        pdbm_t(PDBM pdbm, cindex_t dim);
-
-        /**
-         * Copy constructor. This will increment the reference count
-         * to the priced DBM given.
-         */
-        pdbm_t(const pdbm_t&);
-
-        /**
-         * Destructor. Reduces the reference count to the priced
-         * DBM. This in turn may result in its deallocation.
-         */
-        ~pdbm_t();
-
-        /**
-         * Assignment operator.
-         */
-        pdbm_t& operator=(const pdbm_t&);
+        pdbm_t(PDBMPtr pdbm, cindex_t dim): pdbm{std::move(pdbm)}, dim{dim} {}
 
         /**
          * Type conversion to PDBM. Notice that a reference to the
          * PDBM is provided, thus the pdbm_t object can even be used
          * with pdbm_X() functions modifying the priced DBM.
          */
-        operator PDBM&() { return pdbm; }
+        operator PDBMPtr&() { return pdbm; }
 
         /**
          * Type conversion to constant PDBM.
          */
-        operator PDBM() const { return pdbm; }
+        operator PDBMCPtr() const { return pdbm; }
 
         /**
          * Returns a hash value for the priced DBM.
@@ -134,29 +117,9 @@ namespace dbm
         static pdbm_t readFromMinDBM(cindex_t dimension, const int32_t*);
     };
 
-    inline pdbm_t::pdbm_t(): pdbm(nullptr), dim(0) {}
-
-    inline pdbm_t::pdbm_t(cindex_t dim): pdbm(nullptr), dim(dim) {}
-
-    inline pdbm_t::pdbm_t(PDBM pdbm, cindex_t dim): pdbm(pdbm), dim(dim) { pdbm_incRef(pdbm); }
-
-    inline pdbm_t::pdbm_t(const pdbm_t& other): pdbm(other.pdbm), dim(other.dim) { pdbm_incRef(pdbm); }
-
-    inline pdbm_t::~pdbm_t() { pdbm_decRef(pdbm); }
-
-    inline pdbm_t& pdbm_t::operator=(const pdbm_t& other)
-    {
-        pdbm_incRef(other.pdbm);
-        pdbm_decRef(pdbm);
-        dim = other.dim;
-        pdbm = other.pdbm;
-        return *this;
-    }
-
     inline void pdbm_t::setDimension(cindex_t dim)
     {
-        pdbm_decRef(pdbm);
-        pdbm = nullptr;
+        pdbm.reset();
         this->dim = dim;
     }
 
@@ -220,57 +183,39 @@ namespace dbm
         using iterator = std::list<pdbm_t>::iterator;
 
     protected:
-        struct pfed_s
+        struct pfed_s : std::enable_shared_from_this<pfed_s>
         {
             std::list<pdbm_t> zones;
-            uint32_t count;
-            cindex_t dim;
+            cindex_t dim{0};
         };
 
-        static std::allocator<pfed_s> alloc;
-
         /** Pointer to record holding the federation. */
-        struct pfed_s* ptr;
-
-        /** Increment reference count. */
-        void incRef();
-
-        /** Decrement reference count. */
-        void decRef();
+        std::shared_ptr<pfed_s> ptr = std::make_shared<pfed_s>();
 
         /** Prepare federation for modification. */
         void prepare();
 
-        /** Copy-on-write: Creates an unshared copy of the federation. */
+        /** Copy-on-write: Creates an exclusive copy of the federation. */
         void cow();
 
         /**
          * Adds \a pdbm to the federation. The reference count on pdbm
          * is incremented by one.
          */
-        void add(const PDBM pdbm, cindex_t dim);
+        void add(PDBMPtr pdbm, cindex_t dim);
 
     public:
         /** Allocate empty priced federation of dimension 0. */
-        pfed_t();
+        pfed_t() = default;
 
         /** Allocate empty priced federation of dimension \a dim. */
-        explicit pfed_t(cindex_t dim);
+        explicit pfed_t(cindex_t dim) { ptr->dim = dim; }
 
         /**
          * Allocate a priced federation of dimension \a dim initialised to
          * \a pdbm.
          */
-        pfed_t(const PDBM pdbm, cindex_t dim);
-
-        /** The copy constructor implements copy on write. */
-        pfed_t(const pfed_t&);
-
-        /**
-         * The destructor decrements the reference count and deallocates
-         * the priced DBM when the count reaches zero.
-         */
-        ~pfed_t() noexcept;
+        pfed_t(PDBMPtr pdbm, cindex_t dim): pfed_t{dim} { add(std::move(pdbm), dim); }
 
         /**
          * Constrain x(i) to value.
@@ -427,13 +372,13 @@ namespace dbm
         pfed_t& operator=(const pfed_t&);
 
         /** Assignment operator. */
-        pfed_t& operator=(const PDBM);
+        pfed_t& operator=(const PDBMPtr&);
 
         /** Union operator. */
         pfed_t& operator|=(const pfed_t&);
 
         /** Union operator. */
-        pfed_t& operator|=(const PDBM);
+        pfed_t& operator|=(const PDBMPtr&);
 
         /** Not implemented. */
         pfed_t& operator-=(const pfed_t&);
@@ -567,17 +512,9 @@ namespace dbm
         }
     }
 
-    inline pfed_t::pfed_t(const pfed_t& pfed): ptr(pfed.ptr) { incRef(); }
-
-    inline pfed_t::~pfed_t()
-    {
-        assert(ptr->count > 0);
-        decRef();
-    }
-
     inline void pfed_t::prepare()
     {
-        if (ptr->count > 1) {
+        if (ptr.use_count() > 1) {
             cow();
         }
     }
@@ -602,8 +539,6 @@ namespace dbm
 
     inline size_t pfed_t::size() const { return ptr->zones.size(); }
 
-    inline void pfed_t::incRef() { ptr->count++; }
-
     inline bool pfed_t::isEmpty() const { return ptr->zones.empty(); }
 
     inline const pdbm_t& pfed_t::const_dbmt() const
@@ -618,9 +553,9 @@ namespace dbm
         return ptr->zones.front();
     }
 
-    inline pfed_t& pfed_t::operator=(const PDBM pdbm)
+    inline pfed_t& pfed_t::operator=(const PDBMPtr& pdbm)
     {
-        *this = pfed_t(pdbm, ptr->dim);
+        *this = pfed_t{pdbm, ptr->dim};
         return *this;
     }
 
diff --git a/include/dbm/priced.h b/include/dbm/priced.h
index 239313a..6953f58 100644
--- a/include/dbm/priced.h
+++ b/include/dbm/priced.h
@@ -18,6 +18,7 @@
 
 #include <iosfwd>
 #include <utility>
+#include <memory>
 #include <cstdio>
 
 /**
@@ -68,7 +69,9 @@
 /**
  * Data type for priced dbm.
  */
-typedef struct PDBM_s* PDBM;
+struct PDBM_s;
+using PDBMPtr = std::shared_ptr<PDBM_s>;
+using PDBMCPtr = std::shared_ptr<const PDBM_s>;
 
 /**
  * Computes the size in number of bytes of a priced dbm of the given
@@ -90,7 +93,7 @@ size_t pdbm_size(cindex_t dim);
  *
  * @return An unitialised priced DBM of dimension \a dim.
  */
-PDBM pdbm_reserve(cindex_t dim, void* p);
+PDBMPtr pdbm_reserve(cindex_t dim, void* p);
 
 /**
  * Allocates a new priced DBM. The reference count is initialised to
@@ -100,7 +103,7 @@ PDBM pdbm_reserve(cindex_t dim, void* p);
  * @return A newly allocated priced DBM of dimension \a dim.
  * @pre    dim is larger than 0.
  */
-PDBM pdbm_allocate(cindex_t dim);
+PDBMPtr pdbm_allocate(cindex_t dim);
 
 /**
  * Deallocates a priced DBM.
@@ -109,40 +112,7 @@ PDBM pdbm_allocate(cindex_t dim);
  * - \a pdbm was allocated with \c pdbm_allocate().
  * - The reference count of \a pdbm is zero.
  */
-void pdbm_deallocate(PDBM& pdbm);
-
-/**
- * Increases reference count on priced DBM.
- *
- * @param pdbm is a priced DBM.
- * @pre
- * \a pdbm has been allocated with \c pdbm_allocate() and is not NULL.
- */
-inline static void pdbm_incRef(PDBM pdbm)
-{
-    assert(pdbm);
-
-    (*(int32_t*)pdbm)++;
-}
-
-/**
- * Decreases reference count on priced DBM. The DBM is deallocated
- * when the reference count reaches zero.
- *
- * @param pdbm is a priced DBM.
- * @pre   \a pdbm has been allocated with \c pdbm_allocate().
- */
-inline static void pdbm_decRef(PDBM pdbm)
-{
-    assert(pdbm == nullptr || *(int32_t*)pdbm);
-
-    /* The following relies on the reference counter being the first
-     * field of the structure.
-     */
-    if (pdbm && !--*(int32_t*)pdbm) {
-        pdbm_deallocate(pdbm);
-    }
-}
+void pdbm_deallocate(PDBM_s* pdbm);
 
 /**
  * Copy a priced DBM.
@@ -162,7 +132,7 @@ inline static void pdbm_decRef(PDBM pdbm)
  * @post   The reference count of the return value is zero.
  * @return The destination.
  */
-PDBM pdbm_copy(PDBM dst, const PDBM src, cindex_t dim);
+PDBMPtr pdbm_copy(PDBMPtr dst, const PDBMCPtr& src, cindex_t dim);
 
 /**
  * Initialises a priced DBM to the DBM containing all valuations. The
@@ -172,7 +142,7 @@ PDBM pdbm_copy(PDBM dst, const PDBM src, cindex_t dim);
  * @param pdbm is the priced DBM to initialize.
  * @param dim  is the dimension of \a pdbm.
  */
-void pdbm_init(PDBM& pdbm, cindex_t dim);
+void pdbm_init(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Initialize a priced DBM to only contain the origin with a cost of
@@ -182,7 +152,7 @@ void pdbm_init(PDBM& pdbm, cindex_t dim);
  * @param pdbm is the priced DBM to initialise.
  * @param dim  is the dimension of \a pdbm.
  */
-void pdbm_zero(PDBM& pdbm, cindex_t dim);
+void pdbm_zero(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Constrain a priced DBM.
@@ -201,7 +171,7 @@ void pdbm_zero(PDBM& pdbm, cindex_t dim);
  * @post   The DBM is empty or closed.
  * @return True if and only if the result is not empty.
  */
-bool pdbm_constrain1(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint);
+bool pdbm_constrain1(PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint);
 
 /**
  * Constrain a priced DBM with multiple constraints.
@@ -219,7 +189,7 @@ bool pdbm_constrain1(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t con
  * - or false if the DBM is empty +
  *   empty DBM + inconsistent rates
  */
-bool pdbm_constrainN(PDBM& pdbm, cindex_t dim, const constraint_t* constraints, size_t n);
+bool pdbm_constrainN(PDBMPtr& pdbm, cindex_t dim, const constraint_t* constraints, size_t n);
 
 /**
  * Constrain a priced DBM to a facet (\a i, \a j).
@@ -232,7 +202,7 @@ bool pdbm_constrainN(PDBM& pdbm, cindex_t dim, const constraint_t* constraints,
  * @return
  * true if and only if the result is non empty.
  */
-bool pdbm_constrainToFacet(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j);
+bool pdbm_constrainToFacet(PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j);
 
 /**
  * Relation between two priced DBMs.
@@ -243,7 +213,7 @@ bool pdbm_constrainToFacet(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j);
  * @param  dim         is the dimension of \a pdbm1 and \a pdbm2.
  * @return The relation between pdbm1 and pdbm2
  */
-relation_t pdbm_relation(const PDBM pdbm1, const PDBM pdbm2, cindex_t dim);
+relation_t pdbm_relation(const PDBMCPtr& pdbm1, const PDBMCPtr& pdbm2, cindex_t dim);
 
 /**
  * Relation between 2 priced dbms where one is in compressed. Notice
@@ -258,7 +228,7 @@ relation_t pdbm_relation(const PDBM pdbm1, const PDBM pdbm2, cindex_t dim);
  * @see    dbm_relationWithMinDBM
  * @see    relation_t
  */
-relation_t pdbm_relationWithMinDBM(const PDBM pdbm, cindex_t dim, const mingraph_t minDBM, raw_t* buffer);
+relation_t pdbm_relationWithMinDBM(const PDBMCPtr& pdbm, cindex_t dim, const mingraph_t minDBM, raw_t* buffer);
 
 /**
  * Computes the infimum cost of the priced DBM.
@@ -267,7 +237,7 @@ relation_t pdbm_relationWithMinDBM(const PDBM pdbm, cindex_t dim, const mingraph
  * @param  dim  is the dimension of \a pdbm.
  * @return The infimum cost of \a pdbm.
  */
-int32_t pdbm_getInfimum(const PDBM pdbm, cindex_t dim);
+int32_t pdbm_getInfimum(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Generates a valuation which has the infimum cost of the priced DBM.
@@ -291,7 +261,7 @@ int32_t pdbm_getInfimum(const PDBM pdbm, cindex_t dim);
  * @throw out_of_range if no valuation with the given constraints can
  * be found.
  */
-int32_t pdbm_getInfimumValuation(const PDBM pdbm, cindex_t dim, int32_t* valuation, const bool* free);
+int32_t pdbm_getInfimumValuation(const PDBMCPtr& pdbm, cindex_t dim, int32_t* valuation, const bool* free);
 
 /**
  * Check if a priced DBM satisfies a given constraint.
@@ -302,7 +272,7 @@ int32_t pdbm_getInfimumValuation(const PDBM pdbm, cindex_t dim, int32_t* valuati
  * @param constraint is the raw_t bound.
  * @return true if the DBM satisfies the constraint.
  */
-bool pdbm_satisfies(const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint);
+bool pdbm_satisfies(const PDBMCPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint);
 
 /**
  * Returns true if the priced DBM is empty.
@@ -311,7 +281,7 @@ bool pdbm_satisfies(const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t
  * @param dim  is the dimension of \a pdbm.
  * @return true if and only if the priced dbm is empty.
  */
-bool pdbm_isEmpty(const PDBM pdbm, cindex_t dim);
+bool pdbm_isEmpty(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Check if at least one point can delay infinitely.
@@ -320,7 +290,7 @@ bool pdbm_isEmpty(const PDBM pdbm, cindex_t dim);
  * @param  dim  is the dimension of \a pdbm.
  * @return true if unbounded, false otherwise.
  */
-bool pdbm_isUnbounded(const PDBM pdbm, cindex_t dim);
+bool pdbm_isUnbounded(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Compute a hash value for a priced DBM.
@@ -332,7 +302,7 @@ bool pdbm_isUnbounded(const PDBM pdbm, cindex_t dim);
  * @param  seed is a seed for the hash function.
  * @return hash value.
  */
-uint32_t pdbm_hash(const PDBM pdbm, cindex_t dim, uint32_t seed);
+uint32_t pdbm_hash(const PDBMCPtr& pdbm, cindex_t dim, uint32_t seed);
 
 /**
  * Test if a point is included in the priced DBM.
@@ -342,7 +312,7 @@ uint32_t pdbm_hash(const PDBM pdbm, cindex_t dim, uint32_t seed);
  * @param  pt   is a clock valuation.
  * @return true if \a pt satisfies the constraints of dbm.
  */
-bool pdbm_containsInt(const PDBM pdbm, cindex_t dim, const int32_t* pt);
+bool pdbm_containsInt(const PDBMCPtr& pdbm, cindex_t dim, const int32_t* pt);
 
 /**
  * Test if a point is included in the priced DBM when strictness of
@@ -354,7 +324,7 @@ bool pdbm_containsInt(const PDBM pdbm, cindex_t dim, const int32_t* pt);
  * @return true if \a pt satisfies the constraints of dbm
  *              (ignoring strictness)
  */
-bool pdbm_containsIntWeakly(const PDBM pdbm, cindex_t dim, const int32_t* pt);
+bool pdbm_containsIntWeakly(const PDBMCPtr& pdbm, cindex_t dim, const int32_t* pt);
 
 /**
  * Test if a point is included in the priced DBM.
@@ -364,7 +334,7 @@ bool pdbm_containsIntWeakly(const PDBM pdbm, cindex_t dim, const int32_t* pt);
  * @param  pt   is a clock valuation.
  * @return true if \a pt satisfies the constraints of dbm.
  */
-bool pdbm_containsDouble(const PDBM pdbm, cindex_t dim, const double* pt);
+bool pdbm_containsDouble(const PDBMCPtr& pdbm, cindex_t dim, const double* pt);
 
 /**
  * Delay with the current delay rate.
@@ -374,7 +344,7 @@ bool pdbm_containsDouble(const PDBM pdbm, cindex_t dim, const double* pt);
  * @see   pdbm_delayRate()
  * @post  The priced DBM is closed.
  */
-void pdbm_up(PDBM& pdbm, cindex_t dim);
+void pdbm_up(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Delay with delay rate \a rate. There must be at least one clock
@@ -387,7 +357,7 @@ void pdbm_up(PDBM& pdbm, cindex_t dim);
  *              reference clock.
  * @post  The priced DBM is closed.
  */
-void pdbm_upZero(PDBM& pdbm, cindex_t dim, int32_t rate, cindex_t zero);
+void pdbm_upZero(PDBMPtr& pdbm, cindex_t dim, int32_t rate, cindex_t zero);
 
 /**
  * Updates \a clock to \a value. This is only legitimate if the
@@ -400,7 +370,7 @@ void pdbm_upZero(PDBM& pdbm, cindex_t dim, int32_t rate, cindex_t zero);
  * @pre   pdbm_getRate(pdbm, dim, clock) == 0
  * @post  The priced DBM is closed.
  */
-void pdbm_updateValue(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value);
+void pdbm_updateValue(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, uint32_t value);
 
 /**
  * Updates \a clock to \a value. This is only legitimate if the clock
@@ -416,21 +386,21 @@ void pdbm_updateValue(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value);
  * @post  The priced DBM is closed.
  * @post  pdbm_getRate(pdbm, dim, clock) == 0
  */
-void pdbm_updateValueZero(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value, cindex_t zero);
+void pdbm_updateValueZero(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, uint32_t value, cindex_t zero);
 
 /**
  * Unfinished extrapolation function.
  *
  * @see dbm_extrapolateMaxBounds
  */
-void pdbm_extrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max);
+void pdbm_extrapolateMaxBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* max);
 
 /**
  * Unfinished extrapolation function.
  *
  * @see dbm_diagonalExtrapolateMaxBounds
  */
-void pdbm_diagonalExtrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max);
+void pdbm_diagonalExtrapolateMaxBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* max);
 
 /**
  * Extrapolate a priced zone. The extrapolation is based on a lower
@@ -447,7 +417,7 @@ void pdbm_diagonalExtrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max);
  * @post  The priced DBM is closed.
  * @see dbm_diagonalExtrapolateLUBounds
  */
-void pdbm_diagonalExtrapolateLUBounds(PDBM& pdbm, cindex_t dim, int32_t* lower, int32_t* upper);
+void pdbm_diagonalExtrapolateLUBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* lower, int32_t* upper);
 
 /**
  * Increments the cost of each point in a priced DBM by \a value.
@@ -458,7 +428,7 @@ void pdbm_diagonalExtrapolateLUBounds(PDBM& pdbm, cindex_t dim, int32_t* lower,
  * @post  The priced DBM is closed.
  * @pre   value >= 0
  */
-void pdbm_incrementCost(PDBM& pdbm, cindex_t dim, int32_t value);
+void pdbm_incrementCost(PDBMPtr& pdbm, cindex_t dim, int32_t value);
 
 /**
  * Compute the closure of a priced DBM. This function is only relevant
@@ -469,7 +439,7 @@ void pdbm_incrementCost(PDBM& pdbm, cindex_t dim, int32_t value);
  * @post  The priced DBM is closed or empty.
  * @see   pdbm_setBound
  */
-void pdbm_close(PDBM& pdbm, cindex_t dim);
+void pdbm_close(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Analyze a priced DBM for its minimal graph representation. Computes
@@ -486,7 +456,7 @@ void pdbm_close(PDBM& pdbm, cindex_t dim);
  * @param  bitMatrix  is bit matrix of size dim*dim
  * @return The number of bits marked one in \a bitMatrix.
  */
-size_t pdbm_analyzeForMinDBM(const PDBM pdbm, cindex_t dim, uint32_t* bitMatrix);
+size_t pdbm_analyzeForMinDBM(const PDBMCPtr& pdbm, cindex_t dim, uint32_t* bitMatrix);
 
 /**
  * Convert the DBM to a more compact representation.
@@ -517,7 +487,7 @@ size_t pdbm_analyzeForMinDBM(const PDBM pdbm, cindex_t dim, uint32_t* bitMatrix)
  * @return The converted priced DBM. The first \a offset integers are unused.
  * @pre    allocFunction allocates memory in integer units
  */
-int32_t* pdbm_writeToMinDBMWithOffset(const PDBM pdbm, cindex_t dim, bool minimizeGraph, bool tryConstraints16,
+int32_t* pdbm_writeToMinDBMWithOffset(const PDBMCPtr& pdbm, cindex_t dim, bool minimizeGraph, bool tryConstraints16,
                                       allocator_t c_alloc, uint32_t offset);
 
 /**
@@ -531,7 +501,7 @@ int32_t* pdbm_writeToMinDBMWithOffset(const PDBM pdbm, cindex_t dim, bool minimi
  * @param src  is the compressed priced DBM.
  * @post  dst is a closed priced DBM.
  */
-void pdbm_readFromMinDBM(PDBM& dst, cindex_t dim, mingraph_t src);
+void pdbm_readFromMinDBM(PDBMPtr& dst, cindex_t dim, mingraph_t src);
 
 /**
  * Finds a clock that is on a zero cycle with \a clock. Returns true
@@ -548,7 +518,7 @@ void pdbm_readFromMinDBM(PDBM& dst, cindex_t dim, mingraph_t src);
  * @param  out   is where the clock found is written.
  * @return true if and only if a clock is found.
  */
-bool pdbm_findZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t clock, cindex_t* out);
+bool pdbm_findZeroCycle(const PDBMCPtr& pdbm, cindex_t dim, cindex_t clock, cindex_t* out);
 
 /**
  * Finds a clock that is on a zero cycle with \a clock. Returns true
@@ -563,7 +533,7 @@ bool pdbm_findZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t clock, cindex_t*
  * @param  out   is where the clock found is written.
  * @return true if and only if a clock is found.
  */
-bool pdbm_findNextZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t* out);
+bool pdbm_findNextZeroCycle(const PDBMCPtr& pdbm, cindex_t dim, cindex_t x, cindex_t* out);
 
 /**
  * Returns the slope of the cost plane along the delay trajectory.
@@ -571,7 +541,7 @@ bool pdbm_findNextZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t*
  * @param pdbm  is a closed priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-int32_t pdbm_getSlopeOfDelayTrajectory(const PDBM pdbm, cindex_t dim);
+int32_t pdbm_getSlopeOfDelayTrajectory(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Returns the rate (coefficient of the hyperplane) of \a clock.
@@ -581,9 +551,9 @@ int32_t pdbm_getSlopeOfDelayTrajectory(const PDBM pdbm, cindex_t dim);
  * @param  clock is the clock for which to return the coefficient.
  * @return the rate of \a clock.
  */
-int32_t pdbm_getRate(const PDBM pdbm, cindex_t dim, cindex_t clock);
+int32_t pdbm_getRate(const PDBMCPtr& pdbm, cindex_t dim, cindex_t clock);
 
-const int32_t* pdbm_getRates(const PDBM pdbm, cindex_t dim);
+const int32_t* pdbm_getRates(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Returns the cost of the offset point.
@@ -591,7 +561,7 @@ const int32_t* pdbm_getRates(const PDBM pdbm, cindex_t dim);
  * @param pdbm  is a closed priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-uint32_t pdbm_getCostAtOffset(const PDBM pdbm, cindex_t dim);
+uint32_t pdbm_getCostAtOffset(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Sets the cost at the offset point.
@@ -605,7 +575,7 @@ uint32_t pdbm_getCostAtOffset(const PDBM pdbm, cindex_t dim);
  * @param dim   is the dimension of \a pdbm.
  * @param value is the new cost of the offset point.
  */
-void pdbm_setCostAtOffset(PDBM& pdbm, cindex_t dim, uint32_t value);
+void pdbm_setCostAtOffset(PDBMPtr& pdbm, cindex_t dim, uint32_t value);
 
 /**
  * Returns true if the DBM is valid. Useful for debugging.
@@ -613,7 +583,7 @@ void pdbm_setCostAtOffset(PDBM& pdbm, cindex_t dim, uint32_t value);
  * @param pdbm  is a priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-bool pdbm_isValid(const PDBM pdbm, cindex_t dim);
+bool pdbm_isValid(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Computes the lower facets of a priced DBM relative to \a clock.  As
@@ -627,7 +597,7 @@ bool pdbm_isValid(const PDBM pdbm, cindex_t dim);
  *                the lower facets will be written.
  * @return The number of facets written to \a facets.
  */
-uint32_t pdbm_getLowerRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets);
+uint32_t pdbm_getLowerRelativeFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets);
 
 /**
  * Computes the upper facets of a priced DBM relative to \a clock.  As
@@ -641,7 +611,7 @@ uint32_t pdbm_getLowerRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, c
  *                the upper facets will be written.
  * @return The number of facets written to \a facets.
  */
-uint32_t pdbm_getUpperRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets);
+uint32_t pdbm_getUpperRelativeFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets);
 
 /**
  * Computes the lower facets of a priced DBM.
@@ -652,7 +622,7 @@ uint32_t pdbm_getUpperRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, c
  *                lower facets will be written.
  * @return The number of facets written to \a facets.
  */
-uint32_t pdbm_getLowerFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets);
+uint32_t pdbm_getLowerFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t* facets);
 
 /**
  * Computes the upper facets of a priced DBM.
@@ -663,7 +633,7 @@ uint32_t pdbm_getLowerFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets);
  *                upper facets will be written.
  * @return The number of facets written to \a facets.
  */
-uint32_t pdbm_getUpperFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets);
+uint32_t pdbm_getUpperFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t* facets);
 
 /**
  * Computes the cost of a valuation in a priced DBM.
@@ -674,7 +644,7 @@ uint32_t pdbm_getUpperFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets);
  * @pre    pdbm_containsInt(pdbm, dim, valuation)
  * @return The cost of \a valuation in \a pdbm.
  */
-int32_t pdbm_getCostOfValuation(const PDBM pdbm, cindex_t dim, const int32_t* valuation);
+int32_t pdbm_getCostOfValuation(const PDBMCPtr& pdbm, cindex_t dim, const int32_t* valuation);
 
 /**
  * Makes all strong constraints of a priced DBM weak.
@@ -683,7 +653,7 @@ int32_t pdbm_getCostOfValuation(const PDBM pdbm, cindex_t dim, const int32_t* va
  * @param dim       is the dimension of \a pdbm.
  * @post  The priced DBM is closed.
  */
-void pdbm_relax(PDBM& pdbm, cindex_t dim);
+void pdbm_relax(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Computes the offset point of a priced DBM.
@@ -693,7 +663,7 @@ void pdbm_relax(PDBM& pdbm, cindex_t dim);
  * @param valuation is an array of at least \a dim elements to which the
  *                  offset point is written.
  */
-void pdbm_getOffset(const PDBM pdbm, cindex_t dim, int32_t* valuation);
+void pdbm_getOffset(const PDBMCPtr& pdbm, cindex_t dim, int32_t* valuation);
 
 /**
  * Sets a coefficient of the hyperplane of a priced DBM.
@@ -703,7 +673,7 @@ void pdbm_getOffset(const PDBM pdbm, cindex_t dim, int32_t* valuation);
  * @param clock is the index of a clock for which to set the coefficient.
  * @param rate  is the coefficient.
  */
-void pdbm_setRate(PDBM& pdbm, cindex_t dim, cindex_t clock, int32_t rate);
+void pdbm_setRate(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, int32_t rate);
 
 /**
  * Returns the inner matrix of a priced DBM. The matrix can be
@@ -713,7 +683,7 @@ void pdbm_setRate(PDBM& pdbm, cindex_t dim, cindex_t clock, int32_t rate);
  * @param pdbm  is a priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-raw_t* pdbm_getMutableMatrix(PDBM& pdbm, cindex_t dim);
+raw_t* pdbm_getMutableMatrix(PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Returns the inner matrix of a priced DBM. The matrix is read-only.
@@ -721,7 +691,7 @@ raw_t* pdbm_getMutableMatrix(PDBM& pdbm, cindex_t dim);
  * @param pdbm  is a closed priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-const raw_t* pdbm_getMatrix(const PDBM pdbm, cindex_t dim);
+const raw_t* pdbm_getMatrix(const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Frees a clock of a priced DBM.
@@ -730,7 +700,7 @@ const raw_t* pdbm_getMatrix(const PDBM pdbm, cindex_t dim);
  * @param dim   is the dimension of \a pdbm.
  * @param clock is the index of the clock to free.
  */
-void pdbm_freeClock(PDBM& pdbm, cindex_t dim, cindex_t clock);
+void pdbm_freeClock(PDBMPtr& pdbm, cindex_t dim, cindex_t clock);
 
 /**
  * Prints a priced DBM to a stream.
@@ -740,7 +710,7 @@ void pdbm_freeClock(PDBM& pdbm, cindex_t dim, cindex_t clock);
  * @param dim  is the dimension of \a pdbm.
  * @see dbm_print
  */
-void pdbm_print(FILE* f, const PDBM pdbm, cindex_t dim);
+void pdbm_print(FILE* f, const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Prints a priced DBM to a stream.
@@ -750,7 +720,7 @@ void pdbm_print(FILE* f, const PDBM pdbm, cindex_t dim);
  * @param dim  is the dimension of \a pdbm.
  * @see dbm_print
  */
-std::ostream& pdbm_print(std::ostream& os, const PDBM pdbm, cindex_t dim);
+std::ostream& pdbm_print(std::ostream& os, const PDBMCPtr& pdbm, cindex_t dim);
 
 /**
  * Implementation of the free up operation for priced DBMs.
@@ -760,7 +730,7 @@ std::ostream& pdbm_print(std::ostream& os, const PDBM pdbm, cindex_t dim);
  * @param index is an index of a clock.
  * @see dbm_freeUp
  */
-void pdbm_freeUp(PDBM& pdbm, cindex_t dim, cindex_t index);
+void pdbm_freeUp(PDBMPtr& pdbm, cindex_t dim, cindex_t index);
 
 /**
  * Implementation of the free down operation for priced DBMs.
@@ -770,7 +740,7 @@ void pdbm_freeUp(PDBM& pdbm, cindex_t dim, cindex_t index);
  * @param index is an index of a clock. *
  * @see dbm_freeDown
  */
-void pdbm_freeDown(PDBM& pdbm, cindex_t dim, cindex_t index);
+void pdbm_freeDown(PDBMPtr& pdbm, cindex_t dim, cindex_t index);
 
 /**
  * Checks whether a priced DBM is in normal form.
@@ -778,7 +748,7 @@ void pdbm_freeDown(PDBM& pdbm, cindex_t dim, cindex_t index);
  * @param pdbm  is a closed priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-bool pdbm_hasNormalForm(PDBM pdbm, cindex_t dim);
+bool pdbm_hasNormalForm(const PDBMPtr& pdbm, cindex_t dim);
 
 /**
  * Brings a priced DBM into normal form.
@@ -786,7 +756,7 @@ bool pdbm_hasNormalForm(PDBM pdbm, cindex_t dim);
  * @param pdbm  is a closed priced DBM of dimension \a dim.
  * @param dim   is the dimension of \a pdbm.
  */
-void pdbm_normalise(PDBM pdbm, cindex_t dim);
+void pdbm_normalise(const PDBMPtr& pdbm, cindex_t dim);
 
 ///////////////////////////////////////////////////////////////////////////
 
diff --git a/src/pfed.cpp b/src/pfed.cpp
index 5844da7..232d091 100644
--- a/src/pfed.cpp
+++ b/src/pfed.cpp
@@ -15,57 +15,15 @@
 
 namespace dbm
 {
-    std::allocator<pfed_t::pfed_s> pfed_t::alloc;
-
-    void pfed_t::decRef()
-    {
-        if (--(ptr->count) == 0) {
-            alloc.destroy(ptr);
-            alloc.deallocate(ptr, 1);
-        }
-    }
-
     void pfed_t::cow()
     {
-        assert(ptr->count > 1);
-
-        ptr->count--;
-        pfed_s* old = ptr;
-        ptr = alloc.allocate(1);
-        alloc.construct(ptr, pfed_s());
-        ptr->zones = old->zones;
-        ptr->dim = old->dim;
-        ptr->count = 1;
-    }
-
-    pfed_t::pfed_t()
-    {
-        ptr = alloc.allocate(1);
-        alloc.construct(ptr, pfed_s());
-        ptr->dim = 0;
-        ptr->count = 1;
-    }
-
-    pfed_t::pfed_t(cindex_t dim)
-    {
-        ptr = alloc.allocate(1);
-        alloc.construct(ptr, pfed_s());
-        ptr->dim = dim;
-        ptr->count = 1;
-    }
-
-    pfed_t::pfed_t(const PDBM pdbm, cindex_t dim)
-    {
-        ptr = alloc.allocate(1);
-        alloc.construct(ptr, pfed_s());
-        ptr->dim = dim;
-        ptr->count = 1;
-        add(pdbm, dim);
+        assert(ptr.use_count() > 1);
+        ptr = std::make_shared<pfed_s>(*ptr);
     }
 
     pfed_t::iterator pfed_t::erase(iterator i)
     {
-        assert(ptr->count <= 1);
+        assert(ptr.use_count() <= 1);
         return ptr->zones.erase(i);
     }
 
@@ -79,14 +37,14 @@ namespace dbm
     bool pfed_t::constrain(cindex_t i, cindex_t j, raw_t constraint)
     {
         erase_if_not(
-            [dim = ptr->dim, i, j, constraint](PDBM& pdbm) { return pdbm_constrain1(pdbm, dim, i, j, constraint); });
+            [dim = ptr->dim, i, j, constraint](PDBMPtr& pdbm) { return pdbm_constrain1(pdbm, dim, i, j, constraint); });
         return !isEmpty();
     }
 
     bool pfed_t::constrain(const constraint_t* constraints, size_t n)
     {
         erase_if_not(
-            [dim = ptr->dim, constraints, n](PDBM& pdbm) { return pdbm_constrainN(pdbm, dim, constraints, n); });
+            [dim = ptr->dim, constraints, n](PDBMPtr& pdbm) { return pdbm_constrainN(pdbm, dim, constraints, n); });
         return !isEmpty();
     }
 
@@ -94,7 +52,7 @@ namespace dbm
 
     int32_t pfed_t::getInfimum() const
     {
-        return std::accumulate(cbegin(), cend(), INT_MAX, [dim = ptr->dim](const int32_t a, const PDBM pdbm) {
+        return std::accumulate(cbegin(), cend(), INT_MAX, [dim = ptr->dim](const int32_t a, const PDBMCPtr& pdbm) {
             return min(a, pdbm_getInfimum(pdbm, dim));
         });
     }
@@ -377,23 +335,23 @@ namespace dbm
             pdbm_freeClock(zone, ptr->dim, clock);
     }
 
-    void pfed_t::add(const PDBM pdbm, cindex_t dim)
+    void pfed_t::add(PDBMPtr pdbm, cindex_t dim)
     {
         assert(dim == ptr->dim);
         prepare();
-        ptr->zones.push_front(pdbm_t(pdbm, dim));
+        ptr->zones.emplace_front(std::move(pdbm), dim);
     }
 
     void pfed_t::setZero()
     {
-        PDBM pdbm = nullptr;
+        auto pdbm = PDBMPtr{};
         pdbm_zero(pdbm, ptr->dim);
         *this = pfed_t(pdbm, ptr->dim);
     }
 
     void pfed_t::setInit()
     {
-        PDBM pdbm = nullptr;
+        auto pdbm = PDBMPtr{};
         pdbm_init(pdbm, ptr->dim);
         *this = pfed_t(pdbm, ptr->dim);
     }
@@ -415,9 +373,7 @@ namespace dbm
     pfed_t& pfed_t::operator=(const pfed_t& fed)
     {
         if (ptr != fed.ptr) {
-            decRef();
             ptr = fed.ptr;
-            incRef();
         }
         return *this;
     }
@@ -431,7 +387,7 @@ namespace dbm
         return *this;
     }
 
-    pfed_t& pfed_t::operator|=(const PDBM pdbm)
+    pfed_t& pfed_t::operator|=(const PDBMPtr& pdbm)
     {
         // REVISIT: Eliminate included zones.
         add(pdbm, ptr->dim);
diff --git a/src/priced.cpp b/src/priced.cpp
index 00b590e..2e6649d 100644
--- a/src/priced.cpp
+++ b/src/priced.cpp
@@ -23,24 +23,24 @@
 #include <iostream>
 #include <stdexcept>
 #include <cassert>
-#include <cstdlib>
+#include <memory>
 
-struct PDBM_s
+struct PDBM_s : std::enable_shared_from_this<PDBM_s>
 {
-    uint32_t count;
     uint32_t cost;
     uint32_t infimum;
     int32_t data[];
 };
 
 /** Returns the vectors of coefficients. */
-static inline int32_t* pdbm_rates(const PDBM pdbm) { return pdbm->data; }
+static const int32_t* pdbm_rates(const PDBMCPtr& pdbm) { return pdbm->data; }
+static int32_t* pdbm_rates(const PDBMPtr& pdbm) { return pdbm->data; }
 
 /** Returns the DBM matrix part of the priced DBM. */
-static inline dbm::writer pdbm_matrix(const PDBM pdbm, cindex_t dim) { return {pdbm->data + dim, dim}; }
+static dbm::writer pdbm_matrix(const PDBMPtr& pdbm, cindex_t dim) { return {pdbm->data + dim, dim}; }
 
 /** Returns the cache infimum. */
-static inline auto& pdbm_cache(const PDBM pdbm) { return pdbm->infimum; }
+static auto& pdbm_cache(const PDBMPtr& pdbm) { return pdbm->infimum; }
 
 /** Constant to mark the cached infimum as void. */
 #define INVALID INT_MAX
@@ -55,7 +55,7 @@ static inline auto& pdbm_cache(const PDBM pdbm) { return pdbm->infimum; }
  * @param  j    is the index of a clock
  * @return True if and only if \a i and \a j form a zero cycle in \a pdbm.
  */
-static bool pdbm_areOnZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j)
+static bool pdbm_areOnZeroCycle(const PDBM_ptr& pdbm, cindex_t dim, cindex_t i, cindex_t j)
 {
     assert(pdbm && dim && i < dim && j < dim && i != j);
 
@@ -90,14 +90,12 @@ static void dbm_findZeroCycles(dbm::reader dbm, cindex_t* next)
  * Prepares a priced DBM for modification. If it is shared, a copy
  * will be created.
  */
-static void pdbm_prepare(PDBM& pdbm, cindex_t dim)
+static void pdbm_prepare(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
 
-    if (pdbm->count > 1) {
-        pdbm_decRef(pdbm);
+    if (pdbm.use_count() > 1) {
         pdbm = pdbm_copy(nullptr, pdbm, dim);
-        pdbm_incRef(pdbm);
     }
 }
 
@@ -113,12 +111,10 @@ static void pdbm_prepare(PDBM& pdbm, cindex_t dim)
  *
  *  - no copy is performed, even when the priced DBM was shared.
  */
-static void pdbm_blank(PDBM& pdbm, cindex_t dim)
+static void pdbm_blank(PDBMPtr& pdbm, cindex_t dim)
 {
-    if (pdbm == nullptr || pdbm->count > 1) {
-        pdbm_decRef(pdbm);
+    if (pdbm == nullptr || pdbm.use_count() > 1) {
         pdbm = pdbm_allocate(dim);
-        pdbm_incRef(pdbm);
     }
 }
 
@@ -128,50 +124,40 @@ size_t pdbm_size(cindex_t dim)
     return sizeof(struct PDBM_s) + (dim * dim + dim) * sizeof(int32_t);
 }
 
-PDBM pdbm_reserve(cindex_t dim, void* p)
+PDBMPtr pdbm_reserve(cindex_t dim, void* p)
 {
     assert(dim && p);
-
-    PDBM pdbm = (PDBM)p;
-    pdbm->count = 0;
+    auto pdbm = PDBMPtr{new (p) PDBM_s, &pdbm_deallocate};
     pdbm_cache(pdbm) = INVALID;
     pdbm_rates(pdbm)[0] = 0;
     return pdbm;
 }
 
-PDBM pdbm_allocate(cindex_t dim)
+PDBMPtr pdbm_allocate(cindex_t dim)
 {
     assert(dim);
     return pdbm_reserve(dim, malloc(pdbm_size(dim)));
 }
 
-void pdbm_deallocate(PDBM& pdbm)
+void pdbm_deallocate(PDBM_s* pdbm)
 {
-    assert(pdbm == nullptr || pdbm->count == 0);
-
+    assert(pdbm == nullptr);
     free(pdbm);
-
-    /* Setting the pointer to NULL protects against accidental use of
-     * a deallocated priced DBM.
-     */
-    pdbm = nullptr;
 }
 
-PDBM pdbm_copy(PDBM dst, const PDBM src, cindex_t dim)
+PDBMPtr pdbm_copy(PDBMPtr dst, const PDBMCPtr& src, cindex_t dim)
 {
-    assert(src && dim && (dst == nullptr || dst->count == 0));
-
+    assert(src && dim && (dst == nullptr || dst.use_count() == 0));
     if (dst == nullptr) {
         dst = pdbm_allocate(dim);
     }
 
-    memcpy(dst, src, pdbm_size(dim));
-    dst->count = 0;
+    memcpy((void*)dst.get(), (const void*)src.get(), pdbm_size(dim));
 
     return dst;
 }
 
-void pdbm_init(PDBM& pdbm, cindex_t dim)
+void pdbm_init(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(dim);
 
@@ -185,7 +171,7 @@ void pdbm_init(PDBM& pdbm, cindex_t dim)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_zero(PDBM& pdbm, cindex_t dim)
+void pdbm_zero(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(dim);
 
@@ -199,7 +185,7 @@ void pdbm_zero(PDBM& pdbm, cindex_t dim)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-bool pdbm_constrain1(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
+bool pdbm_constrain1(PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
 {
     assert(pdbm && dim && i < dim && j < dim);
 
@@ -214,9 +200,8 @@ bool pdbm_constrain1(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t con
     /* If constraint will make DBM empty, then mark it as empty.
      */
     if (dbm_negRaw(constraint) >= dbm.at(j, i)) {
-        if (pdbm->count > 1) {
-            pdbm_decRef(pdbm);
-            pdbm = nullptr;
+        if (pdbm.use_count() > 1) {
+            pdbm.reset();
         } else {
             dbm.at(i, j) = constraint;
             dbm.at(0, 0) = -1; /* consistent with isEmpty */
@@ -255,7 +240,7 @@ bool pdbm_constrain1(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t con
     return true;
 }
 
-bool pdbm_constrainN(PDBM& pdbm, cindex_t dim, const constraint_t* constraints, size_t n)
+bool pdbm_constrainN(PDBMPtr& pdbm, cindex_t dim, const constraint_t* constraints, size_t n)
 {
     assert(pdbm && dim);
 
@@ -347,7 +332,7 @@ static int32_t infOfDiff(const raw_t* dbm, uint32_t dim, int32_t cost1, const in
     return pdbm_infimum(dbm, dim, cost, rates.data());
 }
 
-relation_t pdbm_relation(const PDBM pdbm1, const PDBM pdbm2, cindex_t dim)
+relation_t pdbm_relation(const PDBMPtr& pdbm1, const PDBMPtr& pdbm2, cindex_t dim)
 {
     assert(pdbm1 && pdbm2 && dim);
 
@@ -440,7 +425,7 @@ relation_t pdbm_relation(const PDBM pdbm1, const PDBM pdbm2, cindex_t dim)
     }
 }
 
-relation_t pdbm_relationWithMinDBM(const PDBM pdbm1, cindex_t dim, const mingraph_t pdbm2, raw_t* dbm2)
+relation_t pdbm_relationWithMinDBM(const PDBMPtr& pdbm1, cindex_t dim, const mingraph_t pdbm2, raw_t* dbm2)
 {
     assert(pdbm1 && pdbm2 && dim && dbm2);
 
@@ -550,18 +535,18 @@ relation_t pdbm_relationWithMinDBM(const PDBM pdbm1, cindex_t dim, const mingrap
     }
 }
 
-int32_t pdbm_getInfimum(const PDBM pdbm, cindex_t dim)
+int32_t pdbm_getInfimum(const PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
     assert(dbm_isValid(pdbm_matrix(pdbm, dim), dim));
     uint32_t cache = pdbm_cache(pdbm);
     if (cache == INVALID) {
-        pdbm_cache((PDBM)pdbm) = cache = pdbm_infimum(pdbm_matrix(pdbm, dim), dim, pdbm->cost, pdbm_rates(pdbm));
+        pdbm_cache(pdbm) = cache = pdbm_infimum(pdbm_matrix(pdbm, dim), dim, pdbm->cost, pdbm_rates(pdbm));
     }
     return cache;
 }
 
-int32_t pdbm_getInfimumValuation(const PDBM pdbm, cindex_t dim, int32_t* valuation, const bool* free)
+int32_t pdbm_getInfimumValuation(const PDBMPtr& pdbm, cindex_t dim, int32_t* valuation, const bool* free)
 {
     assert(pdbm && dim && valuation);
     assert(pdbm_isValid(pdbm, dim));
@@ -604,37 +589,36 @@ int32_t pdbm_getInfimumValuation(const PDBM pdbm, cindex_t dim, int32_t* valuati
     return cost;
 }
 
-bool pdbm_satisfies(const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
+bool pdbm_satisfies(const PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
 {
     assert(pdbm && dim && i < dim && i < dim);
     return dbm_satisfies(pdbm_matrix(pdbm, dim), dim, i, j, constraint);
 }
 
-bool pdbm_isEmpty(const PDBM pdbm, cindex_t dim)
+bool pdbm_isEmpty(const PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
     return pdbm == nullptr || dbm_isEmpty(pdbm_matrix(pdbm, dim), dim);
 }
 
-bool pdbm_isUnbounded(const PDBM pdbm, cindex_t dim)
+bool pdbm_isUnbounded(const PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
     return dbm_isUnbounded(pdbm_matrix(pdbm, dim), dim);
 }
 
-uint32_t pdbm_hash(const PDBM pdbm, cindex_t dim, uint32_t seed)
+uint32_t pdbm_hash(const PDBMCPtr& pdbm, cindex_t dim, uint32_t seed)
 {
     assert(pdbm && dim && !(pdbm_size(dim) & 3));
-    return hash_computeI32((int32_t*)pdbm, pdbm_size(dim) >> 2, seed);
+    return hash_computeI32((const int32_t*)pdbm.get(), pdbm_size(dim) >> 2, seed);
 }
 
 static bool isPointIncludedWeakly(const int32_t* pt, dbm::reader dbm, cindex_t dim)
 {
-    cindex_t i, j;
     assert(pt && dbm && dim);
 
-    for (i = 0; i < dim; ++i) {
-        for (j = 0; j < dim; ++j) {
+    for (auto i = cindex_t{0}; i < dim; ++i) {
+        for (auto j = cindex_t{0}; j < dim; ++j) {
             if (pt[i] - pt[j] > dbm.bound(i, j)) {
                 return false;
             }
@@ -644,28 +628,28 @@ static bool isPointIncludedWeakly(const int32_t* pt, dbm::reader dbm, cindex_t d
     return true;
 }
 
-bool pdbm_containsInt(const PDBM pdbm, cindex_t dim, const int32_t* pt)
+bool pdbm_containsInt(const PDBMPtr& pdbm, cindex_t dim, const int32_t* pt)
 {
     assert(pdbm && dim && pt);
 
     return dbm_isPointIncluded(pt, pdbm_matrix(pdbm, dim), dim);
 }
 
-bool pdbm_containsIntWeakly(const PDBM pdbm, cindex_t dim, const int32_t* pt)
+bool pdbm_containsIntWeakly(const PDBMPtr& pdbm, cindex_t dim, const int32_t* pt)
 {
     assert(pdbm && dim && pt);
 
     return isPointIncludedWeakly(pt, pdbm_matrix(pdbm, dim), dim);
 }
 
-bool pdbm_containsDouble(const PDBM pdbm, cindex_t dim, const double* pt)
+bool pdbm_containsDouble(const PDBMPtr& pdbm, cindex_t dim, const double* pt)
 {
     assert(pdbm && dim && pt);
 
     return dbm_isRealPointIncluded(pt, pdbm_matrix(pdbm, dim), dim);
 }
 
-void pdbm_up(PDBM& pdbm, cindex_t dim)
+void pdbm_up(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
 
@@ -675,7 +659,7 @@ void pdbm_up(PDBM& pdbm, cindex_t dim)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_upZero(PDBM& pdbm, cindex_t dim, int32_t rate, cindex_t zero)
+void pdbm_upZero(PDBMPtr& pdbm, cindex_t dim, int32_t rate, cindex_t zero)
 {
     assert(pdbm && dim && zero > 0 && zero < dim);
     assert(pdbm_areOnZeroCycle(pdbm, dim, 0, zero));
@@ -692,7 +676,7 @@ void pdbm_upZero(PDBM& pdbm, cindex_t dim, int32_t rate, cindex_t zero)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_updateValue(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value)
+void pdbm_updateValue(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, uint32_t value)
 {
     assert(pdbm && dim && clock < dim);
     assert(pdbm_getRate(pdbm, dim, clock) == 0);
@@ -704,7 +688,7 @@ void pdbm_updateValue(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_updateValueZero(PDBM& pdbm, cindex_t dim, cindex_t clock, uint32_t value, cindex_t zero)
+void pdbm_updateValueZero(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, uint32_t value, cindex_t zero)
 {
     assert(pdbm && dim && clock < dim && zero < dim);
     assert(pdbm_areOnZeroCycle(pdbm, dim, clock, zero));
@@ -766,7 +750,7 @@ U           L
  * preprocessing step, we change the maximum constant to infinity for
  * all clocks with a non-xero cost rate.
  */
-void pdbm_extrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max)
+void pdbm_extrapolateMaxBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* max)
 {
     assert(pdbm && dim);
 
@@ -789,7 +773,7 @@ void pdbm_extrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max)
  * on a zero cycle with another clock, the cost rate can be made zero
  * by transfering the rate to the other clock.
  */
-void pdbm_diagonalExtrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max)
+void pdbm_diagonalExtrapolateMaxBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* max)
 {
     assert(pdbm && dim);
 
@@ -833,7 +817,7 @@ void pdbm_diagonalExtrapolateMaxBounds(PDBM& pdbm, cindex_t dim, int32_t* max)
     dbm_diagonalExtrapolateMaxBounds(pdbm_matrix(pdbm, dim), dim, max);
 }
 
-void pdbm_diagonalExtrapolateLUBounds(PDBM& pdbm, cindex_t dim, int32_t* lower, int32_t* upper)
+void pdbm_diagonalExtrapolateLUBounds(PDBMPtr& pdbm, cindex_t dim, int32_t* lower, int32_t* upper)
 {
     assert(pdbm && dim);
 
@@ -858,7 +842,7 @@ void pdbm_diagonalExtrapolateLUBounds(PDBM& pdbm, cindex_t dim, int32_t* lower,
     dbm_diagonalExtrapolateLUBounds(pdbm_matrix(pdbm, dim), dim, lower, upper);
 }
 
-void pdbm_incrementCost(PDBM& pdbm, cindex_t dim, int32_t value)
+void pdbm_incrementCost(PDBMPtr& pdbm, cindex_t dim, int32_t value)
 {
     assert(pdbm && dim && value >= 0);
 
@@ -869,7 +853,7 @@ void pdbm_incrementCost(PDBM& pdbm, cindex_t dim, int32_t value)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_close(PDBM& pdbm, cindex_t dim)
+void pdbm_close(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(dim);
 
@@ -881,14 +865,14 @@ void pdbm_close(PDBM& pdbm, cindex_t dim)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-size_t pdbm_analyzeForMinDBM(const PDBM pdbm, cindex_t dim, uint32_t* bitMatrix)
+size_t pdbm_analyzeForMinDBM(const PDBMPtr& pdbm, cindex_t dim, uint32_t* bitMatrix)
 {
     assert(pdbm && dim);
 
     return dbm_analyzeForMinDBM(pdbm_matrix(pdbm, dim), dim, bitMatrix);
 }
 
-int32_t* pdbm_writeToMinDBMWithOffset(const PDBM pdbm, cindex_t dim, bool minimizeGraph, bool tryConstraints16,
+int32_t* pdbm_writeToMinDBMWithOffset(const PDBMPtr& pdbm, cindex_t dim, bool minimizeGraph, bool tryConstraints16,
                                       allocator_t allocator, uint32_t offset)
 {
     assert(pdbm && dim);
@@ -902,7 +886,7 @@ int32_t* pdbm_writeToMinDBMWithOffset(const PDBM pdbm, cindex_t dim, bool minimi
     return graph;
 }
 
-void pdbm_readFromMinDBM(PDBM& dst, cindex_t dim, mingraph_t src)
+void pdbm_readFromMinDBM(PDBMPtr& dst, cindex_t dim, mingraph_t src)
 {
     assert(dst && dim);
 
@@ -915,7 +899,7 @@ void pdbm_readFromMinDBM(PDBM& dst, cindex_t dim, mingraph_t src)
     assertx(pdbm_isValid(dst, dim));
 }
 
-bool pdbm_findNextZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t* out)
+bool pdbm_findNextZeroCycle(const PDBMPtr& pdbm, cindex_t dim, cindex_t x, cindex_t* out)
 {
     assert(pdbm && dim && x < dim && out);
 
@@ -934,17 +918,17 @@ bool pdbm_findNextZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t*
     return false;
 }
 
-bool pdbm_findZeroCycle(const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t* out)
+bool pdbm_findZeroCycle(const PDBMCPtr& pdbm, cindex_t dim, cindex_t x, cindex_t* out)
 {
     *out = 0;
     return pdbm_findNextZeroCycle(pdbm, dim, x, out);
 }
 
-int32_t pdbm_getSlopeOfDelayTrajectory(const PDBM pdbm, cindex_t dim)
+int32_t pdbm_getSlopeOfDelayTrajectory(const PDBMCPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
 
-    int32_t* rates = pdbm_rates(pdbm);
+    const int32_t* rates = pdbm_rates(pdbm);
     int32_t sum = 0;
     for (uint32_t i = 1; i < dim; i++) {
         sum += rates[i];
@@ -952,21 +936,21 @@ int32_t pdbm_getSlopeOfDelayTrajectory(const PDBM pdbm, cindex_t dim)
     return sum;
 }
 
-int32_t pdbm_getRate(const PDBM pdbm, cindex_t dim, cindex_t clock)
+int32_t pdbm_getRate(const PDBMCPtr& pdbm, cindex_t dim, cindex_t clock)
 {
     assert(pdbm && dim && clock > 0 && clock < dim);
 
     return pdbm_rates(pdbm)[clock];
 }
 
-uint32_t pdbm_getCostAtOffset(const PDBM pdbm, cindex_t dim)
+uint32_t pdbm_getCostAtOffset(const PDBMCPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
 
     return pdbm->cost;
 }
 
-void pdbm_setCostAtOffset(PDBM& pdbm, cindex_t dim, uint32_t value)
+void pdbm_setCostAtOffset(PDBMPtr& pdbm, cindex_t dim, uint32_t value)
 {
     assert(pdbm && dim);
 
@@ -1002,7 +986,7 @@ static bool isRedundant(dbm::reader dbm, cindex_t i, cindex_t j, cindex_t* next)
     return true;
 }
 
-uint32_t pdbm_getLowerRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets)
+uint32_t pdbm_getLowerRelativeFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets)
 {
     assert(pdbm && dim && clock < dim);
 
@@ -1033,7 +1017,7 @@ uint32_t pdbm_getLowerRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, c
     return cnt;
 }
 
-uint32_t pdbm_getUpperRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets)
+uint32_t pdbm_getUpperRelativeFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, cindex_t* facets)
 {
     assert(pdbm && dim && clock < dim && facets);
 
@@ -1065,7 +1049,7 @@ uint32_t pdbm_getUpperRelativeFacets(PDBM& pdbm, cindex_t dim, cindex_t clock, c
     return cnt;
 }
 
-uint32_t pdbm_getLowerFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets)
+uint32_t pdbm_getLowerFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t* facets)
 {
     assert(pdbm && dim && facets);
 
@@ -1097,7 +1081,7 @@ uint32_t pdbm_getLowerFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets)
     return cnt;
 }
 
-uint32_t pdbm_getUpperFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets)
+uint32_t pdbm_getUpperFacets(PDBMPtr& pdbm, cindex_t dim, cindex_t* facets)
 {
     assert(pdbm && dim && facets);
 
@@ -1129,7 +1113,7 @@ uint32_t pdbm_getUpperFacets(PDBM& pdbm, cindex_t dim, cindex_t* facets)
     return cnt;
 }
 
-int32_t pdbm_getCostOfValuation(const PDBM pdbm, cindex_t dim, const int32_t* valuation)
+int32_t pdbm_getCostOfValuation(const PDBMPtr& pdbm, cindex_t dim, const int32_t* valuation)
 {
     assert(pdbm && dim && valuation);
     assert(pdbm_containsInt(pdbm, dim, valuation));
@@ -1142,7 +1126,7 @@ int32_t pdbm_getCostOfValuation(const PDBM pdbm, cindex_t dim, const int32_t* va
     return cost;
 }
 
-void pdbm_relax(PDBM& pdbm, cindex_t dim)
+void pdbm_relax(PDBMPtr& pdbm, cindex_t dim)
 {
     pdbm_prepare(pdbm, dim);
 
@@ -1156,7 +1140,7 @@ void pdbm_relax(PDBM& pdbm, cindex_t dim)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-bool pdbm_isValid(const PDBM pdbm, cindex_t dim)
+bool pdbm_isValid(const PDBMPtr& pdbm, cindex_t dim)
 {
     assert(dim);
 
@@ -1174,7 +1158,7 @@ bool pdbm_isValid(const PDBM pdbm, cindex_t dim)
            (!pdbm_isUnbounded(pdbm, dim) || pdbm_getSlopeOfDelayTrajectory(pdbm, dim) >= 0);
 }
 
-void pdbm_freeClock(PDBM& pdbm, cindex_t dim, cindex_t clock)
+void pdbm_freeClock(PDBMPtr& pdbm, cindex_t dim, cindex_t clock)
 {
     assert(pdbm && dim && clock > 0 && clock < dim);
     assert(pdbm_rates(pdbm)[clock] == 0);
@@ -1184,7 +1168,7 @@ void pdbm_freeClock(PDBM& pdbm, cindex_t dim, cindex_t clock)
     assertx(pdbm_isValid(pdbm, dim));
 }
 
-void pdbm_getOffset(const PDBM pdbm, cindex_t dim, int32_t* valuation)
+void pdbm_getOffset(const PDBMPtr& pdbm, cindex_t dim, int32_t* valuation)
 {
     assert(pdbm && dim && valuation);
 
@@ -1195,7 +1179,7 @@ void pdbm_getOffset(const PDBM pdbm, cindex_t dim, int32_t* valuation)
     }
 }
 
-void pdbm_setRate(PDBM& pdbm, cindex_t dim, cindex_t clock, int32_t rate)
+void pdbm_setRate(PDBMPtr& pdbm, cindex_t dim, cindex_t clock, int32_t rate)
 {
     assert(pdbm && dim && clock > 0 && clock < dim);
 
@@ -1204,7 +1188,7 @@ void pdbm_setRate(PDBM& pdbm, cindex_t dim, cindex_t clock, int32_t rate)
     pdbm_cache(pdbm) = INVALID;
 }
 
-raw_t* pdbm_getMutableMatrix(PDBM& pdbm, cindex_t dim)
+raw_t* pdbm_getMutableMatrix(PDBMPtr& pdbm, cindex_t dim)
 {
     assert(dim);
 
@@ -1212,33 +1196,32 @@ raw_t* pdbm_getMutableMatrix(PDBM& pdbm, cindex_t dim)
         pdbm_prepare(pdbm, dim);
     } else {
         pdbm = pdbm_allocate(dim);
-        pdbm_incRef(pdbm);
     }
     pdbm_cache(pdbm) = INVALID;
 
     return pdbm_matrix(pdbm, dim);
 }
 
-const raw_t* pdbm_getMatrix(const PDBM pdbm, cindex_t dim)
+const raw_t* pdbm_getMatrix(const PDBMPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
     return pdbm_matrix(pdbm, dim);
 }
 
-const int32_t* pdbm_getRates(const PDBM pdbm, cindex_t dim)
+const int32_t* pdbm_getRates(const PDBMCPtr& pdbm, cindex_t dim)
 {
     assert(pdbm && dim);
     return pdbm_rates(pdbm);
 }
 
-bool pdbm_constrainToFacet(PDBM& pdbm, cindex_t dim, cindex_t i, cindex_t j)
+bool pdbm_constrainToFacet(PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j)
 {
     auto dbm = pdbm_matrix(pdbm, dim);
     auto bound = -dbm.bound(i, j);
     return pdbm_constrain1(pdbm, dim, j, i, dbm_bound2raw(bound, dbm_WEAK));
 }
 
-void pdbm_print(FILE* f, const PDBM pdbm, cindex_t dim)
+void pdbm_print(FILE* f, const PDBMPtr& pdbm, cindex_t dim)
 {
     int32_t infimum = pdbm_getInfimum(pdbm, dim);
     dbm_print(f, pdbm_matrix(pdbm, dim), dim);
@@ -1250,7 +1233,7 @@ void pdbm_print(FILE* f, const PDBM pdbm, cindex_t dim)
     fprintf(f, "Offset: %d Infimum: %d\n", pdbm->cost, infimum);
 }
 
-std::ostream& pdbm_print(std::ostream& os, const PDBM pdbm, cindex_t dim)
+std::ostream& pdbm_print(std::ostream& os, const PDBMPtr& pdbm, cindex_t dim)
 {
     int32_t infimum = pdbm_getInfimum(pdbm, dim);
     dbm_cppPrint(os, pdbm_matrix(pdbm, dim));
@@ -1262,7 +1245,7 @@ std::ostream& pdbm_print(std::ostream& os, const PDBM pdbm, cindex_t dim)
     return os;
 }
 
-void pdbm_freeUp(PDBM& pdbm, cindex_t dim, cindex_t index)
+void pdbm_freeUp(PDBMPtr& pdbm, cindex_t dim, cindex_t index)
 {
     assert(pdbm_rates(pdbm)[index] >= 0);
 
@@ -1270,7 +1253,7 @@ void pdbm_freeUp(PDBM& pdbm, cindex_t dim, cindex_t index)
     dbm_freeUp(pdbm_matrix(pdbm, dim), dim, index);
 }
 
-void pdbm_freeDown(PDBM& pdbm, cindex_t dim, cindex_t index)
+void pdbm_freeDown(PDBMPtr& pdbm, cindex_t dim, cindex_t index)
 {
     assert(pdbm_rates(pdbm)[index] <= 0);
 
@@ -1289,7 +1272,7 @@ void pdbm_freeDown(PDBM& pdbm, cindex_t dim, cindex_t index)
     dbm_freeDown(dbm, dim, index);
 }
 
-void pdbm_normalise(PDBM pdbm, cindex_t dim)
+void pdbm_normalise(PDBMPtr& pdbm, cindex_t dim)
 {
     int32_t* rates = pdbm_rates(pdbm);
     std::vector<cindex_t> next(dim);
@@ -1315,7 +1298,7 @@ void pdbm_normalise(PDBM pdbm, cindex_t dim)
     }
 }
 
-bool pdbm_hasNormalForm(PDBM pdbm, cindex_t dim)
+bool pdbm_hasNormalForm(PDBMPtr& pdbm, cindex_t dim)
 {
     int32_t* rates = pdbm_rates(pdbm);
     std::vector<cindex_t> next(dim);

From 2c70b0adca38d3f042503f1b297bed5a67f0a359 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 13:47:41 +0200
Subject: [PATCH 03/15] Fixed formatting

---
 src/dbm.c                 | 10 +++++-----
 src/fed.cpp               | 12 ++++++------
 src/gen.c                 |  8 ++++----
 src/mingraph_cache.cpp    |  4 ++--
 src/partition.cpp         |  4 ++--
 test/test_ext.c           |  4 ++--
 test/test_extrapolation.c |  2 +-
 test/xdbm.c               |  2 +-
 test/xfed.c               |  2 +-
 9 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/src/dbm.c b/src/dbm.c
index 9b27a1e..bc4e975 100644
--- a/src/dbm.c
+++ b/src/dbm.c
@@ -31,11 +31,11 @@
 
 /* More readable code with this */
 
-#define DBM(I, J)  dbm[(I)*dim + (J)]
-#define SRC(I, J)  src[(I)*dim + (J)]
-#define DST(I, J)  dst[(I)*dim + (J)]
-#define DBM1(I, J) dbm1[(I)*dim + (J)]
-#define DBM2(I, J) dbm2[(I)*dim + (J)]
+#define DBM(I, J)  dbm[(I) * dim + (J)]
+#define SRC(I, J)  src[(I) * dim + (J)]
+#define DST(I, J)  dst[(I) * dim + (J)]
+#define DBM1(I, J) dbm1[(I) * dim + (J)]
+#define DBM2(I, J) dbm2[(I) * dim + (J)]
 
 /** For debugging */
 
diff --git a/src/fed.cpp b/src/fed.cpp
index 7d7d5a1..f6e03af 100644
--- a/src/fed.cpp
+++ b/src/fed.cpp
@@ -38,7 +38,7 @@
 #define IMPROVED_MERGE
 
 // Shouldn't be necessary in practice.
-//#define PARTITION_FIXPOINT
+// #define PARTITION_FIXPOINT
 
 // Variants for subtractions:
 // - desactive disjoint: #define NDISJOINT_SUBTRACTION
@@ -48,11 +48,11 @@
 //         x=2 => reordering of constraints
 //         x=3 => reordering of constraints + skip intersecting facettes
 
-//#define NDISJOINT_SUBTRACTION
-//#define SUBTRACTION_ALGORITHM 0
-//#define SUBTRACTION_ALGORITHM 1
-//#define SUBTRACTION_ALGORITHM 2
-//#define SUBTRACTION_ALGORITHM 3
+// #define NDISJOINT_SUBTRACTION
+// #define SUBTRACTION_ALGORITHM 0
+// #define SUBTRACTION_ALGORITHM 1
+// #define SUBTRACTION_ALGORITHM 2
+// #define SUBTRACTION_ALGORITHM 3
 
 // Default subtraction.
 #ifndef SUBTRACTION_ALGORITHM
diff --git a/src/gen.c b/src/gen.c
index f3134b8..d9eabdf 100644
--- a/src/gen.c
+++ b/src/gen.c
@@ -25,10 +25,10 @@
 #include <stdlib.h>
 
 /* For easy reading */
-#define DBM(I, J) dbm[(I)*dim + (J)]
-#define SRC(I, J) src[(I)*dim + (J)]
-#define DST(I, J) dst[(I)*dim + (J)]
-#define ARG(I, J) arg[(I)*dim + (J)]
+#define DBM(I, J) dbm[(I) * dim + (J)]
+#define SRC(I, J) src[(I) * dim + (J)]
+#define DST(I, J) dst[(I) * dim + (J)]
+#define ARG(I, J) arg[(I) * dim + (J)]
 
 /* For debugging */
 
diff --git a/src/mingraph_cache.cpp b/src/mingraph_cache.cpp
index 9d1ebbf..a208377 100644
--- a/src/mingraph_cache.cpp
+++ b/src/mingraph_cache.cpp
@@ -49,7 +49,7 @@ class Cache
     {
         // cleanup properly even if it is just one instance
         for (uint32_t i = 0; i < MINGRAPH_CACHE_SIZE; ++i) {
-            delete[](uint32_t*) entries[i];
+            delete[] (uint32_t*)entries[i];
         }
     }
 
@@ -86,7 +86,7 @@ void mingraph_putCachedResult(const raw_t* dbm, cindex_t dim, const uint32_t* bi
     uint32_t dim2 = dim * dim;
     cache_t* entry = cache.get(hashValue);
     if (!entry || entry->dim != dim) {
-        delete[](uint32_t*) entry;
+        delete[] (uint32_t*)entry;
         entry = (cache_t*)new uint32_t[intsizeof(cache_t) + dim2 + bits2intsize(dim2)];
     }
     entry->hashValue = hashValue;
diff --git a/src/partition.cpp b/src/partition.cpp
index 2f6b1fe..fb6d62a 100644
--- a/src/partition.cpp
+++ b/src/partition.cpp
@@ -99,7 +99,7 @@ namespace dbm
 
         all.nil();
         // allocate as char*, deallocate as char*
-        delete[]((char*)this);
+        delete[] ((char*)this);
     }
 
     fed_t partition_t::fedtable_t::get(uint32_t id) const
@@ -194,7 +194,7 @@ namespace dbm
             }
 
         all.nil();
-        delete[]((char*)this);
+        delete[] ((char*)this);
         return ftab;
     }
 
diff --git a/test/test_ext.c b/test/test_ext.c
index dc68387..49d73be 100644
--- a/test/test_ext.c
+++ b/test/test_ext.c
@@ -29,8 +29,8 @@
 
 /* make the code more readable
  */
-#define DBM1(I, J) dbm1[(I)*dim1 + (J)]
-#define DBM2(I, J) dbm2[(I)*dim2 + (J)]
+#define DBM1(I, J) dbm1[(I) * dim1 + (J)]
+#define DBM2(I, J) dbm2[(I) * dim2 + (J)]
 
 /* progress spinning bar
  */
diff --git a/test/test_extrapolation.c b/test/test_extrapolation.c
index fea462d..acc56ed 100644
--- a/test/test_extrapolation.c
+++ b/test/test_extrapolation.c
@@ -58,7 +58,7 @@
 #define PROGRESS() debug_spin(stderr)
 
 /* For more readable code */
-#define DBM(I, J) dbm[(I)*dim + (J)]
+#define DBM(I, J) dbm[(I) * dim + (J)]
 
 /* Alternative simple implementations */
 
diff --git a/test/xdbm.c b/test/xdbm.c
index 18cb008..0b188c8 100644
--- a/test/xdbm.c
+++ b/test/xdbm.c
@@ -11,7 +11,7 @@
 #define WIDTH     800
 #define HEIGHT    800
 #define MARGIN    10
-#define DBM(I, J) dbm[(I)*dim + (J)]
+#define DBM(I, J) dbm[(I) * dim + (J)]
 
 typedef struct
 {
diff --git a/test/xfed.c b/test/xfed.c
index 8895a55..b9d9cdf 100644
--- a/test/xfed.c
+++ b/test/xfed.c
@@ -93,7 +93,7 @@ raw_t hull[16];
 #define WIDTH     800
 #define HEIGHT    800
 #define MARGIN    12
-#define DBM(I, J) dbm[(I)*dim + (J)]
+#define DBM(I, J) dbm[(I) * dim + (J)]
 
 typedef struct
 {

From 2f59ada8b735dadd21799c8d660526253f11e952 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 15:34:21 +0200
Subject: [PATCH 04/15] Added interator include for AppleClang

---
 src/fed.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/fed.cpp b/src/fed.cpp
index f6e03af..9f23990 100644
--- a/src/fed.cpp
+++ b/src/fed.cpp
@@ -24,6 +24,7 @@
 
 #include <algorithm>  // find_if
 #include <forward_list>
+#include <iterator>  // front_inserter
 #include <sstream>
 #include <cmath>
 

From 447252edacb046320349d27d15ef3411901040bc Mon Sep 17 00:00:00 2001
From: Marius Mikucionis <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 15:47:44 +0200
Subject: [PATCH 05/15] Fixed std::fill with include algorithm

---
 include/dbm/valuation.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/include/dbm/valuation.h b/include/dbm/valuation.h
index 0a5563e..b5fef86 100644
--- a/include/dbm/valuation.h
+++ b/include/dbm/valuation.h
@@ -19,7 +19,7 @@
 #include "dbm/ClockAccessor.h"
 
 #include <iosfwd>
-#include <limits>
+#include <algorithm>
 #include <vector>
 #include <cassert>
 

From 6283ef8ccf8ee17acf936a785cfb0ec2b787a754 Mon Sep 17 00:00:00 2001
From: Marius Mikucionis <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 16:05:45 +0200
Subject: [PATCH 06/15] Cleaned the build system for macOS

---
 cmake/UUtils.cmake                            |  2 +
 cmake/boost.cmake                             | 58 ++++++++++++++
 ...ew-gcc14.cmake => darwin-brew-gcc14.cmake} |  0
 .../{x86_64-darwin.cmake => darwin.cmake}     |  0
 compile.sh                                    |  8 +-
 getlibs.sh                                    | 77 ++++++++++++++++---
 6 files changed, 133 insertions(+), 12 deletions(-)
 create mode 100644 cmake/boost.cmake
 rename cmake/toolchain/{x86_64-darwin-brew-gcc14.cmake => darwin-brew-gcc14.cmake} (100%)
 rename cmake/toolchain/{x86_64-darwin.cmake => darwin.cmake} (100%)

diff --git a/cmake/UUtils.cmake b/cmake/UUtils.cmake
index c9379b5..3e39df0 100644
--- a/cmake/UUtils.cmake
+++ b/cmake/UUtils.cmake
@@ -1,3 +1,5 @@
+set(BOOST_INCLUDE_LIBRARIES math)
+include(cmake/boost.cmake)
 find_package(UUtils 2.0.5 COMPONENTS base hash debug QUIET)
 
 if (UUtils_FOUND)
diff --git a/cmake/boost.cmake b/cmake/boost.cmake
new file mode 100644
index 0000000..162ecd4
--- /dev/null
+++ b/cmake/boost.cmake
@@ -0,0 +1,58 @@
+# set BOOST_INCLUDE_LIBRARIES to include specific libraries before including this script, e.g.
+# set(BOOST_INCLUDE_LIBRARIES program_options threads)
+set(Boost_NO_SYSTEM_PATHS TRUE)
+set(Boost_USE_STATIC_LIBS    ON)  # only find static libs
+set(Boost_USE_DEBUG_LIBS     OFF) # ignore debug libs and
+set(Boost_USE_RELEASE_LIBS   ON)  # only find release libs
+set(Boost_USE_STATIC_RUNTIME ON) # Mac insists on ON for boost_program_options
+#set(BOOST_USE_MULTITHREADED ON)
+#set(Boost_DEBUG ON)
+set(Boost_VERSION 1.86.0)
+
+if (BOOST_INCLUDE_LIBRARIES)
+  find_package(Boost ${Boost_VERSION} COMPONENTS ${BOOST_INCLUDE_LIBRARIES} QUIET PATHS /usr)
+else(BOOST_INCLUDE_LIBRARIES)
+  find_package(Boost ${Boost_VERSION} QUIET PATHS /usr)
+endif(BOOST_INCLUDE_LIBRARIES)
+
+if (Boost_FOUND)
+  message(STATUS "Found Boost: ${Boost_DIR}")
+else(Boost_FOUND)
+  message(STATUS "Failed to find Boost (${BOOST_INCLUDE_LIBRARIES}), going to compile from source")
+  if (FIND_FATAL)
+    message(FATAL_ERROR "Failed to find Boost with CMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH}")
+  endif(FIND_FATAL)
+  set(BOOST_ENABLE_CMAKE ON)
+  FetchContent_Declare(
+    Boost
+    DOWNLOAD_EXTRACT_TIMESTAMP ON
+    #FIND_PACKAGE_ARGS NAMES Boost COMPONENTS ${BOOST_INCLUDE_LIBRARIES}
+    URL https://github.com/boostorg/boost/releases/download/boost-1.83.0/boost-1.83.0.tar.xz
+    URL_HASH SHA256=c5a0688e1f0c05f354bbd0b32244d36085d9ffc9f932e8a18983a9908096f614
+    # GIT_REPOSITORY https://github.com/boostorg/boost.git
+    # GIT_TAG boost-${Boost_VERSION}
+    # GIT_SHALLOW TRUE # get only the last commit version
+    # GIT_PROGRESS TRUE # show progress of download
+    USES_TERMINAL_DOWNLOAD TRUE # show progress in ninja generator
+    USES_TERMINAL_CONFIGURE ON
+    USES_TERMINAL_BUILD ON
+    USES_TERMINAL_INSTALL ON
+    )
+  FetchContent_GetProperties(Boost)
+  if (Boost_POPULATED)
+    message(STATUS "Found populated Boost (${BOOST_INCLUDE_LIBRARIES}): ${boost_SOURCE_DIR}")
+  else (Boost_POPULATED)
+    FetchContent_Populate(Boost)
+    add_subdirectory(${boost_SOURCE_DIR} ${boost_BINARY_DIR} EXCLUDE_FROM_ALL)
+    # workaround for cmake complaint that boost is not among exports:
+    install(TARGETS boost_headers boost_math boost_assert boost_concept_check boost_config boost_core
+            boost_integer boost_lexical_cast boost_predef boost_random boost_static_assert boost_throw_exception
+            boost_preprocessor boost_type_traits boost_array boost_container boost_numeric_conversion boost_range
+            boost_dynamic_bitset boost_io boost_system boost_utility boost_intrusive boost_move boost_conversion
+            boost_mpl boost_container_hash boost_detail boost_iterator boost_optional boost_regex boost_tuple
+            boost_variant2 boost_winapi boost_smart_ptr boost_typeof boost_describe boost_mp11 boost_function_types
+            boost_fusion boost_functional boost_function boost_bind
+            EXPORT UUtilsConfig DESTINATION ${CMAKE_INSTALL_LIBDIR})
+    message(STATUS "Got Boost (${BOOST_INCLUDE_LIBRARIES}): ${boost_SOURCE_DIR}")
+  endif(Boost_POPULATED)
+endif(Boost_FOUND)
diff --git a/cmake/toolchain/x86_64-darwin-brew-gcc14.cmake b/cmake/toolchain/darwin-brew-gcc14.cmake
similarity index 100%
rename from cmake/toolchain/x86_64-darwin-brew-gcc14.cmake
rename to cmake/toolchain/darwin-brew-gcc14.cmake
diff --git a/cmake/toolchain/x86_64-darwin.cmake b/cmake/toolchain/darwin.cmake
similarity index 100%
rename from cmake/toolchain/x86_64-darwin.cmake
rename to cmake/toolchain/darwin.cmake
diff --git a/compile.sh b/compile.sh
index 48e8d35..7d600ae 100755
--- a/compile.sh
+++ b/compile.sh
@@ -31,6 +31,12 @@ for target in $targets ; do
         win32*|i686-w64-mingw32*)
             PLATFORM=i686-w64-mingw32
             ;;
+        darwin-brew-gcc14*)
+            PLATFORM=darwin-brew-gcc14
+            ;;
+        darwin*)
+            PLATFORM=darwin
+            ;;
         x86_64-darwin-brew-gcc14*)
             PLATFORM=x86_64-darwin-brew-gcc14
             ;;
@@ -45,7 +51,7 @@ for target in $targets ; do
     BUILD_DIR="build-$PLATFORM"
 
     case $target in
-        *-lib*)
+        *-libs*)
             CMAKE_BUILD_TYPE=Release ./getlibs.sh $PLATFORM
             BUILD_EXTRA="$BUILD_EXTRA -DFIND_FATAL=ON"
             export CMAKE_PREFIX_PATH="$PROJECT_DIR/local/$PLATFORM"
diff --git a/getlibs.sh b/getlibs.sh
index feab846..e42e271 100755
--- a/getlibs.sh
+++ b/getlibs.sh
@@ -29,12 +29,75 @@ elif [ "$CMAKE_BUILD_TYPE" != Release ]; then
     echo "WARNING: building libs with CMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE"
 fi
 
+function show_cmake_vars() {
+    for var in CMAKE_TOOLCHAIN_FILE CMAKE_BUILD_TYPE CMAKE_PREFIX_PATH CMAKE_INSTALL_PREFIX \
+               CMAKE_GENERATOR CMAKE_BUILD_PARALLEL_LEVEL; do
+        echo "  $var=${!var:- (unset)}"
+    done
+}
+
 for target in $targets ; do
     PREFIX="$PROJECT_DIR/local/$target"
     export CMAKE_TOOLCHAIN_FILE="$PROJECT_DIR/cmake/toolchain/$target.cmake"
     export CMAKE_PREFIX_PATH="$PREFIX"
     export CMAKE_INSTALL_PREFIX="$PREFIX"
 
+    ## XXHASH for UUtils
+    NAME=xxHash
+    VERSION=0.8.3
+    LIBRARY="${NAME}-${VERSION}"
+    ARCHIVE="$LIBRARY.tgz"
+    SHA256=aae608dfe8213dfd05d909a57718ef82f30722c392344583d3f39050c7f29a80
+    SOURCE="${SOURCES}/$LIBRARY"
+    BUILD="${PREFIX}/build-$LIBRARY"
+    if [ -r "${CMAKE_INSTALL_PREFIX}/include/xxhash.h" ]; then
+        echo "$LIBRARY is already installed in $CMAKE_INSTALL_PREFIX"
+    else
+        pushd "$SOURCES"
+        [ -r "${ARCHIVE}" ] || curl -sL "https://github.com/Cyan4973/xxHash/archive/refs/tags/v$VERSION.tar.gz" -o "${ARCHIVE}"
+        if [ -n "$(command -v shasum)" ]; then
+            echo "$SHA256  $ARCHIVE" | shasum -a256 --check -
+        fi
+        [ -d "$SOURCE" ] || tar xf "${ARCHIVE}"
+        popd
+        echo "Building $LIBRARY in $BUILD from $SOURCE"
+        show_cmake_vars
+        cmake -S "$SOURCE/cmake_unofficial" -B "$BUILD" -DBUILD_SHARED_LIBS=OFF
+        cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
+        cmake --install "$BUILD" --config $CMAKE_BUILD_TYPE --prefix "${CMAKE_INSTALL_PREFIX}"
+        rm -Rf "$BUILD"
+        rm -Rf "$SOURCE"
+    fi
+
+    ## BOOST for UUtils
+    NAME=boost
+    VERSION=1.88.0
+    LIBRARY="${NAME}-${VERSION}"
+    ARCHIVE="${LIBRARY}-cmake.tar.xz"
+    SHA256=f48b48390380cfb94a629872346e3a81370dc498896f16019ade727ab72eb1ec
+    SOURCE="${SOURCES}/${LIBRARY}"
+    BUILD="${PREFIX}/build-${LIBRARY}"
+    if [ -r "${CMAKE_INSTALL_PREFIX}/include/boost/math/distributions/arcsine.hpp" ] ; then
+        echo "$LIBRARY is already installed in $CMAKE_INSTALL_PREFIX"
+    else
+        pushd "$SOURCES"
+        [ -r "${ARCHIVE}" ] || curl -sL "https://github.com/boostorg/boost/releases/download/${LIBRARY}/${ARCHIVE}" -o "${ARCHIVE}"
+        if [ -n "$(command -v shasum)" ]; then
+            echo "$SHA256  $ARCHIVE" | shasum -a256 --check -
+        fi
+        [ -d "${SOURCE}" ] || tar xf "${ARCHIVE}"
+        popd
+        echo "Building $LIBRARY in $BUILD from $SOURCE"
+        show_cmake_vars
+        cmake -S "$SOURCE" -B "$BUILD" -DBUILD_SHARED_LIBS=OFF \
+          -DBOOST_INCLUDE_LIBRARIES="headers;math" -DBOOST_ENABLE_MPI=OFF -DBOOST_ENABLE_PYTHON=OFF \
+          -DBOOST_RUNTIME_LINK=static -DBUILD_TESTING=OFF -DBOOST_INSTALL_LAYOUT=system
+        cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
+        cmake --install "$BUILD" --config $CMAKE_BUILD_TYPE --prefix "${CMAKE_INSTALL_PREFIX}"
+        rm -Rf "$BUILD"
+        rm -Rf "$SOURCE"
+    fi
+
     # doctest for unit testing
     NAME=doctest
     VERSION=2.4.11
@@ -52,12 +115,8 @@ for target in $targets ; do
       [ -d "$SOURCE" ] || tar -xf "$ARCHIVE"
       popd
       echo "Building $LIBRARY in $BUILD"
-      echo "  CMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE"
-      echo "  CMAKE_TOOLCHAIN_FILE=$CMAKE_TOOLCHAIN_FILE"
-      echo "  CMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH"
-      echo "  CMAKE_INSTALL_PREFIX=$CMAKE_INSTALL_PREFIX"
-      echo "  CMAKE_GENERATOR=$CMAKE_GENERATOR"
-      cmake  -S "$SOURCE" -B "$BUILD" -DDOCTEST_WITH_TESTS=OFF \
+      show_cmake_vars
+      cmake -S "$SOURCE" -B "$BUILD" -DDOCTEST_WITH_TESTS=OFF \
            -DDOCTEST_WITH_MAIN_IN_STATIC_LIB=ON -DDOCTEST_USE_STD_HEADERS=OFF
       cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
       cmake --install "$BUILD" --config $CMAKE_BUILD_TYPE --prefix "$CMAKE_INSTALL_PREFIX"
@@ -83,11 +142,7 @@ for target in $targets ; do
       [ -d "$SOURCE" ] || tar -xf "$ARCHIVE"
       popd
       echo "Building $LIBRARY in $BUILD"
-      echo "  CMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE"
-      echo "  CMAKE_TOOLCHAIN_FILE=$CMAKE_TOOLCHAIN_FILE"
-      echo "  CMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH"
-      echo "  CMAKE_INSTALL_PREFIX=$CMAKE_INSTALL_PREFIX"
-      echo "  CMAKE_GENERATOR=$CMAKE_GENERATOR"
+      show_cmake_vars
       cmake -S "$SOURCE" -B "$BUILD" -DUUtils_WITH_TESTS=OFF -DUUtils_WITH_BENCHMARKS=OFF
       cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
       cmake --install "$BUILD" --config $CMAKE_BUILD_TYPE --prefix="$CMAKE_INSTALL_PREFIX"

From 54e36ce0a5c6e06fca3ee1f35440bc6914243810 Mon Sep 17 00:00:00 2001
From: Marius Mikucionis <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 16:07:01 +0200
Subject: [PATCH 07/15] Fixed the missing include

---
 src/valuation.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/valuation.cpp b/src/valuation.cpp
index c0a8058..fc5eac2 100644
--- a/src/valuation.cpp
+++ b/src/valuation.cpp
@@ -11,6 +11,7 @@
 
 #include <iomanip>
 #include <sstream>
+#include <limits>
 
 namespace dbm
 {

From ecfdee8a9c790b11bf70a9b1b63b49bc589f4c1a Mon Sep 17 00:00:00 2001
From: Marius Mikucionis <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 16:25:45 +0200
Subject: [PATCH 08/15] Attempt to fix CMake scripts for automatic fetching of
 libraries

---
 CMakeLists.txt      |  2 +-
 cmake/UUtils.cmake  |  8 +++++---
 cmake/boost.cmake   | 12 ++++++------
 cmake/doctest.cmake |  2 +-
 cmake/xxhash.cmake  |  2 +-
 5 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2c13597..de91187 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.16)
+cmake_minimum_required(VERSION 3.30)
 project(UDBM VERSION 2.0.15 LANGUAGES CXX C)
 include(CMakePackageConfigHelpers)
 include(GNUInstallDirs)
diff --git a/cmake/UUtils.cmake b/cmake/UUtils.cmake
index 3e39df0..97b7b86 100644
--- a/cmake/UUtils.cmake
+++ b/cmake/UUtils.cmake
@@ -1,6 +1,8 @@
 set(BOOST_INCLUDE_LIBRARIES math)
 include(cmake/boost.cmake)
-find_package(UUtils 2.0.5 COMPONENTS base hash debug QUIET)
+include(cmake/xxhash.cmake)
+
+find_package(UUtils 2.0.7 COMPONENTS base hash debug QUIET)
 
 if (UUtils_FOUND)
   message(STATUS "Found UUtils: ${UUtils_DIR}")
@@ -15,7 +17,7 @@ else(UUtils_FOUND)
     FetchContent_Declare(
             UUtils
             GIT_REPOSITORY https://github.com/UPPAALModelChecker/UUtils.git
-            GIT_TAG v2.0.5
+            GIT_TAG v2.0.7
             GIT_SHALLOW TRUE # get only the last commit version
             GIT_PROGRESS TRUE # show progress of download
             # FIND_PACKAGE_ARGS NAMES doctest
@@ -24,7 +26,7 @@ else(UUtils_FOUND)
             USES_TERMINAL_BUILD ON
             USES_TERMINAL_INSTALL ON
     )
-    FetchContent_GetProperties(UUtils)
+    FetchContent_MakeAvailable(UUtils)
     if (uutils_POPULATED)
         message(STATUS "Found populated UUtils: ${uutils_SOURCE_DIR}")
     else (uutils_POPULATED)
diff --git a/cmake/boost.cmake b/cmake/boost.cmake
index 162ecd4..ce7d4df 100644
--- a/cmake/boost.cmake
+++ b/cmake/boost.cmake
@@ -10,9 +10,9 @@ set(Boost_USE_STATIC_RUNTIME ON) # Mac insists on ON for boost_program_options
 set(Boost_VERSION 1.86.0)
 
 if (BOOST_INCLUDE_LIBRARIES)
-  find_package(Boost ${Boost_VERSION} COMPONENTS ${BOOST_INCLUDE_LIBRARIES} QUIET PATHS /usr)
+  find_package(Boost ${Boost_VERSION} COMPONENTS ${BOOST_INCLUDE_LIBRARIES} QUIET)
 else(BOOST_INCLUDE_LIBRARIES)
-  find_package(Boost ${Boost_VERSION} QUIET PATHS /usr)
+  find_package(Boost ${Boost_VERSION} QUIET)
 endif(BOOST_INCLUDE_LIBRARIES)
 
 if (Boost_FOUND)
@@ -27,8 +27,8 @@ else(Boost_FOUND)
     Boost
     DOWNLOAD_EXTRACT_TIMESTAMP ON
     #FIND_PACKAGE_ARGS NAMES Boost COMPONENTS ${BOOST_INCLUDE_LIBRARIES}
-    URL https://github.com/boostorg/boost/releases/download/boost-1.83.0/boost-1.83.0.tar.xz
-    URL_HASH SHA256=c5a0688e1f0c05f354bbd0b32244d36085d9ffc9f932e8a18983a9908096f614
+    URL https://github.com/boostorg/boost/releases/download/boost-1.88.0/boost-1.88.0-cmake.tar.xz
+    URL_HASH SHA256=f48b48390380cfb94a629872346e3a81370dc498896f16019ade727ab72eb1ec
     # GIT_REPOSITORY https://github.com/boostorg/boost.git
     # GIT_TAG boost-${Boost_VERSION}
     # GIT_SHALLOW TRUE # get only the last commit version
@@ -38,11 +38,11 @@ else(Boost_FOUND)
     USES_TERMINAL_BUILD ON
     USES_TERMINAL_INSTALL ON
     )
-  FetchContent_GetProperties(Boost)
+  FetchContent_MakeAvailable(Boost)
   if (Boost_POPULATED)
     message(STATUS "Found populated Boost (${BOOST_INCLUDE_LIBRARIES}): ${boost_SOURCE_DIR}")
   else (Boost_POPULATED)
-    FetchContent_Populate(Boost)
+    FetchContent_MakeAvailable(Boost)
     add_subdirectory(${boost_SOURCE_DIR} ${boost_BINARY_DIR} EXCLUDE_FROM_ALL)
     # workaround for cmake complaint that boost is not among exports:
     install(TARGETS boost_headers boost_math boost_assert boost_concept_check boost_config boost_core
diff --git a/cmake/doctest.cmake b/cmake/doctest.cmake
index 24e7f0a..acbd69a 100644
--- a/cmake/doctest.cmake
+++ b/cmake/doctest.cmake
@@ -34,7 +34,7 @@ else(doctest_FOUND)
             USES_TERMINAL_BUILD ON
             USES_TERMINAL_INSTALL ON
     )
-    FetchContent_GetProperties(doctest)
+    FetchContent_MakeAvailable(doctest)
     if (doctest_POPULATED)
         message(STATUS "Found populated doctest: ${doctest_SOURCE_DIR}")
     else (doctest_POPULATED)
diff --git a/cmake/xxhash.cmake b/cmake/xxhash.cmake
index f577755..79516b5 100644
--- a/cmake/xxhash.cmake
+++ b/cmake/xxhash.cmake
@@ -51,7 +51,7 @@ else(xxHash_FOUND)
     USES_TERMINAL_BUILD ON
     USES_TERMINAL_INSTALL ON
     )
-  FetchContent_GetProperties(xxHash)
+  FetchContent_MakeAvailable(xxHash)
   if (xxhash_POPULATED)
     message(STATUS "Found populated xxHash: ${xxhash_SOURCE_DIR}")
   else (xxhash_POPULATED)

From 3a1f190a778cffdb182db86f1df80d93f981fc76 Mon Sep 17 00:00:00 2001
From: Marius Mikucionis <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 16:33:45 +0200
Subject: [PATCH 09/15] Attempting to fix GH action script

---
 .github/workflows/build.yml | 36 +++++++++++++++++-------------------
 1 file changed, 17 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index dd61aba..4865dc1 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -46,21 +46,21 @@ jobs:
       - name: Build without getlibs
         run: |
           BUILD="build-${{ matrix.target }}-${CMAKE_BUILD_TYPE,,}"
-          cmake -S . -B "$BUILD" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
+          cmake -B "$BUILD" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          (cd "$BUILD" ; ctest -C $CMAKE_BUILD_TYPE)
+          ctest --build "$BUILD" -C $CMAKE_BUILD_TYPE)
       - name: Getlibs
         run: ./getlibs.sh ${{ matrix.target }}
       - name: Build with getlibs
         run: |
           BUILD="build-${{ matrix.target }}-libs-${CMAKE_BUILD_TYPE,,}"          
-          cmake -S . -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/${{ matrix.target }}" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
+          cmake -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/${{ matrix.target }}" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          (cd "$BUILD" ; ctest -C $CMAKE_BUILD_TYPE)
-  build-macos:
+          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE
+  build-darwin:
     runs-on: macos-latest
     env:
-      CMAKE_TOOLCHAIN_FILE: ${{ github.workspace }}/cmake/toolchain/x86_64-darwin.cmake
+      CMAKE_TOOLCHAIN_FILE: ${{ github.workspace }}/cmake/toolchain/darwin.cmake
       CMAKE_BUILD_TYPE: Release
       CTEST_OUTPUT_ON_FAILURE: 1
       CTEST_TEST_TIMEOUT: 20
@@ -73,18 +73,18 @@ jobs:
       - uses: actions/checkout@v3
       - name: Build without getlibs
         run: |
-          BUILD=build-x86_64-darwin-$CMAKE_BUILD_TYPE
-          cmake -S . -B "$BUILD" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
+          BUILD=build-darwin-$CMAKE_BUILD_TYPE
+          cmake -B "$BUILD" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          (cd "$BUILD" ; ctest -C $CMAKE_BUILD_TYPE)
+          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
       - name: Get dependencies
-        run: CMAKE_BUILD_TYPE=Release ./getlibs.sh x86_64-darwin
+        run: CMAKE_BUILD_TYPE=Release ./getlibs.sh darwin
       - name: Build with getlibs
         run: |
-          BUILD=build-x86_64-darwin-libs-$CMAKE_BUILD_TYPE
-          cmake -S . -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/x86_64-darwin" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
+          BUILD=build-darwin-libs-$CMAKE_BUILD_TYPE
+          cmake -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/darwin" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          (cd "$BUILD" ; ctest -C $CMAKE_BUILD_TYPE)
+          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
   build-windows:
     runs-on: windows-latest
     env:
@@ -98,10 +98,9 @@ jobs:
       - name: Build without getlibs
         run: |
           $env:BUILD='build-x86_64-windows'
-          cmake -S . -B $env:BUILD
+          cmake -B $env:BUILD
           cmake --build $env:BUILD --config $env:CMAKE_BUILD_TYPE
-          cd $env:BUILD
-          ctest -C $env:CMAKE_BUILD_TYPE
+          ctest --test-dir $env:BUILD -C $env:CMAKE_BUILD_TYPE
       - name: Get dependencies
         run: |
           vcpkg integrate install
@@ -110,7 +109,6 @@ jobs:
       - name: Build with getlibs
         run: |
           $env:BUILD='build-x86_64-windows-libs'
-          cmake -S . -B $env:BUILD -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/x86_64-w64-mingw32"
+          cmake -B $env:BUILD -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/x86_64-w64-mingw32"
           cmake --build $env:BUILD --config $env:CMAKE_BUILD_TYPE
-          cd $env:BUILD
-          ctest -C $env:CMAKE_BUILD_TYPE
+          ctest --test-dir $env:BUILD -C $env:CMAKE_BUILD_TYPE

From 410f4821591341a1547cf88cdba1e9660b62886b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 16:55:50 +0200
Subject: [PATCH 10/15] Added an option to disable clang-tidy (broken due to
 unrecognized GCC specific options added by CMake)

---
 CMakeLists.txt | 5 ++++-
 compile.sh     | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index de91187..03513d4 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -5,6 +5,7 @@ include(GNUInstallDirs)
 
 option(UDBM_WITH_TESTS "UDBM Unit tests" ON)
 option(UDBM_STATIC "Static linking" OFF)
+option(UDBM_CLANG_TIDY "Linting with clang-tidy" ON)
 option(FIND_FATAL "Stop upon find_package errors" OFF)
 
 cmake_policy(SET CMP0048 NEW) # project() command manages VERSION variables
@@ -18,7 +19,9 @@ set(ENABLE_STORE_MINGRAPH 1)
 CONFIGURE_FILE("src/config.h.cmake" "include/dbm/config.h")
 
 include(cmake/sanitizer.cmake)
-include(cmake/clang-tidy.cmake)
+if (UDBM_CLANG_TIDY)
+  include(cmake/clang-tidy.cmake)
+endif(UDBM_CLANG_TIDY)
 if (UDBM_WITH_TESTS)
     include(cmake/doctest.cmake)
 endif (UDBM_WITH_TESTS)
diff --git a/compile.sh b/compile.sh
index 7d600ae..57eecbf 100755
--- a/compile.sh
+++ b/compile.sh
@@ -94,7 +94,7 @@ for target in $targets ; do
     echo "  CMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE"
     echo "  CMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH"
     echo "  CMAKE_TOOLCHAIN_FILE=$CMAKE_TOOLCHAIN_FILE"
-    cmake -S "$PROJECT_DIR" -B "$BUILD_DIR" $BUILD_EXTRA
+    cmake -S "$PROJECT_DIR" -B "$BUILD_DIR" -DUDBM_CLANG_TIDY=OFF $BUILD_EXTRA
     cmake --build "$BUILD_DIR" --config $CMAKE_BUILD_TYPE
     (cd "$BUILD_DIR" ; ctest -C $CMAKE_BUILD_TYPE --output-on-failure)
 done

From 7a89fb09eba388f269d8d42b815555eaad18e5ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 17:12:22 +0200
Subject: [PATCH 11/15] Moved clang-tidy options to .clang-tidy file

---
 .clang-tidy            | 3 +++
 cmake/clang-tidy.cmake | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)
 create mode 100644 .clang-tidy

diff --git a/.clang-tidy b/.clang-tidy
new file mode 100644
index 0000000..9172d87
--- /dev/null
+++ b/.clang-tidy
@@ -0,0 +1,3 @@
+---
+Checks: '-*,cppcoreguidelines-macro-usage,hicpp-deprecated-headers,modernize-deprecated-headers,hicpp-use-override,hicpp-use-emplace,modernize-use-emplace,hicpp-use-auto,readability-container-size-empty,readability-implicit-bool-conversion,readability-redundant-smartptr-get,readability-qualified-auto,performance-unnecessary-value-param,modernize-make-unique,modernize-make-shared,misc-unused-using-decls,performance-move-const-arg,modernize-use-using,modernize-use-nullptr,modernize-deprecated-headers,modernize-loop-convert,misc-unused-using-decls,misc-static-assert,misc-redundant-expression,modernize-use-bool-literals,readability-delete-null-pointer,readability-redundant-member-init'
+SystemHeaders: false
diff --git a/cmake/clang-tidy.cmake b/cmake/clang-tidy.cmake
index 83792e8..27705a7 100644
--- a/cmake/clang-tidy.cmake
+++ b/cmake/clang-tidy.cmake
@@ -10,8 +10,8 @@ if(CLANG_TIDY_PROGRAM)
     if (TIDY_MAJOR_VERSION GREATER_EQUAL 14)
         # Add good checks which produce a minimal amount of false positives
         # One or two false positives can be dealt with using // NOLINT
-        set(CLANG_TIDY_COMMAND ${CLANG_TIDY_PROGRAM} -checks=-*,cppcoreguidelines-macro-usage,hicpp-deprecated-headers,modernize-deprecated-headers,hicpp-use-override,hicpp-use-emplace,modernize-use-emplace,hicpp-use-auto,readability-container-size-empty,readability-implicit-bool-conversion,readability-redundant-smartptr-get,readability-qualified-auto,performance-unnecessary-value-param,modernize-make-unique,modernize-make-shared,misc-unused-using-decls,performance-move-const-arg,modernize-use-using,modernize-use-nullptr,modernize-deprecated-headers,modernize-loop-convert,misc-unused-using-decls,misc-static-assert,misc-redundant-expression,modernize-use-bool-literals,readability-delete-null-pointer,readability-redundant-member-init)
-        message(STATUS "Enabled clang-tidy ${TIDY_VERSION}: ${CLANG_TIDY_PROGRAM}")
+        set(CLANG_TIDY_COMMAND ${CLANG_TIDY_PROGRAM})
+        message(STATUS "Enabled clang-tidy ${TIDY_VERSION}: ${CLANG_TIDY_PROGRAM} --config-file=${CMAKE_SOURCE_DIR}/.clang-tidy")
     else()
         message(WARNING "Found clang-tidy ${TIDY_VERSION}, but >=14 is required, thus disabled.")
     endif()

From 795ac451bfe05e3f84fa158912848b7a30ceea6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 17:13:15 +0200
Subject: [PATCH 12/15] Disabled GH action for building without getlibs

---
 .github/workflows/build.yml | 38 ++++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 4865dc1..ce2bb60 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -43,17 +43,17 @@ jobs:
           WINEPATH=$($PWD/winepath-for ${{ matrix.target }})
           echo "WINEPATH=$WINEPATH" >> $GITHUB_ENV
           echo "WINARCH=win64" >> $GITHUB_ENV
-      - name: Build without getlibs
-        run: |
-          BUILD="build-${{ matrix.target }}-${CMAKE_BUILD_TYPE,,}"
-          cmake -B "$BUILD" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
-          cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          ctest --build "$BUILD" -C $CMAKE_BUILD_TYPE)
+#      - name: Build without getlibs
+#        run: |
+#          BUILD="build-${{ matrix.target }}-${CMAKE_BUILD_TYPE,,}"
+#          cmake -B "$BUILD" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
+#          cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
+#          ctest --build "$BUILD" -C $CMAKE_BUILD_TYPE)
       - name: Getlibs
         run: ./getlibs.sh ${{ matrix.target }}
       - name: Build with getlibs
         run: |
-          BUILD="build-${{ matrix.target }}-libs-${CMAKE_BUILD_TYPE,,}"          
+          BUILD="build-${{ matrix.target }}-libs-${CMAKE_BUILD_TYPE,,}"
           cmake -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/${{ matrix.target }}" -DUDBM_STATIC=$STATIC -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }} -DENABLE_DBM_NEW=${{ matrix.newdbm }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
           ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE
@@ -71,12 +71,12 @@ jobs:
         sanitizers: [ON, OFF]
     steps:
       - uses: actions/checkout@v3
-      - name: Build without getlibs
-        run: |
-          BUILD=build-darwin-$CMAKE_BUILD_TYPE
-          cmake -B "$BUILD" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
-          cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
+#      - name: Build without getlibs
+#        run: |
+#          BUILD=build-darwin-$CMAKE_BUILD_TYPE
+#          cmake -B "$BUILD" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
+#          cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
+#          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
       - name: Get dependencies
         run: CMAKE_BUILD_TYPE=Release ./getlibs.sh darwin
       - name: Build with getlibs
@@ -95,12 +95,12 @@ jobs:
       CTEST_TEST_TIMEOUT: 20
     steps:
       - uses: actions/checkout@v3
-      - name: Build without getlibs
-        run: |
-          $env:BUILD='build-x86_64-windows'
-          cmake -B $env:BUILD
-          cmake --build $env:BUILD --config $env:CMAKE_BUILD_TYPE
-          ctest --test-dir $env:BUILD -C $env:CMAKE_BUILD_TYPE
+#      - name: Build without getlibs
+#        run: |
+#          $env:BUILD='build-x86_64-windows'
+#          cmake -B $env:BUILD
+#          cmake --build $env:BUILD --config $env:CMAKE_BUILD_TYPE
+#          ctest --test-dir $env:BUILD -C $env:CMAKE_BUILD_TYPE
       - name: Get dependencies
         run: |
           vcpkg integrate install

From 2660fcd3a99e90c6facefe8e0ca09cfc1c9b2dac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Wed, 23 Apr 2025 17:27:34 +0200
Subject: [PATCH 13/15] Fixed GH action script for darwin

---
 .github/workflows/build.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ce2bb60..4697929 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -76,7 +76,7 @@ jobs:
 #          BUILD=build-darwin-$CMAKE_BUILD_TYPE
 #          cmake -B "$BUILD" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
 #          cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-#          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
+#          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE
       - name: Get dependencies
         run: CMAKE_BUILD_TYPE=Release ./getlibs.sh darwin
       - name: Build with getlibs
@@ -84,7 +84,7 @@ jobs:
           BUILD=build-darwin-libs-$CMAKE_BUILD_TYPE
           cmake -B "$BUILD" -DCMAKE_PREFIX_PATH="${{ github.workspace }}/local/darwin" -DASAN=${{ matrix.sanitizers }} -DUBSAN=${{ matrix.sanitizers }}
           cmake --build "$BUILD" --config $CMAKE_BUILD_TYPE
-          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE)
+          ctest --test-dir "$BUILD" -C $CMAKE_BUILD_TYPE
   build-windows:
     runs-on: windows-latest
     env:

From 0e1f8e03898bead42b4559da0ed1bf8c49a7c109 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Mon, 12 May 2025 12:46:15 +0200
Subject: [PATCH 14/15] Fixed debug build and simplified valuation

---
 include/dbm/valuation.h | 66 ++++++++++++++++++++---------------------
 src/pfed.cpp            |  2 +-
 src/priced.cpp          |  2 +-
 test/test_fed_dbm.cpp   |  2 +-
 test/test_valuation.cpp | 32 ++++++++++----------
 5 files changed, 51 insertions(+), 53 deletions(-)

diff --git a/include/dbm/valuation.h b/include/dbm/valuation.h
index b5fef86..1a08c64 100644
--- a/include/dbm/valuation.h
+++ b/include/dbm/valuation.h
@@ -29,18 +29,17 @@ namespace dbm
     template <typename S>
     class valuation_t
     {
-    private:
         size_t static_size;
         size_t dynamic_size;
-        std::vector<S> values;
+        std::vector<S> _values;
 
     public:
         /** Constructor
          * @param size: size of the S valuation vector (number of dimensions).
          * @param dyn: number of dynamic values.
          */
-        valuation_t(size_t size, size_t dyn = 0): static_size{size}, dynamic_size{dyn}, values(size + dyn) {}
-        valuation_t(const std::initializer_list<S>& list): static_size{list.size()}, dynamic_size{0}, values{list} {}
+        explicit valuation_t(size_t size, size_t dyn = 0): static_size{size}, dynamic_size{dyn}, _values(size + dyn) {}
+        valuation_t(const std::initializer_list<S>& list): static_size{list.size()}, dynamic_size{0}, _values{list} {}
 
         valuation_t(const valuation_t& other): valuation_t(other.static_size, other.dynamic_size) { *this = other; }
         valuation_t(valuation_t&&) noexcept = default;
@@ -49,9 +48,8 @@ namespace dbm
         {
             assert(src.static_size == static_size);
             assert(src.dynamic_size <= dynamic_size);
-            std::copy(src.begin(), src.end(), begin_mutable());  // copy the common values
-            std::fill(std::next(begin_mutable(), static_size + src.dynamic_size), end_mutable(),
-                      S{});  // reset remaining
+            std::copy(src.begin(), src.end(), begin());                                 // copy the common values
+            std::fill(std::next(begin(), static_size + src.dynamic_size), end(), S{});  // reset remaining
             return *this;
         }
 
@@ -60,8 +58,8 @@ namespace dbm
          */
         valuation_t& operator+=(S value)
         {
-            if (value != 0 && values.size() > 1)
-                for (auto i = std::next(begin_mutable()); i != end_mutable(); ++i)
+            if (value != 0 && _values.size() > 1)
+                for (auto i = std::next(begin()); i != end(); ++i)
                     *i += value;
             return *this;
         }
@@ -73,19 +71,19 @@ namespace dbm
         /** Reset all values (except #0) to specific value */
         void reset(S value = {})
         {
-            if (values.size() > 1)
-                std::fill(std::next(begin_mutable()), end_mutable(), value);
+            if (_values.size() > 1)
+                std::fill(std::next(begin()), end(), value);
         }
         const S& back() const
         {
-            assert(!values.empty());
-            return values.back();
+            assert(!_values.empty());
+            return _values.back();
         }
 
         S& back()
         {
-            assert(!values.empty());
-            return values.back();
+            assert(!_values.empty());
+            return _values.back();
         }
 
         const S& back_static() const
@@ -98,13 +96,13 @@ namespace dbm
          * argument point. This has any sense iff
          * argument point = this point + some delay.
          */
-        S get_delay_to(const valuation_t<S>& arg) const
+        S get_delay_to(const valuation_t& arg) const
         {
-            if (values.size() <= 1)
-                return 0;                   // Only ref clock.
-            S delay = arg[1] - (*this)[1];  // Get delay.
-#ifndef NDEBUG                              // Check consistency.
-            for (size_t i = 1, n = values.size(); i < n; ++i)
+            if (_values.size() <= 1)
+                return 0;                     // Only ref clock.
+            S delay = arg[1u] - (*this)[1u];  // Get delay.
+#ifndef NDEBUG                                // Check consistency.
+            for (size_t i = 1, n = _values.size(); i < n; ++i)
                 assert(arg[i] - (*this)[i] == delay);
 #endif
             return delay;
@@ -121,32 +119,32 @@ namespace dbm
         bool extend(size_t n, S value = {})
         {
             dynamic_size += n;
-            values.resize(static_size + dynamic_size, value);
+            _values.resize(static_size + dynamic_size, value);
             return true;
         }
 
-        size_t size() const { return values.size(); }
-        auto begin() const { return values.cbegin(); }
-        auto end() const { return values.cend(); }
-        auto begin_mutable() { return values.begin(); }
-        auto end_mutable() { return values.end(); }
+        size_t size() const { return _values.size(); }
+        auto begin() const { return _values.cbegin(); }
+        auto end() const { return _values.cend(); }
+        auto begin() { return _values.begin(); }
+        auto end() { return _values.end(); }
 
-        operator const std::vector<S>&() const { return values; }
-        operator const S*() const { return values.data(); }
-        auto& get_mutable() { return values; }
+        operator const std::vector<S>&() const { return _values; }
+        operator const S*() const { return _values.data(); }
+        auto& values() { return _values; }
 
         /** wrap and check */
         S& operator[](size_t at)
         {
-            assert(at < values.size());
-            return values[at];
+            assert(at < _values.size());
+            return _values[at];
         }
 
         /** wrap and check read-only */
         const S& operator[](size_t at) const
         {
-            assert(at < values.size());
-            return values[at];
+            assert(at < _values.size());
+            return _values[at];
         }
     };
 
diff --git a/src/pfed.cpp b/src/pfed.cpp
index 232d091..c527c05 100644
--- a/src/pfed.cpp
+++ b/src/pfed.cpp
@@ -68,7 +68,7 @@ namespace dbm
             int32_t inf = pdbm_getInfimumValuation(zone, dim, copy.data(), free);
             if (inf < infimum) {
                 infimum = inf;
-                std::copy(copy.begin(), copy.end(), valuation.begin_mutable());
+                std::copy(copy.begin(), copy.end(), valuation.begin());
             }
         }
         return infimum;
diff --git a/src/priced.cpp b/src/priced.cpp
index 2e6649d..f10070e 100644
--- a/src/priced.cpp
+++ b/src/priced.cpp
@@ -55,7 +55,7 @@ static auto& pdbm_cache(const PDBMPtr& pdbm) { return pdbm->infimum; }
  * @param  j    is the index of a clock
  * @return True if and only if \a i and \a j form a zero cycle in \a pdbm.
  */
-static bool pdbm_areOnZeroCycle(const PDBM_ptr& pdbm, cindex_t dim, cindex_t i, cindex_t j)
+static bool pdbm_areOnZeroCycle(const PDBMPtr& pdbm, cindex_t dim, cindex_t i, cindex_t j)
 {
     assert(pdbm && dim && i < dim && j < dim && i != j);
 
diff --git a/test/test_fed_dbm.cpp b/test/test_fed_dbm.cpp
index 4a752ac..a5fb943 100644
--- a/test/test_fed_dbm.cpp
+++ b/test/test_fed_dbm.cpp
@@ -299,7 +299,7 @@ static void test(const cindex_t dim)
 
         // constrain
         CHECK(a == dbm.get());
-        for (k = 7; k > 0 && !dbm_generatePoint(pt.get_mutable().data(), dbm, dim); --k)
+        for (k = 7; k > 0 && !dbm_generatePoint(pt.values().data(), dbm, dim); --k)
             ;
         if (k > 0) {
             bool stop = (rand() & 1) != 0;
diff --git a/test/test_valuation.cpp b/test/test_valuation.cpp
index 0d2f6be..8905c83 100644
--- a/test/test_valuation.cpp
+++ b/test/test_valuation.cpp
@@ -33,8 +33,8 @@ static void test(size_t size)
     (dv += 3.1) -= 2;
 
     if (size > 0) {
-        CHECK(iv[0] == 0.0);
-        CHECK(dv[0] == 0.0);
+        CHECK(iv[0u] == 0.0);
+        CHECK(dv[0u] == 0.0);
     }
 
     for (size_t i = 1; i < size; ++i) {
@@ -56,23 +56,23 @@ TEST_CASE("Valuation assignment")
     auto v1 = dbm::valuation_int(3, 2);
     v1 += 1;
     REQUIRE(v1.size() == 5);
-    CHECK(v1[0] == 0);
-    CHECK(v1[1] == 1);
-    CHECK(v1[2] == 1);
-    CHECK(v1[3] == 1);
-    CHECK(v1[4] == 1);
+    CHECK(v1[0u] == 0);
+    CHECK(v1[1u] == 1);
+    CHECK(v1[2u] == 1);
+    CHECK(v1[3u] == 1);
+    CHECK(v1[4u] == 1);
     auto v2 = dbm::valuation_int(3, 1);
     v2 += 2;
     REQUIRE(v2.size() == 4);
-    CHECK(v2[0] == 0);
-    CHECK(v2[1] == 2);
-    CHECK(v2[2] == 2);
-    CHECK(v2[3] == 2);
+    CHECK(v2[0u] == 0);
+    CHECK(v2[1u] == 2);
+    CHECK(v2[2u] == 2);
+    CHECK(v2[3u] == 2);
     v1 = v2;
     REQUIRE(v1.size() == 5);
-    CHECK(v1[0] == 0);
-    CHECK(v1[1] == 2);
-    CHECK(v1[2] == 2);
-    CHECK(v1[3] == 2);
-    CHECK(v1[4] == 0);
+    CHECK(v1[0u] == 0);
+    CHECK(v1[1u] == 2);
+    CHECK(v1[2u] == 2);
+    CHECK(v1[3u] == 2);
+    CHECK(v1[4u] == 0);
 }
\ No newline at end of file

From d8bc27cae4090c96df70ac48fb1e680ef488a45b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marius=20Miku=C4=8Dionis?= <marius@cs.aau.dk>
Date: Mon, 12 May 2025 12:48:28 +0200
Subject: [PATCH 15/15] Fixed compile script for running tests under wine

---
 compile.sh | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/compile.sh b/compile.sh
index 57eecbf..85bdb24 100755
--- a/compile.sh
+++ b/compile.sh
@@ -9,6 +9,13 @@ else
     targets="$@"
 fi
 
+function show_cmake_vars() {
+    for var in CMAKE_TOOLCHAIN_FILE CMAKE_BUILD_TYPE CMAKE_PREFIX_PATH CMAKE_INSTALL_PREFIX \
+               CMAKE_GENERATOR CMAKE_BUILD_PARALLEL_LEVEL; do
+        echo "  $var=${!var:- (unset)}"
+    done
+}
+
 for target in $targets ; do
     unset BUILD_EXTRA
     unset CMAKE_BUILD_TYPE
@@ -27,9 +34,11 @@ for target in $targets ; do
             ;;
         win64*|x86_64-w64-mingw32*)
             PLATFORM=x86_64-w64-mingw32
+            export WINEPATH=$("$PROJECT_DIR"/winepath-for $PLATFORM)
             ;;
         win32*|i686-w64-mingw32*)
             PLATFORM=i686-w64-mingw32
+            export WINEPATH=$("$PROJECT_DIR"/winepath-for $PLATFORM)
             ;;
         darwin-brew-gcc14*)
             PLATFORM=darwin-brew-gcc14
@@ -91,10 +100,8 @@ for target in $targets ; do
             echo "Unrecognized build type: $target, assuming $CMAKE_BUILD_TYPE"
     esac
     echo "Building $target${BUILD_EXTRA:+ with$BUILD_EXTRA} into $BUILD_DIR"
-    echo "  CMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE"
-    echo "  CMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH"
-    echo "  CMAKE_TOOLCHAIN_FILE=$CMAKE_TOOLCHAIN_FILE"
+    show_cmake_vars
     cmake -S "$PROJECT_DIR" -B "$BUILD_DIR" -DUDBM_CLANG_TIDY=OFF $BUILD_EXTRA
     cmake --build "$BUILD_DIR" --config $CMAKE_BUILD_TYPE
-    (cd "$BUILD_DIR" ; ctest -C $CMAKE_BUILD_TYPE --output-on-failure)
+    ctest --test-dir "$BUILD_DIR" -C $CMAKE_BUILD_TYPE --output-on-failure
 done