Skip to content

Commit dacd791

Browse files
authored
Merge pull request #21 from rmanhaeve/master
Fixed SIGSEGV bug on MacOS, added CI/CD building for all platforms.
2 parents 5a44909 + 088dfe3 commit dacd791

File tree

3 files changed

+209
-17
lines changed

3 files changed

+209
-17
lines changed

.github/workflows/release.yml

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
name: release
2+
on:
3+
push:
4+
tags:
5+
- "v*.*.*"
6+
7+
jobs:
8+
build-linux:
9+
runs-on: ubuntu-latest
10+
strategy:
11+
fail-fast: true
12+
matrix:
13+
variant: [nogmp, gmp]
14+
steps:
15+
- uses: actions/checkout@v4
16+
- name: Install deps
17+
run: |
18+
sudo apt-get update
19+
sudo apt-get install -y g++ make libgmp-dev
20+
- name: Build
21+
run: |
22+
cp Makefile_${{ matrix.variant }} Makefile
23+
make clean
24+
make all
25+
- name: Smoke test
26+
run: |
27+
cat > /tmp/smoke.cnf <<'EOF'
28+
p cnf 1 1
29+
1 0
30+
EOF
31+
./dsharp /tmp/smoke.cnf > /tmp/dsharp.out
32+
cat /tmp/dsharp.out
33+
test -s /tmp/dsharp.out
34+
- name: Package
35+
run: |
36+
mkdir -p dist
37+
OUT="dsharp-${{ github.ref_name }}-linux-x86_64-${{ matrix.variant }}"
38+
cp dsharp "dist/${OUT}"
39+
- uses: actions/upload-artifact@v4
40+
with:
41+
name: dsharp-${{ github.ref_name }}-linux-x86_64-${{ matrix.variant }}
42+
path: dist/dsharp-${{ github.ref_name }}-linux-x86_64-${{ matrix.variant }}
43+
44+
build-windows:
45+
runs-on: windows-latest
46+
strategy:
47+
fail-fast: true
48+
matrix:
49+
variant: [nogmp, gmp]
50+
steps:
51+
- uses: actions/checkout@v4
52+
- uses: msys2/setup-msys2@v2
53+
with:
54+
msystem: MINGW64
55+
update: true
56+
install: >-
57+
base-devel
58+
make
59+
mingw-w64-x86_64-toolchain
60+
mingw-w64-x86_64-gmp
61+
- name: Build
62+
shell: msys2 {0}
63+
run: |
64+
cp Makefile_${{ matrix.variant }} Makefile
65+
make clean
66+
make all
67+
- name: Smoke test
68+
shell: msys2 {0}
69+
run: |
70+
cat > /tmp/smoke.cnf <<'EOF'
71+
p cnf 1 1
72+
1 0
73+
EOF
74+
./dsharp.exe /tmp/smoke.cnf > /tmp/dsharp.out
75+
cat /tmp/dsharp.out
76+
test -s /tmp/dsharp.out
77+
- name: Package
78+
shell: msys2 {0}
79+
run: |
80+
mkdir -p dist
81+
OUT="dsharp-${{ github.ref_name }}-windows-x86_64-${{ matrix.variant }}.exe"
82+
cp dsharp "dist/${OUT}"
83+
- uses: actions/upload-artifact@v4
84+
with:
85+
name: dsharp-${{ github.ref_name }}-windows-x86_64-${{ matrix.variant }}
86+
path: dist/dsharp-${{ github.ref_name }}-windows-x86_64-${{ matrix.variant }}.exe
87+
88+
build-macos:
89+
strategy:
90+
fail-fast: true
91+
matrix:
92+
os: [macos-14]
93+
arch: [x86_64, arm64]
94+
variant: [nogmp, gmp]
95+
runs-on: ${{ matrix.os }}
96+
steps:
97+
- uses: actions/checkout@v4
98+
- name: Setup arch
99+
run: |
100+
if [ "${{ matrix.arch }}" = "x86_64" ]; then
101+
sudo /usr/sbin/softwareupdate --install-rosetta --agree-to-license || true
102+
if [ ! -x /usr/local/bin/brew ]; then
103+
arch -x86_64 /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
104+
fi
105+
echo "ARCH_PREFIX=arch -x86_64" >> "$GITHUB_ENV"
106+
echo "BREW_CMD=arch -x86_64 /usr/local/bin/brew" >> "$GITHUB_ENV"
107+
else
108+
echo "ARCH_PREFIX=" >> "$GITHUB_ENV"
109+
echo "BREW_CMD=brew" >> "$GITHUB_ENV"
110+
fi
111+
- name: Install deps
112+
run: |
113+
if [ "${{ matrix.variant }}" = "gmp" ]; then
114+
${BREW_CMD} install gmp
115+
fi
116+
- name: Build
117+
run: |
118+
cp Makefile_${{ matrix.variant }} Makefile
119+
${ARCH_PREFIX} make clean
120+
if [ "${{ matrix.variant }}" = "gmp" ]; then
121+
GMP_PREFIX="$(${BREW_CMD} --prefix gmp)"
122+
${ARCH_PREFIX} make all CXX=clang++ \
123+
CXXFLAGS="-pipe -O3 -w -arch ${{ matrix.arch }} -I${GMP_PREFIX}/include" \
124+
LFLAGS="-arch ${{ matrix.arch }} -Wl,-rpath,${GMP_PREFIX}/lib" \
125+
LIBS="-L${GMP_PREFIX}/lib -lgmpxx -lgmp"
126+
else
127+
${ARCH_PREFIX} make all CXX=clang++ \
128+
CXXFLAGS="-pipe -O3 -w -arch ${{ matrix.arch }}" \
129+
LFLAGS="-arch ${{ matrix.arch }}"
130+
fi
131+
- name: Smoke test
132+
run: |
133+
cat > /tmp/smoke.cnf <<'EOF'
134+
p cnf 1 1
135+
1 0
136+
EOF
137+
${ARCH_PREFIX} ./dsharp /tmp/smoke.cnf > /tmp/dsharp.out
138+
cat /tmp/dsharp.out
139+
test -s /tmp/dsharp.out
140+
- name: Package
141+
run: |
142+
mkdir -p dist
143+
OUT="dsharp-${{ github.ref_name }}-macos-${{ matrix.arch }}-${{ matrix.variant }}"
144+
cp dsharp "dist/${OUT}"
145+
- uses: actions/upload-artifact@v4
146+
with:
147+
name: dsharp-${{ github.ref_name }}-macos-${{ matrix.arch }}-${{ matrix.variant }}
148+
path: dist/dsharp-${{ github.ref_name }}-macos-${{ matrix.arch }}-${{ matrix.variant }}
149+
150+
universal-macos:
151+
needs: build-macos
152+
runs-on: macos-14
153+
strategy:
154+
fail-fast: true
155+
matrix:
156+
variant: [nogmp, gmp]
157+
steps:
158+
- uses: actions/download-artifact@v4
159+
with:
160+
name: dsharp-${{ github.ref_name }}-macos-x86_64-${{ matrix.variant }}
161+
path: x86_64
162+
- uses: actions/download-artifact@v4
163+
with:
164+
name: dsharp-${{ github.ref_name }}-macos-arm64-${{ matrix.variant }}
165+
path: arm64
166+
- name: Lipo
167+
run: |
168+
OUT="dsharp-${{ github.ref_name }}-macos-universal-${{ matrix.variant }}"
169+
lipo -create -output "${OUT}" x86_64/* arm64/*
170+
- uses: actions/upload-artifact@v4
171+
with:
172+
name: dsharp-${{ github.ref_name }}-macos-universal-${{ matrix.variant }}
173+
path: dsharp-${{ github.ref_name }}-macos-universal-${{ matrix.variant }}
174+
175+
release:
176+
needs:
177+
- build-linux
178+
- build-windows
179+
- universal-macos
180+
runs-on: ubuntu-latest
181+
steps:
182+
- uses: actions/download-artifact@v4
183+
with:
184+
path: artifacts
185+
- name: Create release
186+
uses: softprops/action-gh-release@v2
187+
with:
188+
files: artifacts/**

VERSION.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
1.0.0

src/src_sharpSAT/MainSolver/DecisionTree.cpp

Lines changed: 20 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -290,12 +290,13 @@ void DTNode::compressNode()
290290
if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr
291291
== (*it)->getType()))
292292
{
293-
(*it)->parentDeleted(this);
294-
childDeleted(*it);
293+
DTNode * oldNode = (*it);
294+
oldNode->parentDeleted(this);
295+
childDeleted(oldNode);
295296

296-
if ((0 == (*it)->numParents()) && ((*it)->getType()
297+
if ((0 == oldNode->numParents()) && (oldNode->getType()
297298
!= DT_NodeType::kDTLit))
298-
delete *it;
299+
delete oldNode;
299300
found = true;
300301
break; // Note: required to prevent segfault (mac OS)
301302
}
@@ -312,12 +313,13 @@ void DTNode::compressNode()
312313
{
313314
if (DT_NodeType::kDTTop == (*it)->getType())
314315
{
315-
(*it)->parentDeleted(this);
316-
childDeleted(*it);
316+
DTNode * oldNode = (*it);
317+
oldNode->parentDeleted(this);
318+
childDeleted(oldNode);
317319

318-
if ((0 == (*it)->numParents()) && ((*it)->getType()
320+
if ((0 == oldNode->numParents()) && (oldNode->getType()
319321
!= DT_NodeType::kDTLit))
320-
delete *it;
322+
delete oldNode;
321323
found = true;
322324
break; // Note: required to prevent segfault (mac OS)
323325
}
@@ -448,12 +450,13 @@ void DTNode::compressNode()
448450
if ((DT_NodeType::kDTAnd == (*it)->getType()) || (DT_NodeType::kDTOr
449451
== (*it)->getType()))
450452
{
451-
(*it)->parentDeleted(this);
452-
childDeleted(*it);
453+
DTNode * oldNode = (*it);
454+
oldNode->parentDeleted(this);
455+
childDeleted(oldNode);
453456

454-
if ((0 == (*it)->numParents()) && ((*it)->getType()
457+
if ((0 == oldNode->numParents()) && (oldNode->getType()
455458
!= DT_NodeType::kDTLit))
456-
delete *it;
459+
delete oldNode;
457460
found = true;
458461
break; // Note: required to prevent segfault (mac OS)
459462
}
@@ -470,12 +473,13 @@ void DTNode::compressNode()
470473
{
471474
if (DT_NodeType::kDTBottom == (*it)->getType())
472475
{
473-
(*it)->parentDeleted(this);
474-
childDeleted(*it);
476+
DTNode * oldNode = (*it);
477+
oldNode->parentDeleted(this);
478+
childDeleted(oldNode);
475479

476-
if ((0 == (*it)->numParents()) && ((*it)->getType()
480+
if ((0 == oldNode->numParents()) && (oldNode->getType()
477481
!= DT_NodeType::kDTLit))
478-
delete *it;
482+
delete oldNode;
479483
found = true;
480484
break; // Note: required to prevent segfault (mac OS)
481485
}
@@ -839,4 +843,3 @@ void DTNode::sub_parents(DTNode *newChild) {
839843
}
840844
parents.clear();
841845
}
842-

0 commit comments

Comments
 (0)