summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/saig/saigBmc3.c189
-rw-r--r--src/opt/dar/darCut.c85
2 files changed, 201 insertions, 73 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 5b36c01a..f97bd5da 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -42,13 +42,19 @@ struct Gia_ManBmc_t_
Vec_Int_t * vId2Num; // number of each node
Vec_Ptr_t * vTerInfo; // ternary information
Vec_Ptr_t * vId2Var; // SAT vars for each object
+ // hash table
+ unsigned * pTable;
+ int nTable;
+ int nHashHit;
+ int nHashMiss;
+ int nHashOver;
+ int nBufNum; // the number of simple nodes
+ int nDupNum; // the number of simple nodes
// SAT solver
sat_solver * pSat; // SAT solver
int nSatVars; // SAT variables
int nObjNums; // SAT objects
int nWordNum; // unsigned words for ternary simulation
- int nBufNum; // the number of simple nodes
- int nDupNum; // the number of simple nodes
char * pSopSizes, ** pSops; // CNF representation
};
@@ -692,6 +698,9 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// terminary simulation
p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
+ // hash table
+ p->nTable = 1000003;
+ p->pTable = ABC_CALLOC( unsigned, 6 * p->nTable ); // 2.4 Mb
return p;
}
@@ -708,6 +717,9 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
***********************************************************************/
void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
{
+ if ( p->pPars->fVerbose )
+ printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d.\n",
+ p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver );
// Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
@@ -722,10 +734,11 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
Vec_PtrFreeFree( p->vTerInfo );
sat_solver_delete( p->pSat );
- free( p->pSopSizes );
- free( p->pSops[1] );
- free( p->pSops );
- free( p );
+ ABC_FREE( p->pTable );
+ ABC_FREE( p->pSopSizes );
+ ABC_FREE( p->pSops[1] );
+ ABC_FREE( p->pSops );
+ ABC_FREE( p );
}
@@ -809,23 +822,24 @@ static inline int Saig_ManBmcCof0( int t, int v )
static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
return 0xffff & ((t & ~s_Truth[v]) | ((t & ~s_Truth[v]) << (1<<v)));
}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
static inline int Saig_ManBmcCof1( int t, int v )
{
static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
return 0xffff & ((t & s_Truth[v]) | ((t & s_Truth[v]) >> (1<<v)));
}
+static inline int Saig_ManBmcCofEqual( int t, int v )
+{
+ assert( v >= 0 && v <= 3 );
+ if ( v == 0 )
+ return ((t & 0xAAAA) >> 1) == (t & 0x5555);
+ if ( v == 1 )
+ return ((t & 0xCCCC) >> 2) == (t & 0x3333);
+ if ( v == 2 )
+ return ((t & 0xF0F0) >> 4) == (t & 0x0F0F);
+ if ( v == 3 )
+ return ((t & 0xFF00) >> 8) == (t & 0x00FF);
+ return -1;
+}
/**Function*************************************************************
@@ -838,7 +852,7 @@ static inline int Saig_ManBmcCof1( int t, int v )
SeeAlso []
***********************************************************************/
-static inline int Saig_ManBmcDeriveTruth( int uTruth, int Lits[] )
+static inline int Saig_ManBmcReduceTruth( int uTruth, int Lits[] )
{
int v;
for ( v = 0; v < 4; v++ )
@@ -854,7 +868,9 @@ static inline int Saig_ManBmcDeriveTruth( int uTruth, int Lits[] )
}
for ( v = 0; v < 4; v++ )
if ( Lits[v] == -1 )
- assert( Saig_ManBmcCof0(uTruth, v) == Saig_ManBmcCof1(uTruth, v) );
+ assert( Saig_ManBmcCofEqual(uTruth, v) );
+ else if ( Saig_ManBmcCofEqual(uTruth, v) )
+ Lits[v] = -1;
return uTruth;
}
@@ -978,6 +994,51 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
}
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Saig_ManBmcHashKey( unsigned * pArray )
+{
+ static s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
+ unsigned i, Key = 0;
+ for ( i = 0; i < 5; i++ )
+ Key += pArray[i] * s_Primes[i];
+ return Key;
+}
+static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, unsigned * pArray )
+{
+ unsigned * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
+/*
+int i;
+for ( i = 0; i < 5; i++ )
+printf( "%6d ", pArray[i] );
+printf( "\n" );
+*/
+ if ( memcmp( pTable, pArray, 20 ) )
+ {
+ if ( pTable[0] == 0 )
+ p->nHashMiss++;
+ else
+ p->nHashOver++;
+ memcpy( pTable, pArray, 20 );
+ pTable[5] = 0;
+ }
+ else
+ p->nHashHit++;
+
+ assert( pTable + 5 < pTable + 6 * p->nTable );
+ return (int *)(pTable + 5);
+}
+
/**Function*************************************************************
Synopsis [Derives CNF for one node.]
@@ -989,10 +1050,10 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
SeeAlso []
***********************************************************************/
-int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int fAddClauses )
+int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
{
- int * pMapping, i, iLit, Lits[4], uTruth;
- assert( fAddClauses );
+ extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
+ int * pMapping, * pLookup, i, iLit, Lits[5], uTruth;
iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
if ( iLit != ~0 )
return iLit;
@@ -1000,14 +1061,14 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
if ( Aig_ObjIsCi(pObj) )
{
if ( Saig_ObjIsPi(p->pAig, pObj) )
- iLit = fAddClauses ? toLit( p->nSatVars++ ) : ABC_INFINITY;
+ iLit = toLit( p->nSatVars++ );
else
- iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1, fAddClauses );
+ iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
}
if ( Aig_ObjIsCo(pObj) )
{
- iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame, fAddClauses );
+ iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
if ( Aig_ObjFaninC0(pObj) )
iLit = lit_neg(iLit);
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
@@ -1018,62 +1079,44 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
if ( pMapping[i+1] == -1 )
Lits[i] = -1;
else
- Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame, fAddClauses );
- // derive new truth table
-//uTruth = 0xffff & (unsigned)pMapping[0];
-//printf( "Truth : " );
-//Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
- uTruth = Saig_ManBmcDeriveTruth( 0xffff & (unsigned)pMapping[0], Lits );
+ Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
+ uTruth = 0xffff & (unsigned)pMapping[0];
+ // propagate constants
+ uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
if ( uTruth == 0 || uTruth == 0xffff )
{
iLit = (uTruth == 0xffff);
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
}
- // create CNF
- if ( fAddClauses )
+ // canonicize inputs
+ uTruth = Dar_CutSortVars( uTruth, Lits );
+ assert( uTruth != 0 && uTruth != 0xffff );
+ if ( uTruth == 0xAAAA || uTruth == 0x5555 )
{
- if ( uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
- uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
- uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
- uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00 )
- {
- p->nBufNum++;
-
- if ( uTruth == 0xAAAA )
- iLit = Lits[0];
- else if ( uTruth == 0xCCCC )
- iLit = Lits[1];
- else if ( uTruth == 0xF0F0 )
- iLit = Lits[2];
- else if ( uTruth == 0xFF00 )
- iLit = Lits[3];
- else if ( (0xffff & ~uTruth) == 0xAAAA )
- iLit = Abc_LitNot(Lits[0]);
- else if ( (0xffff & ~uTruth) == 0xCCCC )
- iLit = Abc_LitNot(Lits[1]);
- else if ( (0xffff & ~uTruth) == 0xF0F0 )
- iLit = Abc_LitNot(Lits[2]);
- else if ( (0xffff & ~uTruth) == 0xFF00 )
- iLit = Abc_LitNot(Lits[3]);
-
- }
- else
+ iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
+ p->nBufNum++;
+ }
+ else
+ {
+ assert( !(uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
+ uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
+ uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
+ uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00) );
+
+ Lits[4] = uTruth;
+ pLookup = Saig_ManBmcLookup( p, Lits );
+ if ( *pLookup == 0 )
{
- iLit = toLit( p->nSatVars++ );
- Saig_ManBmcAddClauses( p, uTruth, Lits, iLit );
+ *pLookup = toLit( p->nSatVars++ );
+ Saig_ManBmcAddClauses( p, uTruth, Lits, *pLookup );
if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3])) ||
(Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) ||
(Lits[2] > 1 && (Lits[2] == Lits[3])) )
p->nDupNum++;
}
-
- }
- else
- {
- iLit = ABC_INFINITY;
+ iLit = *pLookup;
}
-// assert( iLit != ABC_INFINITY );
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
}
@@ -1142,7 +1185,7 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
if ( Value != SAIG_TER_UND )
return (int)(Value == SAIG_TER_ONE);
// construct CNF if value is ternary
- return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 1 );
+ return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
}
@@ -1358,8 +1401,8 @@ clkOther += clock() - clk2;
// printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
- printf( "S =%6d. ", p->nBufNum );
- printf( "D =%6d. ", p->nDupNum );
+// printf( "S =%6d. ", p->nBufNum );
+// printf( "D =%6d. ", p->nDupNum );
printf( "\n" );
fflush( stdout );
}
@@ -1422,8 +1465,8 @@ clkOther += clock() - clk2;
// printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
- printf( "Simples = %6d. ", p->nBufNum );
- printf( "Dups = %6d. ", p->nDupNum );
+// printf( "Simples = %6d. ", p->nBufNum );
+// printf( "Dups = %6d. ", p->nDupNum );
printf( "\n" );
fflush( stdout );
}
diff --git a/src/opt/dar/darCut.c b/src/opt/dar/darCut.c
index f0d10100..1056ef32 100644
--- a/src/opt/dar/darCut.c
+++ b/src/opt/dar/darCut.c
@@ -430,6 +430,32 @@ static inline unsigned Dar_CutTruthSwapAdjacentVars( unsigned uTruth, int iVar )
/**Function*************************************************************
+ Synopsis [Swaps polarity of the variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Dar_CutTruthSwapPolarity( unsigned uTruth, int iVar )
+{
+ assert( iVar >= 0 && iVar <= 3 );
+ if ( iVar == 0 )
+ return ((uTruth & 0xAAAA) >> 1) | ((uTruth & 0x5555) << 1);
+ if ( iVar == 1 )
+ return ((uTruth & 0xCCCC) >> 2) | ((uTruth & 0x3333) << 2);
+ if ( iVar == 2 )
+ return ((uTruth & 0xF0F0) >> 4) | ((uTruth & 0x0F0F) << 4);
+ if ( iVar == 3 )
+ return ((uTruth & 0xFF00) >> 8) | ((uTruth & 0x00FF) << 8);
+ assert( 0 );
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Expands the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
@@ -483,6 +509,65 @@ static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned
/**Function*************************************************************
+ Synopsis [Sort variables by their ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Dar_CutSortVars( unsigned uTruth, int * pVars )
+{
+ int i, Temp, fChange, Counter = 0;
+ // replace -1 by large number
+ for ( i = 0; i < 4; i++ )
+ {
+ if ( pVars[i] == -1 )
+ pVars[i] = 0x3FFFFFFF;
+ else
+ if ( Abc_LitIsCompl(pVars[i]) )
+ {
+ pVars[i] = Abc_LitNot( pVars[i] );
+ uTruth = Dar_CutTruthSwapPolarity( uTruth, i );
+ }
+ }
+
+ // permute variables
+ do {
+ fChange = 0;
+ for ( i = 0; i < 3; i++ )
+ {
+ if ( pVars[i] <= pVars[i+1] )
+ continue;
+ Counter++;
+ fChange = 1;
+
+ Temp = pVars[i];
+ pVars[i] = pVars[i+1];
+ pVars[i+1] = Temp;
+
+ uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, i );
+ }
+ } while ( fChange );
+
+ // replace large number by -1
+ for ( i = 0; i < 4; i++ )
+ {
+ if ( pVars[i] == 0x3FFFFFFF )
+ pVars[i] = -1;
+// printf( "%d ", pVars[i] );
+ }
+// printf( "\n" );
+
+ return uTruth;
+}
+
+
+
+/**Function*************************************************************
+
Synopsis [Performs truth table computation.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 16:49:08 +0000