Simple BDD package.

1 files changed, 395 insertions, 0 deletions

diff --git a/src/misc/extra/extraUtilMult.c b/src/misc/extra/extraUtilMult.c
new file mode 100644
index 00000000..10553b47
--- /dev/null
+++ b/src/misc/extra/extraUtilMult.c
@@ -0,0 +1,395 @@
+/**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
+