From 5158acb113586d17895cc32e8d71e12c06705eb5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 27 Jan 2018 13:05:37 -0800 Subject: Experiments with circuit-based SAT. --- src/aig/gia/gia.c | 159 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) (limited to 'src/aig/gia/gia.c') diff --git a/src/aig/gia/gia.c b/src/aig/gia/gia.c index 4fb33a9b..8f18f69c 100644 --- a/src/aig/gia/gia.c +++ b/src/aig/gia/gia.c @@ -26,6 +26,43 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +typedef struct Slv_Man_t_ Slv_Man_t; +struct Slv_Man_t_ +{ + Vec_Int_t vCis; + Vec_Int_t vCos; + Vec_Int_t vFanins; + Vec_Int_t vFanoutN; + Vec_Int_t vFanout0; + Vec_Str_t vValues; + Vec_Int_t vCopies; +}; + +static inline int Slv_ManObjNum ( Slv_Man_t * p ) { return Vec_IntSize(&p->vFanins)/2; } + +static inline int Slv_ObjFaninLit ( Slv_Man_t * p, int iObj, int f ) { return Vec_IntEntry(&p->vFanins, Abc_Var2Lit(iObj, f)); } +static inline int Slv_ObjFanin ( Slv_Man_t * p, int iObj, int f ) { return Abc_Lit2Var(Slv_ObjFaninLit(p, iObj, f)); } +static inline int Slv_ObjFaninC ( Slv_Man_t * p, int iObj, int f ) { return Abc_LitIsCompl(Slv_ObjFaninLit(p, iObj, f)); } + +static inline int Slv_ObjIsCi ( Slv_Man_t * p, int iObj ) { return !Slv_ObjFaninLit(p, iObj, 0) && Slv_ObjFaninLit(p, iObj, 1); } +static inline int Slv_ObjIsCo ( Slv_Man_t * p, int iObj ) { return Slv_ObjFaninLit(p, iObj, 0) && !Slv_ObjFaninLit(p, iObj, 1); } +static inline int Slv_ObjIsAnd ( Slv_Man_t * p, int iObj ) { return Slv_ObjFaninLit(p, iObj, 0) && Slv_ObjFaninLit(p, iObj, 1); } + +static inline int Slv_ObjFanout0 ( Slv_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vFanout0, iObj); } +static inline void Slv_ObjSetFanout0 ( Slv_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vFanout0, iObj, iLit); } + +static inline int Slv_ObjNextFanout ( Slv_Man_t * p, int iLit ) { return Vec_IntEntry(&p->vFanoutN, iLit); } +static inline void Slv_ObjSetNextFanout( Slv_Man_t * p, int iLit, int iLitF ) { Vec_IntWriteEntry(&p->vFanoutN, iLit, iLitF); } + +static inline int Slv_ObjCopyLit ( Slv_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); } +static inline void Slv_ObjSetCopyLit ( Slv_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); } + +#define Slv_ManForEachObj( p, iObj ) \ + for ( iObj = 1; iObj < Slv_ManObjNum(p); iObj++ ) + +#define Slv_ObjForEachFanout( p, iObj, iFanLit ) \ + for ( iFanLit = Slv_ObjFanout0(p, iObj); iFanLit; iFanLit = Slv_ObjNextFanout(p, iFanLit) ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -42,6 +79,128 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +Slv_Man_t * Slv_ManAlloc( int nObjs ) +{ + Slv_Man_t * p = ABC_CALLOC( Slv_Man_t, 1 ); + Vec_IntGrow( &p->vCis, 100 ); + Vec_IntGrow( &p->vCos, 100 ); + Vec_IntGrow( &p->vFanins, 2*nObjs ); + Vec_IntGrow( &p->vFanoutN, 2*nObjs ); + Vec_IntGrow( &p->vFanout0, nObjs ); + Vec_StrGrow( &p->vValues, nObjs ); + // constant node + Vec_IntFill( &p->vFanins, 2, 0 ); + Vec_IntFill( &p->vFanoutN, 2, 0 ); + Vec_IntFill( &p->vFanout0, 1, 0 ); + return p; +} +void Slv_ManFree( Slv_Man_t * p ) +{ + Vec_IntErase( &p->vCis ); + Vec_IntErase( &p->vCos ); + Vec_IntErase( &p->vFanins ); + Vec_IntErase( &p->vFanoutN ); + Vec_IntErase( &p->vFanout0 ); + Vec_StrErase( &p->vValues ); + Vec_IntErase( &p->vCopies ); + ABC_FREE( p ); +} +void Slv_ManPrintFanouts( Slv_Man_t * p ) +{ + int iObj, iFanLit; + Slv_ManForEachObj( p, iObj ) + { + printf( "Fanouts of node %d: ", iObj ); + Slv_ObjForEachFanout( p, iObj, iFanLit ) + printf( "%d ", Abc_Lit2Var(iFanLit) ); + printf( "\n" ); + } +} +static inline int Slv_ManAppendObj( Slv_Man_t * p, int iLit0, int iLit1 ) +{ + int iObj = Slv_ManObjNum(p); + Vec_StrPush( &p->vValues, 0 ); + Vec_IntPush( &p->vFanout0, 0 ); + Vec_IntPushTwo( &p->vFanoutN, 0, 0 ); + if ( !iLit0 ) // primary input + assert(!iLit1), iLit1 = Vec_IntSize(&p->vCis)+1, Vec_IntPush(&p->vCis, iObj); + else if ( !iLit1 ) // primary output + assert(iLit0), Vec_IntPush(&p->vCos, iObj); + else + { + Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 0), Slv_ObjFanout0(p, Abc_Lit2Var(iLit0)) ); + Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 1), Slv_ObjFanout0(p, Abc_Lit2Var(iLit1)) ); + Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit0), Abc_Var2Lit(iObj, 0) ); + Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit1), Abc_Var2Lit(iObj, 1) ); + } + Vec_IntPushTwo( &p->vFanins, iLit0, iLit1 ); + return Abc_Var2Lit( iObj, 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Slv_Man_t * Slv_ManFromGia( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int i; + Slv_Man_t * pNew = Slv_ManAlloc( Gia_ManObjNum(p) ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)) ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), 0 ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Slv_ManAppendObj( pNew, 0, 0 ); + else + assert( 0 ); + } + assert( Gia_ManObjNum(p) == Slv_ManObjNum(pNew) ); + return pNew; +} +Gia_Man_t * Slv_ManToGia( Slv_Man_t * p ) +{ + int iObj; + Gia_Man_t * pNew = Gia_ManStart( Slv_ManObjNum(p) ); + Vec_IntFill( &p->vCopies, Slv_ManObjNum(p), 0 ); + Slv_ManForEachObj( p, iObj ) + if ( Slv_ObjIsCi(p, iObj) ) + Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCi(pNew) ); + else if ( Slv_ObjIsCo(p, iObj) ) + { + int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) ); + Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCo(pNew, iLit0) ); + } + else if ( Slv_ObjIsAnd(p, iObj) ) + { + int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) ); + int iLit1 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 1)), Slv_ObjFaninC(p, iObj, 1) ); + Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendAnd(pNew, iLit0, iLit1) ); + } + else assert(0); + assert( Gia_ManObjNum(pNew) == Slv_ManObjNum(p) ); + return pNew; +} + +Gia_Man_t * Slv_ManToAig( Gia_Man_t * pGia ) +{ + Slv_Man_t * p = Slv_ManFromGia( pGia ); + Gia_Man_t * pNew = Slv_ManToGia( p ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + Slv_ManPrintFanouts( p ); + Slv_ManFree( p ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3