summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaEsop.c2
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/exor/exor.c48
-rw-r--r--src/base/exor/exor.h6
-rw-r--r--src/base/exor/exorLink.c20
-rw-r--r--src/base/exor/exorList.c7
-rw-r--r--src/base/exor/exorUtil.c14
7 files changed, 78 insertions, 23 deletions
diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c
index db69bf02..13627c0c 100644
--- a/src/aig/gia/giaEsop.c
+++ b/src/aig/gia/giaEsop.c
@@ -167,7 +167,7 @@ Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover )
}
}
}
- assert( Vec_WecSize(vRes) == Vec_WecCap(vRes) );
+ assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) );
return vRes;
}
Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2dab60c9..8032a426 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40460,13 +40460,13 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] <file>\n" );
+ Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] [-q] <file>\n" );
Abc_Print( -2, " performs heuristic exclusive sum-of-project minimization\n" );
Abc_Print( -2, " -Q N : minimization quality [default = %d]\n", Quality);
Abc_Print( -2, " increasing this number improves quality and adds to runtime\n");
Abc_Print( -2, " -V N : verbosity level [default = %d]\n", Verbosity);
Abc_Print( -2, " 0 = no output; 1 = outline; 2 = verbose\n");
-// Abc_Print( -2, " -q : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" );
+ Abc_Print( -2, " -q : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" );
Abc_Print( -2, " <file>: the output file name in ESOP-PLA format\n");
Abc_Print( -2, "\n" );
return 1;
diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c
index db93d034..2b8f0903 100644
--- a/src/base/exor/exor.c
+++ b/src/base/exor/exor.c
@@ -90,16 +90,48 @@ static int QCost[16][16] =
{ 56, 56, 56, 56, 58, 60, 62, 64}, // 7
{ 0 }
};
-int CountNegLits( Vec_Int_t * vCube )
+int GetQCost( int nVars, int nNegs )
{
- int i, Entry, nLits = 0;
- Vec_IntForEachEntry( vCube, Entry, i )
- nLits += Abc_LitIsCompl(Entry);
- return nLits;
+ int Extra;
+ assert( nVars >= nNegs );
+ if ( nVars == 0 )
+ return 1;
+ if ( nVars == 1 )
+ {
+ if ( nNegs == 0 ) return 1;
+ if ( nNegs == 1 ) return 2;
+ }
+ if ( nVars == 2 )
+ {
+ if ( nNegs <= 1 ) return 5;
+ if ( nNegs == 2 ) return 6;
+ }
+ if ( nVars == 3 )
+ {
+ if ( nNegs <= 1 ) return 14;
+ if ( nNegs == 2 ) return 16;
+ if ( nNegs == 3 ) return 18;
+ }
+ Extra = nNegs - nVars/2;
+ return 20 + 12 * (nVars - 4) + (Extra > 0 ? 2 * Extra : 0);
+
+}
+void GetQCostTest()
+{
+ int i, k, Limit = 10;
+ for ( i = 0; i < Limit; i++ )
+ {
+ for ( k = 0; k <= i; k++ )
+ printf( "%4d ", GetQCost(i, k) );
+ printf( "\n" );
+ }
}
int ComputeQCost( Vec_Int_t * vCube )
{
- return QCost[Abc_MinInt(Vec_IntSize(vCube), 7)][Abc_MinInt(CountNegLits(vCube), 7)];
+ int i, Entry, nLitsN = 0;
+ Vec_IntForEachEntry( vCube, Entry, i )
+ nLitsN += Abc_LitIsCompl(Entry);
+ return GetQCost( Vec_IntSize(vCube), nLitsN );
}
int ComputeQCostBits( Cube * p )
{
@@ -114,7 +146,7 @@ int ComputeQCostBits( Cube * p )
nLits++;
}
nLits += nLitsN;
- return QCost[Abc_MinInt(nLits, 7)][Abc_MinInt(nLitsN, 7)];
+ return GetQCost( nLits, nLitsN );
}
/**Function*************************************************************
@@ -858,6 +890,8 @@ int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOu
g_CoverInfo.Quality = Quality;
g_CoverInfo.Verbosity = Verbosity;
g_CoverInfo.fUseQCost = fUseQCost;
+ if ( fUseQCost )
+ s_fDecreaseLiterals = 1;
if ( g_CoverInfo.Verbosity )
{
printf( "\nEXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" );
diff --git a/src/base/exor/exor.h b/src/base/exor/exor.h
index 15a62bbe..019b66c5 100644
--- a/src/base/exor/exor.h
+++ b/src/base/exor/exor.h
@@ -167,6 +167,12 @@ extern int FindDiffVars( int *pDiffVars, Cube* pC1, Cube* pC2 );
// determines the variables that are different in cubes pC1 and pC2
// returns the number of variables
+extern int ComputeQCost( Vec_Int_t * vCube );
+extern int ComputeQCostBits( Cube * p );
+
+extern int CountLiterals();
+extern int CountQCost();
+
////////////////////////////////////////////////////////////////////////
/// VARVALUE and CUBEDIST enum typedefs ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/exor/exorLink.c b/src/base/exor/exorLink.c
index fef0d4ca..2d260a27 100644
--- a/src/base/exor/exorLink.c
+++ b/src/base/exor/exorLink.c
@@ -335,7 +335,6 @@ static int DiffVarBits[5];
static drow MaskLiterals;
// the base for counting literals
static int StartingLiterals;
-static int StartingQCost;
// the number of literals in each cube
static int CubeLiterals[32];
static int BitShift;
@@ -525,9 +524,6 @@ int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dis
NewZ += BIT_COUNT(Temp);
}
}
- // set the number of literals
- ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
- ELCubes[CubeNum]->z = NewZ;
// set the variables that should be there
for ( i = 0; i < nDiffVarsIn; i++ )
@@ -536,6 +532,11 @@ int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dis
ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] );
}
+ // set the number of literals
+ ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
+ ELCubes[CubeNum]->z = NewZ;
+ ELCubes[CubeNum]->q = ComputeQCostBits( ELCubes[CubeNum] );
+
// assign the ID
ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++;
// skip through zero-ID
@@ -645,11 +646,6 @@ int ExorLinkCubeIteratorNext( Cube** pGroup )
NewZ += BIT_COUNT(Temp);
}
}
- // set the number of literals and output ones
- ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
- ELCubes[CubeNum]->z = NewZ;
-
- assert( NewZ != 255 );
// set the variables that should be there
for ( i = 0; i < nDiffVarsIn; i++ )
@@ -658,6 +654,12 @@ int ExorLinkCubeIteratorNext( Cube** pGroup )
ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] );
}
+ // set the number of literals and output ones
+ ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
+ ELCubes[CubeNum]->z = NewZ;
+ ELCubes[CubeNum]->q = ComputeQCostBits( ELCubes[CubeNum] );
+ assert( NewZ != 255 );
+
// assign the ID
ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++;
// skip through zero-ID
diff --git a/src/base/exor/exorList.c b/src/base/exor/exorList.c
index 6dc9f231..18b11c6f 100644
--- a/src/base/exor/exorList.c
+++ b/src/base/exor/exorList.c
@@ -393,6 +393,8 @@ SUCCESS:
printf( " NoResh= %4d", s_cAttempts - s_cReshapes );
printf( " Cubes= %3d", g_CoverInfo.nCubesInUse );
printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+ printf( " Lits= %5d", CountLiterals() );
+ printf( " QCost = %6d", CountQCost() );
printf( "\n" );
}
@@ -510,6 +512,8 @@ END_OF_LOOP: {}
printf( " NoResh= %4d", s_cAttempts - s_cReshapes );
printf( " Cubes= %3d", g_CoverInfo.nCubesInUse );
printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+ printf( " Lits= %5d", CountLiterals() );
+ printf( " QCost = %6d", CountQCost() );
printf( "\n" );
}
@@ -619,6 +623,8 @@ END_OF_LOOP: {}
printf( " NoResh= %4d", s_cAttempts - s_cReshapes );
printf( " Cubes= %3d", g_CoverInfo.nCubesInUse );
printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+ printf( " Lits= %5d", CountLiterals() );
+ printf( " QCost = %6d", CountQCost() );
printf( "\n" );
}
@@ -709,6 +715,7 @@ int CheckForCloseCubes( Cube* p, int fAddCube )
p->a--;
if ( s_DiffVarValueP_new == VAR_NEG || s_DiffVarValueP_new == VAR_POS )
p->a++;
+ p->q = ComputeQCostBits(p);
}
// move q to the free cube list
diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c
index 45c9542b..105a6490 100644
--- a/src/base/exor/exorUtil.c
+++ b/src/base/exor/exorUtil.c
@@ -75,7 +75,15 @@ extern varvalue GetVar( Cube* pC, int Var );
///////////////////////////////////////////////////////////////////
int CountLiterals()
-// nCubesAlloc is the number of allocated cubes
+{
+ Cube* p;
+ int LitCounter = 0;
+ for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() )
+ LitCounter += p->a;
+ return LitCounter;
+}
+
+int CountLiteralsCheck()
{
Cube* p;
int Value, v;
@@ -109,9 +117,7 @@ int CountLiterals()
}
int CountQCost()
-// nCubesAlloc is the number of allocated cubes
{
- extern int ComputeQCostBits( Cube * p );
Cube* p;
int QCost = 0;
int QCostControl = 0;
@@ -191,7 +197,7 @@ int WriteResultIntoFile( char * pFileName )
time( &ltime );
TimeStr = asctime( localtime( &ltime ) );
// get the number of literals
- g_CoverInfo.nLiteralsAfter = CountLiterals();
+ g_CoverInfo.nLiteralsAfter = CountLiteralsCheck();
g_CoverInfo.QCostAfter = CountQCost();
fprintf( pFile, "# EXORCISM-4 output for command line arguments: " );
fprintf( pFile, "\"-Q %d -V %d\"\n", g_CoverInfo.Quality, g_CoverInfo.Verbosity );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:16:23 +0000