[CI] Build and relase Win64 binaries

This commit adds a check that cross-compiles a Windows binary, fixes
some minor issues to make the Windows build work, and adds support for
publishing a Windows binary to a (micro-)release.

Note: Regressions are currently not run for Windows builds.

.github/actions/add-to-release/action.yml

@@ -3,6 +3,10 @@ description: Add cvc5 binary to the current release
 inputs:
   binary:
     description: file name of binary
+  binary-ext:
+    description: extension of binary
+  binary-name:
+    description: name of binary in release
   github-token:
     description: token to upload binary
 runs:
@@ -11,7 +15,7 @@ runs:
     - name: Rename binaries for release
       shell: bash
       run: |
-        cp ${{ inputs.binary }} cvc5-${{ runner.os }}
+        cp ${{ inputs.binary }}${{ inputs.binary-ext }} cvc5-${{ inputs.binary-name }}${{ inputs.binary-ext }}
 
     - name: Add binaries to release
       uses: softprops/action-gh-release@v1

.github/actions/install-dependencies/action.yml

@@ -27,7 +27,8 @@ runs:
           libtinfo-dev \
           flex \
           libfl-dev \
-          flexc++
+          flexc++ \
+          mingw-w64
         python3 -m pip install pexpect setuptools toml
         cd /usr/src/googletest
         sudo cmake .

.github/workflows/ci.yml

@@ -13,7 +13,7 @@ jobs:
             python-bindings: true
             build-documentation: true
             check-examples: true
-            store-to-release: true
+            store-to-release-binary: Linux
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
@@ -23,10 +23,18 @@ jobs:
             cache-key: production
             python-bindings: true
             check-examples: true
-            store-to-release: true
+            store-to-release-binary: macOS
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
+          - name: win64:production
+            os: ubuntu-latest
+            config: production --auto-download --win64
+            cache-key: productionwin64
+            store-to-release-binary: Win64
+            binary-ext: .exe
+            build-shared: false
+
           - name: ubuntu:production-clang
             os: ubuntu-18.04
             env: CC=clang CXX=clang++
@@ -82,6 +90,7 @@ jobs:
       run: ccache -s
 
     - name: Run tests
+      if: matrix.run_regression_args
       uses: ./.github/actions/run-tests
       with:
         build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
@@ -91,6 +100,7 @@ jobs:
         regressions-exclude: ${{ matrix.exclude_regress }}
 
     - name: Run tests
+      if: matrix.run_regression_args
       uses: ./.github/actions/run-tests
       with:
         build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }}
@@ -107,10 +117,12 @@ jobs:
         build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
 
     - name: Add binary to release
-      if: matrix.store-to-release && startsWith(github.ref, 'refs/tags/')
+      if: matrix.store-to-release-binary && startsWith(github.ref, 'refs/tags/')
       uses: ./.github/actions/add-to-release
       with:
         binary: ${{ steps.configure-and-build.outputs.static-build-dir }}/bin/cvc5
+        binary-ext: ${{ matrix.binary-ext }}
+        binary-name: ${{ matrix.store-to-release-binary }}
         github-token: ${{ secrets.GITHUB_TOKEN }}
 
 

CMakeLists.txt

@@ -198,6 +198,9 @@ add_check_cxx_supression_flag("-Wno-class-memaccess")
 
 if (WIN32)
   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
+
+  # ANTLR uses pragmas that certain versions of MinGW does not support
+  add_check_c_cxx_flag("-Wno-error=unknown-pragmas")
 endif ()
 
 #-----------------------------------------------------------------------------#

src/base/output.h

@@ -29,10 +29,6 @@
 
 namespace cvc5 {
 
-template <class T, class U>
-std::ostream& operator<<(std::ostream& out,
-                         const std::pair<T, U>& p) CVC5_EXPORT;
-
 template <class T, class U>
 std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
   return out << "[" << p.first << "," << p.second << "]";
@@ -56,14 +52,14 @@ class null_streambuf : public std::streambuf
 }; /* class null_streambuf */
 
 /** A null stream-buffer singleton */
-extern null_streambuf null_sb;
+extern null_streambuf null_sb CVC5_EXPORT;
 /** A null output stream singleton */
 extern std::ostream null_os CVC5_EXPORT;
 
-class CVC5_EXPORT Cvc5ostream
+class Cvc5ostream
 {
-  static const std::string s_tab;
-  static const int s_indentIosIndex;
+  static const std::string s_tab CVC5_EXPORT;
+  static const int s_indentIosIndex CVC5_EXPORT;
 
   /** The underlying ostream */
   std::ostream* d_os;
@@ -111,7 +107,23 @@ class CVC5_EXPORT Cvc5ostream
   std::ostream* getStreamPointer() const { return d_os; }
 
   template <class T>
-  Cvc5ostream& operator<<(T const& t) CVC5_EXPORT;
+  Cvc5ostream& operator<<(T const& t)
+  {
+    if (d_os != NULL)
+    {
+      if (d_firstColumn)
+      {
+        d_firstColumn = false;
+        long indent = d_os->iword(s_indentIosIndex);
+        for (long i = 0; i < indent; ++i)
+        {
+          d_os = &(*d_os << s_tab);
+        }
+      }
+      d_os = &(*d_os << t);
+    }
+    return *this;
+  }
 
   // support manipulators, endl, etc..
   Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
@@ -157,22 +169,6 @@ inline Cvc5ostream& pop(Cvc5ostream& stream)
   return stream;
 }
 
-template <class T>
-Cvc5ostream& Cvc5ostream::operator<<(T const& t)
-{
-  if(d_os != NULL) {
-    if(d_firstColumn) {
-      d_firstColumn = false;
-      long indent = d_os->iword(s_indentIosIndex);
-      for(long i = 0; i < indent; ++i) {
-        d_os = &(*d_os << s_tab);
-      }
-    }
-    d_os = &(*d_os << t);
-  }
-  return *this;
-}
-
 /**
  * Does nothing; designed for compilation of non-debug/non-trace
  * builds.  None of these should ever be called in such builds, but we