Skip to content

Commit 4b1889f

Browse files
arijitsharijitsh
committed
add CI, do [release]
1 parent 9f35cf1 commit 4b1889f

7 files changed

Lines changed: 326 additions & 27 deletions

File tree

‎.github/workflows/build.yml‎

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
name: Build
2+
3+
on:
4+
push:
5+
branches: ["**"]
6+
pull_request:
7+
branches: [main]
8+
9+
jobs:
10+
build-linux:
11+
name: ${{ matrix.name }}
12+
runs-on: ubuntu-24.04
13+
strategy:
14+
fail-fast: false
15+
matrix:
16+
include:
17+
- name: release (linux)
18+
cmake_args: -DCMAKE_BUILD_TYPE=Release
19+
run_tests: true
20+
static_compile: false
21+
22+
# - name: debug-ubsan (linux)
23+
# cmake_args: >-
24+
# -DCMAKE_BUILD_TYPE=Debug
25+
# -DCMAKE_CXX_FLAGS="-fsanitize=undefined,address -fno-sanitize-recover=all"
26+
# -DCMAKE_EXE_LINKER_FLAGS="-fsanitize=undefined,address"
27+
# run_tests: true
28+
# static_compile: false
29+
30+
- name: static (linux)
31+
cmake_args: -DCMAKE_BUILD_TYPE=Release -DSTATICCOMPILE=ON
32+
run_tests: true
33+
static_compile: true
34+
35+
steps:
36+
- uses: actions/checkout@v4
37+
with:
38+
submodules: recursive
39+
40+
- name: Install dependencies
41+
run: |
42+
sudo apt-get update -q
43+
sudo apt-get install -y --no-install-recommends \
44+
build-essential cmake libmlpack-dev libensmallen-dev \
45+
libgmp-dev libboost-all-dev libmpfr-dev \
46+
zlib1g-dev libubsan1 libasan8
47+
48+
- name: Cache built deps
49+
uses: actions/cache@v4
50+
with:
51+
path: |
52+
build/deps_install
53+
deps/cadical
54+
deps/cadiback
55+
key: deps-${{ matrix.name }}-${{ hashFiles('deps/**/*.txt', 'deps/**/*.cmake', 'deps/**/CMakeLists.txt') }}
56+
restore-keys: deps-${{ matrix.name }}-Linux-
57+
58+
- name: Configure
59+
run: cmake -S . -B build -DAUTO_DOWNLOAD=OFF ${{ matrix.cmake_args }}
60+
61+
- name: Build
62+
run: cmake --build build --parallel $(nproc)
63+
64+
- name: Version check
65+
run: build/skolemfc --version
66+
67+
- name: Test — find_inv_bvsle_bvnot_4bit
68+
if: matrix.run_tests
69+
run: |
70+
build/skolemfc -s 1 -e 0.8 -d 0.8 \
71+
utils/baseline/find_inv_bvsle_bvnot_4bit.qdimacs 2>&1 | tee /tmp/out.txt
72+
grep -q "^s fc 2 \*\*" /tmp/out.txt
73+
74+
- name: Upload artifact
75+
if: matrix.static_compile
76+
uses: actions/upload-artifact@v4
77+
with:
78+
name: skolemfc-linux-amd64
79+
path: build/skolemfc
80+
81+
build-macos:
82+
name: ${{ matrix.name }}
83+
runs-on: macos-latest
84+
strategy:
85+
fail-fast: false
86+
matrix:
87+
include:
88+
- name: release (macos)
89+
cmake_args: -DCMAKE_BUILD_TYPE=Release
90+
run_tests: true
91+
static_compile: false
92+
93+
- name: static (macos)
94+
cmake_args: -DCMAKE_BUILD_TYPE=Release -DSTATICCOMPILE=ON
95+
run_tests: true
96+
static_compile: true
97+
98+
steps:
99+
- uses: actions/checkout@v4
100+
with:
101+
submodules: recursive
102+
103+
- name: Install dependencies
104+
run: |
105+
brew install cmake mlpack gmp boost mpfr
106+
echo "CMAKE_PREFIX_PATH=$(brew --prefix)" >> $GITHUB_ENV
107+
108+
- name: Cache built deps
109+
uses: actions/cache@v4
110+
with:
111+
path: |
112+
build/deps_install
113+
deps/cadical
114+
deps/cadiback
115+
key: deps-${{ matrix.name }}-${{ hashFiles('deps/**/*.txt', 'deps/**/*.cmake', 'deps/**/CMakeLists.txt') }}
116+
restore-keys: deps-${{ matrix.name }}-macOS-
117+
118+
- name: Configure
119+
run: cmake -S . -B build -DAUTO_DOWNLOAD=OFF ${{ matrix.cmake_args }}
120+
121+
- name: Build
122+
run: cmake --build build --parallel $(sysctl -n hw.logicalcpu)
123+
124+
- name: Version check
125+
run: build/skolemfc --version
126+
127+
- name: Test — find_inv_bvsle_bvnot_4bit
128+
if: matrix.run_tests
129+
run: |
130+
build/skolemfc -s 1 -e 0.8 -d 0.8 \
131+
utils/baseline/find_inv_bvsle_bvnot_4bit.qdimacs 2>&1 | tee /tmp/out.txt
132+
grep -q "^s fc 2 \*\*" /tmp/out.txt
133+
134+
- name: Upload artifact
135+
if: matrix.static_compile
136+
uses: actions/upload-artifact@v4
137+
with:
138+
name: skolemfc-macos-arm64
139+
path: build/skolemfc
140+
141+
release:
142+
needs: [build-linux, build-macos]
143+
runs-on: ubuntu-latest
144+
if: github.event_name == 'push' && contains(github.event.head_commit.message, '[release]')
145+
permissions:
146+
contents: write
147+
steps:
148+
- uses: actions/checkout@v4
149+
150+
- name: Get version
151+
id: version
152+
run: |
153+
VERSION=$(grep -m1 'project\s*(skolemfc\s*VERSION' CMakeLists.txt \
154+
| grep -oP '\d+\.\d+\.\d+')
155+
echo "version=$VERSION" >> $GITHUB_OUTPUT
156+
157+
- name: Download Linux artifact
158+
uses: actions/download-artifact@v4
159+
with:
160+
name: skolemfc-linux-amd64
161+
path: artifacts/linux
162+
163+
- name: Download macOS artifact
164+
uses: actions/download-artifact@v4
165+
with:
166+
name: skolemfc-macos-arm64
167+
path: artifacts/macos
168+
169+
- name: Prepare release artifacts
170+
run: |
171+
set -euo pipefail
172+
strip artifacts/linux/skolemfc
173+
zip -j artifacts/skolemfc-linux-amd64.zip artifacts/linux/skolemfc
174+
zip -j artifacts/skolemfc-macos-arm64.zip artifacts/macos/skolemfc
175+
176+
- name: Create Release
177+
uses: softprops/action-gh-release@v2
178+
with:
179+
tag_name: v${{ steps.version.outputs.version }}
180+
name: SkolemFC v${{ steps.version.outputs.version }}
181+
generate_release_notes: true
182+
files: |
183+
artifacts/skolemfc-linux-amd64.zip
184+
artifacts/skolemfc-macos-arm64.zip

‎CMakeLists.txt‎

Lines changed: 65 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ if(POLICY CMP0104)
5353
endif()
5454

5555

56-
project (skolemfc)
56+
project (skolemfc VERSION 1.0.0)
5757

5858
# -----------------------------------------------------------------------------
5959
# Make RelWithDebInfo the default build type if otherwise not set
@@ -380,6 +380,22 @@ function(_build_dep _name _src_dir)
380380
return()
381381
endif()
382382

383+
# RPATH is meaningless for static archives; setting it causes cmake's
384+
# install step to fail with "No valid ELF RPATH entry" on .a files.
385+
# When building static, also tell find_library to prefer .a over .so so
386+
# that dep cmake configs don't hardcode .so paths (which break -static links).
387+
if(BUILD_SHARED_LIBS)
388+
set(_rpath_args
389+
-DCMAKE_INSTALL_RPATH=${DEPS_INSTALL_DIR}/lib
390+
-DCMAKE_BUILD_RPATH=${DEPS_INSTALL_DIR}/lib)
391+
set(_find_suffix_args "")
392+
else()
393+
set(_rpath_args
394+
-DCMAKE_SKIP_RPATH=ON
395+
-DCMAKE_SKIP_INSTALL_RPATH=ON)
396+
set(_find_suffix_args "-DCMAKE_FIND_LIBRARY_SUFFIXES=.a")
397+
endif()
398+
383399
message(STATUS "[deps] Configuring ${_name} from ${_src_dir} ...")
384400
execute_process(
385401
COMMAND ${CMAKE_COMMAND}
@@ -388,14 +404,11 @@ function(_build_dep _name _src_dir)
388404
-DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}
389405
-DCMAKE_INSTALL_PREFIX=${DEPS_INSTALL_DIR}
390406
-DCMAKE_PREFIX_PATH=${DEPS_INSTALL_DIR}
391-
# Make the linker find previously-installed dep shared libs.
392-
# (The Config.cmake.in files in these projects do not call
393-
# find_dependency(), so transitive IMPORTED targets may not be
394-
# available. Providing -L lets the linker resolve them.)
407+
# Make the linker find previously-installed dep libs.
395408
"-DCMAKE_SHARED_LINKER_FLAGS=-L${DEPS_INSTALL_DIR}/lib"
396409
"-DCMAKE_EXE_LINKER_FLAGS=-L${DEPS_INSTALL_DIR}/lib"
397-
-DCMAKE_INSTALL_RPATH=${DEPS_INSTALL_DIR}/lib
398-
-DCMAKE_BUILD_RPATH=${DEPS_INSTALL_DIR}/lib
410+
${_rpath_args}
411+
${_find_suffix_args}
399412
-DENABLE_TESTING=OFF
400413
-DBUILD_SHARED_LIBS=${BUILD_SHARED_LIBS}
401414
# Suppress man-page generation: FALSE skips find_program re-search
@@ -549,15 +562,45 @@ if(AUTO_DOWNLOAD OR EXISTS "${CMAKE_SOURCE_DIR}/deps/louvain-community/CMakeList
549562

550563
# Build in strict dependency order; each dep can find previously installed ones
551564
# via CMAKE_PREFIX_PATH=${DEPS_INSTALL_DIR}.
565+
566+
# When building static, find the static GMP paths here (CMAKE_FIND_LIBRARY_SUFFIXES
567+
# is already ".a" at this point) so we can pass full paths to sub-builds.
568+
# The -D override on the cmake command line gets clobbered by platform files, so
569+
# this is the only reliable way.
570+
if(NOT BUILD_SHARED_LIBS)
571+
find_library(_static_gmp NAMES gmp REQUIRED)
572+
find_library(_static_gmpxx NAMES gmpxx REQUIRED)
573+
set(_gmp_override_args
574+
"-DGMP_LIBRARY=${_static_gmp}"
575+
"-DGMPXX_LIBRARY=${_static_gmpxx}"
576+
"-DGMP_LIBRARIES=${_static_gmpxx};${_static_gmp}")
577+
message(STATUS "[deps] static GMP: ${_static_gmp}, GMPXX: ${_static_gmpxx}")
578+
else()
579+
set(_gmp_override_args "")
580+
endif()
581+
552582
# cadical and cadiback are autoconf/make projects built in-place; cryptominisat
553583
# locates them via relative path (../cadical, ../cadiback).
554584
# cadical: configure creates build/ subdir; build only static lib with -fPIC
555585
_build_autoconf_dep(cadical "${_DEPS_SRC}/cadical" "build" "libcadical.a"
556586
"CXXFLAGS=-fPIC")
557-
# cadiback: configure+make in source dir; pass absolute path to cadical
587+
# cadiback: configure+make in source dir; pass absolute path to cadical.
588+
# The `generate` script checks `[ -d .git ]` but inside a git submodule
589+
# .git is a FILE not a directory. Patch it unconditionally (no-op if
590+
# already patched) so both submodule and fresh-clone setups work.
591+
if(EXISTS "${_DEPS_SRC}/cadiback/generate")
592+
file(READ "${_DEPS_SRC}/cadiback/generate" _gen)
593+
string(REPLACE
594+
"[ -d .git ] || die"
595+
"[ -d .git ] || [ -f .git ] || die"
596+
_gen "${_gen}")
597+
file(WRITE "${_DEPS_SRC}/cadiback/generate" "${_gen}")
598+
endif()
558599
_build_autoconf_dep(cadiback "${_DEPS_SRC}/cadiback" "" "libcadiback.a"
559600
"CADICAL=${_DEPS_SRC}/cadical" "CXXFLAGS=-fPIC")
560-
_build_dep(louvain-community "${_DEPS_SRC}/louvain-community")
601+
_build_dep(louvain-community "${_DEPS_SRC}/louvain-community"
602+
"-DCMAKE_POLICY_VERSION_MINIMUM=3.5"
603+
${_gmp_override_args})
561604
# cryptominisat's backbone.cpp uses #include "../cadiback/cadiback.h" relative
562605
# to its src/ dir, so it expects cadiback.h at <cryptominisat_src>/cadiback/.
563606
# Create a symlink there pointing to the real header in deps/cadiback/include/.
@@ -571,12 +614,20 @@ if(AUTO_DOWNLOAD OR EXISTS "${CMAKE_SOURCE_DIR}/deps/louvain-community/CMakeList
571614
_build_dep(cryptominisat "${_DEPS_SRC}/cryptominisat"
572615
# Override find_library to use our local static libs, not system installs
573616
"-Dcadiback=${_DEPS_SRC}/cadiback/libcadiback.a"
574-
"-Dcadical=${_DEPS_SRC}/cadical/build/libcadical.a")
575-
_build_dep(sbva "${_DEPS_SRC}/sbva")
576-
_build_dep(arjun "${_DEPS_SRC}/arjun")
577-
_build_dep(approxmc "${_DEPS_SRC}/approxmc")
617+
"-Dcadical=${_DEPS_SRC}/cadical/build/libcadical.a"
618+
${_gmp_override_args})
619+
_build_dep(sbva "${_DEPS_SRC}/sbva"
620+
${_gmp_override_args})
621+
_build_dep(arjun "${_DEPS_SRC}/arjun"
622+
# Override find_library: arjun searches PATHS last so system cadical
623+
# wins otherwise; pre-fill the cache variable with our meelgroup build.
624+
"-Dcadical=${_DEPS_SRC}/cadical/build/libcadical.a"
625+
${_gmp_override_args})
626+
_build_dep(approxmc "${_DEPS_SRC}/approxmc"
627+
${_gmp_override_args})
578628
if(NOT NOUNIGEN)
579-
_build_dep(unigen "${_DEPS_SRC}/unigen")
629+
_build_dep(unigen "${_DEPS_SRC}/unigen"
630+
${_gmp_override_args})
580631
endif()
581632

582633
# Point find_package to the freshly installed deps

‎README.md‎

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,43 @@
11
# SkolemFC: An Approximate Skolem Function Counter
22

33
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
4-
<!-- ![build](https://github.com/meelgroup/SkolemFC/workflows/build/badge.svg)
5-
[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/SkolemFC/) -->
4+
[![.github/workflows/build.yml](https://github.com/meelgroup/skolemfc/actions/workflows/build.yml/badge.svg)](https://github.com/meelgroup/skolemfc/actions/workflows/build.yml)
65

76
SkolemFC takes in a F(X,Y) formula as input and returns the number of Boolean functions G(X) such that ∃Y F(X, Y) = F(X, G(X)). SkolemFC *counts the number of functions without even generating a single function.*
87

98
To learn more about SkolemFC, please have a look at our [AAAI-24 paper](https://arxiv.org/abs/2312.12026).
109

1110

1211
## How to Build a Binary
13-
To build on Linux, you will need the following:
12+
13+
### Dependencies
14+
15+
**Linux:**
16+
```
17+
sudo apt install build-essential cmake git libubsan1 libasan8 \
18+
zlib1g-dev libmlpack-dev libensmallen-dev libmpfr-dev \
19+
libboost-program-options-dev libboost-serialization-dev libgmp3-dev
1420
```
15-
sudo apt install build-essential cmake git zlib1g-dev libboost-program-options-dev libboost-serialization-dev libgmp3-dev
21+
22+
**macOS:**
23+
```
24+
brew install cmake gmp boost mpfr mlpack
1625
```
1726

18-
Now clone this repository and run `./install.sh`, this should compile SkolemFC and all its dependencies.
27+
### Build
28+
29+
Clone the repository (including submodules) and configure:
1930

2031
```
21-
git clone https://github.com/meelgroup/skolemfc/
32+
git clone --recurse-submodules https://github.com/meelgroup/skolemfc/
2233
cd skolemfc
23-
./install.sh
34+
./configure.sh
35+
cd build && make -j10
2436
```
2537

26-
Please follow [`INSTALL.md`](https://github.com/meelgroup/skolemfc/tree/main/INSTALL.md) if the script reports some error, or you need more instructions for compiling in other OS, etc.
38+
### configure.sh options
2739

40+
Run `./configure.sh --help` for the full usage message.
2841

2942

3043
## How to Use the Binary
@@ -51,6 +64,7 @@ SkolemFC reports that we have approximately `16 (=2 ** 4)` functions satisfying
5164
### Guarantees
5265
SkolemFC provides so-called "PAC", or Probably Approximately Correct, guarantees. In less fancy words, the system guarantees that the solution found is within a certain tolerance (called "epsilon") with a certain probability (called "delta"). The default tolerance and probability, i.e. epsilon and delta values, are set to 0.8 and 0.4, respectively. Both values are configurable.
5366

67+
> Code in this branch does not provide theoretical guarantees. See `main` branch for code which truly follows the paper.
5468
5569
### Issues, questions, bugs, etc.
5670
Please click on "issues" at the top and [create a new issue](https://github.com/meelgroup/skolemfc/issues/new). All issues are responded to promptly.

0 commit comments

Comments
 (0)