summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-04 14:53:07 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-04 14:53:07 -0700
commit9ebcd9eca983890738bc76f84f4e276a9cb693d7 (patch)
tree966c59c9020e85c857678fb1edffcc2138dce545
parentc921058019c22ca917fb63f1139a46cb9f766ae2 (diff)
downloadabc-9ebcd9eca983890738bc76f84f4e276a9cb693d7.tar.gz
abc-9ebcd9eca983890738bc76f84f4e276a9cb693d7.tar.bz2
abc-9ebcd9eca983890738bc76f84f4e276a9cb693d7.zip
Various changes to enable sensitization-based refinement in &gla.
-rw-r--r--src/aig/gia/giaAbsGla.c503
-rw-r--r--src/aig/gia/giaAbsVta.c6
-rw-r--r--src/aig/saig/saigAbsVfa.c2
-rw-r--r--src/opt/dar/dar.h2
-rw-r--r--src/opt/dar/darCore.c6
-rw-r--r--src/opt/dar/darCut.c10
-rw-r--r--src/opt/dar/darInt.h2
-rw-r--r--src/proof/fra/fraClaus.c4
-rw-r--r--src/proof/pdr/pdrCnf.c2
-rw-r--r--src/sat/cnf/cnf.h2
-rw-r--r--src/sat/cnf/cnfCore.c8
11 files changed, 191 insertions, 356 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 3b3799ea..815111b9 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -36,8 +36,8 @@ struct Rfn_Obj_t_
unsigned Value : 1; // value
unsigned fVisit : 1; // visited
unsigned fPPi : 1; // PPI
- unsigned Prio : 18; // priority
- unsigned Sign : 10; // priority
+ unsigned Prio : 16; // priority
+ unsigned Sign : 12; // traversal signature
};
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 * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array
- Vec_Int_t * vPrevCore; // previous core
+ Vec_Int_t * vObjCounts; // object counters
// refinement
Vec_Int_t * pvRefis; // vectors of each object
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*************************************************************
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 []
***********************************************************************/
-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) )
- return 1;
+ return;
Gia_ObjSetTravIdCurrent(p, pGiaObj);
- if ( Gia_ObjIsCi(pGiaObj) )
- return 0;
assert( Gia_ObjIsAnd(pGiaObj) );
- Value0 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds );
- Value1 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds );
- if ( Value0 || Value1 )
- {
- assert( Gia_ObjIsAnd(pGiaObj) );
- Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
- }
- return Value0 || Value1;
+ Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds );
+ Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds );
+ Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
}
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( vPPis );
+ Vec_IntSort( vCos, 0 );
// mark const/PIs/PPIs
Gia_ManIncrementTravId( p->pGia );
@@ -447,7 +442,8 @@ 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 )
-{
+{
+ int Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
assert( (int)pRef->Sign == Sign );
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 < Vec_IntSize(p->vPrioSels) );
+ Vec_IntAddToEntry( p->vObjCounts, f, 1 );
if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
{
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 * 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 ( !fSel0 )
+ if ( pRef0->Prio > 0 )
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 );
}
else // select one value
{
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 );
- else
+ }
+ else
+ {
+ if ( pRef1->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
}
}
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{
-// if ( !fSel0 )
+ if ( pRef0->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
}
else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{
-// if ( !fSel1 )
+ if ( pRef1->Prio > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
}
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 );
}
+
+/**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*************************************************************
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;
Rfn_Obj_t * pRef, * pRef0, * pRef1;
Gia_Obj_t * pObj;
-// Gla_Obj_t * pGla;
int i, f;
Sign++;
@@ -541,6 +602,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
vPPis = Vec_IntAlloc( 1000 );
vRoAnds = Vec_IntAlloc( 1000 );
Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds );
+
/*
// check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
@@ -571,22 +633,17 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// primary input
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->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
- pRef->Prio = 0;
- pRef->Sign = Sign;
+ pRef->Prio = 0;
+ pRef->Sign = Sign;
assert( pRef->fVisit == 0 );
}
// primary input
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
- int ObjId = Gia_ObjId(p->pGia, pObj);
- 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( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
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;
assert( pRef->fVisit == 0 );
}
-
// internal nodes
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) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
if ( Gia_ObjIsRo(p->pGia, pObj) )
@@ -619,13 +671,6 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef->Value = pRef0->Value;
pRef->Prio = pRef0->Prio;
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;
}
@@ -634,51 +679,12 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
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 " );
Gia_ObjPrint( p->pGia, pObj );
- }
}
if ( pRef->Value == 1 )
@@ -702,11 +708,13 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
assert( pRef->fVisit == 0 );
pRef->Sign = Sign;
}
- }
+ }
+
// make sure the output value is 1
pObj = Gia_ManPo( p->pGia, 0 );
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
if ( pRef->Prio == 0 )
@@ -722,57 +730,15 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// select objects
vRes = Vec_IntAlloc( 100 );
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 );
-
+/*
+ for ( f = 0; f < p->pPars->iFrame; f++ )
+ printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
+ printf( "\n" );
+*/
if ( fVerify )
- {
- 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 );
- }
+ Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vRes );
// remap them into GLA objects
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*************************************************************
Synopsis [Adds clauses for the given obj in the given frame.]
@@ -924,7 +818,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
- {
+ {
int Offset = Vec_IntEntry(vMapping, Gia_ObjId(p, pObj));
if ( Offset == 0 )
continue;
@@ -953,7 +847,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
else if ( Gia_ObjIsCo(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) );
Vec_IntPush( pNew->vLutConfigs, i );
}
@@ -978,14 +872,14 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
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;
Aig_Man_t * pAig;
Gia_Obj_t * pObj;
Gla_Obj_t * pGla;
Vec_Int_t * vMappingNew;
- int i, * pLits, * pObj2Count, * pObj2Clause;
+ int i, k, Offset, * pMapping, * pLits, * pObj2Count, * pObj2Clause;
// start
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->vAddedNew = Vec_IntAlloc( 100 );
p->vPrioSels = Vec_IntAlloc( 100 );
+ p->vObjCounts = Vec_IntAlloc( 100 );
// internal data
pAig = Gia_ManToAigSimple( pGia0 );
- p->pCnf = Cnf_DeriveOther( pAig );
+ p->pCnf = Cnf_DeriveOther( pAig, 1 );
Aig_ManStop( pAig );
-
// create working GIA
p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
//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 );
p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
// 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) );
- pObj2Count = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) );
- pObj2Clause = ABC_ALLOC( int, Gia_ManObjNum(p->pGia) );
+ pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
+ pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p->pGia) );
Gia_ManForEachObj( pGia0, pObj, i )
{
+ // skip internal nodes not used in the mapping
if ( !~pObj->Value )
continue;
// replace positive literal by variable
assert( !Abc_LitIsCompl(pObj->Value) );
pObj->Value = Abc_Lit2Var(pObj->Value);
assert( (int)pObj->Value < Gia_ManObjNum(p->pGia) );
- // update mappings
- Vec_IntWriteEntry( vMappingNew, pObj->Value, Vec_IntEntry(p->pCnf->vMapping, i) );
+ // update arrays
pObj2Count[pObj->Value] = p->pCnf->pObj2Count[i];
pObj2Clause[pObj->Value] = p->pCnf->pObj2Clause[i];
if ( Vec_IntEntry(pGia0->vGateClasses, i) )
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;
ABC_FREE( p->pCnf->pObj2Count ); p->pCnf->pObj2Count = pObj2Count;
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);
if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
continue;
- if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
+ if ( Gia_ObjIsCo(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) );
+ pGla->nFanins = 1;
+ pGla->Fanins[0] = Gia_ObjFanin0(pObj)->Value;
+ 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;
}
assert( Gia_ObjIsRo(p->pGia, pObj) );
@@ -1114,7 +1037,7 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
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;
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 );
// internal data
pAig = Gia_ManToAigSimple( p->pGia );
- p->pCnf = Cnf_DeriveOther( pAig );
+ p->pCnf = Cnf_DeriveOther( pAig, 1 );
Aig_ManStop( pAig );
// count the number of variables
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 )
{
Gla_Obj_t * pGla;
+ int i;
// if ( p->pPars->fVerbose )
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 );
+ for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
+ ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla )
ABC_FREE( pGla->vFrames.pArray );
Cnf_DataFree( p->pCnf );
if ( p->pGia0 != NULL )
Gia_ManStop( p->pGia );
sat_solver2_delete( p->pSat );
+ Vec_IntFreeP( &p->vObjCounts );
Vec_IntFreeP( &p->vCla2Obj );
- Vec_IntFreeP( &p->vPrevCore );
Vec_IntFreeP( &p->vAddedNew );
Vec_IntFreeP( &p->vPrioSels );
Vec_IntFreeP( &p->vTemp );
@@ -1359,8 +1285,6 @@ int Gla_ManCountPPis( Gla_Man_t * p )
Vec_IntFree( vPPis );
return RetValue;
}
-
-
void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
{
static int Round = 0;
@@ -1383,99 +1307,6 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
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*************************************************************
@@ -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 );
int iVar, iVar1, iVar2;
- if ( 4786 == iObj && iFrame == 2 )
- {
- int s = 0;
- }
if ( pGlaObj->fConst )
{
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);
memOth += Vec_IntCap(p->vCla2Obj) * 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->vAbs) * sizeof(int);
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 );
Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs );
-// nClaOld = Vec_IntSize( p->vCla2Obj );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
@@ -1874,6 +1699,12 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gla_ManRollBack( p );
goto finish;
}
+ // check timeout
+ if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+ {
+ Gla_ManRollBack( p ); // 1155046
+ goto finish;
+ }
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
@@ -1884,16 +1715,16 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p->nCexes++;
// perform the refinement
clk2 = clock();
-/*
+
vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL )
{
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
}
-*/
- vPPis = Gla_ManCollectPPis( p, NULL );
- Gla_ManExplorePPis( p, vPPis );
+
+// vPPis = Gla_ManCollectPPis( p, NULL );
+// Gla_ManExplorePPis( p, vPPis );
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
@@ -1922,8 +1753,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Gla_ManRollBack( p );
Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
// load this timeframe
- Vec_IntFreeP( &p->vPrevCore );
- p->vPrevCore = Gla_ManRegionStart( p, vCore );
Gia_GlaAddToAbs( p, vCore, 0 );
Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 8a41ec40..40e5a45c 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1674,6 +1674,12 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vga_ManRollBack( p, nObjOld );
goto finish;
}
+ // check timeout
+ if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+ {
+ Vga_ManRollBack( p, nObjOld );
+ goto finish;
+ }
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c
index 897c1638..24414c5a 100644
--- a/src/aig/saig/saigAbsVfa.c
+++ b/src/aig/saig/saigAbsVfa.c
@@ -252,7 +252,7 @@ Abs_VfaMan_t * Abs_VfaManStart( Aig_Man_t * pAig )
Vec_IntPush( p->vVec2Var, -1 );
// transfer values from CNF
- p->pCnf = Cnf_DeriveOther( pAig );
+ p->pCnf = Cnf_DeriveOther( pAig, 0 );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
if ( p->pCnf->pObj2Clause[i] == -1 )
Vec_IntWriteEntry( p->vObj2Vec, i, -1 );
diff --git a/src/opt/dar/dar.h b/src/opt/dar/dar.h
index 5c2c9bcc..ed1f4e74 100644
--- a/src/opt/dar/dar.h
+++ b/src/opt/dar/dar.h
@@ -91,7 +91,7 @@ extern void Dar_BalancePrintStats( Aig_Man_t * p );
/*=== darCore.c ========================================================*/
extern void Dar_ManDefaultRwrParams( 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 ========================================================*/
extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index 54e9cf84..958ab70a 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -281,8 +281,8 @@ int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
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_RwrPar_t Pars, * pPars = &Pars;
Aig_Obj_t * pObj;
@@ -306,7 +306,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
Dar_ObjPrepareCuts( p, pObj );
// compute cuts for each nodes in the topological order
Aig_ManForEachNode( pAig, pObj, i )
- Dar_ObjComputeCuts( p, pObj );
+ Dar_ObjComputeCuts( p, pObj, fSkipTtMin );
// print verbose stats
if ( fVerbose )
{
diff --git a/src/opt/dar/darCut.c b/src/opt/dar/darCut.c
index 1056ef32..da1c9eaf 100644
--- a/src/opt/dar/darCut.c
+++ b/src/opt/dar/darCut.c
@@ -735,14 +735,14 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
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 * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
- int i, k, RetValue;
+ int i, k;
assert( !Aig_IsComplement(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) );
// 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 );
}
@@ -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) );
Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
- return Dar_ObjComputeCuts( p, pObj );
+ return Dar_ObjComputeCuts( p, pObj, 0 );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dar/darInt.h b/src/opt/dar/darInt.h
index 08af70df..caea213c 100644
--- a/src/opt/dar/darInt.h
+++ b/src/opt/dar/darInt.h
@@ -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 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( 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 );
/*=== darData.c ===========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index 571cc510..f651b0ad 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -637,7 +637,7 @@ ABC_PRT( "Lat-cla", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts
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 );
if ( p->fVerbose )
{
@@ -771,7 +771,7 @@ if ( p->fVerbose )
// generate cuts for all nodes, assign cost, and find best cuts
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 );
if ( p->fVerbose )
{
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index 2b039c01..66bea130 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -300,7 +300,7 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
assert( pSat );
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->vVar2Ids = Vec_PtrAlloc( 256 );
}
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 54aaf5ca..478755d6 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -128,7 +128,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
/*=== cnfCore.c ========================================================*/
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_DeriveOther( Aig_Man_t * pAig );
+extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin );
extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/
diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index d1dd8561..65d7ef60 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -60,7 +60,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
- pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = clock() - clk;
// 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
clk = clock();
- pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = clock() - clk;
// find the mapping
@@ -150,7 +150,7 @@ p->timeSave = clock() - clk;
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_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
clk = clock();
- pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
p->timeCuts = clock() - clk;
// find the mapping