diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaCSat.c | 10 | ||||
-rw-r--r-- | src/aig/gia/giaCSatOld.c | 5 | ||||
-rw-r--r-- | src/aig/gia/giaDfs.c | 30 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 2 |
4 files changed, 42 insertions, 5 deletions
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 832eff26..f53a3d33 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -885,6 +885,8 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) pDecVar = Gia_Not(Gia_ObjChild0(pVar)); else pDecVar = Gia_Not(Gia_ObjChild1(pVar)); +// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase ); +// pDecVar = Gia_Not(pDecVar); // decide on first fanin Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL ); if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) ) @@ -955,8 +957,9 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) ***********************************************************************/ void Cbs_ManSatPrintStats( Cbs_Man_t * p ) { - printf( "CO = %6d ", Gia_ManCoNum(p->pAig) ); - printf( "Conf = %5d ", p->Pars.nBTLimit ); + printf( "CO = %8d ", Gia_ManCoNum(p->pAig) ); + printf( "AND = %8d ", Gia_ManAndNum(p->pAig) ); + printf( "Conf = %6d ", p->Pars.nBTLimit ); printf( "JustMax = %5d ", p->Pars.nJustLimit ); printf( "\n" ); printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", @@ -984,6 +987,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p ) ***********************************************************************/ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ) { + extern void Gia_ManCollectTest( Gia_Man_t * pAig ); extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ); Cbs_Man_t * p; Vec_Int_t * vCex, * vVisit, * vCexStore; @@ -991,11 +995,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt Gia_Obj_t * pRoot; int i, status, clk, clkTotal = clock(); assert( Gia_ManRegNum(pAig) == 0 ); +// Gia_ManCollectTest( pAig ); // prepare AIG Gia_ManCreateRefs( pAig ); Gia_ManCleanMark0( pAig ); Gia_ManCleanMark1( pAig ); Gia_ManFillValue( pAig ); // maps nodes into trail ids + Gia_ManSetPhase( pAig ); // maps nodes into trail ids // create logic network p = Cbs_ManAlloc(); p->Pars.nBTLimit = nConfs; diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c index 409af56c..a0d97693 100644 --- a/src/aig/gia/giaCSatOld.c +++ b/src/aig/gia/giaCSatOld.c @@ -674,8 +674,9 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj ) ***********************************************************************/ void Cbs0_ManSatPrintStats( Cbs0_Man_t * p ) { - printf( "CO = %6d ", Gia_ManCoNum(p->pAig) ); - printf( "Conf = %5d ", p->Pars.nBTLimit ); + printf( "CO = %8d ", Gia_ManCoNum(p->pAig) ); + printf( "AND = %8d ", Gia_ManAndNum(p->pAig) ); + printf( "Conf = %6d ", p->Pars.nBTLimit ); printf( "JustMax = %5d ", p->Pars.nJustLimit ); printf( "\n" ); printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index a978dcc3..8a3aef92 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -122,7 +122,7 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN Gia_Obj_t * pObj; int i; Vec_IntClear( vNodes ); - Gia_ManIncrementTravId( p ); +// Gia_ManIncrementTravId( p ); Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); for ( i = 0; i < nNodes; i++ ) { @@ -145,6 +145,34 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN SeeAlso [] ***********************************************************************/ +void Gia_ManCollectTest( Gia_Man_t * p ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int i, iNode, clk = clock(); + vNodes = Vec_IntAlloc( 100 ); + Gia_ManResetTravId( p ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachCo( p, pObj, i ) + { + iNode = Gia_ObjId(p, pObj); + Gia_ManCollectAnds( p, &iNode, 1, vNodes ); + } + Vec_IntFree( vNodes ); + ABC_PRT( "DFS from each output", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Collects support nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Gia_ManSuppSize_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index cdee73d0..041be0f5 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1135,6 +1135,8 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); return; } + if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit + return; assert( pRepr->Value < pObj->Value ); pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) ); pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); |