Skip to content

A
abc
Commit e3e2918e by Alan Mishchenko
Options

Version abc90405

parent 23fd1103
Showing with 1389 additions and 397 deletions
abclib.dsp
...@@ -3695,6 +3695,10 @@ SOURCE=.\src\aig\gia\giaCSat.c ...@@ -3695,6 +3695,10 @@ SOURCE=.\src\aig\gia\giaCSat.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\gia\giaCSatOld.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaDfs.c SOURCE=.\src\aig\gia\giaDfs.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/cec/cec.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [] Synopsis []
......
src/aig/cec/cec.h
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [External declarations.] Synopsis [External declarations.]
...@@ -44,6 +44,7 @@ struct Cec_ParSat_t_ ...@@ -44,6 +44,7 @@ struct Cec_ParSat_t_
int nBTLimit; // conflict limit at a node int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver int nCallsRecycle; // calls to perform before recycling SAT solver
int fNonChrono; // use non-chronological backtracling (for circuit SAT only)
int fPolarFlip; // flops polarity of variables int fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output int fFirstStop; // stop on the first sat output
......
src/aig/cec/cecCec.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Integrated combinatinal equivalence checker.] Synopsis [Integrated combinatinal equivalence checker.]
......
src/aig/cec/cecChoice.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Computation of structural choices.] Synopsis [Computation of structural choices.]
......
src/aig/cec/cecClass.c
...@@ -4,9 +4,9 @@ ...@@ -4,9 +4,9 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Equivalence class representation.] Synopsis [Equivalence class refinement.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
...@@ -838,6 +838,8 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) ...@@ -838,6 +838,8 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
// allocate representation // allocate representation
p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) ); p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
// create references
Gia_ManSetRefs( p->pAig );
// set starting representative of internal nodes to be constant 0 // set starting representative of internal nodes to be constant 0
if ( p->pPars->fLatchCorr ) if ( p->pPars->fLatchCorr )
Gia_ManForEachObj( p->pAig, pObj, i ) Gia_ManForEachObj( p->pAig, pObj, i )
...@@ -848,9 +850,9 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) ...@@ -848,9 +850,9 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
// if sequential simulation, set starting representative of ROs to be constant 0 // if sequential simulation, set starting representative of ROs to be constant 0
if ( p->pPars->fSeqSimulate ) if ( p->pPars->fSeqSimulate )
Gia_ManForEachRo( p->pAig, pObj, i ) Gia_ManForEachRo( p->pAig, pObj, i )
if ( pObj->Value )
Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 ); Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
// perform simulation // perform simulation
Gia_ManSetRefs( p->pAig );
p->nWords = 1; p->nWords = 1;
do { do {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
......
src/aig/cec/cecCore.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Core procedures.] Synopsis [Core procedures.]
...@@ -42,9 +42,10 @@ ...@@ -42,9 +42,10 @@
void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
{ {
memset( p, 0, sizeof(Cec_ParSat_t) ); memset( p, 0, sizeof(Cec_ParSat_t) );
p->nBTLimit = 10; // conflict limit at a node p->nBTLimit = 100; // conflict limit at a node
p->nSatVarMax = 2000; // the max number of SAT variables p->nSatVarMax = 2000; // the max number of SAT variables
p->nCallsRecycle = 200; // calls to perform before recycling SAT solver p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
p->fNonChrono = 0; // use non-chronological backtracling (for circuit SAT only)
p->fPolarFlip = 1; // flops polarity of variables p->fPolarFlip = 1; // flops polarity of variables
p->fCheckMiter = 0; // the circuit is the miter p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output p->fFirstStop = 0; // stop on the first sat output
...@@ -399,7 +400,7 @@ p->timeSat += clock() - clk; ...@@ -399,7 +400,7 @@ p->timeSat += clock() - clk;
// if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved ) // if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
if ( p->nAllFailed > p->nAllProved + p->nAllDisproved ) if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
{ {
if ( pParsSat->nBTLimit >= 10000 ) if ( pParsSat->nBTLimit >= 10001 )
break; break;
pParsSat->nBTLimit *= 10; pParsSat->nBTLimit *= 10;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
...@@ -413,7 +414,7 @@ p->timeSat += clock() - clk; ...@@ -413,7 +414,7 @@ p->timeSat += clock() - clk;
} }
} }
} }
if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
printf( "Switching into reduced mode.\n" ); printf( "Switching into reduced mode.\n" );
......
src/aig/cec/cecCorr.c
/**CFile**************************************************************** /**CFile****************************************************************
FileName [cecLcorr.c] FileName [cecCorr.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Flop correspondence computation.] Synopsis [Latch/signal correspondence computation.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.] Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecLcorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
...@@ -74,14 +74,11 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb ...@@ -74,14 +74,11 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
return; return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{ {
if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
{
Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f ); Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Gia_ObjSetCopyF( p, f, pObj, iLitNew ); Gia_ObjSetCopyF( p, f, pObj, iLitNew );
return; return;
} }
}
assert( Gia_ObjIsCand(pObj) ); assert( Gia_ObjIsCand(pObj) );
iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
Gia_ObjSetCopyF( p, f, pObj, iLitNew ); Gia_ObjSetCopyF( p, f, pObj, iLitNew );
...@@ -117,10 +114,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -117,10 +114,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) ); Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) ); Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
}
for ( f = 0; f < nFrames+fScorr; f++ ) for ( f = 0; f < nFrames+fScorr; f++ )
{ {
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
...@@ -135,8 +129,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -135,8 +129,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
{ {
if ( Gia_ObjIsConst( p, i ) ) if ( Gia_ObjIsConst( p, i ) )
{ {
if ( Gia_ObjIsFailedPair(p, 0, i) )
continue;
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 ) if ( iObjNew != 0 )
...@@ -151,11 +143,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -151,11 +143,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
iPrev = i; iPrev = i;
Gia_ClassForEachObj1( p, i, iObj ) Gia_ClassForEachObj1( p, i, iObj )
{ {
if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
{
iPrev = iObj;
continue;
}
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
...@@ -169,8 +156,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -169,8 +156,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
iPrev = iObj; iPrev = iObj;
} }
iObj = i; iObj = i;
if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
continue;
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
...@@ -191,8 +176,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -191,8 +176,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
continue; continue;
if ( Gia_ObjIsFailedPair(p, Gia_ObjRepr(p, i), i) )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames ); iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
...@@ -216,6 +199,38 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I ...@@ -216,6 +199,38 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
return pNew; return pNew;
} }
/**Function*************************************************************
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
{
unsigned * pInfo;
int k, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom( 0 );
}
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.] Synopsis [Remaps simulation info from SRM to the original AIG.]
...@@ -257,7 +272,7 @@ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo ) ...@@ -257,7 +272,7 @@ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Remaps simulation info from SRM to the original AIG.] Synopsis [Collects information about remapping.]
Description [] Description []
...@@ -276,8 +291,8 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ) ...@@ -276,8 +291,8 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
{ {
// skip ROs without representatives // skip ROs without representatives
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) ) // if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
continue; continue;
assert( Gia_ObjIsRo(p, pRepr) ); assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); // printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
...@@ -319,51 +334,41 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo ) ...@@ -319,51 +334,41 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.] Synopsis [Packs one counter-examples into the array of simulation info.]
Description [Returns 1 if all ndoes are proved.] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ *************************************`**********************************/
int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings ) int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{ {
int i, status, iRepr, iObj; unsigned * pInfo, * pPres;
assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) ); int i;
Vec_StrForEachEntry( vStatus, status, i ) for ( i = 0; i < nLits; i++ )
{
iRepr = Vec_IntEntry( vOutputs, 2*i );
iObj = Vec_IntEntry( vOutputs, 2*i+1 );
if ( status == 1 )
continue;
if ( status == 0 )
{ {
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) if ( Aig_InfoHasBit( pPres, iBit ) &&
Cec_ManSimClassRemoveOne( pSim, iObj ); Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
continue; return 0;
} }
if ( status == -1 ) for ( i = 0; i < nLits; i++ )
{ {
// if ( !Gia_ObjFailed( p, iObj ) ) pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
// Gia_ObjSetFailed( p, iRepr ); Aig_InfoSetBit( pPres, iBit );
// Gia_ObjSetFailed( p, iObj ); if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
if ( fRings ) Aig_InfoXorBit( pInfo, iBit );
Cec_ManSimClassRemoveOne( pSim, iRepr );
Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
} }
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Marks all the nodes as proved.] Synopsis [Performs bitpacking of counter-examples.]
Description [] Description []
...@@ -372,97 +377,44 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu ...@@ -372,97 +377,44 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManSetProvedNodes( Gia_Man_t * p ) int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
{ {
Gia_Obj_t * pObj; Vec_Int_t * vPat;
int i, nLits = 0; Vec_Ptr_t * vPres;
Gia_ManForEachObj1( p, pObj, i ) int nWords = Vec_PtrReadWordsSimInfo(vInfo);
int nBits = 32 * nWords;
int k, nSize, iBit = 1, kMax = 0;
vPat = Vec_IntAlloc( 100 );
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{ {
if ( Gia_ObjRepr(p, i) == GIA_VOID ) // skip the output number
continue; iStart++;
if ( Gia_ObjIsFailedPair( p, Gia_ObjRepr(p, i), i ) ) // get the number of items
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
continue; continue;
Gia_ObjSetProved( p, i ); // extract pattern
nLits++; Vec_IntClear( vPat );
} for ( k = 0; k < nSize; k++ )
// printf( "Identified %d proved literals.\n", nLits ); Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
} // add pattern to storage
for ( k = 1; k < nBits; k++ )
/**Function************************************************************* if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
Synopsis [] kMax = AIG_MAX( kMax, k );
if ( k == nBits-1 )
Description [] break;
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
{
int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsNone(p, i) )
CounterX++;
else if ( Gia_ObjIsConst(p, i) )
Counter0++;
else if ( Gia_ObjIsHead(p, i) )
Counter++;
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
if ( Entry == 1 )
nProve++;
else if ( Entry == 0 )
nDispr++;
else if ( Entry == -1 )
nFail++;
}
printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
ABC_PRT( "T", Time );
}
/**Function*************************************************************
Synopsis [Sets register values from the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
{
unsigned * pInfo;
int k, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom( 0 );
} }
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return iStart;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Performs bitpacking of counter-examples.]
Description [] Description []
...@@ -503,7 +455,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i ...@@ -503,7 +455,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
/**Function************************************************************* /**Function*************************************************************
Synopsis [Packs patterns into array of simulation info.] Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description [] Description []
...@@ -511,33 +463,86 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i ...@@ -511,33 +463,86 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
SeeAlso [] SeeAlso []
*************************************`**********************************/ ***********************************************************************/
int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits ) int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
{ {
unsigned * pInfo, * pPres; Vec_Int_t * vPairs;
int i; Vec_Ptr_t * vSimInfo;
for ( i = 0; i < nLits; i++ ) int RetValue = 0, iStart = 0;
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
Gia_ManSetRefs( pSim->pAig );
// pSim->pPars->nWords = 63;
pSim->pPars->nRounds = nFrames;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{ {
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
if ( Aig_InfoHasBit( pPres, iBit ) && // iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) // Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
return 0; Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
} }
for ( i = 0; i < nLits; i++ ) //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
Vec_IntFree( vPairs );
return RetValue;
}
/**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.]
Description [Returns 1 if all ndoes are proved.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
{
int i, status, iRepr, iObj;
int Counter = 0;
assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
Vec_StrForEachEntry( vStatus, status, i )
{ {
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); iRepr = Vec_IntEntry( vOutputs, 2*i );
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); iObj = Vec_IntEntry( vOutputs, 2*i+1 );
Aig_InfoSetBit( pPres, iBit ); if ( status == 1 )
if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) continue;
Aig_InfoXorBit( pInfo, iBit ); if ( status == 0 )
{
if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
Counter++;
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
if ( status == -1 )
{
// if ( !Gia_ObjFailed( p, iObj ) )
// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
// Gia_ObjSetFailed( p, iRepr );
// Gia_ObjSetFailed( p, iObj );
// if ( fRings )
// Cec_ManSimClassRemoveOne( pSim, iRepr );
Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
}
} }
// if ( Counter )
// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Marks all the nodes as proved.]
Description [] Description []
...@@ -546,54 +551,23 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi ...@@ -546,54 +551,23 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) void Gia_ManSetProvedNodes( Gia_Man_t * p )
{ {
Vec_Int_t * vPat; Gia_Obj_t * pObj;
Vec_Ptr_t * vPres; int i, nLits = 0;
int nWords = Vec_PtrReadWordsSimInfo(vInfo); Gia_ManForEachObj1( p, pObj, i )
int nBits = 32 * nWords;
int k, nSize, iBit = 1, kMax = 0;
vPat = Vec_IntAlloc( 100 );
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{ {
// skip the output number if ( Gia_ObjRepr(p, i) == GIA_VOID )
iStart++;
// get the number of items
nSize = Vec_IntEntry( vCexStore, iStart++ );
if ( nSize <= 0 )
continue; continue;
// extract pattern Gia_ObjSetProved( p, i );
Vec_IntClear( vPat ); nLits++;
for ( k = 0; k < nSize; k++ )
{
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
// printf( "%d(%d) ", Vec_IntEntryLast(vPat)/2, (Vec_IntEntryLast(vPat)&1)==0 );
}
// printf( "\n" );
// add pattern to storage
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
// for ( i = 0; i < 27; i++ )
// printf( "%d(%d) ", i, Aig_InfoHasBit(Vec_PtrEntry(vInfo,i), k) );
// printf( "\n" );
kMax = AIG_MAX( kMax, k );
if ( k == nBits-1 )
break;
} }
// printf( "\n" ); // printf( "Identified %d proved literals.\n", nLits );
// printf( "kMax = %d.\n", kMax );
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return iStart;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Prints statistics during solving.]
Description [] Description []
...@@ -602,37 +576,39 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS ...@@ -602,37 +576,39 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames ) void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
{ {
Vec_Int_t * vPairs; int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
Vec_Ptr_t * vSimInfo; int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
int RetValue = 0, iStart = 0; for ( i = 1; i < Gia_ManObjNum(p); i++ )
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
Gia_ManSetRefs( pSim->pAig );
// pSim->pPars->nWords = 63;
pSim->pPars->nRounds = nFrames;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{ {
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); if ( Gia_ObjIsNone(p, i) )
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) ); CounterX++;
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); else if ( Gia_ObjIsConst(p, i) )
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); Counter0++;
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); else if ( Gia_ObjIsHead(p, i) )
Gia_ManCorrPerformRemapping( vPairs, vSimInfo ); Counter++;
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
} }
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); CounterX -= Gia_ManCoNum(p);
assert( iStart == Vec_IntSize(vCexStore) ); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
Vec_PtrFree( vSimInfo ); printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits );
Vec_IntFree( vPairs ); if ( vStatus )
return RetValue; Vec_StrForEachEntry( vStatus, Entry, i )
{
if ( Entry == 1 )
nProve++;
else if ( Entry == 0 )
nDispr++;
else if ( Entry == -1 )
nFail++;
}
printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
ABC_PRT( "T", Time );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Top-level procedure for register correspondence.]
Description [] Description []
...@@ -643,7 +619,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ...@@ -643,7 +619,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{ {
int nAddFrames = 2; // additional timeframes to simulate int nAddFrames = 1; // additional timeframes to simulate
Vec_Str_t * vStatus; Vec_Str_t * vStatus;
Vec_Int_t * vOutputs; Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore; Vec_Int_t * vCexStore;
...@@ -701,11 +677,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -701,11 +677,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
break; break;
} }
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
// found counter-examples to speculation // found counter-examples to speculation
clk2 = clock(); clk2 = clock();
if ( pPars->fUseCSat ) if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiter( pSrm, pPars->nBTLimit, &vStatus ); vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm ); Gia_ManStop( pSrm );
...@@ -725,28 +700,36 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -725,28 +700,36 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk ); Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
Vec_StrFree( vStatus ); Vec_StrFree( vStatus );
Vec_IntFree( vOutputs ); Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
} }
if ( r == 100000 )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim ); Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal; clkTotal = clock() - clkTotal;
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
// report the results
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
ABC_PRTP( "Srm ", clkSrm, clkTotal ); ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal ); ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal ); ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal ); ABC_PRT( "TOTAL", clkTotal );
} }
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew; return pNew;
} }
......
src/aig/cec/cecInt.h
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [External declarations.] Synopsis [External declarations.]
......
src/aig/cec/cecIso.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Detection of structural isomorphism.] Synopsis [Detection of structural isomorphism.]
......
src/aig/cec/cecMan.c
...@@ -4,9 +4,9 @@ ...@@ -4,9 +4,9 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Manager pcocures.] Synopsis [Manager procedures.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
......
src/aig/cec/cecPat.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Simulation pattern manager.] Synopsis [Simulation pattern manager.]
......
src/aig/cec/cecSeq.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Refinement of sequential equivalence classes.] Synopsis [Refinement of sequential equivalence classes.]
......
src/aig/cec/cecSim.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Simulation manager.] Synopsis [Simulation manager.]
......
src/aig/cec/cecSolve.c
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [Performs one round of SAT solving.] Synopsis [Performs one round of SAT solving.]
......
src/aig/cec/cecSweep.c
/**CFile**************************************************************** /**CFile****************************************************************
FileName [ceFraeep.c] FileName [cecSweep.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal equivalence checking.] PackageName [Combinational equivalence checking.]
Synopsis [SAT sweeping manager.] Synopsis [SAT sweeping manager.]
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.] Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ceFraeep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
......
src/aig/gia/gia.h
...@@ -459,8 +459,10 @@ extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ); ...@@ -459,8 +459,10 @@ extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ); extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
/*=== giaCsatOld.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/ /*=== giaCsat.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus ); extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCof.c =============================================================*/ /*=== giaCof.c =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
......
src/aig/gia/giaCSat.c
...@@ -32,6 +32,7 @@ struct Cbs_Par_t_ ...@@ -32,6 +32,7 @@ struct Cbs_Par_t_
int nJustLimit; // limit on the size of justification queue int nJustLimit; // limit on the size of justification queue
// current parameters // current parameters
int nBTThis; // number of conflicts int nBTThis; // number of conflicts
int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier int nJustTotal; // total size of the frontier
...@@ -59,7 +60,11 @@ struct Cbs_Man_t_ ...@@ -59,7 +60,11 @@ struct Cbs_Man_t_
Gia_Man_t * pAig; // AIG manager Gia_Man_t * pAig; // AIG manager
Cbs_Que_t pProp; // propagation queue Cbs_Que_t pProp; // propagation queue
Cbs_Que_t pJust; // justification queue Cbs_Que_t pJust; // justification queue
Cbs_Que_t pClauses; // clause queue
Gia_Obj_t ** pIter; // iterator through clause vars
Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vModel; // satisfying assignment Vec_Int_t * vModel; // satisfying assignment
Vec_Ptr_t * vTemp; // temporary storage
// SAT calls statistics // SAT calls statistics
int nSatUnsat; // the number of proofs int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure int nSatSat; // the number of failure
...@@ -78,16 +83,26 @@ struct Cbs_Man_t_ ...@@ -78,16 +83,26 @@ struct Cbs_Man_t_
static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; } static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; } static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; } static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; } static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); } static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); }
static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); } static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); } static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
static inline int Cbs_VarDecLevel( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
static inline Gia_Obj_t * Cbs_VarReason0( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
static inline Gia_Obj_t * Cbs_VarReason1( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
static inline int Cbs_ClauseDecLevel( Cbs_Man_t * p, int hClause ) { return Cbs_VarDecLevel( p, p->pClauses.pData[hClause] ); }
#define Cbs_QueForEachEntry( Que, pObj, i ) \ #define Cbs_QueForEachEntry( Que, pObj, i ) \
for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ ) for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
#define Cbs_ClauseForEachVar( p, hClause, pObj ) \
for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
#define Cbs_ClauseForEachVar1( p, hClause, pObj ) \
for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc() ...@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc()
{ {
Cbs_Man_t * p; Cbs_Man_t * p;
p = ABC_CALLOC( Cbs_Man_t, 1 ); p = ABC_CALLOC( Cbs_Man_t, 1 );
p->pProp.nSize = p->pJust.nSize = 10000; p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize ); p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize ); p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
p->pClauses.iHead = p->pClauses.iTail = 1;
p->vModel = Vec_IntAlloc( 1000 ); p->vModel = Vec_IntAlloc( 1000 );
p->vLevReas = Vec_IntAlloc( 1000 );
p->vTemp = Vec_PtrAlloc( 1000 );
Cbs_SetDefaultParams( &p->Pars ); Cbs_SetDefaultParams( &p->Pars );
return p; return p;
} }
...@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc() ...@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc()
***********************************************************************/ ***********************************************************************/
void Cbs_ManStop( Cbs_Man_t * p ) void Cbs_ManStop( Cbs_Man_t * p )
{ {
Vec_IntFree( p->vLevReas );
Vec_IntFree( p->vModel ); Vec_IntFree( p->vModel );
Vec_PtrFree( p->vTemp );
ABC_FREE( p->pClauses.pData );
ABC_FREE( p->pProp.pData ); ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData ); ABC_FREE( p->pJust.pData );
ABC_FREE( p ); ABC_FREE( p );
...@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld ) ...@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld )
p->iTail = iTailOld; p->iTail = iTailOld;
} }
/**Function*************************************************************
Synopsis [Finalized the clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs_QueFinish( Cbs_Que_t * p )
{
int iHeadOld = p->iHead;
assert( p->iHead < p->iTail );
Cbs_QuePush( p, NULL );
p->iHead = p->iTail;
return iHeadOld;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) ...@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Cbs_QueForEachEntry( p->pProp, pVar, i ) Cbs_QueForEachEntry( p->pProp, pVar, i )
Cbs_VarUnassign( pVar ); Cbs_VarUnassign( pVar );
p->pProp.iTail = iBound; p->pProp.iTail = iBound;
Vec_IntShrink( p->vLevReas, 3*iBound );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) ...@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj ) static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
{ {
Gia_Obj_t * pObjR = Gia_Regular(pObj); Gia_Obj_t * pObjR = Gia_Regular(pObj);
assert( Gia_ObjIsCand(pObjR) ); assert( Gia_ObjIsCand(pObjR) );
assert( !Cbs_VarIsAssigned(pObjR) ); assert( !Cbs_VarIsAssigned(pObjR) );
Cbs_VarAssign( pObjR ); Cbs_VarAssign( pObjR );
Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) ); Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
assert( pObjR->Value == ~0 );
pObjR->Value = p->pProp.iTail;
Cbs_QuePush( &p->pProp, pObjR ); Cbs_QuePush( &p->pProp, pObjR );
Vec_IntPush( p->vLevReas, Level );
Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
}
/**Function*************************************************************
Synopsis [Returns clause size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs_ManClauseSize( Cbs_Man_t * p, int hClause )
{
Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t ** pIter;
for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
return pIter - pQue->pData - hClause ;
}
/**Function*************************************************************
Synopsis [Prints conflict clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs_ManPrintClause( Cbs_Man_t * p, int Level, int hClause )
{
Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t * pObj;
int i;
assert( Cbs_QueIsEmpty( pQue ) );
printf( "Level %2d : ", Level );
for ( i = hClause; (pObj = pQue->pData[i]); i++ )
printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs_VarValue(pObj), Cbs_VarDecLevel(p, pObj) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Prints conflict clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs_ManPrintClauseNew( Cbs_Man_t * p, int Level, int hClause )
{
Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t * pObj;
int i;
assert( Cbs_QueIsEmpty( pQue ) );
printf( "Level %2d : ", Level );
for ( i = hClause; (pObj = pQue->pData[i]); i++ )
printf( "%c%d ", Cbs_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Returns conflict clause.]
Description [Performs conflict analysis.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
{
Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t * pObj, * pReason;
int i, k, iLitLevel;
assert( pQue->pData[pQue->iHead] == NULL );
assert( pQue->iHead + 1 < pQue->iTail );
/*
for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
{
pObj = pQue->pData[i];
assert( pObj->fMark0 == 1 );
}
*/
// compact literals
Vec_PtrClear( p->vTemp );
for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
{
pObj = pQue->pData[i];
if ( !pObj->fMark0 ) // unassigned - seen again
continue;
// assigned - seen first time
pObj->fMark0 = 0;
Vec_PtrPush( p->vTemp, pObj );
// check decision level
iLitLevel = Cbs_VarDecLevel( p, pObj );
if ( iLitLevel < Level )
{
pQue->pData[k++] = pObj;
continue;
}
assert( iLitLevel == Level );
pReason = Cbs_VarReason0( p, pObj );
if ( pReason == pObj ) // no reason
{
assert( pQue->pData[pQue->iHead] == NULL );
pQue->pData[pQue->iHead] = pObj;
continue;
}
Cbs_QuePush( pQue, pReason );
pReason = Cbs_VarReason1( p, pObj );
if ( pReason != pObj ) // second reason
Cbs_QuePush( pQue, pReason );
}
assert( pQue->pData[pQue->iHead] != NULL );
pQue->iTail = k;
// clear the marks
Vec_PtrForEachEntry( p->vTemp, pObj, i )
pObj->fMark0 = 1;
}
/**Function*************************************************************
Synopsis [Returns conflict clause.]
Description [Performs conflict analysis.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs_ManAnalyze( Cbs_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
{
Cbs_Que_t * pQue = &(p->pClauses);
assert( Cbs_VarIsAssigned(pVar) );
assert( Cbs_VarIsAssigned(pFan0) );
assert( pFan1 == NULL || Cbs_VarIsAssigned(pFan1) );
assert( Cbs_QueIsEmpty( pQue ) );
Cbs_QuePush( pQue, NULL );
Cbs_QuePush( pQue, pVar );
Cbs_QuePush( pQue, pFan0 );
if ( pFan1 )
Cbs_QuePush( pQue, pFan1 );
Cbs_ManDeriveReason( p, Level );
return Cbs_QueFinish( pQue );
}
/**Function*************************************************************
Synopsis [Performs resolution of two clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs_ManResolve( Cbs_Man_t * p, int Level, int hClause0, int hClause1 )
{
Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t * pObj;
int i, LevelMax = -1, LevelCur;
assert( pQue->pData[hClause0] != NULL );
assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
/*
for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
assert( pObj->fMark0 == 1 );
for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
assert( pObj->fMark0 == 1 );
*/
assert( Cbs_QueIsEmpty( pQue ) );
Cbs_QuePush( pQue, NULL );
for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
{
if ( !pObj->fMark0 ) // unassigned - seen again
continue;
// assigned - seen first time
pObj->fMark0 = 0;
Cbs_QuePush( pQue, pObj );
LevelCur = Cbs_VarDecLevel( p, pObj );
if ( LevelMax < LevelCur )
LevelMax = LevelCur;
}
for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
{
if ( !pObj->fMark0 ) // unassigned - seen again
continue;
// assigned - seen first time
pObj->fMark0 = 0;
Cbs_QuePush( pQue, pObj );
LevelCur = Cbs_VarDecLevel( p, pObj );
if ( LevelMax < LevelCur )
LevelMax = LevelCur;
}
for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
pQue->pData[i]->fMark0 = 1;
Cbs_ManDeriveReason( p, LevelMax );
return Cbs_QueFinish( pQue );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Propagates a variable.] Synopsis [Propagates a variable.]
Description [Returns 1 if conflict; 0 if no conflict.] Description [Returns clause handle if conflict; 0 if no conflict.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar ) static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{ {
int Value0, Value1; int Value0, Value1;
assert( !Gia_IsComplement(pVar) ); assert( !Gia_IsComplement(pVar) );
...@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar ) ...@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Cbs_VarValue(pVar) ) if ( Cbs_VarValue(pVar) )
{ // value is 1 { // value is 1
if ( Value0 == 0 || Value1 == 0 ) // one is 0 if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 1; {
if ( Value0 == 0 && Value1 != 0 )
return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
if ( Value0 != 0 && Value1 == 0 )
return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
assert( Value0 == 0 && Value1 == 0 );
return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
}
if ( Value0 == 2 ) // first is unassigned if ( Value0 == 2 ) // first is unassigned
Cbs_ManAssign( p, Gia_ObjChild0(pVar) ); Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
if ( Value1 == 2 ) // first is unassigned if ( Value1 == 2 ) // first is unassigned
Cbs_ManAssign( p, Gia_ObjChild1(pVar) ); Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
return 0; return 0;
} }
// value is 0 // value is 0
if ( Value0 == 0 || Value1 == 0 ) // one is 0 if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0; return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1 if ( Value0 == 1 && Value1 == 1 ) // both are 1
return 1; return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
if ( Value0 == 1 || Value1 == 1 ) // one is 1 if ( Value0 == 1 || Value1 == 1 ) // one is 1
{ {
if ( Value0 == 2 ) // first is unassigned if ( Value0 == 2 ) // first is unassigned
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
if ( Value1 == 2 ) // first is unassigned if ( Value1 == 2 ) // second is unassigned
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0; return 0;
} }
assert( Cbs_VarIsJust(pVar) ); assert( Cbs_VarIsJust(pVar) );
...@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar ) ...@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar ) static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{ {
int Value0, Value1; int Value0, Value1;
assert( !Gia_IsComplement(pVar) ); assert( !Gia_IsComplement(pVar) );
...@@ -522,12 +788,12 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar ) ...@@ -522,12 +788,12 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Value0 == 0 || Value1 == 0 ) // one is 0 if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0; return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1 if ( Value0 == 1 && Value1 == 1 ) // both are 1
return 1; return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
assert( Value0 == 1 || Value1 == 1 ); assert( Value0 == 1 || Value1 == 1 );
if ( Value0 == 2 ) // first is unassigned if ( Value0 == 2 ) // first is unassigned
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
if ( Value1 == 2 ) // first is unassigned if ( Value1 == 2 ) // first is unassigned
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0; return 0;
} }
...@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar ) ...@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cbs_ManPropagate( Cbs_Man_t * p ) int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
{ {
int hClause;
Gia_Obj_t * pVar; Gia_Obj_t * pVar;
int i, k; int i, k;
while ( 1 ) while ( 1 )
{ {
Cbs_QueForEachEntry( p->pProp, pVar, i ) Cbs_QueForEachEntry( p->pProp, pVar, i )
{ {
if ( Cbs_ManPropagateOne( p, pVar ) ) if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
return 1; return hClause;
} }
p->pProp.iHead = p->pProp.iTail; p->pProp.iHead = p->pProp.iTail;
k = p->pJust.iHead; k = p->pJust.iHead;
...@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p ) ...@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
{ {
if ( Cbs_VarIsJust( pVar ) ) if ( Cbs_VarIsJust( pVar ) )
p->pJust.pData[k++] = pVar; p->pJust.pData[k++] = pVar;
else if ( Cbs_ManPropagateTwo( p, pVar ) ) else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
return 1; return hClause;
} }
if ( k == p->pJust.iTail ) if ( k == p->pJust.iTail )
break; break;
...@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p ) ...@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
Synopsis [Solve the problem recursively.] Synopsis [Solve the problem recursively.]
Description [Returns 1 if unsat or undecided; 0 if satisfiable.] Description [Returns learnt clause if unsat, NULL if sat or undecided.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cbs_ManSolve_rec( Cbs_Man_t * p ) int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
{ {
Gia_Obj_t * pVar; Cbs_Que_t * pQue = &(p->pClauses);
Gia_Obj_t * pVar, * pDecVar;
int hClause, hLearn0, hLearn1;
int iPropHead, iJustHead, iJustTail; int iPropHead, iJustHead, iJustTail;
// propagate assignments // propagate assignments
assert( !Cbs_QueIsEmpty(&p->pProp) ); assert( !Cbs_QueIsEmpty(&p->pProp) );
if ( Cbs_ManPropagate( p ) ) if ( (hClause = Cbs_ManPropagate( p, Level )) )
return 1; return hClause;
// check for satisfying assignment // check for satisfying assignment
assert( Cbs_QueIsEmpty(&p->pProp) ); assert( Cbs_QueIsEmpty(&p->pProp) );
if ( Cbs_QueIsEmpty(&p->pJust) ) if ( Cbs_QueIsEmpty(&p->pJust) )
return 0; return 0;
// quit using resource limits // quit using resource limits
p->Pars.nBTThis++;
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs_ManCheckLimits( p ) ) if ( Cbs_ManCheckLimits( p ) )
return 1; return 0;
// remember the state before branching // remember the state before branching
iPropHead = p->pProp.iHead; iPropHead = p->pProp.iHead;
Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail ); Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
...@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p ) ...@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
pVar = Cbs_ManDecideMaxFF( p ); pVar = Cbs_ManDecideMaxFF( p );
else assert( 0 ); else assert( 0 );
assert( Cbs_VarIsJust( pVar ) ); assert( Cbs_VarIsJust( pVar ) );
// decide using fanout count! // chose decision variable using fanout count
if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
{ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
// decide on first fanin
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
if ( !Cbs_ManSolve_rec( p ) )
return 0;
if ( Cbs_ManCheckLimits( p ) )
return 1;
Cbs_ManCancelUntil( p, iPropHead );
Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
// decide on second fanin
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
}
else else
{ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
// decide on first fanin // decide on first fanin
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
if ( !Cbs_ManSolve_rec( p ) ) if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
return 0; return 0;
if ( Cbs_ManCheckLimits( p ) ) if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
return 1; return hLearn0;
Cbs_ManCancelUntil( p, iPropHead ); Cbs_ManCancelUntil( p, iPropHead );
Cbs_QueRestore( &p->pJust, iJustHead, iJustTail ); Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
// decide on second fanin // decide on second fanin
Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
} if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
if ( !Cbs_ManSolve_rec( p ) )
return 0; return 0;
if ( Cbs_ManCheckLimits( p ) ) if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
return 1; return hLearn1;
return 1; hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 );
// Cbs_ManPrintClauseNew( p, Level, hClause );
// if ( Level > Cbs_ClauseDecLevel(p, hClause) )
// p->Pars.nBTThisNc++;
p->Pars.nBTThis++;
return hClause;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p ) ...@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
***********************************************************************/ ***********************************************************************/
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{ {
// Gia_Obj_t * pTemp; int RetValue = 0;
// int i;
int RetValue;
// Gia_ManForEachObj( p->pAig, pTemp, i )
// assert( pTemp->fMark0 == 0 );
assert( !p->pProp.iHead && !p->pProp.iTail ); assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail ); assert( !p->pJust.iHead && !p->pJust.iTail );
p->Pars.nBTThis = p->Pars.nJustThis = 0; assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
Cbs_ManAssign( p, pObj ); p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
RetValue = Cbs_ManSolve_rec( p ); Cbs_ManAssign( p, pObj, 0, NULL, NULL );
if ( RetValue == 0 ) if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModel( p, p->vModel ); Cbs_ManSaveModel( p, p->vModel );
else
RetValue = 1;
Cbs_ManCancelUntil( p, 0 ); Cbs_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0; p->pJust.iHead = p->pJust.iTail = 0;
p->pClauses.iHead = p->pClauses.iTail = 1;
p->Pars.nBTTotal += p->Pars.nBTThis; p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) ) if ( Cbs_ManCheckLimits( p ) )
return -1; RetValue = -1;
return RetValue; return RetValue;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Procedure to test the new SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs_ManSolveTest( Gia_Man_t * pGia )
{
extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
int nConfsMax = 1000;
int CountUnsat, CountSat, CountUndec;
Cbs_Man_t * p;
Vec_Int_t * vCex;
Vec_Int_t * vVisit;
Gia_Obj_t * pRoot;
int i, RetValue, clk = clock();
Gia_ManCreateRefs( pGia );
// create logic network
p = Cbs_ManAlloc();
p->pAig = pGia;
// prepare AIG
Gia_ManCleanValue( pGia );
Gia_ManCleanMark0( pGia );
Gia_ManCleanMark1( pGia );
// vCex = Vec_IntAlloc( 100 );
vVisit = Vec_IntAlloc( 100 );
// solve for each output
CountUnsat = CountSat = CountUndec = 0;
Gia_ManForEachCo( pGia, pRoot, i )
{
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
continue;
// Gia_ManIncrementTravId( pGia );
//printf( "Output %6d : ", i );
// iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
// RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex );
RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
if ( RetValue == 1 )
CountUnsat++;
else if ( RetValue == -1 )
CountUndec++;
else
{
// int iLit, k;
vCex = Cbs_ReadModel( p );
// printf( "complemented = %d. ", Gia_ObjFaninC0(pRoot) );
//printf( "conflicts = %6d max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis );
// Vec_IntForEachEntry( vCex, iLit, k )
// printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) );
// printf( "\n" );
Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
assert( RetValue == 0 );
CountSat++;
}
// Gia_ManCheckMark0( p );
// Gia_ManCheckMark1( p );
}
Cbs_ManStop( p );
// Vec_IntFree( vCex );
Vec_IntFree( vVisit );
printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec );
ABC_PRT( "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Prints statistics of the manager.] Synopsis [Prints statistics of the manager.]
Description [] Description []
...@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p ) ...@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus ) Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{ {
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ); extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p; Cbs_Man_t * p;
...@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat ...@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Gia_ManCreateRefs( pAig ); Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig ); Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig ); Gia_ManCleanMark1( pAig );
Gia_ManFillValue( pAig ); // maps nodes into trail ids
// create logic network // create logic network
p = Cbs_ManAlloc(); p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs; p->Pars.nBTLimit = nConfs;
...@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat ...@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
} }
else else
{ {
printf( "Constant 0 output of SRM!!!\n" ); // printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 ); Vec_StrPush( vStatus, 1 );
} }
continue; continue;
...@@ -838,12 +1025,15 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat ...@@ -838,12 +1025,15 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
p->Pars.fUseHighest = 1; p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0; p->Pars.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
// printf( "\n" );
/*
if ( status == -1 ) if ( status == -1 )
{ {
p->Pars.fUseHighest = 0; p->Pars.fUseHighest = 0;
p->Pars.fUseLowest = 1; p->Pars.fUseLowest = 1;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
} }
*/
Vec_StrPush( vStatus, (char)status ); Vec_StrPush( vStatus, (char)status );
if ( status == -1 ) if ( status == -1 )
{ {
...@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat ...@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
continue; continue;
} }
p->nSatSat++; p->nSatSat++;
p->nConfUnsat += p->Pars.nBTThis; p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit ); // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i ); Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk; p->timeSatSat += clock() - clk;
...@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat ...@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Vec_IntFree( vVisit ); Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig); p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
// Cbs_ManSatPrintStats( p ); if ( fVerbose )
Cbs_ManSatPrintStats( p );
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
Cbs_ManStop( p ); Cbs_ManStop( p );
*pvStatus = vStatus; *pvStatus = vStatus;
// printf( "Total number of cex literals = %d. (Ave = %d)\n", // printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat ); // (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
......
src/aig/gia/giaCSatOld.c 0 → 100644
/**CFile****************************************************************
FileName [giaCSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [A simple circuit-based solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Cbs0_Par_t_ Cbs0_Par_t;
struct Cbs0_Par_t_
{
// conflict limits
int nBTLimit; // limit on the number of conflicts
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
// decision heuristics
int fUseHighest; // use node with the highest ID
int fUseLowest; // use node with the highest ID
int fUseMaxFF; // use node with the largest fanin fanout
// other
int fVerbose;
};
typedef struct Cbs0_Que_t_ Cbs0_Que_t;
struct Cbs0_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
typedef struct Cbs0_Man_t_ Cbs0_Man_t;
struct Cbs0_Man_t_
{
Cbs0_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager
Cbs0_Que_t pProp; // propagation queue
Cbs0_Que_t pJust; // justification queue
Vec_Int_t * vModel; // satisfying assignment
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
int nSatUndec; // the number of timeouts
int nSatTotal; // the number of calls
// conflicts
int nConfUnsat; // conflicts in unsat problems
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
int timeSatUnsat; // unsat
int timeSatSat; // sat
int timeSatUndec; // undecided
int timeTotal; // total runtime
};
static inline int Cbs0_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
static inline void Cbs0_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
static inline void Cbs0_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; }
static inline int Cbs0_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
static inline void Cbs0_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
static inline int Cbs0_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)); }
static inline int Cbs0_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int Cbs0_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
#define Cbs0_QueForEachEntry( Que, pObj, i ) \
for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sets default values of the parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs0_SetDefaultParams( Cbs0_Par_t * pPars )
{
memset( pPars, 0, sizeof(Cbs0_Par_t) );
pPars->nBTLimit = 1000; // limit on the number of conflicts
pPars->nJustLimit = 100; // limit on the size of justification queue
pPars->fUseHighest = 1; // use node with the highest ID
pPars->fUseLowest = 0; // use node with the highest ID
pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
pPars->fVerbose = 1; // print detailed statistics
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cbs0_Man_t * Cbs0_ManAlloc()
{
Cbs0_Man_t * p;
p = ABC_CALLOC( Cbs0_Man_t, 1 );
p->pProp.nSize = p->pJust.nSize = 10000;
p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
p->vModel = Vec_IntAlloc( 1000 );
Cbs0_SetDefaultParams( &p->Pars );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs0_ManStop( Cbs0_Man_t * p )
{
Vec_IntFree( p->vModel );
ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Returns satisfying assignment.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs0_ReadModel( Cbs0_Man_t * p )
{
return p->vModel;
}
/**Function*************************************************************
Synopsis [Returns 1 if the solver is out of limits.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_ManCheckLimits( Cbs0_Man_t * p )
{
return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
}
/**Function*************************************************************
Synopsis [Saves the satisfying assignment as an array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
{
Gia_Obj_t * pVar;
int i;
Vec_IntClear( vCex );
p->pProp.iHead = 0;
Cbs0_QueForEachEntry( p->pProp, pVar, i )
if ( Gia_ObjIsCi(pVar) )
// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_QueIsEmpty( Cbs0_Que_t * p )
{
return p->iHead == p->iTail;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_QuePush( Cbs0_Que_t * p, Gia_Obj_t * pObj )
{
if ( p->iTail == p->nSize )
{
p->nSize *= 2;
p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
}
p->pData[p->iTail++] = pObj;
}
/**Function*************************************************************
Synopsis [Returns 1 if the object in the queue.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_QueHasNode( Cbs0_Que_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pTemp;
int i;
Cbs0_QueForEachEntry( *p, pTemp, i )
if ( pTemp == pObj )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_QueStore( Cbs0_Que_t * p, int * piHeadOld, int * piTailOld )
{
int i;
*piHeadOld = p->iHead;
*piTailOld = p->iTail;
for ( i = *piHeadOld; i < *piTailOld; i++ )
Cbs0_QuePush( p, p->pData[i] );
p->iHead = *piTailOld;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_QueRestore( Cbs0_Que_t * p, int iHeadOld, int iTailOld )
{
p->iHead = iHeadOld;
p->iTail = iTailOld;
}
/**Function*************************************************************
Synopsis [Max number of fanins fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
{
int Count0, Count1;
assert( !Gia_IsComplement(pObj) );
assert( Gia_ObjIsAnd(pObj) );
Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
return ABC_MAX( Count0, Count1 );
}
/**Function*************************************************************
Synopsis [Find variable with the highest ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Gia_Obj_t * Cbs0_ManDecideHighest( Cbs0_Man_t * p )
{
Gia_Obj_t * pObj, * pObjMax = NULL;
int i;
Cbs0_QueForEachEntry( p->pJust, pObj, i )
if ( pObjMax == NULL || pObjMax < pObj )
pObjMax = pObj;
return pObjMax;
}
/**Function*************************************************************
Synopsis [Find variable with the lowest ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Gia_Obj_t * Cbs0_ManDecideLowest( Cbs0_Man_t * p )
{
Gia_Obj_t * pObj, * pObjMin = NULL;
int i;
Cbs0_QueForEachEntry( p->pJust, pObj, i )
if ( pObjMin == NULL || pObjMin > pObj )
pObjMin = pObj;
return pObjMin;
}
/**Function*************************************************************
Synopsis [Find variable with the maximum number of fanin fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Gia_Obj_t * Cbs0_ManDecideMaxFF( Cbs0_Man_t * p )
{
Gia_Obj_t * pObj, * pObjMax = NULL;
int i, iMaxFF = 0, iCurFF;
assert( p->pAig->pRefs != NULL );
Cbs0_QueForEachEntry( p->pJust, pObj, i )
{
iCurFF = Cbs0_VarFaninFanoutMax( p, pObj );
assert( iCurFF > 0 );
if ( iMaxFF < iCurFF )
{
iMaxFF = iCurFF;
pObjMax = pObj;
}
}
return pObjMax;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_ManCancelUntil( Cbs0_Man_t * p, int iBound )
{
Gia_Obj_t * pVar;
int i;
assert( iBound <= p->pProp.iTail );
p->pProp.iHead = iBound;
Cbs0_QueForEachEntry( p->pProp, pVar, i )
Cbs0_VarUnassign( pVar );
p->pProp.iTail = iBound;
}
/**Function*************************************************************
Synopsis [Assigns the variables a value.]
Description [Returns 1 if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs0_ManAssign( Cbs0_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pObjR = Gia_Regular(pObj);
assert( Gia_ObjIsCand(pObjR) );
assert( !Cbs0_VarIsAssigned(pObjR) );
Cbs0_VarAssign( pObjR );
Cbs0_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
Cbs0_QuePush( &p->pProp, pObjR );
}
/**Function*************************************************************
Synopsis [Propagates a variable.]
Description [Returns 1 if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_ManPropagateOne( Cbs0_Man_t * p, Gia_Obj_t * pVar )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
assert( Cbs0_VarIsAssigned(pVar) );
if ( Gia_ObjIsCi(pVar) )
return 0;
assert( Gia_ObjIsAnd(pVar) );
Value0 = Cbs0_VarFanin0Value(pVar);
Value1 = Cbs0_VarFanin1Value(pVar);
if ( Cbs0_VarValue(pVar) )
{ // value is 1
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 1;
if ( Value0 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_ObjChild0(pVar) );
if ( Value1 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_ObjChild1(pVar) );
return 0;
}
// value is 0
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
return 1;
if ( Value0 == 1 || Value1 == 1 ) // one is 1
{
if ( Value0 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
if ( Value1 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
return 0;
}
assert( Cbs0_VarIsJust(pVar) );
assert( !Cbs0_QueHasNode( &p->pJust, pVar ) );
Cbs0_QuePush( &p->pJust, pVar );
return 0;
}
/**Function*************************************************************
Synopsis [Propagates a variable.]
Description [Returns 1 if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs0_ManPropagateTwo( Cbs0_Man_t * p, Gia_Obj_t * pVar )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
assert( Gia_ObjIsAnd(pVar) );
assert( Cbs0_VarIsAssigned(pVar) );
assert( !Cbs0_VarValue(pVar) );
Value0 = Cbs0_VarFanin0Value(pVar);
Value1 = Cbs0_VarFanin1Value(pVar);
// value is 0
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
return 1;
assert( Value0 == 1 || Value1 == 1 );
if ( Value0 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
if ( Value1 == 2 ) // first is unassigned
Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
return 0;
}
/**Function*************************************************************
Synopsis [Propagates all variables.]
Description [Returns 1 if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cbs0_ManPropagate( Cbs0_Man_t * p )
{
Gia_Obj_t * pVar;
int i, k;
while ( 1 )
{
Cbs0_QueForEachEntry( p->pProp, pVar, i )
{
if ( Cbs0_ManPropagateOne( p, pVar ) )
return 1;
}
p->pProp.iHead = p->pProp.iTail;
k = p->pJust.iHead;
Cbs0_QueForEachEntry( p->pJust, pVar, i )
{
if ( Cbs0_VarIsJust( pVar ) )
p->pJust.pData[k++] = pVar;
else if ( Cbs0_ManPropagateTwo( p, pVar ) )
return 1;
}
if ( k == p->pJust.iTail )
break;
p->pJust.iTail = k;
}
return 0;
}
/**Function*************************************************************
Synopsis [Solve the problem recursively.]
Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
{
Gia_Obj_t * pVar, * pDecVar;
int iPropHead, iJustHead, iJustTail;
// propagate assignments
assert( !Cbs0_QueIsEmpty(&p->pProp) );
if ( Cbs0_ManPropagate( p ) )
return 1;
// check for satisfying assignment
assert( Cbs0_QueIsEmpty(&p->pProp) );
if ( Cbs0_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs0_ManCheckLimits( p ) )
return 0;
// remember the state before branching
iPropHead = p->pProp.iHead;
Cbs0_QueStore( &p->pJust, &iJustHead, &iJustTail );
// find the decision variable
if ( p->Pars.fUseHighest )
pVar = Cbs0_ManDecideHighest( p );
else if ( p->Pars.fUseLowest )
pVar = Cbs0_ManDecideLowest( p );
else if ( p->Pars.fUseMaxFF )
pVar = Cbs0_ManDecideMaxFF( p );
else assert( 0 );
assert( Cbs0_VarIsJust( pVar ) );
// chose decision variable using fanout count
if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
pDecVar = Gia_Not(Gia_ObjChild0(pVar));
else
pDecVar = Gia_Not(Gia_ObjChild1(pVar));
// decide on first fanin
Cbs0_ManAssign( p, pDecVar );
if ( !Cbs0_ManSolve_rec( p ) )
return 0;
Cbs0_ManCancelUntil( p, iPropHead );
Cbs0_QueRestore( &p->pJust, iJustHead, iJustTail );
// decide on second fanin
Cbs0_ManAssign( p, Gia_Not(pDecVar) );
if ( !Cbs0_ManSolve_rec( p ) )
return 0;
p->Pars.nBTThis++;
return 1;
}
/**Function*************************************************************
Synopsis [Looking for a satisfying assignment of the node.]
Description [Assumes that each node has flag pObj->fMark0 set to 0.
Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
The node may be complemented. ]
SideEffects []
SeeAlso []
***********************************************************************/
int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
{
int RetValue;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
p->Pars.nBTThis = p->Pars.nJustThis = 0;
Cbs0_ManAssign( p, pObj );
RetValue = Cbs0_ManSolve_rec( p );
if ( RetValue == 0 && !Cbs0_ManCheckLimits(p) )
Cbs0_ManSaveModel( p, p->vModel );
Cbs0_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs0_ManCheckLimits( p ) )
RetValue = -1;
// printf( "Outcome = %2d. Confs = %6d. Decision level max = %3d.\n",
// RetValue, p->Pars.nBTThis, p->DecLevelMax );
return RetValue;
}
/**Function*************************************************************
Synopsis [Prints statistics of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
{
printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
printf( "Conf = %5d ", p->Pars.nBTLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}
/**Function*************************************************************
Synopsis [Procedure to test the new SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs0_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore;
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;
int i, status, clk, clkTotal = clock();
assert( Gia_ManRegNum(pAig) == 0 );
// prepare AIG
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
// create logic network
p = Cbs0_ManAlloc();
p->Pars.nBTLimit = nConfs;
p->pAig = pAig;
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
vVisit = Vec_IntAlloc( 100 );
vCex = Cbs0_ReadModel( p );
// solve for each output
Gia_ManForEachCo( pAig, pRoot, i )
{
Vec_IntClear( vCex );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
{
if ( Gia_ObjFaninC0(pRoot) )
{
printf( "Constant 1 output of SRM!!!\n" );
Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
Vec_StrPush( vStatus, 0 );
}
else
{
// printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
}
clk = clock();
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
/*
if ( status == -1 )
{
p->Pars.fUseHighest = 0;
p->Pars.fUseLowest = 1;
status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
}
*/
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += clock() - clk;
continue;
}
if ( status == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
}
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
if ( fVerbose )
Cbs0_ManSatPrintStats( p );
Cbs0_ManStop( p );
*pvStatus = vStatus;
// printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
return vCexStore;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/gia/giaRetime.c
...@@ -243,6 +243,7 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe ...@@ -243,6 +243,7 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe
// finally derive the new manager // finally derive the new manager
pNew = Gia_ManRetimeDupForward( p, vCut ); pNew = Gia_ManRetimeDupForward( p, vCut );
Vec_PtrFree( vCut ); Vec_PtrFree( vCut );
if ( vObjClasses )
Vec_IntFree( vObjClasses ); Vec_IntFree( vObjClasses );
pNew->vFlopClasses = vFlopClasses; pNew->vFlopClasses = vFlopClasses;
return pNew; return pNew;
......
src/aig/gia/giaSim.c
...@@ -405,7 +405,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) ...@@ -405,7 +405,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit ); printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC ); printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
} }
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) ) if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{ {
......
src/aig/gia/module.make
...@@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \ ...@@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAig.c \ src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \ src/aig/gia/giaAiger.c \
src/aig/gia/giaCof.c \ src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \ src/aig/gia/giaCSat.c \
src/aig/gia/giaDfs.c \ src/aig/gia/giaDfs.c \
src/aig/gia/giaDup.c \ src/aig/gia/giaDup.c \
......
src/base/abci/abc.c
...@@ -17681,7 +17681,7 @@ usage: ...@@ -17681,7 +17681,7 @@ usage:
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
// fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll ); // fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
// fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta ); // fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" ); fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
// fprintf( pErr, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" ); // fprintf( pErr, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
...@@ -23472,7 +23472,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23472,7 +23472,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCSat = 0; int fCSat = 0;
Cec_ManSatSetDefaultParams( pPars ); Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfcvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -23509,6 +23509,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23509,6 +23509,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nCallsRecycle < 0 ) if ( pPars->nCallsRecycle < 0 )
goto usage; goto usage;
break; break;
case 'n':
pPars->fNonChrono ^= 1;
break;
case 'm': case 'm':
pPars->fCheckMiter ^= 1; pPars->fCheckMiter ^= 1;
break; break;
...@@ -23534,7 +23537,10 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23534,7 +23537,10 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Vec_Int_t * vCounters; Vec_Int_t * vCounters;
Vec_Str_t * vStatus; Vec_Str_t * vStatus;
vCounters = Cbs_ManSolveMiter( pAbc->pAig, 10*pPars->nBTLimit, &vStatus ); if ( pPars->fNonChrono )
vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else
vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
Vec_IntFree( vCounters ); Vec_IntFree( vCounters );
Vec_StrFree( vStatus ); Vec_StrFree( vStatus );
} }
...@@ -23546,11 +23552,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23546,11 +23552,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: &sat [-CSN <num>] [-mfcvh]\n" ); fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" );
fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" ); fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax ); fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle ); fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
fprintf( stdout, "\t-n : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" );
fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment