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 8, 2024
1 parent 639fe80 commit 50bc3ff
Show file tree
Hide file tree
Showing 65 changed files with 5,776 additions and 321 deletions.
38 changes: 19 additions & 19 deletions .github/workflows/CI.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -9,29 +9,29 @@ jobs:
fail-fast: false
matrix:
target:
- double: aarch64-linux # target we are building for
system: aarch64-linux # system we are building on
emulated: true # whether this build is being emulated
runner: ubuntu-24.04 # GitHub runner the build is running on
flake: bundled # flake package to build
interpreter: /lib/ld-linux-aarch64.so.1 # path to libc interpreter
# - double: aarch64-linux # target we are building for
# system: aarch64-linux # system we are building on
# emulated: true # whether this build is being emulated
# runner: ubuntu-24.04 # GitHub runner the build is running on
# flake: bundled # flake package to build
# interpreter: /lib/ld-linux-aarch64.so.1 # path to libc interpreter
- 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
runner: macos-latest
flake: bundled
- double: x86_64-darwin
system: x86_64-darwin
runner: macos-13
flake: bundled
- double: x86_64-windows
system: x86_64-linux
runner: ubuntu-24.04
flake: bundled-windows
# - double: aarch64-darwin
# system: aarch64-darwin
# runner: macos-latest
# flake: bundled
# - double: x86_64-darwin
# system: x86_64-darwin
# runner: macos-13
# flake: bundled
# - double: x86_64-windows
# system: x86_64-linux
# runner: ubuntu-24.04
# flake: bundled-windows
runs-on: ${{ matrix.target.runner }}
steps:
- name: Checkout
Expand Down
86 changes: 43 additions & 43 deletions .github/workflows/Container.yaml
Original file line number Diff line number Diff line change
@@ -1,43 +1,43 @@
name: Container

on:
- push

env:
REGISTRY: ghcr.io
IMAGE_NAME: softvare-group/d4v2
TAG: ${{ github.ref_name }}

jobs:
Build:
strategy:
matrix:
target:
- double: aarch64-linux # target we are building for
architecture: arm64 # container architecture label
emulated: true # whether this build host is being emulated
- double: x86_64-linux
architecture: amd64
runs-on: ubuntu-24.04
steps:
- name: Checkout
uses: actions/checkout@v4
- name: QEMU
if: ${{ matrix.target.emulated }}
run: sudo apt-get install -y qemu-user-static
- name: Nix
uses: DeterminateSystems/nix-installer-action@v10
with:
extra-conf: |
extra-platforms = ${{ matrix.target.double }}
- name: Cache
uses: DeterminateSystems/magic-nix-cache-action@v4
- name: Build
run: nix build -L .#packages.${{ matrix.target.double }}.container
- name: Login
run: nix run nixpkgs#skopeo -- login $REGISTRY --username ${{ github.actor }} --password ${{ secrets.GITHUB_TOKEN }}
- name: Push
run: nix run nixpkgs#skopeo -- copy docker-archive:result docker://$REGISTRY/$IMAGE_NAME:$TAG-${{ matrix.target.architecture }}
- name: Push latest tag
if: ${{ github.ref_type == 'tag' }}
run: nix run nixpkgs#skopeo -- copy docker://$REGISTRY/$IMAGE_NAME:$TAG-${{ matrix.target.architecture }} docker://$REGISTRY/$IMAGE_NAME:latest-${{ matrix.target.architecture }}
#name: Container
#
#on:
# - push
#
#env:
# REGISTRY: ghcr.io
# IMAGE_NAME: softvare-group/d4v2
# TAG: ${{ github.ref_name }}
#
#jobs:
# Build:
# strategy:
# matrix:
# target:
# - double: aarch64-linux # target we are building for
# architecture: arm64 # container architecture label
# emulated: true # whether this build host is being emulated
# - double: x86_64-linux
# architecture: amd64
# runs-on: ubuntu-24.04
# steps:
# - name: Checkout
# uses: actions/checkout@v4
# - name: QEMU
# if: ${{ matrix.target.emulated }}
# run: sudo apt-get install -y qemu-user-static
# - name: Nix
# uses: DeterminateSystems/nix-installer-action@v10
# with:
# extra-conf: |
# extra-platforms = ${{ matrix.target.double }}
# - name: Cache
# uses: DeterminateSystems/magic-nix-cache-action@v4
# - name: Build
# run: nix build -L .#packages.${{ matrix.target.double }}.container
# - name: Login
# run: nix run nixpkgs#skopeo -- login $REGISTRY --username ${{ github.actor }} --password ${{ secrets.GITHUB_TOKEN }}
# - name: Push
# run: nix run nixpkgs#skopeo -- copy docker-archive:result docker://$REGISTRY/$IMAGE_NAME:$TAG-${{ matrix.target.architecture }}
# - name: Push latest tag
# if: ${{ github.ref_type == 'tag' }}
# run: nix run nixpkgs#skopeo -- copy docker://$REGISTRY/$IMAGE_NAME:$TAG-${{ matrix.target.architecture }} docker://$REGISTRY/$IMAGE_NAME:latest-${{ matrix.target.architecture }}
56 changes: 28 additions & 28 deletions .github/workflows/Portable.yaml
Original file line number Diff line number Diff line change
@@ -1,28 +1,28 @@
name: Portable

on:
- push

jobs:
Build:
strategy:
fail-fast: false
matrix:
target:
- double: x86_64-linux
runner: ubuntu-latest
runs-on: ${{ matrix.target.runner }}
steps:
- name: Checkout
uses: actions/checkout@v4
- name: Nix
uses: DeterminateSystems/nix-installer-action@v10
- name: Cache
uses: DeterminateSystems/magic-nix-cache-action@v4
- name: Bundle
run: nix bundle --bundler github:DavHau/nix-portable -o bundle
- name: Upload
uses: actions/upload-artifact@v4
with:
name: d4-${{ matrix.target.double }}-portable
path: bundle
#name: Portable
#
#on:
# - push
#
#jobs:
# Build:
# strategy:
# fail-fast: false
# matrix:
# target:
# - double: x86_64-linux
# runner: ubuntu-latest
# runs-on: ${{ matrix.target.runner }}
# steps:
# - name: Checkout
# uses: actions/checkout@v4
# - name: Nix
# uses: DeterminateSystems/nix-installer-action@v10
# - name: Cache
# uses: DeterminateSystems/magic-nix-cache-action@v4
# - name: Bundle
# run: nix bundle --bundler github:DavHau/nix-portable -o bundle
# - name: Upload
# uses: actions/upload-artifact@v4
# with:
# name: d4-${{ matrix.target.double }}-portable
# path: bundle
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
16 changes: 11 additions & 5 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -21,16 +21,20 @@ if(NOT BUILD_SHARED_LIBS)
set(glucose_USE_STATIC_LIBS ON)
endif()

set(GPMC_USE_STATIC_LIBS ON)

find_package(GMP REQUIRED)
find_package(Boost REQUIRED COMPONENTS program_options)
find_package(MtKaHyPar REQUIRED)
find_package(arjun REQUIRED)
find_package(GPMC REQUIRED)
find_package(glucose 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()
#if(USE_GLUCOSE)
# find_package(glucose REQUIRED)
# include_directories(${glucose_INCLUDE_DIRS})
#endif()

include_directories(${CMAKE_CURRENT_SOURCE_DIR})
include_directories(${CMAKE_CURRENT_SOURCE_DIR}/3rdParty/glucose-3.0)
Expand All @@ -39,6 +43,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 @@ -154,7 +160,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)

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()
11 changes: 10 additions & 1 deletion flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,9 @@
{
default = self.packages.${system}.d4;

glucose = pkgs.callPackage ./nix/glucose.nix { };
glucose-windows = pkgs-windows.callPackage ./nix/glucose.nix { };

cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { };
cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix {
cadical = self.packages.${system}.cadical;
Expand All @@ -95,6 +98,7 @@

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

tbb = tbb pkgs;
Expand All @@ -107,13 +111,18 @@

d4 = pkgs.callPackage ./nix/d4.nix {
mt-kahypar = self.packages.${system}.mt-kahypar;
sbva = self.packages.${system}.sbva;
arjun = self.packages.${system}.arjun;
gpmc = self.packages.${system}.gpmc;
glucose = self.packages.${system}.glucose;
cryptominisat = self.packages.${system}.cryptominisat;
};

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

container = pkgs.dockerTools.buildLayeredImage {
Expand Down
Loading

0 comments on commit 50bc3ff

Please sign in to comment.