summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaDup.c39
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/proof/ssc/sscCore.c12
-rw-r--r--src/proof/ssc/sscInt.h1
-rw-r--r--src/proof/ssc/sscSim.c45
-rw-r--r--src/proof/ssc/sscUtil.c20
7 files changed, 103 insertions, 19 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 95700aaf..b2905571 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -857,6 +857,7 @@ extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 92248225..c5e5a0b7 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -974,10 +974,32 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
+Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManFillValue( p );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ pNew->nConstrs = p->nConstrs;
+ if ( p->pCexSeq )
+ pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
- Synopsis [Duplicates AIG in the DFS order.]
+ Synopsis [Duplicates the AIG in the DFS order while rehashing.]
Description []
@@ -986,7 +1008,16 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( ~pObj->Value )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@@ -998,11 +1029,13 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ pNew->nConstrs = p->nConstrs;
if ( p->pCexSeq )
pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 239771b5..b18704f7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22161,7 +22161,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConstrs > 0 )
{
if ( Abc_NtkIsComb(pNtk) )
- Abc_Print( -1, "The network is combinational.\n" );
+ Abc_Print( 0, "The network is combinational.\n" );
if ( Abc_NtkConstrNum(pNtk) > 0 )
{
Abc_Print( -1, "The network already has constraints.\n" );
@@ -22172,7 +22172,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The number of constraints specified (%d) should be less than POs (%d).\n", nConstrs, Abc_NtkPoNum(pNtk) );
return 0;
}
- Abc_Print( 0, "Considering the last %d POs as constraint outputs.\n", nConstrs );
+ Abc_Print( 1, "Setting the last %d POs as constraint outputs.\n", nConstrs );
pNtk->nConstrs = nConstrs;
return 0;
}
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index b29a0193..55f0e140 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -83,8 +83,9 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
p->pPars = pPars;
p->pAig = pAig;
p->pCare = pCare;
- p->pFraig = Gia_ManDup( p->pCare );
- Gia_ManHashStart( p->pFraig );
+ p->pFraig = Gia_ManDupDfs( p->pCare );
+ assert( p->pFraig->pHTable == NULL );
+ assert( !Gia_ManHasDangling(p->pFraig) );
Gia_ManInvertPos( p->pFraig );
Ssc_ManStartSolver( p );
if ( p->pSat == NULL )
@@ -170,6 +171,8 @@ clk = clock();
p = Ssc_ManStart( pAig, pCare, pPars );
if ( p == NULL )
return Gia_ManDup( pAig );
+ if ( p->pPars->fVerbose )
+ printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 10), 640 );
// perform simulation
if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
{
@@ -189,6 +192,9 @@ p->timeSimInit += clock() - clk;
Gia_ManConst0(pAig)->Value = 0;
Gia_ManForEachCi( pAig, pObj, i )
pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
+// Gia_ManLevelNum(pAig);
+ // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart)
+ Gia_ManHashStart( p->pFraig );
// perform sweeping
Ssc_GiaResetPiPattern( pAig, pPars->nWords );
Ssc_GiaSavePiPattern( pAig, p->vPivot );
@@ -207,6 +213,7 @@ clk = clock();
Ssc_GiaResetPiPattern( pAig, pPars->nWords );
Ssc_GiaSavePiPattern( pAig, p->vPivot );
p->timeSimSat += clock() - clk;
+//printf( "\n" );
}
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -272,7 +279,6 @@ p->timeSimSat += clock() - clk;
// count the number of representatives
if ( pPars->fVerbose )
{
-// Gia_ManEquivPrintClasses( pAig, 0, 0 );
Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ",
Gia_ManAndNum(pAig), Gia_ManAndNum(pResult),
100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index f0a556a6..1226f4ee 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -116,6 +116,7 @@ extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_
extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
extern void Ssc_GiaSimRound( Gia_Man_t * p );
extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p );
+extern int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords );
/*=== sscUtil.c ===================================================*/
extern Gia_Man_t * Ssc_GenerateOneHot( int nVars );
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
index 9a2c1033..d28db432 100644
--- a/src/proof/ssc/sscSim.c
+++ b/src/proof/ssc/sscSim.c
@@ -82,6 +82,24 @@ static inline int Ssc_SimFindBit( word * pSim, int nWords )
return -1;
}
+static inline int Ssc_SimCountBitsWord( word x )
+{
+ x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
+ x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
+ x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ x = x + (x >> 32);
+ return (int)(x & 0xFF);
+}
+static inline int Ssc_SimCountBits( word * pSim, int nWords )
+{
+ int w, Counter = 0;
+ for ( w = 0; w < nWords; w++ )
+ Counter += Ssc_SimCountBitsWord(pSim[w]);
+ return Counter;
+}
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -245,6 +263,14 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
return vInit;
}
+Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
+{
+ Vec_Int_t * vInit;
+ Ssc_GiaRandomPiPattern( p, 1, NULL );
+ Ssc_GiaSimRound( p );
+ vInit = Ssc_GiaGetOneSim( p );
+ return vInit;
+}
/**Function*************************************************************
@@ -257,13 +283,22 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
+int Ssc_GiaCountCaresSim( Gia_Man_t * p )
{
- Vec_Int_t * vInit;
- Ssc_GiaRandomPiPattern( p, 1, NULL );
+ Gia_Obj_t * pObj;
+ int i, Count, nWords = Gia_ObjSimWords( p );
+ word * pRes = ABC_FALLOC( word, nWords );
+ Gia_ManForEachPo( p, pObj, i )
+ Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
+ Count = Ssc_SimCountBits( pRes, nWords );
+ ABC_FREE( pRes );
+ return Count;
+}
+int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords )
+{
+ Ssc_GiaRandomPiPattern( p, nWords, NULL );
Ssc_GiaSimRound( p );
- vInit = Ssc_GiaGetOneSim( p );
- return vInit;
+ return Ssc_GiaCountCaresSim( p );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
index 0ced578f..52aea52c 100644
--- a/src/proof/ssc/sscUtil.c
+++ b/src/proof/ssc/sscUtil.c
@@ -52,6 +52,7 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
Gia_Obj_t * pObj;
Vec_Int_t * vLits, * vKeep;
sat_solver * pSat;
+ int ConstLit = Abc_Var2Lit(pDat->pVarNums[0], 0);
int i, status;//, Count = 0;
Aig_ManStop( pMan );
@@ -75,10 +76,10 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
return NULL;
}
}
+ Cnf_DataFree( pDat );
status = sat_solver_simplify( pSat );
if ( status == 0 )
{
- Cnf_DataFree( pDat );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
return NULL;
@@ -92,17 +93,15 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) );
if ( status == l_False )
- Vec_IntWriteEntry( vLits, i, Abc_Var2Lit(pDat->pVarNums[0], 0) ); // const1 SAT var is always true
+ Vec_IntWriteEntry( vLits, i, ConstLit ); // const1 SAT var is always true
else
{
assert( status = l_True );
Vec_IntPush( vKeep, i );
}
}
- Cnf_DataFree( pDat );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
-
if ( Vec_IntSize(vKeep) == Gia_ManPoNum(p) )
{
Vec_IntFree( vKeep );
@@ -140,19 +139,28 @@ Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
return pTemp;
Ssc_ManSetDefaultParams( pPars );
pPars->fAppend = 1;
- pPars->fVerbose = 1;
+ pPars->fVerbose = 0;
pTemp->nConstrs = Gia_ManPoNum(pTemp) - 1;
for ( i = 0; i < Gia_ManPoNum(pTemp); i++ )
{
+ // move i-th PO forward
Gia_ManSwapPos( pTemp, i );
+ pTemp = Gia_ManDupDfs( pAux = pTemp );
+ Gia_ManStop( pAux );
+ // minimize this PO
pTemp = Ssc_PerformSweepingConstr( pAux = pTemp, pPars );
Gia_ManStop( pAux );
- pTemp = Gia_ManDupNormalize( pAux = pTemp );
+ pTemp = Gia_ManDupDfs( pAux = pTemp );
Gia_ManStop( pAux );
+ // move i-th PO back
Gia_ManSwapPos( pTemp, i );
+ pTemp = Gia_ManDupDfs( pAux = pTemp );
+ Gia_ManStop( pAux );
+ // report results
printf( "AIG%3d : ", i );
Gia_ManPrintStats( pTemp, 0, 0, 0 );
}
+ pTemp->nConstrs = 0;
return pTemp;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 03:49:23 +0000