Rebased and fixed several errors

3rd-party/lace/CMakeLists.txt

@@ -1,5 +1,3 @@
-cmake_minimum_required(VERSION 3.16)
-
 project(lace
     VERSION 1.3.1
     DESCRIPTION "Lace, a work-stealing framework for multi-core fork-join parallelism"
@@ -26,23 +24,16 @@ if(LACE_USE_MMAP)
 endif()
 
 add_library(lace STATIC)
-add_library(lace14 STATIC)
 add_library(lace::lace ALIAS lace)
-add_library(lace::lace14 ALIAS lace14)
 
 target_sources(lace PRIVATE src/lace.c PUBLIC src/lace.h)
-target_sources(lace14 PRIVATE src/lace14.c PUBLIC src/lace14.h)
 target_include_directories(lace PUBLIC ${CMAKE_CURRENT_LIST_DIR}/src ${CMAKE_CURRENT_BINARY_DIR})
-target_include_directories(lace14 PUBLIC ${CMAKE_CURRENT_LIST_DIR}/src ${CMAKE_CURRENT_BINARY_DIR})
 target_compile_features(lace PRIVATE c_std_11)
-target_compile_features(lace14 PRIVATE c_std_11)
 target_link_libraries(lace PUBLIC pthread)
-target_link_libraries(lace14 PUBLIC pthread)
 
 if(LACE_USE_HWLOC)
     find_package(Hwloc REQUIRED)
     target_link_libraries(lace PUBLIC ${HWLOC_LIBRARIES})
-    target_link_libraries(lace14 PUBLIC ${HWLOC_LIBRARIES})
 endif()
 
 configure_file(src/lace_config.h.in ${CMAKE_CURRENT_BINARY_DIR}/lace_config.h)

3rd-party/sylvan/CMakeLists.txt

@@ -1,5 +1,3 @@
-cmake_minimum_required(VERSION 3.16)
-
 project(sylvan
     VERSION 1.8.0
     DESCRIPTION "Sylvan, a parallel decision diagram library"

3rd-party/sylvan/src/CMakeLists.txt

@@ -42,6 +42,7 @@ target_sources(sylvan
 
 target_include_directories(sylvan PUBLIC .)
 target_compile_options(sylvan PRIVATE -Wno-pedantic)
+target_link_libraries(sylvan PUBLIC m pthread lace)
 
 option(SYLVAN_USE_MMAP "Let Sylvan use mmap to allocate (virtual) memory" ON)
 if(SYLVAN_USE_MMAP)

3rd-party/sylvan/src/sylvan_ldd.hpp

@@ -282,21 +282,18 @@ inline ldd follow(const ldd& A, std::uint32_t value)
 // union(A,B) = A ∪ B
 inline ldd union_(const ldd& A, const ldd& B)
 {
-  LACE_ME;
   return ldd(lddmc_union(A.get(), B.get()));
 }
 
 // minus(A,B) = A \ B
 inline ldd minus(const ldd& A, const ldd& B)
 {
-  LACE_ME;
   return ldd(lddmc_minus(A.get(), B.get()));
 }
 
 // zip(A,B) = (X,Y) such that X = A U B, Y = B \ A
 inline std::pair<ldd, ldd> zip(const ldd& A, const ldd& B)
 {
-  LACE_ME;
   MDD result[2];
   lddmc_zip(A.get(), B.get(), result);
   return {ldd(result[0]), ldd(result[1]) };
@@ -305,42 +302,36 @@ inline std::pair<ldd, ldd> zip(const ldd& A, const ldd& B)
 // project(A,p) = the projection of the set A according to the projection vector p
 inline ldd project(const ldd& A, const ldd& p)
 {
-  LACE_ME;
   return ldd(lddmc_project(A.get(), p.get()));
 }
 
 // project_minus(A,p,B) = minus(project(A,p),B)
 inline ldd project_minus(const ldd& A, const ldd& p, const ldd& B)
 {
-  LACE_ME;
   return ldd(lddmc_project_minus(A.get(), p.get(), B.get()));
 }
 
 // intersect(A,B) = A ∩ B
 inline ldd intersect(const ldd& A, const ldd& B)
 {
-  LACE_ME;
   return ldd(lddmc_intersect(A.get(), B.get()));
 }
 
 // match(A,B,meta) = A ∩ B, with B defined on subset of the variables of A according to meta
 inline ldd match(const ldd& A, const ldd& B, const ldd& meta)
 {
-  LACE_ME;
   return ldd(lddmc_match(A.get(), B.get(), meta.get()));
 }
 
 // join(A,B,pA,pB) = A ∩ B, but A and B are projections of the state vector, described by pA and pB
 inline ldd join(const ldd& A, const ldd& B, const ldd& px, const ldd& py)
 {
-  LACE_ME;
   return ldd(lddmc_join(A.get(), B.get(), px.get(), py.get()));
 }
 
 // cube(v) = the singleton set containing the tuple with values in v
 inline ldd cube(const std::uint32_t* v, std::size_t n)
 {
-  LACE_ME;
   return ldd(lddmc_cube(const_cast<std::uint32_t*>(v), n));
 }
 
@@ -353,14 +344,12 @@ inline ldd cube(const std::vector<std::uint32_t>& v)
 // member_cube(A,v) = check if cube(v) is in the set A
 inline ldd member_cube(const ldd& A, const std::vector<std::uint32_t>& v)
 {
-  LACE_ME;
   return ldd(lddmc_member_cube(A.get(), const_cast<std::uint32_t*>(v.data()), v.size()));
 }
 
 // union_cube(A,v) = union_(A,cube(v))
 inline ldd union_cube(const ldd& A, const std::uint32_t* v, std::size_t n)
 {
-  LACE_ME;
   return ldd(lddmc_union_cube(A.get(), const_cast<std::uint32_t*>(v), n));
 }
 
@@ -373,58 +362,50 @@ inline ldd union_cube(const ldd& A, const std::vector<std::uint32_t>& v)
 // <undocumented>
 inline ldd cube_copy(const std::vector<std::uint32_t>& v, const std::vector<int>& copy)
 {
-  LACE_ME;
   return ldd(lddmc_cube_copy(const_cast<std::uint32_t*>(v.data()), const_cast<int*>(copy.data()), v.size()));
 }
 
 // <undocumented>
 inline int member_cube_copy(const ldd& A, const std::vector<std::uint32_t>& v, const std::vector<int>& copy)
 {
-  LACE_ME;
   return lddmc_member_cube_copy(A.get(), const_cast<std::uint32_t*>(v.data()), const_cast<int*>(copy.data()), v.size());
 }
 
 // union_cube(A,v) = union_(A,cube(v))
 inline ldd union_cube_copy(const ldd& A, const std::uint32_t* v, const int* copy, std::size_t n)
 {
-  LACE_ME;
   return ldd(lddmc_union_cube_copy(A.get(), const_cast<std::uint32_t*>(v), const_cast<int*>(copy), n));
 }
 
 // <undocumented>
 inline ldd union_cube_copy(const ldd& A, const std::vector<std::uint32_t>& v, const std::vector<int>& copy)
 {
-  LACE_ME;
   return union_cube_copy(A, v.data(), copy.data(), v.size());
 }
 
 // relprod(A,B,meta) = the successors of the states in A according to the transition relation B which is described by meta
 // meta: -1 (end; rest not in rel), 0 (not in rel), 1 (read), 2 (write), 3 (only-read), 4 (only-write), 5 (action label)
 inline ldd relprod(const ldd& A, const ldd& B, const ldd& meta)
 {
-  LACE_ME;
   return ldd(lddmc_relprod(A.get(), B.get(), meta.get()));
 }
 
 // relprod_union(A,B,meta) = union_(A,relprod(A,B,meta))
 // TODO: the parameter U is undocumented
 inline ldd relprod_union(const ldd& A, const ldd& B, const ldd& meta, const ldd& U)
 {
-  LACE_ME;
   return ldd(lddmc_relprod_union(A.get(), B.get(), meta.get(), U.get()));
 }
 
 // relprev(A,B,meta,U) = the predecessors of the states in A according to the transition relation B which is described by meta, restricted to states in U
 inline ldd relprev(const ldd& A, const ldd& B, const ldd& meta, const ldd& U)
 {
-  LACE_ME;
   return ldd(lddmc_relprev(A.get(), B.get(), meta.get(), U.get()));
 }
 
 // satcount(A) = the size of the set A
 inline double satcount(const ldd& A)
 {
-  LACE_ME;
   return lddmc_satcount(A.get());
 }
 
@@ -440,7 +421,6 @@ std::size_t nodecount(const ldd& A)
 template <typename OutputIterator>
 inline int sat_one(const ldd& A, OutputIterator to)
 {
-  LACE_ME;
   MDD mdd = A.get();
   while (mdd != lddmc_false && mdd != lddmc_true)
   {
@@ -463,31 +443,27 @@ std::vector<std::uint32_t> sat_one_vector(const ldd& A)
 inline
 void sat_all(const ldd& A, lddmc_enum_cb cb, void* context = nullptr)
 {
-  LACE_ME;
   lddmc_sat_all_par(A.get(), cb, context);
 }
 
 // sat_all_par(A,cb) = sat_all(A,cb), but parallelized
 inline
 void sat_all_nopar(const ldd& A, lddmc_enum_cb cb, void* context = nullptr)
 {
-  LACE_ME;
   lddmc_sat_all_nopar(A.get(), cb, context);
 }
 
 // collect(A,cb) = sat_all_par(A,cb), but the callback cb returns some set encoded as an LDD, and all returned LDDs are combined using union
 // TODO: this is probably wrong, because there are two more undocumented parameters
 inline ldd collect(const ldd& A, lddmc_collect_cb cb, void* context = nullptr)
 {
-  LACE_ME;
   return ldd(lddmc_collect(A.get(), cb, context));
 }
 
 // match_sat(A,B,m,cb) = sat_all_par(match(A,B,m),cb)
 inline
 void match_sat(const ldd& A, const ldd& B, const ldd& meta, lddmc_enum_cb cb, void* context = nullptr)
 {
-  LACE_ME;
   lddmc_match_sat_par(A.get(), B.get(), meta.get(), cb, context);
 }