summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaAig.c77
-rw-r--r--src/aig/gia/giaAig.h2
-rw-r--r--src/aig/gia/giaCSat.c8
-rw-r--r--src/aig/gia/giaDup.c41
5 files changed, 128 insertions, 1 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2d633d5c..571a6ef8 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -513,6 +513,7 @@ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index a4f1ab44..4b3692e4 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -105,6 +105,46 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Duplicates AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Gia_ManStart( Aig_ManObjNum(p) );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsAnd(pObj) )
+ pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+ else if ( Aig_ObjIsPi(pObj) )
+ pObj->iData = Gia_ManAppendCi( pNew );
+ else if ( Aig_ObjIsPo(pObj) )
+ pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+ else if ( Aig_ObjIsConst1(pObj) )
+ pObj->iData = 1;
+ else
+ assert( 0 );
+ }
+ Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+ if ( pNew->pNexts )
+ Gia_ManDeriveReprs( pNew );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Handles choices as additional combinational outputs.]
Description []
@@ -243,6 +283,43 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
return pMan;
}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers representatives from pGia to pAig.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
+{
+ Aig_Obj_t * pObj;
+ Gia_Obj_t * pGiaObj, * pGiaRepr;
+ int i;
+ assert( p->pReprs == NULL );
+ assert( pGia->pReprs != NULL );
+ // move pointers from AIG to GIA
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
+ pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
+ pGiaObj->Value = i;
+ }
+ // set the pointers to the nodes in AIG
+ Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+ Gia_ManForEachObj( pGia, pGiaObj, i )
+ {
+ pGiaRepr = Gia_ObjReprObj( pGia, i );
+ if ( pGiaRepr == NULL )
+ continue;
+ Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) );
+ }
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 0c0ee598..507e5143 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -47,8 +47,10 @@
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
+extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
#ifdef __cplusplus
}
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index f53a3d33..e005dfc2 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -473,6 +473,8 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Vec_IntShrink( p->vLevReas, 3*iBound );
}
+int s_Counter = 0;
+
/**Function*************************************************************
Synopsis [Assigns the variables a value.]
@@ -498,6 +500,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
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 );
+ s_Counter++;
}
@@ -925,6 +928,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{
int RetValue = 0;
+ s_Counter = 0;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
@@ -941,6 +945,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) )
RetValue = -1;
+
+// printf( "%d ", s_Counter );
return RetValue;
}
@@ -1019,7 +1025,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
{
if ( Gia_ObjFaninC0(pRoot) )
{
- printf( "Constant 1 output of SRM!!!\n" );
+// printf( "Constant 1 output of SRM!!!\n" );
Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
Vec_StrPush( vStatus, 0 );
}
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 63748403..cde19a22 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -246,6 +246,47 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG while complementing the flops.]
+
+ Description [The array of initial state contains the init state
+ for each state bit of the flops in the design.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ {
+ pObj->Value = Gia_ManAppendCi( pNew );
+ if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
+ pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
+ pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
+ pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
+ }
+ }
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 21:58:46 +0000