diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 2d0894364..c9f5e2b4f 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -17,14 +17,6 @@ jobs: with: submodules: recursive - - name: Process project files to compile on Github Actions - run: | - sed -i 's#ABC_USE_PTHREADS\"#ABC_DONT_USE_PTHREADS\" /D \"_ALLOW_KEYWORD_MACROS=1\"#g' *.dsp - awk 'BEGIN { del=0; } /# Begin Group "uap"/ { del=1; } /# End Group/ { if( del > 0 ) {del=0; next;} } del==0 {print;} ' abclib.dsp > tmp.dsp - copy tmp.dsp abclib.dsp - del tmp.dsp - unix2dos *.dsp - - name: Prepare MSVC uses: bus1/cabuild/action/msdevshell@v1 with: @@ -32,20 +24,43 @@ jobs: - name: Upgrade project files to latest Visual Studio, ignoring upgrade errors, and build run: | - devenv abcspace.dsw /upgrade ; if (-not $? ) { cat UpgradeLog.htm } - msbuild abcspace.sln /m /nologo /p:Configuration=Release /p:PlatformTarget=x86 + 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 '') { + $content = $content -replace 'Default', 'stdcpp17' + } else { + # Add LanguageStandard if it doesn't exist + $content = $content -replace '()', '$1stdcpp17' + } + Set-Content abclib.vcxproj -NoNewline $content + } + if (Test-Path abcexe.vcxproj) { + $content = Get-Content abcexe.vcxproj -Raw + if ($content -match '') { + $content = $content -replace 'Default', 'stdcpp17' + } else { + # Add LanguageStandard if it doesn't exist + $content = $content -replace '()', '$1stdcpp17' + } + 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" } - name: Test Executable run: | - _TEST\abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + 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" } - name: Stage Executable run: | - mkdir staging - copy _TEST/abc.exe staging/ - copy UpgradeLog.htm staging/ + mkdir staging + copy _TEST\abc.exe staging\ - - name: Upload pacakge artifact + - name: Upload package artifact uses: actions/upload-artifact@v4 with: name: package-windows diff --git a/abcexe.dsp b/abcexe.dsp index 9d5152fc2..80f0f1252 100644 --- a/abcexe.dsp +++ b/abcexe.dsp @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /c +# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -67,7 +67,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /GZ /c +# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe diff --git a/abclib.dsp b/abclib.dsp index f7c80a25b..7b36b34e8 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -41,7 +41,7 @@ RSC=rc.exe # PROP Intermediate_Dir "ReleaseLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c -# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /c +# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -64,7 +64,7 @@ LIB32=link.exe -lib # PROP Intermediate_Dir "DebugLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c -# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /GZ /c +# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe @@ -513,6 +513,10 @@ SOURCE=.\src\base\abci\abcVerify.c SOURCE=.\src\base\abci\abcXsim.c # End Source File +# Begin Source File + +SOURCE=.\src\base\abci\abcTopo.c +# End Source File # End Group # Begin Group "cmd" @@ -709,6 +713,10 @@ SOURCE=.\src\base\io\ioWriteSmv.c SOURCE=.\src\base\io\ioWriteVerilog.c # End Source File +# Begin Source File + +SOURCE=.\src\base\io\ioJsonc.c +# End Source File # End Group # Begin Group "main" @@ -2153,6 +2161,18 @@ SOURCE=.\src\sat\bmc\bmcMulti.c SOURCE=.\src\sat\bmc\bmcUnroll.c # End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj7.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj8.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj9.c +# End Source File # End Group # Begin Group "bsat2" @@ -3329,6 +3349,49 @@ SOURCE=.\src\opt\fxu\fxuSingle.c SOURCE=.\src\opt\fxu\fxuUpdate.c # End Source File +# Begin Group "untk" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\untk\NtkCmd.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\untk\Netlist.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\untk\NtkNtk.cpp +# End Source File +# End Group +# Begin Group "ufar" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarCmd.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarMgr.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarPth.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarPth.h +# End Source File +# End Group +# Begin Group "util" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\util\util.cpp +# End Source File # End Group # Begin Group "rar" @@ -4445,6 +4508,10 @@ SOURCE=.\src\map\if\acd\ac_wrapper.cpp SOURCE=.\src\map\if\ifUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\map\if\ifDecJ.c +# End Source File # End Group # Begin Group "amap" @@ -5021,6 +5088,30 @@ SOURCE=.\src\misc\util\utilSort.c SOURCE=.\src\misc\util\utilTruth.h # End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilBipart.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilLinear.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMiniver.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMulSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilAigSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilNet.c +# End Source File # End Group # Begin Group "nm" @@ -6241,6 +6332,22 @@ SOURCE=.\src\aig\gia\giaUnate.c SOURCE=.\src\aig\gia\giaUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaDecGraph.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaAgi.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaLutCas.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaMulFind3.c +# End Source File # End Group # Begin Group "miniaig" @@ -6474,7 +6581,6 @@ SOURCE=.\src\bool\rpo\rpo.c SOURCE=.\src\bool\rpo\rpo.h # End Source File # End Group -# End Group # Begin Group "prove" # PROP Default_Filter "" @@ -6570,6 +6676,7 @@ SOURCE=.\src\proof\cec\cecSweep.c SOURCE=.\src\proof\cec\cecSynth.c # End Source File # End Group +# End Group # Begin Group "dch" # PROP Default_Filter "" @@ -7213,12 +7320,14 @@ SOURCE=.\src\proof\acec\acecUtil.c SOURCE=.\src\proof\acec\acecXor.c # End Source File -# End Group + # End Group # End Group # Begin Group "Header Files" # PROP Default_Filter "h;hpp;hxx;hm;inl" # End Group +# End Group +# End Group # End Target # End Project diff --git a/src/aig/gia/giaLutCas.c b/src/aig/gia/giaLutCas.c index 340996565..dd18c7544 100644 --- a/src/aig/gia/giaLutCas.c +++ b/src/aig/gia/giaLutCas.c @@ -19,6 +19,10 @@ ***********************************************************************/ #include "gia.h" + +#ifdef _WIN32 +#include +#endif #include "sat/cnf/cnf.h" #include "misc/util/utilTruth.h" #include "sat/cadical/cadicalSolver.h" @@ -183,9 +187,13 @@ Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLu if ( Seed ) srand(Seed); else { +#ifdef _WIN32 + unsigned int seed = (unsigned int)GetTickCount(); +#else struct timespec ts; clock_gettime(CLOCK_REALTIME, &ts); unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec); +#endif srand(seed); } int fOwnPerm = (pPermStr == NULL); diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 3ab099655..fbe5c1f6c 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -31,8 +31,10 @@ #ifdef _WIN32 +#ifndef _MSC_VER #define inline __inline // compatible with MS VS 6.0 #endif +#endif /*---------------------------------------------------------------------------*/ /* Nested includes */ diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 5e1651d2e..c5a0327e0 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -31,7 +31,9 @@ #ifdef _WIN32 #ifndef __MINGW32__ +#ifndef _MSC_VER #define inline __inline // compatible with MS VS 6.0 +#endif #pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression #pragma warning(disable : 4200) // warning C4200: nonstandard extension used : zero-sized array in struct/union #pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data diff --git a/src/misc/util/utilAigSim.c b/src/misc/util/utilAigSim.c index a12d71d81..3bbde59a8 100644 --- a/src/misc/util/utilAigSim.c +++ b/src/misc/util/utilAigSim.c @@ -25,7 +25,44 @@ #include #include #include +#ifdef _WIN32 +#include +#define mkstemp(p) _mktemp_s(p, strlen(p)+1) +#else #include // mkstemp(), close(), unlink() +#endif + +#ifdef _WIN32 +// Windows doesn't have __builtin_ctzll, implement it using portable algorithm +static inline int __builtin_ctzll(uint64_t x) { + if (x == 0) return 64; + unsigned int n = 0; + if ((x & 0xFFFFFFFFULL) == 0) { + n += 32; + x >>= 32; + } + if ((x & 0xFFFFULL) == 0) { + n += 16; + x >>= 16; + } + if ((x & 0xFFULL) == 0) { + n += 8; + x >>= 8; + } + if ((x & 0xFULL) == 0) { + n += 4; + x >>= 4; + } + if ((x & 0x3ULL) == 0) { + n += 2; + x >>= 2; + } + if ((x & 0x1ULL) == 0) { + n += 1; + } + return n; +} +#endif #define AIGSIM_LIBRARY_ONLY @@ -147,6 +184,17 @@ static AigMan* Aig_ManLoadAigerBinary(const char *filename, int verbose) { static inline uint64_t u64_mask_n(int nBits) { return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull)); } + +#ifdef _WIN32 +// Windows doesn't support __int128, so we limit to 32 variables on Windows +static void u128_to_dec(uint64_t x, char *buf, size_t cap) { + char tmp[64]; int n = 0; + if (!x) { snprintf(buf, cap, "0"); return; } + while (x && n < (int)sizeof(tmp)) { tmp[n++] = (char)('0' + (unsigned)(x % 10)); x /= 10; } + int k = 0; while (n && k + 1 < (int)cap) buf[k++] = tmp[--n]; + buf[k] = 0; +} +#else static void u128_to_dec(unsigned __int128 x, char *buf, size_t cap) { char tmp[64]; int n = 0; if (!x) { snprintf(buf, cap, "0"); return; } @@ -154,6 +202,7 @@ static void u128_to_dec(unsigned __int128 x, char *buf, size_t cap) { int k = 0; while (n && k + 1 < (int)cap) buf[k++] = tmp[--n]; buf[k] = 0; } +#endif enum { NW = 64, BATCH = NW * 64 }; // 4096 patterns/round @@ -334,7 +383,16 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); +#ifdef _WIN32 + // Windows doesn't support __int128, limit to 32 variables + if (nVars > 32) { + fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + return 0; + } + const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; +#else const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; +#endif uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); uint32_t *co2 = ABC_ALLOC(uint32_t, p2->nCos); @@ -348,12 +406,21 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; +#ifdef _WIN32 + uint64_t patsDone = 0; +#else unsigned __int128 patsDone = 0; +#endif clock_t t0 = clock(); +#ifdef _WIN32 + for (uint64_t base = 0; base < combs; base += BATCH) { + uint64_t remain = combs - base; +#else for (unsigned __int128 base = 0; base < combs; base += BATCH) { unsigned __int128 remain = combs - base; +#endif int nThis = (remain < BATCH) ? (int)remain : BATCH; int left = nThis; @@ -454,7 +521,16 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); +#ifdef _WIN32 + // Windows doesn't support __int128, limit to 32 variables + if (nVars > 32) { + fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + return 0; + } + const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; +#else const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; +#endif // Precompute AIG CO literals uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); @@ -475,12 +551,21 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; +#ifdef _WIN32 + uint64_t patsDone = 0; +#else unsigned __int128 patsDone = 0; +#endif clock_t t0 = clock(); +#ifdef _WIN32 + for (uint64_t base = 0; base < combs; base += BATCH) { + uint64_t remain = combs - base; +#else for (unsigned __int128 base = 0; base < combs; base += BATCH) { unsigned __int128 remain = combs - base; +#endif int nThis = (remain < BATCH) ? (int)remain : BATCH; int left = nThis; diff --git a/src/misc/util/utilNet.c b/src/misc/util/utilNet.c index db21c8c3b..5d3173bb8 100755 --- a/src/misc/util/utilNet.c +++ b/src/misc/util/utilNet.c @@ -22,7 +22,11 @@ #include #include #include +#ifdef _WIN32 +#include +#else #include +#endif #include #include "abc_global.h" @@ -1083,7 +1087,11 @@ tn_vi * Tn_ParseSolution( const char * pFileName ) assert( 0 ); } fclose( pFile ); +#ifdef _WIN32 + _unlink( pFileName ); +#else unlink( pFileName ); +#endif return vRes; } tn_vi * Tn_SolveSat( const char * pFileNameIn, const char * pFileNameOut, int Seed, int TimeOut, int fVerbose ) diff --git a/src/misc/util/utilPrefix.cpp b/src/misc/util/utilPrefix.cpp index 50db0723c..cde54a42e 100644 --- a/src/misc/util/utilPrefix.cpp +++ b/src/misc/util/utilPrefix.cpp @@ -37,6 +37,7 @@ #include #include #include +#include //#include //#include //#include diff --git a/src/misc/util/utilPth.c b/src/misc/util/utilPth.c index aeb912597..940f7929a 100644 --- a/src/misc/util/utilPth.c +++ b/src/misc/util/utilPth.c @@ -23,6 +23,22 @@ #include #include +#ifdef _WIN32 +#include +#include +// nanosleep implementation for Windows +static inline int nanosleep(const struct timespec *req, struct timespec *rem) { + LARGE_INTEGER li; + li.QuadPart = -((LONGLONG)req->tv_sec * 10000000 + req->tv_nsec / 100); + HANDLE timer = CreateWaitableTimer(NULL, TRUE, NULL); + if (!timer) return -1; + SetWaitableTimer(timer, &li, 0, NULL, NULL, 0); + WaitForSingleObject(timer, INFINITE); + CloseHandle(timer); + return 0; +} +#endif + #ifdef ABC_USE_PTHREADS #ifdef _WIN32 @@ -35,7 +51,23 @@ #include using namespace std; #else +#ifndef _WIN32 #include +#else +// MSVC doesn't have stdatomic.h, use Interlocked functions instead +#define atomic_bool volatile LONG +#define atomic_int volatile LONG +#define atomic_store(obj, val) InterlockedExchange((LONG*)obj, val) +#define atomic_load(obj) (*(volatile LONG*)obj) +#define atomic_compare_exchange_strong(obj, expected, desired) \ + (InterlockedCompareExchange((LONG*)obj, desired, *expected) == *expected ? \ + (*expected = desired, 1) : (*expected = *(volatile LONG*)obj, 0)) +#define atomic_store_explicit(obj, val, order) InterlockedExchange((LONG*)obj, val) +#define atomic_load_explicit(obj, order) (*(volatile LONG*)obj) +#define memory_order_acquire 0 +#define memory_order_release 0 +#define memory_order_seq_cst 0 +#endif #include #endif diff --git a/src/misc/util/winsock_compat.h b/src/misc/util/winsock_compat.h new file mode 100644 index 000000000..501ec5d43 --- /dev/null +++ b/src/misc/util/winsock_compat.h @@ -0,0 +1,22 @@ +/* + * winsock_compat.h + * + * Compatibility header for timeval on Windows + * This must be included BEFORE windows.h to prevent winsock.h forward declaration conflicts + */ + +#ifndef SRC_MISC_UTIL_WINSOCK_COMPAT_H_ +#define SRC_MISC_UTIL_WINSOCK_COMPAT_H_ + +#ifdef _WIN32 + +// Define timeval before windows.h includes winsock.h +// This prevents winsock.h from forward declaring it as an incomplete type +struct timeval { + long tv_sec; + long tv_usec; +}; + +#endif /* _WIN32 */ + +#endif /* SRC_MISC_UTIL_WINSOCK_COMPAT_H_ */ \ No newline at end of file diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 162105c40..5bedeeca6 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -5,6 +5,12 @@ * Author: Yen-Sheng Ho */ +#ifdef _WIN32 +#include +#else +#include +#endif + #include #include #include diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index ea565b5e4..924ad0d6b 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -14,7 +14,11 @@ #include #include +#ifdef _WIN32 +#include +#else #include +#endif #include #include diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h index dad82f6a2..ad2f9c477 100755 --- a/src/opt/ufar/UfarMgr.h +++ b/src/opt/ufar/UfarMgr.h @@ -15,7 +15,22 @@ #include #include #include +#ifdef _WIN32 +// Define timeval before windows.h to prevent winsock.h forward declaration conflicts +#ifndef _TIMEVAL_DEFINED +#define _TIMEVAL_DEFINED +struct timeval { + long tv_sec; + long tv_usec; +}; +#endif +#ifndef WIN32_LEAN_AND_MEAN +#define WIN32_LEAN_AND_MEAN +#endif +#include +#else #include +#endif #include "misc/util/abc_namespaces.h" diff --git a/src/opt/ufar/UfarPth.cpp b/src/opt/ufar/UfarPth.cpp index 6df45657f..f2ef59374 100755 --- a/src/opt/ufar/UfarPth.cpp +++ b/src/opt/ufar/UfarPth.cpp @@ -1,8 +1,12 @@ #include "misc/util/abc_namespaces.h" +#ifdef _WIN32 +#include "../lib/pthread.h" +#else #include #include +#endif #include "sat/bmc/bmc.h" #include "proof/pdr/pdr.h" diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 0ee5e5fd7..62ab1e343 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -5,8 +5,12 @@ * Author: Yen-Sheng Ho */ +#ifdef _WIN32 +#include +#else #include #include +#endif #include #include diff --git a/src/opt/util/util.cpp b/src/opt/util/util.cpp index df5de2fd8..a4b3ceba5 100644 --- a/src/opt/util/util.cpp +++ b/src/opt/util/util.cpp @@ -7,7 +7,11 @@ #include #include +#ifdef _WIN32 +#include +#else #include +#endif #ifdef __linux__ #include diff --git a/src/opt/util/util.h b/src/opt/util/util.h index 24dd153a1..2153e70d0 100755 --- a/src/opt/util/util.h +++ b/src/opt/util/util.h @@ -16,7 +16,37 @@ #include #include +#ifdef _WIN32 +// Define timeval before windows.h to prevent winsock.h forward declaration conflicts +#ifndef _TIMEVAL_DEFINED +#define _TIMEVAL_DEFINED +struct timeval { + long tv_sec; + long tv_usec; +}; +#endif +#ifndef WIN32_LEAN_AND_MEAN +#define WIN32_LEAN_AND_MEAN +#endif +#include + +static inline int gettimeofday(struct timeval *tv, struct timezone *tz) { + if (tv) { + FILETIME ft; + GetSystemTimeAsFileTime(&ft); + ULARGE_INTEGER uli; + uli.LowPart = ft.dwLowDateTime; + uli.HighPart = ft.dwHighDateTime; + ULONGLONG time_in_us = (uli.QuadPart - 116444736000000000ULL) / 10ULL; + tv->tv_sec = (long)(time_in_us / 1000000ULL); + tv->tv_usec = (long)(time_in_us % 1000000ULL); + } + (void)tz; + return 0; +} +#else #include +#endif #include "misc/util/abc_namespaces.h" diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c index 89b680684..3a65f17dd 100644 --- a/src/proof/ssw/sswPart.c +++ b/src/proof/ssw/sswPart.c @@ -26,7 +26,20 @@ #ifdef ABC_USE_PTHREADS #ifdef _WIN32 +#include +#include #include "../lib/pthread.h" +// nanosleep implementation for Windows +static inline int nanosleep(const struct timespec *req, struct timespec *rem) { + LARGE_INTEGER li; + li.QuadPart = -((LONGLONG)req->tv_sec * 10000000 + req->tv_nsec / 100); + HANDLE timer = CreateWaitableTimer(NULL, TRUE, NULL); + if (!timer) return -1; + SetWaitableTimer(timer, &li, 0, NULL, NULL, 0); + WaitForSingleObject(timer, INFINITE); + CloseHandle(timer); + return 0; +} #else #include #include @@ -36,7 +49,23 @@ #include using namespace std; #else +#ifndef _WIN32 #include +#else +// MSVC doesn't have stdatomic.h, use Interlocked functions instead +#define atomic_bool volatile LONG +#define atomic_int volatile LONG +#define atomic_store(obj, val) InterlockedExchange((LONG*)obj, val) +#define atomic_load(obj) (*(volatile LONG*)obj) +#define atomic_compare_exchange_strong(obj, expected, desired) \ + (InterlockedCompareExchange((LONG*)obj, desired, *expected) == *expected ? \ + (*expected = desired, 1) : (*expected = *(volatile LONG*)obj, 0)) +#define atomic_store_explicit(obj, val, order) InterlockedExchange((LONG*)obj, val) +#define atomic_load_explicit(obj, order) (*(volatile LONG*)obj) +#define memory_order_acquire 0 +#define memory_order_release 0 +#define memory_order_seq_cst 0 +#endif #include #endif diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index b82f35777..1b05c7605 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -27,6 +27,10 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +#endif + ABC_NAMESPACE_IMPL_START @@ -1084,9 +1088,13 @@ Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize, int Seed ) if ( Seed ) srand(Seed); else { +#ifdef _WIN32 + unsigned int seed = (unsigned int)GetTickCount(); +#else struct timespec ts; clock_gettime(CLOCK_REALTIME, &ts); unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec); +#endif srand(seed); } for ( int i = 0; i < 1000; i++ ) { diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index a80f97330..b0c5391a9 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -27,6 +27,11 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +typedef __int64 int64_t; +#endif + #define KISSAT_UNSAT 20 #define KISSAT_SAT 10 #define KISSAT_UNDEC 0 diff --git a/src/sat/bmc/bmcMaj9.c b/src/sat/bmc/bmcMaj9.c index cc15c153a..ea8ac9d17 100644 --- a/src/sat/bmc/bmcMaj9.c +++ b/src/sat/bmc/bmcMaj9.c @@ -27,7 +27,12 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +typedef __int64 int64_t; +#else #include +#endif #include #define KISSAT_UNSAT 20