Skip to content

A
abc
Commit 1c990fc4 by Alan Mishchenko
Options

Experiments with path enumeration.

parent dca22182
Showing with 473 additions and 7 deletions
src/base/abci/abc.c
......@@ -315,6 +315,7 @@ static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCubeEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPathEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -1001,6 +1002,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "permute", Abc_CommandPermute, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "unpermute", Abc_CommandUnpermute, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cubeenum", Abc_CommandCubeEnum, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "pathenum", Abc_CommandPathEnum, 0 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
......@@ -12945,7 +12947,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
int nCutMax = 1;
int nLeafMax = 4;
int nDivMax = 2;
int nDecMax = 70;
int nDecMax = 3;
int nNumOnes = 4;
int fNewAlgo = 0;
int fNewOrder = 0;
......@@ -13150,7 +13152,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Cba_PrsReadBlifTest();
}
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
// Abc_EnumeratePathsTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
......@@ -22826,6 +22827,63 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPathEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_EnumerateFrontierTest( int nSize );
int c, nSize = 4, fZddAlgo = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nzvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nSize < 0 )
goto usage;
break;
case 'z':
fZddAlgo ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
Abc_Print( -2, "Unknown switch.\n");
goto usage;
}
}
Abc_EnumerateFrontierTest( nSize );
return 0;
usage:
Abc_Print( -2, "usage: pathenum [-N num] [-vh]\n" );
Abc_Print( -2, "\t enumerates self-avoiding paths on the NxN grid\n" );
Abc_Print( -2, "\t-N num : the size of the grid to consider [default = %d]\n", nSize );
// Abc_Print( -2, "\t-z : toggle using ZDD-based algorithm [default = %s]\n", fZddAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
src/misc/extra/extraUtilPath.c
......@@ -23,6 +23,7 @@
#include <string.h>
#include <assert.h>
#include "aig/gia/gia.h"
#include "misc/vec/vecHsh.h"
ABC_NAMESPACE_IMPL_START
......@@ -86,10 +87,18 @@ Gia_Man_t * Abc_EnumeratePaths( int nSize )
ABC_FREE( pNodes );
return pGia;
}
void Abc_EnumeratePathsTest()
{
int nSize = 2;
Gia_Man_t * pGia = Abc_EnumeratePaths( nSize );
Gia_AigerWrite( pGia, "testpath.aig", 0, 0 );
Gia_ManStop( pGia );
}
/**Function*************************************************************
Synopsis []
Synopsis [Generate NxN grid.]
Description []
......@@ -98,12 +107,411 @@ Gia_Man_t * Abc_EnumeratePaths( int nSize )
SeeAlso []
***********************************************************************/
void Abc_EnumeratePathsTest()
Vec_Int_t * Abc_GraphGrid( int n )
{
int nSize = 2;
Gia_Man_t * pGia = Abc_EnumeratePaths( nSize );
Gia_AigerWrite( pGia, "testpath.aig", 0, 0 );
Vec_Int_t * vEdges = Vec_IntAlloc( 4*n*(n-1) ); // two nodes per edge
int i, k;
for ( i = 0; i < n; i++ )
{
for ( k = 0; k < n-1; k++ )
Vec_IntPushTwo( vEdges, i*n+k, i*n+k+1 );
if ( i == n-1 ) break;
for ( k = 0; k < n; k++ )
Vec_IntPushTwo( vEdges, i*n+k, i*n+k+n );
}
//Vec_IntPrint( vEdges );
return vEdges;
}
Vec_Int_t * Abc_GraphNodeLife( Vec_Int_t * vEdges, int n )
{
Vec_Int_t * vLife = Vec_IntStartFull( 2*n*n ); // start/stop per node
int One, Two, i;
Vec_IntForEachEntryDouble( vEdges, One, Two, i )
{
if ( Vec_IntEntry(vLife, 2*One) == -1 )
Vec_IntWriteEntry(vLife, 2*One, i/2);
if ( Vec_IntEntry(vLife, 2*Two) == -1 )
Vec_IntWriteEntry(vLife, 2*Two, i/2);
Vec_IntWriteEntry(vLife, 2*One+1, i/2);
Vec_IntWriteEntry(vLife, 2*Two+1, i/2);
}
//Vec_IntPrint( vLife );
return vLife;
}
Vec_Wec_t * Abc_GraphFrontiers( Vec_Int_t * vEdges, Vec_Int_t * vLife )
{
Vec_Wec_t * vFronts = Vec_WecAlloc( Vec_IntSize(vEdges)/2 ); // front for each edge
Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vLife)/2 );
int e, n;
Vec_WecPushLevel(vFronts);
for ( e = 0; e < Vec_IntSize(vEdges)/2; e++ )
{
int * pNodes = Vec_IntEntryP(vEdges, 2*e);
for ( n = 0; n < 2; n++ )
if ( Vec_IntEntry(vLife, 2*pNodes[n]) == e ) // first time
Vec_IntPush( vTemp, pNodes[n] );
else if ( Vec_IntEntry(vLife, 2*pNodes[n]+1) == e ) // last time
Vec_IntRemove( vTemp, pNodes[n] );
Vec_IntAppend( Vec_WecPushLevel(vFronts), vTemp );
}
//Vec_WecPrint( vFronts, 0 );
Vec_IntFree( vTemp );
return vFronts;
}
/**Function*************************************************************
Synopsis [Print grid.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_GraphPathPrint4( int * pBuffer, Vec_Int_t * vEdges )
{
char Box[13][13];
int x, y;
int e, nEdges = Vec_IntSize(vEdges)/2;
for ( y = 0; y < 13; y++ )
for ( x = 0; x < 13; x++ )
if ( y % 4 == 0 && x % 4 == 0 )
Box[y][x] = '*';
else
Box[y][x] = ' ';
for ( e = 0; e < nEdges; e++ )
{
int * pNodes = Vec_IntEntryP(vEdges, 2*e);
int y0 = 4*(pNodes[0]/4);
int x0 = 4*(pNodes[0]%4);
int y1 = 4*(pNodes[1]/4);
int x1 = 4*(pNodes[1]%4);
if ( !pBuffer[e] )
continue;
if ( y0 == y1 )
{
for ( x = x0+1; x < x1; x++ )
Box[y0][x] = '-';
}
else if ( x0 == x1 )
{
for ( y = y0+1; y < y1; y++ )
Box[y][x0] = '|';
}
else assert( 0 );
}
for ( y = 0; y < 13; y++, printf("\n") )
for ( x = 0; x < 13; x++ )
printf( "%c", Box[y][x] );
printf( "\n\n=================================\n\n" );
}
void Abc_GraphPathPrint5( int * pBuffer, Vec_Int_t * vEdges )
{
char Box[17][17];
int x, y;
int e, nEdges = Vec_IntSize(vEdges)/2;
for ( y = 0; y < 17; y++ )
for ( x = 0; x < 17; x++ )
if ( y % 4 == 0 && x % 4 == 0 )
Box[y][x] = '*';
else
Box[y][x] = ' ';
for ( e = 0; e < nEdges; e++ )
{
int * pNodes = Vec_IntEntryP(vEdges, 2*e);
int y0 = 4*(pNodes[0]/5);
int x0 = 4*(pNodes[0]%5);
int y1 = 4*(pNodes[1]/5);
int x1 = 4*(pNodes[1]%5);
if ( !pBuffer[e] )
continue;
if ( y0 == y1 )
{
for ( x = x0+1; x < x1; x++ )
Box[y0][x] = '-';
}
else if ( x0 == x1 )
{
for ( y = y0+1; y < y1; y++ )
Box[y][x0] = '|';
}
else assert( 0 );
}
for ( y = 0; y < 17; y++, printf("\n") )
for ( x = 0; x < 17; x++ )
printf( "%c", Box[y][x] );
printf( "\n\n=================================\n\n" );
}
/**Function*************************************************************
Synopsis [Count paths.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
double Abc_GraphCountPaths_rec( int Lev, int Node, Vec_Wec_t * vNodes, double ** pCache, int * pBuffer, Vec_Int_t * vEdges )
{
double Res0, Res1;
// if ( Node == -2 ) Abc_GraphPathPrint4( pBuffer, vEdges );
if ( Node == -2 )
return 1;
if ( Node == -1 )
return 0;
if ( pCache[Lev][Node] != -1.0 )
return pCache[Lev][Node];
pBuffer[Lev] = 0;
Res0 = Abc_GraphCountPaths_rec( Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node ), vNodes, pCache, pBuffer, vEdges );
pBuffer[Lev] = 1;
Res1 = Abc_GraphCountPaths_rec( Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node+1 ), vNodes, pCache, pBuffer, vEdges );
return (pCache[Lev][Node] = Res0 + Res1);
}
double Abc_GraphCountPaths( Vec_Wec_t * vNodes, Vec_Int_t * vEdges )
{
int i, k, pBuffer[1000] = {0};
double ** pCache = ABC_ALLOC( double *, Vec_WecSize(vNodes) );
Vec_Int_t * vLevel; double Value;
Vec_WecForEachLevel( vNodes, vLevel, i )
{
pCache[i] = ABC_ALLOC( double, Vec_IntSize(vLevel) );
for ( k = 0; k < Vec_IntSize(vLevel); k++ )
pCache[i][k] = -1.0;
}
Value = Abc_GraphCountPaths_rec( 0, 0, vNodes, pCache, pBuffer, vEdges );
for ( i = 0; i < Vec_WecSize(vNodes); i++ )
ABC_FREE( pCache[i] );
ABC_FREE( pCache );
return Value;
}
/**Function*************************************************************
Synopsis [Build AIG for paths.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_GraphDeriveGia_rec( Gia_Man_t * p, int Lev, int Node, Vec_Wec_t * vNodes, int ** pCache, int * pBuffer, Vec_Int_t * vEdges )
{
int Res0, Res1;
if ( Node == -2 )
return 1;
if ( Node == -1 )
return 0;
if ( pCache[Lev][Node] != -1 )
return pCache[Lev][Node];
pBuffer[Lev] = 0;
Res0 = Abc_GraphDeriveGia_rec( p, Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node ), vNodes, pCache, pBuffer, vEdges );
pBuffer[Lev] = 1;
Res1 = Abc_GraphDeriveGia_rec( p, Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node+1 ), vNodes, pCache, pBuffer, vEdges );
return ( pCache[Lev][Node] = Gia_ManHashMux(p, Gia_Obj2Lit(p, Gia_ManCi(p, Lev)), Res1, Res0) );
}
Gia_Man_t * Abc_GraphDeriveGia( Vec_Wec_t * vNodes, Vec_Int_t * vEdges )
{
int ** pCache;
int i, Value, pBuffer[1000] = {0};
Vec_Int_t * vLevel;
// start AIG
Gia_Man_t * pTemp, * p = Gia_ManStart( 1000 );
p->pName = Abc_UtilStrsav("paths");
for ( i = 0; i < Vec_IntSize(vEdges)/2; i++ )
Gia_ManAppendCi(p);
Gia_ManHashAlloc(p);
// alloc cache
pCache = ABC_ALLOC( int *, Vec_WecSize(vNodes) );
Vec_WecForEachLevel( vNodes, vLevel, i )
pCache[i] = ABC_FALLOC( int, Vec_IntSize(vLevel) );
Value = Abc_GraphDeriveGia_rec( p, 0, 0, vNodes, pCache, pBuffer, vEdges );
for ( i = 0; i < Vec_WecSize(vNodes); i++ )
ABC_FREE( pCache[i] );
ABC_FREE( pCache );
// cleanup
Gia_ManAppendCo( p, Value );
p = Gia_ManCleanup( pTemp = p );
Gia_ManStop( pTemp );
return p;
}
void Abc_GraphDeriveGiaDump( Vec_Wec_t * vNodes, Vec_Int_t * vEdges, int Size )
{
char pFileName[100];
Gia_Man_t * pGia = Abc_GraphDeriveGia( vNodes, vEdges );
sprintf( pFileName, "grid_%dx%d_e%03d.aig", Size, Size, Vec_IntSize(vEdges)/2 );
Gia_AigerWrite( pGia, pFileName, 0, 0 );
Gia_ManStop( pGia );
printf( "Finished dumping AIG into file \"%s\".\n", pFileName );
}
/**Function*************************************************************
Synopsis [Build frontier.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_GraphBuildState( Vec_Int_t * vState, int e, int x, Vec_Int_t * vEdges, Vec_Int_t * vLife, Vec_Wec_t * vFronts, int * pFront, Vec_Int_t * vStateNew, int fVerbose )
{
Vec_Int_t * vFront = Vec_WecEntry( vFronts, e );
Vec_Int_t * vFront2 = Vec_WecEntry( vFronts, e+1 );
int * pNodes = Vec_IntEntryP(vEdges, 2*e);
int nNodes = Vec_IntSize(vLife)/2;
int i, n, Node, First, pEquivs[2];
assert( pNodes[0] < pNodes[1] );
if ( fVerbose ) printf( "Edge = %d. Arc = %d.\nCurrent state: ", e, x );
Vec_IntForEachEntry( vFront, Node, i )
{
pFront[Node] = Vec_IntEntry(vState, i);
if ( fVerbose ) printf( "%d(%d) ", pFront[Node] & 0xFFFF, pFront[Node] >> 16 );
}
if ( fVerbose ) printf( "\n" );
for ( n = 0; n < 2; n++ )
if ( Vec_IntEntry(vLife, 2*pNodes[n]) == e ) // first time
pFront[pNodes[n]] = pNodes[n]; // degree = 0; comp = singleton
if ( x )
{
if ( (pFront[pNodes[0]] & 0xFFFF) == (pFront[pNodes[1]] & 0xFFFF) ) // the same comp
return -1; // const 0
for ( n = 0; n < 2; n++ )
{
int Degree = pFront[pNodes[n]] >> 16;
if ( (pNodes[n] == 0 || pNodes[n] == nNodes-1) ? Degree >= 1 : Degree >= 2 )
return -1; // const 0
pFront[pNodes[n]] += (1 << 16); // degree++
}
}
// remember equivalence classes
pEquivs[0] = pFront[pNodes[0]] & 0xFFFF;
pEquivs[1] = pFront[pNodes[1]] & 0xFFFF;
// remove some nodes from the frontier
for ( n = 0; n < 2; n++ )
if ( Vec_IntEntry(vLife, 2*pNodes[n]+1) == e ) // last time
{
int Degree = pFront[pNodes[n]] >> 16;
if ( (pNodes[n] == 0 || pNodes[n] == nNodes-1) ? Degree != 1 : Degree != 0 && Degree != 2 )
return -1; // const 0
// if it is part of the comp, update
First = -1;
Vec_IntForEachEntry( vFront2, Node, i )
{
assert( Node != pNodes[n] );
if ( (pFront[Node] & 0xFFFF) == pEquivs[n] )
{
if ( First == -1 )
First = Node;
pFront[Node] = (pFront[Node] & 0xFFFF0000) | First;
}
}
if ( First != -1 )
pEquivs[n] = First;
}
if ( x )
{
// union comp
int First = -1;
Vec_IntForEachEntry( vFront2, Node, i )
if ( (pFront[Node] & 0xFFFF) == pEquivs[0] || (pFront[Node] & 0xFFFF) == pEquivs[1] )
{
if ( First == -1 )
First = Node;
pFront[Node] = (pFront[Node] & 0xFFFF0000) | First;
}
}
// create next state
Vec_IntClear( vStateNew );
if ( fVerbose ) printf( "Next state: " );
Vec_IntForEachEntry( vFront2, Node, i )
{
Vec_IntPush( vStateNew, pFront[Node] );
if ( fVerbose ) printf( "%d(%d) ", pFront[Node] & 0xFFFF, pFront[Node] >> 16 );
}
if ( fVerbose ) printf( "\n\n" );
return 1;
}
void Abc_GraphBuildFrontier( int nSize, Vec_Int_t * vEdges, Vec_Int_t * vLife, Vec_Wec_t * vFronts, int fVerbose )
{
abctime clk = Abc_Clock();
double nPaths;
int nEdges = Vec_IntSize(vEdges)/2;
int nNodes = Vec_IntSize(vLife)/2;
Vec_Wec_t * vNodes = Vec_WecAlloc( nEdges );
Vec_Int_t * vStateNew = Vec_IntAlloc( nNodes );
Vec_Int_t * vStateCount = Vec_IntAlloc( nEdges );
int e, s, x, Next, * pFront = ABC_CALLOC( int, nNodes );
Hsh_VecMan_t * pThis = Hsh_VecManStart( 1000 );
Hsh_VecMan_t * pNext = Hsh_VecManStart( 1000 );
Hsh_VecManAdd( pThis, vStateNew );
for ( e = 0; e < nEdges; e++ )
{
Vec_Int_t * vNode = Vec_WecPushLevel(vNodes);
int nStates = Hsh_VecSize( pThis );
Vec_IntPush( vStateCount, nStates );
if ( fVerbose )
{
printf( "\n" );
printf( "Processing edge %d = {%d %d}\n", e, Vec_IntEntry(vEdges, 2*e), Vec_IntEntry(vEdges, 2*e+1) );
printf( "Frontier: " ); Vec_IntPrint( Vec_WecEntry(vFronts, e) );
printf( "\n" );
}
for ( s = 0; s < nStates; s++ )
{
Vec_Int_t * vState = Hsh_VecReadEntry(pThis, s);
for ( x = 0; x < 2; x++ )
{
Next = Abc_GraphBuildState(vState, e, x, vEdges, vLife, vFronts, pFront, vStateNew, fVerbose);
if ( Next == 1 )
{
if ( e == nEdges - 1 ) // last edge
Next = -2; // const1
else
Next = Hsh_VecManAdd( pNext, vStateNew );
}
if ( fVerbose ) printf( "Return value = %d\n", Next );
Vec_IntPush( vNode, Next );
}
}
Hsh_VecManStop( pThis );
pThis = pNext;
pNext = Hsh_VecManStart( 1000 );
}
nPaths = Abc_GraphCountPaths(vNodes, vEdges);
printf( "States = %8d Paths = %24.0f ", Vec_IntSum(vStateCount), nPaths );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
Vec_IntPrint( vStateCount );
Abc_GraphDeriveGiaDump( vNodes, vEdges, nSize );
ABC_FREE( pFront );
Vec_WecFree( vNodes );
Vec_IntFree( vStateNew );
Vec_IntFree( vStateCount );
Hsh_VecManStop( pThis );
Hsh_VecManStop( pNext );
}
void Abc_EnumerateFrontierTest( int nSize )
{
//int nSize = 3;
int fVerbose = 0;
Vec_Int_t * vEdges = Abc_GraphGrid( nSize );
Vec_Int_t * vLife = Abc_GraphNodeLife( vEdges, nSize );
Vec_Wec_t * vFronts = Abc_GraphFrontiers( vEdges, vLife );
Abc_GraphBuildFrontier( nSize, vEdges, vLife, vFronts, fVerbose );
Vec_WecFree( vFronts );
Vec_IntFree( vLife );
Vec_IntFree( vEdges );
}
////////////////////////////////////////////////////////////////////////
......
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