Fix CI: modernize Windows build and deduplicate triggers

.github/workflows/build-posix-cmake.yml

@@ -2,6 +2,7 @@ name: Build Posix CMake
 
 on:
   push:
+    branches: [main, master]
   pull_request:
 
 jobs:

.github/workflows/build-posix.yml

@@ -2,6 +2,7 @@ name: Build Posix
 
 on:
   push:
+    branches: [main, master]
   pull_request:
 
 jobs:

.github/workflows/build-windows.yml

@@ -2,63 +2,53 @@ name: Build Windows
 
 on:
   push:
+    branches: [main, master]
   pull_request:
 
 jobs:
 
   build-windows:
 
-    runs-on: windows-2019
+    runs-on: windows-latest
+
+    defaults:
+      run:
+        shell: msys2 {0}
 
     steps:
 
+    - name: Setup MSYS2
+      uses: msys2/setup-msys2@v2
+      with:
+        msystem: MINGW64
+        update: false
+        install: >-
+          mingw-w64-x86_64-gcc
+          mingw-w64-x86_64-cmake
+          mingw-w64-x86_64-ninja
+          make
+
     - name: Git Checkout
       uses: actions/checkout@v4
       with:
         submodules: recursive
 
-    - name: Prepare MSVC
-      uses: bus1/cabuild/action/msdevshell@v1
-      with:
-        architecture: x86
+    - name: Configure CMake
+      run: |
+        ABC_USE_STDINT_H=1 cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_FLAGS="-DWIN32 -DWIN32_NO_DLL" -DCMAKE_CXX_FLAGS="-DWIN32 -DWIN32_NO_DLL" -DREADLINE_FOUND=FALSE -DABC_SKIP_TESTS=1 -B build
 
-    - name: Upgrade project files to latest Visual Studio, ignoring upgrade errors, and build
+    - name: Build
       run: |
-        devenv abcspace.dsw /upgrade
-        # Fix the upgraded vcxproj files to use C++17
-        if (Test-Path abclib.vcxproj) {
-            $content = Get-Content abclib.vcxproj -Raw
-            if ($content -match '<LanguageStandard>') {
-                $content = $content -replace '<LanguageStandard>Default</LanguageStandard>', '<LanguageStandard>stdcpp17</LanguageStandard>'
-            } else {
-                # Add LanguageStandard if it doesn't exist
-                $content = $content -replace '(<ClCompile>)', '$1<LanguageStandard>stdcpp17</LanguageStandard>'
-            }
-            Set-Content abclib.vcxproj -NoNewline $content
-        }
-        if (Test-Path abcexe.vcxproj) {
-            $content = Get-Content abcexe.vcxproj -Raw
-            if ($content -match '<LanguageStandard>') {
-                $content = $content -replace '<LanguageStandard>Default</LanguageStandard>', '<LanguageStandard>stdcpp17</LanguageStandard>'
-            } else {
-                # Add LanguageStandard if it doesn't exist
-                $content = $content -replace '(<ClCompile>)', '$1<LanguageStandard>stdcpp17</LanguageStandard>'
-            }
-            Set-Content abcexe.vcxproj -NoNewline $content
-        }
-        msbuild abcspace.sln /m /nologo /v:m /p:Configuration=Release /p:UseMultiToolTask=true /p:PlatformToolset=v142 /p:PreprocessorDefinitions="_WINSOCKAPI_"
-        if ($LASTEXITCODE -ne 0) { throw "Build failed with exit code $LASTEXITCODE" }
+        cmake --build build
 
     - name: Test Executable
       run: |
-        copy lib\x86\pthreadVC2.dll _TEST\
-        .\_TEST\abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
-        if ($LASTEXITCODE -ne 0) { throw "Test failed with exit code $LASTEXITCODE" }
+        ./build/abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
 
     - name: Stage Executable
       run: |
-        mkdir staging
-        copy _TEST\abc.exe staging\
+        mkdir -p staging
+        cp build/abc.exe staging/
 
     - name: Upload package artifact
       uses: actions/upload-artifact@v4

Makefile

@@ -141,11 +141,26 @@ endif
 # LIBS := -ldl -lrt
 LIBS += -lm
 ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD NetBSD))
-  LIBS += -ldl
+  ifeq ($(findstring MINGW,$(OS)),)
+    ifeq ($(findstring MSYS,$(OS)),)
+      LIBS += -ldl
+    endif
+  endif
 endif
 
 ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD NetBSD Darwin))
-   LIBS += -lrt
+  ifeq ($(findstring MINGW,$(OS)),)
+    ifeq ($(findstring MSYS,$(OS)),)
+      LIBS += -lrt
+    endif
+  endif
+endif
+
+ifneq ($(findstring MINGW,$(OS)),)
+  LIBS += -lshlwapi
+endif
+ifneq ($(findstring MSYS,$(OS)),)
+  LIBS += -lshlwapi
 endif
 
 ifdef ABC_USE_LIBSTDCXX

src/base/abci/abc.c

@@ -32668,7 +32668,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzhb" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzhb" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32789,9 +32789,21 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->pInvFileName = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'X':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" );
+                goto usage;
+            }
+            pPars->pCexFilePrefix = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'a':
             pPars->fSolveAll ^= 1;
             break;
+        case 'l':
+            pPars->fAnytime ^= 1;
+            break;
         case 'x':
             pPars->fStoreCex ^= 1;
             break;
@@ -32899,7 +32911,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-X <prefix>] [-axrmuyfqipdegjonctkvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -32914,7 +32926,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n",                          pPars->nRandomSeed );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n",                                          pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n",                                    pPars->pInvFileName ? pPars->pInvFileName : "default name" );
+    Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as <pref>*.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled");
     Abc_Print( -2, "\t-a     : toggle solving all outputs even if one of them is SAT [default = %s]\n",      pPars->fSolveAll? "yes": "no" );
+    Abc_Print( -2, "\t-l     : toggle anytime schedule when solving all outputs [default = %s]\n",           pPars->fAnytime? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",              pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n",                    pPars->fMonoCnf? "yes": "no" );

src/base/cmd/cmdHist.c

@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_USE_HISTORY 1
+// #define ABC_USE_HISTORY 1
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///

src/misc/util/utilPth.c

@@ -51,7 +51,7 @@ static inline int nanosleep(const struct timespec *req, struct timespec *rem) {
 #include <atomic>
 using namespace std;
 #else
-#ifndef _WIN32
+#if !defined(_WIN32) || defined(__MINGW32__)
 #include <stdatomic.h>
 #else
 // MSVC doesn't have stdatomic.h, use Interlocked functions instead

src/proof/pdr/pdr.h

@@ -72,6 +72,7 @@ struct Pdr_Par_t_
     int fSilent;          // totally silent execution
     int fSolveAll;        // do not stop when found a SAT output
     int fStoreCex;        // enable storing counter-examples in MO mode
+    int fAnytime;         // enable anytime scheduling
     int fUseBridge;       // use bridge interface
     int fUsePropOut;      // use property output
     int nFailOuts;        // the number of failed outputs
@@ -86,6 +87,7 @@ struct Pdr_Par_t_
     abctime timeLastSolved; // the time when the last output was solved
     Vec_Int_t * vOutMap;  // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
     char * pInvFileName;  // invariable file name
+    char * pCexFilePrefix;  // CEX output prefix
     int fBlocking;        // clause pushing with blocking
 };
 
@@ -98,6 +100,7 @@ struct Pdr_Par_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== pdrCore.c ==========================================================*/
+extern void               Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex );
 extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
 extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );