diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 22:08:54 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 22:08:54 -0800 |
commit | 5fd6dc0fca7f15d87f1fbd6401c3caa2c993834a (patch) | |
tree | 73b0e3d71a2de7e7a598ca20b9f8740083513241 | |
parent | 716969190a4d6d944cfa24a085c9e7069d868dab (diff) | |
download | abc-5fd6dc0fca7f15d87f1fbd6401c3caa2c993834a.tar.gz abc-5fd6dc0fca7f15d87f1fbd6401c3caa2c993834a.tar.bz2 abc-5fd6dc0fca7f15d87f1fbd6401c3caa2c993834a.zip |
Profiling quantification and other changes.
-rw-r--r-- | src/aig/gia/gia.h | 5 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 1 | ||||
-rw-r--r-- | src/proof/cec/cecSat.c | 67 | ||||
-rw-r--r-- | src/proof/cec/cecSatG.c | 14 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 70 |
5 files changed, 89 insertions, 68 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 920ebb06..c8b64a16 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -148,6 +148,7 @@ struct Gia_Man_t_ Abc_Cex_t * pCexSeq; // sequential counter-example Vec_Ptr_t * vSeqModelVec; // sequential counter-examples Vec_Int_t vCopies; // intermediate copies + Vec_Int_t vCopies2; // intermediate copies Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vGateClasses; // classes of gates for abstraction @@ -532,6 +533,10 @@ static inline int Gia_ObjCopyArray( Gia_Man_t * p, int iObj ) static inline void Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); } static inline void Gia_ManCleanCopyArray( Gia_Man_t * p ) { Vec_IntFill( &p->vCopies, Gia_ManObjNum(p), -1 ); } +static inline int Gia_ObjCopy2Array( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies2, iObj); } +static inline void Gia_ObjSetCopy2Array( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies2, iObj, iLit); } +static inline void Gia_ManCleanCopy2Array( Gia_Man_t * p ) { Vec_IntFill( &p->vCopies2, Gia_ManObjNum(p), -1 ); } + static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } static inline int Gia_ObjFanin0CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p,pObj)), Gia_ObjFaninC0(pObj)); } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 6ff822c3..a8b03207 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -117,6 +117,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); Vec_IntErase( &p->vCopies ); + Vec_IntErase( &p->vCopies2 ); Vec_IntFreeP( &p->vTtNums ); Vec_IntFreeP( &p->vTtNodes ); Vec_WrdFreeP( &p->vTtMemory ); diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index aa9d8f10..0f4bf2bb 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -73,9 +73,9 @@ struct Cec2_Man_t_ abctime timeStart; }; -static inline int Cec2_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); } -static inline int Cec2_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec2_ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; } -static inline void Cec2_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec2_ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); } +static inline int Cec2_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj)); } +static inline int Cec2_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec2_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); return Num; } +static inline void Cec2_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec2_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -310,49 +310,54 @@ void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFronti if ( Gia_ObjIsAnd(pObj) ) Vec_PtrPush( vFrontier, pObj ); } -int Cec2_ObjGetCnfVar( Cec2_Man_t * p, int iObj ) +int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr_t * vFanins, satoko_t * pSat ) { Gia_Obj_t * pNode, * pFanin; - Gia_Obj_t * pObj = Gia_ManObj(p->pNew, iObj); + Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj); int i, k, fUseMuxes = 1; + if ( Vec_IntSize(&pGia->vCopies2) < Gia_ManObjNum(pGia) ) + Vec_IntFillExtra( &pGia->vCopies2, Gia_ManObjNum(pGia), -1 ); // quit if CNF is ready - if ( Cec2_ObjSatId(p->pNew,pObj) >= 0 ) - return Cec2_ObjSatId(p->pNew,pObj); + if ( Cec2_ObjSatId(pGia,pObj) >= 0 ) + return Cec2_ObjSatId(pGia,pObj); assert( iObj > 0 ); if ( Gia_ObjIsCi(pObj) ) - return Cec2_ObjSetSatId( p->pNew, pObj, satoko_add_variable(p->pSat, 0) ); + return Cec2_ObjSetSatId( pGia, pObj, satoko_add_variable(pSat, 0) ); assert( Gia_ObjIsAnd(pObj) ); // start the frontier - Vec_PtrClear( p->vFrontier ); - Cec2_ObjAddToFrontier( p->pNew, pObj, p->vFrontier, p->pSat ); + Vec_PtrClear( vFrontier ); + Cec2_ObjAddToFrontier( pGia, pObj, vFrontier, pSat ); // explore nodes in the frontier - Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i ) + Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i ) { // create the supergate - assert( Cec2_ObjSatId(p->pNew,pNode) >= 0 ); + assert( Cec2_ObjSatId(pGia,pNode) >= 0 ); if ( fUseMuxes && pNode->fMark0 ) { - Vec_PtrClear( p->vFanins ); - Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) - Cec2_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat ); - Cec2_AddClausesMux( p->pNew, pNode, p->pSat ); + Vec_PtrClear( vFanins ); + Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k ) + Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat ); + Cec2_AddClausesMux( pGia, pNode, pSat ); } else { - Cec2_CollectSuper( pNode, fUseMuxes, p->vFanins ); - Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) - Cec2_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat ); - Cec2_AddClausesSuper( p->pNew, pNode, p->vFanins, p->pSat ); + Cec2_CollectSuper( pNode, fUseMuxes, vFanins ); + Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k ) + Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat ); + Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat ); } - assert( Vec_PtrSize(p->vFanins) > 1 ); + assert( Vec_PtrSize(vFanins) > 1 ); } - return Cec2_ObjSatId(p->pNew,pObj); + return Cec2_ObjSatId(pGia,pObj); +} +int Cec2_ObjGetCnfVar( Cec2_Man_t * p, int iObj ) +{ + return Gia_ObjGetCnfVar( p->pNew, iObj, p->vFrontier, p->vFanins, p->pSat ); } - /**Function************************************************************* @@ -673,7 +678,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) Gia_ManForEachCi( pAig, pObj, i ) pObj->Value = Gia_ManAppendCi( p->pNew ); Gia_ManHashAlloc( p->pNew ); - Vec_IntFill( &p->pNew->vCopies, Gia_ManObjNum(p->pNew), -1 ); + Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(p->pNew), -1 ); // SAT solving memset( &Pars, 0, sizeof(satoko_opts_t) ); p->pSat = satoko_create(); @@ -952,14 +957,14 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) ); // duplicate the node pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Vec_IntSize(&pMan->pNew->vCopies) == Abc_Lit2Var(pObj->Value) ) + if ( Vec_IntSize(&pMan->pNew->vCopies2) == Abc_Lit2Var(pObj->Value) ) { pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) ); pObjNew->fMark0 = Gia_ObjIsMuxType( pObjNew ); Gia_ObjSetPhase( pMan->pNew, pObjNew ); - Vec_IntPush( &pMan->pNew->vCopies, -1 ); + Vec_IntPush( &pMan->pNew->vCopies2, -1 ); } - assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) ); + assert( Vec_IntSize(&pMan->pNew->vCopies2) == Gia_ManObjNum(pMan->pNew) ); pRepr = Gia_ObjReprObj( p, i ); if ( pRepr == NULL || !~pRepr->Value ) continue; diff --git a/src/proof/cec/cecSatG.c b/src/proof/cec/cecSatG.c index d0f146fd..08e9c4d9 100644 --- a/src/proof/cec/cecSatG.c +++ b/src/proof/cec/cecSatG.c @@ -73,9 +73,9 @@ struct Cec3_Man_t_ abctime timeStart; }; -static inline int Cec3_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); } -static inline int Cec3_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec3_ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; } -static inline void Cec3_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec3_ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); } +static inline int Cec3_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj)); } +static inline int Cec3_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec3_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); return Num; } +static inline void Cec3_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec3_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } static inline void satoko_mark_cone( bmcg_sat_solver * p, int * pVars, int nVars ) {} static inline void satoko_unmark_cone( bmcg_sat_solver * p, int * pVars, int nVars ) {} @@ -676,7 +676,7 @@ Cec3_Man_t * Cec3_ManCreate( Gia_Man_t * pAig, Cec3_Par_t * pPars ) Gia_ManForEachCi( pAig, pObj, i ) pObj->Value = Gia_ManAppendCi( p->pNew ); Gia_ManHashAlloc( p->pNew ); - Vec_IntFill( &p->pNew->vCopies, Gia_ManObjNum(p->pNew), -1 ); + Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(p->pNew), -1 ); // SAT solving //memset( &Pars, 0, sizeof(satoko_opts_t) ); p->pSat = bmcg_sat_solver_start(); @@ -965,14 +965,14 @@ int Cec3_ManPerformSweeping( Gia_Man_t * p, Cec3_Par_t * pPars, Gia_Man_t ** ppN assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) ); // duplicate the node pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Vec_IntSize(&pMan->pNew->vCopies) == Abc_Lit2Var(pObj->Value) ) + if ( Vec_IntSize(&pMan->pNew->vCopies2) == Abc_Lit2Var(pObj->Value) ) { pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) ); pObjNew->fMark0 = Gia_ObjIsMuxType( pObjNew ); Gia_ObjSetPhase( pMan->pNew, pObjNew ); - Vec_IntPush( &pMan->pNew->vCopies, -1 ); + Vec_IntPush( &pMan->pNew->vCopies2, -1 ); } - assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) ); + assert( Vec_IntSize(&pMan->pNew->vCopies2) == Gia_ManObjNum(pMan->pNew) ); pRepr = Gia_ObjReprObj( p, i ); if ( pRepr == NULL || !~pRepr->Value ) continue; diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index eea56d25..474acb6b 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -911,10 +911,11 @@ abctime clkQuaSynth = 0; int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ) { + int fSynthesize = 0; abctime clk = Abc_Clock(), clkAll = Abc_Clock(); extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); Gia_Man_t * pMan, * pNew, * pTemp; Vec_Str_t * vSop; - int i, CiId, ObjId, Res, nCubes, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit); + int i, CiId, ObjId, Res, nCubes = 0, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit); Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 ); Gia_ManCollectCis( p, &iNode, 1, vCisUsed ); Vec_IntSort( vCisUsed, 0 ); @@ -927,6 +928,7 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT // duplicate cone pNew = Gia_ManDupConeSupp( p, iLit, vCisUsed ); assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCisUsed) ); + nNodes = Gia_ManAndNum(pNew); // perform quantification one CI at a time assert( pFuncCiToKeep ); @@ -947,40 +949,48 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT return RetValue; } - clk = Abc_Clock(); - vSop = bmcg_sat_solver_sop( pNew, 0 ); - nNodes = Gia_ManAndNum(pNew); - Gia_ManStop( pNew ); - clkQuaSolve += Abc_Clock() - clk; - - clk = Abc_Clock(); - pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 ); - clkQuaSynth += Abc_Clock() - clk; - nCubes = Vec_StrCountEntry(vSop, '\n'); - if ( vDLits ) + if ( fSynthesize ) { - // convert into object IDs - Vec_Int_t * vCisObjs = Vec_IntAlloc( Vec_IntSize(vCisUsed) ); - Vec_IntForEachEntry( vCisUsed, CiId, i ) - Vec_IntPush( vCisObjs, CiId + 1 ); - bmcg_sat_generate_dvars( vCisObjs, vSop, vDLits ); - Vec_IntFree( vCisObjs ); + clk = Abc_Clock(); + vSop = bmcg_sat_solver_sop( pNew, 0 ); + Gia_ManStop( pNew ); + clkQuaSolve += Abc_Clock() - clk; + + clk = Abc_Clock(); + pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 ); + nCubes = Vec_StrCountEntry(vSop, '\n'); + clkQuaSynth += Abc_Clock() - clk; + + if ( vDLits ) + { + // convert into object IDs + Vec_Int_t * vCisObjs = Vec_IntAlloc( Vec_IntSize(vCisUsed) ); + Vec_IntForEachEntry( vCisUsed, CiId, i ) + Vec_IntPush( vCisObjs, CiId + 1 ); + bmcg_sat_generate_dvars( vCisObjs, vSop, vDLits ); + Vec_IntFree( vCisObjs ); + } + Vec_StrFree( vSop ); + + if ( Gia_ManPoIsConst(pMan, 0) ) + { + int RetValue = Gia_ManPoIsConst1(pMan, 0); + Vec_IntFree( vCisUsed ); + Gia_ManStop( pMan ); + return RetValue; + } } - Vec_StrFree( vSop ); - if ( Gia_ManPoIsConst(pMan, 0) ) + else { - int RetValue = Gia_ManPoIsConst1(pMan, 0); - Vec_IntFree( vCisUsed ); - Gia_ManStop( pMan ); - return RetValue; + pMan = pNew; } Res = Gia_ManDupConeBack( p, pMan, vCisUsed ); // report the result - printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", - nNodes, Vec_IntSize(vCisUsed) - Count, Count, nCubes, Gia_ManAndNum(pMan) ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); +// printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", +// nNodes, Vec_IntSize(vCisUsed) - Count, Count, nCubes, Gia_ManAndNum(pMan) ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); Vec_IntFree( vCisUsed ); Gia_ManStop( pMan ); @@ -1162,9 +1172,9 @@ int bmcg_sat_solver_quantify3( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLi clkQuaSynth += Abc_Clock() - clk; // report the result - printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", - Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); +// printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", +// Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); cleanup: Vec_IntForEachEntry( vObjsUsed, iVar, i ) |