extraUtilMult.c

/**CFile****************************************************************

  FileName    [extraUtilMult.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [extra]

  Synopsis    [Simple BDD package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - May 23, 2018.]

  Revision    [$Id: extraUtilMult.c,v 1.0 2018/05/23 00:00:00 alanmi Exp $]

***********************************************************************/

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/gia/gia.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Abc_BddMan_ Abc_BddMan;
struct Abc_BddMan_ 
{
    int                nVars;         // the number of variables
    int                nObjs;         // the number of nodes used
    int                nObjsAlloc;    // the number of nodes allocated
    int *              pUnique;       // unique table for nodes
    int *              pNexts;        // next pointer for nodes
    int *              pCache;        // array of triples <arg0, arg1, AND(arg0, arg1)>
    int *              pObjs;         // array of pairs <cof0, cof1> for each node
    unsigned char *    pVars;         // array of variables for each node
    unsigned char *    pMark;         // array of marks for each BDD node
    unsigned           nUniqueMask;   // selection mask for unique table
    unsigned           nCacheMask;    // selection mask for computed table
    int                nCacheLookups; // the number of computed table lookups
    int                nCacheMisses;  // the number of computed table misses
    word               nMemory;       // total amount of memory used (in bytes)
};

static inline int      Abc_BddIthVar( int i )                        { return Abc_Var2Lit(i + 1, 0);                            }
static inline unsigned Abc_BddHash( int Arg0, int Arg1, int Arg2 )   { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; }

static inline int      Abc_BddVar( Abc_BddMan * p, int i )           { return (int)p->pVars[Abc_Lit2Var(i)];                    }
static inline int      Abc_BddThen( Abc_BddMan * p, int i )          { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)], Abc_LitIsCompl(i));    }
static inline int      Abc_BddElse( Abc_BddMan * p, int i )          { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)+1], Abc_LitIsCompl(i));  }

static inline int      Abc_BddMark( Abc_BddMan * p, int i )          { return (int)p->pMark[Abc_Lit2Var(i)];                    }
static inline void     Abc_BddSetMark( Abc_BddMan * p, int i, int m ){ p->pMark[Abc_Lit2Var(i)] = m;                            }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Creating new node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Abc_BddUniqueCreateInt( Abc_BddMan * p, int Var, int Then, int Else )
{
    int *q = p->pUnique + (Abc_BddHash(Var, Then, Else) & p->nUniqueMask);
    for ( ; *q; q = p->pNexts + *q )
        if ( (int)p->pVars[*q] == Var && p->pObjs[*q+*q] == Then && p->pObjs[*q+*q+1] == Else )
            return Abc_Var2Lit(*q, 0);
    if ( p->nObjs == p->nObjsAlloc )
        printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout);
    assert( p->nObjs < p->nObjsAlloc );     
    *q = p->nObjs++;
    p->pVars[*q] = Var;
    p->pObjs[*q+*q] = Then;
    p->pObjs[*q+*q+1] = Else;
//    printf( "Added node %3d: Var = %3d.  Then = %3d.  Else = %3d\n", *q, Var, Then, Else );
    assert( !Abc_LitIsCompl(Else) );
    return Abc_Var2Lit(*q, 0);
}
static inline int Abc_BddUniqueCreate( Abc_BddMan * p, int Var, int Then, int Else )
{
    assert( Var >= 0 && Var < p->nVars );
    assert( Var < Abc_BddVar(p, Then)  );
    assert( Var < Abc_BddVar(p, Else) );
    if ( Then == Else )
        return Else;
    if ( !Abc_LitIsCompl(Else) )
        return Abc_BddUniqueCreateInt( p, Var, Then, Else );
    return Abc_LitNot( Abc_BddUniqueCreateInt(p, Var, Abc_LitNot(Then), Abc_LitNot(Else)) );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Abc_BddCacheLookup( Abc_BddMan * p, int Arg1, int Arg2 )
{
    int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask);
    p->nCacheLookups++;
    return (pEnt[0] == Arg1 && pEnt[1] == Arg2) ? pEnt[2] : -1;
}
static inline int Abc_BddCacheInsert( Abc_BddMan * p, int Arg1, int Arg2, int Res )
{
    int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask);
    pEnt[0] = Arg1;  pEnt[1] = Arg2;  pEnt[2] = Res;
    p->nCacheMisses++;
    assert( Res >= 0 );
    return Res;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_BddMan * Abc_BddManAlloc( int nVars, int nObjs )
{
    Abc_BddMan * p; int i;
    p = ABC_CALLOC( Abc_BddMan, 1 );
    p->nVars       = nVars;
    p->nObjsAlloc  = nObjs;
    p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1;
    p->nCacheMask  = (1 << Abc_Base2Log(nObjs)) - 1;
    p->pUnique     = ABC_CALLOC( int, p->nUniqueMask + 1 );
    p->pNexts      = ABC_CALLOC( int, p->nObjsAlloc );
    p->pCache      = ABC_CALLOC( int, 3*(p->nCacheMask + 1) );
    p->pObjs       = ABC_CALLOC( int, 2*p->nObjsAlloc );
    p->pMark       = ABC_CALLOC( unsigned char, p->nObjsAlloc );
    p->pVars       = ABC_CALLOC( unsigned char, p->nObjsAlloc );
    p->pVars[0]    = 0xff;
    p->nObjs       = 1;
    for ( i = 0; i < nVars; i++ )
        Abc_BddUniqueCreate( p, i, 1, 0 );
    assert( p->nObjs == nVars + 1 );
    p->nMemory = sizeof(Abc_BddMan)/4 + 
        p->nUniqueMask + 1 + p->nObjsAlloc + 
        (p->nCacheMask + 1) * 3 * sizeof(int)/4 + 
        p->nObjsAlloc * 2 * sizeof(int)/4;
    return p;
}
void Abc_BddManFree( Abc_BddMan * p )
{
    printf( "BDD stats: Var = %d  Obj = %d  Alloc = %d  Hit = %d  Miss = %d  ", 
        p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses );
    printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) );
    ABC_FREE( p->pUnique );
    ABC_FREE( p->pNexts );
    ABC_FREE( p->pCache );
    ABC_FREE( p->pObjs );
    ABC_FREE( p->pVars );
    ABC_FREE( p );
}

/**Function*************************************************************

  Synopsis    [Boolean AND.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_BddAnd( Abc_BddMan * p, int a, int b )
{
    int r0, r1, r;
    if ( a == 0 ) return 0;
    if ( b == 0 ) return 0;
    if ( a == 1 ) return b;
    if ( b == 1 ) return a;
    if ( a == b ) return a;
    if ( a > b )  return Abc_BddAnd( p, b, a );
    if ( (r = Abc_BddCacheLookup(p, a, b)) >= 0 )
        return r;
    if ( Abc_BddVar(p, a) < Abc_BddVar(p, b) )
        r0 = Abc_BddAnd( p, Abc_BddElse(p, a), b ), 
        r1 = Abc_BddAnd( p, Abc_BddThen(p, a), b );
    else if ( Abc_BddVar(p, a) > Abc_BddVar(p, b) )
        r0 = Abc_BddAnd( p, a, Abc_BddElse(p, b) ), 
        r1 = Abc_BddAnd( p, a, Abc_BddThen(p, b) );
    else // if ( Abc_BddVar(p, a) == Abc_BddVar(p, b) )
        r0 = Abc_BddAnd( p, Abc_BddElse(p, a), Abc_BddElse(p, b) ), 
        r1 = Abc_BddAnd( p, Abc_BddThen(p, a), Abc_BddThen(p, b) );
    r = Abc_BddUniqueCreate( p, Abc_MinInt(Abc_BddVar(p, a), Abc_BddVar(p, b)), r1, r0 );
    return Abc_BddCacheInsert( p, a, b, r );
}
int Abc_BddOr( Abc_BddMan * p, int a, int b )
{
    return Abc_LitNot( Abc_BddAnd(p, Abc_LitNot(a), Abc_LitNot(b)) );
}

/**Function*************************************************************

  Synopsis    [Counting nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_BddCount_rec( Abc_BddMan * p, int i )
{
    if ( i < 2 )
        return 0;
    if ( Abc_BddMark(p, i) )
        return 0;
    Abc_BddSetMark( p, i, 1 );
    return 1 + Abc_BddCount_rec(p, Abc_BddElse(p, i)) + Abc_BddCount_rec(p, Abc_BddThen(p, i));
}
void Abc_BddUnmark_rec( Abc_BddMan * p, int i )
{
    if ( i < 2 )
        return;
    if ( !Abc_BddMark(p, i) )
        return;
    Abc_BddSetMark( p, i, 0 );
    Abc_BddUnmark_rec( p, Abc_BddElse(p, i) );
    Abc_BddUnmark_rec( p, Abc_BddThen(p, i) );
}
int Abc_BddCountNodes( Abc_BddMan * p, int i )
{
    int Count = Abc_BddCount_rec( p, i );
    Abc_BddUnmark_rec( p, i );
    return Count;
}
int Abc_BddCountNodesArray( Abc_BddMan * p, Vec_Int_t * vNodes )
{
    int i, a, Count = 0;
    Vec_IntForEachEntry( vNodes, a, i )
        Count += Abc_BddCount_rec( p, a );
    Vec_IntForEachEntry( vNodes, a, i )
        Abc_BddUnmark_rec( p, a );
    return Count;
}
int Abc_BddCountNodesArray2( Abc_BddMan * p, Vec_Int_t * vNodes )
{
    int i, a, Count = 0;
    Vec_IntForEachEntry( vNodes, a, i )
    {
        Count += Abc_BddCount_rec( p, a );
        Abc_BddUnmark_rec( p, a );
    }
    return Count;
}



/**Function*************************************************************

  Synopsis    [Printing BDD.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_BddPrint_rec( Abc_BddMan * p, int a, int * pPath )
{
    if ( a == 0 ) 
        return;
    if ( a == 1 )
    { 
        int i;
        for ( i = 0; i < p->nVars; i++ )
            if ( pPath[i] == 0 || pPath[i] == 1 )
                printf( "%c%d", pPath[i] ? '+' : '-', i );
        printf( " " );
        return; 
    }
    pPath[Abc_BddVar(p, a)] =  0;
    Abc_BddPrint_rec( p, Abc_BddElse(p, a), pPath );
    pPath[Abc_BddVar(p, a)] =  1;
    Abc_BddPrint_rec( p, Abc_BddThen(p, a), pPath );
    pPath[Abc_BddVar(p, a)] = -1;
}
void Abc_BddPrint( Abc_BddMan * p, int a )
{
    int * pPath = ABC_FALLOC( int, p->nVars );
    printf( "BDD %d = ", a );
    Abc_BddPrint_rec( p, a, pPath );
    ABC_FREE( pPath );
    printf( "\n" );
}
void Abc_BddPrintTest( Abc_BddMan * p )
{
    int bVarA = Abc_BddIthVar(0);
    int bVarB = Abc_BddIthVar(1);
    int bVarC = Abc_BddIthVar(2);
    int bVarD = Abc_BddIthVar(3);
    int bAndAB = Abc_BddAnd( p, bVarA, bVarB );
    int bAndCD = Abc_BddAnd( p, bVarC, bVarD );
    int bFunc  = Abc_BddOr( p, bAndAB, bAndCD );
    Abc_BddPrint( p, bFunc );
    printf( "Nodes = %d\n", Abc_BddCountNodes(p, bFunc) );
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_BddGiaTest2( Gia_Man_t * pGia, int fVerbose )
{
    Abc_BddMan * p = Abc_BddManAlloc( 10, 100 );
    Abc_BddPrintTest( p );
    Abc_BddManFree( p );
}

void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose )
{
    Abc_BddMan * p;
    Vec_Int_t * vNodes;
    Gia_Obj_t * pObj; int i;
    p = Abc_BddManAlloc( Gia_ManCiNum(pGia), 1 << 20 ); // 30 B/node
    Gia_ManFillValue( pGia );
    Gia_ManConst0(pGia)->Value = 0;
    Gia_ManForEachCi( pGia, pObj, i )
        pObj->Value = Abc_BddIthVar( i );
    vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) );
    Gia_ManForEachAnd( pGia, pObj, i )
    {
        int Cof0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj));
        int Cof1 = Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj));
        pObj->Value = Abc_BddAnd( p, Cof0, Cof1 );
    }
    Gia_ManForEachCo( pGia, pObj, i )
        pObj->Value = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj));
    Gia_ManForEachCo( pGia, pObj, i )
    {
        if ( fVerbose )
            Abc_BddPrint( p, pObj->Value );
        Vec_IntPush( vNodes, pObj->Value );
    }
    printf( "Shared nodes = %d.\n", Abc_BddCountNodesArray2(p, vNodes) );
    Vec_IntFree( vNodes );
    Abc_BddManFree( p );
}

/*
    abc 04> c.aig; &get; &test
    Shared nodes = 80.
    BDD stats: Var = 23  Obj = 206  Alloc = 1048576  Hit = 59  Miss = 216  Mem = 28.00 MB

    abc 05> c.aig; clp -r; ps
    c                             : i/o =   23/    2  lat =    0  nd =     2  edge =     46  bdd  =    80  lev = 1
*/

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END