summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-01-13 13:32:18 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-01-13 13:32:18 -0800
commit624af674a0e7f1a675917afaaf371db6a5588821 (patch)
treec08e1438c9033da80c85b61585292ba4e95cb244
parentab80b015a4efdf196334aafc19d589d48778f0bb (diff)
downloadabc-624af674a0e7f1a675917afaaf371db6a5588821.tar.gz
abc-624af674a0e7f1a675917afaaf371db6a5588821.tar.bz2
abc-624af674a0e7f1a675917afaaf371db6a5588821.zip
New code since Dec 2010.
-rw-r--r--src/aig/gia/giaSim2.c705
-rw-r--r--src/aig/saig/saigTempor.c199
-rw-r--r--src/sat/pdr/module.make8
-rw-r--r--src/sat/pdr/pdr.c53
-rw-r--r--src/sat/pdr/pdr.h77
-rw-r--r--src/sat/pdr/pdrClass.c223
-rw-r--r--src/sat/pdr/pdrCnf.c354
-rw-r--r--src/sat/pdr/pdrCore.c692
-rw-r--r--src/sat/pdr/pdrInt.h187
-rw-r--r--src/sat/pdr/pdrInv.c351
-rw-r--r--src/sat/pdr/pdrMan.c190
-rw-r--r--src/sat/pdr/pdrSat.c351
-rw-r--r--src/sat/pdr/pdrTsim.c450
-rw-r--r--src/sat/pdr/pdrUtil.c547
14 files changed, 4387 insertions, 0 deletions
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
new file mode 100644
index 00000000..4131f942
--- /dev/null
+++ b/src/aig/gia/giaSim2.c
@@ -0,0 +1,705 @@
+/**CFile****************************************************************
+
+ FileName [giaSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Fast sequential simulator.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Gia_Sim2_t_ Gia_Sim2_t;
+struct Gia_Sim2_t_
+{
+ Gia_Man_t * pAig;
+ Gia_ParSim_t * pPars;
+ int nWords;
+ unsigned * pDataSim;
+ Vec_Int_t * vClassOld;
+ Vec_Int_t * vClassNew;
+};
+
+static inline unsigned * Gia_Sim2Data( Gia_Sim2_t * p, int i ) { return p->pDataSim + i * p->nWords; }
+
+extern void Gia_ManResetRandom( Gia_ParSim_t * pPars );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_Sim2Delete( Gia_Sim2_t * p )
+{
+ Vec_IntFreeP( &p->vClassOld );
+ Vec_IntFreeP( &p->vClassNew );
+ ABC_FREE( p->pDataSim );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates fast simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Sim2_t * Gia_Sim2Create( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
+{
+ Gia_Sim2_t * p;
+ Gia_Obj_t * pObj;
+ int i;
+ p = ABC_CALLOC( Gia_Sim2_t, 1 );
+ p->pAig = pAig;
+ p->pPars = pPars;
+ p->nWords = pPars->nWords;
+ p->pDataSim = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
+ if ( !p->pDataSim )
+ {
+ Abc_Print( 1, "Simulator could not allocate %.2f Gb for simulation info.\n",
+ 4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
+ Gia_Sim2Delete( p );
+ return NULL;
+ }
+ p->vClassOld = Vec_IntAlloc( 100 );
+ p->vClassNew = Vec_IntAlloc( 100 );
+ if ( pPars->fVerbose )
+ Abc_Print( 1, "Memory: AIG = %7.2f Mb. SimInfo = %7.2f Mb.\n",
+ 12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
+ // prepare AIG
+ Gia_ManSetPhase( pAig );
+ Gia_ManForEachObj( pAig, pObj, i )
+ pObj->Value = i;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoRandom( Gia_Sim2_t * p, unsigned * pInfo )
+{
+ int w;
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = Gia_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoZero( Gia_Sim2_t * p, unsigned * pInfo )
+{
+ int w;
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoOne( Gia_Sim2_t * p, unsigned * pInfo )
+{
+ int w;
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = ~0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoCopy( Gia_Sim2_t * p, unsigned * pInfo, unsigned * pInfo0 )
+{
+ int w;
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateCo( Gia_Sim2_t * p, Gia_Obj_t * pObj )
+{
+ unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
+ unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
+ int w;
+ if ( Gia_ObjFaninC0(pObj) )
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = ~pInfo0[w];
+ else
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateNode( Gia_Sim2_t * p, Gia_Obj_t * pObj )
+{
+ unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
+ unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
+ unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
+ int w;
+ if ( Gia_ObjFaninC0(pObj) )
+ {
+ if ( Gia_ObjFaninC1(pObj) )
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
+ else
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = ~pInfo0[w] & pInfo1[w];
+ }
+ else
+ {
+ if ( Gia_ObjFaninC1(pObj) )
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = pInfo0[w] & ~pInfo1[w];
+ else
+ for ( w = p->nWords-1; w >= 0; w-- )
+ pInfo[w] = pInfo0[w] & pInfo1[w];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoTransfer( Gia_Sim2_t * p )
+{
+ Gia_Obj_t * pObjRo, * pObjRi;
+ unsigned * pInfo0, * pInfo1;
+ int i;
+ Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
+ {
+ pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
+ pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
+ Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateRound( Gia_Sim2_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ pObj = Gia_ManConst0(p->pAig);
+ assert( Gia_ObjValue(pObj) == 0 );
+ Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+ Gia_ManForEachPi( p->pAig, pObj, i )
+ Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+ Gia_ManForEachAnd( p->pAig, pObj, i )
+ {
+ assert( Gia_ObjValue(pObj) == i );
+ Gia_Sim2SimulateNode( p, pObj );
+ }
+ Gia_ManForEachCo( p->pAig, pObj, i )
+ Gia_Sim2SimulateCo( p, pObj );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Compares simulation info of two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_Sim2CompareEqual( unsigned * p0, unsigned * p1, int nWords, int fCompl )
+{
+ int w;
+ if ( !fCompl )
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != p1[w] )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != ~p1[w] )
+ return 0;
+ return 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares simulation info of one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_Sim2CompareZero( unsigned * p0, int nWords, int fCompl )
+{
+ int w;
+ if ( !fCompl )
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != 0 )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != ~0 )
+ return 0;
+ return 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates equivalence class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_Sim2ClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
+{
+ int Repr = GIA_VOID, EntPrev = -1, Ent, i;
+ assert( Vec_IntSize(vClass) > 0 );
+ Vec_IntForEachEntry( vClass, Ent, i )
+ {
+ if ( i == 0 )
+ {
+ Repr = Ent;
+ Gia_ObjSetRepr( p, Ent, GIA_VOID );
+ EntPrev = Ent;
+ }
+ else
+ {
+ assert( Repr < Ent );
+ Gia_ObjSetRepr( p, Ent, Repr );
+ Gia_ObjSetNext( p, EntPrev, Ent );
+ EntPrev = Ent;
+ }
+ }
+ Gia_ObjSetNext( p, EntPrev, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines one equivalence class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_Sim2ClassRefineOne( Gia_Sim2_t * p, int i )
+{
+ Gia_Obj_t * pObj0, * pObj1;
+ unsigned * pSim0, * pSim1;
+ int Ent;
+ Vec_IntClear( p->vClassOld );
+ Vec_IntClear( p->vClassNew );
+ Vec_IntPush( p->vClassOld, i );
+ pObj0 = Gia_ManObj( p->pAig, i );
+ pSim0 = Gia_Sim2Data( p, i );
+ Gia_ClassForEachObj1( p->pAig, i, Ent )
+ {
+ pObj1 = Gia_ManObj( p->pAig, Ent );
+ pSim1 = Gia_Sim2Data( p, Ent );
+ if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
+ Vec_IntPush( p->vClassOld, Ent );
+ else
+ Vec_IntPush( p->vClassNew, Ent );
+ }
+ if ( Vec_IntSize( p->vClassNew ) == 0 )
+ return 0;
+ Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
+ Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
+ if ( Vec_IntSize(p->vClassNew) > 1 )
+ return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash key of the simuation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_Sim2HashKey( unsigned * pSim, int nWords, int nTableSize )
+{
+ static int s_Primes[16] = {
+ 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
+ 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+ unsigned uHash = 0;
+ int i;
+ if ( pSim[0] & 1 )
+ for ( i = 0; i < nWords; i++ )
+ uHash ^= ~pSim[i] * s_Primes[i & 0xf];
+ else
+ for ( i = 0; i < nWords; i++ )
+ uHash ^= pSim[i] * s_Primes[i & 0xf];
+ return (int)(uHash % nTableSize);
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines nodes belonging to candidate constant class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
+{
+ unsigned * pSim;
+ int * pTable, nTableSize, i, k, Key;
+ if ( Vec_IntSize(vRefined) == 0 )
+ return;
+ nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
+ pTable = ABC_CALLOC( int, nTableSize );
+ Vec_IntForEachEntry( vRefined, i, k )
+ {
+ pSim = Gia_Sim2Data( p, i );
+ Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
+ if ( pTable[Key] == 0 )
+ {
+ assert( Gia_ObjRepr(p->pAig, i) == 0 );
+ assert( Gia_ObjNext(p->pAig, i) == 0 );
+ Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+ }
+ else
+ {
+ Gia_ObjSetNext( p->pAig, pTable[Key], i );
+ Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
+ if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
+ Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
+ assert( Gia_ObjRepr(p->pAig, i) > 0 );
+ }
+ pTable[Key] = i;
+ }
+/*
+ Vec_IntForEachEntry( vRefined, i, k )
+ {
+ if ( Gia_ObjIsHead( p->pAig, i ) )
+ Gia_Sim2ClassRefineOne( p, i );
+ }
+*/
+ ABC_FREE( pTable );
+}
+/**Function*************************************************************
+
+ Synopsis [Refines equivalences after one simulation round.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_Sim2InfoRefineEquivs( Gia_Sim2_t * p )
+{
+ Vec_Int_t * vRefined;
+ Gia_Obj_t * pObj;
+ unsigned * pSim;
+ int i, Count = 0;
+ // process constant candidates
+ vRefined = Vec_IntAlloc( 100 );
+ Gia_ManForEachObj1( p->pAig, pObj, i )
+ {
+ if ( !Gia_ObjIsConst(p->pAig, i) )
+ continue;
+ pSim = Gia_Sim2Data( p, i );
+//Extra_PrintBinary( stdout, pSim, 32 * p->nWords ); printf( "\n" );
+ if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
+ {
+ Vec_IntPush( vRefined, i );
+ Count++;
+ }
+ }
+ Gia_Sim2ProcessRefined( p, vRefined );
+ Vec_IntFree( vRefined );
+ // process other classes
+ Gia_ManForEachClass( p->pAig, i )
+ Count += Gia_Sim2ClassRefineOne( p, i );
+// if ( Count )
+// printf( "Refined %d times.\n", Count );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns index of the first pattern that failed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Gia_Sim2InfoIsZero( Gia_Sim2_t * p, unsigned * pInfo )
+{
+ int w;
+ for ( w = 0; w < p->nWords; w++ )
+ if ( pInfo[w] )
+ return 32*w + Gia_WordFindFirstBit( pInfo[w] );
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns index of the PO and pattern that failed it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Gia_Sim2CheckPos( Gia_Sim2_t * p, int * piPo, int * piPat )
+{
+ Gia_Obj_t * pObj;
+ int i, iPat;
+ Gia_ManForEachPo( p->pAig, pObj, i )
+ {
+ iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
+ if ( iPat >= 0 )
+ {
+ *piPo = i;
+ *piPat = iPat;
+ return 1;
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat )
+{
+ Abc_Cex_t * p;
+ unsigned * pData;
+ int f, i, w, Counter;
+ p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+ p->iFrame = iFrame;
+ p->iPo = iOut;
+ // fill in the binary data
+ Counter = p->nRegs;
+ pData = ABC_ALLOC( unsigned, nWords );
+ for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+ for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
+ {
+ for ( w = nWords-1; w >= 0; w-- )
+ pData[w] = Gia_ManRandom( 0 );
+ if ( Gia_InfoHasBit( pData, iPat ) )
+ Gia_InfoSetBit( p->pData, Counter + i );
+ }
+ ABC_FREE( pData );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs simulation to refine equivalence classes.]
+
+ Description [Returns 1 if counter-example is detected.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
+{
+ Gia_Sim2_t * p;
+ Gia_Obj_t * pObj;
+ int i, clkTotal = clock();
+ int RetValue = 0, iOut, iPat;
+ assert( pAig->pReprs && pAig->pNexts );
+ ABC_FREE( pAig->pCexSeq );
+ p = Gia_Sim2Create( pAig, pPars );
+ Gia_ManResetRandom( pPars );
+ Gia_ManForEachRo( p->pAig, pObj, i )
+ Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+ for ( i = 0; i < pPars->nIters; i++ )
+ {
+ Gia_Sim2SimulateRound( p );
+ if ( pPars->fVerbose )
+ {
+ Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
+ if ( pAig->pReprs && pAig->pNexts )
+ Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
+ Abc_Print( 1, "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
+ }
+ if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
+ {
+ Gia_ManResetRandom( pPars );
+ pPars->iOutFail = iOut;
+ pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
+ Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
+ if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+ {
+// Abc_Print( 1, "\n" );
+ Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
+// Abc_Print( 1, "\n" );
+ }
+ else
+ {
+// Abc_Print( 1, "\n" );
+// if ( pPars->fVerbose )
+// Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
+// Abc_Print( 1, "\n" );
+ }
+ RetValue = 1;
+ break;
+ }
+ if ( pAig->pReprs && pAig->pNexts )
+ Gia_Sim2InfoRefineEquivs( p );
+ if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+ {
+ i++;
+ break;
+ }
+ if ( i < pPars->nIters - 1 )
+ Gia_Sim2InfoTransfer( p );
+ }
+ Gia_Sim2Delete( p );
+ if ( pAig->pCexSeq == NULL )
+ Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
+ Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
new file mode 100644
index 00000000..80bde75c
--- /dev/null
+++ b/src/aig/saig/saigTempor.c
@@ -0,0 +1,199 @@
+/**CFile****************************************************************
+
+ FileName [saigTempor.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Temporal decomposition.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates initialized timeframes for temporal decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f;
+ // start the frames package
+ Aig_ManCleanData( pAig );
+ pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+ pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ // initiliaze the flops
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->pData = Aig_ManConst0(pFrames);
+ // for each timeframe
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
+ Saig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pFrames);
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Aig_ManForEachPo( pAig, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
+ }
+ // create POs for the flop inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreatePo( pFrames, pObj->pData );
+ Aig_ManCleanup( pFrames );
+ return pFrames;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
+{
+ Aig_Man_t * pAigNew, * pFrames;
+ Aig_Obj_t * pObj, * pReset;
+ int i;
+ if ( pAig->nConstrs > 0 )
+ {
+ printf( "The AIG manager should have no constraints.\n" );
+ return NULL;
+ }
+ // create initialized timeframes
+ pFrames = Saig_ManTemporFrames( pAig, nFrames );
+ assert( Aig_ManPoNum(pFrames) == Aig_ManRegNum(pAig) );
+
+ // start the new manager
+ Aig_ManCleanData( pAig );
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ // map the constant node and primary inputs
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ Saig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+
+ // insert initialization logic
+ Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
+ Aig_ManForEachPi( pFrames, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ Aig_ManForEachNode( pFrames, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Aig_ManForEachPo( pFrames, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+
+ // create reset latch (the first one among the latches)
+ pReset = Aig_ObjCreatePi( pAigNew );
+
+ // create flop output values
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), Aig_ManPo(pFrames, i)->pData );
+ Aig_ManStop( pFrames );
+
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create primary outputs
+ Saig_ManForEachPo( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+
+ // create reset latch (the first one among the latches)
+ Aig_ObjCreatePo( pAigNew, Aig_ManConst1(pAigNew) );
+ // create latch inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+
+ // finalize
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
+{
+ extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose );
+ int RetValue, nFramesFinished = -1;
+ assert( nFrames >= 0 );
+ if ( nFrames == 0 )
+ {
+ nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose );
+ if ( nFrames == 1 )
+ {
+ printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
+ return NULL;
+ }
+ Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
+ }
+ else
+ Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
+ // run BMC2
+ if ( fUseBmc )
+ {
+ RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+ if ( RetValue == 0 )
+ {
+ printf( "A cex found in the first %d frames.\n", nFrames );
+ return NULL;
+ }
+ if ( nFramesFinished < nFrames )
+ {
+ printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
+ return NULL;
+ }
+ }
+ return Saig_ManTemporDecompose( pAig, nFrames );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/module.make b/src/sat/pdr/module.make
new file mode 100644
index 00000000..5cf4491c
--- /dev/null
+++ b/src/sat/pdr/module.make
@@ -0,0 +1,8 @@
+SRC += src/sat/pdr/pdr.c \
+ src/sat/pdr/pdrCnf.c \
+ src/sat/pdr/pdrCore.c \
+ src/sat/pdr/pdrInv.c \
+ src/sat/pdr/pdrMan.c \
+ src/sat/pdr/pdrSat.c \
+ src/sat/pdr/pdrTsim.c \
+ src/sat/pdr/pdrUtil.c
diff --git a/src/sat/pdr/pdr.c b/src/sat/pdr/pdr.c
new file mode 100644
index 00000000..6bdf75b5
--- /dev/null
+++ b/src/sat/pdr/pdr.c
@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+ FileName [pdr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
new file mode 100644
index 00000000..1099c621
--- /dev/null
+++ b/src/sat/pdr/pdr.h
@@ -0,0 +1,77 @@
+/**CFile****************************************************************
+
+ FileName [pdr.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __PDR_H__
+#define __PDR_H__
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pdr_Par_t_ Pdr_Par_t;
+struct Pdr_Par_t_
+{
+ int iOutput; // zero-based number of primary output to solve
+ int nRecycle; // limit on vars for recycling
+ int nFrameMax; // limit on frame count
+ int nConfLimit; // limit on SAT solver conflicts
+ int nTimeOut; // timeout in seconds
+ int fTwoRounds; // use two rounds for generalization
+ int fMonoCnf; // monolythic CNF
+ int fDumpInv; // dump inductive invariant
+ int fShortest; // forces bug traces to be shortest
+ int fVerbose; // verbose output
+ int fVeryVerbose; // very verbose output
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pdrCore.c ==========================================================*/
+extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
+extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c
new file mode 100644
index 00000000..31449735
--- /dev/null
+++ b/src/sat/pdr/pdrClass.c
@@ -0,0 +1,223 @@
+/**CFile****************************************************************
+
+ FileName [pdrClass.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Equivalence classes of register outputs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs duplication with the variable map.]
+
+ Description [Var map contains -1 if const0 and <reg_num> otherwise.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj;
+ int i, iReg;
+ assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) );
+ // start the fraig package
+ pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+ pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+ // create CI mapping
+ Aig_ManCleanData( pAig );
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pFrames);
+ Saig_ManForEachLo( pAig, pObj, i )
+ {
+ iReg = Vec_IntEntry(vMap, i);
+ if ( iReg == -1 )
+ pObj->pData = Aig_ManConst0(pFrames);
+ else
+ pObj->pData = Saig_ManLo(pAig, iReg)->pData;
+ }
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // add output nodes
+ Aig_ManForEachPo( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ // finish off
+ Aig_ManCleanup( pFrames );
+ Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates mapping of registers.]
+
+ Description [Var map contains -1 if const0 and <reg_num> otherwise.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ Vec_Int_t * vMap;
+ int * pLit2Id, Lit, i;
+ pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 );
+ for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ )
+ pLit2Id[i] = -1;
+ vMap = Vec_IntAlloc( Aig_ManRegNum(p) );
+ Saig_ManForEachLi( p, pObj, i )
+ {
+ if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) )
+ {
+ Vec_IntPush( vMap, -1 );
+ continue;
+ }
+ Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj);
+ if ( pLit2Id[Lit] < 0 ) // the first time
+ pLit2Id[Lit] = i;
+ Vec_IntPush( vMap, pLit2Id[Lit] );
+ }
+ ABC_FREE( pLit2Id );
+ return vMap;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts reduced registers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManCountMap( Vec_Int_t * vMap )
+{
+ int i, Entry, Counter = 0;
+ Vec_IntForEachEntry( vMap, Entry, i )
+ if ( Entry != i )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts reduced registers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManPrintMap( Vec_Int_t * vMap )
+{
+ Vec_Int_t * vMarks;
+ int f, i, iClass, Entry, Counter = 0;
+ printf( " Consts: " );
+ Vec_IntForEachEntry( vMap, Entry, i )
+ if ( Entry == -1 )
+ printf( "%d ", i );
+ printf( "\n" );
+ vMarks = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntry( vMap, iClass, f )
+ {
+ if ( iClass == -1 )
+ continue;
+ if ( iClass == f )
+ continue;
+ // check previous classes
+ if ( Vec_IntFind( vMarks, iClass ) >= 0 )
+ continue;
+ Vec_IntPush( vMarks, iClass );
+ // print class
+ printf( " Class %d : ", iClass );
+ Vec_IntForEachEntry( vMap, Entry, i )
+ if ( Entry == iClass )
+ printf( "%d ", i );
+ printf( "\n" );
+ }
+ Vec_IntFree( vMarks );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManEquivClasses( Aig_Man_t * pAig )
+{
+ Vec_Int_t * vMap;
+ Aig_Man_t * pTemp;
+ int f, nFrames = 100;
+ assert( Saig_ManRegNum(pAig) > 0 );
+ // start the map
+ vMap = Vec_IntAlloc( 0 );
+ Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 );
+ // iterate and print changes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // implement variable map
+ pTemp = Pdr_ManRehashWithMap( pAig, vMap );
+ // report the result
+ printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
+ f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap),
+ Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
+ // recreate the map
+ Pdr_ManPrintMap( vMap );
+ Vec_IntFree( vMap );
+ vMap = Pdr_ManCreateMap( pTemp );
+ Aig_ManStop( pTemp );
+ if ( Pdr_ManCountMap(vMap) == 0 )
+ break;
+ }
+ Vec_IntFree( vMap );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
new file mode 100644
index 00000000..b40ed6d9
--- /dev/null
+++ b/src/sat/pdr/pdrCnf.c
@@ -0,0 +1,354 @@
+/**CFile****************************************************************
+
+ FileName [pdrCnf.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [CNF computation on demand.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrCnf.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+ The CNF (p->pCnf2) is expressed in terms of object IDs.
+ Each node in the CNF is marked if it has clauses (p->pCnf2->pObj2Count[Id] > 0).
+ Each node in the CNF has the first clause (p->pCnf2->pObj2Clause)
+ and the number of clauses (p->pCnf2->pObj2Count).
+ Each node used in a CNF of any timeframe has its SAT var recorded.
+ Each frame has a reserve mapping of SAT variables into ObjIds.
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns SAT variable of the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
+{
+ return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns SAT variable of the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
+{
+ assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
+ if ( p->pvId2Vars[Aig_ObjId(pObj)] == NULL )
+ p->pvId2Vars[Aig_ObjId(pObj)] = Vec_IntStart( 16 );
+ if ( Vec_IntGetEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ) == 0 )
+ {
+ sat_solver * pSat = Pdr_ManSolver(p, k);
+ Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
+ int iVarNew = Vec_IntSize( vVar2Ids );
+ assert( iVarNew > 0 );
+ Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
+ Vec_IntWriteEntry( p->pvId2Vars[Aig_ObjId(pObj)], k, iVarNew );
+ sat_solver_setnvars( pSat, iVarNew + 1 );
+ if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
+ {
+ int Lit = toLitCond( iVarNew, 1 );
+ int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+ assert( RetValue == 1 );
+ sat_solver_compress( pSat );
+ }
+ }
+ return Vec_IntEntry( p->pvId2Vars[Aig_ObjId(pObj)], k );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively adds CNF for the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vLits;
+ Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
+ int nVarCount = Vec_IntSize(vVar2Ids);
+ int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
+ int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
+ if ( nVarCount == Vec_IntSize(vVar2Ids) )
+ return iVarThis;
+ assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
+ if ( Aig_ObjIsPi(pObj) )
+ return iVarThis;
+ nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
+ iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
+ assert( nClauses > 0 );
+ pSat = Pdr_ManSolver(p, k);
+ vLits = Vec_IntAlloc( 16 );
+ for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
+ {
+ Vec_IntClear( vLits );
+ for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
+ {
+ iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)) );
+ Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+ }
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+ assert( RetValue );
+ }
+ Vec_IntFree( vLits );
+ return iVarThis;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns SAT variable of the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
+{
+ if ( p->pPars->fMonoCnf )
+ return Pdr_ObjSatVar1( p, k, pObj );
+ else
+ return Pdr_ObjSatVar2( p, k, pObj );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns register number for the given SAT variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Pdr_ObjRegNum1( Pdr_Man_t * p, int k, int iSatVar )
+{
+ int RegId;
+ assert( iSatVar >= 0 );
+ // consider the case of auxiliary variable
+ if ( iSatVar >= p->pCnf1->nVars )
+ return -1;
+ // consider the case of register output
+ RegId = Vec_IntEntry( p->vVar2Reg, iSatVar );
+ assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
+ return RegId;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns register number for the given SAT variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
+{
+ Aig_Obj_t * pObj;
+ int ObjId;
+ Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
+ assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) );
+ ObjId = Vec_IntEntry( vVar2Ids, iSatVar );
+ if ( ObjId == -1 ) // activation variable
+ return -1;
+ pObj = Aig_ManObj( p->pAig, ObjId );
+ if ( Saig_ObjIsLi( p->pAig, pObj ) )
+ return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig);
+ assert( 0 ); // should be called for register inputs only
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns register number for the given SAT variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar )
+{
+ if ( p->pPars->fMonoCnf )
+ return Pdr_ObjRegNum1( p, k, iSatVar );
+ else
+ return Pdr_ObjRegNum2( p, k, iSatVar );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns the index of unused SAT variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManFreeVar( Pdr_Man_t * p, int k )
+{
+ if ( p->pPars->fMonoCnf )
+ return sat_solver_nvars( Pdr_ManSolver(p, k) );
+ else
+ {
+ Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( p->vVar2Ids, k );
+ Vec_IntPush( vVar2Ids, -1 );
+ return Vec_IntSize( vVar2Ids ) - 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
+{
+ sat_solver * pSat;
+ Aig_Obj_t * pObj;
+ int i;
+ if ( p->pCnf1 == NULL )
+ {
+ int nRegs = p->pAig->nRegs;
+ p->pAig->nRegs = Aig_ManPoNum(p->pAig);
+ p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
+ p->pAig->nRegs = nRegs;
+ assert( p->vVar2Reg == NULL );
+ p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
+ }
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf1, 1, fInit );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vVar2Ids;
+ int i, Entry;
+ if ( p->pCnf2 == NULL )
+ {
+ p->pCnf2 = Cnf_DeriveOther( p->pAig );
+ p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
+ p->vVar2Ids = Vec_PtrAlloc( 256 );
+ }
+ // update the variable mapping
+ vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( p->vVar2Ids, k );
+ if ( vVar2Ids == NULL )
+ {
+ vVar2Ids = Vec_IntAlloc( 500 );
+ Vec_PtrWriteEntry( p->vVar2Ids, k, vVar2Ids );
+ }
+ Vec_IntForEachEntry( vVar2Ids, Entry, i )
+ {
+ if ( Entry == -1 )
+ continue;
+ assert( Vec_IntEntry( p->pvId2Vars[Entry], k ) > 0 );
+ Vec_IntWriteEntry( p->pvId2Vars[Entry], k, 0 );
+ }
+ Vec_IntClear( vVar2Ids );
+ Vec_IntPush( vVar2Ids, -1 );
+ // start the SAT solver
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, 500 );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit )
+{
+ if ( p->pPars->fMonoCnf )
+ return Pdr_ManNewSolver1( p, k, fInit );
+ else
+ return Pdr_ManNewSolver2( p, k, fInit );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
new file mode 100644
index 00000000..f1c10443
--- /dev/null
+++ b/src/sat/pdr/pdrCore.c
@@ -0,0 +1,692 @@
+/**CFile****************************************************************
+
+ FileName [pdrCore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the state could be blocked.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Pdr_Par_t) );
+ pPars->iOutput = -1; // zero-based output number
+ pPars->nRecycle = 300; // limit on vars for recycling
+ pPars->nFrameMax = 5000; // limit on number of timeframes
+ pPars->nTimeOut = 0; // timeout in seconds
+ pPars->nConfLimit = 100000; // limit on SAT solver conflicts
+ pPars->fTwoRounds = 0; // use two rounds for generalization
+ pPars->fMonoCnf = 0; // monolythic CNF
+ pPars->fDumpInv = 0; // dump inductive invariant
+ pPars->fShortest = 0; // forces bug traces to be shortest
+ pPars->fVerbose = 0; // verbose output
+ pPars->fVeryVerbose = 0; // very verbose output
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces clause using analyzeFinal.]
+
+ Description [Assumes that the SAT solver just terminated an UNSAT call.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+ Pdr_Set_t * pCubeMin;
+ Vec_Int_t * vLits;
+ int i, Entry, nCoreLits, * pCoreLits;
+ // get relevant SAT literals
+ nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
+ // translate them into register literals and remove auxiliary
+ vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
+ // skip if there is no improvement
+ if ( Vec_IntSize(vLits) == pCube->nLits )
+ return NULL;
+ assert( Vec_IntSize(vLits) < pCube->nLits );
+ // if the cube overlaps with init, add any literal
+ Vec_IntForEachEntry( vLits, Entry, i )
+ if ( lit_sign(Entry) == 0 ) // positive literal
+ break;
+ if ( i == Vec_IntSize(vLits) ) // only negative literals
+ {
+ // add the first positive literal
+ for ( i = 0; i < pCube->nLits; i++ )
+ if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
+ {
+ Vec_IntPush( vLits, pCube->Lits[i] );
+ break;
+ }
+ assert( i < pCube->nLits );
+ }
+ // generate a starting cube
+ pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
+ assert( !Pdr_SetIsInit(pCubeMin, -1) );
+/*
+ // make sure the cube works
+ {
+ int RetValue;
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
+ assert( RetValue );
+ }
+*/
+ return pCubeMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the state could be blocked.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManPushClauses( Pdr_Man_t * p )
+{
+ Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
+ Vec_Ptr_t * vArrayK, * vArrayK1;
+ int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1;
+ int Counter = 0;
+ int clk = clock();
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax-1 )
+ {
+ Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ vArrayK1 = (Vec_Ptr_t *)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 ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
+ continue;
+ Pdr_SetDeref( pTemp );
+ Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
+ Vec_PtrPop(vArrayK);
+ m--;
+ }
+
+ // check if the clause can be moved to the next frame
+ if ( !Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ) )
+ continue;
+
+ {
+ Pdr_Set_t * pCubeMin;
+ pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
+ if ( pCubeMin != NULL )
+ {
+// printf( "%d ", pCubeK->nLits - pCubeMin->nLits );
+ Pdr_SetDeref( pCubeK );
+ pCubeK = pCubeMin;
+ }
+ }
+
+ // if it can be moved, add it to the next frame
+ Pdr_ManSolverAddClause( p, k+1, pCubeK );
+ // check if the clause subsumes others
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
+ {
+ if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
+ continue;
+ Pdr_SetDeref( pCubeK1 );
+ Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
+ Vec_PtrPop(vArrayK1);
+ i--;
+ }
+ // add the last clause
+ Vec_PtrPush( vArrayK1, pCubeK );
+ Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
+ Vec_PtrPop(vArrayK);
+ j--;
+ }
+ if ( Vec_PtrSize(vArrayK) == 0 )
+ RetValue = 1;
+ }
+
+ // clean up the last one
+ vArrayK = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, kMax );
+ Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
+ {
+ // remove cubes in the same frame that are contained by pCubeK
+ Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
+ {
+ if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
+ continue;
+/*
+ printf( "===\n" );
+ Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
+ printf( "\n" );
+ Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
+ printf( "\n" );
+*/
+ Pdr_SetDeref( pTemp );
+ Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
+ Vec_PtrPop(vArrayK);
+ m--;
+ }
+ }
+ p->tPush += clock() - clk;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the clause is contained in higher clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
+{
+ Pdr_Set_t * pThis;
+ Vec_Ptr_t * vArrayK;
+ int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax )
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
+ if ( Pdr_SetContains( pSet, pThis ) )
+ return 1;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Sorts literals by priority.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
+{
+ int * pPrios = Vec_IntArray(p->vPrio);
+ int * pArray = p->pOrder;
+ int temp, i, j, best_i, nSize = pCube->nLits;
+ // initialize variable order
+ for ( i = 0; i < nSize; i++ )
+ pArray[i] = i;
+ for ( i = 0; i < nSize-1; i++ )
+ {
+ best_i = i;
+ for ( j = i+1; j < nSize; j++ )
+// if ( pArray[j] < pArray[best_i] )
+ if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
+ best_i = j;
+ temp = pArray[i];
+ pArray[i] = pArray[best_i];
+ pArray[best_i] = temp;
+ }
+/*
+ for ( i = 0; i < pCube->nLits; i++ )
+ printf( "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
+ printf( "\n" );
+*/
+ return pArray;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the state could be blocked.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
+{
+ Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
+ int i, j, n, Lit, RetValue, clk = clock();
+ int * pOrder;
+ // if there is no induction, return
+ *ppCubeMin = NULL;
+ RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ return -1;
+ if ( RetValue == 0 )
+ {
+ p->tGeneral += clock() - clk;
+ return 0;
+ }
+ // reduce clause using assumptions
+// pCubeMin = Pdr_SetDup( pCube );
+ pCubeMin = Pdr_ManReduceClause( p, k, pCube );
+ if ( pCubeMin == NULL )
+ pCubeMin = Pdr_SetDup( pCube );
+
+ // sort literals by their occurences
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+
+ // try removing literals
+ for ( j = 0; j < pCubeMin->nLits; j++ )
+ {
+ // use ordering
+// i = j;
+ i = pOrder[j];
+
+ // check init state
+ assert( pCubeMin->Lits[i] != -1 );
+ if ( Pdr_SetIsInit(pCubeMin, i) )
+ continue;
+ // try removing this literal
+ Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ {
+ Pdr_SetDeref( pCubeMin );
+ return -1;
+ }
+ pCubeMin->Lits[i] = Lit;
+ if ( RetValue == 0 )
+ continue;
+
+ // remove j-th entry
+ for ( n = j; n < pCubeMin->nLits-1; n++ )
+ pOrder[n] = pOrder[n+1];
+ j--;
+
+ // success - update the cube
+ pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+ Pdr_SetDeref( pCubeTmp );
+ assert( pCubeMin->nLits > 0 );
+ i--;
+
+ // get the ordering by decreasing priorit
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ }
+
+ if ( p->pPars->fTwoRounds )
+ for ( j = 0; j < pCubeMin->nLits; j++ )
+ {
+ // use ordering
+// i = j;
+ i = pOrder[j];
+
+ // check init state
+ assert( pCubeMin->Lits[i] != -1 );
+ if ( Pdr_SetIsInit(pCubeMin, i) )
+ continue;
+ // try removing this literal
+ Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ {
+ Pdr_SetDeref( pCubeMin );
+ return -1;
+ }
+ pCubeMin->Lits[i] = Lit;
+ if ( RetValue == 0 )
+ continue;
+
+ // remove j-th entry
+ for ( n = j; n < pCubeMin->nLits-1; n++ )
+ pOrder[n] = pOrder[n+1];
+ j--;
+
+ // success - update the cube
+ pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+ Pdr_SetDeref( pCubeTmp );
+ assert( pCubeMin->nLits > 0 );
+ i--;
+
+ // get the ordering by decreasing priorit
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ }
+
+ assert( ppCubeMin != NULL );
+ *ppCubeMin = pCubeMin;
+ p->tGeneral += clock() - clk;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the state could be blocked.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
+{
+ Pdr_Obl_t * pThis;
+ Pdr_Set_t * pPred, * pCubeMin;
+ int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
+ int kMax = Vec_PtrSize(p->vSolvers)-1, clk;
+ p->nBlocks++;
+ // create first proof obligation
+ assert( p->pQueue == NULL );
+ pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
+ Pdr_QueuePush( p, pThis );
+ // try to solve it recursively
+ while ( !Pdr_QueueIsEmpty(p) )
+ {
+ Counter++;
+ pThis = Pdr_QueueHead( p );
+ if ( pThis->iFrame == 0 )
+ return 0; // SAT
+ pThis = Pdr_QueuePop( p );
+ assert( pThis->iFrame > 0 );
+ assert( !Pdr_SetIsInit(pThis->pState, -1) );
+
+ clk = clock();
+ if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
+ {
+ p->tContain += clock() - clk;
+ Pdr_OblDeref( pThis );
+ continue;
+ }
+ p->tContain += clock() - clk;
+
+ // check if the cube is already contained
+ if ( Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState ) ) // cube is blocked by clauses in this frame
+ {
+ Pdr_OblDeref( pThis );
+ continue;
+ }
+
+ // check if the cube holds with relative induction
+ pCubeMin = NULL;
+ RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
+ if ( RetValue == -1 )
+ {
+ Pdr_OblDeref( pThis );
+ return -1;
+ }
+ if ( RetValue ) // cube is blocked inductively in this frame
+ {
+ assert( pCubeMin != NULL );
+
+ // k is the last frame where pCubeMin holds
+ k = pThis->iFrame;
+
+ // check other frames
+ assert( pPred == NULL );
+ for ( k = pThis->iFrame; k < kMax; k++ )
+ if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) )
+ break;
+
+ // add new clause
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "Adding cube " );
+ Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
+ printf( " to frame %d.\n", k );
+ }
+ // set priority flops
+ for ( i = 0; i < pCubeMin->nLits; i++ )
+ {
+ assert( pCubeMin->Lits[i] >= 0 );
+ assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
+ Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
+ }
+
+ Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
+ p->nCubes++;
+ // add clause
+ for ( i = 1; i <= k; i++ )
+ Pdr_ManSolverAddClause( p, i, pCubeMin );
+ // schedule proof obligation
+ if ( k < kMax && !p->pPars->fShortest )
+ {
+ pThis->iFrame = k+1;
+ pThis->prio = Prio--;
+ Pdr_QueuePush( p, pThis );
+ }
+ else
+ {
+ Pdr_OblDeref( pThis );
+ }
+ }
+ else
+ {
+ assert( pCubeMin == NULL );
+ assert( pPred != NULL );
+ pThis->prio = Prio--;
+ Pdr_QueuePush( p, pThis );
+
+ pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
+ Pdr_QueuePush( p, pThis );
+ }
+
+ // check the timeout
+ if ( p->timeToStop && clock() >= p->timeToStop )
+ return -1;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManSolveInt( Pdr_Man_t * p )
+{
+ int fPrintClauses = 0;
+ Pdr_Set_t * pCube;
+ int k, RetValue = -1;
+ int clkTotal = clock();
+ int clkStart = clock();
+ p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut);
+ assert( Vec_PtrSize(p->vSolvers) == 0 );
+ // create the first timeframe
+ Pdr_ManCreateSolver( p, (k = 0) );
+ while ( 1 )
+ {
+ p->nFrames = k;
+ assert( k == Vec_PtrSize(p->vSolvers)-1 );
+ RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ return -1;
+ }
+ if ( RetValue == 0 )
+ {
+ RetValue = Pdr_ManBlockCube( p, pCube );
+ if ( RetValue == -1 )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ return -1;
+ }
+ if ( RetValue == 0 )
+ {
+ if ( fPrintClauses )
+ {
+ printf( "*** Clauses after frame %d:\n", k );
+ Pdr_ManPrintClauses( p, 0 );
+ }
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ return 0; // SAT
+ }
+ }
+ else
+ {
+ // open a new timeframe
+ assert( pCube == NULL );
+ Pdr_ManSetPropertyOutput( p, k );
+ Pdr_ManCreateSolver( p, ++k );
+ if ( fPrintClauses )
+ {
+ printf( "*** Clauses after frame %d:\n", k );
+ Pdr_ManPrintClauses( p, 0 );
+ }
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 0, clock() - clkStart );
+ // push clauses into this timeframe
+ if ( Pdr_ManPushClauses( p ) )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManReportInvariant( p );
+ Pdr_ManVerifyInvariant( p );
+ if ( p->pPars->fDumpInv )
+ Pdr_ManDumpClauses( p, (char *)"inv.pla" );
+ return 1; // UNSAT
+ }
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ clkStart = clock();
+ }
+
+ // check the timeout
+ if ( p->timeToStop && clock() >= p->timeToStop )
+ {
+ if ( fPrintClauses )
+ {
+ printf( "*** Clauses after frame %d:\n", k );
+ Pdr_ManPrintClauses( p, 0 );
+ }
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ return -1;
+ }
+ if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
+ return -1;
+ }
+ }
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex )
+{
+ Pdr_Man_t * p;
+ int RetValue;
+ int clk = clock();
+ p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
+ RetValue = Pdr_ManSolveInt( p );
+ *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+// if ( *ppCex && pPars->fVerbose )
+// printf( "Found counter-example in frame %d after exploring %d frames.\n",
+// (*ppCex)->iFrame, p->nFrames );
+ p->tTotal += clock() - clk;
+ if ( pvPrioInit )
+ {
+ *pvPrioInit = p->vPrio;
+ p->vPrio = NULL;
+ }
+ Pdr_ManStop( p );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+{
+/*
+ Vec_Int_t * vPrioInit = NULL;
+ int RetValue, nTimeOut;
+ if ( pPars->nTimeOut > 0 )
+ return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
+ nTimeOut = pPars->nTimeOut;
+ pPars->nTimeOut = 10;
+ RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
+ pPars->nTimeOut = nTimeOut;
+ if ( RetValue == -1 )
+ RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
+ Vec_IntFree( vPrioInit );
+ return RetValue;
+*/
+ return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
new file mode 100644
index 00000000..d0211278
--- /dev/null
+++ b/src/sat/pdr/pdrInt.h
@@ -0,0 +1,187 @@
+/**CFile****************************************************************
+
+ FileName [pdrInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Internal declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __PDR_INT_H__
+#define __PDR_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+#include "pdr.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pdr_Set_t_ Pdr_Set_t;
+struct Pdr_Set_t_
+{
+ word Sign; // signature
+ int nRefs; // ref counter
+ short nTotal; // total literals
+ short nLits; // num flop literals
+ int Lits[0];
+};
+
+typedef struct Pdr_Obl_t_ Pdr_Obl_t;
+struct Pdr_Obl_t_
+{
+ int iFrame; // time frame
+ int prio; // priority
+ int nRefs; // reference counter
+ Pdr_Set_t * pState; // state cube
+ Pdr_Obl_t * pNext; // next one
+ Pdr_Obl_t * pLink; // queue link
+};
+
+typedef struct Pdr_Man_t_ Pdr_Man_t;
+struct Pdr_Man_t_
+{
+ // input problem
+ Pdr_Par_t * pPars; // parameters
+ Aig_Man_t * pAig; // user's AIG
+ // static CNF representation
+ Cnf_Dat_t * pCnf1; // CNF for this AIG
+ Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
+ // dynamic CNF representation
+ Cnf_Dat_t * pCnf2; // CNF for this AIG
+ Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var
+ Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId
+ // data representation
+ Vec_Ptr_t * vSolvers; // SAT solvers
+ Vec_Vec_t * vClauses; // clauses by timeframe
+ Pdr_Obl_t * pQueue; // proof obligations
+ int * pOrder; // ordering of the lits
+ Vec_Int_t * vActVars; // the counter of activation variables
+ // internal use
+ Vec_Int_t * vPrio; // priority flops
+ Vec_Int_t * vLits; // array of literals
+ Vec_Int_t * vCiObjs; // cone leaves
+ Vec_Int_t * vCoObjs; // cone roots
+ Vec_Int_t * vCiVals; // cone leaf values
+ Vec_Int_t * vCoVals; // cone root values
+ Vec_Int_t * vNodes; // cone nodes
+ Vec_Int_t * vUndo; // cone undos
+ Vec_Int_t * vVisits; // intermediate
+ Vec_Int_t * vCi2Rem; // CIs to be removed
+ Vec_Int_t * vRes; // final result
+ // statistics
+ int nBlocks; // the number of times blockState was called
+ int nObligs; // the number of proof obligations derived
+ int nCubes; // the number of cubes derived
+ int nCalls; // the number of SAT calls
+ int nCallsS; // the number of SAT calls (sat)
+ int nCallsU; // the number of SAT calls (unsat)
+ int nStarts; // the number of SAT solver restarts
+ int nFrames; // frames explored
+ // runtime
+ int timeStart;
+ int timeToStop;
+ // time stats
+ int tSat;
+ int tSatSat;
+ int tSatUnsat;
+ int tGeneral;
+ int tPush;
+ int tTsim;
+ int tContain;
+ int tCnf;
+ int tTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pdrCex.c ==========================================================*/
+extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
+/*=== pdrCnf.c ==========================================================*/
+extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
+extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
+extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
+extern sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit );
+/*=== pdrInv.c ==========================================================*/
+extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
+extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
+extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName );
+extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
+extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
+/*=== pdrMan.c ==========================================================*/
+extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
+extern void Pdr_ManStop( Pdr_Man_t * p );
+extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
+/*=== pdrSat.c ==========================================================*/
+extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
+extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
+extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
+extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
+extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
+extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
+extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
+extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
+extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
+/*=== pdrTsim.c ==========================================================*/
+extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
+/*=== pdrUtil.c ==========================================================*/
+extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
+extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
+extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
+extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
+extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
+extern void Pdr_SetDeref( Pdr_Set_t * p );
+extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
+extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
+extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
+extern int Pdr_SetCompare( 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 );
+extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
+extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
+extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
+extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
+extern void Pdr_QueuePrint( Pdr_Man_t * p );
+extern void Pdr_QueueStop( Pdr_Man_t * p );
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
new file mode 100644
index 00000000..184b6c4f
--- /dev/null
+++ b/src/sat/pdr/pdrInv.c
@@ -0,0 +1,351 @@
+/**CFile****************************************************************
+
+ FileName [pdrInv.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Invariant computation, printing, verification.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
+{
+ extern int Extra_Base10Log( unsigned int Num );
+ static int PastSize;
+ Vec_Ptr_t * vVec;
+ int i, ThisSize, Length, LengthStart;
+ if ( Vec_PtrSize(p->vSolvers) < 2 )
+ return;
+ // count the total length of the printout
+ Length = 0;
+ Vec_VecForEachLevel( p->vClauses, vVec, i )
+ Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
+ // determine the starting point
+ LengthStart = ABC_MAX( 0, Length - 70 );
+ printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
+ ThisSize = 6;
+ if ( LengthStart > 0 )
+ {
+ printf( " ..." );
+ ThisSize += 4;
+ }
+ Length = 0;
+ Vec_VecForEachLevel( p->vClauses, vVec, i )
+ {
+ if ( Length < LengthStart )
+ {
+ Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
+ continue;
+ }
+ printf( " %d", Vec_PtrSize(vVec) );
+ Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
+ ThisSize += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
+ }
+ if ( fClose )
+ {
+ for ( i = 0; i < PastSize - ThisSize; i++ )
+ printf( " " );
+ printf( "\n" );
+ }
+ else
+ {
+ printf( "\r" );
+ PastSize = ThisSize;
+ }
+// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts how many times each flop appears in the set of cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
+{
+ Vec_Int_t * vFlopCount;
+ Pdr_Set_t * pCube;
+ int i, n;
+ vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
+ Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+ for ( n = 0; n < pCube->nLits; n++ )
+ {
+ assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
+ Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
+ }
+ return vFlopCount;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
+{
+ Vec_Ptr_t * vArrayK;
+ int k, kMax = Vec_PtrSize(p->vSolvers)-1;
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
+ if ( Vec_PtrSize(vArrayK) == 0 )
+ return k;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of variables used in the clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
+{
+ Vec_Ptr_t * vResult;
+ Vec_Ptr_t * vArrayK;
+ Pdr_Set_t * pSet;
+ int i, j;
+ vResult = Vec_PtrAlloc( 100 );
+ Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
+ Vec_PtrPush( vResult, pSet );
+ return vResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of variables used in the clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
+{
+ Vec_Int_t * vFlopCounts;
+ Vec_Ptr_t * vCubes;
+ int i, Entry, Counter = 0;
+ vCubes = Pdr_ManCollectCubes( p, kStart );
+ vFlopCounts = Pdr_ManCountFlops( p, vCubes );
+ Vec_IntForEachEntry( vFlopCounts, Entry, i )
+ Counter += (Entry > 0);
+ Vec_IntFreeP( &vFlopCounts );
+ Vec_PtrFree( vCubes );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
+{
+ Vec_Ptr_t * vArrayK;
+ Pdr_Set_t * pCube;
+ int i, k, Counter = 0;
+ Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
+ {
+ Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
+ {
+ printf( "C=%4d. F=%4d ", Counter++, k );
+ Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
+ printf( "\n" );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
+{
+ int fUseSupp = 1;
+ FILE * pFile;
+ Vec_Int_t * vFlopCounts;
+ Vec_Ptr_t * vCubes;
+ Pdr_Set_t * pCube;
+ int i, kStart;
+ // create file
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file \"%s\" for writing invariant.\n", pFileName );
+ return;
+ }
+ // collect cubes
+ kStart = Pdr_ManFindInvariantStart( p );
+ vCubes = Pdr_ManCollectCubes( p, kStart );
+ Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+ // collect variable appearances
+ vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
+ // output the header
+ fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
+ fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
+ fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
+ fprintf( pFile, ".o 1\n" );
+ fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
+ // output cubes
+ Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+ {
+ Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
+ fprintf( pFile, " 1\n" );
+ }
+ fprintf( pFile, ".e\n\n" );
+ fclose( pFile );
+ Vec_IntFreeP( &vFlopCounts );
+ Vec_PtrFree( vCubes );
+ printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManReportInvariant( Pdr_Man_t * p )
+{
+ Vec_Ptr_t * vCubes;
+ int kStart = Pdr_ManFindInvariantStart( p );
+ vCubes = Pdr_ManCollectCubes( p, kStart );
+ printf( "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
+ kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
+ Vec_PtrFree( vCubes );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vLits;
+ Vec_Ptr_t * vCubes;
+ Pdr_Set_t * pCube;
+ int i, kStart, kThis, RetValue, Counter = 0, clk = clock();
+ // collect cubes used in the inductive invariant
+ kStart = Pdr_ManFindInvariantStart( p );
+ vCubes = Pdr_ManCollectCubes( p, kStart );
+ // create solver with the cubes
+ kThis = Vec_PtrSize(p->vSolvers);
+ pSat = Pdr_ManCreateSolver( p, kThis );
+ // add the property output
+ Pdr_ManSetPropertyOutput( p, kThis );
+ // add the clauses
+ Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+ {
+ vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ assert( RetValue );
+ sat_solver_compress( pSat );
+ }
+ // check each clause
+ Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+ {
+ 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 )
+ {
+ printf( "Verification of clause %d failed.\n", i );
+ Counter++;
+ }
+ }
+ if ( Counter )
+ printf( "Verification of %d clauses has failed.\n", Counter );
+ else
+ {
+ printf( "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ }
+// sat_solver_delete( pSat );
+ Vec_PtrFree( vCubes );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
new file mode 100644
index 00000000..f33f6586
--- /dev/null
+++ b/src/sat/pdr/pdrMan.c
@@ -0,0 +1,190 @@
+/**CFile****************************************************************
+
+ FileName [pdr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Manager procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
+{
+ Pdr_Man_t * p;
+ p = ABC_CALLOC( Pdr_Man_t, 1 );
+ p->pPars = pPars;
+ p->pAig = pAig;
+ p->vSolvers = Vec_PtrAlloc( 0 );
+ p->vClauses = Vec_VecAlloc( 0 );
+ p->pQueue = NULL;
+ p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
+ p->vActVars = Vec_IntAlloc( 256 );
+ // internal use
+ p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops
+ p->vLits = Vec_IntAlloc( 100 ); // array of literals
+ p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves
+ p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots
+ p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values
+ p->vCoVals = Vec_IntAlloc( 100 ); // cone root values
+ p->vNodes = Vec_IntAlloc( 100 ); // cone nodes
+ p->vUndo = Vec_IntAlloc( 100 ); // cone undos
+ p->vVisits = Vec_IntAlloc( 100 ); // intermediate
+ p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed
+ p->vRes = Vec_IntAlloc( 100 ); // final result
+ // additional AIG data-members
+ if ( pAig->pFanData == NULL )
+ Aig_ManFanoutStart( pAig );
+ if ( pAig->pTerSimData == NULL )
+ pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
+ p->timeStart = clock();
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManStop( Pdr_Man_t * p )
+{
+ Pdr_Set_t * pCla;
+ sat_solver * pSat;
+ int i, k;
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
+ p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
+ ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
+ ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
+ ABC_PRTP( " sat ", p->tSatSat, p->tTotal );
+ ABC_PRTP( "Generalize ", p->tGeneral, p->tTotal );
+ ABC_PRTP( "Push clause", p->tPush, p->tTotal );
+ ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal );
+ ABC_PRTP( "Containment", p->tContain, p->tTotal );
+ ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
+ ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
+ }
+
+ Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
+ sat_solver_delete( pSat );
+ Vec_PtrFree( p->vSolvers );
+ Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
+ Pdr_SetDeref( pCla );
+ Vec_VecFree( p->vClauses );
+ Pdr_QueueStop( p );
+ ABC_FREE( p->pOrder );
+ Vec_IntFree( p->vActVars );
+ // static CNF
+ Cnf_DataFree( p->pCnf1 );
+ Vec_IntFreeP( &p->vVar2Reg );
+ // dynamic CNF
+ Cnf_DataFree( p->pCnf2 );
+ if ( p->pvId2Vars )
+ for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
+ Vec_IntFreeP( &p->pvId2Vars[i] );
+ ABC_FREE( p->pvId2Vars );
+ Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
+ // internal use
+ Vec_IntFreeP( &p->vPrio ); // priority flops
+ Vec_IntFree( p->vLits ); // array of literals
+ Vec_IntFree( p->vCiObjs ); // cone leaves
+ Vec_IntFree( p->vCoObjs ); // cone roots
+ Vec_IntFree( p->vCiVals ); // cone leaf values
+ Vec_IntFree( p->vCoVals ); // cone root values
+ Vec_IntFree( p->vNodes ); // cone nodes
+ Vec_IntFree( p->vUndo ); // cone undos
+ Vec_IntFree( p->vVisits ); // intermediate
+ Vec_IntFree( p->vCi2Rem ); // CIs to be removed
+ Vec_IntFree( p->vRes ); // final result
+ // additional AIG data-members
+ if ( p->pAig->pFanData != NULL )
+ Aig_ManFanoutStop( p->pAig );
+ if ( p->pAig->pTerSimData != NULL )
+ ABC_FREE( p->pAig->pTerSimData );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
+{
+ extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+ Abc_Cex_t * pCex;
+ Pdr_Obl_t * pObl;
+ int i, f, Lit, nFrames = 0;
+ // count the number of frames
+ for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
+ nFrames++;
+ // create the counter-example
+ pCex = Gia_ManAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
+ pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
+ pCex->iFrame = nFrames-1;
+ for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
+ for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
+ {
+ Lit = pObl->pState->Lits[i];
+ if ( lit_sign(Lit) )
+ continue;
+ assert( lit_var(Lit) < pCex->nPis );
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+ }
+ assert( f == nFrames );
+ return pCex;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
new file mode 100644
index 00000000..45ada5c0
--- /dev/null
+++ b/src/sat/pdr/pdrSat.c
@@ -0,0 +1,351 @@
+/**CFile****************************************************************
+
+ FileName [pdrSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [SAT solver procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates new SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
+{
+ sat_solver * pSat;
+ assert( Vec_PtrSize(p->vSolvers) == k );
+ assert( Vec_VecSize(p->vClauses) == k );
+ assert( Vec_IntSize(p->vActVars) == k );
+ // create new solver
+ pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
+ Vec_PtrPush( p->vSolvers, pSat );
+ Vec_VecExpand( p->vClauses, k );
+ Vec_IntPush( p->vActVars, 0 );
+ // add property cone
+ Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns old or restarted solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
+{
+ sat_solver * pSat;
+ Vec_Ptr_t * vArrayK;
+ Pdr_Set_t * pCube;
+ int i, j;
+ pSat = Pdr_ManSolver(p, k);
+ if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
+ return pSat;
+ assert( k < Vec_PtrSize(p->vSolvers) - 1 );
+ p->nStarts++;
+ sat_solver_delete( pSat );
+ // create new SAT solver
+ pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
+ // write new SAT solver
+ Vec_PtrWriteEntry( p->vSolvers, k, pSat );
+ Vec_IntWriteEntry( p->vActVars, k, 0 );
+ // set the property output
+ Pdr_ManSetPropertyOutput( p, k );
+ // add the clauses
+ Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
+ Pdr_ManSolverAddClause( p, k, pCube );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts SAT variables into register IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
+{
+ int i, RegId;
+ Vec_IntClear( p->vLits );
+ for ( i = 0; i < nArray; i++ )
+ {
+ RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
+ if ( RegId == -1 )
+ continue;
+ assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
+ Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
+ }
+ assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
+ return p->vLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
+{
+ Aig_Obj_t * pObj;
+ int i, iVar, iVarMax = 0;
+ int clk = clock();
+ Vec_IntClear( p->vLits );
+ for ( i = 0; i < pCube->nLits; i++ )
+ {
+ if ( pCube->Lits[i] == -1 )
+ continue;
+ if ( fNext )
+ pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
+ else
+ pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
+ iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
+ iVarMax = ABC_MAX( iVarMax, iVar );
+ Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
+ }
+// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
+ p->tCnf += clock() - clk;
+ return p->vLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the property output to 0 (sat) forever.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
+{
+ sat_solver * pSat;
+ int Lit, RetValue;
+ pSat = Pdr_ManSolver(p, k);
+ Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
+ RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+ assert( RetValue == 1 );
+ sat_solver_compress( pSat );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vLits;
+ int RetValue;
+ pSat = Pdr_ManSolver(p, k);
+ vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ assert( RetValue == 1 );
+ sat_solver_compress( pSat );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
+{
+ sat_solver * pSat;
+ Aig_Obj_t * pObj;
+ int iVar, i;
+ Vec_IntClear( vValues );
+ pSat = Pdr_ManSolver(p, k);
+ Aig_ManForEachNodeVec( p->pAig, vObjIds, pObj, i )
+ {
+ iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
+ Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
+
+ Description [Return 1/0 if cube or property are proved to hold/fail
+ in k-th timeframe. Returns the predecessor bad state in ppPred.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vLits;
+ int RetValue;
+ pSat = Pdr_ManFetchSolver( p, k );
+ vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
+ RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+ assert( RetValue != l_Undef );
+ return (RetValue == l_False);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
+
+ Description [Return 1/0 if cube or property are proved to hold/fail
+ in k-th timeframe. Returns the predecessor bad state in ppPred.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
+{
+ int fUseLit = 1;
+ int fLitUsed = 0;
+ sat_solver * pSat;
+ Vec_Int_t * vLits;
+ int Lit, RetValue, clk;
+ p->nCalls++;
+ pSat = Pdr_ManFetchSolver( p, k );
+ if ( pCube == NULL ) // solve the property
+ {
+ clk = clock();
+ Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
+ RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
+ if ( RetValue == l_Undef )
+ return -1;
+ }
+ else // check relative containment in terms of next states
+ {
+ if ( fUseLit )
+ {
+ fLitUsed = 1;
+ Vec_IntAddToEntry( p->vActVars, k, 1 );
+ // add the cube in terms of current state variables
+ vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
+ // add activation literal
+ Lit = toLit( Pdr_ManFreeVar(p, k) );
+ // add activation literal
+ Vec_IntPush( vLits, Lit );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ assert( RetValue == 1 );
+ sat_solver_compress( pSat );
+ // create assumptions
+ vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
+ // add activation literal
+ Vec_IntPush( vLits, lit_neg(Lit) );
+ }
+ else
+ vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
+
+ // solve
+ clk = clock();
+ RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
+ if ( RetValue == l_Undef )
+ return -1;
+ }
+ clk = clock() - clk;
+ p->tSat += clk;
+ assert( RetValue != l_Undef );
+ if ( RetValue == l_False )
+ {
+ p->tSatUnsat += clk;
+ p->nCallsU++;
+ if ( ppPred )
+ *ppPred = NULL;
+ RetValue = 1;
+ }
+ else // if ( RetValue == l_True )
+ {
+ p->tSatSat += clk;
+ p->nCallsS++;
+ if ( ppPred )
+ *ppPred = Pdr_ManTernarySim( p, k, pCube );
+ RetValue = 0;
+ }
+
+/* // for some reason, it does not work...
+ if ( fLitUsed )
+ {
+ int RetValue;
+ Lit = lit_neg(Lit);
+ RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+ assert( RetValue == 1 );
+ sat_solver_compress( pSat );
+ }
+*/
+ return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c
new file mode 100644
index 00000000..01b54e3f
--- /dev/null
+++ b/src/sat/pdr/pdrTsim.c
@@ -0,0 +1,450 @@
+/**CFile****************************************************************
+
+ FileName [pdrTsim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Ternary simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define PDR_ZER 1
+#define PDR_ONE 2
+#define PDR_UND 3
+
+static inline int Pdr_ManSimInfoNot( int Value )
+{
+ if ( Value == PDR_ZER )
+ return PDR_ONE;
+ if ( Value == PDR_ONE )
+ return PDR_ZER;
+ return PDR_UND;
+}
+
+static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
+{
+ if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
+ return PDR_ZER;
+ if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
+ return PDR_ONE;
+ return PDR_UND;
+}
+
+static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
+}
+
+static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
+{
+ assert( Value >= PDR_ZER && Value <= PDR_UND );
+ Value ^= Pdr_ManSimInfoGet( p, pObj );
+ p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cone and collects CIs and nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+ assert( !Aig_IsComplement(pObj) );
+ if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(pAig, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
+ return;
+ }
+ Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
+ if ( Aig_ObjIsPo(pObj) )
+ return;
+ Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
+ Vec_IntPush( vNodes, Aig_ObjId(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cone and collects CIs and nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_IntClear( vCiObjs );
+ Vec_IntClear( vNodes );
+ Aig_ManIncrementTravId( pAig );
+ Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+ Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
+{
+ int Value0, Value1, Value;
+ Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
+ if ( Aig_ObjFaninC0(pObj) )
+ Value0 = Pdr_ManSimInfoNot( Value0 );
+ if ( Aig_ObjIsPo(pObj) )
+ {
+ Pdr_ManSimInfoSet( pAig, pObj, Value0 );
+ return Value0;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
+ if ( Aig_ObjFaninC1(pObj) )
+ Value1 = Pdr_ManSimInfoNot( Value1 );
+ Value = Pdr_ManSimInfoAnd( Value0, Value1 );
+ Pdr_ManSimInfoSet( pAig, pObj, Value );
+ return Value;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one design.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManSimDataInit( Aig_Man_t * pAig,
+ Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
+ Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ // set the CI values
+ Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
+ Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
+ // set the FOs to remove
+ if ( vCi2Rem != NULL )
+ Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
+ // perform ternary simulation
+ Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+ Pdr_ManExtendOneEval( pAig, pObj );
+ // transfer results to the output
+ Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ Pdr_ManExtendOneEval( pAig, pObj );
+ // check the results
+ Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tries to assign ternary value to one of the CIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
+{
+ Aig_Obj_t * pFanout;
+ int i, k, iFanout, Value, Value2;
+ assert( Saig_ObjIsLo(pAig, pObj) );
+ assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
+ // save original value
+ Value = Pdr_ManSimInfoGet( pAig, pObj );
+ assert( Value == PDR_ZER || Value == PDR_ONE );
+ Vec_IntPush( vUndo, Aig_ObjId(pObj) );
+ Vec_IntPush( vUndo, Value );
+ // update original value
+ Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
+ // traverse
+ Vec_IntClear( vVis );
+ Vec_IntPush( vVis, Aig_ObjId(pObj) );
+ Aig_ManForEachNodeVec( pAig, vVis, pObj, i )
+ {
+ Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
+ {
+ if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
+ continue;
+ assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
+ Value = Pdr_ManSimInfoGet( pAig, pFanout );
+ if ( Value == PDR_UND )
+ continue;
+ Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
+ if ( Value2 == Value )
+ continue;
+ assert( Value2 == PDR_UND );
+ Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
+ Vec_IntPush( vUndo, Value );
+ if ( Aig_ObjIsPo(pFanout) )
+ return 0;
+ assert( Aig_ObjIsNode(pFanout) );
+ Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
+ }
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Undoes the partial results of ternary simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
+{
+ Aig_Obj_t * pObj;
+ int i, Value;
+ Aig_ManForEachNodeVec( pAig, vUndo, pObj, i )
+ {
+ Value = Vec_IntEntry(vUndo, ++i);
+ assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
+ Pdr_ManSimInfoSet( pAig, pObj, Value );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the resulting cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
+{
+ Aig_Obj_t * pObj;
+ int i, Lit;
+ // mark removed flop outputs
+ Aig_ManIncrementTravId( pAig );
+ Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ {
+ assert( Saig_ObjIsLo( pAig, pObj ) );
+ Aig_ObjSetTravIdCurrent(pAig, pObj);
+ }
+ // collect flop outputs that are not marked
+ Vec_IntClear( vRes );
+ Vec_IntClear( vPiLits );
+ Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ {
+ if ( Saig_ObjIsPi(pAig, pObj) )
+ {
+ Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
+ Vec_IntPush( vPiLits, Lit );
+ continue;
+ }
+ assert( Saig_ObjIsLo(pAig, pObj) );
+ if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ continue;
+ Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
+ Vec_IntPush( vRes, Lit );
+ }
+ if ( Vec_IntSize(vRes) == 0 )
+ Vec_IntPush(vRes, 0);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the resulting cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
+ for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
+ pBuff[i] = '-';
+ pBuff[i] = 0;
+ Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
+ if ( vCi2Rem )
+ Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ pBuff[Aig_ObjPioNum(pObj)] = 'x';
+ printf( "%s\n", pBuff );
+ ABC_FREE( pBuff );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Shrinks values using ternary simulation.]
+
+ Description [The cube contains the set of flop index literals which,
+ when converted into a clause and applied to the combinational outputs,
+ led to a satisfiable SAT run in frame k (values stored in the SAT solver).
+ If the cube is NULL, it is assumed that the first property output was
+ asserted and failed.
+ The resulting array is a set of flop index literals that asserts the COs.
+ Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+ Vec_Int_t * vPrio = p->vPrio; // priority flops (flop indices)
+ Vec_Int_t * vPiLits = p->vLits; // array of literals (0/1 PI values)
+ Vec_Int_t * vCiObjs = p->vCiObjs; // cone leaves (CI obj IDs)
+ Vec_Int_t * vCoObjs = p->vCoObjs; // cone roots (CO obj IDs)
+ Vec_Int_t * vCiVals = p->vCiVals; // cone leaf values (0/1 CI values)
+ Vec_Int_t * vCoVals = p->vCoVals; // cone root values (0/1 CO values)
+ Vec_Int_t * vNodes = p->vNodes; // cone nodes (node obj IDs)
+ Vec_Int_t * vUndo = p->vUndo; // cone undos (node obj IDs)
+ Vec_Int_t * vVisits = p->vVisits; // intermediate (obj IDs)
+ Vec_Int_t * vCi2Rem = p->vCi2Rem; // CIs to be removed (CI obj IDs)
+ Vec_Int_t * vRes = p->vRes; // final result (flop literals)
+ Aig_Obj_t * pObj;
+ int i, Entry, RetValue;
+ int clk = clock();
+
+ // collect CO objects
+ Vec_IntClear( vCoObjs );
+ if ( pCube == NULL ) // the target is the property output
+ Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
+ else // the target is the cube
+ {
+ for ( i = 0; i < pCube->nLits; i++ )
+ {
+ if ( pCube->Lits[i] == -1 )
+ continue;
+ pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
+ Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
+ }
+ }
+if ( p->pPars->fVeryVerbose )
+{
+printf( "Trying to justify cube " );
+if ( pCube )
+ Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
+else
+ printf( "<prop=fail>" );
+printf( " in frame %d.\n", k );
+}
+
+ // collect CI objects
+ Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
+ // collect values
+ Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
+ Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
+ // simulate for the first time
+if ( p->pPars->fVeryVerbose )
+Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
+ RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
+ assert( RetValue );
+
+ // try removing high-priority flops
+ Vec_IntClear( vCi2Rem );
+ Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
+ if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
+ // try removing low-priority flops
+ Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
+ if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
+if ( p->pPars->fVeryVerbose )
+Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
+ RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
+ assert( RetValue );
+
+ // derive the set of resulting registers
+ Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
+ assert( Vec_IntSize(vRes) > 0 );
+ p->tTsim += clock() - clk;
+ return Pdr_SetCreate( vRes, vPiLits );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c
new file mode 100644
index 00000000..7e83102b
--- /dev/null
+++ b/src/sat/pdr/pdrUtil.c
@@ -0,0 +1,547 @@
+/**CFile****************************************************************
+
+ FileName [pdrUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Various utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntSelectSort( int * pArray, int nSize )
+{
+ int temp, i, j, best_i;
+ for ( i = 0; i < nSize-1; i++ )
+ {
+ best_i = i;
+ for ( j = i+1; j < nSize; j++ )
+ if ( pArray[j] < pArray[best_i] )
+ best_i = j;
+ temp = pArray[i];
+ pArray[i] = pArray[best_i];
+ pArray[best_i] = temp;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
+{
+ Pdr_Set_t * p;
+ int i;
+ assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<15) );
+ p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
+ p->nLits = Vec_IntSize(vLits);
+ p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
+ p->nRefs = 1;
+ p->Sign = 0;
+ for ( i = 0; i < p->nLits; i++ )
+ {
+ p->Lits[i] = Vec_IntEntry(vLits, i);
+ p->Sign |= ((word)1 << (p->Lits[i] % 63));
+ }
+ Vec_IntSelectSort( p->Lits, p->nLits );
+/*
+ for ( i = 0; i < p->nLits; i++ )
+ printf( "%d ", p->Lits[i] );
+ printf( "\n" );
+*/
+ // remember PI literals
+ for ( i = p->nLits; i < p->nTotal; i++ )
+ p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
+{
+ Pdr_Set_t * p;
+ int i, k = 0;
+ assert( iRemove >= 0 && iRemove < pSet->nLits );
+ p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
+ p->nLits = pSet->nLits - 1;
+ p->nTotal = pSet->nTotal - 1;
+ p->nRefs = 1;
+ p->Sign = 0;
+ for ( i = 0; i < pSet->nTotal; i++ )
+ {
+ if ( i == iRemove )
+ continue;
+ p->Lits[k++] = pSet->Lits[i];
+ if ( i >= pSet->nLits )
+ continue;
+ p->Sign |= ((word)1 << (pSet->Lits[i] % 63));
+ }
+ assert( k == p->nTotal );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
+{
+ Pdr_Set_t * p;
+ int i, k = 0;
+ assert( nLits >= 0 && nLits <= pSet->nLits );
+ p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
+ p->nLits = nLits;
+ p->nTotal = nLits + pSet->nTotal - pSet->nLits;
+ p->nRefs = 1;
+ p->Sign = 0;
+ for ( i = 0; i < nLits; i++ )
+ {
+ assert( pLits[i] >= 0 );
+ p->Lits[k++] = pLits[i];
+ p->Sign |= ((word)1 << (pLits[i] % 63));
+ }
+ Vec_IntSelectSort( p->Lits, p->nLits );
+ for ( i = pSet->nLits; i < pSet->nTotal; i++ )
+ p->Lits[k++] = pSet->Lits[i];
+ assert( k == p->nTotal );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
+{
+ Pdr_Set_t * p;
+ int i;
+ p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
+ p->nLits = pSet->nLits;
+ p->nTotal = pSet->nTotal;
+ p->nRefs = 1;
+ p->Sign = pSet->Sign;
+ for ( i = 0; i < pSet->nTotal; i++ )
+ p->Lits[i] = pSet->Lits[i];
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p )
+{
+ p->nRefs++;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_SetDeref( Pdr_Set_t * p )
+{
+ if ( --p->nRefs == 0 )
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
+{
+ char * pBuff;
+ int i, k, Entry;
+ pBuff = ABC_ALLOC( char, nRegs + 1 );
+ for ( i = 0; i < nRegs; i++ )
+ pBuff[i] = '-';
+ pBuff[i] = 0;
+ for ( i = 0; i < p->nLits; i++ )
+ {
+ if ( p->Lits[i] == -1 )
+ continue;
+ pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+ }
+ if ( vFlopCounts )
+ {
+ // skip some literals
+ k = 0;
+ Vec_IntForEachEntry( vFlopCounts, Entry, i )
+ if ( Entry )
+ pBuff[k++] = pBuff[i];
+ pBuff[k] = 0;
+ }
+ fprintf( pFile, "%s", pBuff );
+ ABC_FREE( pBuff );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Return 1 if pOld set-theoretically contains pNew.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
+{
+ int * pOldInt, * pNewInt;
+ assert( pOld->nLits > 0 );
+ assert( pNew->nLits > 0 );
+ if ( pOld->nLits < pNew->nLits )
+ return 0;
+ if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
+ return 0;
+ pOldInt = pOld->Lits + pOld->nLits - 1;
+ pNewInt = pNew->Lits + pNew->nLits - 1;
+ while ( pNew->Lits <= pNewInt )
+ {
+ if ( pOld->Lits > pOldInt )
+ return 0;
+ assert( *pNewInt != -1 );
+ assert( *pOldInt != -1 );
+ if ( *pNewInt == *pOldInt )
+ pNewInt--, pOldInt--;
+ else if ( *pNewInt < *pOldInt )
+ pOldInt--;
+ else
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Return 1 if the state cube contains init state (000...0).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
+{
+ int i;
+ for ( i = 0; i < pCube->nLits; i++ )
+ {
+ assert( pCube->Lits[i] != -1 );
+ if ( i == iRemove )
+ continue;
+ if ( lit_sign( pCube->Lits[i] ) == 0 )
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
+{
+ Pdr_Set_t * p1 = *pp1;
+ Pdr_Set_t * p2 = *pp2;
+ 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;
+ }
+ if ( i == p1->nLits && i < p2->nLits )
+ return -1;
+ if ( i < p1->nLits && i == p2->nLits )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
+{
+ Pdr_Obl_t * p;
+ p = ABC_ALLOC( Pdr_Obl_t, 1 );
+ p->iFrame = k;
+ p->prio = prio;
+ p->nRefs = 1;
+ p->pState = pState;
+ p->pNext = pNext;
+ p->pLink = NULL;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
+{
+ p->nRefs++;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_OblDeref( Pdr_Obl_t * p )
+{
+ if ( --p->nRefs == 0 )
+ {
+ if ( p->pNext )
+ Pdr_OblDeref( p->pNext );
+ Pdr_SetDeref( p->pState );
+ ABC_FREE( p );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pdr_QueueIsEmpty( Pdr_Man_t * p )
+{
+ return p->pQueue == NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
+{
+ return p->pQueue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
+{
+ Pdr_Obl_t * pRes = p->pQueue;
+ if ( p->pQueue == NULL )
+ return NULL;
+ p->pQueue = p->pQueue->pLink;
+ Pdr_OblDeref( pRes );
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
+{
+ Pdr_Obl_t * pTemp, ** ppPrev;
+ p->nObligs++;
+ Pdr_OblRef( pObl );
+ if ( p->pQueue == NULL )
+ {
+ p->pQueue = pObl;
+ return;
+ }
+ for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
+ if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
+ break;
+ *ppPrev = pObl;
+ pObl->pLink = pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_QueuePrint( Pdr_Man_t * p )
+{
+ Pdr_Obl_t * pObl;
+ for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
+ printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pdr_QueueStop( Pdr_Man_t * p )
+{
+ Pdr_Obl_t * pObl;
+ while ( !Pdr_QueueIsEmpty(p) )
+ {
+ pObl = Pdr_QueuePop(p);
+ Pdr_OblDeref( pObl );
+ }
+ p->pQueue = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+