Skip to content

Commit

Permalink
feat: add projected compilation
Browse files Browse the repository at this point in the history
  • Loading branch information
uulm-janbaudisch committed Oct 12, 2024
1 parent 639fe80 commit f896ad9
Show file tree
Hide file tree
Showing 65 changed files with 5,732 additions and 257 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/CI.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ jobs:
- double: x86_64-linux
system: x86_64-linux
runner: ubuntu-24.04
flake: bundled
flake: d4
interpreter: /lib64/ld-linux-x86-64.so.2
- double: aarch64-darwin
system: aarch64-darwin
Expand Down
7 changes: 3 additions & 4 deletions 3rdParty/GPMC/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -21,20 +21,19 @@ add_subdirectory(flow-cutter-pace17)
add_library(gpmc
core/ComponentCache.cc
core/ComponentManager.cc
core/Counter.cc
core/Config.cc
core/Counter.cc
core/gpmc.cpp
core/Instance.cc
core/Solver.cc
ddnnf/DecisionTree.cc
core/Solver.cc
utils/Options.cc
utils/System.cc
preprocessor/Preprocessor.cc
preprocessor/TestSolver.cc
preprocessor/lib_sharpsat_td/subsumer.cpp
preprocessor/TreeDecomposition.cc
preprocessor/IFlowCutter.cc
core/gpmc.cpp
core/Solver.h
)

set_target_properties(gpmc PROPERTIES PUBLIC_HEADER include/gpmc.hpp)
Expand Down
2 changes: 1 addition & 1 deletion 3rdParty/glucose-3.0/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,6 @@ set_target_properties(binary PROPERTIES OUTPUT_NAME glucose)
target_link_libraries(binary glucose)

install(
TARGETS glucose
TARGETS glucose binary
FILE_SET HEADERS DESTINATION include/glucose
)
5 changes: 0 additions & 5 deletions 3rdParty/glucose-3.0/core/Main.cc
Original file line number Diff line number Diff line change
Expand Up @@ -94,11 +94,6 @@ int main(int argc, char** argv)
setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// printf("This is MiniSat 2.0 beta\n");

#if defined(__linux__)
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
printf("c WARNING: for repeatability, setting FPU to use double precision\n");
#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
Expand Down
5 changes: 0 additions & 5 deletions 3rdParty/glucose-3.0/simp/Main.cc
Original file line number Diff line number Diff line change
Expand Up @@ -96,11 +96,6 @@ int main(int argc, char** argv)
setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");


#if defined(__linux__)
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
printf("WARNING: for repeatability, setting FPU to use double precision\n");
#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
Expand Down
4 changes: 0 additions & 4 deletions 3rdParty/glucose-3.0/utils/System.h
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Glucose_System_h
#define Glucose_System_h

#if defined(__linux__)
#include <fpu_control.h>
#endif

#include "mtl/IntTypes.h"

//-------------------------------------------------------------------------------------------------
Expand Down
15 changes: 8 additions & 7 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -18,19 +18,16 @@ if(NOT BUILD_SHARED_LIBS)
set(GMP_USE_STATIC_LIBS ON)
set(Boost_USE_STATIC_LIBS ON)
set(MtKaHyPar_USE_STATIC_LIBS ON)
set(GPMC_USE_STATIC_LIBS ON)
set(glucose_USE_STATIC_LIBS ON)
endif()

find_package(GMP REQUIRED)
find_package(Boost REQUIRED COMPONENTS program_options)
find_package(MtKaHyPar REQUIRED)
find_package(arjun REQUIRED)

# glucose is only needed when requested, which it is not by default.
if(USE_GLUCOSE)
find_package(glucose REQUIRED)
include_directories(${glucose_INCLUDE_DIRS})
endif()
find_package(GPMC REQUIRED)
find_package(glucose REQUIRED)

include_directories(${CMAKE_CURRENT_SOURCE_DIR})
include_directories(${CMAKE_CURRENT_SOURCE_DIR}/3rdParty/glucose-3.0)
Expand All @@ -39,6 +36,8 @@ include_directories(${GMPXX_INCLUDE_DIRS})
include_directories(${Boost_INCLUDE_DIRS})
include_directories(${MtKaHyPar_INCLUDE_DIR})
include_directories(${arjun_INCLUDE_DIR})
include_directories(${GMPC_INCLUDE_DIR})
include_directories(${glucose_INCLUDE_DIRS})

add_library(caching OBJECT
src/caching/BucketAllocator.cpp
Expand Down Expand Up @@ -102,7 +101,9 @@ add_library(partitioner OBJECT
)

add_library(preprocs OBJECT
src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp
src/preprocs/cnf/util/PreprocGPMC.cpp
src/preprocs/cnf/util/TestSolver.cpp
src/preprocs/cnf/PreprocBackboneCnf.cpp
src/preprocs/cnf/PreprocBasicCnf.cpp
src/preprocs/cnf/PreprocGPMC.cpp
Expand Down Expand Up @@ -154,7 +155,7 @@ add_library(core STATIC
$<TARGET_OBJECTS:utils>
)

target_link_libraries(core GMP::GMPXX GMP::GMP MtKaHyPar::MtKaHyPar arjun)
target_link_libraries(core MtKaHyPar::MtKaHyPar GPMC::GPMC arjun glucose::glucose GMP::GMPXX GMP::GMP cadiback cadical)

if(USE_GLUCOSE)
target_link_libraries(core glucose::glucose)
Expand Down
54 changes: 54 additions & 0 deletions cmake/FindGPMC.cmake
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
include(FindPackageHandleStandardArgs)

# Keep track of the original library suffixes to reset them later.
set(_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES ${CMAKE_FIND_LIBRARY_SUFFIXES})

# Look for .a or .lib libraries in case of a static library.
if(GPMC_USE_STATIC_LIBS)
set(CMAKE_FIND_LIBRARY_SUFFIXES .a .lib)
endif()

# Find libraries and headers.
find_library(GPMC_LIBRARY NAMES gpmc)
find_path(GPMC_INCLUDE_DIR NAMES gpmc.hpp)

# Windows (dynamic): Also find import libraries.
if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
set(CMAKE_FIND_LIBRARY_SUFFIXES .dll.a .lib)
find_library(GPMC_IMPORT_LIBRARY NAMES gpmc)
endif()

# Reset library suffixes.
set(CMAKE_FIND_LIBRARY_SUFFIXES ${_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES})

# Register the found package.
if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
# Windows (dynamic): also require import libraries.
find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_IMPORT_LIBRARY GPMC_INCLUDE_DIR)
else()
find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_INCLUDE_DIR)
endif()

if(GPMC_FOUND)
mark_as_advanced(GPMC_LIBRARY)
mark_as_advanced(GPMC_IMPORT_LIBRARY)
mark_as_advanced(GPMC_INCLUDE_DIR)

# Create targets in case not already done.
if(NOT TARGET GPMC::GPMC)
if(GPMC_USE_STATIC_LIBS)
add_library(GPMC::GPMC STATIC IMPORTED)
else()
add_library(GPMC::GPMC SHARED IMPORTED)
endif()

# Set library and include paths.
set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_LOCATION ${GPMC_LIBRARY})
target_include_directories(GPMC::GPMC INTERFACE ${GPMC_INCLUDE_DIR})

# Windows (dynamic): Also set import library.
if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_IMPLIB ${GPMC_IMPORT_LIBRARY})
endif()
endif()
endif()
6 changes: 3 additions & 3 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

81 changes: 61 additions & 20 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,9 @@
"x86_64-linux"
];

# If building for Windows, appends -windows, otherwise nothing.
windowsSuffix = pkgs: name: if pkgs.stdenv.hostPlatform.isWindows then "${name}-windows" else name;

# Different platforms require different TBB versions and the Windows one is not in upstream Nixpkgs yet.
tbb =
pkgs:
Expand All @@ -26,23 +29,23 @@
else
pkgs.tbb_2021_11;

mt-kahypar = pkgs: pkgs.callPackage ./nix/mt-kahypar.nix { tbb = tbb pkgs; };
d4 = pkgs: pkgs.callPackage ./nix/d4.nix { mt-kahypar = mt-kahypar pkgs; };

# All required runtime dependencies.
dependencies =
pkgs:
let
system = pkgs.stdenv.system;
windowsSuffix' = windowsSuffix pkgs;
in
pkgs.buildEnv {
name = "d4-dependencies";
paths = [
(mt-kahypar pkgs)
(tbb pkgs)
self.packages.${system}.${windowsSuffix' "mt-kahypar"}
self.packages.${system}.${windowsSuffix' "tbb"}
pkgs.hwloc.lib
pkgs.gmp
] ++ lib.optionals pkgs.stdenv.cc.isClang [ pkgs.libcxx ];
};

# A simple README explaining how to setup the built directories to run the binary.
documentation =
pkgs:
pkgs.stdenv.mkDerivation {
Expand All @@ -57,12 +60,16 @@
# The binary with all dependencies.
bundled =
pkgs:
let
system = pkgs.stdenv.system;
windowsSuffix' = windowsSuffix pkgs;
in
pkgs.buildEnv {
name = "d4";
paths = [
(d4 pkgs)
(dependencies pkgs)
(documentation pkgs)
self.packages.${system}.${windowsSuffix' "d4"}
self.packages.${system}.${windowsSuffix' "dependencies"}
self.packages.${system}.${windowsSuffix' "documentation"}
];
};
in
Expand All @@ -72,29 +79,57 @@
system:
let
pkgs = nixpkgs.legacyPackages.${system};
pkgs-static = if pkgs.stdenv.isDarwin then pkgs else pkgs.pkgsStatic;
pkgs-windows = pkgs.pkgsCross.mingwW64;
in
{
default = self.packages.${system}.d4;

cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { };
cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix {
glucose = pkgs-static.callPackage ./nix/glucose.nix { };
glucose-windows = pkgs-windows.callPackage ./nix/glucose.nix { };

cadical = pkgs-static.callPackage ./nix/cadical.nix { };
cadical-windows = pkgs-windows.callPackage ./nix/cadical.nix { };

cadiback = pkgs-static.callPackage ./nix/cadiback.nix {
cadical = self.packages.${system}.cadical;
};

cryptominisat = pkgs.pkgsStatic.callPackage ./nix/cryptominisat.nix {
cadiback-windows = pkgs-windows.callPackage ./nix/cadiback.nix {
cadical = self.packages.${system}.cadical-windows;
};

cryptominisat = pkgs-static.callPackage ./nix/cryptominisat.nix {
cadical = self.packages.${system}.cadical;
cadiback = self.packages.${system}.cadiback;
};

sbva = pkgs.pkgsStatic.callPackage ./nix/sbva.nix { };
cryptominisat-windows = pkgs-windows.callPackage ./nix/cryptominisat.nix {
cadical = self.packages.${system}.cadical-windows;
cadiback = self.packages.${system}.cadiback-windows;
};

sbva = pkgs-static.callPackage ./nix/sbva.nix { };
sbva-windows = pkgs-windows.callPackage ./nix/sbva.nix { };

arjun = pkgs.pkgsStatic.callPackage ./nix/arjun.nix {
arjun = pkgs-static.callPackage ./nix/arjun.nix {
cryptominisat = self.packages.${system}.cryptominisat;
sbva = self.packages.${system}.sbva;
};

gpmc = pkgs.pkgsStatic.callPackage ./nix/gpmc.nix {
arjun-windows = pkgs-windows.callPackage ./nix/arjun.nix {
cryptominisat = self.packages.${system}.cryptominisat-windows;
sbva = self.packages.${system}.sbva-windows;
};

gpmc = pkgs-static.callPackage ./nix/gpmc.nix {
arjun = self.packages.${system}.arjun;
cryptominisat = self.packages.${system}.cryptominisat;
};

gpmc-windows = pkgs-windows.callPackage ./nix/gpmc.nix {
arjun = self.packages.${system}.arjun-windows;
cryptominisat = self.packages.${system}.cryptominisat-windows;
};

tbb = tbb pkgs;
Expand All @@ -108,13 +143,16 @@
d4 = pkgs.callPackage ./nix/d4.nix {
mt-kahypar = self.packages.${system}.mt-kahypar;
arjun = self.packages.${system}.arjun;
gpmc = self.packages.${system}.gpmc;
glucose = self.packages.${system}.glucose;
};

# TODO: arjun on windows
#d4-windows = pkgs-windows.callPackage ./nix/d4.nix {
# mt-kahypar = self.packages.${system}.mt-kahypar-windows;
# arjun = self.packages.${system}.arjun-windows;
#};
d4-windows = pkgs-windows.callPackage ./nix/d4.nix {
mt-kahypar = self.packages.${system}.mt-kahypar-windows;
arjun = self.packages.${system}.arjun-windows;
gpmc = self.packages.${system}.gmpc-windows;
glucose = self.packages.${system}.glucose-windows;
};

container = pkgs.dockerTools.buildLayeredImage {
name = "d4";
Expand All @@ -132,6 +170,9 @@
dependencies = dependencies pkgs;
dependencies-windows = dependencies pkgs-windows;

documentation = documentation pkgs;
documentation-windows = documentation pkgs-windows;

bundled = bundled pkgs;
bundled-windows = bundled pkgs-windows;
}
Expand Down
3 changes: 3 additions & 0 deletions nix/cryptominisat.nix
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
cmake,
gmp,
zlib,
cadical,
cadiback,
}:
stdenv.mkDerivation rec {
Expand Down Expand Up @@ -34,6 +35,8 @@ stdenv.mkDerivation rec {
gmp.dev
];

cmakeFlags = [ "-DBUILD_SHARED_LIBS=OFF" ];

meta = {
mainProgram = "cryptominisat5";
description = "An advanced SAT solver";
Expand Down
4 changes: 4 additions & 0 deletions nix/d4.nix
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
gmp,
mt-kahypar,
arjun,
gpmc,
glucose,
}:
stdenv.mkDerivation rec {
pname = "d4";
Expand All @@ -21,6 +23,8 @@ stdenv.mkDerivation rec {
arjun.dev
boost.dev
gmp.dev
gpmc.dev
glucose.dev
];

meta = with lib; {
Expand Down
Loading

0 comments on commit f896ad9

Please sign in to comment.