diff options
| -rw-r--r-- | .appveyor.yml | 39 | ||||
| -rw-r--r-- | .github/disabled-workflows/build-posix.yml | 62 | ||||
| -rw-r--r-- | .github/disabled-workflows/build-windows.yml | 48 | ||||
| -rw-r--r-- | .github/workflows/build-posix-cmake.yml | 62 | ||||
| -rw-r--r-- | .travis.yml | 36 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | README.md | 4 | ||||
| -rw-r--r-- | src/base/acb/acbTest.c | 2 | ||||
| -rw-r--r-- | src/proof/cec/cecSolveG.c | 2 | ||||
| -rw-r--r-- | src/sat/msat/msatClause.c | 2 | ||||
| -rw-r--r-- | src/sat/msat/msatSolverSearch.c | 10 |
11 files changed, 184 insertions, 87 deletions
diff --git a/.appveyor.yml b/.appveyor.yml deleted file mode 100644 index c706ed8c..00000000 --- a/.appveyor.yml +++ /dev/null @@ -1,39 +0,0 @@ -version: '{build}' - -environment: - - matrix: - - - APPVEYOR_BUILD_WORKER_IMAGE: "Visual Studio 2017" - VCVARS_SCRIPT: "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Auxiliary\\Build\\vcvarsall.bat" - VCVARS_PLATFORM: x86 - -init: - - - cmd: '"%VCVARS_SCRIPT%" %VCVARS_PLATFORM%' - -build_script: - - - cmd: | - sed -i 's#ABC_USE_PTHREADS"#ABC_DONT_USE_PTHREADS" /D "_XKEYCHECK_H"#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 - - - cmd: | - appveyor PushArtifact abcspace.dsw - appveyor PushArtifact abclib.dsp - appveyor PushArtifact abcexe.dsp - - - cmd: | - devenv abcspace.dsw /upgrade || dir - appveyor PushArtifact UpgradeLog.htm - msbuild abcspace.sln /m /nologo /p:Configuration=Release - - - cmd: | - _TEST\abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" - - - cmd: | - appveyor PushArtifact _TEST/abc.exe - diff --git a/.github/disabled-workflows/build-posix.yml b/.github/disabled-workflows/build-posix.yml new file mode 100644 index 00000000..aa97aca2 --- /dev/null +++ b/.github/disabled-workflows/build-posix.yml @@ -0,0 +1,62 @@ +on: [push] + +jobs: + + build-posix: + strategy: + matrix: + os: [macos-latest, ubuntu-latest] + use_namespace: [false, true] + + runs-on: ${{ matrix.os }} + + env: + MAKE_ARGS: ${{ matrix.use_namespace && 'ABC_USE_NAMESPACE=xxx' || '' }} + DEMO_ARGS: ${{ matrix.use_namespace && '-DABC_NAMESPACE=xxx' || '' }} + DEMO_GCC: ${{ matrix.use_namespace && 'g++ -x c++' || 'gcc' }} + + steps: + + - name: Git Checkout + uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Install brew dependencies + run: | + HOMEBREW_NO_AUTO_UPDATE=1 brew install readline + if: ${{ contains(matrix.os, 'macos') }} + + - name: Install APT dependencies + run: | + sudo apt install -y libreadline-dev + if: ${{ !contains(matrix.os, 'macos') }} + + - name: Build Executable + run: | + make -j3 ${MAKE_ARGS} abc + + - name: Test Executable + run: | + ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + + - name: Build Library + run: | + make -j3 ${MAKE_ARGS} libabc.a + + - name: Test Library + run: | + ${DEMO_GCC} ${DEMO_ARGS} -Wall -c src/demo.c -o demo.o + g++ -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread + ./demo i10.aig + + - name: Stage Executable + run: | + mkdir staging + cp abc libabc.a staging/ + + - name: Upload pacakge artifact + uses: actions/upload-artifact@v1 + with: + name: package + path: staging/ diff --git a/.github/disabled-workflows/build-windows.yml b/.github/disabled-workflows/build-windows.yml new file mode 100644 index 00000000..6312780d --- /dev/null +++ b/.github/disabled-workflows/build-windows.yml @@ -0,0 +1,48 @@ +on: [push] + +jobs: + + build-windows: + + runs-on: windows-latest + + steps: + + - name: Git Checkout + uses: actions/checkout@v2 + 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: + architecture: x86 + + - 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 + + - name: Test Executable + run: | + _TEST\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/ + copy UpgradeLog.htm staging/ + + - name: Upload pacakge artifact + uses: actions/upload-artifact@v1 + with: + name: package + path: staging/ diff --git a/.github/workflows/build-posix-cmake.yml b/.github/workflows/build-posix-cmake.yml new file mode 100644 index 00000000..68d325b2 --- /dev/null +++ b/.github/workflows/build-posix-cmake.yml @@ -0,0 +1,62 @@ +on: [push] + +jobs: + + build-posix: + strategy: + matrix: + os: [macos-latest, ubuntu-latest] + use_namespace: [false, true] + + runs-on: ${{ matrix.os }} + + env: + MAKE_ARGS: ${{ matrix.use_namespace && '-DABC_USE_NAMESPACE=ON' || '' }} + DEMO_ARGS: ${{ matrix.use_namespace && '-DABC_NAMESPACE=xxx' || '' }} + DEMO_GCC: ${{ matrix.use_namespace && 'g++ -x c++' || 'gcc' }} + + steps: + + - name: Git Checkout + uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Install brew dependencies + run: | + HOMEBREW_NO_AUTO_UPDATE=1 brew install readline ninja + if: ${{ contains(matrix.os, 'macos') }} + + - name: Install APT dependencies + run: | + sudo apt install -y libreadline-dev ninja-build + if: ${{ !contains(matrix.os, 'macos') }} + + - name: Configure CMake + run: | + cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -B build + + - name: Build CMake + run: | + cmake --build build + + - name: Test Executable + run: | + ./build/abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + + - name: Test Library + run: | + ${DEMO_GCC} ${DEMO_ARGS} -Wall -c src/demo.c -o demo.o + g++ -o demo demo.o build/libabc.a -lm -ldl -lreadline -lpthread + ./demo i10.aig + + - name: Stage Executable + run: | + mkdir staging + cp abc libabc.a staging/ + + - name: Upload pacakge artifact + uses: actions/upload-artifact@v1 + with: + name: package + path: staging/ diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index b9add8c4..00000000 --- a/.travis.yml +++ /dev/null @@ -1,36 +0,0 @@ -language: cpp - -matrix: - include: - - - os: linux - addons: - apt: - packages: - - libreadline-dev - - - os: linux - addons: - apt: - packages: - - libreadline-dev - env: - MAKE_ARGS: ABC_USE_NAMESPACE=xxx - DEMO_ARGS: -DABC_NAMESPACE=xxx - - - os: osx - osx_image: xcode10 - addons: - homebrew: - packages: - - readline - -script: - - - make ${MAKE_ARGS} -j2 abc - - ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" - - - make ${MAKE_ARGS} libabc.a - - g++ ${DEMO_ARGS} -Wall -c src/demo.c -o demo.o - - g++ -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread - - ./demo i10.aig @@ -61,9 +61,9 @@ ifneq ($(findstring arm,$(shell uname -m)),) CFLAGS += -DABC_MEMALIGN=4 endif -# compile ABC using the C++ comipler and put everything in the namespace $(ABC_NAMESPACE) +# compile ABC using the C++ compiler and put everything in the namespace $(ABC_NAMESPACE) ifdef ABC_USE_NAMESPACE - CFLAGS += -DABC_NAMESPACE=$(ABC_USE_NAMESPACE) -fpermissive + CFLAGS += -DABC_NAMESPACE=$(ABC_USE_NAMESPACE) -fpermissive -x c++ CC := $(CXX) $(info $(MSG_PREFIX)Compiling in namespace $(ABC_NAMESPACE)) endif @@ -1,5 +1,5 @@ -[](https://travis-ci.org/berkeley-abc/abc) -[](https://ci.appveyor.com/project/berkeley-abc/abc) +[](https://github.com/sterin/abc/actions/workflows/build-posix.yml) +[](https://github.com/sterin/abc/actions/workflows/build-windows.yml) # ABC: System for Sequential Logic Synthesis and Formal Verification diff --git a/src/base/acb/acbTest.c b/src/base/acb/acbTest.c index 1faea72a..6290b88e 100644 --- a/src/base/acb/acbTest.c +++ b/src/base/acb/acbTest.c @@ -466,7 +466,7 @@ Gia_Man_t * Acb_NtkGiaDeriveMiter( Gia_Man_t * pOne, Gia_Man_t * pTwo, int Type ***********************************************************************/ void Acb_OutputFile( char * pFileName, Acb_Ntk_t * pNtkF, int * pModel ) { - char * pFileName0 = pFileName? pFileName : "output"; + const char * pFileName0 = pFileName? pFileName : "output"; FILE * pFile = fopen( pFileName0, "wb" ); if ( pFile == NULL ) { diff --git a/src/proof/cec/cecSolveG.c b/src/proof/cec/cecSolveG.c index 0bb68a7f..c4b01b50 100644 --- a/src/proof/cec/cecSolveG.c +++ b/src/proof/cec/cecSolveG.c @@ -445,7 +445,7 @@ void CecG_ManSatSolverRecycle( Cec_ManSat_t * p ) // memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) ); sat_solver_stop( p->pSat ); } - p->pSat = sat_solver_start(); + p->pSat = (struct sat_solver_t*)sat_solver_start(); assert( 0 <= p->pPars->SolverType && p->pPars->SolverType <= 2 ); sat_solver_set_jftr( p->pSat, p->pPars->SolverType ); //sat_solver_setnvars( p->pSat, 1000 ); // minisat only diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index 6b1b9e98..3d1fa2fc 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -522,7 +522,7 @@ void Msat_ClausePrintSymbols( Msat_Clause_t * pC ) // if ( pC->fLearned ) // printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); for ( i = 0; i < (int)pC->nSize; i++ ) - printf(" "L_LIT, L_lit(pC->pData[i])); + printf(" " L_LIT, L_lit(pC->pData[i])); } printf( "\n" ); } diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index b3190e39..2eda5038 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -52,7 +52,7 @@ int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) { assert( Msat_QueueReadSize(p->pQueue) == 0 ); if ( p->fVerbose ) - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "assume(" L_LIT ")\n", L_ind, L_lit(Lit)); Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) ); // assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 ); // assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars ); @@ -83,7 +83,7 @@ void Msat_SolverUndoOne( Msat_Solver_t * p ) Msat_OrderVarUnassigned( p->pOrder, Var ); if ( p->fVerbose ) - printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "unbind(" L_LIT")\n", L_ind, L_lit(Lit)); } /**Function************************************************************* @@ -107,7 +107,7 @@ void Msat_SolverCancel( Msat_Solver_t * p ) { Msat_Lit_t Lit; Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); - printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "cancel(" L_LIT ")\n", L_ind, L_lit(Lit)); } } for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- ) @@ -188,7 +188,7 @@ int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) if ( p->fVerbose ) { // printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit)); - printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit)); + printf(L_IND "bind(" L_LIT ") ", L_ind, L_lit(Lit)); Msat_ClausePrintSymbols( pC ); } p->pAssigns[Var] = Lit; @@ -513,7 +513,7 @@ void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * nReasonSize = Msat_IntVecReadSize( vLits_out ); pReasonArray = Msat_IntVecReadArray( vLits_out ); for ( j = 0; j < nReasonSize; j++ ) - printf(" "L_LIT, L_lit(pReasonArray[j])); + printf(" " L_LIT, L_lit(pReasonArray[j])); printf(" } at level %d\n", *pLevel_out); } } |