Version abc60115

abc.dsp

@@ -1045,6 +1045,70 @@ SOURCE=.\src\sat\csat\csat_apis.c
 SOURCE=.\src\sat\csat\csat_apis.h
 # End Source File
 # End Group
+# Begin Group "aig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigReplace.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigClass.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigProve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigSim.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "opt"
 

abc.plg

@@ -6,13 +6,13 @@
 --------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" with contents
 [
 /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
-"C:\_projects\abc\src\opt\xyz\xyzCore.c"
+"C:\_projects\abc\src\sat\aig\aigReplace.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
 .\Debug\abcAig.obj
@@ -187,6 +187,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\msatClause.obj
 .\Debug\msatClauseVec.obj
 .\Debug\msatMem.obj
+.\Debug\msatOrderJ.obj
 .\Debug\msatQueue.obj
 .\Debug\msatRead.obj
 .\Debug\msatSolverApi.obj
@@ -208,6 +209,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\fraigUtil.obj
 .\Debug\fraigVec.obj
 .\Debug\csat_apis.obj
+.\Debug\aigBalance.obj
+.\Debug\aigFanout.obj
+.\Debug\aigMan.obj
+.\Debug\aigMem.obj
+.\Debug\aigNode.obj
+.\Debug\aigOper.obj
+.\Debug\aigUtil.obj
 .\Debug\fxu.obj
 .\Debug\fxuCreate.obj
 .\Debug\fxuHeapD.obj
@@ -338,14 +346,20 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\mvcPrint.obj
 .\Debug\mvcSort.obj
 .\Debug\mvcUtils.obj
-.\Debug\msatOrderJ.obj
+.\Debug\aigTable.obj
+.\Debug\aigCheck.obj
+.\Debug\aigReplace.obj
+.\Debug\fraigCore.obj
+.\Debug\fraigProve.obj
+.\Debug\fraigSim.obj
+.\Debug\fraigClass.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp"
 <h3>Output Window</h3>
 Compiling...
-xyzCore.c
+aigReplace.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with contents
 [
 /nologo /o"Debug/abc.bsc" 
 .\Debug\abcAig.sbr
@@ -520,6 +534,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\msatClause.sbr
 .\Debug\msatClauseVec.sbr
 .\Debug\msatMem.sbr
+.\Debug\msatOrderJ.sbr
 .\Debug\msatQueue.sbr
 .\Debug\msatRead.sbr
 .\Debug\msatSolverApi.sbr
@@ -541,6 +556,13 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\fraigUtil.sbr
 .\Debug\fraigVec.sbr
 .\Debug\csat_apis.sbr
+.\Debug\aigBalance.sbr
+.\Debug\aigFanout.sbr
+.\Debug\aigMan.sbr
+.\Debug\aigMem.sbr
+.\Debug\aigNode.sbr
+.\Debug\aigOper.sbr
+.\Debug\aigUtil.sbr
 .\Debug\fxu.sbr
 .\Debug\fxuCreate.sbr
 .\Debug\fxuHeapD.sbr
@@ -671,8 +693,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\mvcPrint.sbr
 .\Debug\mvcSort.sbr
 .\Debug\mvcUtils.sbr
-.\Debug\msatOrderJ.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp"
+.\Debug\aigTable.sbr
+.\Debug\aigCheck.sbr
+.\Debug\aigReplace.sbr
+.\Debug\fraigCore.sbr
+.\Debug\fraigProve.sbr
+.\Debug\fraigSim.sbr
+.\Debug\fraigClass.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 

abclib.dsp

@@ -457,6 +457,10 @@ SOURCE=.\src\base\io\ioWriteList.c
 
 SOURCE=.\src\base\io\ioWritePla.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteVerilog.c
+# End Source File
 # End Group
 # Begin Group "main"
 

src/base/abc/abc.h

@@ -211,7 +211,7 @@ struct Abc_Ntk_t_
 // transforming floats into ints and back
 static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
 static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);             }
-static inline int         Abc_BitWordNum( int nBits )                { return nBits/32 + ((nBits%32) > 0);  }
+static inline int         Abc_BitWordNum( int nBits )                { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
 
 // checking the network type
 static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST; }
@@ -487,6 +487,8 @@ extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
+extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
+extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
 extern void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );

src/base/abci/abc.c

@@ -3745,7 +3745,9 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
+//    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
+    pNtkRes = NULL;
+
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -3811,7 +3813,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    Abc_NtkTestEsop( pNtk );
+//    Abc_NtkTestEsop( pNtk );
 //    Abc_NtkTestSop( pNtk );
 //    printf( "This command is currently not used.\n" );
 

src/base/abci/abcMiter.c

@@ -350,6 +350,94 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of two cofactors of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
+{
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( 1 == Abc_NtkCoNum(pNtk) );
+    assert( In < Abc_NtkCiNum(pNtk) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter->pName = util_strsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
+
+    // get the root output
+    pRoot = Abc_NtkCo( pNtk, 0 );
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    // set the first cofactor
+    Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) );
+    // add the first cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+    // save the output
+    pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
+
+    // set the second cofactor
+    Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter );
+    // add the second cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+    // save the output
+    pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
+
+    // create the miter of the two outputs
+    if ( fExist ) 
+        pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    else
+        pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiter: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of two cofactors of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkTemp;
+    Abc_Obj_t * pObj;
+    int i;
+
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        pNtk = Abc_NtkMiterQuantify( pNtkTemp = pNtk, i, 1 );
+        Abc_NtkDelete( pNtkTemp );
+    }
+
+    return pNtk;
+}
+
 
 
 

src/sat/aig/aigBalance.c

+/**CFile****************************************************************
+
+  FileName    [aigBalance.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigBalance.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigCheck.c

+/**CFile****************************************************************
+
+  FileName    [aigCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_ManCheck( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pObj, * pAnd;
+    int i;
+    Aig_ManForEachNode( pMan, pObj, i )
+    {
+        if ( pObj == pMan->pConst1 || Aig_NodeIsPi(pObj) )
+        {
+            if ( pObj->Fans[0].iNode || pObj->Fans[1].iNode || pObj->Level )
+            {
+                printf( "Aig_ManCheck: The AIG has non-standard constant or PI node \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        if ( Aig_NodeIsPo(pObj) )
+        {
+            if ( pObj->Fans[1].iNode )
+            {
+                printf( "Aig_ManCheck: The AIG has non-standard PO node \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        // consider the AND node
+        if ( !pObj->Fans[0].iNode || !pObj->Fans[1].iNode )
+        {
+            printf( "Aig_ManCheck: The AIG has node \"%d\" with a constant fanin.\n", pObj->Id );
+            return 0;
+        }
+        if ( pObj->Fans[0].iNode > pObj->Fans[1].iNode )
+        {
+            printf( "Aig_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
+            return 0;
+        }
+        if ( pObj->Level != 1 + AIG_MAX(Aig_NodeFanin0(pObj)->Level, Aig_NodeFanin1(pObj)->Level) )
+            printf( "Aig_ManCheck: Node \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
+        pAnd = Aig_TableLookupNode( pMan, Aig_NodeChild0(pObj), Aig_NodeChild1(pObj) );
+        if ( pAnd != pObj )
+            printf( "Aig_ManCheck: Node \"%d\" is not in the structural hashing table.\n", pObj->Id );
+    }
+    // count the number of nodes in the table
+    if ( Aig_TableNumNodes(pMan->pTable) != Aig_ManAndNum(pMan) )
+    {
+        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the node has a combination loop of depth 1 or 2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot )
+{
+    Aig_Node_t * pFanin0, * pFanin1;
+    Aig_Node_t * pChild00, * pChild01;
+    Aig_Node_t * pChild10, * pChild11;
+    if ( !Aig_NodeIsAnd(pNode) )
+        return 1;
+    pFanin0 = Aig_NodeFanin0(pNode);
+    pFanin1 = Aig_NodeFanin1(pNode);
+    if ( pRoot == pFanin0 || pRoot == pFanin1 )
+        return 0;
+    if ( Aig_NodeIsPi(pFanin0) )
+    {
+        pChild00 = NULL;
+        pChild01 = NULL;
+    }
+    else
+    {
+        pChild00 = Aig_NodeFanin0(pFanin0);
+        pChild01 = Aig_NodeFanin1(pFanin0);
+        if ( pRoot == pChild00 || pRoot == pChild01 )
+            return 0;
+    }
+    if ( Aig_NodeIsPi(pFanin1) )
+    {
+        pChild10 = NULL;
+        pChild11 = NULL;
+    }
+    else
+    {
+        pChild10 = Aig_NodeFanin0(pFanin1);
+        pChild11 = Aig_NodeFanin1(pFanin1);
+        if ( pRoot == pChild10 || pRoot == pChild11 )
+            return 0;
+    }
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigMan.c

+/**CFile****************************************************************
+
+  FileName    [aigMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSetDefaultParams( Aig_Param_t * pParam )
+{
+    memset( pParam, 0, sizeof(Aig_Param_t) );
+    pParam->nPatsRand = 1024;  // the number of random patterns
+    pParam->nBTLimit  =   99;  // backtrack limit at the intermediate nodes
+    pParam->nSeconds  =    1;  // the timeout for the final miter in seconds
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
+{
+    Aig_Man_t * p;
+    // set the random seed for simulation
+    srand( 0xDEADCAFE );
+    // start the manager
+    p = ALLOC( Aig_Man_t, 1 );
+    memset( p, 0, sizeof(Aig_Man_t) );
+    p->pParam = &p->Param;
+    p->nTravIds = 1;
+    // set the defaults
+    *p->pParam = *pParam;
+    // start memory managers
+    p->mmNodes    = Aig_MemFixedStart( sizeof(Aig_Node_t) );
+    // allocate node arrays
+    p->vPis       = Vec_PtrAlloc( 1000 );    // the array of primary inputs
+    p->vPos       = Vec_PtrAlloc( 1000 );    // the array of primary outputs
+    p->vNodes     = Vec_PtrAlloc( 1000 );    // the array of internal nodes
+    // start the table
+    p->pTable     = Aig_TableCreate( 1000 );
+    // create the constant node
+    p->pConst1    = Aig_NodeCreateConst( p );
+    // initialize other variables
+    p->vFanouts   = Vec_PtrAlloc( 10 ); 
+    p->vToReplace = Vec_PtrAlloc( 10 ); 
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCleanup( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pAnd;
+    int i, nNodesOld;
+    nNodesOld = Aig_ManAndNum(pMan);
+    Aig_ManForEachAnd( pMan, pAnd, i )
+        if ( pAnd->nRefs == 0 )
+            Aig_NodeDeleteAnd_rec( pMan, pAnd );
+    return nNodesOld - Aig_ManAndNum(pMan);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStop( Aig_Man_t * p )
+{
+    if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots );
+    if ( p->vFanFans0 )  Vec_PtrFree( p->vFanFans0 );
+    if ( p->vFanFans1 )  Vec_PtrFree( p->vFanFans1 );
+    if ( p->vClasses  )  Vec_VecFree( p->vClasses );
+    Aig_MemFixedStop( p->mmNodes, 0 );
+    Vec_PtrFree( p->vNodes );
+    Vec_PtrFree( p->vPis );
+    Vec_PtrFree( p->vPos );
+    Vec_PtrFree( p->vFanouts );
+    Vec_PtrFree( p->vToReplace );
+    Aig_TableFree( p->pTable );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigMem.c

+/**CFile****************************************************************
+
+  FileName    [aigMem.c]
+
+  PackageName [ABC: Logic synthesis and verification system.]
+
+  Synopsis    [Fixed-size-entry memory manager for the AIG package.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - October 1, 2004]
+
+  Revision    [$Id: aigMem.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Aig_MemFixed_t_
+{
+    // information about individual entries
+    int           nEntrySize;    // the size of one entry
+    int           nEntriesAlloc; // the total number of entries allocated
+    int           nEntriesUsed;  // the number of entries in use
+    int           nEntriesMax;   // the max number of entries in use
+    char *        pEntriesFree;  // the linked list of free entries
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the internal memory manager.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize )
+{
+    Aig_MemFixed_t * p;
+
+    p = ALLOC( Aig_MemFixed_t, 1 );
+    memset( p, 0, sizeof(Aig_MemFixed_t) );
+
+    p->nEntrySize    = nEntrySize;
+    p->nEntriesAlloc = 0;
+    p->nEntriesUsed  = 0;
+    p->pEntriesFree  = NULL;
+
+    if ( nEntrySize * (1 << 10) < (1<<16) )
+        p->nChunkSize = (1 << 10);
+    else
+        p->nChunkSize = (1<<16) / nEntrySize;
+    if ( p->nChunkSize < 8 )
+        p->nChunkSize = 8;
+
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+            p->nEntrySize, p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts one entry from the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p )
+{
+    char * pTemp;
+    int i;
+
+    // check if there are still free entries
+    if ( p->nEntriesUsed == p->nEntriesAlloc )
+    { // need to allocate more entries
+        assert( p->pEntriesFree == NULL );
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+        // transform these entries into a linked list
+        pTemp = p->pEntriesFree;
+        for ( i = 1; i < p->nChunkSize; i++ )
+        {
+            *((char **)pTemp) = pTemp + p->nEntrySize;
+            pTemp += p->nEntrySize;
+        }
+        // set the last link
+        *((char **)pTemp) = NULL;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+        // add to the number of entries allocated
+        p->nEntriesAlloc += p->nChunkSize;
+    }
+    // incrememt the counter of used entries
+    p->nEntriesUsed++;
+    if ( p->nEntriesMax < p->nEntriesUsed )
+        p->nEntriesMax = p->nEntriesUsed;
+    // return the first entry in the free entry list
+    pTemp = p->pEntriesFree;
+    p->pEntriesFree = *((char **)pTemp);
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns one entry into the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry )
+{
+    // decrement the counter of used entries
+    p->nEntriesUsed--;
+    // add the entry to the linked list of free entries
+    *((char **)pEntry) = p->pEntriesFree;
+    p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees all associated memory and resets the manager.]
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedRestart( Aig_MemFixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // delocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    p->nChunks = 1;
+    // transform these entries into a linked list
+    pTemp = p->pChunks[0];
+    for ( i = 1; i < p->nChunkSize; i++ )
+    {
+        *((char **)pTemp) = pTemp + p->nEntrySize;
+        pTemp += p->nEntrySize;
+    }
+    // set the last link
+    *((char **)pTemp) = NULL;
+    // set the free entry list
+    p->pEntriesFree  = p->pChunks[0];
+    // set the correct statistics
+    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
+    p->nMemoryUsed   = 0;
+    p->nEntriesAlloc = p->nChunkSize;
+    p->nEntriesUsed  = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports the memory usage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigNode.c

+/**CFile****************************************************************
+
+  FileName    [aigNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    // create the node
+    pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes );
+    memset( pNode, 0, sizeof(Aig_Node_t) );
+    // assign the number and add to the array of nodes
+    pNode->Id = p->vNodes->nSize;
+    Vec_PtrPush( p->vNodes, pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the constant 1 node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    pNode->fPhase = 1; // sim value for 000... pattern
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary input node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Vec_PtrPush( p->vPis, pNode );
+    pNode->fPhase  =  0;  // sim value for 000... pattern
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary output node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Vec_PtrPush( p->vPos, pNode );
+    // connect to the fanin
+    pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
+    pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id;
+    pNode->fPhase = pNode->Fans[0].fComp ^ Aig_Regular(pFanin)->fPhase;  // sim value for 000... pattern
+    pNode->Level = Aig_Regular(pFanin)->Level;
+    Aig_Regular(pFanin)->nRefs++;
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin, pNode );
+    // update global level if needed
+    if ( p->nLevelMax < (int)pNode->Level )
+        p->nLevelMax = pNode->Level;
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the nodes to the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode )
+{
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_NodeIsAnd(pNode) );
+    // add the fanins
+    pNode->Fans[0].fComp = Aig_IsComplement(pFanin0);
+    pNode->Fans[0].iNode = Aig_Regular(pFanin0)->Id;
+    pNode->Fans[1].fComp = Aig_IsComplement(pFanin1);
+    pNode->Fans[1].iNode = Aig_Regular(pFanin1)->Id;
+    // compute the phase (sim value for 000... pattern)
+    pNode->fPhase = (pNode->Fans[0].fComp ^ Aig_Regular(pFanin0)->fPhase) & 
+                    (pNode->Fans[1].fComp ^ Aig_Regular(pFanin1)->fPhase);
+    pNode->Level = Aig_NodeGetLevelNew(pNode);
+    // reference the fanins
+    Aig_Regular(pFanin0)->nRefs++;
+    Aig_Regular(pFanin1)->nRefs++;
+    // add the fanouts
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin0, pNode );
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin1, pNode );
+    // add the node to the structural hash table
+    Aig_TableInsertNode( pNode->pMan, pFanin0, pFanin1, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the nodes to the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeDisconnectAnd( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanin0, * pFanin1;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_NodeIsAnd(pNode) );
+    // get the fanins
+    pFanin0 = Aig_NodeFanin0(pNode);
+    pFanin1 = Aig_NodeFanin1(pNode);
+    // dereference the fanins
+    pFanin0->nRefs--;
+    pFanin0->nRefs--;
+    // remove the fanouts
+    if ( pNode->pMan->vFanPivots )  Aig_NodeRemoveFaninFanout( pFanin0, pNode );
+    if ( pNode->pMan->vFanPivots )  Aig_NodeRemoveFaninFanout( pFanin1, pNode );
+    // remove the node from the structural hash table
+    Aig_TableDeleteNode( pNode->pMan, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal deletion step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot )
+{
+    Aig_Node_t * pNode0, * pNode1;
+    // make sure the node is regular and dangling
+    assert( !Aig_IsComplement(pRoot) );
+    assert( pRoot->nRefs == 0 );
+    assert( Aig_NodeIsAnd(pRoot) );
+    // save the children
+    pNode0 = Aig_NodeFanin0(pRoot);
+    pNode1 = Aig_NodeFanin1(pRoot);
+    // disconnect the node
+    Aig_NodeDisconnectAnd( pRoot );
+    // recycle the node
+    Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL );
+    Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot );
+    // call recursively
+    if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pNode0 );
+    if ( Aig_NodeIsAnd(pNode1) && pNode1->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pNode1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the AIG node for debugging purposes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodePrint( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pNodeR = Aig_Regular(pNode);
+    if ( Aig_NodeIsPi(pNode) )
+    {
+        printf( "PI %4s%s.\n", Aig_NodeName(pNode), Aig_IsComplement(pNode)? "\'" : "" );
+        return;
+    }
+    if ( Aig_NodeIsConst(pNode) )
+    {
+        printf( "Constant 1 %s.\n", Aig_IsComplement(pNode)? "(complemented)" : ""  );
+        return;
+    }
+    // print the node's function
+    printf( "%7s%s", Aig_NodeName(pNodeR),                 Aig_IsComplement(pNode)? "\'" : "" );
+    printf( " = " );
+    printf( "%7s%s", Aig_NodeName(Aig_NodeFanin0(pNodeR)), Aig_NodeFaninC0(pNodeR)? "\'" : "" );
+    printf( " * " );
+    printf( "%7s%s", Aig_NodeName(Aig_NodeFanin1(pNodeR)), Aig_NodeFaninC1(pNodeR)? "\'" : "" );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the name of the node.]
+
+  Description [The name should be used before this procedure is called again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_NodeName( Aig_Node_t * pNode )
+{
+    static char Buffer[100];
+    sprintf( Buffer, "%d", Aig_Regular(pNode)->Id );
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigOper.c

+/**CFile****************************************************************
+
+  FileName    [aigOper.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigOper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    Aig_Node_t * pAnd;
+    // check for trivial cases
+    if ( p0 == p1 )
+        return p0;
+    if ( p0 == Aig_Not(p1) )
+        return Aig_Not(pMan->pConst1);
+    if ( Aig_Regular(p0) == pMan->pConst1 )
+    {
+        if ( p0 == pMan->pConst1 )
+            return p1;
+        return Aig_Not(pMan->pConst1);
+    }
+    if ( Aig_Regular(p1) == pMan->pConst1 )
+    {
+        if ( p1 == pMan->pConst1 )
+            return p0;
+        return Aig_Not(pMan->pConst1);
+    }
+    // order the arguments
+    if ( Aig_Regular(p0)->Id > Aig_Regular(p1)->Id )
+    {
+        if ( pAnd = Aig_TableLookupNode( pMan, p1, p0 ) )
+            return pAnd;
+        return Aig_NodeCreateAnd( pMan, p1, p0 );
+    }
+    else
+    {
+        if ( pAnd = Aig_TableLookupNode( pMan, p0, p1 ) )
+            return pAnd;
+        return Aig_NodeCreateAnd( pMan, p0, p1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean OR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    return Aig_Not( Aig_And( pMan, Aig_Not(p0), Aig_Not(p1) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    return Aig_Or( pMan, Aig_And(pMan, p0, Aig_Not(p1)), 
+                         Aig_And(pMan, p1, Aig_Not(p0)) );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 )
+{
+    return Aig_Or( pMan, Aig_And(pMan, pC, p1), Aig_And(pMan, Aig_Not(pC), p0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Miter_rec( Aig_Man_t * pMan, Aig_Node_t ** ppObjs, int nObjs )
+{
+    Aig_Node_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Aig_Miter_rec( pMan, ppObjs,           nObjs/2         );
+    pObj2 = Aig_Miter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
+    return Aig_Or( pMan, pObj1, pObj2 );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs )
+{
+    int i;
+    if ( vPairs->nSize == 0 )
+        return Aig_Not( pMan->pConst1 );
+    assert( vPairs->nSize % 2 == 0 );
+    // go through the cubes of the node's SOP
+    for ( i = 0; i < vPairs->nSize; i += 2 )
+        vPairs->pArray[i/2] = Aig_Xor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    vPairs->nSize = vPairs->nSize/2;
+    return Aig_Miter_rec( pMan, (Aig_Node_t **)vPairs->pArray, vPairs->nSize );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigReplace.c

+/**CFile****************************************************************
+
+  FileName    [aigUpdate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigUpdate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal replacement step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_AigReplace_int( Aig_Man_t * pMan, int fUpdateLevel )
+{
+    Vec_Ptr_t * vFanouts;
+    Aig_Node_t * pOld, * pNew, * pFanin0, * pFanin1, * pFanout, * pTemp, * pFanoutNew;
+    int k, iFanin;
+    // get the pair of nodes to replace
+    assert( Vec_PtrSize(pMan->vToReplace) > 0 );
+    pNew = Vec_PtrPop( pMan->vToReplace );
+    pOld = Vec_PtrPop( pMan->vToReplace );
+    // make sure the old node is internal, regular, and has fanouts
+    // (the new node can be PI or internal, is complemented, and can have fanouts)
+    assert( !Aig_IsComplement(pOld) );
+    assert( pOld->nRefs > 0 );
+    assert( Aig_NodeIsAnd(pOld) );
+    assert( Aig_NodeIsPo(pNew) );
+    // look at the fanouts of old node
+    vFanouts = Aig_NodeGetFanouts( pOld );
+    Vec_PtrForEachEntry( vFanouts, pFanout, k )
+    {
+        if ( Aig_NodeIsPo(pFanout) )
+        {
+            // patch the first fanin of the PO
+            pFanout->Fans[0].iNode  = Aig_Regular(pNew)->Id;
+            pFanout->Fans[0].fComp ^= Aig_IsComplement(pNew);
+            continue;
+        }
+        // find the old node as a fanin of this fanout
+        iFanin = Aig_NodeWhatFanin( pFanout, pOld );
+        assert( iFanin == 0 || iFanin == 1 );
+        // get the new fanin
+        pFanin0 = Aig_NotCond( pNew, pFanout->Fans[iFanin].fComp );
+        assert( Aig_Regular(pFanin0) != pFanout );
+        // get another fanin
+        pFanin1 = iFanin? Aig_NodeChild0(pFanout) : Aig_NodeChild1(pFanout);
+        assert( Aig_Regular(pFanin1) != pFanout );
+        assert( Aig_Regular(pFanin0) != Aig_Regular(pFanin1) );             
+        // order them
+        if ( Aig_Regular(pFanin0)->Id > Aig_Regular(pFanin1)->Id ) 
+            pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
+        // check if the node with these fanins exists
+        if ( pFanoutNew = Aig_TableLookupNode( pMan, pFanin0, pFanin1 ) )
+        { // such node exists (it may be a constant)
+            // schedule replacement of the old fanout by the new fanout
+            Vec_PtrPush( pMan->vToReplace, pFanout );
+            Vec_PtrPush( pMan->vToReplace, pFanoutNew );
+            continue;
+        }
+        // such node does not exist - modify the old fanout node 
+        // (this way the change will not propagate all the way to the COs)
+        Aig_NodeDisconnectAnd( pFanout );
+        Aig_NodeConnectAnd( pFanin0, pFanin1, pFanout );
+        // recreate the old fanout with new fanins and add it to the table
+        assert( Aig_NodeIsAcyclic(pFanout, pFanout) );
+        // update the level if requested
+        if ( fUpdateLevel )
+        {
+            if ( Aig_NodeUpdateLevel_int(pFanout) )
+                pMan->nLevelMax = Aig_ManGetLevelMax( pMan );
+            //Aig_NodeGetLevelRNew( pFanout );
+            Aig_NodeUpdateLevelR_int( pFanout );
+        }
+    }
+    // if the node has no fanouts left, remove its MFFC
+    if ( pOld->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one AIG node by the other.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel )
+{
+    assert( Vec_PtrSize(pMan->vToReplace) == 0 );
+    Vec_PtrPush( pMan->vToReplace, pOld );
+    Vec_PtrPush( pMan->vToReplace, pNew );
+    while ( Vec_PtrSize(pMan->vToReplace) )
+        Abc_AigReplace_int( pMan, fUpdateLevel );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/aigUtil.c

+/**CFile****************************************************************
+
+  FileName    [aigUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManIncrementTravId( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pObj;
+    int i;
+    if ( pMan->nTravIds == (1<<24)-1 )
+    {
+        pMan->nTravIds = 0;
+        Aig_ManForEachNode( pMan, pObj, i )
+            pObj->TravId = 0;
+    }
+    pMan->nTravIds++;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/fraigClass.c

+/**CFile****************************************************************
+
+  FileName    [aigFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "stmm.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the equivalence classes of patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
+{
+    Vec_Vec_t * vClasses;     // equivalence classes
+    stmm_table * tSim2Node;  // temporary hash table hashing key into the class number
+    Aig_Node_t * pNode;       
+    unsigned uKey;
+    int i, * pSpot, ClassNum;
+    assert( pInfo->Type == 1 );
+    // fill in the hash table
+    tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vClasses = Vec_VecAlloc( 100 );
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        if ( Aig_NodeIsPo(pNode) )
+            continue;
+        uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords );
+        if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist
+            *pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing
+        else if ( (*pSpot) & 1 ) // this is a node
+        {
+            // create the class
+            ClassNum = Vec_VecSize( vClasses );
+            Vec_VecPush( vClasses, ClassNum, (void *)((*pSpot) >> 1) );
+            Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
+            // save the class
+            *pSpot = (ClassNum << 1); 
+        }
+        else // this is a class
+        {
+            ClassNum = (*pSpot) >> 1;
+            Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
+        }
+    }
+    stmm_free_table( tSim2Node );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the hash key of the simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Aig_ManHashKey( unsigned * pData, int nWords )
+{
+    static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
+    unsigned uKey;
+    int i;
+    uKey = 0;
+    for ( i = 0; i < nWords; i++ )
+        uKey ^= pData[i] * Primes[i%10];
+    return uKey;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/fraigCore.c

+/**CFile****************************************************************
+
+  FileName    [aigFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/fraigProve.c

+/**CFile****************************************************************
+
+  FileName    [aigProve.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/aig/fraigSim.c

+/**CFile****************************************************************
+
+  FileName    [aigSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates all nodes using random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
+{
+    Aig_SimInfo_t * pInfoPi, * pInfoAll;
+    assert( p->pInfo && p->pInfoTemp );
+    // create random PI info
+    pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
+    Aig_SimInfoRandom( pInfoPi );
+    // simulate it though the circuit
+    pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
+    // detect classes
+    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+    Aig_SimInfoFree( pInfoAll );
+    // save simulation info
+    p->pInfo = pInfoPi;
+    p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates all nodes using the given simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
+{
+    Aig_SimInfo_t * pInfoAll;
+    Aig_Node_t * pNode;
+    unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
+    int i, k, fComp0, fComp1;
+
+    assert( !pInfoPi->Type ); // PI siminfo
+    // allocate sim info for all nodes
+    pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
+    // set the constant sim info
+    pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
+    for ( k = 0; k < pInfoPi->nWords; k++ )
+        pData1[k] = ~((unsigned)0);
+    // copy the PI siminfo
+    Vec_PtrForEachEntry( p->vPis, pNode, i )
+    {
+        pDataPi  = Aig_SimInfoForPi( pInfoPi, i );
+        pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
+        for ( k = 0; k < pInfoPi->nWords; k++ )
+            pDataAnd[k] = pDataPi[k];
+    }
+    // simulate the nodes
+    Vec_PtrForEachEntry( p->vNodes, pNode, i )
+    {
+        if ( !Aig_NodeIsAnd(pNode) )
+            continue;
+        pData0   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
+        pData1   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
+        pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode                 );
+        fComp0 = Aig_NodeFaninC0(pNode);
+        fComp1 = Aig_NodeFaninC1(pNode);
+        if ( fComp0 && fComp1 )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] = ~pData0[k] & ~pData1[k];
+        else if ( fComp0  )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] = ~pData0[k] &  pData1[k];
+        else if ( fComp1 )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] =  pData0[k] & ~pData1[k];
+        else 
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] =  pData0[k] &  pData1[k];
+    }
+    return pInfoAll;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
+{
+    Aig_SimInfo_t * p;
+    p = ALLOC( Aig_SimInfo_t, 1 );
+    memset( p, 0, sizeof(Aig_SimInfo_t) );
+    p->Type     = Type;
+    p->nNodes   = nNodes;
+    p->nWords   = nWords;
+    p->nPatsMax = nWords * sizeof(unsigned) * 8;
+    p->pData    = ALLOC( unsigned, nNodes * nWords );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoClean( Aig_SimInfo_t * p )
+{
+    int i, Size = p->nNodes * p->nWords;
+    p->nPatsCur = 0;
+    for ( i = 0; i < Size; i++ )
+        p->pData[i] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoRandom( Aig_SimInfo_t * p )
+{
+    int i, Size = p->nNodes * p->nWords;
+    unsigned * pData;
+    for ( i = 0; i < Size; i++ )
+        p->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
+    // make sure the first bit of all nodes is 0
+    for ( i = 0; i < p->nNodes; i++ )
+    {
+        pData = p->pData + p->nWords * i;
+        *pData <<= 1;
+    }
+    p->nPatsCur = p->nPatsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoResize( Aig_SimInfo_t * p )
+{
+    unsigned * pData;
+    int i, k;
+    assert( p->nPatsCur == p->nPatsMax );
+    pData = ALLOC( unsigned, 2 * p->nNodes * p->nWords );
+    for ( i = 0; i < p->nNodes; i++ )
+    {
+        for ( k = 0; k < p->nWords; k++ )
+            pData[2 * p->nWords * i + k] = p->pData[p->nWords * i + k];
+        for ( k = 0; k < p->nWords; k++ )
+            pData[2 * p->nWords * i + k + p->nWords] = 0;
+    }
+    p->nPatsMax *= 2;
+    p->nWords   *= 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoFree( Aig_SimInfo_t * p )
+{
+    free( p->pData );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/csat/csat_apis.c

@@ -291,6 +291,8 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
     // check that there is no dangling nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( i == 0 ) 
+            continue;
         if ( Abc_ObjFanoutNum(pObj) == 0 )
         {
             printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );

src/sat/fraig/fraigSat.c

@@ -233,7 +233,7 @@ clk = clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
 
-Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
+//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
 
     if ( RetValue1 == MSAT_FALSE )
     {