Skip to content

A
abc
Commit 81607212 by Alan Mishchenko
Options

Experiment with support minimization.

parent fe5b5ffe
Showing with 287 additions and 7 deletions
abclib.dsp
......@@ -1451,6 +1451,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcEco.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcFault.c
# End Source File
# Begin Source File
......@@ -2739,6 +2743,10 @@ SOURCE=.\src\misc\extra\extraUtilReader.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraUtilSupp.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraUtilTruth.c
# End Source File
# Begin Source File
......@@ -3791,6 +3799,10 @@ SOURCE=.\src\aig\gia\giaIso2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaIso3.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaJf.c
# End Source File
# Begin Source File
......
src/base/abci/abc.c
......@@ -10317,18 +10317,19 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
// Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int nCutMax = 1;
int nLeafMax = 10;
int nLeafMax = 4;
int nDivMax = 2;
int nDecMax = 3;
int nDecMax = 20;
int nNumOnes = 4;
int fNewAlgo = 0;
int fNewOrder = 0;
int fVerbose = 0;
int fVeryVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNaovwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNMaovwh" ) ) != EOF )
{
switch ( c )
{
......@@ -10376,6 +10377,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nDecMax < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
nNumOnes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nNumOnes < 0 )
goto usage;
break;
case 'a':
fNewAlgo ^= 1;
break;
......@@ -10464,6 +10476,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Abc_EnumerateFuncs( int nDecMax, int nDivMax, int fVerbose );
// Abc_EnumerateFuncs( nDecMax, nDivMax, fVerbose );
}
if ( fNewAlgo )
{
extern void Abc_SuppTest( int nOnes, int nVars, int fVerbose );
Abc_SuppTest( nNumOnes, nDecMax, fVerbose );
}
else
{
extern void Bmc_EcoMiterTest();
Bmc_EcoMiterTest();
......@@ -10483,12 +10502,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
Abc_Print( -2, "\t testbench for new procedures\n" );
Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax );
Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax );
Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax );
Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax );
Abc_Print( -2, "\t-M num : the max number of ones in the vector [default = %d]\n", nNumOnes );
Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using new ordering [default = %s]\n", fNewOrder? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
src/misc/extra/extraUtilSupp.c 0 → 100644
/**CFile****************************************************************
FileName [extraUtilSupp.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Support minimization.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: extraUtilSupp.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Generate m-out-of-n vectors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_SuppCountOnes( unsigned i )
{
i = i - ((i >> 1) & 0x55555555);
i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
i = ((i + (i >> 4)) & 0x0F0F0F0F);
return (i*(0x01010101))>>24;
}
Vec_Int_t * Abc_SuppGen( int m, int n )
{
Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
int i, Size = (1 << n);
for ( i = 0; i < Size; i++ )
if ( Abc_SuppCountOnes(i) == m )
Vec_IntPush( vRes, i );
return vRes;
}
/**Function*************************************************************
Synopsis [Generate pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_SuppGenPairs( Vec_Int_t * p, int nBits )
{
Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) );
int * pLimit = Vec_IntLimit(p);
int * pEntry1 = Vec_IntArray(p);
int * pEntry2, Value;
for ( ; pEntry1 < pLimit; pEntry1++ )
for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
{
Value = *pEntry1 ^ *pEntry2;
if ( Abc_InfoHasBit(pMap, Value) )
continue;
Abc_InfoXorBit( pMap, Value );
Vec_IntPush( vRes, Value );
}
ABC_FREE( pMap );
return vRes;
}
/**Function*************************************************************
Synopsis [Select variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppPrintMask( unsigned uMask, int nBits )
{
int i;
for ( i = 0; i < nBits; i++ )
printf( "%d", (uMask >> i) & 1 );
printf( "\n" );
}
void Abc_SuppGenProfile( Vec_Int_t * p, int nBits, int * pCounts )
{
int i, k, b, Ent;
Vec_IntForEachEntry( p, Ent, i )
for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ )
pCounts[k] += ((Ent >> k) & 1) ^ b;
}
void Abc_SuppPrintProfile( Vec_Int_t * p, int nBits )
{
int k, Counts[32] = {0};
Abc_SuppGenProfile( p, nBits, Counts );
for ( k = 0; k < nBits; k++ )
printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_IntSize(p) );
}
int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit )
{
int k, kBest = 0, Counts[32] = {0};
Abc_SuppGenProfile( p, nBits, Counts );
for ( k = 1; k < nBits; k++ )
if ( Counts[kBest] < Counts[k] )
kBest = k;
*pMerit = Counts[kBest];
return kBest;
}
void Abc_SuppGenSelectVar( Vec_Int_t * p, int nBits, int iVar )
{
int * pEntry = Vec_IntArray(p);
int * pLimit = Vec_IntLimit(p);
for ( ; pEntry < pLimit; pEntry++ )
if ( (*pEntry >> iVar) & 1 )
*pEntry ^= (1 << nBits);
}
void Abc_SuppGenFilter( Vec_Int_t * p, int nBits )
{
int i, k = 0, Ent;
Vec_IntForEachEntry( p, Ent, i )
if ( ((Ent >> nBits) & 1) == 0 )
Vec_IntWriteEntry( p, k++, Ent );
Vec_IntShrink( p, k );
}
unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits )
{
unsigned uMask = 0;
int Prev = -1, This, Var;
while ( 1 )
{
Var = Abc_SuppGenFindBest( p, nBits, &This );
if ( Prev >= This )
break;
Prev = This;
Abc_SuppGenSelectVar( p, nBits, Var );
uMask |= (1 << Var);
}
return uMask;
}
int Abc_SuppMinimize( Vec_Int_t * p, int nBits, int fVerbose )
{
unsigned uMask; int i;
for ( i = 0; Vec_IntSize(p) > 0; i++ )
{
// Abc_SuppPrintProfile( p, nBits );
uMask = Abc_SuppFindOne( p, nBits );
Abc_SuppGenFilter( p, nBits );
if ( !fVerbose )
continue;
// print stats
printf( "%2d : ", i );
printf( "%6d ", Vec_IntSize(p) );
Abc_SuppPrintMask( uMask, nBits );
// printf( "\n" );
}
return i;
}
/**Function*************************************************************
Synopsis [Create representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_SuppTest( int nOnes, int nVars, int fVerbose )
{
int nVarsMin;
abctime clk = Abc_Clock();
// create the problem
Vec_Int_t * vRes = Abc_SuppGen( nOnes, nVars );
Vec_Int_t * vPairs = Abc_SuppGenPairs( vRes, nVars );
printf( "M = %2d N = %2d : ", nOnes, nVars );
printf( "K = %6d ", Vec_IntSize(vRes) );
printf( "Total = %10d ", Vec_IntSize(vRes) * (Vec_IntSize(vRes) - 1) /2 );
printf( "Distinct = %8d ", Vec_IntSize(vPairs) );
Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
// solve the problem
clk = Abc_Clock();
nVarsMin = Abc_SuppMinimize( vPairs, nVars, fVerbose );
printf( "Solution with %d variables found. ", nVarsMin );
Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
Vec_IntFree( vPairs );
Vec_IntFree( vRes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/misc/extra/module.make
......@@ -17,5 +17,6 @@ SRC += src/misc/extra/extraBddAuto.c \
src/misc/extra/extraUtilPerm.c \
src/misc/extra/extraUtilProgress.c \
src/misc/extra/extraUtilReader.c \
src/misc/extra/extraUtilSupp.c \
src/misc/extra/extraUtilTruth.c \
src/misc/extra/extraUtilUtil.c
src/sat/bmc/bmcEco.c
......@@ -264,12 +264,33 @@ int Bmc_EcoPatch( Gia_Man_t * p, int nIns, int nOuts )
***********************************************************************/
void Bmc_EcoMiterTest()
{
char * pFileGold = "eco_gold.aig";
char * pFileOld = "eco_old.aig";
Vec_Int_t * vFans;
FILE * pFile;
Gia_Man_t * pMiter;
Gia_Obj_t * pObj;
Gia_Man_t * pGold = Gia_AigerRead( "eco_gold.aig", 0, 0 );
Gia_Man_t * pOld = Gia_AigerRead( "eco_old.aig", 0, 0 );
Gia_Man_t * pGold;
Gia_Man_t * pOld;
int i, RetValue;
// check that the files exist
pFile = fopen( pFileGold, "r" );
if ( pFile == NULL )
{
printf( "File \"%s\" does not exist.\n", pFileGold );
return;
}
fclose( pFile );
pFile = fopen( pFileOld, "r" );
if ( pFile == NULL )
{
printf( "File \"%s\" does not exist.\n", pFileOld );
return;
}
fclose( pFile );
// read files
pGold = Gia_AigerRead( pFileGold, 0, 0 );
pOld = Gia_AigerRead( pFileOld, 0, 0 );
// create ECO miter
vFans = Vec_IntAlloc( Gia_ManCiNum(pOld) );
Gia_ManForEachCi( pOld, pObj, i )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment