Skip to content

A
abc
Commit 9521d134 by Alan Mishchenko
Options

Improvements to 'satclp'.

parent fe0487da
Showing with 354 additions and 23 deletions
src/aig/gia/gia.h
......@@ -1452,6 +1452,7 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
extern int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp );
extern int Gia_ManHasDangling( Gia_Man_t * p );
extern int Gia_ManMarkDangling( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
......
src/aig/gia/giaUtil.c
......@@ -1143,6 +1143,47 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
/**Function*************************************************************
Synopsis [Returns the number of internal nodes in the MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
{
if ( Gia_ObjIsTravIdCurrent(p, pNode) )
return;
Gia_ObjSetTravIdCurrent(p, pNode);
if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) )
{
Vec_IntPush( vSupp, Gia_ObjId(p, pNode) );
return;
}
assert( Gia_ObjIsAnd(pNode) );
Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
}
int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
{
int ConeSize1, ConeSize2;
assert( !Gia_IsComplement(pNode) );
assert( Gia_ObjIsAnd(pNode) );
Vec_IntClear( vSupp );
Gia_ManIncrementTravId( p );
ConeSize1 = Gia_NodeDeref_rec( p, pNode );
Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
ConeSize2 = Gia_NodeRef_rec( p, pNode );
assert( ConeSize1 == ConeSize2 );
assert( ConeSize1 >= 0 );
return ConeSize1;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
......
src/base/abci/abcCollapse.c
......@@ -583,6 +583,51 @@ Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
/**Function*************************************************************
Synopsis [Minimize SOP by removing redundant variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#define Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
{
int j = 0, k, iVar, nVars = Vec_IntSize(vSupp);
char * pCube, * pSop = Vec_StrArray(vSop);
Vec_Int_t * vPres = Vec_IntStart( nVars );
Abc_NtkSopForEachCube( pSop, nVars, pCube )
for ( k = 0; k < nVars; k++ )
if ( pCube[k] != '-' )
Vec_IntWriteEntry( vPres, k, 1 );
if ( Vec_IntCountZero(vPres) == 0 )
{
Vec_IntFree( vPres );
return 0;
}
// reduce cubes
Abc_NtkSopForEachCube( pSop, nVars, pCube )
for ( k = 0; k < nVars + 3; k++ )
if ( k >= nVars || Vec_IntEntry(vPres, k) )
Vec_StrWriteEntry( vSop, j++, pCube[k] );
Vec_StrWriteEntry( vSop, j++, '\0' );
Vec_StrShrink( vSop, j );
// reduce support
j = 0;
Vec_IntForEachEntry( vSupp, iVar, k )
if ( Vec_IntEntry(vPres, k) )
Vec_IntWriteEntry( vSupp, j++, iVar );
Vec_IntShrink( vSupp, j );
Vec_IntFree( vPres );
return 1;
}
/**Function*************************************************************
Synopsis [Computes SOPs for each output.]
Description []
......@@ -606,6 +651,10 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
return NULL;
if ( Vec_StrSize(vSop) == 4 ) // constant
Vec_IntClear(vSupp);
else
Abc_NtkCollapseCountVars( vSop, vSupp );
if ( fVerbose )
printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return vSop;
......@@ -613,27 +662,18 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
{
ProgressBar * pProgress;
abctime clk = Abc_Clock();
Vec_Ptr_t * vSops = NULL, * vSopsRepr;
Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
int i, k, Entry, iCo, * pOrder;
Vec_Wec_t * vClasses;
// check the largest output
if ( nCubeLim > 0 && nCostMax > 0 )
{
int iCoMax = Gia_ManCoLargestSupp( p, vSupps );
int iObjMax = Gia_ObjId( p, Gia_ManCo(p, iCoMax) );
int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 );
word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
if ( Cost > (word)nCostMax )
{
printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n",
nNodeMax, nSuppMax, nCubeLim, nCostMax );
return NULL;
}
}
// derive classes of outputs
vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
if ( fVerbose )
{
printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) );
Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
}
// derive representatives
vReprs = Vec_WecCollectFirsts( vClasses );
vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) );
......@@ -693,6 +733,23 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
int i, k, iCi;
pGia = Abc_NtkClpGia( pNtk );
vSupps = Gia_ManCreateCoSupps( pGia, fVerbose );
// check the largest output
if ( nCubeLim > 0 && nCostMax > 0 )
{
int iCoMax = Gia_ManCoLargestSupp( pGia, vSupps );
int iObjMax = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) );
int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
int nNodeMax = Gia_ManConeSize( pGia, &iObjMax, 1 );
word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
if ( Cost > (word)nCostMax )
{
printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n",
nNodeMax, nSuppMax, nCubeLim, nCostMax );
Gia_ManStop( pGia );
Vec_WecFree( vSupps );
return NULL;
}
}
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
Gia_ManStop( pGia );
......
src/proof/abs/absRpm.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "abs.h"
#include "misc/vec/vecWec.h"
ABC_NAMESPACE_IMPL_START
......@@ -106,6 +107,86 @@ void Gia_ManComputeDoms( Gia_Man_t * p )
Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Gia_ManCreateSupps( Gia_Man_t * p, int fVerbose )
{
abctime clk = Abc_Clock();
Gia_Obj_t * pObj; int i, Id;
Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
Gia_ManForEachCiId( p, Id, i )
Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
Gia_ManForEachAnd( p, pObj, Id )
Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
Vec_WecEntry(vSupps, Id) );
// Gia_ManForEachCo( p, pObj, i )
// Vec_IntAppend( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
if ( fVerbose )
Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
return vSupps;
}
void Gia_ManDomTest( Gia_Man_t * p )
{
Vec_Int_t * vDoms = Vec_IntAlloc( 100 );
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Vec_Wec_t * vSupps = Gia_ManCreateSupps( p, 1 );
Vec_Wec_t * vDomeds = Vec_WecStart( Gia_ManObjNum(p) );
Gia_Obj_t * pObj, * pDom; int i, Id, nMffcSize;
Gia_ManCreateRefs( p );
Gia_ManComputeDoms( p );
Gia_ManForEachCi( p, pObj, i )
{
if ( Gia_ObjDom(p, pObj) == -1 )
continue;
for ( pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj)); Gia_ObjIsAnd(pDom); pDom = Gia_ManObj(p, Gia_ObjDom(p, pDom)) )
Vec_IntPush( Vec_WecEntry(vDomeds, Gia_ObjId(p, pDom)), i );
}
Gia_ManForEachAnd( p, pObj, i )
if ( Vec_IntEqual(Vec_WecEntry(vSupps, i), Vec_WecEntry(vDomeds, i)) )
Vec_IntPush( vDoms, i );
Vec_WecFree( vSupps );
Vec_WecFree( vDomeds );
// check MFFC sizes
Vec_IntForEachEntry( vDoms, Id, i )
Gia_ObjRefInc( p, Gia_ManObj(p, Id) );
Vec_IntForEachEntry( vDoms, Id, i )
{
nMffcSize = Gia_NodeMffcSizeSupp( p, Gia_ManObj(p, Id), vSupp );
printf( "%d(%d:%d) ", Id, Vec_IntSize(vSupp), nMffcSize );
}
printf( "\n" );
Vec_IntForEachEntry( vDoms, Id, i )
Gia_ObjRefDec( p, Gia_ManObj(p, Id) );
// Vec_IntPrint( vDoms );
Vec_IntFree( vDoms );
Vec_IntFree( vSupp );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManTestDoms2( Gia_Man_t * p )
{
Vec_Int_t * vNodes;
......
src/sat/bmc/bmcClp.c
......@@ -36,14 +36,158 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [For a given random pattern, compute output change.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bmc_ComputeSimDiff( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vPat2 )
{
Gia_Obj_t * pObj;
int i, Id; word Sim, Sim0, Sim1;
Gia_ManForEachCiId( p, Id, i )
{
Sim = Vec_IntEntry(vPat, i) ? ~(word)0 : 0;
Sim ^= (word)1 << (i + 1);
Vec_WrdWriteEntry( p->vSims, Id, Sim );
}
Gia_ManForEachAnd( p, pObj, i )
{
Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, i) );
Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1(pObj, i) );
Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
Vec_WrdWriteEntry( p->vSims, i, Sim0 & Sim1 );
}
Gia_ManForEachCo( p, pObj, i )
{
Id = Gia_ObjId( p, pObj );
Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, Id) );
Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
Vec_WrdWriteEntry( p->vSims, Id, Sim0 );
}
pObj = Gia_ManCo( p, 0 );
Sim = Vec_WrdEntry( p->vSims, Gia_ObjId(p, pObj) );
Vec_IntClear( vPat2 );
for ( i = 1; i <= Gia_ManCiNum(p); i++ )
Vec_IntPush( vPat2, (int)((Sim & 1) ^ ((Sim >> i) & 1)) );
return (int)(Sim & 1);
}
void Bmc_ComputeSimTest( Gia_Man_t * p )
{
int i, v, w, Res, Bit, Bit2, nPats = 256;
int Count[2][64][64] = {{{0}}};
int PatCount[64][2][2] = {{{0}}};
int DiffCount[64] = {0};
Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
Vec_Int_t * vPat2 = Vec_IntAlloc( Gia_ManCiNum(p) );
Vec_WrdFreeP( &p->vSims );
p->vSims = Vec_WrdStart( Gia_ManObjNum(p) );
printf( "Number of patterns = %d.\n", nPats );
for ( i = 0; i < nPats; i++ )
{
Vec_IntClear( vPat );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
Vec_IntPush( vPat, rand() & 1 );
// Vec_IntForEachEntry( vPat, Bit, v )
// printf( "%d", Bit );
// printf( " " );
Res = Bmc_ComputeSimDiff( p, vPat, vPat2 );
// printf( "%d ", Res );
// Vec_IntForEachEntry( vPat2, Bit, v )
// printf( "%d", Bit );
// printf( "\n" );
Vec_IntForEachEntry( vPat, Bit, v )
PatCount[v][Res][Bit]++;
Vec_IntForEachEntry( vPat2, Bit, v )
{
if ( Bit )
DiffCount[v]++;
Vec_IntForEachEntryStart( vPat2, Bit2, w, v + 1 )
if ( Bit && Bit2 )
Count[Res][v][w]++;
}
}
Vec_IntFree( vPat );
Vec_IntFree( vPat2 );
Vec_WrdFreeP( &p->vSims );
printf( "\n" );
printf( " " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3c ", 'a'+v );
printf( "\n" );
printf( "Off0 " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3d ", PatCount[v][0][0] );
printf( "\n" );
printf( "Off1 " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3d ", PatCount[v][0][1] );
printf( "\n" );
printf( "On0 " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3d ", PatCount[v][1][0] );
printf( "\n" );
printf( "On1 " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3d ", PatCount[v][1][1] );
printf( "\n" );
printf( "\n" );
printf( "Diff " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3d ", DiffCount[v] );
printf( "\n" );
printf( "\n" );
for ( i = 0; i < 2; i++ )
{
printf( " " );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
printf( "%3c ", 'a'+v );
printf( "\n" );
for ( v = 0; v < Gia_ManCiNum(p); v++ )
{
printf( " %c ", 'a'+v );
for ( w = 0; w < Gia_ManCiNum(p); w++ )
{
if ( Count[i][v][w] )
printf( "%3d ", Count[i][v][w] );
else
printf( " . " );
}
printf( "\n" );
}
printf( "\n" );
}
}
static abctime clkCheck1 = 0;
static abctime clkCheck2 = 0;
static abctime clkCheckS = 0;
static abctime clkCheckU = 0;
// enumerate cubes and literals
#define Bmc_SopForEachCube( pSop, nVars, pCube ) \
for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
// iterator thought the cubes
#define Bmc_SopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
/**Function*************************************************************
......@@ -270,11 +414,6 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
}
// if ( pSatOn )
// printf( "\n" );
// put into new array
Vec_IntClear( vNums );
Vec_IntForEachEntry( vLits, iLit, n )
if ( iLit != -1 )
Vec_IntPush( vNums, n );
return 0;
}
......@@ -311,9 +450,21 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit
if ( k == nFinal )
Vec_IntWriteEntry( vLits, i, -1 );
}
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon );
}
else
{
Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon );
}
{
// put into new array
int i, iLit;
Vec_IntClear( vNums );
Vec_IntForEachEntry( vLits, iLit, i )
if ( iLit != -1 )
Vec_IntPush( vNums, i );
}
return 0;
}
......
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