Skip to content

Commit

Permalink
Merge pull request #52 from GaloisInc/T51-macos-13
Browse files Browse the repository at this point in the history
Build x86-64 macOS solvers on `macos-13`
  • Loading branch information
RyanGlScott authored Nov 8, 2024
2 parents 34585a2 + 531431b commit 982ebbb
Show file tree
Hide file tree
Showing 5 changed files with 116 additions and 15 deletions.
4 changes: 4 additions & 0 deletions .github/ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ build_abc() {

build_bitwuzla() {
pushd repos/bitwuzla
# Backport a fix for https://github.com/bitwuzla/bitwuzla/issues/118
patch -p1 -i $PATCHES/bitwuzla-fix-missing-includes-gcc14.patch
if [ "$GITHUB_MATRIX_OS" == 'ubuntu-20.04' ] ; then
# Ubuntu 20.04 uses an older version of glibc that is susceptible to
# https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909, so we must apply a
Expand Down Expand Up @@ -82,6 +84,8 @@ build_boolector() {
build_cvc4() {
pushd repos/CVC4-archived
patch -p1 -i $PATCHES/cvc4-antlr-check-aarch64.patch
# Add missing #include statements that macos-14's version of Clang++ requires.
patch -p1 -i $PATCHES/cvc4-fix-missing-includes.patch
./contrib/get-antlr-3.4
./contrib/get-symfpu
if $IS_WIN ; then
Expand Down
28 changes: 14 additions & 14 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-22.04, ubuntu-20.04, macos-12, macos-14, windows-2019]
os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019]
solver: [abc, bitwuzla, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14]
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v4
with:
submodules: true
fetch-depth: 0
Expand Down Expand Up @@ -65,7 +65,7 @@ jobs:
if: runner.os == 'Windows'

- name: Install Python
uses: actions/setup-python@v4
uses: actions/setup-python@v5
with:
python-version: '3.10'

Expand Down Expand Up @@ -94,7 +94,7 @@ jobs:
GITHUB_MATRIX_OS: ${{ matrix.os }}
if: runner.os == 'Windows'

- uses: actions/upload-artifact@v2
- uses: actions/upload-artifact@v4
with:
path: bin
name: ${{ matrix.os }}-${{ runner.arch }}-${{ matrix.solver }}-bin
Expand All @@ -105,44 +105,44 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-22.04, ubuntu-20.04, macos-12, macos-14, windows-2019]
os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019]
steps:
- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-abc-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-bitwuzla-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-boolector-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-cvc4-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-cvc5-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-yices-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.8-bin"
path: bin

- uses: actions/download-artifact@v2
- uses: actions/download-artifact@v4
with:
name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.14-bin"
path: bin
Expand All @@ -155,7 +155,7 @@ jobs:
shell: bash
run: cp bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3

- uses: actions/upload-artifact@v2
- uses: actions/upload-artifact@v4
with:
path: bin
name: ${{ matrix.os }}-${{ runner.arch }}-bin
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Currently, `what4-solvers` offers the following solver versions:

Built for the following operating systems:

* macOS Monterey 12 (x86-64)
* macOS Ventura 13 (x86-64)
* macOS Sonoma 14 (arm64)
* Ubuntu 20.04 (x86-64)
* Ubuntu 22.04 (x86-64)
Expand Down
61 changes: 61 additions & 0 deletions patches/bitwuzla-fix-missing-includes-gcc14.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
diff --git a/src/lib/bitblast/aig/aig_cnf.cpp b/src/lib/bitblast/aig/aig_cnf.cpp
index a9a00c8e..69a19ad6 100644
--- a/src/lib/bitblast/aig/aig_cnf.cpp
+++ b/src/lib/bitblast/aig/aig_cnf.cpp
@@ -10,6 +10,7 @@

#include "bitblast/aig/aig_cnf.h"

+#include <cstdlib>
#include <functional>

namespace bzla::bb {
diff --git a/src/lib/bitblast/aig/aig_manager.cpp b/src/lib/bitblast/aig/aig_manager.cpp
index 878ef276..7d36b76a 100644
--- a/src/lib/bitblast/aig/aig_manager.cpp
+++ b/src/lib/bitblast/aig/aig_manager.cpp
@@ -10,6 +10,8 @@

#include "bitblast/aig/aig_manager.h"

+#include <cstdlib>
+
namespace bzla::bb {

bool
diff --git a/src/main/options.cpp b/src/main/options.cpp
index 0d1e518a..5f3fb97c 100644
--- a/src/main/options.cpp
+++ b/src/main/options.cpp
@@ -2,6 +2,7 @@

#include <bitwuzla/cpp/bitwuzla.h>

+#include <algorithm>
#include <cassert>
#include <iomanip>
#include <iostream>
diff --git a/src/parser/smt2/parser.cpp b/src/parser/smt2/parser.cpp
index 3bd26ffc..164a48be 100644
--- a/src/parser/smt2/parser.cpp
+++ b/src/parser/smt2/parser.cpp
@@ -10,6 +10,7 @@

#include "parser/smt2/parser.h"

+#include <algorithm>
#include <iostream>

namespace bzla {
diff --git a/test/unit/api/test_api.cpp b/test/unit/api/test_api.cpp
index c80bb32d..da7c743d 100644
--- a/test/unit/api/test_api.cpp
+++ b/test/unit/api/test_api.cpp
@@ -11,6 +11,7 @@
#include <bitwuzla/cpp/bitwuzla.h>
#include <bitwuzla/cpp/parser.h>

+#include <algorithm>
#include <chrono>
#include <fstream>

36 changes: 36 additions & 0 deletions patches/cvc4-fix-missing-includes.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 55e07747e..250185809 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -19,6 +19,7 @@

#pragma once

+#include <cstddef>
#include <iosfwd>

namespace CVC4 {
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index f8464392a..985a3ca2a 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -19,6 +19,7 @@
#ifndef CVC4__EXPR__EXPR_IOMANIP_H
#define CVC4__EXPR__EXPR_IOMANIP_H

+#include <cstddef>
#include <iosfwd>

namespace CVC4 {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 180bb0c32..25c5c9ad2 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -17,6 +17,7 @@
#ifndef CVC4__UTIL__REGEXP_H
#define CVC4__UTIL__REGEXP_H

+#include <cstddef>
#include <cstdint>
#include <iosfwd>

0 comments on commit 982ebbb

Please sign in to comment.