Version abc60115

17 files changed, 2750 insertions, 1 deletions

diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
new file mode 100644
index 00000000..009a17bb
--- /dev/null
+++ b/src/sat/aig/aig.h
@@ -0,0 +1,308 @@
+/**CFile****************************************************************
+
+  FileName    [aig.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __AIG_H__
+#define __AIG_H__
+
+/*
+    AIG is an And-Inv Graph with structural hashing.
+    It is always structurally hashed. It means that at any time:
+    - for each AND gate, there are no other AND gates with the same children
+    - the constants are propagated
+    - there is no single-input nodes (inverters/buffers)
+    Additionally the following invariants are satisfied:
+    - there are no dangling nodes (the nodes without fanout)
+    - the level of each AND gate reflects the levels of this fanins
+    - the AND nodes are in the topological order
+    - the constant 1 node has always number 0 in the object list
+    The operations that are performed on AIGs:
+    - building new nodes (Aig_And)
+    - performing elementary Boolean operations (Aig_Or, Aig_Xor, etc)
+    - replacing one node by another (Abc_AigReplace)
+    - propagating constants (Abc_AigReplace)
+    - deleting dangling nodes (Abc_AigDelete)
+    When AIG is duplicated, the new graph is structurally hashed too.
+    If this repeated hashing leads to fewer nodes, it means the original
+    AIG was not strictly hashed (one of the conditions above is violated).
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+//typedef int                   bool;
+#ifndef bool
+#define bool int
+#endif
+
+typedef struct Aig_Param_t_     Aig_Param_t;
+typedef struct Aig_Man_t_       Aig_Man_t;
+typedef struct Aig_Node_t_      Aig_Node_t;
+typedef struct Aig_Edge_t_      Aig_Edge_t;
+typedef struct Aig_MemFixed_t_  Aig_MemFixed_t;
+typedef struct Aig_SimInfo_t_   Aig_SimInfo_t;
+typedef struct Aig_Table_t_     Aig_Table_t;
+
+// network types
+typedef enum { 
+    AIG_NONE = 0,  // 0: unknown
+    AIG_PI,        // 1: primary input
+    AIG_PO,        // 2: primary output
+    AIG_AND        // 3: internal node
+} Aig_NodeType_t;
+
+// the AIG parameters
+struct Aig_Param_t_
+{
+    int              nPatsRand;     // the number of random patterns
+    int              nBTLimit;      // backtrack limit at the intermediate nodes
+    int              nSeconds;      // the runtime limit at the final miter
+};
+
+// the AIG edge 
+struct Aig_Edge_t_ 
+{
+    unsigned         iNode   : 31;  // the node
+    unsigned         fComp   :  1;  // the complemented attribute
+};
+
+// the AIG node
+struct Aig_Node_t_  // 8 words
+{
+    // various numbers associated with the node
+    int              Id;            // the unique number (SAT var number) of this node 
+    int              nRefs;         // the reference counter
+    unsigned         Type    :  2;  // the node type
+    unsigned         fPhase  :  1;  // the phase of this node
+    unsigned         fMarkA  :  1;  // the mask
+    unsigned         fMarkB  :  1;  // the mask
+    unsigned         fMarkC  :  1;  // the mask
+    unsigned         TravId  : 26;  // the traversal ID
+    unsigned         Level   : 16;  // the direct level of the node
+    unsigned         LevelR  : 16;  // the reverse level of the node
+    Aig_Edge_t       Fans[2];       // the fanins
+    int              NextH;         // next node in the hash table          
+    int              Data;          // miscelleneous data
+    Aig_Man_t *      pMan;          // the parent manager
+};
+
+// the AIG manager
+struct Aig_Man_t_
+{
+    // the AIG parameters
+    Aig_Param_t      Param;         // the full set of AIG parameters
+    Aig_Param_t *    pParam;        // the pointer to the above set
+    // the nodes
+    Aig_Node_t *     pConst1;       // the constant 1 node (ID=0)
+    Vec_Ptr_t *      vNodes;        // all nodes by ID
+    Vec_Ptr_t *      vPis;          // all PIs
+    Vec_Ptr_t *      vPos;          // all POs
+    Aig_Table_t *    pTable;        // structural hash table
+    int              nLevelMax;     // the maximum level
+    // fanout representation
+    Vec_Ptr_t *      vFanPivots;    // fanout pivots
+    Vec_Ptr_t *      vFanFans0;     // the next fanout of the first fanin
+    Vec_Ptr_t *      vFanFans1;     // the next fanout of the second fanin 
+    // the memory managers
+    Aig_MemFixed_t * mmNodes;       // the memory manager for nodes
+    int              nTravIds;      // the traversal ID
+    // simulation info
+    Aig_SimInfo_t *  pInfo;         // random and systematic sim info for PIs
+    Aig_SimInfo_t *  pInfoTemp;     // temporary sim info for all nodes
+    // simulation patterns
+    int              nPiWords;      // the number of words in the PI info
+    int              nPatsMax;      // the max number of patterns 
+    Vec_Ptr_t *      vPats;         // simulation patterns to try
+    // equivalence classes
+    Vec_Vec_t *      vClasses;      // the non-trival equivalence classes of nodes
+    // temporary data
+    Vec_Ptr_t *      vFanouts;      // temporary storage for fanouts of a node
+    Vec_Ptr_t *      vToReplace;    // the nodes to replace
+};
+
+// the AIG simulation info
+struct Aig_SimInfo_t_  
+{
+    int              Type;          // the type (0 = PI, 1 = all)
+    int              nNodes;        // the number of nodes for which allocated
+    int              nWords;        // the number of words for each node
+    int              nPatsMax;      // the maximum number of patterns
+    int              nPatsCur;      // the current number of patterns
+    unsigned *       pData;         // the simulation data
+};
+
+// iterators over nodes, PIs, POs, ANDs
+#define Aig_ManForEachNode( pMan, pNode, i )                                                  \
+    for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ )
+#define Aig_ManForEachPi( pMan, pNode, i )                                                    \
+    for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
+#define Aig_ManForEachPo( pMan, pNode, i )                                                    \
+    for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
+#define Aig_ManForEachAnd( pNtk, pNode, i )                                                   \
+    for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ )   \
+        if ( Aig_NodeIsAnd(pNode) ) {} else
+
+// maximum/minimum operators
+#define AIG_MIN(a,b)  (((a) < (b))? (a) : (b))
+#define AIG_MAX(a,b)  (((a) > (b))? (a) : (b))
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 0);    }
+
+static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i);  }
+static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i )   { return Vec_PtrEntry(pMan->vPis, i);    }
+static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i )   { return Vec_PtrEntry(pMan->vPos, i);    }
+
+static inline int          Aig_ManNodeNum( Aig_Man_t * pMan )     { return Vec_PtrSize(pMan->vNodes);      }
+static inline int          Aig_ManPiNum( Aig_Man_t * pMan )       { return Vec_PtrSize(pMan->vPis);        }
+static inline int          Aig_ManPoNum( Aig_Man_t * pMan )       { return Vec_PtrSize(pMan->vPos);        }
+static inline int          Aig_ManAndNum( Aig_Man_t * pMan )      { return Aig_ManNodeNum(pMan)-Aig_ManPiNum(pMan)-Aig_ManPoNum(pMan)-1;  }
+
+static inline Aig_Node_t * Aig_Regular( Aig_Node_t * p )          { return (Aig_Node_t *)((unsigned)(p) & ~01);  }
+static inline Aig_Node_t * Aig_Not( Aig_Node_t * p )              { return (Aig_Node_t *)((unsigned)(p) ^  01);  }
+static inline Aig_Node_t * Aig_NotCond( Aig_Node_t * p, int c )   { return (Aig_Node_t *)((unsigned)(p) ^ (c));  }
+static inline bool         Aig_IsComplement( Aig_Node_t * p )     { return (bool)(((unsigned)p) & 01);           }
+
+static inline bool         Aig_NodeIsConst( Aig_Node_t * pNode )  { return Aig_Regular(pNode)->Id == 0;          }
+static inline bool         Aig_NodeIsPi( Aig_Node_t * pNode )     { return Aig_Regular(pNode)->Type == AIG_PI;   }
+static inline bool         Aig_NodeIsPo( Aig_Node_t * pNode )     { return Aig_Regular(pNode)->Type == AIG_PO;   }
+static inline bool         Aig_NodeIsAnd( Aig_Node_t * pNode )    { return Aig_Regular(pNode)->Type == AIG_AND;  }
+
+static inline int          Aig_NodeId( Aig_Node_t * pNode )       { assert( !Aig_IsComplement(pNode) ); return pNode->Id;                      }
+static inline int          Aig_NodeRefs( Aig_Node_t * pNode )     { assert( !Aig_IsComplement(pNode) ); return pNode->nRefs;                   }
+static inline bool         Aig_NodePhase( Aig_Node_t * pNode )    { assert( !Aig_IsComplement(pNode) ); return pNode->fPhase;                  }
+static inline int          Aig_NodeLevel( Aig_Node_t * pNode )    { assert( !Aig_IsComplement(pNode) ); return pNode->Level;                   }
+static inline int          Aig_NodeLevelR( Aig_Node_t * pNode )   { assert( !Aig_IsComplement(pNode) ); return pNode->LevelR;                  }
+static inline int          Aig_NodeData( Aig_Node_t * pNode )     { assert( !Aig_IsComplement(pNode) ); return pNode->Data;                    }
+static inline Aig_Man_t *  Aig_NodeMan( Aig_Node_t * pNode )      { assert( !Aig_IsComplement(pNode) ); return pNode->pMan;                    }
+static inline int          Aig_NodeFaninId0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].iNode;           }
+static inline int          Aig_NodeFaninId1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].iNode;           }
+static inline bool         Aig_NodeFaninC0( Aig_Node_t * pNode )  { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].fComp;           }
+static inline bool         Aig_NodeFaninC1( Aig_Node_t * pNode )  { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].fComp;           }
+static inline Aig_Node_t * Aig_NodeFanin0( Aig_Node_t * pNode )   { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId0(pNode) );   }
+static inline Aig_Node_t * Aig_NodeFanin1( Aig_Node_t * pNode )   { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId1(pNode) );   }
+static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode )   { return Aig_NotCond( Aig_NodeFanin0(pNode), Aig_NodeFaninC0(pNode) ); }
+static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode )   { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); }
+static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode )    { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL;  }
+static inline int          Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin )    { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; }
+static inline int          Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+
+static inline unsigned *   Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode )  { assert(  p->Type ); return p->pData + p->nWords * pNode->Id; }
+static inline unsigned *   Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num )               { assert( !p->Type ); return p->pData + p->nWords * Num;       }
+
+static inline void         Aig_NodeSetTravId( Aig_Node_t * pNode, int TravId ) { pNode->TravId = TravId;                                    }
+static inline void         Aig_NodeSetTravIdCurrent( Aig_Node_t * pNode )      { pNode->TravId = pNode->pMan->nTravIds;                     }
+static inline void         Aig_NodeSetTravIdPrevious( Aig_Node_t * pNode )     { pNode->TravId = pNode->pMan->nTravIds - 1;                 }
+static inline bool         Aig_NodeIsTravIdCurrent( Aig_Node_t * pNode )       { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds);     }
+static inline bool         Aig_NodeIsTravIdPrevious( Aig_Node_t * pNode )      { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds - 1); }
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== aigCheck.c ==========================================================*/
+extern bool                Aig_ManCheck( Aig_Man_t * pMan );
+extern bool                Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot );
+/*=== aigFanout.c ==========================================================*/
+extern void                Aig_ManCreateFanouts( Aig_Man_t * p );
+extern void                Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout );
+extern void                Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove );
+extern int                 Aig_NodeGetFanoutNum( Aig_Node_t * pNode );
+extern Vec_Ptr_t *         Aig_NodeGetFanouts( Aig_Node_t * pNode );
+extern int                 Aig_NodeGetLevelRNew( Aig_Node_t * pNode );
+extern int                 Aig_ManSetLevelR( Aig_Man_t * pMan );
+extern int                 Aig_ManGetLevelMax( Aig_Man_t * pMan );
+extern int                 Aig_NodeUpdateLevel_int( Aig_Node_t * pNode );
+extern int                 Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode );
+/*=== aigMem.c =============================================================*/
+extern Aig_MemFixed_t *    Aig_MemFixedStart( int nEntrySize );
+extern void                Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose );
+extern char *              Aig_MemFixedEntryFetch( Aig_MemFixed_t * p );
+extern void                Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry );
+extern void                Aig_MemFixedRestart( Aig_MemFixed_t * p );
+extern int                 Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p );
+/*=== aigMan.c =============================================================*/
+extern void                Aig_ManSetDefaultParams( Aig_Param_t * pParam );
+extern Aig_Man_t *         Aig_ManStart( Aig_Param_t * pParam );
+extern int                 Aig_ManCleanup( Aig_Man_t * pMan );
+extern void                Aig_ManStop( Aig_Man_t * p );
+/*=== aigNode.c =============================================================*/
+extern Aig_Node_t *        Aig_NodeCreateConst( Aig_Man_t * p );
+extern Aig_Node_t *        Aig_NodeCreatePi( Aig_Man_t * p );
+extern Aig_Node_t *        Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin );
+extern Aig_Node_t *        Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
+extern void                Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode );
+extern void                Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
+extern void                Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
+extern void                Aig_NodePrint( Aig_Node_t * pNode );
+extern char *              Aig_NodeName( Aig_Node_t * pNode );
+/*=== aigOper.c ==========================================================*/
+extern Aig_Node_t *        Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 );
+extern Aig_Node_t *        Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs );
+/*=== aigReplace.c ==========================================================*/
+extern void                Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel );
+/*=== aigTable.c ==========================================================*/
+extern Aig_Table_t *       Aig_TableCreate( int nSize );
+extern void                Aig_TableFree( Aig_Table_t * p );
+extern int                 Aig_TableNumNodes( Aig_Table_t * p );
+extern Aig_Node_t *        Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd );
+extern void                Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis );
+extern void                Aig_TableResize( Aig_Man_t * pMan );
+extern void                Aig_TableRehash( Aig_Man_t * pMan );
+/*=== aigUtil.c ==========================================================*/
+extern void                Aig_ManIncrementTravId( Aig_Man_t * pMan );
+extern void                Aig_PrintNode( Aig_Node_t * pNode );
+
+
+/*=== fraigClasses.c ==========================================================*/
+extern Vec_Vec_t *         Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
+/*=== fraigSim.c ==========================================================*/
+extern Aig_SimInfo_t *     Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
+extern void                Aig_SimInfoClean( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoRandom( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoResize( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoFree( Aig_SimInfo_t * p );
+extern Aig_SimInfo_t *     Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/sat/aig/aigBalance.c b/src/sat/aig/aigBalance.c
new file mode 100644
index 00000000..1dd8ab01
--- /dev/null
+++ b/src/sat/aig/aigBalance.c
@@ -0,0 +1,47 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigCheck.c b/src/sat/aig/aigCheck.c
new file mode 100644
index 00000000..a9facef3
--- /dev/null
+++ b/src/sat/aig/aigCheck.c
@@ -0,0 +1,146 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigFanout.c b/src/sat/aig/aigFanout.c
new file mode 100644
index 00000000..aed38426
--- /dev/null
+++ b/src/sat/aig/aigFanout.c
@@ -0,0 +1,423 @@
+/**CFile****************************************************************
+
+  FileName    [aigFanout.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: aigFanout.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Node_t *  Aig_NodeFanPivot( Aig_Node_t * pNode )                { return Vec_PtrEntry(pNode->pMan->vFanPivots, pNode->Id); }
+static inline Aig_Node_t *  Aig_NodeFanFan0( Aig_Node_t * pNode )                 { return Vec_PtrEntry(pNode->pMan->vFanFans0, pNode->Id);  }
+static inline Aig_Node_t *  Aig_NodeFanFan1( Aig_Node_t * pNode )                 { return Vec_PtrEntry(pNode->pMan->vFanFans1, pNode->Id);  }
+static inline Aig_Node_t ** Aig_NodeFanPivotPlace( Aig_Node_t * pNode )           { return ((Aig_Node_t **)pNode->pMan->vFanPivots->pArray) + pNode->Id; }
+static inline Aig_Node_t ** Aig_NodeFanFan0Place( Aig_Node_t * pNode )            { return ((Aig_Node_t **)pNode->pMan->vFanFans0->pArray) + pNode->Id;  }
+static inline Aig_Node_t ** Aig_NodeFanFan1Place( Aig_Node_t * pNode )            { return ((Aig_Node_t **)pNode->pMan->vFanFans1->pArray) + pNode->Id;  }
+static inline void Aig_NodeSetFanPivot( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanPivots, pNode->Id, pNode2); }
+static inline void Aig_NodeSetFanFan0( Aig_Node_t * pNode, Aig_Node_t * pNode2 )  { Vec_PtrWriteEntry(pNode->pMan->vFanFans0, pNode->Id, pNode2);  }
+static inline void Aig_NodeSetFanFan1( Aig_Node_t * pNode, Aig_Node_t * pNode2 )  { Vec_PtrWriteEntry(pNode->pMan->vFanFans1, pNode->Id, pNode2);  }
+static inline Aig_Node_t * Aig_NodeNextFanout( Aig_Node_t * pNode, Aig_Node_t * pFanout )       { if ( pFanout == NULL ) return NULL; return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0(pFanout) : Aig_NodeFanFan1(pFanout); }
+static inline Aig_Node_t ** Aig_NodeNextFanoutPlace( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0Place(pFanout) : Aig_NodeFanFan1Place(pFanout); }
+
+// iterator through the fanouts of the node
+#define Aig_NodeForEachFanout( pNode, pFanout )                           \
+    for ( pFanout = Aig_NodeFanPivot(pNode); pFanout;                     \
+          pFanout = Aig_NodeNextFanout(pNode, pFanout) )
+// safe iterator through the fanouts of the node
+#define Aig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 )             \
+    for ( pFanout  = Aig_NodeFanPivot(pNode),                             \
+          pFanout2 = Aig_NodeNextFanout(pNode, pFanout);              \
+          pFanout;                                                        \
+          pFanout  = pFanout2,                                            \
+          pFanout2 = Aig_NodeNextFanout(pNode, pFanout) )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the fanouts for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCreateFanouts( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    int i;
+    assert( p->vFanPivots == NULL );
+    p->vFanPivots = Vec_PtrStart( Aig_ManNodeNum(p) );
+    p->vFanFans0  = Vec_PtrStart( Aig_ManNodeNum(p) );
+    p->vFanFans1  = Vec_PtrStart( Aig_ManNodeNum(p) );
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        if ( Aig_NodeIsPi(pNode) || i == 0 )
+            continue;
+        Aig_NodeAddFaninFanout( Aig_NodeFanin0(pNode), pNode );
+        if ( Aig_NodeIsPo(pNode) )
+            continue;
+        Aig_NodeAddFaninFanout( Aig_NodeFanin1(pNode), pNode );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the fanouts for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ManResizeFanouts( Aig_Man_t * p, int nSizeNew )
+{
+    assert( p->vFanPivots );
+    if ( Vec_PtrSize(p->vFanPivots) < nSizeNew )
+    {
+        Vec_PtrFillExtra( p->vFanPivots, nSizeNew + 1000, NULL );
+        Vec_PtrFillExtra( p->vFanFans0,  nSizeNew + 1000, NULL );
+        Vec_PtrFillExtra( p->vFanFans1,  nSizeNew + 1000, NULL );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the fanout to the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout )
+{
+    Aig_Node_t * pPivot;
+
+    // check that they are not complemented
+    assert( !Aig_IsComplement(pFanin) );
+    assert( !Aig_IsComplement(pFanout) );
+    // check that pFanins is a fanin of pFanout
+    assert( Aig_NodeFaninId0(pFanout) == pFanin->Id || Aig_NodeFaninId1(pFanout) == pFanin->Id );
+
+    // resize the fanout manager
+    Aig_ManResizeFanouts( pFanin->pMan, 1 + AIG_MAX(pFanin->Id, pFanout->Id) );
+
+    // consider the case of the first fanout
+    pPivot = Aig_NodeFanPivot(pFanin);
+    if ( pPivot == NULL )
+    {
+        Aig_NodeSetFanPivot( pFanin, pFanout );
+        return;
+    }
+
+    // consider the case of more than one fanouts
+    if ( Aig_NodeFaninId0(pPivot) == pFanin->Id )
+    {
+        if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan0(pPivot) );
+            Aig_NodeSetFanFan0( pPivot, pFanout );
+        }
+        else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan0(pPivot) );
+            Aig_NodeSetFanFan0( pPivot, pFanout );
+        }
+    }
+    else // if ( Aig_NodeFaninId1(pPivot) == pFanin->Id )
+    {
+        assert( Aig_NodeFaninId1(pPivot) == pFanin->Id );
+        if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan1(pPivot) );
+            Aig_NodeSetFanFan1( pPivot, pFanout );
+        }
+        else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan1(pPivot) );
+            Aig_NodeSetFanFan1( pPivot, pFanout );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the fanout to the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove )
+{
+    Aig_Node_t * pFanout, * pFanout2, ** ppFanList;
+    // start the linked list of fanouts
+    ppFanList = Aig_NodeFanPivotPlace(pFanin); 
+    // go through the fanouts
+    Aig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 )
+    {
+        // skip the fanout-to-remove
+        if ( pFanout == pFanoutToRemove )
+            continue;
+        // add useful fanouts to the list
+        *ppFanList = pFanout;
+        ppFanList = Aig_NodeNextFanoutPlace( pFanin, pFanout );
+    }
+    *ppFanList = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of fanouts of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeGetFanoutNum( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int Counter = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    Vec_PtrClear( pNode->pMan->vFanouts );
+    Aig_NodeForEachFanout( pNode, pFanout )
+        Vec_PtrPush( pNode->pMan->vFanouts, pFanout );
+    return pNode->pMan->vFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node has at least one complemented fanout.]
+
+  Description [A fanout is complemented if the fanout's fanin edge pointing
+  to the given node is complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_NodeHasComplFanoutEdge( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int iFanin;
+    Aig_NodeForEachFanout( pNode, pFanout )
+    {
+        iFanin = Aig_NodeWhatFanin( pFanout, pNode );
+        assert( iFanin >= 0 );
+        if ( iFanin && Aig_NodeFaninC1(pFanout) || !iFanin && Aig_NodeFaninC0(pFanout) )
+            return 1;
+    }
+    return 0;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes and assigns the reverse level of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Aig_NodeSetLevelR_rec( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int LevelR = 0;
+    if ( Aig_NodeIsPo(pNode) )
+        return pNode->LevelR = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        if ( LevelR < Aig_NodeSetLevelR_rec(pFanout) )
+            LevelR = pFanout->LevelR;
+    return pNode->LevelR = 1 + LevelR;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reverse level of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSetLevelR( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pNode;
+    int i, LevelR = 0;
+    Aig_ManForEachPi( pMan, pNode, i )
+        if ( LevelR < Aig_NodeSetLevelR_rec(pNode) )
+            LevelR = pNode->LevelR;
+    return LevelR;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the global number of logic levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManGetLevelMax( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pNode;
+    int i, LevelsMax = 0;
+    Aig_ManForEachPo( pMan, pNode, i )
+        if ( LevelsMax < (int)pNode->Level )
+            LevelsMax = (int)pNode->Level;
+    return LevelsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes but does not assign the reverse level of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeGetLevelRNew( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    unsigned LevelR = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        LevelR = AIG_MAX( LevelR, pFanout->LevelR );
+    return LevelR + !Aig_NodeIsPi(pNode);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the direct level of one node.]
+
+  Description [Returns 1 if direct level of at least one CO was changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    unsigned LevelNew, fStatus = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+    {
+        LevelNew = Aig_NodeGetLevelNew( pFanout );
+        if ( pFanout->Level == LevelNew )
+            continue;
+        // the level has changed
+        pFanout->Level = LevelNew;
+        if ( Aig_NodeIsPo(pNode) )
+            fStatus = 1;
+        else
+            fStatus |= Aig_NodeUpdateLevel_int( pFanout );
+    }
+    return fStatus;    
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the reverse level of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanin;
+    unsigned LevelNew;
+    assert( !Aig_NodeIsPo(pNode) );
+    pFanin = Aig_NodeFanin0(pNode);
+    LevelNew = Aig_NodeGetLevelRNew(pFanin);
+    if ( pFanin->LevelR != LevelNew )
+    {
+        pFanin->LevelR = LevelNew;
+        if ( Aig_NodeIsAnd(pFanin) )
+            Aig_NodeUpdateLevelR_int( pFanin );
+    }
+    pFanin = Aig_NodeFanin1(pNode);
+    LevelNew = Aig_NodeGetLevelRNew(pFanin);
+    if ( pFanin->LevelR != LevelNew )
+    {
+        pFanin->LevelR = LevelNew;
+        if ( Aig_NodeIsAnd(pFanin) )
+            Aig_NodeUpdateLevelR_int( pFanin );
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
new file mode 100644
index 00000000..2058f6b0
--- /dev/null
+++ b/src/sat/aig/aigMan.c
@@ -0,0 +1,142 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
new file mode 100644
index 00000000..280cf98b
--- /dev/null
+++ b/src/sat/aig/aigMem.c
@@ -0,0 +1,246 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
new file mode 100644
index 00000000..afccd985
--- /dev/null
+++ b/src/sat/aig/aigNode.c
@@ -0,0 +1,292 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigOper.c b/src/sat/aig/aigOper.c
new file mode 100644
index 00000000..a10cc7ff
--- /dev/null
+++ b/src/sat/aig/aigOper.c
@@ -0,0 +1,175 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigReplace.c b/src/sat/aig/aigReplace.c
new file mode 100644
index 00000000..d928fdf8
--- /dev/null
+++ b/src/sat/aig/aigReplace.c
@@ -0,0 +1,133 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
new file mode 100644
index 00000000..cfc94f6b
--- /dev/null
+++ b/src/sat/aig/aigTable.c
@@ -0,0 +1,335 @@
+/**CFile****************************************************************
+
+  FileName    [aigTable.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: aigTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the hash table 
+struct Aig_Table_t_
+{
+    Aig_Node_t **    pBins;         // the table bins
+    int              nBins;         // the size of the table
+    int              nEntries;      // the total number of entries in the table
+};
+
+// iterators through the entries in the linked lists of nodes
+#define Aig_TableBinForEachEntry( pBin, pEnt )                 \
+    for ( pEnt = pBin;                                         \
+          pEnt;                                                \
+          pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
+#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 )      \
+    for ( pEnt = pBin,                                         \
+          pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL;            \
+          pEnt;                                                \
+          pEnt = pEnt2,                                        \
+          pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL )
+
+// hash key for the structural hash table
+static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
+//static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
+
+static unsigned int Cudd_PrimeAig( unsigned int  p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Table_t * Aig_TableCreate( int nSize )
+{
+    Aig_Table_t * p;
+    // allocate the table
+    p = ALLOC( Aig_Table_t, 1 );
+    memset( p, 0, sizeof(Aig_Table_t) );
+    // allocate and clean the bins
+    p->nBins = Cudd_PrimeAig(nSize);
+    p->pBins = ALLOC( Aig_Node_t *, p->nBins );
+    memset( p->pBins, 0, sizeof(Aig_Node_t *) * p->nBins );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the supergate hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableFree( Aig_Table_t * p )
+{
+    FREE( p->pBins );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of nodes in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TableNumNodes( Aig_Table_t * p )
+{
+    return p->nEntries;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    Aig_Node_t * pAnd;
+    unsigned Key;
+    assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
+    assert( p0->pMan == p1->pMan );
+    // get the hash key for these two nodes
+    Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+    // find the matching node in the table
+    Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
+        if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) )
+             return pAnd;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd )
+{
+    unsigned Key;
+    assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
+    // check if it is a good time for table resizing
+    if ( pMan->pTable->nEntries > 2 * pMan->pTable->nBins )
+        Aig_TableResize( pMan );
+    // add the node to the corresponding linked list in the table
+    Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+    pAnd->NextH = pMan->pTable->pBins[Key]->Id;
+    pMan->pTable->pBins[Key]->NextH = pAnd->Id;
+    pMan->pTable->nEntries++;
+    return pAnd;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes an AIG node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
+{
+    Aig_Node_t * pAnd, * pPlace = NULL;
+    unsigned Key;
+    assert( !Aig_IsComplement(pThis) );
+    assert( Aig_NodeIsAnd(pThis) );
+    assert( pMan == pThis->pMan );
+    // get the hash key for these two nodes
+    Key = Abc_HashKey2( Aig_NodeChild0(pThis), Aig_NodeChild1(pThis), pMan->pTable->nBins );
+    // find the matching node in the table
+    Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
+    {
+        if ( pThis != pAnd )
+        {
+            pPlace = pAnd;
+            continue;
+        }
+        if ( pPlace == NULL )
+            pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
+        else
+            pPlace->NextH = pThis->Id;
+        break;
+    }
+    assert( pThis == pAnd );
+    pMan->pTable->nEntries--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableResize( Aig_Man_t * pMan )
+{
+    Aig_Node_t ** pBinsNew;
+    Aig_Node_t * pEnt, * pEnt2;
+    int nBinsNew, Counter, i, clk;
+    unsigned Key;
+
+clk = clock();
+    // get the new table size
+    nBinsNew = Cudd_PrimeCopy( 3 * pMan->pTable->nBins ); 
+    // allocate a new array
+    pBinsNew = ALLOC( Aig_Node_t *, nBinsNew );
+    memset( pBinsNew, 0, sizeof(Aig_Node_t *) * nBinsNew );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->pTable->nBins; i++ )
+        Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
+        {
+            Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
+            pEnt->NextH = pBinsNew[Key]->Id;
+            pBinsNew[Key]->NextH = pEnt->Id;
+            Counter++;
+        }
+    assert( Counter == pMan->pTable->nEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pMan->pTable->pBins );
+    pMan->pTable->pBins = pBinsNew;
+    pMan->pTable->nBins = nBinsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableRehash( Aig_Man_t * pMan )
+{
+    Aig_Node_t ** pBinsNew;
+    Aig_Node_t * pEnt, * pEnt2;
+    unsigned Key;
+    int Counter, Temp, i;
+    // allocate a new array
+    pBinsNew = ALLOC( Aig_Node_t *, pMan->pTable->nBins );
+    memset( pBinsNew, 0, sizeof(Aig_Node_t *) * pMan->pTable->nBins );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->pTable->nBins; i++ )
+        Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
+        {
+            // swap the fanins if needed
+            if ( pEnt->Fans[0].iNode > pEnt->Fans[1].iNode )
+            {
+                Temp = pEnt->Fans[0].iNode;
+                pEnt->Fans[0].iNode = pEnt->Fans[1].iNode;
+                pEnt->Fans[1].iNode = Temp;
+                Temp = pEnt->Fans[0].fComp;
+                pEnt->Fans[0].fComp = pEnt->Fans[1].fComp;
+                pEnt->Fans[1].fComp = Temp;
+           }
+            // rehash the node
+            Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
+            pEnt->NextH = pBinsNew[Key]->Id;
+            pBinsNew[Key]->NextH = pEnt->Id;
+            Counter++;
+        }
+    assert( Counter == pMan->pTable->nEntries );
+    // replace the table and the parameters
+    free( pMan->pTable->pBins );
+    pMan->pTable->pBins = pBinsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the smallest prime larger than the number.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned int Cudd_PrimeAig( unsigned int p )
+{
+    int i,pn;
+
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c
new file mode 100644
index 00000000..a1c9ca44
--- /dev/null
+++ b/src/sat/aig/aigUtil.c
@@ -0,0 +1,60 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
new file mode 100644
index 00000000..b3040e2a
--- /dev/null
+++ b/src/sat/aig/fraigClass.c
@@ -0,0 +1,108 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
new file mode 100644
index 00000000..6187538b
--- /dev/null
+++ b/src/sat/aig/fraigCore.c
@@ -0,0 +1,47 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
new file mode 100644
index 00000000..b5cce582
--- /dev/null
+++ b/src/sat/aig/fraigProve.c
@@ -0,0 +1,47 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
new file mode 100644
index 00000000..1d547621
--- /dev/null
+++ b/src/sat/aig/fraigSim.c
@@ -0,0 +1,238 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 74503a2b..eb1c5374 100644
--- a/src/sat/csat/csat_apis.c
+++ b/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" );
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 13f6b50b..a9e09f61 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/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 )
     {