summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/aig/cec/cec.c2
-rw-r--r--src/aig/cec/cec.h3
-rw-r--r--src/aig/cec/cecCec.c2
-rw-r--r--src/aig/cec/cecChoice.c2
-rw-r--r--src/aig/cec/cecClass.c10
-rw-r--r--src/aig/cec/cecCore.c9
-rw-r--r--src/aig/cec/cecCorr.c457
-rw-r--r--src/aig/cec/cecInt.h2
-rw-r--r--src/aig/cec/cecIso.c2
-rw-r--r--src/aig/cec/cecMan.c4
-rw-r--r--src/aig/cec/cecPat.c2
-rw-r--r--src/aig/cec/cecSeq.c2
-rw-r--r--src/aig/cec/cecSim.c2
-rw-r--r--src/aig/cec/cecSolve.c2
-rw-r--r--src/aig/cec/cecSweep.c6
-rw-r--r--src/aig/gia/gia.h4
-rw-r--r--src/aig/gia/giaCSat.c497
-rw-r--r--src/aig/gia/giaCSatOld.c797
-rw-r--r--src/aig/gia/giaRetime.c1
-rw-r--r--src/aig/gia/giaSim.c2
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c15
23 files changed, 1410 insertions, 418 deletions
diff --git a/abclib.dsp b/abclib.dsp
index e11e9b9e..ffe0a866 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3695,6 +3695,10 @@ SOURCE=.\src\aig\gia\giaCSat.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\gia\giaCSatOld.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\gia\giaDfs.c
# End Source File
# Begin Source File
diff --git a/src/aig/cec/cec.c b/src/aig/cec/cec.c
index a017f831..17b27ec5 100644
--- a/src/aig/cec/cec.c
+++ b/src/aig/cec/cec.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis []
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index e26455ba..a965730f 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [External declarations.]
@@ -44,6 +44,7 @@ struct Cec_ParSat_t_
int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables
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 fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index f3d3dea9..82df6008 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Integrated combinatinal equivalence checker.]
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index ff30e1bb..2a619e39 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Computation of structural choices.]
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index a8ed017a..49930836 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -4,9 +4,9 @@
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]
@@ -838,6 +838,8 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
// allocate representation
p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, 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
if ( p->pPars->fLatchCorr )
Gia_ManForEachObj( p->pAig, pObj, i )
@@ -848,9 +850,9 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
// if sequential simulation, set starting representative of ROs to be constant 0
if ( p->pPars->fSeqSimulate )
Gia_ManForEachRo( p->pAig, pObj, i )
- Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
+ if ( pObj->Value )
+ Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
// perform simulation
- Gia_ManSetRefs( p->pAig );
p->nWords = 1;
do {
if ( p->pPars->fVerbose )
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index d3c54948..7759428e 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Core procedures.]
@@ -42,9 +42,10 @@
void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
{
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->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->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
@@ -399,7 +400,7 @@ p->timeSat += clock() - clk;
// if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
{
- if ( pParsSat->nBTLimit >= 10000 )
+ if ( pParsSat->nBTLimit >= 10001 )
break;
pParsSat->nBTLimit *= 10;
if ( p->pPars->fVerbose )
@@ -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 )
printf( "Switching into reduced mode.\n" );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index abc76416..05259bc7 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -1,12 +1,12 @@
/**CFile****************************************************************
- FileName [cecLcorr.c]
+ FileName [cecCorr.c]
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]
@@ -14,7 +14,7 @@
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,13 +74,10 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
return;
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 );
- iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
- Gia_ObjSetCopyF( p, f, pObj, iLitNew );
- return;
- }
+ Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
+ iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+ Gia_ObjSetCopyF( p, f, pObj, iLitNew );
+ return;
}
assert( Gia_ObjIsCand(pObj) );
iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
@@ -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_ManForEachRo( p, pObj, i )
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++ )
{
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
{
if ( Gia_ObjIsConst( p, i ) )
{
- if ( Gia_ObjIsFailedPair(p, 0, i) )
- continue;
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
@@ -151,11 +143,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
- if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
- {
- iPrev = iObj;
- continue;
- }
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
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
iPrev = iObj;
}
iObj = i;
- if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
- continue;
iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
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
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
- if ( Gia_ObjIsFailedPair(p, Gia_ObjRepr(p, i), i) )
- continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
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
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*************************************************************
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 )
/**Function*************************************************************
- Synopsis [Remaps simulation info from SRM to the original AIG.]
+ Synopsis [Collects information about remapping.]
Description []
@@ -276,8 +291,8 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
{
// skip ROs without representatives
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_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), 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)) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
@@ -319,51 +334,7 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo )
/**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;
- assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
- Vec_StrForEachEntry( vStatus, status, 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) )
-// 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;
- }
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Marks all the nodes as proved.]
+ Synopsis [Packs one counter-examples into the array of simulation info.]
Description []
@@ -371,67 +342,33 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
SeeAlso []
-***********************************************************************/
-void Gia_ManSetProvedNodes( Gia_Man_t * p )
+*************************************`**********************************/
+int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{
- Gia_Obj_t * pObj;
- int i, nLits = 0;
- Gia_ManForEachObj1( p, pObj, i )
- {
- if ( Gia_ObjRepr(p, i) == GIA_VOID )
- continue;
- if ( Gia_ObjIsFailedPair( p, Gia_ObjRepr(p, i), i ) )
- continue;
- Gia_ObjSetProved( p, i );
- nLits++;
- }
-// printf( "Identified %d proved literals.\n", nLits );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- 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++ )
+ unsigned * pInfo, * pPres;
+ int i;
+ for ( i = 0; i < nLits; i++ )
{
- if ( Gia_ObjIsNone(p, i) )
- CounterX++;
- else if ( Gia_ObjIsConst(p, i) )
- Counter0++;
- else if ( Gia_ObjIsHead(p, i) )
- Counter++;
+ pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ if ( Aig_InfoHasBit( pPres, iBit ) &&
+ Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ return 0;
}
- 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 )
+ for ( i = 0; i < nLits; i++ )
{
- if ( Entry == 1 )
- nProve++;
- else if ( Entry == 0 )
- nDispr++;
- else if ( Entry == -1 )
- nFail++;
+ pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ Aig_InfoSetBit( pPres, iBit );
+ if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ Aig_InfoXorBit( pInfo, iBit );
}
- printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
- ABC_PRT( "T", Time );
+ return 1;
}
/**Function*************************************************************
- Synopsis [Sets register values from the counter-example.]
+ Synopsis [Performs bitpacking of counter-examples.]
Description []
@@ -440,29 +377,44 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
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++ )
+int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
+{
+ Vec_Int_t * vPat;
+ Vec_Ptr_t * vPres;
+ 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) )
{
- pInfo = Vec_PtrEntry( vInfo, k );
- for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom( 0 );
+ // skip the output number
+ iStart++;
+ // get the number of items
+ nSize = Vec_IntEntry( vCexStore, iStart++ );
+ if ( nSize <= 0 )
+ continue;
+ // extract pattern
+ Vec_IntClear( vPat );
+ for ( k = 0; k < nSize; k++ )
+ Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
+ // add pattern to storage
+ for ( k = 1; k < nBits; k++ )
+ if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+ break;
+ kMax = AIG_MAX( kMax, k );
+ if ( k == nBits-1 )
+ break;
}
+ Vec_PtrFree( vPres );
+ Vec_IntFree( vPat );
+ return iStart;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Performs bitpacking of counter-examples.]
Description []
@@ -503,7 +455,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
/**Function*************************************************************
- Synopsis [Packs patterns into array of simulation info.]
+ Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
@@ -511,33 +463,86 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
SeeAlso []
-*************************************`**********************************/
-int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
-{
- unsigned * pInfo, * pPres;
- int i;
- for ( i = 0; i < nLits; i++ )
+***********************************************************************/
+int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
+{
+ Vec_Int_t * vPairs;
+ Vec_Ptr_t * vSimInfo;
+ 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]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- if ( Aig_InfoHasBit( pPres, iBit ) &&
- Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- return 0;
+ Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
+ iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
+// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
+// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
+ 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]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- Aig_InfoSetBit( pPres, iBit );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- Aig_InfoXorBit( pInfo, iBit );
+ 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) )
+ 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;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Marks all the nodes as proved.]
Description []
@@ -546,54 +551,23 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
SeeAlso []
***********************************************************************/
-int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
-{
- Vec_Int_t * vPat;
- Vec_Ptr_t * vPres;
- 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) )
+void Gia_ManSetProvedNodes( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i, nLits = 0;
+ Gia_ManForEachObj1( p, pObj, i )
{
- // skip the output number
- iStart++;
- // get the number of items
- nSize = Vec_IntEntry( vCexStore, iStart++ );
- if ( nSize <= 0 )
+ if ( Gia_ObjRepr(p, i) == GIA_VOID )
continue;
- // extract pattern
- Vec_IntClear( vPat );
- 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;
+ Gia_ObjSetProved( p, i );
+ nLits++;
}
-// printf( "\n" );
-// printf( "kMax = %d.\n", kMax );
- Vec_PtrFree( vPres );
- Vec_IntFree( vPat );
- return iStart;
+// printf( "Identified %d proved literals.\n", nLits );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Prints statistics during solving.]
Description []
@@ -602,37 +576,39 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
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;
- Vec_Ptr_t * vSimInfo;
- 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) )
+ 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++ )
{
-//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
- Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
- iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
-// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
-// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
- Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
- RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
-// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
+ if ( Gia_ObjIsNone(p, i) )
+ CounterX++;
+ else if ( Gia_ObjIsConst(p, i) )
+ Counter0++;
+ else if ( Gia_ObjIsHead(p, i) )
+ Counter++;
}
-//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
- assert( iStart == Vec_IntSize(vCexStore) );
- Vec_PtrFree( vSimInfo );
- Vec_IntFree( vPairs );
- return RetValue;
+ 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 []
+ Synopsis [Top-level procedure for register correspondence.]
Description []
@@ -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 )
{
- int nAddFrames = 2; // additional timeframes to simulate
+ int nAddFrames = 1; // additional timeframes to simulate
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
@@ -701,11 +677,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
break;
}
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
-
// found counter-examples to speculation
clk2 = clock();
if ( pPars->fUseCSat )
- vCexStore = Cbs_ManSolveMiter( pSrm, pPars->nBTLimit, &vStatus );
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
@@ -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 );
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
-//Gia_ManEquivPrintClasses( pAig, 1, 0 );
Vec_StrFree( vStatus );
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 );
clkTotal = clock() - clkTotal;
if ( pPars->fVerbose )
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 )
{
+ 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( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, 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;
}
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 86af2614..22bd292b 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [External declarations.]
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
index 08d4b7ec..ddb539c2 100644
--- a/src/aig/cec/cecIso.c
+++ b/src/aig/cec/cecIso.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Detection of structural isomorphism.]
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 430d961e..eb582e4c 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -4,9 +4,9 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
- Synopsis [Manager pcocures.]
+ Synopsis [Manager procedures.]
Author [Alan Mishchenko]
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index dacc5daf..a5be4c1c 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Simulation pattern manager.]
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index e69b526e..3d05172f 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Refinement of sequential equivalence classes.]
diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c
index dbd3bd5e..61610a46 100644
--- a/src/aig/cec/cecSim.c
+++ b/src/aig/cec/cecSim.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Simulation manager.]
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index a69d1d2a..fc2d5d7f 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [Performs one round of SAT solving.]
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 3024ac24..f5e5bd06 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [ceFraeep.c]
+ FileName [cecSweep.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [Combinatinoal equivalence checking.]
+ PackageName [Combinational equivalence checking.]
Synopsis [SAT sweeping manager.]
@@ -14,7 +14,7 @@
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 $]
***********************************************************************/
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 87c85516..5395f361 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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 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 );
+/*=== giaCsatOld.c ============================================================*/
+extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== 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 =============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 5fa9f40f..15faea72 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -32,6 +32,7 @@ struct Cbs_Par_t_
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
+ int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
@@ -48,7 +49,7 @@ struct Cbs_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
- int nSize; // allocated size
+ int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
@@ -59,7 +60,11 @@ struct Cbs_Man_t_
Gia_Man_t * pAig; // AIG manager
Cbs_Que_t pProp; // propagation 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_Ptr_t * vTemp; // temporary storage
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
@@ -78,16 +83,26 @@ struct Cbs_Man_t_
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_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 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_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)); }
-#define Cbs_QueForEachEntry( Que, pObj, i ) \
+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 ) \
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 ///
////////////////////////////////////////////////////////////////////////
@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc()
{
Cbs_Man_t * p;
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->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
- p->vModel = Vec_IntAlloc( 1000 );
+ p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->vModel = Vec_IntAlloc( 1000 );
+ p->vLevReas = Vec_IntAlloc( 1000 );
+ p->vTemp = Vec_PtrAlloc( 1000 );
Cbs_SetDefaultParams( &p->Pars );
return p;
}
@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc()
***********************************************************************/
void Cbs_ManStop( Cbs_Man_t * p )
{
+ Vec_IntFree( p->vLevReas );
Vec_IntFree( p->vModel );
+ Vec_PtrFree( p->vTemp );
+ ABC_FREE( p->pClauses.pData );
ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData );
ABC_FREE( p );
@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int 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*************************************************************
@@ -400,7 +442,7 @@ static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p )
pObjMax = pObj;
}
}
- return pObjMax;
+ return pObjMax;
}
@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Cbs_QueForEachEntry( p->pProp, pVar, i )
Cbs_VarUnassign( pVar );
p->pProp.iTail = iBound;
+ Vec_IntShrink( p->vLevReas, 3*iBound );
}
/**Function*************************************************************
@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
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);
assert( Gia_ObjIsCand(pObjR) );
assert( !Cbs_VarIsAssigned(pObjR) );
Cbs_VarAssign( pObjR );
Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ assert( pObjR->Value == ~0 );
+ pObjR->Value = p->pProp.iTail;
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*************************************************************
Synopsis [Propagates a variable.]
- Description [Returns 1 if conflict; 0 if no conflict.]
+ Description [Returns clause handle if conflict; 0 if no conflict.]
SideEffects []
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;
assert( !Gia_IsComplement(pVar) );
@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Cbs_VarValue(pVar) )
{ // value is 1
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
- Cbs_ManAssign( p, Gia_ObjChild0(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_ObjChild1(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
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;
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
if ( Value0 == 1 || Value1 == 1 ) // one is 1
{
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // second is unassigned
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
assert( Cbs_VarIsJust(pVar) );
@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
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;
assert( !Gia_IsComplement(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
return 0;
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 );
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
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso []
***********************************************************************/
-int Cbs_ManPropagate( Cbs_Man_t * p )
+int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
{
+ int hClause;
Gia_Obj_t * pVar;
int i, k;
while ( 1 )
{
Cbs_QueForEachEntry( p->pProp, pVar, i )
{
- if ( Cbs_ManPropagateOne( p, pVar ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
+ return hClause;
}
p->pProp.iHead = p->pProp.iTail;
k = p->pJust.iHead;
@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
{
if ( Cbs_VarIsJust( pVar ) )
p->pJust.pData[k++] = pVar;
- else if ( Cbs_ManPropagateTwo( p, pVar ) )
- return 1;
+ else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
+ return hClause;
}
if ( k == p->pJust.iTail )
break;
@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
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 []
SeeAlso []
-
+
***********************************************************************/
-int Cbs_ManSolve_rec( Cbs_Man_t * p )
-{
- Gia_Obj_t * pVar;
+int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pVar, * pDecVar;
+ int hClause, hLearn0, hLearn1;
int iPropHead, iJustHead, iJustTail;
// propagate assignments
assert( !Cbs_QueIsEmpty(&p->pProp) );
- if ( Cbs_ManPropagate( p ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagate( p, Level )) )
+ return hClause;
// check for satisfying assignment
assert( Cbs_QueIsEmpty(&p->pProp) );
if ( Cbs_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
- p->Pars.nBTThis++;
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs_ManCheckLimits( p ) )
- return 1;
+ return 0;
// remember the state before branching
iPropHead = p->pProp.iHead;
Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
pVar = Cbs_ManDecideMaxFF( p );
else assert( 0 );
assert( Cbs_VarIsJust( pVar ) );
- // decide using fanout count!
- if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(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)) );
- }
+ // 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
- {
- // decide on first fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(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_ObjChild0(pVar)) );
- }
- if ( !Cbs_ManSolve_rec( p ) )
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+ // decide on first fanin
+ Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+ if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- return 1;
+ if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+ return hLearn0;
+ Cbs_ManCancelUntil( p, iPropHead );
+ Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+ if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+ return hLearn1;
+ 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*************************************************************
@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
***********************************************************************/
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{
-// Gia_Obj_t * pTemp;
-// int i;
- int RetValue;
-// Gia_ManForEachObj( p->pAig, pTemp, i )
-// assert( pTemp->fMark0 == 0 );
+ int RetValue = 0;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
- p->Pars.nBTThis = p->Pars.nJustThis = 0;
- Cbs_ManAssign( p, pObj );
- RetValue = Cbs_ManSolve_rec( p );
- if ( RetValue == 0 )
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
Cbs_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
+ p->pClauses.iHead = p->pClauses.iTail = 1;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) )
- return -1;
+ RetValue = -1;
return RetValue;
}
/**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.]
Description []
@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
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 );
Cbs_Man_t * p;
@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
+ Gia_ManFillValue( pAig ); // maps nodes into trail ids
// create logic network
p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs;
@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
}
else
{
- printf( "Constant 0 output of SRM!!!\n" );
+// printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
@@ -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.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+// printf( "\n" );
+/*
if ( status == -1 )
{
p->Pars.fUseHighest = 0;
p->Pars.fUseLowest = 1;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
}
+*/
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
continue;
}
p->nSatSat++;
- p->nConfUnsat += p->Pars.nBTThis;
+ p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
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 );
*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 );
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
new file mode 100644
index 00000000..409af56c
--- /dev/null
+++ b/src/aig/gia/giaCSatOld.c
@@ -0,0 +1,797 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 4f2c6e08..965b5981 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -243,6 +243,7 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe
// finally derive the new manager
pNew = Gia_ManRetimeDupForward( p, vCut );
Vec_PtrFree( vCut );
+ if ( vObjClasses )
Vec_IntFree( vObjClasses );
pNew->vFlopClasses = vFlopClasses;
return pNew;
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 7ee0ddc4..020683ad 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -405,7 +405,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
if ( pPars->fVerbose )
{
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 ) )
{
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 055d7580..916414fc 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaCof.c \
+ src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
src/aig/gia/giaDfs.c \
src/aig/gia/giaDup.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 876266af..ef7969be 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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-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-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-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" );
@@ -23472,7 +23472,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCSat = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
{
switch ( c )
{
@@ -23509,6 +23509,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nCallsRecycle < 0 )
goto usage;
break;
+ case 'n':
+ pPars->fNonChrono ^= 1;
+ break;
case 'm':
pPars->fCheckMiter ^= 1;
break;
@@ -23534,7 +23537,10 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vCounters;
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_StrFree( vStatus );
}
@@ -23546,11 +23552,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
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-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-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-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" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 07:16:04 +0000