From 4a93fcf482483733cba1c93e9eea409ef4426f9c Mon Sep 17 00:00:00 2001
From: viktor <viktor.teren@gmail.com>
Date: Fri, 19 Apr 2024 14:44:29 +0200
Subject: [PATCH] Revert some changes.

---
 CMakeLists.txt | 199 ++++++++++++++++++++++++++++++++++---------------
 src/main.cpp   |   1 +
 2 files changed, 139 insertions(+), 61 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 801a9f1..4ed4995 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,68 +1,145 @@
-cmake_minimum_required(VERSION 3.9)
-project (Seto LANGUAGES CXX C)
+cmake_minimum_required(VERSION 3.1)
+include(${CMAKE_ROOT}/Modules/ExternalProject.cmake)
 
-include(GNUInstallDirs)
-
-find_package(OpenMP)
+set(CUDD_DIR ${CMAKE_SOURCE_DIR}/libs/cudd)
+if(MSVC OR MINGW)
+    if (CMAKE_CL_64)
+        set(CUDD_CONFIG_DIR ${CMAKE_SOURCE_DIR}/libs/cudd-config/windows)
+    else()
+        set(CUDD_CONFIG_DIR ${CMAKE_SOURCE_DIR}/libs/cudd-config/windows-32)
+    endif()
+else()
+    set(CUDD_CONFIG_DIR ${CMAKE_SOURCE_DIR}/libs/cudd-config/unix)
+endif()
+set(UNISTD_INCLUDE_DIR ${CMAKE_SOURCE_DIR}/libs/unistd)
+set(GETOPT_INCLUDE_DIR ${CMAKE_SOURCE_DIR}/libs/getopt)
 
-add_library(libminisat STATIC
-        # Impl files
-        libs/minisat/core/Solver.cc
-        libs/minisat/core/SolverTypes.cc
-        libs/minisat/utils/Options.cc
-        # Header files for IDEs
-        libs/minisat/core/Dimacs.h
-        libs/minisat/core/Solver.h
-        libs/minisat/core/SolverTypes.h
-        libs/minisat/mtl/Alg.h
-        libs/minisat/mtl/Alloc.h
-        libs/minisat/mtl/Heap.h
-        libs/minisat/mtl/IntTypes.h
-        libs/minisat/mtl/Map.h
-        libs/minisat/mtl/Queue.h
-        libs/minisat/mtl/Sort.h
-        libs/minisat/mtl/Vec.h
-        libs/minisat/mtl/XAlloc.h
-        libs/minisat/utils/Options.h)
+set(SOURCES
+        ${CUDD_DIR}/cudd/cuddAddAbs.c
+        ${CUDD_DIR}/cudd/cuddAddApply.c
+        ${CUDD_DIR}/cudd/cuddAddFind.c
+        ${CUDD_DIR}/cudd/cuddAddInv.c
+        ${CUDD_DIR}/cudd/cuddAddIte.c
+        ${CUDD_DIR}/cudd/cuddAddNeg.c
+        ${CUDD_DIR}/cudd/cuddAddWalsh.c
+        ${CUDD_DIR}/cudd/cuddAndAbs.c
+        ${CUDD_DIR}/cudd/cuddAnneal.c
+        ${CUDD_DIR}/cudd/cuddApa.c
+        ${CUDD_DIR}/cudd/cuddAPI.c
+        ${CUDD_DIR}/cudd/cuddApprox.c
+        ${CUDD_DIR}/cudd/cuddBddAbs.c
+        ${CUDD_DIR}/cudd/cuddBddCorr.c
+        ${CUDD_DIR}/cudd/cuddBddIte.c
+        ${CUDD_DIR}/cudd/cuddBridge.c
+        ${CUDD_DIR}/cudd/cuddCache.c
+        ${CUDD_DIR}/cudd/cuddCheck.c
+        ${CUDD_DIR}/cudd/cuddClip.c
+        ${CUDD_DIR}/cudd/cuddCof.c
+        ${CUDD_DIR}/cudd/cuddCompose.c
+        ${CUDD_DIR}/cudd/cuddDecomp.c
+        ${CUDD_DIR}/cudd/cuddEssent.c
+        ${CUDD_DIR}/cudd/cuddExact.c
+        ${CUDD_DIR}/cudd/cuddExport.c
+        ${CUDD_DIR}/cudd/cuddGenCof.c
+        ${CUDD_DIR}/cudd/cuddGenetic.c
+        ${CUDD_DIR}/cudd/cuddGroup.c
+        ${CUDD_DIR}/cudd/cuddHarwell.c
+        ${CUDD_DIR}/cudd/cuddInit.c
+        ${CUDD_DIR}/cudd/cuddInteract.c
+        ${CUDD_DIR}/cudd/cuddLCache.c
+        ${CUDD_DIR}/cudd/cuddLevelQ.c
+        ${CUDD_DIR}/cudd/cuddLinear.c
+        ${CUDD_DIR}/cudd/cuddLiteral.c
+        ${CUDD_DIR}/cudd/cuddMatMult.c
+        ${CUDD_DIR}/cudd/cuddPriority.c
+        ${CUDD_DIR}/cudd/cuddRead.c
+        ${CUDD_DIR}/cudd/cuddRef.c
+        ${CUDD_DIR}/cudd/cuddReorder.c
+        ${CUDD_DIR}/cudd/cuddSat.c
+        ${CUDD_DIR}/cudd/cuddSign.c
+        ${CUDD_DIR}/cudd/cuddSolve.c
+        ${CUDD_DIR}/cudd/cuddSplit.c
+        ${CUDD_DIR}/cudd/cuddSubsetHB.c
+        ${CUDD_DIR}/cudd/cuddSubsetSP.c
+        ${CUDD_DIR}/cudd/cuddSymmetry.c
+        ${CUDD_DIR}/cudd/cuddTable.c
+        ${CUDD_DIR}/cudd/cuddUtil.c
+        ${CUDD_DIR}/cudd/cuddWindow.c
+        ${CUDD_DIR}/cudd/cuddZddCount.c
+        ${CUDD_DIR}/cudd/cuddZddFuncs.c
+        ${CUDD_DIR}/cudd/cuddZddGroup.c
+        ${CUDD_DIR}/cudd/cuddZddIsop.c
+        ${CUDD_DIR}/cudd/cuddZddLin.c
+        ${CUDD_DIR}/cudd/cuddZddMisc.c
+        ${CUDD_DIR}/cudd/cuddZddPort.c
+        ${CUDD_DIR}/cudd/cuddZddReord.c
+        ${CUDD_DIR}/cudd/cuddZddSetop.c
+        ${CUDD_DIR}/cudd/cuddZddSymm.c
+        ${CUDD_DIR}/cudd/cuddZddUtil.c
+        ${CUDD_DIR}/util/cpu_stats.c
+        ${CUDD_DIR}/util/cpu_time.c
+        ${CUDD_DIR}/util/cstringstream.c
+        ${CUDD_DIR}/util/datalimit.c
+        ${CUDD_DIR}/util/pathsearch.c
+        ${CUDD_DIR}/util/pipefork.c
+        ${CUDD_DIR}/util/prtime.c
+        ${CUDD_DIR}/util/strsav.c
+        ${CUDD_DIR}/util/texpand.c
+        ${CUDD_DIR}/util/ucbqsort.c
+        ${CUDD_DIR}/util/safe_mem.c
+        ${CUDD_DIR}/st/st.c
+        ${CUDD_DIR}/epd/epd.c
+        ${CUDD_DIR}/mtr/mtrBasic.c
+        ${CUDD_DIR}/mtr/mtrGroup.c
+        ${CUDD_DIR}/cplusplus/cuddObj.cc
+)
 
-target_include_directories(libminisat
-        PUBLIC
-        $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/libs>
-        )
+add_library(cudd STATIC ${SOURCES})
+target_include_directories(cudd PRIVATE ${CUDD_DIR}/cudd ${CUDD_DIR}/util ${CUDD_DIR}/st ${CUDD_DIR}/epd ${CUDD_DIR}/mtr ${CUDD_DIR} ${CUDD_CONFIG_DIR})
+if (MSVC)
+    target_include_directories(cudd PRIVATE ${UNISTD_INCLUDE_DIR} ${GETOPT_INCLUDE_DIR})
+endif()
+#add_dependencies(cudd CUDD_DOWNLOAD)
 
-add_subdirectory(${CMAKE_CURRENT_SOURCE_DIR}/libs)
+if (MSVC)
+    set(CUDD_INCLUDE_DIR ${CUDD_DIR}/cplusplus ${CUDD_DIR}/cudd ${CUDD_DIR}/util ${CUDD_CONFIG_DIR} ${UNISTD_INCLUDE_DIR} ${GETOPT_INCLUDE_DIR} PARENT_SCOPE)
+else()
+    set(CUDD_INCLUDE_DIR ${CUDD_DIR}/cplusplus ${CUDD_DIR}/cudd ${CUDD_DIR}/util ${CUDD_CONFIG_DIR} PARENT_SCOPE)
+endif()
 
-# Grab the files
-file(GLOB SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/*.cpp)
-file(GLOB HEADERS ${CMAKE_CURRENT_SOURCE_DIR}/include/*.h)
+set(PBLIB_DIR ${CMAKE_SOURCE_DIR}/libs/pblib/pblib)
 
-add_executable(${PROJECT_NAME} ${SOURCES} ${HEADERS}
-        include/main.h)
+set(PBLIB_SOURCE_FILES
+        ${PBLIB_DIR}/auxvarmanager.cpp
+        ${PBLIB_DIR}/clausedatabase.cpp
+        ${PBLIB_DIR}/formula.cpp
+        ${PBLIB_DIR}/helper.cpp
+        ${PBLIB_DIR}/incpbconstraint.cpp
+        ${PBLIB_DIR}/IncrementalData.cpp
+        ${PBLIB_DIR}/IncSimplePBConstraint.cpp
+        ${PBLIB_DIR}/pb2cnf.cpp
+        ${PBLIB_DIR}/PBConfig.cpp
+        ${PBLIB_DIR}/pbconstraint.cpp
+        ${PBLIB_DIR}/PBFuzzer.cpp
+        ${PBLIB_DIR}/PBParser.cpp
+        ${PBLIB_DIR}/preencoder.cpp
+        ${PBLIB_DIR}/SimplePBConstraint.cpp
+        ${PBLIB_DIR}/VectorClauseDatabase.cpp
+        ${PBLIB_DIR}/encoder/adderencoding.cpp
+        ${PBLIB_DIR}/encoder/amo.cpp
+        ${PBLIB_DIR}/encoder/bdd.cpp
+        ${PBLIB_DIR}/encoder/BDD_Seq_Amo.cpp
+        ${PBLIB_DIR}/encoder/bimander_amo_encoding.cpp
+        ${PBLIB_DIR}/encoder/binary_amo.cpp
+        ${PBLIB_DIR}/encoder/BinaryMerge.cpp
+        ${PBLIB_DIR}/encoder/cardencoding.cpp
+        ${PBLIB_DIR}/encoder/commander_encoding.cpp
+        ${PBLIB_DIR}/encoder/Encoder.cpp
+        ${PBLIB_DIR}/encoder/k-product.cpp
+        ${PBLIB_DIR}/encoder/naive_amo_encoder.cpp
+        ${PBLIB_DIR}/encoder/sorting_merging.cpp
+        ${PBLIB_DIR}/encoder/SortingNetworks.cpp
+        ${PBLIB_DIR}/encoder/SWC.cpp
+)
 
-target_link_libraries(${PROJECT_NAME} libminisat)
-target_link_libraries(${PROJECT_NAME} pblib)
-if( python3.10_FOUND )
-    target_link_libraries(${PROJECT_NAME} python3.10)   #needed for networkx usage
-endif()
-target_link_libraries(${PROJECT_NAME} cudd)
-if( OpenMP_FOUND )
-    target_link_libraries(${PROJECT_NAME} OpenMP::OpenMP_CXX)
-endif()
-target_include_directories(${PROJECT_NAME} PRIVATE ${CUDD_INCLUDE_DIR})
-add_dependencies(${PROJECT_NAME} cudd)
-
-if( python3.10_FOUND )
-    if ( CMAKE_CXX_COMPILER_ID MATCHES "Clang|AppleClang|GNU" )
-        target_compile_options(${PROJECT_NAME} PRIVATE  -Wall -Wextra  -I/usr/include/python3.10)
-    endif()
-    if ( CMAKE_CXX_COMPILER_ID MATCHES "MSVC" )
-        target_compile_options(${PROJECT_NAME} PRIVATE /W4 /wd4267 -I/usr/include/python3.10)
-    endif()
-else()
-    if ( CMAKE_CXX_COMPILER_ID MATCHES "Clang|AppleClang|GNU" )
-        target_compile_options(${PROJECT_NAME} PRIVATE  -Wall -Wextra)
-    endif()
-    if ( CMAKE_CXX_COMPILER_ID MATCHES "MSVC" )
-        target_compile_options(${PROJECT_NAME} PRIVATE /W4 /wd4267)
-    endif()
-endif()
\ No newline at end of file
+add_library(pblib STATIC ${PBLIB_SOURCE_FILES})
diff --git a/src/main.cpp b/src/main.cpp
index 5d9b9ca..c1d38fe 100755
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -287,6 +287,7 @@ int main(int argc, char **argv) {
                 PyRun_SimpleString(python_code.c_str());
                 Py_Finalize();
 
+
                 cout << "=================[END PYTHON]=================" << endl;
 
                 read_SMs("final_FSMs.txt", SMs, *aliases_region_pointer);