summaryrefslogtreecommitdiffstats
path: root/src/aig/cec/cecMan.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec/cecMan.c')
-rw-r--r--src/aig/cec/cecMan.c174
1 files changed, 114 insertions, 60 deletions
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index b8ee75b2..1a94409f 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -30,7 +30,7 @@
/**Function*************************************************************
- Synopsis [Creates AIG.]
+ Synopsis [Creates the manager.]
Description []
@@ -39,26 +39,25 @@
SeeAlso []
***********************************************************************/
-Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t * pPars )
-{
- Cec_ManCsw_t * p;
- p = ABC_ALLOC( Cec_ManCsw_t, 1 );
- memset( p, 0, sizeof(Cec_ManCsw_t) );
- p->pAig = pAig;
- p->pPars = pPars;
- p->pObjs = ABC_CALLOC( Cec_ObjCsw_t, Gia_ManObjNum(pAig) );
- // temporaries
- p->vClassOld = Vec_IntAlloc( 1000 );
- p->vClassNew = Vec_IntAlloc( 1000 );
- p->vClassTemp = Vec_IntAlloc( 1000 );
- p->vRefinedC = Vec_IntAlloc( 10000 );
- p->vXorNodes = Vec_IntAlloc( 1000 );
+Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+{
+ Cec_ManSat_t * p;
+ // create interpolation manager
+ p = ABC_ALLOC( Cec_ManSat_t, 1 );
+ memset( p, 0, sizeof(Cec_ManSat_t) );
+ p->pPars = pPars;
+ p->pAig = pAig;
+ // SAT solving
+ p->nSatVars = 1;
+ p->pSatVars = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
+ p->vUsedNodes = Vec_PtrAlloc( 1000 );
+ p->vFanins = Vec_PtrAlloc( 100 );
return p;
}
/**Function*************************************************************
- Synopsis [Deletes AIG.]
+ Synopsis [Prints statistics of the manager.]
Description []
@@ -67,19 +66,46 @@ Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t * pPars )
SeeAlso []
***********************************************************************/
-void Cec_ManCswStop( Cec_ManCsw_t * p )
+void Cec_ManSatPrintStats( Cec_ManSat_t * p )
{
- Vec_IntFree( p->vXorNodes );
- Vec_IntFree( p->vClassOld );
- Vec_IntFree( p->vClassNew );
- Vec_IntFree( p->vClassTemp );
- Vec_IntFree( p->vRefinedC );
- ABC_FREE( p->pMems );
- ABC_FREE( p->pObjs );
+ printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
+ printf( "Conf = %5d ", p->pPars->nBTLimit );
+ printf( "MinVar = %5d ", p->pPars->nSatVarMax );
+ printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
+ 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 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSatStop( Cec_ManSat_t * p )
+{
+ if ( p->pSat )
+ sat_solver_delete( p->pSat );
+ Vec_PtrFree( p->vUsedNodes );
+ Vec_PtrFree( p->vFanins );
+ ABC_FREE( p->pSatVars );
ABC_FREE( p );
}
+
/**Function*************************************************************
Synopsis [Creates AIG.]
@@ -147,9 +173,11 @@ void Cec_ManPatStop( Cec_ManPat_t * p )
ABC_FREE( p );
}
+
+
/**Function*************************************************************
- Synopsis [Creates the manager.]
+ Synopsis [Creates AIG.]
Description []
@@ -158,25 +186,31 @@ void Cec_ManPatStop( Cec_ManPat_t * p )
SeeAlso []
***********************************************************************/
-Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
-{
- Cec_ManSat_t * p;
- // create interpolation manager
- p = ABC_ALLOC( Cec_ManSat_t, 1 );
- memset( p, 0, sizeof(Cec_ManSat_t) );
- p->pPars = pPars;
- p->pAig = pAig;
- // SAT solving
- p->nSatVars = 1;
- p->pSatVars = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
- p->vUsedNodes = Vec_PtrAlloc( 1000 );
- p->vFanins = Vec_PtrAlloc( 100 );
+Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+{
+ Cec_ManSim_t * p;
+ p = ABC_ALLOC( Cec_ManSim_t, 1 );
+ memset( p, 0, sizeof(Cec_ManSim_t) );
+ p->pAig = pAig;
+ p->pPars = pPars;
+ p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
+ p->vClassOld = Vec_IntAlloc( 1000 );
+ p->vClassNew = Vec_IntAlloc( 1000 );
+ p->vClassTemp = Vec_IntAlloc( 1000 );
+ p->vRefinedC = Vec_IntAlloc( 10000 );
+ p->vCiSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(p->pAig), pPars->nWords );
+ if ( pPars->fCheckMiter || Gia_ManRegNum(p->pAig) )
+ {
+ p->vCoSimInfo = Vec_PtrAllocSimInfo( Gia_ManCoNum(p->pAig), pPars->nWords );
+ Vec_PtrCleanSimInfo( p->vCoSimInfo, 0, pPars->nWords );
+ }
+ p->iOut = -1;
return p;
}
/**Function*************************************************************
- Synopsis [Prints statistics of the manager.]
+ Synopsis [Deletes AIG.]
Description []
@@ -185,26 +219,27 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
SeeAlso []
***********************************************************************/
-void Cec_ManSatPrintStats( Cec_ManSat_t * p )
+void Cec_ManSimStop( Cec_ManSim_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
- printf( "Conf = %5d ", p->pPars->nBTLimit );
- printf( "MinVar = %5d ", p->pPars->nSatVarMax );
- printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
- 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 );
+ Vec_IntFree( p->vClassOld );
+ Vec_IntFree( p->vClassNew );
+ Vec_IntFree( p->vClassTemp );
+ Vec_IntFree( p->vRefinedC );
+ if ( p->vCiSimInfo )
+ Vec_PtrFree( p->vCiSimInfo );
+ if ( p->vCoSimInfo )
+ Vec_PtrFree( p->vCoSimInfo );
+ ABC_FREE( p->pCexComb );
+ ABC_FREE( p->pCexes );
+ ABC_FREE( p->pMems );
+ ABC_FREE( p->pSimInfo );
+ ABC_FREE( p );
}
+
/**Function*************************************************************
- Synopsis [Frees the manager.]
+ Synopsis [Creates AIG.]
Description []
@@ -213,16 +248,35 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
SeeAlso []
***********************************************************************/
-void Cec_ManSatStop( Cec_ManSat_t * p )
+Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
+{
+ Cec_ManFra_t * p;
+ p = ABC_ALLOC( Cec_ManFra_t, 1 );
+ memset( p, 0, sizeof(Cec_ManFra_t) );
+ p->pAig = pAig;
+ p->pPars = pPars;
+ p->vXorNodes = Vec_IntAlloc( 1000 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deletes AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManFraStop( Cec_ManFra_t * p )
{
- if ( p->pSat )
- sat_solver_delete( p->pSat );
- Vec_PtrFree( p->vUsedNodes );
- Vec_PtrFree( p->vFanins );
- ABC_FREE( p->pSatVars );
+ Vec_IntFree( p->vXorNodes );
ABC_FREE( p );
}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-25 07:50:14 +0000