summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaDup.c53
-rw-r--r--src/base/abci/abc.c99
-rw-r--r--src/misc/util/utilCex.c58
-rw-r--r--src/misc/util/utilCex.h1
-rw-r--r--src/sat/bmc/bmcCexCut.c104
6 files changed, 312 insertions, 4 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e24c9c2c..93387a05 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -767,6 +767,7 @@ extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut );
extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
+extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 378193b2..b0c5ca21 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1216,6 +1216,59 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
/**Function*************************************************************
+ Synopsis [Duplicates transition relation from p1 and property from p2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
+{
+ Gia_Man_t * pTemp, * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ // there is no flops in p2
+ assert( Gia_ManRegNum(p2) == 0 );
+ // there is only one PO in p2
+ assert( Gia_ManPoNum(p2) == 1 );
+ // flop count of p1 is equal to input count of p2
+ assert( Gia_ManRegNum(p1) == Gia_ManPiNum(p2) );
+
+ // start new AIG
+ pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) );
+ pNew->pName = Abc_UtilStrsav( p1->pName );
+ pNew->pSpec = Abc_UtilStrsav( p1->pSpec );
+ Gia_ManHashAlloc( pNew );
+ // dup first AIG
+ Gia_ManConst0(p1)->Value = 0;
+ Gia_ManForEachCi( p1, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachAnd( p1, pObj, i )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // dup second AIG
+ Gia_ManConst0(p2)->Value = 0;
+ Gia_ManForEachPi( p2, pObj, i )
+ pObj->Value = Gia_ManRo(p1, i)->Value;
+ Gia_ManForEachAnd( p2, pObj, i )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // add property output
+ pObj = Gia_ManPo( p2, 0 );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ // add flop inputs
+ Gia_ManForEachRi( p1, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManHashStop( pNew );
+// Gia_ManPrintStats( pGiaNew, 0 );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Print representatives.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 09e1c94e..7618c164 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -365,6 +365,7 @@ static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -820,6 +821,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmin", Abc_CommandAbc9CexMin, 0 );
Cmd_CommandAdd( pAbc, "Abstraction", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 );
@@ -28661,7 +28663,7 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
{
- Abc_Print( 1, "Current counter-example is not a valid counter-example for &-space AIG \"%s\".\n", Gia_ManName(pAbc->pGia) );
+ Abc_Print( 1, "Current CEX does not fail AIG \"%s\" in the &-space.\n", Gia_ManName(pAbc->pGia) );
return 0;
}
if ( iFrStop == ABC_INFINITY )
@@ -28681,7 +28683,100 @@ usage:
Abc_Print( -2, "\t extract logic representation of bad states\n" );
Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
- Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9CexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Cex_t * pCexNew;
+ int c;
+ int iFrStart = 0;
+ int iFrStop = ABC_INFINITY;
+ int fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStart = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStart < 0 )
+ goto usage;
+ break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStop < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pCex == NULL )
+ {
+ Abc_Print( 1, "There is no current cex.\n");
+ return 0;
+ }
+ if ( pAbc->pCex2 == NULL )
+ {
+ Abc_Print( 1, "There is no saved cex.\n");
+ return 0;
+ }
+ if ( iFrStop - iFrStart > pAbc->pCex->iFrame )
+ {
+ Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
+ return 0;
+ }
+ pCexNew = Abc_CexMerge( pAbc->pCex2, pAbc->pCex, iFrStart, iFrStop );
+ if ( pCexNew == NULL )
+ {
+ Abc_Print( 1, "Merging CEXes has failed.\n");
+ return 0;
+ }
+ // replace the saved CEX
+ ABC_FREE( pAbc->pCex2 );
+ pAbc->pCex2 = pCexNew;
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &cexmerge [-FG num] [-vh]\n" );
+ Abc_Print( -2, "\t merges the current CEX into the saved one\n" );
+ Abc_Print( -2, "\t and sets the resulting CEX as the saved one\n" );
+ Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
+ Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 80d8e141..16dbb076 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -172,6 +172,64 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
/**Function*************************************************************
+ Synopsis [Derives CEX from comb model.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd )
+{
+ Abc_Cex_t * pNew;
+ int nFramesGain;
+ int i, f, iBit;
+
+ if ( iFrBeg < 0 )
+ { printf( "Starting frame is less than 0.\n" ); return NULL; }
+ if ( iFrEnd < 0 )
+ { printf( "Stopping frame is less than 0.\n" ); return NULL; }
+ if ( iFrBeg > pCex->iFrame )
+ { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+ if ( iFrEnd > pCex->iFrame )
+ { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+ if ( iFrBeg >= iFrEnd )
+ { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
+ assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
+ assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
+ assert( iFrBeg < iFrEnd );
+
+ assert( pCex->nPis == pPart->nPis );
+ assert( iFrEnd - iFrBeg > pPart->iFrame );
+
+ nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
+ pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
+ pNew->iPo = pCex->iPo;
+ pNew->iFrame = pCex->iFrame - nFramesGain;
+
+ for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
+ if ( Abc_InfoHasBit(pCex->pData, iBit) )
+ Abc_InfoSetBit( pNew->pData, iBit++ );
+ for ( f = 0; f < iFrBeg; f++ )
+ for ( i = 0; i < pCex->nPis; i++ )
+ if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
+ Abc_InfoSetBit( pNew->pData, iBit++ );
+ for ( f = 0; f < pPart->iFrame; f++ )
+ for ( i = 0; i < pCex->nPis; i++ )
+ if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
+ Abc_InfoSetBit( pNew->pData, iBit++ );
+ for ( f = iFrEnd; f <= pCex->iFrame; f++ )
+ for ( i = 0; i < pCex->nPis; i++ )
+ if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
+ Abc_InfoSetBit( pNew->pData, iBit++ );
+ assert( iBit == pNew->nBits );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Prints out the counter-example.]
Description []
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index b45cd27b..1fd06f96 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -61,6 +61,7 @@ extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int
extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo );
+extern Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd );
extern void Abc_CexPrintStats( Abc_Cex_t * p );
extern void Abc_CexPrint( Abc_Cex_t * p );
extern void Abc_CexFreeP( Abc_Cex_t ** p );
diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
index 79944097..96d46fb3 100644
--- a/src/sat/bmc/bmcCexCut.c
+++ b/src/sat/bmc/bmcCexCut.c
@@ -42,9 +42,109 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd )
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose )
{
- return NULL;
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+ Vec_Bit_t * vInitNew;
+ int i, k, iBit = 0;
+
+ if ( iFrBeg < 0 )
+ { printf( "Starting frame is less than 0.\n" ); return NULL; }
+ if ( iFrEnd < 0 )
+ { printf( "Stopping frame is less than 0.\n" ); return NULL; }
+ if ( iFrBeg > pCex->iFrame )
+ { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+ if ( iFrEnd > pCex->iFrame )
+ { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+ if ( iFrBeg >= iFrEnd )
+ { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
+ assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
+ assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
+ assert( iFrBeg < iFrEnd );
+
+ // skip trough the first iFrEnd frames
+ Gia_ManCleanMark0(p);
+ Gia_ManForEachRo( p, pObj, i )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
+ for ( i = 0; i < iFrEnd; i++ )
+ {
+ // remember values in frame iFrBeg
+ if ( i == iFrBeg )
+ Gia_ManForEachRo( p, pObjRo, k )
+ if ( pObjRo->fMark0 )
+ Vec_BitWriteEntry( vInitNew, k, 1 );
+ // simulate other values
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ Gia_ManForEachAnd( p, pObj, k )
+ pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
+ (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ Gia_ManForEachCo( p, pObj, k )
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ pObjRo->fMark0 = pObjRi->fMark0;
+ }
+ assert( i == iFrEnd );
+
+ // create new AIG manager
+ pNew = Gia_ManStart( 10000 );
+ Gia_ManConst0(p)->Value = 1;
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->Value = 1;
+ Gia_ManForEachRo( p, pObjRo, i )
+ pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
+ Gia_ManHashStart( p );
+ for ( i = iFrEnd; i <= pCex->iFrame; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ Gia_ManForEachAnd( p, pObj, k )
+ {
+ pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
+ (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ if ( pObj->fMark0 )
+ pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 )
+ pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !Gia_ObjFanin0(pObj)->fMark0 )
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ else if ( !Gia_ObjFanin1(pObj)->fMark0 )
+ pObj->Value = Gia_ObjFanin1(pObj)->Value;
+ else assert( 0 );
+ }
+ Gia_ManForEachCo( p, pObj, k )
+ {
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ }
+ if ( i == pCex->iFrame )
+ break;
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ {
+ pObjRo->fMark0 = pObjRi->fMark0;
+ pObjRo->Value = pObjRi->Value;
+ }
+ }
+ Gia_ManHashStop( p );
+ assert( iBit == pCex->nBits );
+
+ // create PO
+ Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
+ // cleanup
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+
+ // create new GIA
+ pNew = Gia_ManDupWithNewPo( p, pTemp = pNew );
+ Gia_ManStop( pTemp );
+
+ // create new initial state
+ pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
+ Gia_ManStop( pTemp );
+ Vec_BitFree( vInitNew );
+ return pNew;
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 22:07:04 +0000