From 5838789ee7d7e1b9bbfdf091e33f6749a9b1286f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Jul 2012 12:34:59 -0700 Subject: Scalable gate-level abstraction. --- src/aig/gia/gia.h | 2 + src/aig/gia/giaAbsGla2.c | 529 ++++++++++++++++++----------------------------- src/aig/gia/giaMan.c | 1 + src/base/abci/abc.c | 19 +- 4 files changed, 221 insertions(+), 330 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b3a8fdc1..6abda070 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -128,6 +128,7 @@ struct Gia_Man_t_ Vec_Int_t * vFanoutNums; // static fanout Vec_Int_t * vFanout; // static fanout int * pMapping; // mapping for each node + Vec_Int_t * vMapping; Vec_Int_t * vLutConfigs; // LUT configurations Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexSeq; // sequential counter-example @@ -718,6 +719,7 @@ extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); /*=== giaAbsGla.c ===========================================================*/ extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta ); +extern int Ga2_ManPerform( Gia_Man_t * p, Gia_ParVta_t * pPars ); /*=== giaAbsVta.c ===========================================================*/ extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ); extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index d883340d..7edacf3c 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -38,31 +38,30 @@ typedef struct Ga2_Man_t_ Ga2_Man_t; // manager struct Ga2_Man_t_ { // user data - Gia_Man_t * pGia; // working AIG manager - Gia_ParVta_t * pPars; // parameters + Gia_Man_t * pGia; // working AIG manager + Gia_ParVta_t * pPars; // parameters // markings - int nMarked; // total number of marked nodes and flops - Vec_Int_t * vMapping; // for each object: leaf count, leaves, truth table - Vec_Ptr_t * vDatas; // for each object: leaves, CNF0, CNF1 + int nMarked; // total number of marked nodes and flops + Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1 // abstraction - Vec_Int_t * vAbs; // array of abstracted objects - Vec_Int_t * vValues; // array of objects with SAT numbers assigned - int LimAbs; // limit value for starting abstraction objects - int LimPpi; // limit value for starting PPI objects + Vec_Int_t * vIds; // abstraction ID for each object + Vec_Int_t * vAbs; // array of abstracted objects + Vec_Int_t * vValues; // array of objects with SAT numbers assigned + int LimAbs; // limit value for starting abstraction objects + int LimPpi; // limit value for starting PPI objects // refinement - Rnm_Man_t * pRnm; // refinement manager + Rnm_Man_t * pRnm; // refinement manager // SAT solver and variables - Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal - sat_solver2 * pSat; // incremental SAT solver - int nSatVars; // the number of SAT variables - int nProofIds; // the counter of proof IDs + Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal + sat_solver2 * pSat; // incremental SAT solver + int nSatVars; // the number of SAT variables + int nProofIds; // the counter of proof IDs // temporaries - Vec_Int_t * vCnf; Vec_Int_t * vLits; Vec_Int_t * vIsopMem; - char * pSopSizes, ** pSops; // CNF representation - int nCexes; // the number of counter-examples - int nObjAdded; // objs added during refinement + char * pSopSizes, ** pSops; // CNF representation + int nCexes; // the number of counter-examples + int nObjAdded; // objs added during refinement // statistics clock_t timeStart; clock_t timeInit; @@ -72,38 +71,39 @@ struct Ga2_Man_t_ clock_t timeOther; }; -static inline int Ga2_ObjOffset( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_IntEntry(p->vMapping, Gia_ObjId(p->pGia, pObj)); } -static inline int Ga2_ObjLeaveNum( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } -static inline int * Ga2_ObjLeavePtr( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } -static inline unsigned Ga2_ObjTruth( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } -static inline int Ga2_ObjRefNum( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } -static inline Vec_Int_t * Ga2_ObjLeaves( Ga2_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t vVec; vVec.nSize = Ga2_ObjLeaveNum(p, pObj), vVec.pArray = Ga2_ObjLeavePtr(p, pObj); return &vVec; } +static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } +static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } +static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } +static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } +static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } +static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } -static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_PtrEntry(p->vDatas, (pObj->Value << 1) ); } -static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_PtrEntry(p->vDatas, (pObj->Value << 1)+1); } +static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); } +static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); } -static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert( pObj->Value ); return (int)pObj->Value < p->LimAbs; } -static inline int Ga2_ObjIsPPI( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert( pObj->Value ); return (int)pObj->Value >= p->LimAbs && (int)pObj->Value < p->LimPpi; } +static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1) ); } +static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry(p->vCnfs, (Ga2_ObjId(p,pObj) << 1)+1); } -static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); } +static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) < p->LimAbs; } +static inline int Ga2_ObjIsPpi( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; } +static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); } // returns literal of this object, or -1 if SAT variable of the object is not assigned static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { - assert( pObj->fPhase ); - assert( pObj->Value && pObj->Value < Vec_IntSize(p->vValues) ); + assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) ); if ( f == Vec_PtrSize(p->vId2Lit) ) Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) ); assert( f < Vec_PtrSize(p->vId2Lit) ); - return Vec_IntEntry( Ga2_MapFrameMap(p, f), pObj->Value ); + return Vec_IntEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj) ); } // inserts literal of this object static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit ) { assert( Lit > 1 ); assert( Ga2_ObjFindLit(p, pObj, f) == -1 ); - Vec_IntSetEntry( Ga2_MapFrameMap(p, f), pObj->Value, Lit ); + Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit ); } // returns or inserts-and-returns literal of this object static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) @@ -118,7 +118,6 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) return Lit; } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -147,21 +146,11 @@ unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst ) unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves ) { static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; - unsigned Res, Values[5]; Gia_Obj_t * pObj; int i; - // assign elementary truth tables Gia_ManForEachObjVec( vLeaves, p, pObj, i ) - { - assert( pObj->fPhase ); - Values[i] = pObj->Value; pObj->Value = uTruth5[i]; - } - Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); - // return values - Gia_ManForEachObjVec( vLeaves, p, pObj, i ) - pObj->Value = Values[i]; - return Res; + return Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); } /**Function************************************************************* @@ -243,11 +232,10 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 ); Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 ); } -int Ga2_ManMarkup( Gia_Man_t * p, int N, Vec_Int_t ** pvMap ) +int Ga2_ManMarkup( Gia_Man_t * p, int N ) { static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; clock_t clk = clock(); - Vec_Int_t * vMap; Vec_Int_t * vLeaves; Gia_Obj_t * pObj; int i, k, Leaf, CountMarks; @@ -289,7 +277,8 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, Vec_Int_t ** pvMap ) } // verify that the tree is split correctly CountMarks = 0; - vMap = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_IntFreeP( &p->vMapping ); + p->vMapping = Vec_IntStart( Gia_ManObjNum(p) ); Gia_ManForEachAnd( p, pObj, i ) { if ( !pObj->fPhase ) @@ -299,18 +288,18 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, Vec_Int_t ** pvMap ) // printf( "%d ", Vec_IntSize(vLeaves) ); assert( Vec_IntSize(vLeaves) <= N ); // create map - Vec_IntWriteEntry( vMap, i, Vec_IntSize(vMap) ); - Vec_IntPush( vMap, Vec_IntSize(vLeaves) ); + Vec_IntWriteEntry( p->vMapping, i, Vec_IntSize(p->vMapping) ); + Vec_IntPush( p->vMapping, Vec_IntSize(vLeaves) ); Vec_IntForEachEntry( vLeaves, Leaf, k ) - { - Vec_IntPush( vMap, Leaf ); + { + Vec_IntPush( p->vMapping, Leaf ); Gia_ManObj(p, Leaf)->Value = uTruth5[k]; + assert( Gia_ManObj(p, Leaf)->fPhase ); } - Vec_IntPush( vMap, (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) ); - Vec_IntPush( vMap, -1 ); // placeholder for ref counter + Vec_IntPush( p->vMapping, (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) ); + Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter CountMarks++; } - *pvMap = vMap; // printf( "Internal nodes = %d. ", CountMarks ); Abc_PrintTime( 1, "Time", clock() - clk ); Vec_IntFree( vLeaves ); @@ -319,22 +308,23 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, Vec_Int_t ** pvMap ) void Ga2_ManComputeTest( Gia_Man_t * p ) { clock_t clk; - Vec_Int_t * vLeaves, * vMap; +// unsigned uTruth; Gia_Obj_t * pObj; - int i; - Ga2_ManMarkup( p, 5, &vMap ); + int i, Counter = 0; clk = clock(); - vLeaves = Vec_IntAlloc( 100 ); + Ga2_ManMarkup( p, 5 ); + Abc_PrintTime( 1, "Time", clock() - clk ); Gia_ManForEachAnd( p, pObj, i ) { if ( !pObj->fPhase ) continue; - Vec_IntClear( vLeaves ); - Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 ); - Ga2_ManComputeTruth( p, pObj, vLeaves ); +// uTruth = Ga2_ObjTruth( p, pObj ); +// printf( "%6d : ", Counter ); +// Kit_DsdPrintFromTruth( &uTruth, Ga2_ObjLeaveNum(p, pObj) ); +// printf( "\n" ); + Counter++; } - Vec_IntFree( vLeaves ); - Vec_IntFree( vMap ); + printf( "Marked AND nodes = %6d. ", Counter ); Abc_PrintTime( 1, "Time", clock() - clk ); } @@ -355,57 +345,69 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p = ABC_CALLOC( Ga2_Man_t, 1 ); p->timeStart = clock(); // user data - p->pGia = pGia; - p->pPars = pPars; + p->pGia = pGia; + p->pPars = pPars; // markings - p->nMarked = Gia_ManRegNum(p->pGia) + Ga2_ManMarkup( pGia, 5, &p->vMapping ); - p->vDatas = Vec_PtrAlloc( 1000 ); - Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) ); - Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) ); + p->nMarked = Ga2_ManMarkup( pGia, 5 ) + Gia_ManRegNum( p->pGia ); + p->vCnfs = Vec_PtrAlloc( 1000 ); + Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) ); + Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) ); // abstraction - p->vAbs = Vec_IntAlloc( 1000 ); - p->vValues = Vec_IntAlloc( 1000 ); + p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) ); + p->vAbs = Vec_IntAlloc( 1000 ); + p->vValues = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vValues, -1 ); // refinement - p->pRnm = Rnm_ManStart( pGia ); + p->pRnm = Rnm_ManStart( pGia ); // SAT solver and variables - p->vId2Lit = Vec_PtrAlloc( 1000 ); + p->vId2Lit = Vec_PtrAlloc( 1000 ); // temporaries - p->vCnf = Vec_IntAlloc( 100 ); - p->vLits = Vec_IntAlloc( 100 ); - p->vIsopMem = Vec_IntAlloc( 100 ); + p->vLits = Vec_IntAlloc( 100 ); + p->vIsopMem = Vec_IntAlloc( 100 ); Cnf_ReadMsops( &p->pSopSizes, &p->pSops ); - // prepare - Gia_ManCleanValue( pGia ); return p; } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ +void Ga2_ManReportMemory( Ga2_Man_t * p ) +{ + double memTot = 0; + double memAig = 1.0 * p->pGia->nObjsAlloc * sizeof(Gia_Obj_t) + Vec_IntMemory(p->pGia->vMapping); + double memSat = sat_solver2_memory( p->pSat, 1 ); + double memPro = sat_solver2_memory_proof( p->pSat ); + double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit ); + double memRef = Rnm_ManMemoryUsage( p->pRnm ); + double memOth = sizeof(Ga2_Man_t); + memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs ); + memOth += Vec_IntMemory( p->vIds ); + memOth += Vec_IntMemory( p->vAbs ); + memOth += Vec_IntMemory( p->vValues ); + memOth += Vec_IntMemory( p->vLits ); + memOth += Vec_IntMemory( p->vIsopMem ); + memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536; + memTot = memAig + memSat + memPro + memMap + memRef + memOth; + ABC_PRMP( "Memory: AIG ", memAig, memTot ); + ABC_PRMP( "Memory: SAT ", memSat, memTot ); + ABC_PRMP( "Memory: Proof ", memPro, memTot ); + ABC_PRMP( "Memory: Map ", memMap, memTot ); + ABC_PRMP( "Memory: Refine", memRef, memTot ); + ABC_PRMP( "Memory: Other ", memOth, memTot ); + ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); +} void Ga2_ManStop( Ga2_Man_t * p ) { + Vec_IntFreeP( &p->pGia->vMapping ); + Gia_ManSetPhase( p->pGia ); // if ( p->pPars->fVerbose ) Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); - Vec_IntFree( p->vMapping ); - Vec_VecFree( (Vec_Vec_t *)p->vDatas ); + if( p->pSat ) sat_solver2_delete( p->pSat ); + Vec_VecFree( (Vec_Vec_t *)p->vCnfs ); + Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); + Vec_IntFree( p->vIds ); Vec_IntFree( p->vAbs ); Vec_IntFree( p->vValues ); - Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); - Vec_IntFree( p->vCnf ); Vec_IntFree( p->vLits ); Vec_IntFree( p->vIsopMem ); Rnm_ManStop( p->pRnm, 1 ); - sat_solver2_delete( p->pSat ); ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); ABC_FREE( p->pSops ); @@ -415,10 +417,12 @@ void Ga2_ManStop( Ga2_Man_t * p ) /**Function************************************************************* - Synopsis [Computes and minimizes the truth table.] + Synopsis [Computes a minimized truth table.] - Description [Array of input literals may contain 0 (const0), 1 (const1) - or 2 (literal). Upon exit, it contains the variables in the support.] + Description [Input literals can be 0/1 (const 0/1), non-trivial literals + (integers that are more than 1) and unassigned literals (large integers). + This procedure computes the truth table that essentially depends on input + variables ordered in the increasing order of their positive literals.] SideEffects [] @@ -427,63 +431,65 @@ void Ga2_ManStop( Ga2_Man_t * p ) ***********************************************************************/ static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v ) { + static unsigned uInvTruth5[5] = { 0x55555555, 0x33333333, 0x0F0F0F0F, 0x00FF00FF, 0x0000FFFF }; assert( v >= 0 && v <= 4 ); - if ( v == 0 ) - return ((t ^ (t >> 1)) & 0x55555555); - if ( v == 1 ) - return ((t ^ (t >> 2)) & 0x33333333); - if ( v == 2 ) - return ((t ^ (t >> 4)) & 0x0F0F0F0F); - if ( v == 3 ) - return ((t ^ (t >> 8)) & 0x00FF00FF); - if ( v == 4 ) - return ((t ^ (t >>16)) & 0x0000FFFF); - return -1; + return ((t ^ (t >> (1 << v))) & uInvTruth5[v]); } unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits ) { static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; - unsigned Res, Values[5]; Gia_Obj_t * pObj; - int i, k, Entry; + int i, Entry; + unsigned Res; // assign elementary truth tables Gia_ManForEachObjVec( vLeaves, p, pObj, i ) { - assert( pObj->fPhase ); - Values[i] = pObj->Value; Entry = Vec_IntEntry( vLits, i ); - assert( Entry >= 0 && Entry <= 2 ); + assert( Entry >= 0 ); if ( Entry == 0 ) pObj->Value = 0; else if ( Entry == 1 ) pObj->Value = ~0; - else // if ( Entry == 2 ) + else // non-trivial literal pObj->Value = uTruth5[i]; } + // compute truth table Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); - Vec_IntClear( vLits ); if ( Res != 0 && Res != ~0 ) { - // check if truth table depends on them - // and create a new array of literals with essential-support variables - k = 0; + // find essential variables + int nUsed = 0, pUsed[5]; + for ( i = 0; i < Vec_IntSize(vLeaves); i++ ) + if ( Ga2_ObjTruthDepends( Res, i ) ) + pUsed[nUsed++] = i; + assert( nUsed > 0 ); + // order the by literal value + Vec_IntSelectSortCost( pUsed, nUsed, vLits ); + assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) ); + // assign elementary truth tables to the leaves Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + pObj->Value = 0; + for ( i = 0; i < nUsed; i++ ) { - if ( Ga2_ObjTruthDepends( Res, i ) ) - { - pObj->Value = uTruth5[k++]; - Vec_IntPush( vLits, i ); - } + Entry = Vec_IntEntry( vLits, pUsed[i] ); + assert( Entry > 1 ); + pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) ); + pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i]; + // remember this literal + pUsed[i] = Abc_LitRegular(Entry); } - // recompute the truth table + // compute truth table Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); - // verify that the truthe table depends on them - for ( i = 0; i < Vec_IntSize(vLeaves); i++ ) - assert( (i < Vec_IntSize(vLits)) == (Ga2_ObjTruthDepends(Res, i) > 0) ); + // reload the literals + Vec_IntClear( vLits ); + for ( i = 0; i < nUsed; i++ ) + { + Vec_IntPush( vLits, pUsed[i] ); + assert( Ga2_ObjTruthDepends(Res, i) ); + } } - // return values - Gia_ManForEachObjVec( vLeaves, p, pObj, i ) - pObj->Value = Values[i]; + else + Vec_IntClear( vLits ); return Res; } @@ -510,7 +516,6 @@ Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ) return Vec_IntDup( vCover ); } - /**Function************************************************************* Synopsis [Derives CNF for one node.] @@ -539,20 +544,18 @@ static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], Cube = p->pSops[uTruth][k]; for ( b = 3; b >= 0; b-- ) { - if ( Cube % 3 == 0 ) // value 0 --> write positive literal + if ( Cube % 3 == 0 ) // value 0 --> add positive literal { assert( Lits[b] > 1 ); ClaLits[nClaLits++] = Lits[b]; } - else if ( Cube % 3 == 1 ) // value 1 --> write negative literal + else if ( Cube % 3 == 1 ) // value 1 --> add negative literal { assert( Lits[b] > 1 ); ClaLits[nClaLits++] = lit_neg(Lits[b]); } Cube = Cube / 3; } -// if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) ) -// assert( 0 ); sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } @@ -575,13 +578,13 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In for ( b = 0; b < 5; b++ ) { Literal = 3 & (Cube >> (b << 1)); - if ( Literal == 1 ) // value 0 --> write positive literal + if ( Literal == 1 ) // value 0 --> add positive literal { // pCube[b] = '0'; assert( Lits[b] > 1 ); ClaLits[nClaLits++] = Lits[b]; } - else if ( Literal == 2 ) // value 1 --> write negative literal + else if ( Literal == 2 ) // value 1 --> add negative literal { // pCube[b] = '1'; assert( Lits[b] > 1 ); @@ -590,8 +593,6 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In else if ( Literal != 0 ) assert( 0 ); } -// if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) ) -// assert( 0 ); sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } @@ -614,25 +615,25 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) unsigned uTruth; int nLeaves; assert( pObj->fPhase ); - assert( Vec_PtrSize(p->vDatas) == 2 * Vec_IntSize(p->vValues) ); - // assign value to the node - if ( pObj->Value == 0 ) + assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) ); + // assign abstraction ID to the node + if ( Ga2_ObjId(p,pObj) == 0 ) { - pObj->Value = Vec_IntSize(p->vValues); + Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) ); Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) ); - Vec_PtrPush( p->vDatas, NULL ); - Vec_PtrPush( p->vDatas, NULL ); + Vec_PtrPush( p->vCnfs, NULL ); + Vec_PtrPush( p->vCnfs, NULL ); } assert( Ga2_ObjCnf0(p, pObj) == NULL ); if ( !fAbs ) return; // compute parameters - nLeaves = Ga2_ObjLeaveNum(p, pObj); - uTruth = Ga2_ObjTruth( p, pObj ); + nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj); + uTruth = Ga2_ObjTruth( p->pGia, pObj ); // create CNF for pos/neg phases - Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) ); - Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) ); } void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) @@ -649,8 +650,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) // add PPI objects Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k, ) + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Ga2_ManSetupNode( p, pObj, 0 ); } // clean mapping in the timeframes @@ -661,9 +662,9 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) { iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); - vLeaves = Ga2_ObjLeaves( p, pObj ); + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Vec_IntClear( p->vLits ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k, ) + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, p->nProofIds + i ); } @@ -679,9 +680,9 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) if ( i < p->LimAbs ) continue; iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); - vLeaves = Ga2_ObjLeaves( p, pObj ); + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); Vec_IntClear( p->vLits ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k, ) + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) ); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, i - p->LimAbs ); } @@ -703,25 +704,25 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues ) continue; Vec_IntFree( Ga2_ObjCnf0(p, pObj) ); Vec_IntFree( Ga2_ObjCnf1(p, pObj) ); - Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value, NULL ); - Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value + 1, NULL ); + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), NULL ); + Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, NULL ); } Vec_IntShrink( p->vAbs, nAbs ); // shrink values Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) { - assert( pObj->Value ); + assert( Ga2_ObjId(p,pObj) ); if ( i < nValues ) continue; - pObj->Value = 0; + Ga2_ObjSetId( p, pObj, 0 ); } Vec_IntShrink( p->vValues, nValues ); + Vec_PtrShrink( p->vCnfs, 2 * nValues ); // clean mapping into timeframes Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) Vec_IntShrink( vMap, nValues ); } - /**Function************************************************************* Synopsis [] @@ -742,6 +743,7 @@ void Ga2_ManAbsTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClas Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 ); Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 ); } + Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) { Vec_Int_t * vGateClasses; @@ -752,34 +754,26 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 ); return vGateClasses; } + Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p ) { Vec_Int_t * vToAdd; Gia_Obj_t * pObj; int i; vToAdd = Vec_IntAlloc( 1000 ); - Gia_ManForEachObj( p, pObj, i ) + Gia_ManForEachRo( p, pObj, i ) + if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) + Vec_IntPush( vToAdd, i ); + Gia_ManForEachAnd( p, pObj, i ) if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) ) Vec_IntPush( vToAdd, i ); return vToAdd; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ void Ga2_ManRestart( Ga2_Man_t * p ) { Vec_Int_t * vToAdd; - assert( p->pGia != NULL ); - assert( p->pGia->vGateClasses != NULL ); + assert( p->pGia != NULL && p->pGia->vGateClasses != NULL ); assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set // clear mappings from objects Ga2_ManShrinkAbs( p, 0, 1 ); @@ -814,7 +808,6 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { int fSimple = 1; unsigned uTruth; - Vec_Int_t * vLeaves; Gia_Obj_t * pLeaf; int nLeaves, * pLeaves; int i, Lit, pLits[5]; @@ -826,12 +819,13 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { Lit = Ga2_ObjFindOrAddLit( p, pObj, f ); Lit = Abc_LitNot(Lit); - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); assert( Lit > 1 ); + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); return Lit; } return 0; } + assert( pObj->fPhase ); Lit = Ga2_ObjFindLit( p, pObj, f ); if ( Lit >= 0 ) return Lit; @@ -844,12 +838,16 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Ga2_ObjAddLit( p, pObj, f, Lit ); return Lit; } + nLeaves = Ga2_ObjLeaveNum( p->pGia, pObj ); + pLeaves = Ga2_ObjLeavePtr( p->pGia, pObj ); if ( fSimple ) { // collect fanin literals - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i ) + for ( i = 0; i < nLeaves; i++ ) + { + pLeaf = Gia_ManObj(p->pGia, pLeaves[i]); pLits[i] = Ga2_ManUnroll_rec( p, pLeaf, f ); + } // create fanout literal Lit = Ga2_ObjFindOrAddLit( p, pObj, f ); // create clauses @@ -857,168 +855,44 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) return Lit; } // collect fanin literals - nLeaves = Ga2_ObjLeaveNum( p, pObj ); - pLeaves = Ga2_ObjLeavePtr( p, pObj ); for ( i = 0; i < nLeaves; i++ ) { pLeaf = Gia_ManObj( p->pGia, pLeaves[i] ); if ( Ga2_ObjIsAbs(p, pLeaf) ) // belongs to original abstraction pLits[i] = Ga2_ManUnroll_rec( p, pLeaf, f ); - else if ( Ga2_ObjIsPPI(p, pLeaf) ) // belongs to original PPIs + else if ( Ga2_ObjIsPpi(p, pLeaf) ) // belongs to original PPIs pLits[i] = GA2_BIG_NUM + i; - else - assert( 0 ); + else assert( 0 ); } // collect literals Vec_IntClear( p->vLits ); for ( i = 0; i < nLeaves; i++ ) Vec_IntPush( p->vLits, pLits[i] ); // minimize truth table - vLeaves = Ga2_ObjLeaves( p, pObj ); - uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); - if ( uTruth == 0 || uTruth == ~0 ) - Ga2_ObjAddLit( p, pObj, f, uTruth == 0 ? 3 : 2 ); // const 0 / 1 + uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, Ga2_ObjLeaves(p->pGia, pObj), p->vLits ); + if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1 + Lit = (uTruth > 0); else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter { Lit = Vec_IntEntry( p->vLits, 0 ); - pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); - Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); - Ga2_ObjAddLit( p, pObj, f, Abc_LitNotCond(Lit, uTruth == 0x55555555) ); - } - else - { - // replace numbers of literals by actual literals - Vec_IntForEachEntry( p->vLits, Lit, i ) + if ( Lit >= GA2_BIG_NUM ) { - pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); - Lit = Ga2_ObjFindOrAddLit(p, pLeaf, f); - Vec_IntWriteEntry( p->vLits, i, Lit ); - } - // add CNF - Lit = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, 0 ); - Ga2_ObjAddLit( p, pObj, f, Lit ); - } - return Lit; -} - -/**Function************************************************************* - - Synopsis [Unrolls one timeframe.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -/* -void Ga2_ManUnroll2( Ga2_Man_t * p, int f ) -{ - Gia_Obj_t * pObj, * pObjRi, * pLeaf; - Vec_Int_t * vLeaves; - unsigned uTruth; - int i, k, Lit, iLitOut, fFullTable; - // construct CNF for internal nodes - Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) - { - // assign RO literal values (no need to add clauses) - assert( pObj->fPhase && pObj->Value ); - if ( Gia_ObjIsConst0(pObj) ) - { - Ga2_ObjAddLit( p, pObj, f, 3 ); // const 0 - continue; - } - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - pObjRi = Gia_ObjRoToRi(p->pGia, pObj); - Lit = f ? Ga2_ObjFindOrAddLit( p, pObjRi, f-1 ) : 3; // const 0 - Ga2_ObjAddLit( p, pObj, f, Lit ); - continue; - } - assert( Gia_ObjIsAnd(pObj) ); - assert( pObj->Value > 0 ); - vLeaves = Ga2_ObjLeaves(p, pObj); - // for nodes recently added to abstraction, add CNF without const propagation - fFullTable = 1; - if ( i < p->nAbs ) - { - Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) - { - Lit = Ga2_ObjFindLit( p, pLeaf, f ); - if ( Lit == 2 || Lit == 3 ) - { - fFullTable = 0; - break; - } - } - } - if ( fFullTable ) - { - Vec_IntClear( p->vLits ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) - Vec_IntWriteEntry( p->vLits, k, Ga2_ObjFindOrAddLit(p, pLeaf, f) ); - iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddStatic( p, &p->pvCnfs0[pObj->Value], &p->pvCnfs1[pObj->Value], - Vec_IntArray(p->vLits), iLitOut, i < p->nAbs ? 0 : Gia_ObjId(p->pGia, pObj) ); - continue; - } - assert( i < p->nAbs ); - // collect literal types - Vec_IntClear( p->vLits ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) - { - Lit = Ga2_ObjFindLit( p, pLeaf, f ); - if ( Lit == 3 ) // const 0 - Vec_IntPush( p->vLits, 0 ); - else if ( Lit == 2 ) // const 1 - Vec_IntPush( p->vLits, 1 ); - else - Vec_IntPush( p->vLits, 2 ); - } - uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); - if ( uTruth == 0 || uTruth == ~0 ) - Ga2_ObjAddLit( p, pObj, f, uTruth == 0 ? 3 : 2 ); // const 0 / 1 - else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter - { - Lit = Vec_IntEntry( p->vLits, 0 ); - pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); + pLeaf = Gia_ManObj( p->pGia, pLeaves[Lit-GA2_BIG_NUM] ); Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); - Ga2_ObjAddLit( p, pObj, f, Abc_LitNotCond(Lit, uTruth == 0x55555555) ); - } - else - { - // replace numbers of literals by actual literals - Vec_IntForEachEntry( p->vLits, Lit, i ) - { - pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); - Lit = Ga2_ObjFindOrAddLit(p, pLeaf, f); - Vec_IntWriteEntry( p->vLits, i, Lit ); - } - // add CNF - iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), iLitOut, 0 ); } + Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 ); } - // propagate literals to the PO and flop outputs - pObjRi = Gia_ManPo( p->pGia, 0 ); - Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f ); - assert( Lit > 1 ); - Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) ); - Ga2_ObjAddLit( p, pObj, f, Lit ); - Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) + else { - if ( !Gia_ObjIsRo(p->pGia, pObj) ) - continue; - pObjRi = Gia_ObjRoToRi(p->pGia, pObj); - Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f ); - assert( Lit > 1 ); - Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) ); - Ga2_ObjAddLit( p, pObjRi, f, Lit ); + // perform structural hashing here!!! + + // add new node + Lit = Ga2_ObjFindOrAddLit(p, pObj, f); + Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, -1 ); } + Ga2_ObjAddLit( p, pObj, f, Lit ); + return Lit; } -*/ /**Function************************************************************* @@ -1041,7 +915,6 @@ int Vec_IntCheckUnique( Vec_Int_t * p ) return RetValue; } - /**Function************************************************************* Synopsis [] @@ -1072,7 +945,7 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv { if ( Ga2_ObjIsAbs(p, pObj) ) continue; - assert( Ga2_ObjIsPPI(p, pObj) ); + assert( Ga2_ObjIsPpi(p, pObj) ); assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) ); Vec_IntPush( vMap, Gia_ObjId(p->pGia, pObj) ); } @@ -1125,7 +998,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) Vec_IntFree( vMap ); // these objects should be PPIs that are not abstracted yet Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) - assert( Ga2_ObjIsPPI(p, pObj) && !Ga2_ObjIsAbs(p, pObj) ); + assert( Ga2_ObjIsPpi(p, pObj) && !Ga2_ObjIsAbs(p, pObj) ); p->nObjAdded += Vec_IntSize(vVec); return vVec; } @@ -1146,7 +1019,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; clock_t clk = clock(); - int i, c, f, Lit, nAbs, nValues, Status, RetValue = -1;; + int nAbs, nValues, Status, RetValue = -1; + int i, c, f, Lit; // start the manager p = Ga2_ManStart( pAig, pPars ); // check trivial case @@ -1203,10 +1077,14 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) for ( c = 0; ; c++ ) { // perform SAT solving + clk = clock(); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( Status == l_True ) // perform refinement { + p->timeSat += clock() - clk; + clk = clock(); vPPis = Ga2_ManRefine( p ); + p->timeCex += clock() - clk; if ( vPPis == NULL ) goto finish; Ga2_ManAddToAbs( p, vPPis ); @@ -1216,6 +1094,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); continue; } + p->timeUnsat += clock() - clk; if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout goto finish; if ( Status == l_Undef ) // ran out of resources @@ -1292,7 +1171,7 @@ finish: ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); -// Ga2_ManReportMemory( p ); + Ga2_ManReportMemory( p ); } Ga2_ManStop( p ); fflush( stdout ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index a0208376..5b5fe13a 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -90,6 +90,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vTtNodes ); Vec_WrdFreeP( &p->vTtMemory ); Vec_PtrFreeP( &p->vTtInputs ); + Vec_IntFreeP( &p->vMapping ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); ABC_FREE( p->pTravIds ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 74fe7fc2..bca80155 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28109,10 +28109,10 @@ usage: int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_ParVta_t Pars, * pPars = &Pars; - int c, fStartVta = 0; + int c, fStartVta = 0, fNewAlgo = 0; Gia_VtaSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadnvh" ) ) != EOF ) { switch ( c ) { @@ -28242,6 +28242,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pPars->fDumpVabs ^= 1; break; + case 'n': + fNewAlgo ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -28278,13 +28281,16 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); return 0; } - pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta ); + if ( fNewAlgo ) + pAbc->Status = Ga2_ManPerform( pAbc->pGia, pPars ); + else + pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadvh]\n" ); + Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadnvh]\n" ); Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); @@ -28299,6 +28305,7 @@ usage: Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" ); Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" ); + Abc_Print( -2, "\t-n : toggle using new algorithms [default = %s]\n", fNewAlgo? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -29677,7 +29684,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); // extern int Gia_ManSuppSizeTest( Gia_Man_t * p ); // extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); - extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); +// extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); + extern void Ga2_ManComputeTest( Gia_Man_t * p ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -29716,6 +29724,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManSuppSizeTest( pAbc->pGia ); // Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); // Gia_IsoTest( pAbc->pGia, fVerbose ); + Ga2_ManComputeTest( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); -- cgit v1.2.3