/**CFile****************************************************************
FileName [extraUtilPath.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Path enumeration.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: extraUtilPath.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 "aig/gia/gia.h"
#include "misc/vec/vecHsh.h"
#include <math.h>
#include "sat/bmc/bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes AIG representing the set of all paths in the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeVarX( int nSize, int y, int x )
{
return Abc_Var2Lit( nSize * y + x, 0 );
}
int Abc_NodeVarY( int nSize, int y, int x )
{
return Abc_Var2Lit( nSize * (nSize + 1) + nSize * x + y, 0 );
}
Gia_Man_t * Abc_EnumeratePaths( int nSize )
{
Gia_Man_t * pTemp, * pGia = Gia_ManStart( 10000 );
int * pNodes = ABC_CALLOC( int, nSize+1 );
int x, y, nVars = 2*nSize*(nSize+1);
for ( x = 0; x < nVars; x++ )
Gia_ManAppendCi( pGia );
Gia_ManHashAlloc( pGia );
// y = 0; x = 0;
pNodes[0] = 1;
// y = 0; x > 0
for ( x = 1; x <= nSize; x++ )
pNodes[x] = Gia_ManHashAnd( pGia, pNodes[x-1], Abc_NodeVarX(nSize, 0, x) );
// y > 0; x >= 0
for ( y = 1; y <= nSize; y++ )
{
// y > 0; x = 0
pNodes[0] = Gia_ManHashAnd( pGia, pNodes[0], Abc_NodeVarY(nSize, y, 0) );
// y > 0; x > 0
for ( x = 1; x <= nSize; x++ )
{
int iHor = Gia_ManHashAnd( pGia, pNodes[x-1], Abc_NodeVarX(nSize, y, x) );
int iVer = Gia_ManHashAnd( pGia, pNodes[x], Abc_NodeVarY(nSize, y, x) );
pNodes[x] = Gia_ManHashOr( pGia, iHor, iVer );
}
}
Gia_ManAppendCo( pGia, pNodes[nSize] );
pGia = Gia_ManCleanup( pTemp = pGia );
Gia_ManStop( pTemp );
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, 0 );
Gia_ManStop( pGia );
}
/**Function*************************************************************
Synopsis [Generate NxN grid.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_GraphGrid( int n )
{
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, 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 );
}
/**Function*************************************************************
Synopsis [Performs SAT-based path enumeration.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
double Abc_Word2Double( word w )
{
double Res = 0; int i;
for ( i = 0; i < 64; i++ )
if ( (w >> i) & 1 )
Res += pow(2,i);
return Res;
}
void Abc_GraphSolve( Gia_Man_t * pGia )
{
int nIters = 1000;
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
sat_solver * pSat; Vec_Int_t * vLits = Vec_IntAlloc( 100 );
int i, k, iLit, nVars = Gia_ManCiNum(pGia);
int iCiVarBeg = pCnf->nVars - nVars;
word Total = 0;
word Mint1 = 0;
word Mint2 = 0;
// restart the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// create trivial assignment
Vec_IntClear( vLits );
for ( k = 0; k < nVars; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iCiVarBeg+k, 1) );
// generate random assignment
for ( i = 0; i < nIters; i++ )
{
int Status = sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) );
if ( Status != l_True )
break;
assert( Status == l_True );
// block this assignment
Vec_IntForEachEntry( vLits, iLit, k )
Vec_IntWriteEntry( vLits, k, Abc_LitNot(iLit) );
if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ) )
break;
Vec_IntForEachEntry( vLits, iLit, k )
Vec_IntWriteEntry( vLits, k, Abc_LitNot(iLit) );
// collect new minterm
Mint2 = 0;
Vec_IntForEachEntry( vLits, iLit, k )
if ( !Abc_LitIsCompl(iLit) )
Mint2 |= ((word)1) << (nVars-1-k);
if ( Mint1 == 0 )
Mint1 = Mint2;
// report
//printf( "Iter %3d : ", i );
//Extra_PrintBinary( stdout, (unsigned *)&Mint2, Abc_MinInt(64, nVars) ); printf( "\n" );
}
//Mint1 = 0;
Total = (Mint2-Mint1)/nIters;
printf( "Vars = %d Iters = %d Ave = %.0f Total = %.0f ", nVars, nIters, Abc_Word2Double(Mint2-Mint1), Abc_Word2Double(Total) );
printf( "Estimate = %.0f\n", (pow(2,nVars)-Abc_Word2Double(Mint1))/Abc_Word2Double((Mint2-Mint1)/nIters) );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Vec_IntFree( vLits );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END