summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAiger.c2
-rw-r--r--src/aig/gia/giaCSat.c6
-rw-r--r--src/aig/gia/giaCSatOld.c6
-rw-r--r--src/aig/gia/giaEquiv.c235
5 files changed, 237 insertions, 15 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index af92acc9..9dad2742 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -557,6 +557,7 @@ extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
extern void Gia_ManDeriveReprs( Gia_Man_t * p );
+extern int Gia_ManEquivCountLits( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
@@ -565,6 +566,7 @@ extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq,
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
+extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
extern void Gia_ManEquivImprove( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
@@ -663,6 +665,7 @@ extern void Tas_ManStop( Tas_Man_t * p );
extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
#ifdef __cplusplus
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index afe9164f..6c8ace8a 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -841,7 +841,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
// create normalized AIG
if ( !Gia_ManIsNormalized(pInit) )
{
- printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
+// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
p = Gia_ManDupNormalized( pInit );
}
else
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 644ccda5..e3aca7df 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -969,13 +969,13 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
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 );
+ p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, 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 );
+ p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, 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 );
+ p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index a0d97693..bd8f061b 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -680,13 +680,13 @@ void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
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 );
+ p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, 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 );
+ p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, 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 );
+ p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 8458268c..0f680e31 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -256,6 +256,69 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
SeeAlso []
***********************************************************************/
+void Gia_ManPrintStatsClasses( Gia_Man_t * p )
+{
+ int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
+ for ( i = 1; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjIsHead(p, i) )
+ Counter++;
+ else if ( Gia_ObjIsConst(p, i) )
+ Counter0++;
+ else if ( Gia_ObjIsNone(p, i) )
+ CounterX++;
+ if ( Gia_ObjProved(p, i) )
+ Proved++;
+ }
+ CounterX -= Gia_ManCoNum(p);
+ nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+
+// printf( "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
+// printf( "and =%5d ", Gia_ManAndNum(p) );
+// printf( "lev =%3d ", Gia_ManLevelNum(p) );
+ printf( "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivCountLits( Gia_Man_t * p )
+{
+ int i, Counter = 0, Counter0 = 0, CounterX = 0;
+ if ( p->pReprs == NULL || p->pNexts == NULL )
+ return 0;
+ for ( i = 1; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjIsHead(p, i) )
+ Counter++;
+ else if ( Gia_ObjIsConst(p, i) )
+ Counter0++;
+ else if ( Gia_ObjIsNone(p, i) )
+ CounterX++;
+ }
+ CounterX -= Gia_ManCoNum(p);
+ return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
{
int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
@@ -274,6 +337,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n",
Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
+// printf( "cst =%8d cls =%7d lit =%8d\n",
+// Counter0, Counter, nLits );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
@@ -696,6 +761,29 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
/**Function*************************************************************
+ Synopsis [Returns 1 if AIG has dangling nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManHasNoEquivs( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ if ( p->pReprs == NULL )
+ return 1;
+ Gia_ManForEachObj( p, pObj, i )
+ if ( Gia_ObjReprObj(p, i) != NULL )
+ break;
+ return i == Gia_ManObjNum(p);
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the AIG in the DFS order.]
Description []
@@ -743,16 +831,11 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
- // check if there are any equivalences defined
- Gia_ManForEachObj( p, pObj, i )
- if ( Gia_ObjReprObj(p, i) != NULL )
- break;
- if ( i == Gia_ManObjNum(p) )
+ if ( Gia_ManHasNoEquivs(p) )
{
printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
return NULL;
}
-
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
@@ -792,7 +875,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
return pNew;
}
-
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@@ -879,6 +961,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
+
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
@@ -918,7 +1001,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{
- printf( "Speculatively reduced model has no primary outputs.\n" );
+// printf( "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 );
}
ABC_FREE( p->pCopies );
@@ -931,6 +1014,41 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
/**Function*************************************************************
+ Synopsis [Creates initialized SRM with the given number of frames.]
+
+ Description [Uses as many frames as needed to create the number of
+ output not less than the number of equivalence literals.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
+{
+ Gia_Man_t * pFrames;
+ int f, nLits;
+ nLits = Gia_ManEquivCountLits( p );
+ for ( f = 1; ; f++ )
+ {
+ pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
+ if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
+ (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
+ break;
+ if ( f == nFramesMax )
+ break;
+ Gia_ManStop( pFrames );
+ pFrames = NULL;
+ }
+ if ( f == nFramesMax )
+ printf( "Stopped unrolling after %d frames.\n", nFramesMax );
+ if ( pnFrames )
+ *pnFrames = f;
+ return pFrames;
+}
+
+/**Function*************************************************************
+
Synopsis [Transforms equiv classes by removing the AB nodes.]
Description []
@@ -1292,6 +1410,107 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
return pNew;
}
+#include "aig.h"
+#include "saig.h"
+#include "cec.h"
+#include "giaAig.h"
+
+/**Function*************************************************************
+
+ Synopsis [Implements iteration during speculation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
+{
+ extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
+ Aig_Man_t * pTemp;
+ Gia_Man_t * pSrm, * pReduce, * pAux;
+ int nIter, nStart = 0;
+ if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
+ {
+ printf( "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
+ return 0;
+ }
+ // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
+ Gia_ManCleanMark0( pGia );
+ Gia_ManPrintStats( pGia, 0 );
+ for ( nIter = 0; ; nIter++ )
+ {
+ if ( Gia_ManHasNoEquivs(pGia) )
+ {
+ printf( "Gia_CommandSpecI: No equivalences left.\n" );
+ break;
+ }
+ printf( "ITER %3d : ", nIter );
+// if ( fVerbose )
+// printf( "Starting BMC from frame %d.\n", nStart );
+// if ( fVerbose )
+// Gia_ManPrintStats( pGia, 0 );
+ Gia_ManPrintStatsClasses( pGia );
+ // perform speculative reduction
+// if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
+ if ( !Cec_ManCheckNonTrivialCands(pGia) )
+ {
+ printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+ break;
+ }
+ pSrm = Gia_ManSpecReduce( pGia, 0, 0 );
+ // bmc2 -F 100 -C 25000
+ {
+ Gia_Cex_t * pCex;
+ int nFrames = nFramesInit; // different from default
+ int nNodeDelta = 2000;
+ int nBTLimit = nBTLimitInit; // different from default
+ int nBTLimitAll = 2000000;
+ pTemp = Gia_ManToAig( pSrm, 0 );
+// Aig_ManPrintStats( pTemp );
+ Gia_ManStop( pSrm );
+ Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 20, nBTLimit, nBTLimitAll, fVerbose, 0 );
+ pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+ Aig_ManStop( pTemp );
+ if ( pCex == NULL )
+ {
+ printf( "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
+ break;
+ }
+ if ( fStart )
+ nStart = pCex->iFrame;
+ // perform simulation
+ {
+ Cec_ParSim_t Pars, * pPars = &Pars;
+ Cec_ManSimSetDefaultParams( pPars );
+ pPars->fCheckMiter = fCheckMiter;
+ if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
+ {
+ ABC_FREE( pCex );
+ break;
+ }
+ ABC_FREE( pCex );
+ }
+ }
+ // write equivalence classes
+ Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
+ // reduce the model
+ pReduce = Gia_ManSpecReduce( pGia, 0, 0 );
+ if ( pReduce )
+ {
+ pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
+ Gia_ManStop( pAux );
+ Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+// Gia_ManPrintStatsShort( pReduce );
+ Gia_ManStop( pReduce );
+ }
+ }
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:53:19 +0000