From 6d52a1e44999ac19d53d9a8204cc5276db9cdc81 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Jun 2023 13:58:51 +0200 Subject: [PATCH 1/9] fold: Option (-s) to make sequential cleanup optional (cherry picked from commit 1bd088d027262bc66c6ec2f1ca65c338c71dd168) --- src/aig/saig/saig.h | 2 +- src/aig/saig/saigConstr2.c | 5 +++-- src/base/abci/abc.c | 12 +++++++++--- src/base/abci/abcDar.c | 4 ++-- src/base/wlc/wlcMem.c | 2 +- 5 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 16e7fb442..4744b8f86 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -114,7 +114,7 @@ extern Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * v extern int Saig_ManDetectConstrTest( Aig_Man_t * p ); extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); /*=== saigConstr2.c ==========================================================*/ -extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ); +extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup ); extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); // -- jlong -- begin extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt ); diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 6e560b59e..79f557616 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -939,7 +939,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nCo SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ) +Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup ) { Aig_Man_t * pAigNew; Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj; @@ -1000,7 +1000,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo // perform cleanup Aig_ManCleanup( pAigNew ); - Aig_ManSeqCleanup( pAigNew ); + if ( fSeqCleanup ) + Aig_ManSeqCleanup( pAigNew ); return pAigNew; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a78706032..17e5b2905 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29681,14 +29681,16 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int fCompl; int fVerbose; + int fSeqCleanup; int c; - extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup ); pNtk = Abc_FrameReadNtk(pAbc); // set defaults fCompl = 0; fVerbose = 0; + fSeqCleanup = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cvsh" ) ) != EOF ) { switch ( c ) { @@ -29698,6 +29700,9 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 's': + fSeqCleanup ^= 1; + break; case 'h': goto usage; default: @@ -29727,7 +29732,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Abc_NtkIsComb(pNtk) ) Abc_Print( 0, "The network is combinational.\n" ); // modify the current network - pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose ); + pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose, fSeqCleanup ); if ( pNtkRes == NULL ) { Abc_Print( 1,"Transformation has failed.\n" ); @@ -29742,6 +29747,7 @@ usage: Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" ); Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle performing sequential cleanup [default = %s]\n", fSeqCleanup? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 76c7cf547..a209143f3 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -4682,7 +4682,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nPr SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; @@ -4690,7 +4690,7 @@ Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose ) pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return NULL; - pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose ); + pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose, fSeqCleanup ); Aig_ManStop( pTemp ); pNtkAig = Abc_NtkFromAigPhase( pMan ); pNtkAig->pName = Extra_UtilStrsav(pMan->pName); diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c index b2d5c5ee0..1f35f324e 100644 --- a/src/base/wlc/wlcMem.c +++ b/src/base/wlc/wlcMem.c @@ -1024,7 +1024,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); pAig->nConstrs = 1; - pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 ); + pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0, 1 ); Aig_ManStop( pTempAig ); pAbs = Gia_ManFromAigSimple( pAig ); Aig_ManStop( pAig ); From adbcb914b293064d0823b151d9ba6ffa7e21ed78 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 13:21:59 +0200 Subject: [PATCH 2/9] Add '-p' option to 'constr' to allow fully removing constraints Invoking 'constr -r' converts constraints into POs but does not fully remove them. Now 'constr -pr' can be used to completely remove them, leaving the set of non-constraint POs unchanged. (cherry picked from commit 8c923ad4929870d4e819b84f62c7f9177b0d0d17) --- src/base/abci/abc.c | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 17e5b2905..3b01b4614 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29337,17 +29337,20 @@ usage: int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtkRes; int c; int nFrames; int nConfs; int nProps; int fRemove; + int fPurge; int fStruct; int fInvert; int fOldAlgo; int fVerbose; int nConstrs; extern void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange ); pNtk = Abc_FrameReadNtk(pAbc); // set defaults @@ -29355,13 +29358,14 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) nConfs = 1000; nProps = 1000; fRemove = 0; + fPurge = 0; fStruct = 0; fInvert = 0; fOldAlgo = 0; fVerbose = 0; nConstrs = -1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrpsiavh" ) ) != EOF ) { switch ( c ) { @@ -29412,6 +29416,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRemove ^= 1; break; + case 'p': + fPurge ^= 1; + break; case 's': fStruct ^= 1; break; @@ -29447,7 +29454,22 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Constraints are not defined.\n" ); return 0; } - Abc_Print( 1, "Constraints are converted to be primary outputs.\n" ); + + if ( fPurge ) + { + Abc_Print( 1, "Constraints are removed.\n" ); + pNtkRes = Abc_NtkMakeOnePo( pNtk, 0, Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) ); + if ( pNtkRes == NULL ) + { + Abc_Print( 1,"Transformation has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + pNtk = Abc_FrameReadNtk(pAbc); + } + else + Abc_Print( 1, "Constraints are converted to be primary outputs.\n" ); pNtk->nConstrs = 0; return 0; } @@ -29492,7 +29514,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" ); + Abc_Print( -2, "usage: constr [-FCPN num] [-rpisavh]\n" ); Abc_Print( -2, "\t a toolkit for constraint manipulation\n" ); Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" ); Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" ); @@ -29501,7 +29523,8 @@ usage: Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs ); Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps ); Abc_Print( -2, "\t-N num : manually set the last POs to be constraints [default = %d]\n", nConstrs ); - Abc_Print( -2, "\t-r : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" ); + Abc_Print( -2, "\t-r : manually remove the constraints, converting them to POs [default = %s]\n", fRemove? "yes": "no" ); + Abc_Print( -2, "\t-p : remove constraints instead of converting them to POs [default = %s]\n", fPurge? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" ); Abc_Print( -2, "\t-a : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" ); From 1383c7646421461d242857b048e73fd115a3ec85 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 7 Aug 2024 15:13:26 +0200 Subject: [PATCH 3/9] Pull YosysHQ read_cex/write_cex changes See - YosysHQ/abc#19 - YosysHQ/abc#16 - commit 6234e18d - YosysHQ/abc#14 - YosysHQ/abc#12 - YosysHQ/abc#11 Co-authored-by: Jannis Harder Co-authored-by: Claire Xenia Wolf Co-authored-by: Miodrag Milanovic --- src/base/io/io.c | 447 +++++++++++++++++++++++++++++++++++--- src/sat/bmc/bmc.h | 4 +- src/sat/bmc/bmcCexCare.c | 38 +++- src/sat/bmc/bmcCexTools.c | 47 ++++ 4 files changed, 498 insertions(+), 38 deletions(-) diff --git a/src/base/io/io.c b/src/base/io/io.c index fa7a961a5..8f805d639 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -116,6 +117,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); @@ -686,6 +688,331 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode ) +{ + FILE * pFile; + Abc_Cex_t * pCex; + Abc_Cex_t * pCexCare; + Vec_Int_t * vNums; + int c, nRegs = -1, nFrames = -1; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open log file for reading \"%s\".\n" , pFileName ); + return -1; + } + + vNums = Vec_IntAlloc( 100 ); + int usedX = 0; + *fOldFormat = 0; + + int MaxLine = 1000000; + char *Buffer; + int BufferLen = 0; + int state = 0; + int iPo = 0; + nFrames = -1; + int status = 0; + int i; + int nRegsNtk = 0; + Abc_Obj_t * pObj; + Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++; + + Buffer = ABC_ALLOC( char, MaxLine ); + while ( fgets( Buffer, MaxLine, pFile ) != NULL ) + { + if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' ) + continue; + BufferLen = strlen(Buffer) - 1; + Buffer[BufferLen] = '\0'; + if (state==0 && BufferLen>1) { + // old format detected + *fOldFormat = 1; + state = 2; + iPo = 0; + status = 1; + } + if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') { + // old format detected, first line was actually register + *fOldFormat = 1; + state = 3; + Vec_IntPush( vNums, status ); + status = 1; + } + if (Buffer[0] == '.' ) + break; + switch(state) { + case 0 : + { + char c = Buffer[0]; + if ( c == '0' || c == '1' || c == '2' ) { + status = c - '0' ; + state = 1; + } else if ( c == 'x' ) { + // old format with one x state latch + usedX = 1; + // set to 2 so we can Abc_LatchSetInitNone + // acts like 0 when setting bits + Vec_IntPush( vNums, 2 ); + nRegs = Vec_IntSize(vNums); + state = 3; + } else { + printf( "ERROR: Bad aiger status line.\n" ); + return -1; + } + } + break; + case 1 : + iPo = atoi(Buffer+1); + state = 2; + break; + case 2 : + for (i=0; i nRegsNtk ) + { + printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" ); + Vec_IntShrink( vNums, nRegsNtk ); + nRegs = nRegsNtk; + } + state = 3; + break; + default: + for (i=0; i= Abc_NtkPoNum(pNtk) ) + { + printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" ); + iPo = 0; + } + Abc_NtkForEachLatch( pNtk, pObj, i ) { + if ( Vec_IntEntry(vNums, i) == 1 ) + Abc_LatchSetInit1(pObj); + else if ( Vec_IntEntry(vNums, i) == 2 && xMode ) + Abc_LatchSetInitNone(pObj); + else + Abc_LatchSetInit0(pObj); + } + + pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 ); + pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1); + // the zero-based number of PO, for which verification failed + // fails in Bmc_CexVerify if not less than actual number of PO + pCex->iPo = iPo; + pCexCare->iPo = iPo; + // the zero-based number of the time-frame, for which verificaiton failed + pCex->iFrame = iFrameCex; + pCexCare->iFrame = iFrameCex; + assert( Vec_IntSize(vNums) == pCex->nBits ); + for ( c = 0; c < pCex->nBits; c++ ) { + if ( Vec_IntEntry(vNums, c) == 1) + { + Abc_InfoSetBit( pCex->pData, c ); + Abc_InfoSetBit( pCexCare->pData, c ); + } + else if ( Vec_IntEntry(vNums, c) == 2 && xMode ) + { + // nothing to set + } + else + Abc_InfoSetBit( pCexCare->pData, c ); + } + + Vec_IntFree( vNums ); + Abc_CexFreeP( ppCex ); + if ( ppCex ) + *ppCex = pCex; + else + Abc_CexFree( pCex ); + Abc_CexFreeP( ppCexCare ); + if ( ppCexCare ) + *ppCexCare = pCexCare; + else + Abc_CexFree( pCexCare ); + + if ( pnFrames ) + *pnFrames = nFrames; + return status; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk; + Abc_Cex_t * pCex = NULL; + Abc_Cex_t * pCexCare = NULL; + char * pFileName; + FILE * pFile; + int fCheck = 1; + int fXMode = 0; + int c; + int fOldFormat = 0; + int verified; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fCheck ^= 1; + break; + case 'x': + fXMode ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + + // get the input file name + pFileName = argv[globalUtilOptind]; + if ( (pFile = fopen( pFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + return 1; + } + fclose( pFile ); + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + Abc_FrameClearVerifStatus( pAbc ); + pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode); + if ( fOldFormat && !fCheck ) + printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" ); + + if ( fCheck && pAbc->Status==1) { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); + + verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false ); + if (!verified) + { + printf( "Checking CEX for any PO.\n" ); + int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false ); + Aig_ManStop( pAig ); + if (verified < 0) + { + Abc_CexFreeP(&pCex); + Abc_CexFreeP(&pCexCare); + return 1; + } + pAbc->pCex->iPo = verified; + } + + Abc_CexFreeP(&pCexCare); + Abc_FrameReplaceCex( pAbc, &pCex ); + } + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_cex [-ch] \n" ); + fprintf( pAbc->Err, "\t reads the witness cex\n" ); + fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" ); + fprintf( pAbc->Err, "\t-x : read x bits for verification [default = %s]\n", fXMode? "yes":"no" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} /**Function************************************************************* Synopsis [] @@ -2549,10 +2876,15 @@ void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex } +extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose ); +extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose ); + void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, - int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, - int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) + int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, + int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended ) { + Abc_Cex_t * pCare = NULL; Abc_Obj_t * pObj; int i, f; if ( fPrintFull ) @@ -2568,15 +2900,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) ); Abc_CexFreeP( &pCexFull ); } - else if ( fNames ) + else { - Abc_Cex_t * pCare = NULL; + if ( fNames ) + { + fprintf( pFile, "# FALSIFYING OUTPUTS:"); + fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + } if ( fMinimize ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); if ( fUseOldMin ) { pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); @@ -2584,21 +2918,47 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose ); } else if ( fUseSatBased ) - pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); + { + if ( Abc_NtkPoNum( pNtk ) == 1 ) + pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); + else + printf( "SAT-based CEX minimization requires having a single PO.\n" ); + } + else if ( fCexInfo ) + { + Gia_Man_t * p = Gia_ManFromAigSimple( pAig ); + Abc_Cex_t * pCexImpl = NULL; + Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose ); + Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose ); + Abc_Cex_t * pCexEss; + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) ) + printf( "Counter-example care-set verification has failed.\n" ); + + pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose ); + + // pCare is pCexMin from Bmc_CexTest + pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose ); + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) ) + printf( "Counter-example min-set verification has failed.\n" ); + Abc_CexFreeP( &pCexStates ); + Abc_CexFreeP( &pCexImpl ); + Abc_CexFreeP( &pCexCare ); + Abc_CexFreeP( &pCexEss ); + } else pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose ); Aig_ManStop( pAig ); - if(pCare == NULL) + if(pCare == NULL) printf( "Counter-example minimization has failed.\n" ); } - else + if (fNames) { - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + fprintf( pFile, "\n"); + fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); } - fprintf( pFile, "\n"); - fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); - if ( fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) + if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) { int * pValues; int nXValues = 0, iFlop = 0, iPivotPi = -1; @@ -2638,29 +2998,36 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, } else { + if (fExtended && fAiger && !fNames) { + fprintf( pFile, "1\n"); + fprintf( pFile, "b%d\n", pCex->iPo); + } // output flop values (unaffected by the minimization) Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + if ( fNames ) + fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + else + fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); // output PI values (while skipping the minimized ones) - for ( f = 0; f <= pCex->iFrame; f++ ) + for ( f = 0; f <= pCex->iFrame; f++ ) { Abc_NtkForEachPi( pNtk, pObj, i ) if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) - fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + if ( fNames ) + fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else + fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else if ( !fNames ) + fprintf( pFile, "x"); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); + } + if (fExtended && fAiger && !fNames) + fprintf( pFile, ".\n"); } Abc_CexFreeP( &pCare ); } - else - { - Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); - - for ( i = pCex->nRegs; i < pCex->nBits; i++ ) - { - if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0) - fprintf( pFile, "\n"); - fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) ); - } - } } /**Function************************************************************* @@ -2689,9 +3056,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) int fPrintFull = 0; int fUseFfNames = 0; int fVerbose = 0; + int fCexInfo = 0; + int fExtended = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF ) { switch ( c ) { @@ -2728,6 +3097,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) case 'v': fVerbose ^= 1; break; + case 'x': + fCexInfo ^= 1; + break; + case 't': + fExtended ^= 1; + break; case 'h': goto usage; default: @@ -2776,8 +3151,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pAbc->pCex ) { Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } else if ( pAbc->vCexVec ) { @@ -2785,10 +3160,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) { if ( pCex == NULL ) continue; - fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); + fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } } fprintf( pFile, "# DONE\n" ); @@ -2832,8 +3207,10 @@ usage: fprintf( pAbc->Err, "\t-u : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" ); fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" ); fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" ); + fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" ); fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" ); + fprintf( pAbc->Err, "\t-t : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" ); fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" ); fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" ); fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 844497ad0..343563598 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -227,7 +227,8 @@ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); -extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ @@ -238,6 +239,7 @@ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC /*=== bmcCexTool.c ==========================================================*/ extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose ); extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); +extern int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); /*=== bmcICheck.c ==========================================================*/ extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ); extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index c274b04cb..d9a677c35 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t SeeAlso [] ***********************************************************************/ -void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) { + int result; Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); if ( fVerbose ) { @@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in printf( "Minimized: " ); Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); } - if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) ) + result = Bmc_CexVerify( pGia, pCex, pCexMin ); + if ( !result ) printf( "Counter-example verification has failed.\n" ); else printf( "Counter-example verification succeeded.\n" ); Gia_ManStop( pGia ); + return result; } /* { @@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in } */ +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +{ + int iPo; + Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); + if ( fVerbose ) + { + printf( "Original : " ); + Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 ); + printf( "Minimized: " ); + Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); + } + iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin ); + if ( iPo < 0 ) + printf( "Counter-example verification has failed.\n" ); + else + printf( "Counter-example verification succeeded.\n" ); + Gia_ManStop( pGia ); + return iPo; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 6cc298577..6bea6fc5f 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -374,6 +374,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) return Gia_ObjTerSimGet1(pObj); } +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example for an arbitrary PO.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) +{ + Gia_Obj_t * pObj; + int i, k; +// assert( pCex->nRegs > 0 ); +// assert( pCexCare->nRegs == 0 ); + Gia_ObjTerSimSet0( Gia_ManConst0(p) ); + Gia_ManForEachRi( p, pObj, k ) + Gia_ObjTerSimSet0( pObj ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + { + if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) ) + Gia_ObjTerSimSetX( pObj ); + else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachRo( p, pObj, k ) + Gia_ObjTerSimRo( p, pObj ); + Gia_ManForEachAnd( p, pObj, k ) + Gia_ObjTerSimAnd( pObj ); + Gia_ManForEachCo( p, pObj, k ) + Gia_ObjTerSimCo( pObj ); + } + for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++) + { + pObj = Gia_ManPo( p, i ); + if (Gia_ObjTerSimGet1(pObj)) + return i; + } + return -1; +} + /**Function************************************************************* Synopsis [Computes internal states of the CEX.] From eef8c01340842079a64cd7064cd9b131839ec6e4 Mon Sep 17 00:00:00 2001 From: David A Roberts Date: Mon, 1 Apr 2024 09:40:41 +1000 Subject: [PATCH 4/9] Fix Assertion using &if: `pCutSet->nCuts > 0' (cherry picked from commit 316eec6d3f7addf81424bd51f846731f3b8696d7) --- src/map/if/ifMap.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 0ad63f050..07e6cac82 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -460,7 +460,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->Delay = If_CutDelay( p, pObj, pCut ); if ( pCut->Delay == -1 ) continue; - if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon ) + if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon && pCutSet->nCuts > 0 ) continue; // compute area of the cut (this area may depend on the application specific cost) pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut ); From 3e65b259423541f8fa9f91a2f6f17c888d69c8cb Mon Sep 17 00:00:00 2001 From: David A Roberts Date: Mon, 1 Apr 2024 10:03:10 +1000 Subject: [PATCH 5/9] Apply patch to If_ObjPerformMappingChoice too (cherry picked from commit accf50468a0fb88db8de9743b751ab9226e8f343) --- src/map/if/ifMap.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 07e6cac82..d508afd9d 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -558,7 +558,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP continue; // check if the cut satisfies the required times // assert( pCut->Delay == If_CutDelay( p, pTemp, pCut ) ); - if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon ) + if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon && pCutSet->nCuts > 0 ) continue; // set the phase attribute pCut->fCompl = pObj->fPhase ^ pTemp->fPhase; From e334586ae4c60100c01191e790e800fc7b4754b6 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 8 Sep 2022 16:04:24 +0200 Subject: [PATCH 6/9] Additional fix for large liberty files (cherry picked from commit ab5b16ede2ff3a4ab5209df24db2c76700899684) --- src/map/scl/sclLiberty.c | 48 ++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c index e04b95845..707a8c585 100644 --- a/src/map/scl/sclLiberty.c +++ b/src/map/scl/sclLiberty.c @@ -57,12 +57,12 @@ typedef struct Scl_Item_t_ Scl_Item_t; struct Scl_Item_t_ { int Type; // Scl_LibertyType_t - int iLine; // file line where the item's spec begins + long iLine; // file line where the item's spec begins Scl_Pair_t Key; // key part Scl_Pair_t Head; // head part Scl_Pair_t Body; // body part - int Next; // next item in the list - int Child; // first child item + long Next; // next item in the list + long Child; // first child item }; typedef struct Scl_Tree_t_ Scl_Tree_t; @@ -71,9 +71,9 @@ struct Scl_Tree_t_ char * pFileName; // input Liberty file name char * pContents; // file contents long nContents; // file size - int nLines; // line counter - int nItems; // number of items - int nItermAlloc; // number of items allocated + long nLines; // line counter + long nItems; // number of items + long nItermAlloc; // number of items allocated Scl_Item_t * pItems; // the items char * pError; // the error string abctime clkStart; // beginning time @@ -89,11 +89,11 @@ static inline int Scl_LibertyGlobMatch(const char * pattern, const char #endif } static inline Scl_Item_t * Scl_LibertyRoot( Scl_Tree_t * p ) { return p->pItems; } -static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, int v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; } -static inline int Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((int)strlen(pStr) != Pair.End-Pair.Beg); } +static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, long v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; } +static inline long Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((long)strlen(pStr) != Pair.End-Pair.Beg); } static inline void Scl_PrintWord( FILE * pFile, Scl_Tree_t * p, Scl_Pair_t Pair ) { char * pBeg = p->pContents+Pair.Beg, * pEnd = p->pContents+Pair.End; while ( pBeg < pEnd ) fputc( *pBeg++, pFile ); } -static inline void Scl_PrintSpace( FILE * pFile, int nOffset ) { int i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); } -static inline int Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; } +static inline void Scl_PrintSpace( FILE * pFile, long nOffset ) { long i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); } +static inline long Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; } #define Scl_ItemForEachChild( p, pItem, pChild ) \ for ( pChild = Scl_LibertyItem(p, pItem->Child); pChild; pChild = Scl_LibertyItem(p, pChild->Next) ) @@ -181,9 +181,9 @@ int Scl_LibertyParseDump( Scl_Tree_t * p, char * pFileName ) SeeAlso [] ***********************************************************************/ -int Scl_LibertyCountItems( char * pBeg, char * pEnd ) +long Scl_LibertyCountItems( char * pBeg, char * pEnd ) { - int Counter = 0; + long Counter = 0; for ( ; pBeg < pEnd; pBeg++ ) Counter += (*pBeg == '(' || *pBeg == ':'); return Counter; @@ -228,11 +228,11 @@ void Scl_LibertyWipeOutComments( char * pBeg, char * pEnd ) } } } -static inline int Scl_LibertyCharIsSpace( char c ) +static inline long Scl_LibertyCharIsSpace( char c ) { return c == ' ' || c == '\t' || c == '\r' || c == '\n' || c == '\\'; } -static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine ) +static inline long Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine ) { char * pPos = *ppPos; for ( ; pPos < pEnd; pPos++ ) @@ -250,7 +250,7 @@ static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * p return pPos == pEnd; } // skips entry delimited by " :;(){}" and returns 1 if reached the end -static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) +static inline long Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) { char * pPos = *ppPos; if ( *pPos == '\"' ) @@ -277,7 +277,7 @@ static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) // finds the matching closing symbol static inline char * Scl_LibertyFindMatch( char * pPos, char * pEnd ) { - int Counter = 0; + long Counter = 0; assert( *pPos == '(' || *pPos == '{' ); if ( *pPos == '(' ) { @@ -387,10 +387,10 @@ char * Scl_LibertyReadString( Scl_Tree_t * p, Scl_Pair_t Pair ) Buffer[Pair.End-Pair.Beg] = 0; return Buffer; } -int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) +long Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) { Scl_Item_t * pItem; - int Counter = 0; + long Counter = 0; Scl_ItemForEachChildName( p, pRoot, pItem, pName ) Counter++; return Counter; @@ -407,7 +407,7 @@ int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) SeeAlso [] ***********************************************************************/ -int Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd ) +long Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd ) { Scl_Item_t * pItem; Scl_Pair_t Key, Head, Body; @@ -513,7 +513,7 @@ exit: if ( p->pError == NULL ) { p->pError = ABC_ALLOC( char, 1000 ); - sprintf( p->pError, "File \"%s\". Line %6d. Failed to parse entry \"%s\".\n", + sprintf( p->pError, "File \"%s\". Line %6ld. Failed to parse entry \"%s\".\n", p->pFileName, p->nLines, Scl_LibertyReadString(p, Key) ); } return -1; @@ -556,7 +556,7 @@ char * Scl_LibertyFileContents( char * pFileName, long nContents ) { FILE * pFile = fopen( pFileName, "rb" ); char * pContents = ABC_ALLOC( char, nContents+1 ); - int RetValue = 0; + long RetValue = 0; RetValue = fread( pContents, nContents, 1, pFile ); fclose( pFile ); pContents[nContents] = 0; @@ -565,7 +565,7 @@ char * Scl_LibertyFileContents( char * pFileName, long nContents ) void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr ) { FILE * pFile = fopen( pFileName, "wb" ); - int RetValue = 0; + long RetValue = 0; if ( pFile == NULL ) { printf( "Scl_LibertyStringDump(): The output file is unavailable.\n" ); @@ -721,10 +721,10 @@ int Scl_LibertyReadCellIsThreeState( Scl_Tree_t * p, Scl_Item_t * pCell ) return 1; return 0; } -int Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell ) +long Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell ) { Scl_Item_t * pPin; - int Counter = 0; + long Counter = 0; Scl_ItemForEachChildName( p, pCell, pPin, "pin" ) if ( Scl_LibertyReadPinFormula(p, pPin) ) Counter++; From e62e8ac52850e1916e8b9a586fbba306179390df Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 2 Feb 2024 16:47:38 +0100 Subject: [PATCH 7/9] pdr -X to write CEXes immediately (cherry picked from commit f63471bdf5d64c44e0b107fbe9e2629f969030b6) --- src/base/abci/abc.c | 14 ++++++++++++-- src/proof/pdr/pdr.h | 2 ++ src/proof/pdr/pdrCore.c | 41 +++++++++++++++++++++++++++++++++++++++-- src/proof/pdr/pdrIncr.c | 4 +++- 4 files changed, 56 insertions(+), 5 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3b01b4614..7841f0df9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30241,7 +30241,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -30362,6 +30362,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pInvFileName = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" ); + goto usage; + } + pPars->pCexFilePrefix = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fSolveAll ^= 1; break; @@ -30469,7 +30478,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDQTHGS ] [-LI ] [-axrmuyfqipdegjonctkvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDQTHGS ] [-LI ] [-X ] [-axrmuyfqipdegjonctkvwzh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); @@ -30484,6 +30493,7 @@ usage: Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" ); + Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as *.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled"); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index d8a548d5c..00d15a8bc 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -84,6 +84,7 @@ struct Pdr_Par_t_ abctime timeLastSolved; // the time when the last output was solved Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) char * pInvFileName; // invariable file name + char * pCexFilePrefix; // CEX output prefix }; //////////////////////////////////////////////////////////////////////// @@ -95,6 +96,7 @@ struct Pdr_Par_t_ //////////////////////////////////////////////////////////////////////// /*=== pdrCore.c ==========================================================*/ +extern void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ); extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars ); diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 34a327034..371dda168 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -80,6 +80,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->nDropOuts = 0; // the number of timed out outputs pPars->timeLastSolved = 0; // last one solved pPars->pInvFileName = NULL; // invariant file name + pPars->pCexFilePrefix = NULL; // CEX output prefix } /**Function************************************************************* @@ -1026,6 +1027,38 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) return 1; } +void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ) +{ + int i, f, iBit; + size_t iCexPathSize; + char * pCexPath; + FILE * pCexFile; + + iCexPathSize = snprintf( NULL, 0, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ) + 1; + pCexPath = malloc( iCexPathSize ); + snprintf( pCexPath, iCexPathSize, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ); + Abc_Print( 1, "Writing CEX for output %d to %s\n", pCex->iPo, pCexPath ); + pCexFile = fopen( pCexPath, "w" ); + free( pCexPath ); + + fprintf( pCexFile, "1\n"); + fprintf( pCexFile, "b%d\n", pCex->iPo); + + iBit = 0; + for ( i = 0; i < pCex->nRegs; i++, iBit++ ) + putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile ); + putc( '\n', pCexFile ); + + for ( f = 0; f <= pCex->iFrame; f++ ) + { + for ( i = 0; i < pCex->nPis; i++, iBit++ ) + putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile ); + putc( '\n', pCexFile ); + } + fprintf( pCexFile, ".\n"); + fclose( pCexFile ); +} + /**Function************************************************************* Synopsis [] @@ -1100,7 +1133,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pAig->pSeqModel = pCexNew; return 0; // SAT } - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( !p->pPars->fNotVerbose ) @@ -1109,6 +1142,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); + if ( p->pPars->pCexFilePrefix ) + Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { @@ -1217,11 +1252,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); + if ( p->pPars->pCexFilePrefix ) + Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 9ca72ba69..6ba68db99 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -484,7 +484,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) p->pAig->pSeqModel = pCexNew; return 0; // SAT } - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( !p->pPars->fNotVerbose ) @@ -493,6 +493,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); + if ( p->pPars->pCexFilePrefix ) + Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { From c8d64b8682473be6f82b3b8c85a89687b08f398a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Feb 2024 18:37:53 +0100 Subject: [PATCH 8/9] Fix pdr timing output (cherry picked from commit acbe1b1f03c4df825698c6843d1f69f0f1316379) --- src/proof/pdr/pdrCore.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 371dda168..842324c90 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -1035,7 +1035,7 @@ void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ) FILE * pCexFile; iCexPathSize = snprintf( NULL, 0, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ) + 1; - pCexPath = malloc( iCexPathSize ); + pCexPath = (char *)malloc( iCexPathSize ); snprintf( pCexPath, iCexPathSize, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ); Abc_Print( 1, "Writing CEX for output %d to %s\n", pCex->iPo, pCexPath ); pCexFile = fopen( pCexPath, "w" ); From 5444cf281c0cff7d583444bf0dbdffa36aec1ca9 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 27 Feb 2024 10:35:32 +0100 Subject: [PATCH 9/9] Improved anytime pdr (cherry picked from commit c832967200f1b5578cf4a057cb9b5b5acf816844) --- src/base/abci/abc.c | 6 +- src/proof/pdr/pdr.h | 1 + src/proof/pdr/pdrCore.c | 333 ++++++++++++++++++++++++++++++++++++---- src/proof/pdr/pdrIncr.c | 4 +- src/proof/pdr/pdrInt.h | 8 + src/proof/pdr/pdrInv.c | 77 +++++++--- src/proof/pdr/pdrMan.c | 3 +- src/proof/pdr/pdrSat.c | 3 +- src/proof/pdr/pdrUtil.c | 39 +++++ 9 files changed, 423 insertions(+), 51 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7841f0df9..516c78419 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30241,7 +30241,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -30374,6 +30374,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fSolveAll ^= 1; break; + case 'l': + pPars->fAnytime ^= 1; + break; case 'x': pPars->fStoreCex ^= 1; break; @@ -30495,6 +30498,7 @@ usage: Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" ); Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as *.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled"); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); + Abc_Print( -2, "\t-l : toggle anytime schedule when solving all outputs [default = %s]\n", pPars->fAnytime? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 00d15a8bc..8f62e9b69 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -72,6 +72,7 @@ struct Pdr_Par_t_ int fSilent; // totally silent execution int fSolveAll; // do not stop when found a SAT output int fStoreCex; // enable storing counter-examples in MO mode + int fAnytime; // enable anytime scheduling int fUseBridge; // use bridge interface int fUsePropOut; // use property output int nFailOuts; // the number of failed outputs diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 842324c90..225b6b34a 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -136,6 +136,150 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) return pCubeMin; } +void Pdr_ManCompactNullClauses( Pdr_Man_t * p, int k ) +{ + Pdr_Set_t * pCubeK; + Vec_Ptr_t * vArrayK; + int j; + vArrayK = Vec_VecEntry( p->vClauses, k ); + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + if ( pCubeK != NULL ) + continue; + Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); + Vec_PtrPop(vArrayK); + j--; + } +} + +int Pdr_ManPushInfAndRecycledClauses( Pdr_Man_t * p ) +{ + Pdr_Set_t * pTemp, * pCubeK; + Vec_Ptr_t * vArrayK, * vArrayK1; + Aig_Obj_t * pObj; + int j, k, m, RetValue2, fReduce = p->fNewInfClauses; + + p->fNewInfClauses = 0; + + k = Vec_PtrSize(p->vSolvers) - 2; + assert (k >= 0); + + if ( fReduce && p->pPars->fVeryVerbose ) + Abc_Print( 1, "Reducing inf and recycled clauses for frame %d.\n", k ); + + vArrayK = Vec_VecEntry( p->vClauses, k ); + vArrayK1 = Vec_VecEntry( p->vClauses, k + 1 ); + + Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetBoundSizeLextCompare ); + + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + if ( pCubeK == NULL || pCubeK->iBound != PDR_INF_BOUND ) + continue; + + if (fReduce) + { + // remove cubes in the same frame that are contained by pCubeK + Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) + { + if ( pTemp == NULL ) + continue; + // This is not needed here due to the sort order we're using + // if ( pTemp->iBound > pCubeK->iBound ) + // continue; + if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp + continue; + pTemp->iBound = 0; + Pdr_SetDeref( pTemp ); + Vec_PtrWriteEntry( vArrayK, m, NULL ); + } + } + + // Is it already implied by other clauses? + RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0; + if ( RetValue2 == -1 ) + { + Pdr_ManCompactNullClauses( p, k ); + return -1; + } + if ( RetValue2 == 1 ) + { + pCubeK->iBound = 0; + p->nInfClauses--; + Pdr_SetDeref( pCubeK ); + Vec_PtrWriteEntry( vArrayK, j, NULL ); + continue; + } + + Pdr_ManSolverAddClause( p, k+1, pCubeK ); + Vec_PtrWriteEntry( vArrayK, j, NULL ); + Vec_PtrPush( vArrayK1, pCubeK ); + } + + if ( (p->pPars->fAnytime || p->pPars->fSolveAll) && fReduce ) + { + Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) + { + if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) >= 0 ) + continue; + RetValue2 = Pdr_ManCheckCube( p, k+1, NULL, NULL, p->pPars->nConfLimit, 0, 1 ); + if ( RetValue2 == -1 ) + { + Pdr_ManCompactNullClauses( p, k ); + return -1; + } + if ( RetValue2 == 1 ) + { + // if the output is already in timeout we need to adjust the stats! + if ( Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == -1 ) + p->pPars->nDropOuts--; + Abc_Print( 1, "Proved output %d in frame %d.\n", p->iOutCur, k ); + p->pPars->nProveOuts++; + Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 1 ); + } + } + } + + // Extra debug checks + + // Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, j ) + // { + // assert( pCubeK1->iBound == PDR_INF_BOUND ); + // assert( Pdr_ManCheckCubeCs( p, k+1, pCubeK1 ) != 0 ); + // assert( Pdr_ManCheckCube( p, k, pCubeK1, NULL, 0, 0, 1 ) != 0 ); + // } + + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + if ( pCubeK == NULL || pCubeK->iBound <= k ) + continue; + + // Is it already implied by other clauses? + RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0; + if ( RetValue2 == -1 ) + { + Pdr_ManCompactNullClauses( p, k ); + return -1; + } + if ( RetValue2 == 1 ) + { + Pdr_SetDeref( pCubeK ); + Vec_PtrWriteEntry( vArrayK, j, NULL ); + continue; + } + + Pdr_ManSolverAddClause( p, k+1, pCubeK ); + Vec_PtrWriteEntry( vArrayK, j, NULL ); + Vec_PtrPush( vArrayK1, pCubeK ); + } + + // Compact NULL entries + Pdr_ManCompactNullClauses( p, k ); + + return 0; +} + + /**Function************************************************************* Synopsis [Returns 1 if the state could be blocked.] @@ -153,7 +297,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) Vec_Ptr_t * vArrayK, * vArrayK1; int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1; - int Counter = 0; abctime clk = Abc_Clock(); assert( p->iUseFrame > 0 ); Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) @@ -162,11 +305,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) vArrayK1 = Vec_VecEntry( p->vClauses, k+1 ); Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) { - Counter++; - // remove cubes in the same frame that are contained by pCubeK Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) { + if ( pTemp->iBound > pCubeK->iBound ) + continue; if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp continue; Pdr_SetDeref( pTemp ); @@ -198,6 +341,9 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) // check if the clause subsumes others Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i ) { + // Subsuming a clause of the invariant with a non-invariant clause could break the invariant + if ( pCubeK1->iBound > pCubeK->iBound ) + continue; if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1 continue; Pdr_SetDeref( pCubeK1 ); @@ -206,6 +352,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) i--; } // add the last clause + pCubeK->iBound = k+1; Vec_PtrPush( vArrayK1, pCubeK ); Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); Vec_PtrPop(vArrayK); @@ -223,6 +370,8 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) // remove cubes in the same frame that are contained by pCubeK Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) { + if ( pTemp->iBound > pCubeK->iBound ) + continue; if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp continue; /* @@ -908,6 +1057,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) while ( !Pdr_QueueIsEmpty(p) ) { Counter++; + if (Counter % 100 == 0) { + Pdr_ManPrintProgress( p, 1, Abc_Clock() - p->tStart ); + } pThis = Pdr_QueueHead( p ); if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) ) return 0; // SAT @@ -987,6 +1139,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } + pCubeMin->iBound = k; Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref p->nCubes++; // add clause @@ -1076,24 +1229,36 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_Set_t * pCube = NULL; Aig_Obj_t * pObj; Abc_Cex_t * pCexNew; - int iFrame, RetValue = -1; + int iFrame, i, RetValue = -1, SomeActive = 1, ClausesAdded = 1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; + p->tStart = clkStart; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved - if ( p->pPars->fSolveAll ) - Saig_ManForEachPo( p->pAig, pObj, iFrame ) - if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) + if ( p->pPars->fSolveAll || p->pPars->fAnytime ) + Saig_ManForEachPo( p->pAig, pObj, i ) + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) && Vec_IntEntry( p->pPars->vOutMap, i ) == -2) { - Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat + Abc_Print( 1, "Proved output %d in frame 0 (trivial).\n", i ); p->pPars->nProveOuts++; if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); + Gia_ManToBridgeResult( stdout, 1, NULL, i ); } // create the first timeframe p->pPars->timeLastSolved = Abc_Clock(); Pdr_ManCreateSolver( p, (iFrame = 0) ); + if ( p->vInfCubes != NULL ) + { + Vec_PtrForEachEntry( Pdr_Set_t *, p->vInfCubes, pCube, i ) + { + Pdr_ManSolverAddClause( p, 0, pCube ); + Vec_VecPush( p->vClauses, 0, pCube ); + } + pCube = NULL; + } + while ( 1 ) { int fRefined = 0; @@ -1113,11 +1278,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->nFrames = iFrame; assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = Abc_MaxInt(iFrame, 1); + SomeActive = 0; Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) ) continue; + // skip otuput that was already solved + if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == 1 ) + continue; // skip output whose time has run out if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 ) continue; @@ -1159,6 +1328,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->timeLastSolved = Abc_Clock(); continue; } + SomeActive += 1; // try to solve this output if ( p->pTime4Outs ) { @@ -1203,6 +1373,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( RetValue == 0 ) { + ClausesAdded = 1; RetValue = Pdr_ManBlockCube( p, pCube ); if ( RetValue == -1 ) { @@ -1276,6 +1447,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // all SAT Pdr_QueueClean( p ); pCube = NULL; + SomeActive--; break; // keep solving } if ( p->pPars->fVerbose ) @@ -1289,13 +1461,19 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) abctime timeSince = Abc_Clock() - clkOne; assert( p->pTime4Outs[p->iOutCur] > 0 ); p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0; - if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided + if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) ) // undecided { + SomeActive--; p->pPars->nDropOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); if ( !p->pPars->fNotVerbose ) - Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); + { + if ( p->pPars->fAnytime ) + Abc_Print( 1, "Timing out on output %*d in frame %d (retrying in next anytime pass).\n", nOutDigits, p->iOutCur, iFrame ); + else + Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); + } } p->timeToStopOne = 0; } @@ -1316,6 +1494,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); + + if ( p->pPars->fAnytime && ClausesAdded ) + Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) ); + Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManCreateSolver( p, ++iFrame ); if ( fPrintClauses ) @@ -1324,14 +1506,23 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintClauses( p, 0 ); } // push clauses into this timeframe - RetValue = Pdr_ManPushClauses( p ); - if ( RetValue == -1 ) + RetValue = 0; + if ( p->pPars->fAnytime ) + { + RetValue = Pdr_ManPushInfAndRecycledClauses( p ); + ClausesAdded = 0; + } + + RetValue = RetValue == -1 ? -1 : Pdr_ManPushClauses( p ); + if ( RetValue == -1 || !SomeActive ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) { - if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + if ( !SomeActive ) + Abc_Print( 1, "All outputs solved or timed out in frame %d.\n", iFrame ); + else if ( p->timeToStop && Abc_Clock() > p->timeToStop ) Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); @@ -1343,22 +1534,34 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); - if ( !p->pPars->fSilent ) - Pdr_ManReportInvariant( p ); - if ( !p->pPars->fSilent ) - Pdr_ManVerifyInvariant( p ); + if ( !p->pPars->fAnytime ) + { + if ( !p->pPars->fSilent ) + Pdr_ManReportInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManVerifyInvariant( p ); + } p->pPars->iFrame = iFrame; - // count the number of UNSAT outputs - p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' if ( p->pPars->vOutMap ) - for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ ) - if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown + { + for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ ) + if ( Vec_IntEntry(p->pPars->vOutMap, i) == -2 ) // unknown { - Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat + Abc_Print( 1, "Proved output %d in frame %d (converged).\n", i ); + p->pPars->nProveOuts++; if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); + Gia_ManToBridgeResult( stdout, 1, NULL, i ); } + if ( p->pPars->nDropOuts > 0 ) + return -1; + } + else + { + // count the number of UNSAT outputs + p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; + } if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) return 1; // UNSAT if ( p->pPars->nFailOuts > 0 ) @@ -1416,6 +1619,61 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return -1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_ManResetReuseInvariant( Pdr_Man_t * p ) +{ + int i, k, nTimeOutU; + Pdr_Set_t * pCla; + sat_solver * pSat; + + Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) ); + + Vec_PtrClear( p->vInfCubes ); + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k ) + Vec_PtrPush( p->vInfCubes, pCla ); + + Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i ) + sat_solver_delete( pSat ); + Vec_PtrFree( p->vSolvers ); + Vec_VecFree( p->vClauses ); + Pdr_QueueStop( p ); + Vec_IntFree( p->vActVars ); + + p->vSolvers = Vec_PtrAlloc( 0 ); + p->vClauses = Vec_VecAlloc( 0 ); + p->pQueue = NULL; + p->vActVars = Vec_IntAlloc( 256 ); + + + Vec_IntFill (p->vPrio, Vec_IntSize(p->vPrio), 0); + p->nAbsFlops = 0; + + for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ ) + { + p->pTime4Outs[i] = p->pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; + + if ( Vec_IntEntry(p->pPars->vOutMap, i) == -1 ) // timeout + Vec_IntWriteEntry( p->pPars->vOutMap, i, -2 ); // unknown + } + + p->pPars->nDropOuts = 0; + p->pPars->nTimeOutOne *= 2; + nTimeOutU = p->pPars->nTimeOutOne * (Saig_ManPoNum(p->pAig) - p->pPars->nProveOuts - p->pPars->nFailOuts); + p->pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX + + Abc_Print( 1, "Starting new anytime pass, reusing clauses.\n" ); +} + /**Function************************************************************* Synopsis [] @@ -1430,12 +1688,21 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; - int k, RetValue; + int k, RetValue, nTimeOutU; abctime clk = Abc_Clock(); - if ( pPars->nTimeOutOne && !pPars->fSolveAll ) + if ( pPars->fAnytime ) + { + if ( pPars->nTimeOutOne == 0 ) + pPars->nTimeOutOne = 200; + } + if ( pPars->nTimeOutOne && !(pPars->fSolveAll || pPars->fAnytime) ) pPars->nTimeOutOne = 0; if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 ) - pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0); + { + nTimeOutU = pPars->nTimeOutOne * (Saig_ManPoNum(pAig) - pPars->nProveOuts - pPars->nFailOuts); + pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX + } + if ( pPars->fVerbose ) { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); @@ -1451,7 +1718,17 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) } ABC_FREE( pAig->pSeqModel ); p = Pdr_ManStart( pAig, pPars, NULL ); - RetValue = Pdr_ManSolveInt( p ); + + while (1) { + + RetValue = Pdr_ManSolveInt( p ); + if ( RetValue == -1 && Saig_ManPoNum(p->pAig) == pPars->nProveOuts + pPars->nFailOuts ) + RetValue = pPars->nFailOuts == 0; + if ( RetValue == -1 && pPars->fAnytime ) + Pdr_ManResetReuseInvariant( p ); + else + break; + } if ( RetValue == 0 ) assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); if ( p->vCexes ) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 6ba68db99..28cf491e4 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -379,6 +379,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) int iFrame, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; + p->tStart = clkStart; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; // assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved @@ -678,7 +679,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) //if ( p->pPars->fUseAbs && p->vAbsFlops ) // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); // open a new timeframe - p->nQueLim = p->pPars->nRestLimit; + p->nQueLim = iFrame + p->pPars->nRestLimit; + p->nQueLimStep = 1; assert( pCube == NULL ); Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManCreateSolver( p, ++iFrame ); diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 4a96b071b..b1375e1be 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -58,6 +58,8 @@ #define sat_solver_compress(s) #endif +#define PDR_INF_BOUND ((int)((~((unsigned int)0)) >> 1)) + ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// @@ -76,6 +78,7 @@ struct Pdr_Set_t_ { word Sign; // signature int nRefs; // ref counter + int iBound; // known to hold up to this frame, INT_MAX = inf int nTotal; // total literals int nLits; // num flop literals int Lits[0]; @@ -156,8 +159,11 @@ struct Pdr_Man_t_ int nQueCur; int nQueMax; int nQueLim; + int nQueLimStep; int nXsimRuns; int nXsimLits; + int nInfClauses; + int fNewInfClauses; // runtime abctime timeToStop; abctime timeToStopOne; @@ -172,6 +178,7 @@ struct Pdr_Man_t_ abctime tCnf; abctime tAbs; abctime tTotal; + abctime tStart; }; //////////////////////////////////////////////////////////////////////// @@ -253,6 +260,7 @@ extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec extern void ZPdr_SetPrint( Pdr_Set_t * p ); extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); +extern int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); extern void Pdr_OblDeref( Pdr_Obl_t * p ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index ae61ce2c0..d1ae5d9d1 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -48,14 +48,15 @@ ABC_NAMESPACE_IMPL_START void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) { Vec_Ptr_t * vVec; - int i, ThisSize, Length, LengthStart; + int i, ThisSize, Length, LengthStart, kLast, Value, Width; if ( Vec_PtrSize(p->vSolvers) < 2 ) { Abc_Print(1, "Frame " ); Abc_Print(1, "Clauses " ); Abc_Print(1, "Max Queue " ); Abc_Print(1, "Flops " ); - Abc_Print(1, "Cex " ); + if ( p->pPars->fUseAbs ) + Abc_Print(1, "Cex " ); Abc_Print(1, "Time" ); Abc_Print(1, "\n" ); return; @@ -64,8 +65,12 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) return; // count the total length of the printout Length = 0; + kLast = Vec_VecSize( p->vClauses ) - 1; + Vec_VecForEachLevel( p->vClauses, vVec, i ) - Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); + Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1 - (i == kLast ? p->nInfClauses : 0) ); + if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 ) + Length += 2 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+1); // determine the starting point LengthStart = Abc_MaxInt( 0, Length - 60 ); Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 ); @@ -78,26 +83,37 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Length = 0; Vec_VecForEachLevel( p->vClauses, vVec, i ) { + Value = Vec_PtrSize(vVec) - (i == kLast ? p->nInfClauses : 0); + Width = 1 + Abc_Base10Log(Value+1); if ( Length < LengthStart ) { - Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); + Length += Width; continue; } - Abc_Print( 1, " %d", Vec_PtrSize(vVec) ); - Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); - ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); + Abc_Print( 1, " %d", Value ); + Length += Width; + ThisSize += Width; + } + if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 ) + { + Abc_Print( 1, " ~%d", Vec_PtrSize(p->vInfCubes) ); + Length += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2); + ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2); } for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%5d", p->nQueMax ); Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); if ( p->pPars->fUseAbs ) - Abc_Print( 1, "%4d", p->nCexes ); + Abc_Print( 1, "%4d", p->nCexes ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); if ( p->pPars->nTimeOutOne ) Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); + if ( p->pPars->fAnytime ) + Abc_Print( 1, " PRV =%3d", p->pPars->nProveOuts ); + Abc_Print( 1, "%s", fClose ? "\n":"\r" ); if ( fClose ) p->nQueMax = 0, p->nCexes = 0; @@ -123,7 +139,7 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) + if ( pCube->iBound != PDR_INF_BOUND ) continue; for ( n = 0; n < pCube->nLits; n++ ) { @@ -376,7 +392,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Count = 0; Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) + if ( pCube->iBound != PDR_INF_BOUND ) continue; Count++; } @@ -406,7 +422,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) + if ( pCube->iBound != PDR_INF_BOUND ) continue; Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); fprintf( pFile, " 1\n" ); @@ -452,7 +468,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) + if ( pCube->iBound != PDR_INF_BOUND ) continue; Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); } @@ -566,7 +582,7 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) // add the clauses Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) // skip non-inductive + if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) // skip known non-inf continue; vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); @@ -576,31 +592,45 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) // check each clause Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) // skip non-inductive + if ( pCube->iBound >= 0 ) // skip clauses with known inf-ness continue; vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); - if ( RetValue != l_False ) // mark as non-inductive + if ( RetValue != l_False ) // mark as non-inf { - pCube->nRefs = -1; + pCube->iBound = ~pCube->iBound; fChanges = 1; } else Counter++; } + + + Vec_Ptr_t *vLevel; + sat_solver_delete( (sat_solver *)Vec_PtrPop( p->vSolvers ) ); + vLevel = (Vec_Ptr_t *)Vec_PtrPop( (Vec_Ptr_t *)p->vClauses ); + assert (Vec_PtrSize( vLevel ) == 0); + Vec_PtrFree( vLevel ); + Vec_IntPop( p->vActVars ); //Abc_Print(1, "Clauses = %d.\n", Counter ); //sat_solver_delete( pSat ); return fChanges; } + Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) { Vec_Int_t * vResult; Vec_Ptr_t * vCubes; Pdr_Set_t * pCube; - int i, v, kStart; + int i, v, kStart, kMax; // collect cubes used in the inductive invariant + kMax = Vec_PtrSize( p->vSolvers ); kStart = Pdr_ManFindInvariantStart( p ); vCubes = Pdr_ManCollectCubes( p, kStart ); + // mark all non-inf clauses as candidates + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + if (pCube->iBound != PDR_INF_BOUND) + pCube->iBound = ~pCube->iBound; // refine as long as there are changes if ( fReduce ) while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); @@ -609,14 +639,23 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) Vec_IntPush( vResult, 0 ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->nRefs == -1 ) // skip non-inductive + if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) { + Vec_PtrWriteEntry( vCubes, i, Vec_PtrEntryLast( vCubes ) ); + Vec_PtrPop( vCubes ); + i--; continue; + } + if (pCube->iBound != PDR_INF_BOUND) + { + p->nInfClauses++; + p->fNewInfClauses = 1; + pCube->iBound = PDR_INF_BOUND; + } Vec_IntAddToEntry( vResult, 0, 1 ); Vec_IntPush( vResult, pCube->nLits ); for ( v = 0; v < pCube->nLits; v++ ) Vec_IntPush( vResult, pCube->Lits[v] ); } - //Vec_PtrFree( vCubes ); Vec_PtrFreeP( &p->vInfCubes ); p->vInfCubes = vCubes; Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 7686ec03b..052dd731e 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -296,8 +296,9 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; } if ( pPars->fSolveAll ) - { p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); + if ( pPars->fSolveAll || p->pPars->fAnytime ) + { p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) ); Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 ); } diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index b1a5b66c4..becf713fd 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -99,7 +99,8 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ) // add the clauses Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) - Pdr_ManSolverAddClause( p, k, pCube ); + if ( pCube != NULL ) + Pdr_ManSolverAddClause( p, k, pCube ); return pSat; } diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index b2eaa2c76..e4b9fd18d 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -71,6 +71,7 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ) p->nLits = Vec_IntSize(vLits); p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits); p->nRefs = 1; + p->iBound = 0; p->Sign = 0; for ( i = 0; i < p->nLits; i++ ) { @@ -104,6 +105,7 @@ Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ) p->nLits = pSet->nLits - 1; p->nTotal = pSet->nTotal - 1; p->nRefs = 1; + p->iBound = 0; p->Sign = 0; for ( i = 0; i < pSet->nTotal; i++ ) { @@ -138,6 +140,7 @@ Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ) p->nLits = nLits; p->nTotal = nLits + pSet->nTotal - pSet->nLits; p->nRefs = 1; + p->iBound = 0; p->Sign = 0; for ( i = 0; i < nLits; i++ ) { @@ -171,6 +174,7 @@ Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ) p->nLits = pSet->nLits; p->nTotal = pSet->nTotal; p->nRefs = 1; + p->iBound = 0; p->Sign = pSet->Sign; for ( i = 0; i < pSet->nTotal; i++ ) p->Lits[i] = pSet->Lits[i]; @@ -501,6 +505,41 @@ int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) return 0; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) +{ + Pdr_Set_t * p1 = *pp1; + Pdr_Set_t * p2 = *pp2; + if (p1->iBound > p2->iBound) + return -1; + if (p1->iBound < p2->iBound) + return 1; + if (p1->nLits < p2->nLits) + return -1; + if (p1->nLits > p2->nLits) + return 1; + + int i; + for ( i = 0; i < p1->nLits && i < p2->nLits; i++ ) + { + if ( p1->Lits[i] > p2->Lits[i] ) + return -1; + if ( p1->Lits[i] < p2->Lits[i] ) + return 1; + } + return 0; +} + /**Function************************************************************* Synopsis []