summaryrefslogtreecommitdiffstats
path: root/src/proof/llb/llb1Group.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/llb/llb1Group.c')
-rw-r--r--src/proof/llb/llb1Group.c474
1 files changed, 0 insertions, 474 deletions
diff --git a/src/proof/llb/llb1Group.c b/src/proof/llb/llb1Group.c
deleted file mode 100644
index 1099b2cd..00000000
--- a/src/proof/llb/llb1Group.c
+++ /dev/null
@@ -1,474 +0,0 @@
-/**CFile****************************************************************
-
- FileName [llb1Group.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [BDD based reachability.]
-
- Synopsis [Initial partition computation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: llb1Group.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "llbInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan )
-{
- Llb_Grp_t * p;
- p = ABC_CALLOC( Llb_Grp_t, 1 );
- p->pMan = pMan;
- p->vIns = Vec_PtrAlloc( 8 );
- p->vOuts = Vec_PtrAlloc( 8 );
- p->Id = Vec_PtrSize( pMan->vGroups );
- Vec_PtrPush( pMan->vGroups, p );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManGroupStop( Llb_Grp_t * p )
-{
- if ( p == NULL )
- return;
- Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
- Vec_PtrFreeP( &p->vIns );
- Vec_PtrFreeP( &p->vOuts );
- Vec_PtrFreeP( &p->vNodes );
- ABC_FREE( p );
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
- if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(pAig, pObj);
- if ( Aig_ObjIsConst1(pObj) )
- return;
- if ( Aig_ObjIsCo(pObj) )
- {
- Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
- return;
- }
- assert( Aig_ObjIsAnd(pObj) );
- Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
- Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes );
- Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the support of MFFC.]
-
- Description [Returns the number of internal nodes in the MFFC.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Llb_ManGroupCollect( Llb_Grp_t * pGroup )
-{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj;
- int i;
- vNodes = Vec_PtrAlloc( 100 );
- Aig_ManIncrementTravId( pGroup->pMan->pAig );
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
- Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj );
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
- Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj );
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
- Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes );
- return vNodes;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
-{
- if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(pAig, pObj);
- if ( Aig_ObjIsConst1(pObj) )
- return;
- if ( pObj->fMarkA )
- {
- Vec_PtrPush( vSupp, pObj );
- return;
- }
- assert( Aig_ObjIsAnd(pObj) );
- Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp );
- Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
-{
- Llb_Grp_t * p;
- assert( pObj->fMarkA == 1 );
- // derive group
- p = Llb_ManGroupAlloc( pMan );
- Vec_PtrPush( p->vOuts, pObj );
- Aig_ManIncrementTravId( pMan->pAig );
- if ( Aig_ObjIsCo(pObj) )
- Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
- else
- {
- Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
- Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns );
- }
- // derive internal objects
- assert( p->vNodes == NULL );
- p->vNodes = Llb_ManGroupCollect( p );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupCreateFirst( Llb_Man_t * pMan )
-{
- Llb_Grp_t * p;
- Aig_Obj_t * pObj;
- int i;
- p = Llb_ManGroupAlloc( pMan );
- Saig_ManForEachLo( pMan->pAig, pObj, i )
- Vec_PtrPush( p->vOuts, pObj );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupCreateLast( Llb_Man_t * pMan )
-{
- Llb_Grp_t * p;
- Aig_Obj_t * pObj;
- int i;
- p = Llb_ManGroupAlloc( pMan );
- Saig_ManForEachLi( pMan->pAig, pObj, i )
- Vec_PtrPush( p->vIns, pObj );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 )
-{
- Llb_Grp_t * p;
- Aig_Obj_t * pObj;
- int i;
- p = Llb_ManGroupAlloc( p1->pMan );
- // create inputs
- Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
- Vec_PtrPush( p->vIns, pObj );
- Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
- Vec_PtrPushUnique( p->vIns, pObj );
- // create outputs
- Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
- Vec_PtrPush( p->vOuts, pObj );
- Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
- Vec_PtrPushUnique( p->vOuts, pObj );
-
- // derive internal objects
- assert( p->vNodes == NULL );
- p->vNodes = Llb_ManGroupCollect( p );
- return p;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManGroupMarkNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- return;
- if ( Aig_ObjIsTravIdPrevious(p, pObj) )
- {
- Aig_ObjSetTravIdCurrent(p, pObj);
- return;
- }
- Aig_ObjSetTravIdCurrent(p, pObj);
- assert( Aig_ObjIsNode(pObj) );
- Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin0(pObj) );
- Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin1(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates group from two cuts derived by the flow computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
-{
- Llb_Grp_t * p;
- Aig_Obj_t * pObj;
- int i;
- p = Llb_ManGroupAlloc( pMan );
-
- // mark Cut1
- Aig_ManIncrementTravId( pMan->pAig );
- Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
- Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
- // collect unmarked Cut2
- Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
- if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
- Vec_PtrPush( p->vOuts, pObj );
-
- // mark nodes reachable from Cut2
- Aig_ManIncrementTravId( pMan->pAig );
- Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
- Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
- // collect marked Cut1
- Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
- if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
- Vec_PtrPush( p->vIns, pObj );
-
- // derive internal objects
- assert( p->vNodes == NULL );
- p->vNodes = Llb_ManGroupCollect( p );
- return p;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManPrepareGroups( Llb_Man_t * pMan )
-{
- Aig_Obj_t * pObj;
- int i;
- assert( pMan->vGroups == NULL );
- pMan->vGroups = Vec_PtrAlloc( 1000 );
- Llb_ManGroupCreateFirst( pMan );
- Aig_ManForEachNode( pMan->pAig, pObj, i )
- {
- if ( pObj->fMarkA )
- Llb_ManGroupCreate( pMan, pObj );
- }
- Saig_ManForEachLi( pMan->pAig, pObj, i )
- {
- if ( pObj->fMarkA )
- Llb_ManGroupCreate( pMan, pObj );
- }
- Llb_ManGroupCreateLast( pMan );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManPrintSpan( Llb_Man_t * p )
-{
- Llb_Grp_t * pGroup;
- Aig_Obj_t * pVar;
- int i, k, Span = 0, SpanMax = 0;
- Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
- {
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
- if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
- Span++;
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
- if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
- Span++;
-
- SpanMax = Abc_MaxInt( SpanMax, Span );
-printf( "%d ", Span );
-
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
- if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
- Span--;
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
- if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
- Span--;
- }
-printf( "\n" );
-printf( "Max = %d\n", SpanMax );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar )
-{
- Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup );
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
- if ( pObj->Id == iVar )
- return 1;
- Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
- if ( pObj->Id == iVar )
- return 1;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Llb_ManPrintHisto( Llb_Man_t * p )
-{
- Aig_Obj_t * pObj;
- int i, k;
- Aig_ManForEachObj( p->pAig, pObj, i )
- {
- if ( Vec_IntEntry(p->vObj2Var, i) < 0 )
- continue;
- printf( "%3d :", i );
- for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ )
- printf( " " );
- for ( ; k <= Vec_IntEntry(p->vVarEnds, i); k++ )
- printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' );
- printf( "\n" );
- }
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-11 17:19:48 +0000