mirror of https://github.com/YosysHQ/abc.git
Fix(Workflow): Bring windows build back to life
Signed-off-by: JingrenWang <wjrforcyber@163.com>
This commit is contained in:
JingrenWang
parent
57544eb9ca
commit
ad267aca8a
|
|
@ -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 '<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" }
|
||||
|
||||
- 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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
117
abclib.dsp
117
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
|
||||
|
|
|
|||
|
|
@ -19,6 +19,10 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#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);
|
||||
|
|
|
|||
|
|
@ -31,8 +31,10 @@
|
|||
|
||||
|
||||
#ifdef _WIN32
|
||||
#ifndef _MSC_VER
|
||||
#define inline __inline // compatible with MS VS 6.0
|
||||
#endif
|
||||
#endif
|
||||
|
||||
/*---------------------------------------------------------------------------*/
|
||||
/* Nested includes */
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -25,7 +25,44 @@
|
|||
#include <assert.h>
|
||||
#include <ctype.h>
|
||||
#include <time.h>
|
||||
#ifdef _WIN32
|
||||
#include <io.h>
|
||||
#define mkstemp(p) _mktemp_s(p, strlen(p)+1)
|
||||
#else
|
||||
#include <unistd.h> // 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;
|
||||
|
|
|
|||
|
|
@ -22,7 +22,11 @@
|
|||
#include <stdlib.h>
|
||||
#include <string.h>
|
||||
#include <assert.h>
|
||||
#ifdef _WIN32
|
||||
#include <io.h>
|
||||
#else
|
||||
#include <unistd.h>
|
||||
#endif
|
||||
#include <time.h>
|
||||
|
||||
#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 )
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@
|
|||
#include <random>
|
||||
#include <climits>
|
||||
#include <iomanip>
|
||||
#include <string>
|
||||
//#include <cstdlib>
|
||||
//#include <cstring>
|
||||
//#include <cstdio>
|
||||
|
|
|
|||
|
|
@ -23,6 +23,22 @@
|
|||
#include <stdlib.h>
|
||||
#include <assert.h>
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#include <time.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;
|
||||
}
|
||||
#endif
|
||||
|
||||
#ifdef ABC_USE_PTHREADS
|
||||
|
||||
#ifdef _WIN32
|
||||
|
|
@ -35,7 +51,23 @@
|
|||
#include <atomic>
|
||||
using namespace std;
|
||||
#else
|
||||
#ifndef _WIN32
|
||||
#include <stdatomic.h>
|
||||
#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 <stdbool.h>
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -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_ */
|
||||
|
|
@ -5,6 +5,12 @@
|
|||
* Author: Yen-Sheng Ho
|
||||
*/
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#else
|
||||
#include <sys/time.h>
|
||||
#endif
|
||||
|
||||
#include <iostream>
|
||||
#include <iomanip>
|
||||
#include <climits>
|
||||
|
|
|
|||
|
|
@ -14,7 +14,11 @@
|
|||
#include <array>
|
||||
#include <regex>
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#else
|
||||
#include <sys/wait.h>
|
||||
#endif
|
||||
|
||||
#include <base/wlc/wlc.h>
|
||||
#include <sat/cnf/cnf.h>
|
||||
|
|
|
|||
|
|
@ -15,7 +15,22 @@
|
|||
#include <sstream>
|
||||
#include <iostream>
|
||||
#include <memory>
|
||||
#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 <windows.h>
|
||||
#else
|
||||
#include <sys/time.h>
|
||||
#endif
|
||||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,12 @@
|
|||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
|
||||
#ifdef _WIN32
|
||||
#include "../lib/pthread.h"
|
||||
#else
|
||||
#include <pthread.h>
|
||||
#include <unistd.h>
|
||||
#endif
|
||||
|
||||
#include "sat/bmc/bmc.h"
|
||||
#include "proof/pdr/pdr.h"
|
||||
|
|
|
|||
|
|
@ -5,8 +5,12 @@
|
|||
* Author: Yen-Sheng Ho
|
||||
*/
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#else
|
||||
#include <unistd.h>
|
||||
#include <sys/wait.h>
|
||||
#endif
|
||||
#include <fstream>
|
||||
|
||||
#include <base/wlc/wlc.h>
|
||||
|
|
|
|||
|
|
@ -7,7 +7,11 @@
|
|||
|
||||
#include <iomanip>
|
||||
#include <csignal>
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#else
|
||||
#include <unistd.h>
|
||||
#endif
|
||||
|
||||
#ifdef __linux__
|
||||
#include <sys/prctl.h>
|
||||
|
|
|
|||
|
|
@ -16,7 +16,37 @@
|
|||
#include <map>
|
||||
#include <vector>
|
||||
|
||||
#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 <windows.h>
|
||||
|
||||
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 <sys/time.h>
|
||||
#endif
|
||||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -26,7 +26,20 @@
|
|||
#ifdef ABC_USE_PTHREADS
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#include <time.h>
|
||||
#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 <pthread.h>
|
||||
#include <unistd.h>
|
||||
|
|
@ -36,7 +49,23 @@
|
|||
#include <atomic>
|
||||
using namespace std;
|
||||
#else
|
||||
#ifndef _WIN32
|
||||
#include <stdatomic.h>
|
||||
#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 <stdbool.h>
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -27,6 +27,10 @@
|
|||
#include "base/main/main.h"
|
||||
#include "base/cmd/cmd.h"
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#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++ ) {
|
||||
|
|
|
|||
|
|
@ -27,6 +27,11 @@
|
|||
#include "base/main/main.h"
|
||||
#include "base/cmd/cmd.h"
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
typedef __int64 int64_t;
|
||||
#endif
|
||||
|
||||
#define KISSAT_UNSAT 20
|
||||
#define KISSAT_SAT 10
|
||||
#define KISSAT_UNDEC 0
|
||||
|
|
|
|||
|
|
@ -27,7 +27,12 @@
|
|||
#include "base/main/main.h"
|
||||
#include "base/cmd/cmd.h"
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
typedef __int64 int64_t;
|
||||
#else
|
||||
#include <unistd.h>
|
||||
#endif
|
||||
#include <limits.h>
|
||||
|
||||
#define KISSAT_UNSAT 20
|
||||
|
|
|
|||
Loading…
Reference in New Issue