luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Various changes to enable sensitization-based refinement in &gla.

This commit is contained in:
Alan Mishchenko 2012-07-04 14:53:07 -07:00
parent c921058019
commit 9ebcd9eca9
11 changed files with 191 additions and 356 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

497
src/aig/gia/giaAbsGla.c
View File

@ -36,8 +36,8 @@ struct Rfn_Obj_t_
unsigned Value : 1; // value unsigned Value : 1; // value
unsigned fVisit : 1; // visited unsigned fVisit : 1; // visited
unsigned fPPi : 1; // PPI unsigned fPPi : 1; // PPI
unsigned Prio : 18; // priority unsigned Prio : 16; // priority
unsigned Sign : 10; // priority unsigned Sign : 12; // traversal signature
}; };
typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
@ -80,7 +80,7 @@ struct Gla_Man_t_
Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs
Vec_Int_t * vTemp; // temporary array Vec_Int_t * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array Vec_Int_t * vAddedNew; // temporary array
Vec_Int_t * vPrevCore; // previous core Vec_Int_t * vObjCounts; // object counters
// refinement // refinement
Vec_Int_t * pvRefis; // vectors of each object Vec_Int_t * pvRefis; // vectors of each object
Vec_Int_t * vPrioSels; // selected priorities Vec_Int_t * vPrioSels; // selected priorities
@ -333,6 +333,8 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
/**Function************************************************************* /**Function*************************************************************
Synopsis [Derives counter-example using current assignments.] Synopsis [Derives counter-example using current assignments.]
@ -373,23 +375,15 @@ Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t * vRoAnds ) void Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t * vRoAnds )
{ {
int Value0, Value1;
if ( Gia_ObjIsTravIdCurrent(p, pGiaObj) ) if ( Gia_ObjIsTravIdCurrent(p, pGiaObj) )
return 1; return;
Gia_ObjSetTravIdCurrent(p, pGiaObj); Gia_ObjSetTravIdCurrent(p, pGiaObj);
if ( Gia_ObjIsCi(pGiaObj) )
return 0;
assert( Gia_ObjIsAnd(pGiaObj) ); assert( Gia_ObjIsAnd(pGiaObj) );
Value0 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds ); Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds );
Value1 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds ); Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds );
if ( Value0 || Value1 ) Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
{
assert( Gia_ObjIsAnd(pGiaObj) );
Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
}
return Value0 || Value1;
} }
void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds ) void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds )
{ {
@ -414,6 +408,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
} }
Vec_IntUniqify( vPis ); Vec_IntUniqify( vPis );
Vec_IntUniqify( vPPis ); Vec_IntUniqify( vPPis );
Vec_IntSort( vCos, 0 );
// mark const/PIs/PPIs // mark const/PIs/PPIs
Gia_ManIncrementTravId( p->pGia ); Gia_ManIncrementTravId( p->pGia );
@ -448,6 +443,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
***********************************************************************/ ***********************************************************************/
void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes, int Sign ) void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes, int Sign )
{ {
int Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
assert( (int)pRef->Sign == Sign ); assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit ) if ( pRef->fVisit )
@ -457,6 +453,7 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
{ {
assert( (int)pRef->Prio > 0 ); assert( (int)pRef->Prio > 0 );
assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) ); assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
Vec_IntAddToEntry( p->vObjCounts, f, 1 );
if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
{ {
Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 ); Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 );
@ -476,35 +473,36 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
{ {
Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f ); Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
int fSel0 = Vec_IntEntry( p->vPrioSels, pRef0->Prio );
int fSel1 = Vec_IntEntry( p->vPrioSels, pRef1->Prio );
if ( pRef->Value == 1 ) if ( pRef->Value == 1 )
{ {
// if ( !fSel0 ) if ( pRef0->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
// if ( !fSel1 ) if ( pRef1->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
} }
else // select one value else // select one value
{ {
if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{ {
// if ( !fSel0 && !fSel1 ) if ( pRef0->Prio <= pRef1->Prio ) // choice
{ {
if ( pRef0->Prio <= pRef1->Prio ) // choice if ( pRef0->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
else }
else
{
if ( pRef1->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
} }
} }
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{ {
// if ( !fSel0 ) if ( pRef0->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
} }
else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{ {
// if ( !fSel1 ) if ( pRef1->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
} }
else assert( 0 ); else assert( 0 );
@ -513,6 +511,70 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
else assert( 0 ); else assert( 0 );
} }
/**Function*************************************************************
Synopsis [Performs refinement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vRoAnds, Vec_Int_t * vCos, Vec_Int_t * vRes )
{
Gia_Obj_t * pObj;
int i, f;
// Gia_ManForEachObj( p->pGia, pObj, i )
// assert( Gia_ObjTerSimGetC(pObj) );
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected
Gia_ObjTerSimSetX( pObj );
else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
Gia_ObjTerSimAnd( pObj );
else if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( p->pGia, pObj );
}
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( p->pGia, 0 );
if ( !Gia_ObjTerSimGet1(pObj) )
printf( "\nRefinement verification has failed!!!\n" );
// clear
Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs refinement.] Synopsis [Performs refinement.]
@ -531,7 +593,6 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vRes = NULL; Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vRes = NULL;
Rfn_Obj_t * pRef, * pRef0, * pRef1; Rfn_Obj_t * pRef, * pRef0, * pRef1;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
// Gla_Obj_t * pGla;
int i, f; int i, f;
Sign++; Sign++;
@ -541,6 +602,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
vPPis = Vec_IntAlloc( 1000 ); vPPis = Vec_IntAlloc( 1000 );
vRoAnds = Vec_IntAlloc( 1000 ); vRoAnds = Vec_IntAlloc( 1000 );
Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds ); Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds );
/* /*
// check how many pseudo PIs have variables // check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPis, p, pGla, i ) Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
@ -571,22 +633,17 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// primary input // primary input
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i ) Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{ {
assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) ); // assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = 0; pRef->Prio = 0;
pRef->Sign = Sign; pRef->Sign = Sign;
assert( pRef->fVisit == 0 ); assert( pRef->fVisit == 0 );
} }
// primary input // primary input
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i ) Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{ {
int ObjId = Gia_ObjId(p->pGia, pObj); // assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
if ( 1308 == Gia_ObjId(p->pGia, pObj) )
{
int s = 0;
}
assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ); pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
@ -595,14 +652,9 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef->Sign = Sign; pRef->Sign = Sign;
assert( pRef->fVisit == 0 ); assert( pRef->fVisit == 0 );
} }
// internal nodes // internal nodes
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i ) Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{ {
if ( 1598 == Gia_ObjId(p->pGia, pObj) )
{
int s = 0;
}
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef ); pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
if ( Gia_ObjIsRo(p->pGia, pObj) ) if ( Gia_ObjIsRo(p->pGia, pObj) )
@ -619,13 +671,6 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef->Value = pRef0->Value; pRef->Value = pRef0->Value;
pRef->Prio = pRef0->Prio; pRef->Prio = pRef0->Prio;
pRef->Sign = Sign; pRef->Sign = Sign;
if ( (int)pRef->Value != Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
{
Gla_Obj_t * pGla = Gla_ManObj(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj))]);
int s = 0;
}
} }
continue; continue;
} }
@ -634,51 +679,12 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f ); pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj)); pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 && Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) ) if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 &&
Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) &&
(int)pRef->Value != Gla_ObjSatValue(p, Gia_ObjId(p->pGia, pObj), f) )
{ {
Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
int iff = Gia_ObjId(p->pGia, pFan1);
// assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) );
if ( (int)pRef->Value != Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
{
Gia_Obj_t * pFanin0 = Gia_ObjFanin0(pObj);
Gia_Obj_t * pFanin1 = Gia_ObjFanin1(pObj);
int id = Gia_ObjId(p->pGia, pObj);
int v = p->pObj2Obj[Gia_ObjId(p->pGia, pObj)];
int v1 = p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj))];
int v2 = p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj))];
int c = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f);
// int c1 = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj))], f);
// int c2 = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj))], f);
int Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj) , f );
// int Value1 = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj)), f );
// int Value2 = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj)), f );
Gla_Obj_t * pGla= Gla_ManObj( p, v );
Gla_Obj_t * pFanin;
int j;
Gla_ObjForEachFanin( p, pGla, pFanin, j )
{
Rfn_Obj_t * pRef3 = Gla_ObjRef( p, pFanin->iGiaObj, f );
int c = Gla_ManCheckVar(p, p->pObj2Obj[pFanin->iGiaObj], f);
Gia_ObjPrint( p->pGia, Gia_ManObj(p->pGia, pFanin->iGiaObj) );
if ( (int)pRef3->Value != Gla_ObjSatValue( p, pFanin->iGiaObj, f ) )
{
int s = 0;
}
}
printf( "Object has value mismatch " ); printf( "Object has value mismatch " );
Gia_ObjPrint( p->pGia, pObj ); Gia_ObjPrint( p->pGia, pObj );
}
} }
if ( pRef->Value == 1 ) if ( pRef->Value == 1 )
@ -703,10 +709,12 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef->Sign = Sign; pRef->Sign = Sign;
} }
} }
// make sure the output value is 1 // make sure the output value is 1
pObj = Gia_ManPo( p->pGia, 0 ); pObj = Gia_ManPo( p->pGia, 0 );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame ); pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame );
assert( pRef->Value == 1 ); if ( pRef->Value != 1 )
printf( "\nCounter-example verification has failed!!!\n" );
// check the CEX // check the CEX
if ( pRef->Prio == 0 ) if ( pRef->Prio == 0 )
@ -722,57 +730,15 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// select objects // select objects
vRes = Vec_IntAlloc( 100 ); vRes = Vec_IntAlloc( 100 );
Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 ); Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes, Sign ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes, Sign );
/*
for ( f = 0; f < p->pPars->iFrame; f++ )
printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
printf( "\n" );
*/
if ( fVerify ) if ( fVerify )
{ Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vRes );
Gia_ManForEachObj( p->pGia, pObj, i )
assert( Gia_ObjTerSimGetC(pObj) );
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected
Gia_ObjTerSimSetX( pObj );
else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
Gia_ObjTerSimAnd( pObj );
else if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( p->pGia, pObj );
}
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( p->pGia, 0 );
if ( !Gia_ObjTerSimGet1(pObj) )
printf( "Refinement verification has failed!!!\n" );
// clear
Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gia_ObjTerSimSetC( pObj );
}
// remap them into GLA objects // remap them into GLA objects
Gia_ManForEachObjVec( vRes, p->pGia, pObj, i ) Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
@ -786,78 +752,6 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
} }
/**Function*************************************************************
Synopsis [Selects items that are new in the current abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManRegionStart( Gla_Man_t * p, Vec_Int_t * vCore )
{
Vec_Int_t * vRes;
Gla_Obj_t * pGla;
int i;
vRes = Vec_IntAlloc( 100 );
Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
if ( !pGla->fAbs )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
return vRes;
}
/**Function*************************************************************
Synopsis [Finds adjacent to previous core among select (or all if NULL).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManRegionFilter( Gla_Man_t * p, Vec_Int_t * vSelected, Vec_Int_t * vPrevCore )
{
Vec_Int_t * vRes;
Gla_Obj_t * pGla, * pFanin;
int i, k;
// mark fanins of previous core
Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
{
assert( pGla->fMark == 0 );
Gla_ObjForEachFanin( p, pGla, pFanin, k )
pFanin->fMark = 1;
}
// select those not marked and included in the abstraction
vRes = Vec_IntAlloc( 100 );
if ( vSelected == NULL )
{
Gla_ManForEachObj( p, pGla )
if ( !pGla->fAbs && pGla->fMark )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
}
else
{
Gla_ManForEachObjAbsVec( vSelected, p, pGla, i )
if ( !pGla->fAbs && pGla->fMark )
Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
}
// unmark fanins of previous core
Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
Gla_ObjForEachFanin( p, pGla, pFanin, k )
pFanin->fMark = 0;
return vRes;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Adds clauses for the given obj in the given frame.] Synopsis [Adds clauses for the given obj in the given frame.]
@ -953,7 +847,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
else if ( Gia_ObjIsCo(pObj) ) else if ( Gia_ObjIsCo(pObj) )
{ {
Gia_ObjFanin0(pObj)->Value = pObj2Obj[Gia_ObjFaninId0p(p, pObj)]; Gia_ObjFanin0(pObj)->Value = pObj2Obj[Gia_ObjFaninId0p(p, pObj)];
assert( Gia_ObjFanin0(pObj)->Value >= 0 ); assert( ~Gia_ObjFanin0(pObj)->Value );
pObj2Obj[i] = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pObj2Obj[i] = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntPush( pNew->vLutConfigs, i ); Vec_IntPush( pNew->vLutConfigs, i );
} }
@ -978,14 +872,14 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
{ {
Gla_Man_t * p; Gla_Man_t * p;
Aig_Man_t * pAig; Aig_Man_t * pAig;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Gla_Obj_t * pGla; Gla_Obj_t * pGla;
Vec_Int_t * vMappingNew; Vec_Int_t * vMappingNew;
int i, * pLits, * pObj2Count, * pObj2Clause; int i, k, Offset, * pMapping, * pLits, * pObj2Count, * pObj2Clause;
// start // start
p = ABC_CALLOC( Gla_Man_t, 1 ); p = ABC_CALLOC( Gla_Man_t, 1 );
@ -995,12 +889,12 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
p->vTemp = Vec_IntAlloc( 100 ); p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 ); p->vAddedNew = Vec_IntAlloc( 100 );
p->vPrioSels = Vec_IntAlloc( 100 ); p->vPrioSels = Vec_IntAlloc( 100 );
p->vObjCounts = Vec_IntAlloc( 100 );
// internal data // internal data
pAig = Gia_ManToAigSimple( pGia0 ); pAig = Gia_ManToAigSimple( pGia0 );
p->pCnf = Cnf_DeriveOther( pAig ); p->pCnf = Cnf_DeriveOther( pAig, 1 );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
// create working GIA // create working GIA
p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping ); p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
//printf( "Old GIA = %d. New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) ); //printf( "Old GIA = %d. New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
@ -1009,24 +903,41 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
assert( pGia0->vGateClasses != 0 ); assert( pGia0->vGateClasses != 0 );
p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) ); p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
// update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause
// (here are not updating p->pCnf->pVarNums because it is not needed)
vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) ); vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
pObj2Count = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) ); pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
pObj2Clause = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) ); pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
Gia_ManForEachObj( pGia0, pObj, i ) Gia_ManForEachObj( pGia0, pObj, i )
{ {
// skip internal nodes not used in the mapping
if ( !~pObj->Value ) if ( !~pObj->Value )
continue; continue;
// replace positive literal by variable // replace positive literal by variable
assert( !Abc_LitIsCompl(pObj->Value) ); assert( !Abc_LitIsCompl(pObj->Value) );
pObj->Value = Abc_Lit2Var(pObj->Value); pObj->Value = Abc_Lit2Var(pObj->Value);
assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) ); assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) );
// update mappings // update arrays
Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntEntry(p->pCnf->vMapping, i) );
pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i]; pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i];
pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i]; pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i];
if ( Vec_IntEntry(pGia0->vGateClasses, i) ) if ( Vec_IntEntry(pGia0->vGateClasses, i) )
Vec_IntWriteEntry( p->pGia->vGateClasses, pObj->Value, 1 ); Vec_IntWriteEntry( p->pGia->vGateClasses, pObj->Value, 1 );
// update mappings
Offset = Vec_IntEntry(p->pCnf->vMapping, i);
Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntSize(vMappingNew) );
pMapping = Vec_IntEntryP(p->pCnf->vMapping, Offset);
Vec_IntPush( vMappingNew, pMapping[0] );
for ( k = 1; k <= 4; k++ )
{
if ( pMapping[k] == -1 )
Vec_IntPush( vMappingNew, -1 );
else
{
assert( ~Gia_ManObj(pGia0, pMapping[k])->Value );
Vec_IntPush( vMappingNew, Gia_ManObj(pGia0, pMapping[k])->Value );
}
}
} }
// update mapping after the offset (currently not being done because it is not used)
Vec_IntFree( p->pCnf->vMapping ); p->pCnf->vMapping = vMappingNew; Vec_IntFree( p->pCnf->vMapping ); p->pCnf->vMapping = vMappingNew;
ABC_FREE( p->pCnf->pObj2Count ); p->pCnf->pObj2Count = pObj2Count; ABC_FREE( p->pCnf->pObj2Count ); p->pCnf->pObj2Count = pObj2Count;
ABC_FREE( p->pCnf->pObj2Clause ); p->pCnf->pObj2Clause = pObj2Clause; ABC_FREE( p->pCnf->pObj2Clause ); p->pCnf->pObj2Clause = pObj2Clause;
@ -1074,11 +985,23 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
pGla->fAnd = Gia_ObjIsAnd(pObj); pGla->fAnd = Gia_ObjIsAnd(pObj);
if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
continue; continue;
if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ) if ( Gia_ObjIsCo(pObj) )
{ {
Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp ); pGla->nFanins = 1;
pGla->nFanins = Vec_IntSize( p->vTemp ); pGla->Fanins[0] = Gia_ObjFanin0(pObj)->Value;
memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) ); continue;
}
if ( Gia_ObjIsAnd(pObj) )
{
// Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
// pGla->nFanins = Vec_IntSize( p->vTemp );
// memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
Offset = Vec_IntEntry( p->pCnf->vMapping, i );
pMapping = Vec_IntEntryP( p->pCnf->vMapping, Offset );
pGla->nFanins = 0;
for ( k = 1; k <= 4; k++ )
if ( pMapping[k] != -1 )
pGla->Fanins[ pGla->nFanins++ ] = Gia_ManObj(p->pGia, pMapping[k])->Value;
continue; continue;
} }
assert( Gia_ObjIsRo(p->pGia, pObj) ); assert( Gia_ObjIsRo(p->pGia, pObj) );
@ -1114,7 +1037,7 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{ {
Gla_Man_t * p; Gla_Man_t * p;
Aig_Man_t * pAig; Aig_Man_t * pAig;
@ -1131,7 +1054,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vPrioSels = Vec_IntAlloc( 100 ); p->vPrioSels = Vec_IntAlloc( 100 );
// internal data // internal data
pAig = Gia_ManToAigSimple( p->pGia ); pAig = Gia_ManToAigSimple( p->pGia );
p->pCnf = Cnf_DeriveOther( pAig ); p->pCnf = Cnf_DeriveOther( pAig, 1 );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
// count the number of variables // count the number of variables
p->nObjs = 1; p->nObjs = 1;
@ -1211,17 +1134,20 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Gla_ManStop( Gla_Man_t * p ) void Gla_ManStop( Gla_Man_t * p )
{ {
Gla_Obj_t * pGla; Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose ) // if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n", Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes ); sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla ) Gla_ManForEachObj( p, pGla )
ABC_FREE( pGla->vFrames.pArray ); ABC_FREE( pGla->vFrames.pArray );
Cnf_DataFree( p->pCnf ); Cnf_DataFree( p->pCnf );
if ( p->pGia0 != NULL ) if ( p->pGia0 != NULL )
Gia_ManStop( p->pGia ); Gia_ManStop( p->pGia );
sat_solver2_delete( p->pSat ); sat_solver2_delete( p->pSat );
Vec_IntFreeP( &p->vObjCounts );
Vec_IntFreeP( &p->vCla2Obj ); Vec_IntFreeP( &p->vCla2Obj );
Vec_IntFreeP( &p->vPrevCore );
Vec_IntFreeP( &p->vAddedNew ); Vec_IntFreeP( &p->vAddedNew );
Vec_IntFreeP( &p->vPrioSels ); Vec_IntFreeP( &p->vPrioSels );
Vec_IntFreeP( &p->vTemp ); Vec_IntFreeP( &p->vTemp );
@ -1359,8 +1285,6 @@ int Gla_ManCountPPis( Gla_Man_t * p )
Vec_IntFree( vPPis ); Vec_IntFree( vPPis );
return RetValue; return RetValue;
} }
void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis ) void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
{ {
static int Round = 0; static int Round = 0;
@ -1383,99 +1307,6 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
Vec_IntShrink( vPPis, j ); Vec_IntShrink( vPPis, j );
} }
// add those having more than one shared fanin
void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis )
{
static int Round = 0;
Vec_Int_t * vTemp;
Gla_Obj_t * pGla, * pFanin;
int i, k, Entry, Count;
if ( p->vPrevCore == NULL )
return;
if ( (Round++ % 10) == 0 )
{
p->vPrevCore = Gla_ManRegionFilter( p, vPPis, vTemp = p->vPrevCore );
Vec_IntFree( vTemp );
}
else
{
p->vPrevCore = Gla_ManRegionFilter( p, NULL, vTemp = p->vPrevCore );
Vec_IntFree( vTemp );
// save a copy
vTemp = Vec_IntDup( vPPis );
// udpate
Vec_IntClear( vPPis );
Vec_IntForEachEntry( p->vPrevCore, Entry, i )
Vec_IntPush( vPPis, Entry );
// mark those included as abstracted
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
{
assert( pGla->fAbs == 0 );
pGla->fAbs = 1;
}
// add those not included but to close to abstracted
Gla_ManForEachObjAbsVec( vTemp, p, pGla, i )
{
if ( pGla->fAbs )
continue;
Count = 0;
Gla_ObjForEachFanin( p, pGla, pFanin, k )
Count += pFanin->fAbs;
if ( Count == 0 || Count == 1 )
continue;
Vec_IntPush( vPPis, Gla_ObjId(p, pGla) );
}
// unmark those included
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
pGla->fAbs = 0;
// cleanup
Vec_IntFree( vTemp );
}
}
/*
void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis, int iIter )
{
Gla_Obj_t * pObj, * pFanin;
int i, j, k;
if ( iIter > 10 )
{
Gla_ManForEachObj( p, pObj )
pObj->fMark = 0;
return;
}
j = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
{
assert( pObj->fAbs == 0 );
if ( pObj->fMark == 0 )
{
Gla_ObjForEachFanin( p, pObj, pFanin, k )
if ( pObj->fMark )
break;
if ( k == (int)pObj->nFanins )
continue;
}
Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
}
// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
Vec_IntShrink( vPPis, j );
// update
Gla_ManForEachObj( p, pObj )
pObj->fMark = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
Gla_ObjForEachFanin( p, pObj, pFanin, k )
pFanin->fMark = 1;
}
*/
/**Function************************************************************* /**Function*************************************************************
@ -1513,10 +1344,6 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
{ {
Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj ); Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj );
int iVar, iVar1, iVar2; int iVar, iVar1, iVar2;
if ( 4786 == iObj && iFrame == 2 )
{
int s = 0;
}
if ( pGlaObj->fConst ) if ( pGlaObj->fConst )
{ {
iVar = Gla_ManGetVar( p, iObj, iFrame ); iVar = Gla_ManGetVar( p, iObj, iFrame );
@ -1744,7 +1571,6 @@ void Gla_ManReportMemory( Gla_Man_t * p )
memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int); memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int); memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memOth += (p->vPrevCore ? Vec_IntCap(p->vPrevCore) : 0) * sizeof(int);
memOth += Vec_IntCap(p->vTemp) * sizeof(int); memOth += Vec_IntCap(p->vTemp) * sizeof(int);
memOth += Vec_IntCap(p->vAbs) * sizeof(int); memOth += Vec_IntCap(p->vAbs) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + memRef + memOth; memTot = memAig + memSat + memPro + memMap + memRef + memOth;
@ -1862,7 +1688,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
sat_solver2_bookmark( p->pSat ); sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew ); Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs ); p->nAbsOld = Vec_IntSize( p->vAbs );
// nClaOld = Vec_IntSize( p->vCla2Obj );
// iterate as long as there are counter-examples // iterate as long as there are counter-examples
for ( i = 0; ; i++ ) for ( i = 0; ; i++ )
{ {
@ -1874,6 +1699,12 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gla_ManRollBack( p ); Gla_ManRollBack( p );
goto finish; goto finish;
} }
// check timeout
if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
{
Gla_ManRollBack( p ); // 1155046
goto finish;
}
if ( vCore != NULL ) if ( vCore != NULL )
{ {
p->timeUnsat += clock() - clk2; p->timeUnsat += clock() - clk2;
@ -1884,16 +1715,16 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p->nCexes++; p->nCexes++;
// perform the refinement // perform the refinement
clk2 = clock(); clk2 = clock();
/*
vPPis = Gla_ManRefinement( p ); vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL ) if ( vPPis == NULL )
{ {
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL; pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break; break;
} }
*/
vPPis = Gla_ManCollectPPis( p, NULL ); // vPPis = Gla_ManCollectPPis( p, NULL );
Gla_ManExplorePPis( p, vPPis ); // Gla_ManExplorePPis( p, vPPis );
Gia_GlaAddToAbs( p, vPPis, 1 ); Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis ); Gia_GlaAddOneSlice( p, f, vPPis );
@ -1922,8 +1753,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gla_ManRollBack( p ); Gla_ManRollBack( p );
Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 ); Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
// load this timeframe // load this timeframe
Vec_IntFreeP( &p->vPrevCore );
p->vPrevCore = Gla_ManRegionStart( p, vCore );
Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddToAbs( p, vCore, 0 );
Gia_GlaAddOneSlice( p, f, vCore ); Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore ); Vec_IntFree( vCore );

6
src/aig/gia/giaAbsVta.c
View File

@ -1674,6 +1674,12 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vga_ManRollBack( p, nObjOld ); Vga_ManRollBack( p, nObjOld );
goto finish; goto finish;
} }
// check timeout
if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
if ( vCore != NULL ) if ( vCore != NULL )
{ {
p->timeUnsat += clock() - clk2; p->timeUnsat += clock() - clk2;

2
src/aig/saig/saigAbsVfa.c
View File

@ -252,7 +252,7 @@ Abs_VfaMan_t * Abs_VfaManStart( Aig_Man_t * pAig )
Vec_IntPush( p->vVec2Var, -1 ); Vec_IntPush( p->vVec2Var, -1 );
// transfer values from CNF // transfer values from CNF
p->pCnf = Cnf_DeriveOther( pAig ); p->pCnf = Cnf_DeriveOther( pAig, 0 );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
if ( p->pCnf->pObj2Clause[i] == -1 ) if ( p->pCnf->pObj2Clause[i] == -1 )
Vec_IntWriteEntry( p->vObj2Vec, i, -1 ); Vec_IntWriteEntry( p->vObj2Vec, i, -1 );

2
src/opt/dar/dar.h
View File

@ -91,7 +91,7 @@ extern void Dar_BalancePrintStats( Aig_Man_t * p );
/*=== darCore.c ========================================================*/ /*=== darCore.c ========================================================*/
extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ); extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ); extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose ); extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtMin, int fVerbose );
/*=== darRefact.c ========================================================*/ /*=== darRefact.c ========================================================*/
extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ); extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ); extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );

4
src/opt/dar/darCore.c
View File

@ -281,7 +281,7 @@ int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose ) Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtMin, int fVerbose )
{ {
Dar_Man_t * p; Dar_Man_t * p;
Dar_RwrPar_t Pars, * pPars = &Pars; Dar_RwrPar_t Pars, * pPars = &Pars;
@ -306,7 +306,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
Dar_ObjPrepareCuts( p, pObj ); Dar_ObjPrepareCuts( p, pObj );
// compute cuts for each nodes in the topological order // compute cuts for each nodes in the topological order
Aig_ManForEachNode( pAig, pObj, i ) Aig_ManForEachNode( pAig, pObj, i )
Dar_ObjComputeCuts( p, pObj ); Dar_ObjComputeCuts( p, pObj, fSkipTtMin );
// print verbose stats // print verbose stats
if ( fVerbose ) if ( fVerbose )
{ {

10
src/opt/dar/darCut.c
View File

@ -735,14 +735,14 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ) Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj, int fSkipTtMin )
{ {
Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) ); Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0); Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1); Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut; Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
int i, k, RetValue; int i, k;
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
@ -779,9 +779,9 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) ); pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );
// minimize support of the cut // minimize support of the cut
if ( Dar_CutSuppMinimize( pCut ) ) if ( !fSkipTtMin && Dar_CutSuppMinimize( pCut ) )
{ {
RetValue = Dar_CutFilter( pObj, pCut ); int RetValue = Dar_CutFilter( pObj, pCut );
assert( !RetValue ); assert( !RetValue );
} }
@ -825,7 +825,7 @@ Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj )
return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) ); return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) ); Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) ); Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
return Dar_ObjComputeCuts( p, pObj ); return Dar_ObjComputeCuts( p, pObj, 0 );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

2
src/opt/dar/darInt.h
View File

@ -137,7 +137,7 @@ extern void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot );
extern void Dar_ManCutsFree( Dar_Man_t * p ); extern void Dar_ManCutsFree( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj ); extern Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj ); extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ); extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj, int fSkipTtMin );
extern void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
/*=== darData.c ===========================================================*/ /*=== darData.c ===========================================================*/
extern Vec_Int_t * Dar_LibReadNodes(); extern Vec_Int_t * Dar_LibReadNodes();

4
src/proof/fra/fraClaus.c
View File

@ -637,7 +637,7 @@ ABC_PRT( "Lat-cla", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 ); pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
// pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 ); // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
if ( p->fVerbose ) if ( p->fVerbose )
{ {
@ -771,7 +771,7 @@ if ( p->fVerbose )
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 ); // pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose ); pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
if ( p->fVerbose ) if ( p->fVerbose )
{ {

2
src/proof/pdr/pdrCnf.c
View File

@ -300,7 +300,7 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
assert( pSat ); assert( pSat );
if ( p->pCnf2 == NULL ) if ( p->pCnf2 == NULL )
{ {
p->pCnf2 = Cnf_DeriveOther( p->pAig ); p->pCnf2 = Cnf_DeriveOther( p->pAig, 0 );
p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) ); p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
p->vVar2Ids = Vec_PtrAlloc( 256 ); p->vVar2Ids = Vec_PtrAlloc( 256 );
} }

2
src/sat/cnf/cnf.h
View File

@ -128,7 +128,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
/*=== cnfCore.c ========================================================*/ /*=== cnfCore.c ========================================================*/
extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ); extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig );
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ); extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig ); extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin );
extern Cnf_Man_t * Cnf_ManRead(); extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory(); extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/ /*=== cnfCut.c ========================================================*/

8
src/sat/cnf/cnfCore.c
View File

@ -60,7 +60,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 ); pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = clock() - clk; p->timeCuts = clock() - clk;
// find the mapping // find the mapping
@ -113,7 +113,7 @@ Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 ); pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = clock() - clk; p->timeCuts = clock() - clk;
// find the mapping // find the mapping
@ -150,7 +150,7 @@ p->timeSave = clock() - clk;
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig ) Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
{ {
Cnf_Man_t * p; Cnf_Man_t * p;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
@ -166,7 +166,7 @@ Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig )
// generate cuts for all nodes, assign cost, and find best cuts // generate cuts for all nodes, assign cost, and find best cuts
clk = clock(); clk = clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 ); pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
p->timeCuts = clock() - clk; p->timeCuts = clock() - clk;
// find the mapping // find the mapping