diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 34 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 1 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilPrime.c | 2 | ||||
| -rw-r--r-- | src/sat/satoko/utils/sdbl.h | 4 |
5 files changed, 42 insertions, 3 deletions
@@ -5543,6 +5543,10 @@ SOURCE=.\src\proof\cec\cecSolve.c # End Source File # Begin Source File +SOURCE=.\src\proof\cec\cecSolveG.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\cec\cecSplit.c # End Source File # Begin Source File diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 2409df2e..2762dbac 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2460,6 +2460,40 @@ Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ComputeTest() +{ + char * pStart, Line [1000]; float Total = 0; + char * pFileName = "data.txt"; + FILE * pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { printf( "Input file \"%s\" cannot be opened.\n", pFileName ); return; } + while ( fgets( Line, 1000, pFile ) != NULL ) + { + if ( !strstr(Line, "xxx") ) + continue; + if ( !strstr(Line, "yyy") ) + continue; + //printf( "%s", Line ); + pStart = strstr(Line, "zzz"); + if ( pStart == NULL ) + continue; + //printf( "%s", pStart + 4 ); + Total += -atof( pStart + 4 ); + } + printf( "Total = %.2f\n", Total ); + fclose( pFile ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 13f8caea..7aef638d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36669,6 +36669,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Gia_Man_t * Gia_ManCombSpecReduce( Gia_Man_t * p ); pTemp = Gia_ManCombSpecReduce( pAbc->pGia ); Abc_FrameUpdateGia( pAbc, pTemp ); + Result = 0; return 0; } sprintf(pFileName, "gsrm%s.aig", fSpeculate? "" : "s" ); diff --git a/src/misc/extra/extraUtilPrime.c b/src/misc/extra/extraUtilPrime.c index 215de367..13558092 100644 --- a/src/misc/extra/extraUtilPrime.c +++ b/src/misc/extra/extraUtilPrime.c @@ -583,7 +583,7 @@ void Tab_DecomposeTest() Vec_Int_t * vPrimes = Abc_GenPrimes( nVars ); Tab_Man_t * p = Tab_ManAlloc( nVars, Vec_IntSize(vPrimes) ); Tab_ManStart( p, vPrimes ); - printf( "Created %d cubes dependent on %d variables with %d literals.\n", p->nCubes, p->nVars ); + printf( "Created %d cubes dependent on %d variables.\n", p->nCubes, p->nVars ); vPairs = Tab_ManCollectDist1( p, 0 ); printf( "Collected %d pairs.\n", Vec_IntSize(vPairs)/2 ); Vec_IntFree( vPairs ); diff --git a/src/sat/satoko/utils/sdbl.h b/src/sat/satoko/utils/sdbl.h index 9f90ba02..a26794c7 100644 --- a/src/sat/satoko/utils/sdbl.h +++ b/src/sat/satoko/utils/sdbl.h @@ -121,8 +121,8 @@ static inline void sdbl_test() { sdbl_t ten100_ = ABC_CONST(0x014c924d692ca61b); printf("%f\n", sdbl2double(ten100_)); - printf("%016lX\n", double2sdbl(1 /0.95)); - printf("%016lX\n", SDBL_CONST1); + //printf("%016lX\n", double2sdbl(1 /0.95)); + //printf("%016lX\n", SDBL_CONST1); printf("%f\n", sdbl2double(SDBL_CONST1)); printf("%f\n", sdbl2double(ABC_CONST(0x000086BCA1AF286B))); |