From adce11979f0c6df2c67fdf71b946f9bbb91cd6dc Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Fri, 15 Sep 2017 23:28:57 -0700 Subject: bridge relates: (1) fix netlist reader to read the latest version written by ZZ, (2) replace printf() with Abc_Print() in pdr so that it will not interfer with bridge messages --- src/misc/util/utilBridge.c | 11 +++++++++++ src/proof/pdr/pdrInv.c | 48 +++++++++++++++++++++++----------------------- 2 files changed, 35 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c index 885e6ccc..70ea8ec7 100644 --- a/src/misc/util/utilBridge.c +++ b/src/misc/util/utilBridge.c @@ -312,6 +312,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I Gia_Man_t * p = NULL; unsigned char * pBufferPivot, * pBufferEnd = pBuffer + Size; int i, nInputs, nFlops, nGates, nProps; + int verFairness, nFairness, nConstraints; unsigned iFan0, iFan1; nInputs = Gia_AigerReadUnsigned( &pBuffer ); @@ -370,6 +371,16 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I // complement property output!!! Gia_ManAppendCo( p, Abc_LitNot(iFan0) ); } + + verFairness = Gia_AigerReadUnsigned( &pBuffer ); + assert( verFairness == 1 ); + + nFairness = Gia_AigerReadUnsigned( &pBuffer ); + assert( nFairness == 0 ); + + nConstraints = Gia_AigerReadUnsigned( &pBuffer ); + assert( nConstraints == 0); + // make sure the end of buffer is reached assert( pBufferEnd == pBuffer ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index baade033..bc4e3ffc 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -51,13 +51,13 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) int i, ThisSize, Length, LengthStart; if ( Vec_PtrSize(p->vSolvers) < 2 ) { - printf( "Frame " ); - printf( "Clauses " ); - printf( "Max Queue " ); - printf( "Flops " ); - printf( "Cex " ); - printf( "Time" ); - printf( "\n" ); + Abc_Print(1, "Frame " ); + Abc_Print(1, "Clauses " ); + Abc_Print(1, "Max Queue " ); + Abc_Print(1, "Flops " ); + Abc_Print(1, "Cex " ); + Abc_Print(1, "Time" ); + Abc_Print(1, "\n" ); return; } if ( Abc_FrameIsBatchMode() && !fClose ) @@ -272,10 +272,10 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ) void Pdr_SetPrintOne( Pdr_Set_t * p ) { int i; - printf( "Clause: {" ); + Abc_Print(1, "Clause: {" ); for ( i = 0; i < p->nLits; i++ ) - printf( " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) ); - printf( " }\n" ); + Abc_Print(1, " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) ); + Abc_Print(1, " }\n" ); } /**Function************************************************************* @@ -327,7 +327,7 @@ Aig_Man_t * Pdr_ManDupAigWithClauses( Aig_Man_t * p, Vec_Ptr_t * vCubes ) Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); // check the resulting network if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDupSimple(): The check has failed.\n" ); + Abc_Print(1, "Aig_ManDupSimple(): The check has failed.\n" ); return pNew; } void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes ) @@ -335,7 +335,7 @@ void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes ) Aig_Man_t * pNew = Pdr_ManDupAigWithClauses( p, vCubes ); Ioa_WriteAiger( pNew, "aig_with_clauses.aig", 0, 0 ); Aig_ManStop( pNew ); - printf( "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" ); + Abc_Print(1, "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" ); } /**Function************************************************************* @@ -588,7 +588,7 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) else Counter++; } - //printf( "Clauses = %d.\n", Counter ); + //Abc_Print(1, "Clauses = %d.\n", Counter ); //sat_solver_delete( pSat ); return fChanges; } @@ -692,12 +692,12 @@ Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ) } void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ) { - printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) ); + Abc_Print(1, "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) ); if ( fVerbose ) { Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts ); - printf( "%s", Vec_StrArray( vStr ) ); + Abc_Print(1, "%s", Vec_StrArray( vStr ) ); Vec_IntFree( vCounts ); Vec_StrFree( vStr ); } @@ -743,7 +743,7 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver if ( status == l_True ) // sat - property fails { if ( fVerbose ) - printf( "Coverage check failed for output %d.\n", i ); + Abc_Print(1, "Coverage check failed for output %d.\n", i ); nFailedOuts++; if ( fSkip ) { @@ -767,14 +767,14 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver // if it does not intersect, then it is redundant and can be skipped status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); if ( status != l_True && fVerbose ) - printf( "Finished checking clause %d (out of %d)...\r", i, pList[0] ); + Abc_Print(1, "Finished checking clause %d (out of %d)...\r", i, pList[0] ); if ( status == l_Undef ) // timeout break; if ( status == l_False ) // unsat -- correct continue; assert( status == l_True ); if ( fVerbose ) - printf( "Inductiveness check failed for clause %d.\n", i ); + Abc_Print(1, "Inductiveness check failed for clause %d.\n", i ); nFailed++; if ( fSkip ) { @@ -892,14 +892,14 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) if ( fCannot ) continue; if ( fVerbose ) - printf( "Removing clause %d.\n", i ); + Abc_Print(1, "Removing clause %d.\n", i ); Vec_BitWriteEntry( vRemoved, i, 1 ); nRemoved++; } if ( nRemoved ) - printf( "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes ); + Abc_Print(1, "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes ); else - printf( "Invariant minimization did not change the invariant. " ); + Abc_Print(1, "Invariant minimization did not change the invariant. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // cleanup cover if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes @@ -941,7 +941,7 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) else { if ( fVerbose ) - printf( "Removing lit %d from clause %d.\n", k, i ); + Abc_Print(1, "Removing lit %d from clause %d.\n", k, i ); nRemoved++; } sat_solver_delete( pSat ); @@ -952,9 +952,9 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) Cnf_DataFree( pCnf ); //sat_solver_delete( pSat ); if ( nRemoved ) - printf( "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits ); + Abc_Print(1, "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits ); else - printf( "Invariant minimization did not change the invariant. " ); + Abc_Print(1, "Invariant minimization did not change the invariant. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( nRemoved > 0 ) // finished without timeout and removed some lits { -- cgit v1.2.3