Version abc90215

1 files changed, 421 insertions, 0 deletions

diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
new file mode 100644
index 00000000..6d127223
--- /dev/null
+++ b/src/aig/gia/giaSat.c
@@ -0,0 +1,421 @@
+/**CFile****************************************************************
+
+  FileName    [giaSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [New constraint-propagation procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define GIA_LIMIT 10
+
+
+typedef struct Gia_ManSat_t_ Gia_ManSat_t;
+struct Gia_ManSat_t_
+{
+    Aig_MmFlex_t *    pMem;
+};
+
+typedef struct Gia_ObjSat1_t_ Gia_ObjSat1_t;
+struct Gia_ObjSat1_t_
+{
+    char              nFans;
+    char              nOffset;
+    char              PathsH;
+    char              PathsV;
+};
+
+typedef struct Gia_ObjSat2_t_ Gia_ObjSat2_t;
+struct Gia_ObjSat2_t_
+{
+    unsigned          fTerm :  1;
+    unsigned          iLit  : 31;
+};
+
+typedef struct Gia_ObjSat_t_ Gia_ObjSat_t;
+struct Gia_ObjSat_t_
+{
+    union {
+        Gia_ObjSat1_t Obj1;
+        Gia_ObjSat2_t Obj2;
+    };
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_ManSat_t * Gia_ManSatStart()
+{
+    Gia_ManSat_t * p;
+    p = ABC_CALLOC( Gia_ManSat_t, 1 );
+    p->pMem = Aig_MmFlexStart();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSatStop( Gia_ManSat_t * p )
+{
+    Aig_MmFlexStop( p->pMem, 0 );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate rooted at this ]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSatPartCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLits, int * pnLits )
+{
+    Gia_Obj_t * pFanin;
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( pObj->fMark0 == 0 );
+    pFanin = Gia_ObjFanin0(pObj);
+    if ( pFanin->fMark0 || Gia_ObjFaninC0(pObj) )
+        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC0(pObj));
+    else
+        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
+    pFanin = Gia_ObjFanin1(pObj);
+    if ( pFanin->fMark0 || Gia_ObjFaninC1(pObj) )
+        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC1(pObj));
+    else
+        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of words used.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSatPartCreate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pObjPlace, int * pStore )
+{
+    Gia_Obj_t * pFanin;
+    int i, nWordsUsed, nSuperSize = 0, Super[2*GIA_LIMIT];
+    // make sure this is a valid node
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( pObj->fMark0 == 0 );
+    // collect inputs to the supergate
+    Gia_ManSatPartCollectSuper( p, pObj, Super, &nSuperSize );
+    assert( nSuperSize <= 2*GIA_LIMIT );
+    // create the root entry
+    *pObjPlace = 0;
+    ((Gia_ObjSat1_t *)pObjPlace)->nFans   = Gia_Var2Lit( nSuperSize, 0 );
+    ((Gia_ObjSat1_t *)pObjPlace)->nOffset = pStore - pObjPlace;
+    nWordsUsed = nSuperSize;
+    for ( i = 0; i < nSuperSize; i++ )
+    {
+        pFanin = Gia_ManObj( p, Gia_Lit2Var(Super[i]) );
+        if ( pFanin->fMark0 )
+        {
+            ((Gia_ObjSat2_t *)(pStore + i))->fTerm = 1;
+            ((Gia_ObjSat2_t *)(pStore + i))->iLit  = Super[i];
+        }
+        else
+        {
+            assert( Gia_LitIsCompl(Super[i]) );
+            nWordsUsed += Gia_ManSatPartCreate_rec( p, pFanin, pStore + i, pStore + nWordsUsed );
+        }
+    }
+    return nWordsUsed;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates part and returns the number of words used.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSatPartCreate( Gia_Man_t * p, Gia_Obj_t * pObj, int * pStore )
+{
+    return 1 + Gia_ManSatPartCreate_rec( p, pObj, pStore, pStore + 1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of internal nodes in the leaf-DAG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSatPartCountClauses( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnOnset, int * pnOffset )
+{
+    Gia_Obj_t * pFanin;
+    int nOnset0, nOnset1, nOffset0, nOffset1;
+    assert( Gia_ObjIsAnd(pObj) );
+    pFanin = Gia_ObjFanin0(pObj);
+    if ( pFanin->fMark0 )
+        nOnset0 = 1, nOffset0 = 1;
+    else
+    {
+        Gia_ManSatPartCountClauses(p, pFanin, &nOnset0, &nOffset0);
+        if ( Gia_ObjFaninC0(pObj) )
+        {
+            int Temp = nOnset0;
+            nOnset0 = nOffset0;
+            nOffset0 = Temp;
+        }
+    }
+    pFanin = Gia_ObjFanin1(pObj);
+    if ( pFanin->fMark0 )
+        nOnset1 = 1, nOffset1 = 1;
+    else
+    {
+        Gia_ManSatPartCountClauses(p, pFanin, &nOnset1, &nOffset1);
+        if ( Gia_ObjFaninC1(pObj) )
+        {
+            int Temp = nOnset1;
+            nOnset1 = nOffset1;
+            nOffset1 = Temp;
+        }
+    }
+    *pnOnset  = nOnset0  * nOnset1;
+    *pnOffset = nOffset0 + nOffset1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of internal nodes in the leaf-DAG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int * pnNodes )
+{
+    Gia_Obj_t * pFanin;
+    int Level0 = 0, Level1 = 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( pObj->fMark0 == 0 );
+    (*pnNodes)++;
+    pFanin = Gia_ObjFanin0(pObj);
+    if ( pFanin->fMark0 )
+        (*pnLeaves)++;
+    else
+        Level0 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC0(pObj);
+    pFanin = Gia_ObjFanin1(pObj);
+    if ( pFanin->fMark0 )
+        (*pnLeaves)++;
+    else
+        Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
+    return AIG_MAX( Level0, Level1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of internal nodes in the leaf-DAG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSatPartCountNodes( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pFanin;
+    int nNodes0 = 0, nNodes1 = 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( pObj->fMark0 == 0 );
+    pFanin = Gia_ObjFanin0(pObj);
+    if ( !(pFanin->fMark0) )
+        nNodes0 = Gia_ManSatPartCountNodes(p, pFanin);
+    pFanin = Gia_ObjFanin1(pObj);
+    if ( !(pFanin->fMark0) )
+        nNodes1 = Gia_ManSatPartCountNodes(p, pFanin);
+    return nNodes0 + nNodes1 + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of internal nodes in the leaf-DAG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSatPartPrint( Gia_Man_t * p, Gia_Obj_t * pObj, int Step )
+{
+    Gia_Obj_t * pFanin;
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( pObj->fMark0 == 0 );
+    pFanin = Gia_ObjFanin0(pObj);
+    if ( pFanin->fMark0 )
+        printf( "%s%d", Gia_ObjFaninC0(pObj)?"!":"", Gia_ObjId(p,pFanin) );
+    else
+    {
+        if ( Gia_ObjFaninC0(pObj) )
+            printf( "(" );
+        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC0(pObj));
+        if ( Gia_ObjFaninC0(pObj) )
+            printf( ")" );
+    }
+    printf( "%s", (Step & 1)? " + " : "*" );
+    pFanin = Gia_ObjFanin1(pObj);
+    if ( pFanin->fMark0 )
+        printf( "%s%d", Gia_ObjFaninC1(pObj)?"!":"", Gia_ObjId(p,pFanin) );
+    else
+    {
+        if ( Gia_ObjFaninC1(pObj) )
+            printf( "(" );
+        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC1(pObj));
+        if ( Gia_ObjFaninC1(pObj) )
+            printf( ")" );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSatExperiment( Gia_Man_t * p )
+{
+    int nStored, Storage[1000], * pStart; 
+    Gia_ManSat_t * pMan;
+    Gia_Obj_t * pObj;
+    int i, nLevels, nLeaves, nNodes, nCount[2*GIA_LIMIT+2] = {0}, nCountAll = 0;
+    int Num0 = 0, Num1 = 0;
+    int clk = clock(), nWords = 0, nWords2 = 0;
+    pMan = Gia_ManSatStart();
+    // mark the nodes to become roots of leaf-DAGs
+    Gia_ManSetRefs( p );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->fMark0 = 1;
+        else if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( pObj->Value > 1 || Gia_ManSatPartCountNodes(p,pObj) >= GIA_LIMIT )
+                pObj->fMark0 = 1;
+        }
+        pObj->Value = 0;
+    }
+    // compute the sizes of leaf-DAGs
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( pObj->fMark0 == 0 )
+            continue;
+        pObj->fMark0 = 0;
+
+        nCountAll++;
+        nStored = Gia_ManSatPartCreate( p, pObj, Storage );
+        nWords2 += nStored;
+        assert( nStored < 500 );
+        pStart = (int *)Aig_MmFlexEntryFetch( pMan->pMem, sizeof(int) * nStored );
+        memcpy( pStart, Storage, sizeof(int) * nStored );
+
+        nLeaves = nNodes = 0;
+        nLevels = 1+Gia_ManSatPartCount( p, pObj, &nLeaves, &nNodes );
+        nWords += nLeaves + nNodes;
+        if ( nNodes <= 2*GIA_LIMIT )
+            nCount[nNodes]++;
+        else
+            nCount[2*GIA_LIMIT+1]++;
+//        if ( nNodes > 10 && i % 100 == 0 )
+//        if ( nNodes > 5 )
+        if ( 0 )
+        {
+            Gia_ManSatPartCountClauses( p, pObj, &Num0, &Num1 );
+            printf( "%8d :  And = %3d.  Lev = %2d. Clauses = %3d. (%3d + %3d).\n", i, nNodes, nLevels, Num0+Num1, Num0, Num1 );
+            Gia_ManSatPartPrint( p, pObj, 0 );
+            printf( "\n" );
+        }
+
+        pObj->fMark0 = 1;
+    }
+    printf( "\n" );
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = 0;
+    Gia_ManSatStop( pMan );
+    for ( i = 0; i < 2*GIA_LIMIT+2; i++ )
+        printf( "%2d=%6d  %7.2f %%  %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) );
+    ABC_PRM( "MemoryEst", 4*nWords );
+    ABC_PRM( "MemoryReal", 4*nWords2 );
+    printf( "%5.2f bpn  ", 4.0*nWords2/Gia_ManObjNum(p) );
+    ABC_PRT( "Time", clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+