Version abc60822

22 files changed, 0 insertions, 4952 deletions

diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
deleted file mode 100644
index a0d63ce9..00000000
--- a/src/sat/aig/aig.h
+++ /dev/null
@@ -1,377 +0,0 @@
-/**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__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-/*
-    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 "solver.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-//typedef int                   bool;
-#ifndef __cplusplus
-#ifndef bool
-#define bool int
-#endif
-#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;
-typedef struct Aig_Pattern_t_   Aig_Pattern_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;
-
-// proof outcomes
-typedef enum { 
-    AIG_PROOF_NONE = 0,  // 0: unknown
-    AIG_PROOF_SAT,       // 1: primary input
-    AIG_PROOF_UNSAT,     // 2: primary output
-    AIG_PROOF_TIMEOUT,   // 3: primary output
-    AIG_PROOF_FAIL       // 4: internal node
-} Aig_ProofType_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
-    int              fVerbose;      // verbosity
-    int              fSatVerbose;   // verbosity of SAT
-};
-
-// 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
-    // SAT solver and related structures
-    solver *         pSat;
-    Vec_Int_t *      vVar2Sat;      // mapping of nodes into their SAT var numbers (for each node num)
-    Vec_Int_t *      vSat2Var;      // mapping of the SAT var numbers into nodes (for each SAT var)
-    Vec_Int_t *      vPiSatNums;    // the SAT variable numbers (for each PI)
-    int *            pModel;        // the satisfying assignment (for each PI)
-    int              nMuxes;        // the number of MUXes
-    // 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 *  pInfoPi;       // temporary sim info for the PI nodes
-    Aig_SimInfo_t *  pInfoTemp;     // temporary sim info for all nodes
-    Aig_Pattern_t *  pPatMask;      // the mask which shows what patterns are used
-    // 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
-    Vec_Int_t *      vClassTemp;    // temporary class representatives
-};
-
-// the simulation patter
-struct Aig_Pattern_t_  
-{
-    int              nBits;
-    int              nWords;
-    unsigned *       pData;
-};
-
-// 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( pMan, 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>>5) + ((nBits&31) > 0);     }
-static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
-static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));             }
-static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));             }
-
-static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan )      { return pMan->pConst1;                  }
-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 int          Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
-
-static inline unsigned *   Aig_SimInfoForNodeId( Aig_SimInfo_t * p, int NodeId )        { assert(  p->Type ); return p->pData + p->nWords * NodeId;    }
-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 );
-extern Aig_Node_t *        Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
-extern Aig_Node_t *        Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin );
-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 );
-extern void                Aig_PrintNode( 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 bool                Aig_NodeIsMuxType( Aig_Node_t * pNode );
-extern Aig_Node_t *        Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE );
-
-
-/*=== fraigCore.c ==========================================================*/
-extern Aig_ProofType_t     Aig_FraigProve( Aig_Man_t * pMan );
-/*=== fraigClasses.c ==========================================================*/
-extern Vec_Vec_t *         Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
-extern int                 Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask );
-extern void                Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats );
-/*=== fraigCnf.c ==========================================================*/
-extern Aig_ProofType_t     Aig_ClauseSolverStart( Aig_Man_t * pMan );
-/*=== fraigEngine.c ==========================================================*/
-extern void                Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
-extern void                Aig_EngineSimulateFirst( Aig_Man_t * p );
-extern int                 Aig_EngineSimulate( Aig_Man_t * p );
-/*=== fraigSim.c ==========================================================*/
-extern Aig_SimInfo_t *     Aig_SimInfoAlloc( int nNodes, int nBits, int Type );
-extern void                Aig_SimInfoClean( Aig_SimInfo_t * p );
-extern void                Aig_SimInfoRandom( Aig_SimInfo_t * p );
-extern void                Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat );
-extern void                Aig_SimInfoResize( Aig_SimInfo_t * p );
-extern void                Aig_SimInfoFree( Aig_SimInfo_t * p );
-extern void                Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll );
-extern Aig_Pattern_t *     Aig_PatternAlloc( int nBits );
-extern void                Aig_PatternClean( Aig_Pattern_t * pPat );
-extern void                Aig_PatternFill( Aig_Pattern_t * pPat );
-extern int                 Aig_PatternCount( Aig_Pattern_t * pPat );
-extern void                Aig_PatternRandom( Aig_Pattern_t * pPat );
-extern void                Aig_PatternFree( Aig_Pattern_t * pPat );
- 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/aig/aigBalance.c b/src/sat/aig/aigBalance.c
deleted file mode 100644
index 1dd8ab01..00000000
--- a/src/sat/aig/aigBalance.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**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
deleted file mode 100644
index a9facef3..00000000
--- a/src/sat/aig/aigCheck.c
+++ /dev/null
@@ -1,146 +0,0 @@
-/**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
deleted file mode 100644
index aed38426..00000000
--- a/src/sat/aig/aigFanout.c
+++ /dev/null
@@ -1,423 +0,0 @@
-/**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
deleted file mode 100644
index 4c64c897..00000000
--- a/src/sat/aig/aigMan.c
+++ /dev/null
@@ -1,157 +0,0 @@
-/**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 = 4096;  // 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;
-    p->nPatsMax   = 25;
-    // 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 ); 
-    p->vClassTemp = Vec_IntAlloc( 10 );
-    p->vPats      = Vec_PtrAlloc( p->nPatsMax );
-    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 )
-{
-    // SAT solver
-    if ( p->pSat )       solver_delete( p->pSat );
-    if ( p->vVar2Sat )   Vec_IntFree( p->vVar2Sat );
-    if ( p->vSat2Var )   Vec_IntFree( p->vSat2Var );
-    if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums );
-    // fanouts
-    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 );
-    // patterns
-    if ( p->vPats )      Vec_PtrFree( p->vPats );
-    if ( p->pPatMask )   Aig_PatternFree( p->pPatMask );
-    // nodes
-    Aig_MemFixedStop( p->mmNodes, 0 );
-    Vec_PtrFree( p->vNodes );
-    Vec_PtrFree( p->vPis );
-    Vec_PtrFree( p->vPos );
-    // temporary
-    Vec_PtrFree( p->vFanouts );
-    Vec_PtrFree( p->vToReplace );
-    Vec_IntFree( p->vClassTemp );
-    Aig_TableFree( p->pTable );
-    free( p );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
deleted file mode 100644
index 32709bf6..00000000
--- a/src/sat/aig/aigMem.c
+++ /dev/null
@@ -1,246 +0,0 @@
-/**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;
-
-    // deallocate 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
deleted file mode 100644
index ce458353..00000000
--- a/src/sat/aig/aigNode.c
+++ /dev/null
@@ -1,316 +0,0 @@
-/**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->pMan = p;
-    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->Type   = AIG_NONE;
-    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->Type   = AIG_PI;
-    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 * pNode;
-    pNode = Aig_NodeCreate( p );
-    pNode->Type = AIG_PO;
-    Vec_PtrPush( p->vPos, pNode );
-    return pNode;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a primary output node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin )
-{
-    assert( Aig_NodeIsPo(pNode) );
-    assert( !Aig_IsComplement(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 );
-    pNode->Type = AIG_AND;
-    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) );
-    // remember 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 );
-    memset( pRoot, 0, sizeof(Aig_Node_t) ); // this is a temporary hack to skip dead children below!!!
-    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
deleted file mode 100644
index a10cc7ff..00000000
--- a/src/sat/aig/aigOper.c
+++ /dev/null
@@ -1,175 +0,0 @@
-/**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
deleted file mode 100644
index d928fdf8..00000000
--- a/src/sat/aig/aigReplace.c
+++ /dev/null
@@ -1,133 +0,0 @@
-/**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
deleted file mode 100644
index e6fe87d6..00000000
--- a/src/sat/aig/aigTable.c
+++ /dev/null
@@ -1,334 +0,0 @@
-/**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 = Aig_NodeNextH(pEnt) )
-#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 );
-    // 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]? pMan->pTable->pBins[Key]->Id : 0;
-    pMan->pTable->pBins[Key] = pAnd;
-    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->NextH;
-        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]? pBinsNew[Key]->Id : 0;
-            pBinsNew[Key] = pEnt;
-            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]? pBinsNew[Key]->Id : 0;
-            pBinsNew[Key] = pEnt;
-            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
deleted file mode 100644
index 40f7aba1..00000000
--- a/src/sat/aig/aigUtil.c
+++ /dev/null
@@ -1,190 +0,0 @@
-/**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++;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Aig_NodeIsMuxType( Aig_Node_t * pNode )
-{
-    Aig_Node_t * pNode0, * pNode1;
-    // check that the node is regular
-    assert( !Aig_IsComplement(pNode) );
-    // if the node is not AND, this is not MUX
-    if ( !Aig_NodeIsAnd(pNode) )
-        return 0;
-    // if the children are not complemented, this is not MUX
-    if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) )
-        return 0;
-    // get children
-    pNode0 = Aig_NodeFanin0(pNode);
-    pNode1 = Aig_NodeFanin1(pNode);
-    // if the children are not ANDs, this is not MUX
-    if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) )
-        return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
-    return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) || 
-           (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) ||
-           (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
-           (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
-
-  Description [If the node is a MUX, returns the control variable C.
-  Assigns nodes T and E to be the then and else variables of the MUX. 
-  Node C is never complemented. Nodes T and E can be complemented.
-  This function also recognizes EXOR/NEXOR gates as MUXes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE )
-{
-    Aig_Node_t * pNode0, * pNode1;
-    assert( !Aig_IsComplement(pNode) );
-    assert( Aig_NodeIsMuxType(pNode) );
-    // get children
-    pNode0 = Aig_NodeFanin0(pNode);
-    pNode1 = Aig_NodeFanin1(pNode);
-    // find the control variable
-//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
-    if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Aig_NodeFaninC0(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
-            return Aig_NodeChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
-            return Aig_NodeChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
-    else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Aig_NodeFaninC0(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
-            return Aig_NodeChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
-            return Aig_NodeChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
-    else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Aig_NodeFaninC1(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
-            return Aig_NodeChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
-            return Aig_NodeChild1(pNode0);//pNode1->p2;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
-    else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Aig_NodeFaninC1(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
-            return Aig_NodeChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
-            return Aig_NodeChild1(pNode0);//pNode1->p2;
-        }
-    }
-    assert( 0 ); // this is not MUX
-    return NULL;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
deleted file mode 100644
index a8df9a72..00000000
--- a/src/sat/aig/fraigClass.c
+++ /dev/null
@@ -1,320 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigClass.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: fraigClass.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, bool fPhase );
-
-////////////////////////////////////////////////////////////////////////
-///                     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, Entry, ClassNum;
-    assert( pInfo->Type == 1 );
-    // fill in the hash table
-    tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
-    vClasses = Vec_VecAlloc( 100 );
-    // enumerate the nodes considered in the equivalence classes
-//    Aig_ManForEachNode( p, pNode, i )
-    Vec_IntForEachEntry( p->vSat2Var, Entry, i )
-    {
-        pNode = Aig_ManNode( p, Entry );
-
-        if ( Aig_NodeIsPo(pNode) )
-            continue;
-        uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase );
-        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 );
-/*
-    // print the classes
-    {
-        Vec_Ptr_t * vVec;
-        printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n", 
-            Aig_ManPiNum(p), Aig_ManPoNum(p), 
-            Aig_ManNodeNum(p) - Aig_ManPoNum(p), 
-            Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) );
-
-        Vec_VecForEachLevel( vClasses, vVec, i )
-            printf( "%d ", Vec_PtrSize(vVec) );
-        printf( "\n" );
-    }
-*/
-    printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) );
-    return vClasses;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the hash key of the simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
-{
-    static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
-    unsigned uKey;
-    int i;
-    uKey = 0;
-    if ( fPhase )
-        for ( i = 0; i < nWords; i++ )
-            uKey ^= i * Primes[i%10] * pData[i];
-    else
-        for ( i = 0; i < nWords; i++ )
-            uKey ^= i * Primes[i%10] * ~pData[i];
-    return uKey;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Splits the equivalence class.]
-
-  Description [Given an equivalence class (vClass) and the simulation info, 
-  split the class into two based on the info.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManSplitClass( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Int_t * vClass, Vec_Int_t * vClass2, Aig_Pattern_t * pPat )
-{
-    int NodeId, i, k, w;
-    Aig_Node_t * pRoot, * pTemp;
-    unsigned * pRootData, * pTempData;
-    assert( Vec_IntSize(vClass) > 1 );
-    assert( pInfo->nPatsCur == pPat->nBits );
-//    printf( "Class = %5d.  -->  ", Vec_IntSize(vClass) ); 
-    // clear storage for the new classes
-    Vec_IntClear( vClass2 );
-    // get the root member of the class
-    pRoot = Aig_ManNode( p, Vec_IntEntry(vClass, 0) );
-    pRootData = Aig_SimInfoForNode( pInfo, pRoot );
-    // sort the class members:
-    // (1) with the same siminfo as pRoot remain in vClass
-    // (2) nodes with other siminfo go to vClass2
-    k = 1;
-    Vec_IntForEachEntryStart( vClass, NodeId, i, 1 )
-    {
-        NodeId = Vec_IntEntry(vClass, i);
-        pTemp  = Aig_ManNode( p, NodeId );
-        pTempData = Aig_SimInfoForNode( pInfo, pTemp );
-        if ( pRoot->fPhase == pTemp->fPhase )
-        {
-            for ( w = 0; w < pInfo->nWords; w++ )
-                if ( pRootData[w] != pTempData[w] )
-                    break;
-            if ( w == pInfo->nWords ) // the same info
-                Vec_IntWriteEntry( vClass, k++, NodeId );
-            else
-            {
-                Vec_IntPush( vClass2, NodeId );
-                // record the diffs if they are not distinguished by the first pattern
-                if ( ((pRootData[0] ^ pTempData[0]) & 1) == 0 )
-                    for ( w = 0; w < pInfo->nWords; w++ )
-                        pPat->pData[w] |= (pRootData[w] ^ pTempData[w]);
-            }
-        }
-        else
-        {
-            for ( w = 0; w < pInfo->nWords; w++ )
-                if ( pRootData[w] != ~pTempData[w] )
-                    break;
-            if ( w == pInfo->nWords ) // the same info
-                Vec_IntWriteEntry( vClass, k++, NodeId );
-            else
-            {
-                Vec_IntPush( vClass2, NodeId );
-                // record the diffs if they are not distinguished by the first pattern
-                if ( ((pRootData[0] ^ ~pTempData[0]) & 1) == 0 )
-                    for ( w = 0; w < pInfo->nWords; w++ )
-                        pPat->pData[w] |= (pRootData[w] ^ ~pTempData[w]);
-            }
-        }
-    }
-    Vec_IntShrink( vClass, k );
-//    printf( "Class1 = %5d. Class2 = %5d.\n", Vec_IntSize(vClass), Vec_IntSize(vClass2) ); 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the equivalence classes using the simulation info.]
-
-  Description [Records successful simulation patterns into the pattern
-  storage.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask )
-{
-    Vec_Ptr_t * vClass;
-    int i, k, fSplit = 0;
-    assert( Vec_VecSize(vClasses) > 0 );
-    // collect patterns that lead to changes
-    Aig_PatternClean( pPatMask );
-    // split the classes using the new symmetry info
-    Vec_VecForEachLevel( vClasses, vClass, i )
-    {
-        if ( i == 0 )
-            continue;
-        // split vClass into two parts (vClass and vClassTemp)
-        Aig_ManSplitClass( p, pInfo, (Vec_Int_t *)vClass, p->vClassTemp, pPatMask );
-        // check if there is any splitting
-        if ( Vec_IntSize(p->vClassTemp) > 0 )
-            fSplit = 1;
-        // skip the new class if it is empty or trivial
-        if ( Vec_IntSize(p->vClassTemp) < 2 )
-            continue;
-        // consider replacing the current class with the new one
-        if ( Vec_PtrSize(vClass) == 1 )
-        {
-            assert( vClasses->pArray[i] == vClass );
-            vClasses->pArray[i] = p->vClassTemp;
-            p->vClassTemp = (Vec_Int_t *)vClass;
-            i--;
-            continue;
-        }
-        // add the new non-trival class in the end
-        Vec_PtrPush( (Vec_Ptr_t *)vClasses, p->vClassTemp );
-        p->vClassTemp = Vec_IntAlloc( 10 );
-    }
-    // free trivial classes
-    k = 0;
-    Vec_VecForEachLevel( vClasses, vClass, i )
-    {
-        assert( Vec_PtrSize(vClass) > 0 );
-        if ( Vec_PtrSize(vClass) == 1 )
-            Vec_PtrFree(vClass);
-        else
-            vClasses->pArray[k++] = vClass;
-    }
-    Vec_PtrShrink( (Vec_Ptr_t *)vClasses, k );
-    // catch the patterns which led to splitting
-    printf( "Classes = %6d. Pairs = %6d.  Patterns = %3d.\n", 
-        Vec_VecSize(vClasses), 
-        Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses), 
-        Vec_PtrSize(p->vPats) );
-    return fSplit;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects useful patterns.]
-
-  Description [If the flag fAddToVector is 1, creates and adds new patterns
-  to the internal storage of patterns.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats )
-{
-    Aig_SimInfo_t * pInfoRes = p->pInfo;
-    Aig_Pattern_t * pPatNew;
-    Aig_Node_t * pNode;
-    int i, k;
-
-    assert( Aig_InfoHasBit(pMask->pData, 0) == 0 );
-    for ( i = 0; i < pMask->nBits; i++ )
-    {
-        if ( vPats && Vec_PtrSize(vPats) >= p->nPatsMax )
-            break;
-        if ( i == 0 || Aig_InfoHasBit(pMask->pData, i) )
-        {
-            // expand storage if needed
-            if ( pInfoRes->nPatsCur == pInfoRes->nPatsMax )
-                Aig_SimInfoResize( pInfoRes );
-            // create a new pattern
-            if ( vPats )
-            {
-                pPatNew = Aig_PatternAlloc( Aig_ManPiNum(p) );
-                Aig_PatternClean( pPatNew );
-            }
-            // go through the PIs
-            Aig_ManForEachPi( p, pNode, k )
-            {
-                if ( Aig_InfoHasBit( Aig_SimInfoForNode(pInfo, pNode), i ) )
-                {
-                    Aig_InfoSetBit( Aig_SimInfoForPi(pInfoRes, k), pInfoRes->nPatsCur );
-                    if ( vPats ) Aig_InfoSetBit( pPatNew->pData, k );
-                }
-            }
-            // store the new pattern
-            if ( vPats ) Vec_PtrPush( vPats, pPatNew ); 
-            // increment the number of patterns stored
-            pInfoRes->nPatsCur++;
-        }
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c
deleted file mode 100644
index 913165b2..00000000
--- a/src/sat/aig/fraigCnf.c
+++ /dev/null
@@ -1,476 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigCnf.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: fraigCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ClauseTriv( solver * pSat, Aig_Node_t * pNode, Vec_Int_t * vVars )
-{
-//printf( "Adding triv %d.         %d\n", Aig_Regular(pNode)->Id, (int)pSat->solver_stats.clauses );
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond( Aig_Regular(pNode)->Data, Aig_IsComplement(pNode) ) );
-//    Vec_IntPush( vVars, toLitCond( (int)Aig_Regular(pNode)->Id, Aig_IsComplement(pNode) ) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ClauseAnd( solver * pSat, Aig_Node_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
-{
-    int fComp1, Var, Var1, i;
-//printf( "Adding AND %d.  (%d)    %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses );
-
-    assert( !Aig_IsComplement( pNode ) );
-    assert( Aig_NodeIsAnd( pNode ) );
-
-//    nVars = solver_nvars(pSat);
-    Var = pNode->Data;
-//    Var = pNode->Id;
-
-//    assert( Var  < nVars ); 
-    for ( i = 0; i < vSuper->nSize; i++ )
-    {
-        // get the predecessor nodes
-        // get the complemented attributes of the nodes
-        fComp1 = Aig_IsComplement(vSuper->pArray[i]);
-        // determine the variable numbers
-        Var1 = Aig_Regular(vSuper->pArray[i])->Data;
-//        Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
-
-        // check that the variables are in the SAT manager
-//        assert( Var1 < nVars );
-
-        // suppose the AND-gate is A * B = C
-        // add !A => !C   or   A + !C
-    //  fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
-        vVars->nSize = 0;
-        Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
-        Vec_IntPush( vVars, toLitCond(Var,  1     ) );
-        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-            return 0;
-    }
-
-    // add A & B => C   or   !A + !B + C
-//  fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
-    vVars->nSize = 0;
-    for ( i = 0; i < vSuper->nSize; i++ )
-    {
-        // get the predecessor nodes
-        // get the complemented attributes of the nodes
-        fComp1 = Aig_IsComplement(vSuper->pArray[i]);
-        // determine the variable numbers
-        Var1 = Aig_Regular(vSuper->pArray[i])->Data;
-//        Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
-        // add this variable to the array
-        Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
-    }
-    Vec_IntPush( vVars, toLitCond(Var, 0) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Adds trivial clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ClauseMux( solver * pSat, Aig_Node_t * pNode, Aig_Node_t * pNodeC, Aig_Node_t * pNodeT, Aig_Node_t * pNodeE, Vec_Int_t * vVars )
-{
-    int VarF, VarI, VarT, VarE, fCompT, fCompE;
-//printf( "Adding mux %d.         %d\n", pNode->Id, (int)pSat->solver_stats.clauses );
-
-    assert( !Aig_IsComplement( pNode ) );
-    assert( Aig_NodeIsMuxType( pNode ) );
-    // get the variable numbers
-    VarF = pNode->Data;
-    VarI = pNodeC->Data;
-    VarT = Aig_Regular(pNodeT)->Data;
-    VarE = Aig_Regular(pNodeE)->Data;
-//    VarF = (int)pNode->Id;
-//    VarI = (int)pNodeC->Id;
-//    VarT = (int)Aig_Regular(pNodeT)->Id;
-//    VarE = (int)Aig_Regular(pNodeE)->Id;
-
-    // get the complementation flags
-    fCompT = Aig_IsComplement(pNodeT);
-    fCompE = Aig_IsComplement(pNodeE);
-
-    // f = ITE(i, t, e)
-    // i' + t' + f
-    // i' + t  + f'
-    // i  + e' + f
-    // i  + e  + f'
-    // create four clauses
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarI,  1) );
-    Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarI,  1) );
-    Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarI,  0) );
-    Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
-    Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarI,  0) );
-    Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
-    Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
-
-    if ( VarT == VarE )
-    {
-//        assert( fCompT == !fCompE );
-        return 1;
-    }
-
-    // two additional clauses
-    // t' & e' -> f'       t  + e   + f'
-    // t  & e  -> f        t' + e'  + f 
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
-    Vec_IntPush( vVars, toLitCond(VarF,  1) );
-    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
-        return 0;
-    vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
-    Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
-    Vec_IntPush( vVars, toLitCond(VarF,  0) );
-    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ClauseCollectSupergate_rec( Aig_Node_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
-{
-    int RetValue1, RetValue2, i;
-    // check if the node is visited
-    if ( Aig_Regular(pNode)->fMarkB )
-    {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pNode )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Aig_Not(pNode) )
-                return -1;
-        assert( 0 );
-        return 0;
-    }
-    // if the new node is complemented or a PI, another gate begins
-    if ( !fFirst )
-    if ( Aig_IsComplement(pNode) || !Aig_NodeIsAnd(pNode) || Aig_NodeRefs(pNode) > 1 || fStopAtMux && Aig_NodeIsMuxType(pNode) )
-    {
-        Vec_PtrPush( vSuper, pNode );
-        Aig_Regular(pNode)->fMarkB = 1;
-        return 0;
-    }
-    assert( !Aig_IsComplement(pNode) );
-    assert( Aig_NodeIsAnd(pNode) );
-    // go through the branches
-    RetValue1 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild0(pNode), vSuper, 0, fStopAtMux );
-    RetValue2 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild1(pNode), vSuper, 0, fStopAtMux );
-    if ( RetValue1 == -1 || RetValue2 == -1 )
-        return -1;
-    // return 1 if at least one branch has a duplicate
-    return RetValue1 || RetValue2;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ClauseCollectSupergate( Aig_Node_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
-{
-    int RetValue, i;
-    assert( !Aig_IsComplement(pNode) );
-    // collect the nodes in the implication supergate
-    Vec_PtrClear( vNodes );
-    RetValue = Aig_ClauseCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
-    assert( vNodes->nSize > 1 );
-    // unmark the visited nodes
-    for ( i = 0; i < vNodes->nSize; i++ )
-        Aig_Regular((Aig_Node_t *)vNodes->pArray[i])->fMarkB = 0;
-    // if we found the node and its complement in the same implication supergate, 
-    // return empty set of nodes (meaning that we should use constant-0 node)
-    if ( RetValue == -1 )
-        vNodes->nSize = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Sets up the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ClauseCreateCnfInt( solver * pSat, Aig_Man_t * pNtk )
-{
-    Aig_Node_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
-    Vec_Ptr_t * vNodes, * vSuper;
-    Vec_Int_t * vVars;
-    int i, k, fUseMuxes = 1;
-
-    // start the data structures
-    vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
-    vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
-    vVars  = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
-
-    // add the clause for the constant node
-    pNode = Aig_ManConst1(pNtk);
-    pNode->fMarkA = 1;
-    pNode->Data = vNodes->nSize;
-    Vec_PtrPush( vNodes, pNode );
-    Aig_ClauseTriv( pSat, pNode, vVars );
-
-    // collect the nodes that need clauses and top-level assignments
-    Aig_ManForEachPo( pNtk, pNode, i )
-    {
-        // get the fanin
-        pFanin = Aig_NodeFanin0(pNode);
-        // create the node's variable
-        if ( pFanin->fMarkA == 0 )
-        {
-            pFanin->fMarkA = 1;
-            pFanin->Data = vNodes->nSize;
-            Vec_PtrPush( vNodes, pFanin );
-        }
-        // add the trivial clause
-        if ( !Aig_ClauseTriv( pSat, Aig_NodeChild0(pNode), vVars ) )
-            return 0;
-    }
-
-    // add the clauses
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        assert( !Aig_IsComplement(pNode) );
-        if ( !Aig_NodeIsAnd(pNode) )
-            continue;
-//printf( "%d ", pNode->Id );
-
-        // add the clauses
-        if ( fUseMuxes && Aig_NodeIsMuxType(pNode) )
-        {
-            pNode->pMan->nMuxes++;
-            pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
-            Vec_PtrClear( vSuper );
-            Vec_PtrPush( vSuper, pNodeC );
-            Vec_PtrPush( vSuper, pNodeT );
-            Vec_PtrPush( vSuper, pNodeE );
-            // add the fanin nodes to explore
-            Vec_PtrForEachEntry( vSuper, pFanin, k )
-            {
-                pFanin = Aig_Regular(pFanin);
-                if ( pFanin->fMarkA == 0 )
-                {
-                    pFanin->fMarkA = 1;
-                    pFanin->Data = vNodes->nSize;
-                    Vec_PtrPush( vNodes, pFanin );
-                }
-            }
-            // add the clauses
-            if ( !Aig_ClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
-                return 0;
-        }
-        else
-        {
-            // get the supergate
-            Aig_ClauseCollectSupergate( pNode, fUseMuxes, vSuper );
-            // add the fanin nodes to explore
-            Vec_PtrForEachEntry( vSuper, pFanin, k )
-            {
-                pFanin = Aig_Regular(pFanin);
-                if ( pFanin->fMarkA == 0 )
-                {
-                    pFanin->fMarkA = 1;
-                    pFanin->Data = vNodes->nSize;
-                    Vec_PtrPush( vNodes, pFanin );
-                }
-            }
-            // add the clauses
-            if ( vSuper->nSize == 0 )
-            {
-                if ( !Aig_ClauseTriv( pSat, Aig_Not(pNode), vVars ) )
-                    return 0;
-            }
-            else
-            {
-                if ( !Aig_ClauseAnd( pSat, pNode, vSuper, vVars ) )
-                    return 0;
-            }
-        }
-    }
-
-    // delete
-    Vec_IntFree( vVars );
-    Vec_PtrFree( vNodes );
-    Vec_PtrFree( vSuper );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets up the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-solver * Aig_ClauseCreateCnf( Aig_Man_t * pMan )
-{
-    solver * pSat;
-    Aig_Node_t * pNode;
-    int RetValue, i, clk = clock();
-    // clean the marks
-    Aig_ManForEachNode( pMan, pNode, i )
-        pNode->fMarkA = 0, pNode->Data = -1;
-    // create the solver
-    pMan->nMuxes = 0;
-    pSat = solver_new();
-    RetValue = Aig_ClauseCreateCnfInt( pSat, pMan );
-//    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
-    if ( RetValue == 0 )
-    {
-        solver_delete(pSat);
-        Aig_ManForEachNode( pMan, pNode, i )
-            pNode->fMarkA = 0;
-        return NULL;
-    }
-    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", 
-        pNode->pMan->nMuxes, 300.0*pNode->pMan->nMuxes/Aig_ManNodeNum(pMan) );
-    PRT( "Creating solver", clock() - clk );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan )
-{
-    Aig_Node_t * pNode;
-    int i;
-
-    // make sure it has one PO
-    if ( Aig_ManPoNum(pMan) != 1 )
-    {
-        printf( "The miter has other than 1 output.\n" );
-        return AIG_PROOF_FAIL;
-    }
-
-    // get the solver
-    assert( pMan->pSat == NULL );
-    pMan->pSat = Aig_ClauseCreateCnf( pMan );
-    if ( pMan->pSat == NULL )
-        return AIG_PROOF_UNSAT;
-
-    // get the variable mappings
-    pMan->vVar2Sat = Vec_IntStart( Aig_ManNodeNum(pMan) );
-    pMan->vSat2Var = Vec_IntStart( solver_nvars(pMan->pSat) );
-    Aig_ManForEachNode( pMan, pNode, i )
-    {
-        Vec_IntWriteEntry( pMan->vVar2Sat, i, pNode->Data );
-        if ( pNode->Data >= 0 ) Vec_IntWriteEntry( pMan->vSat2Var, pNode->Data, i );
-    }
-    // get the SAT var numbers of the primary inputs
-    pMan->vPiSatNums = Vec_IntAlloc( Aig_ManPiNum(pMan) );
-    Aig_ManForEachPi( pMan, pNode, i )
-        Vec_IntPush( pMan->vPiSatNums, (pNode->Data >= 0)? pNode->Data : 0 );
-    return AIG_PROOF_NONE;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
deleted file mode 100644
index 03781180..00000000
--- a/src/sat/aig/fraigCore.c
+++ /dev/null
@@ -1,129 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigCore.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: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Top-level equivalence checking procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
-{
-    Aig_ProofType_t RetValue;
-    int clk, status;
-    
-    // create the solver
-    RetValue = Aig_ClauseSolverStart( pMan );
-    if ( RetValue != AIG_PROOF_NONE )
-        return RetValue;
-    // perform solving
-
-    // simplify the problem
-    clk = clock();
-    status = solver_simplify(pMan->pSat);
-    if ( status == 0 )
-    {
-//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return AIG_PROOF_UNSAT;
-    }
-
-    // try to prove the output
-    RetValue = Aig_FraigProveOutput( pMan );
-    if ( RetValue != AIG_PROOF_TIMEOUT )
-        return RetValue;
-
-    // create equivalence classes
-    Aig_EngineSimulateRandomFirst( pMan );
-    // reduce equivalence classes using simulation
-    Aig_EngineSimulateFirst( pMan );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Top-level equivalence checking procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
-{
-    Aig_ProofType_t RetValue;
-    int clk, status;
-
-    // solve the miter
-    clk = clock();
-    pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
-    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit );
-    if ( status == l_Undef )
-    {
-//        printf( "The problem timed out.\n" );
-        RetValue = AIG_PROOF_TIMEOUT;
-    }
-    else if ( status == l_True )
-    {
-//        printf( "The problem is SATISFIABLE.\n" );
-        RetValue = AIG_PROOF_SAT;
-    }
-    else if ( status == l_False )
-    {
-//        printf( "The problem is UNSATISFIABLE.\n" );
-        RetValue = AIG_PROOF_UNSAT;
-    }
-    else
-        assert( 0 );
-//    PRT( "SAT solver time", clock() - clk );
-
-    // if the problem is SAT, get the counterexample
-    if ( status == l_True )
-    {
-        if ( pMan->pModel ) free( pMan->pModel );
-        pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize );
-        printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] );
-    }
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c
deleted file mode 100644
index 17468e8f..00000000
--- a/src/sat/aig/fraigEngine.c
+++ /dev/null
@@ -1,174 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigEngine.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: fraigEngine.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 for the first time.]
-
-  Description [Assigns the original simulation info and the storage for the
-  future simulation info.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
-{
-    Aig_SimInfo_t * pInfoPi, * pInfoAll;
-    assert( !p->pInfo && !p->pInfoTemp );
-    // create random PI info
-    pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 );
-    Aig_SimInfoRandom( pInfoPi );
-    // allocate sim info for all nodes
-    pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 1 );
-    // simulate though the circuit
-    Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
-    // detect classes
-    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
-    Aig_SimInfoFree( pInfoAll );
-    // save simulation info
-    p->pInfo     = pInfoPi;
-    p->pInfoPi   = Aig_SimInfoAlloc( Aig_ManPiNum(p),   Aig_ManPiNum(p)+1,  0 );
-    p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1,  1 );
-    p->pPatMask  = Aig_PatternAlloc( Aig_ManPiNum(p)+1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the simulation engine for the first time.]
-
-  Description [Tries several random patterns and their distance-1 
-  minterms hoping to get simulation started.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_EngineSimulateFirst( Aig_Man_t * p )
-{
-    Aig_Pattern_t * pPat;
-    int i, Counter;
-
-    // simulate the pattern of all zeros
-    pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); 
-    Aig_PatternClean( pPat );
-    Vec_PtrPush( p->vPats, pPat );
-    if ( !Aig_EngineSimulate( p ) )
-        return;
-
-    // simulate the pattern of all ones
-    pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); 
-    Aig_PatternFill( pPat );
-    Vec_PtrPush( p->vPats, pPat );
-    if ( !Aig_EngineSimulate( p ) )
-        return;
-
-    // simulate random until the number of new patterns is reasonable
-    do {
-        // generate random PI siminfo
-        Aig_SimInfoRandom( p->pInfoPi );
-        // simulate this info
-        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
-        // split the classes and collect the new patterns
-        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
-            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL );
-        if ( Vec_VecSize(p->vClasses) == 0 )
-            return;
-        // count the number of useful patterns
-        Counter = Aig_PatternCount(p->pPatMask);
-    }
-    while ( Counter > p->nPatsMax/2 );
-
-    // perform targetted simulation
-    for ( i = 0; i < 3; i++ )
-    {
-        assert( Vec_PtrSize(p->vPats) == 0 );
-        // generate random PI siminfo
-        Aig_SimInfoRandom( p->pInfoPi );
-        // simulate this info
-        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
-        // split the classes and collect the new patterns
-        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
-            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
-        if ( Vec_VecSize(p->vClasses) == 0 )
-            return;
-        // simulate the remaining patters
-        if ( Vec_PtrSize(p->vPats) > 0 )
-            if ( !Aig_EngineSimulate( p ) )
-                return;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements intelligent simulation engine.]
-
-  Description [Assumes that the good simulation patterns have been 
-  assigned (p->vPats). Simulates until all of them are gone. Returns 1 
-  if some classes are left. Returns 0 if there is no more classes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_EngineSimulate( Aig_Man_t * p )
-{
-    Aig_Pattern_t * pPat;
-    if ( Vec_VecSize(p->vClasses) == 0 )
-        return 0;
-    assert( Vec_PtrSize(p->vPats) > 0 );
-    // process patterns
-    while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 )
-    {
-        // get the pattern and create new siminfo
-        pPat = Vec_PtrPop(p->vPats);
-        assert( pPat->nBits == Aig_ManPiNum(p) );
-        // create the new siminfo
-        Aig_SimInfoFromPattern( p->pInfoPi, pPat );
-        // free the pattern
-        Aig_PatternFree( pPat );
-
-        // simulate this info
-        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
-        // split the classes and collect the new patterns
-        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
-            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
-    }
-    return Vec_VecSize(p->vClasses) > 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
deleted file mode 100644
index 901f2fe2..00000000
--- a/src/sat/aig/fraigProve.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigProve.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: fraigProve.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
deleted file mode 100644
index 6d4f214c..00000000
--- a/src/sat/aig/fraigSim.c
+++ /dev/null
@@ -1,361 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigSim.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: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates all nodes using the given simulation info.]
-
-  Description [Returns the simulation info for all nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
-{
-    Aig_Node_t * pNode;
-    unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
-    int i, k, fComp0, fComp1;
-
-    assert( !pInfoPi->Type ); // PI siminfo
-    // set the constant sim info
-    pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
-    for ( k = 0; k < pInfoPi->nWords; k++ )
-        pData1[k] = ~((unsigned)0);
-    // set the PI siminfo
-    Aig_ManForEachPi( p, 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
-    Aig_ManForEachAnd( p, pNode, i )
-    {
-        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];
-    }
-    // derive the PO siminfo
-    Aig_ManForEachPo( p, pNode, i )
-    {
-        pDataPo  = Aig_SimInfoForNode( pInfoAll, pNode );
-        pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
-        if ( Aig_NodeFaninC0(pNode) )
-            for ( k = 0; k < pInfoPi->nWords; k++ )
-                pDataPo[k] = ~pDataAnd[k];
-        else
-            for ( k = 0; k < pInfoPi->nWords; k++ )
-                pDataPo[k] = pDataAnd[k];
-    }
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, 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   = Aig_BitWordNum(nBits);
-    p->nPatsCur = nBits;
-    p->nPatsMax = p->nWords * sizeof(unsigned) * 8;
-    p->pData    = ALLOC( unsigned, nNodes * p->nWords );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the simulation info to zero.]
-
-  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    [Sets the random simulation info.]
-
-  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;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the random simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
-{
-    unsigned * pData;
-    int i, k;
-    assert( p->Type == 0 );
-    assert( p->nPatsCur == pPat->nBits+1 );
-    for ( i = 0; i < p->nPatsCur; i++ )
-    {
-        // get the pointer to the bitdata for node i
-        pData = p->pData + p->nWords * i;
-        // fill in the bit data according to the pattern
-        if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1
-            for ( k = 0; k < p->nWords; k++ )
-                pData[k] = ~((unsigned)0);
-        else
-            for ( k = 0; k < p->nWords; k++ )
-                pData[k] = 0;
-        // flip one bit, starting from the first pattern
-        if ( i ) Aig_InfoXorBit( pData, i-1 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the simulation info.]
-
-  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->nWords   *= 2;
-    p->nPatsMax *= 2;
-    free( p->pData );
-    p->pData = pData;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_SimInfoFree( Aig_SimInfo_t * p )
-{
-    free( p->pData );
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Pattern_t * Aig_PatternAlloc( int nBits )
-{
-    Aig_Pattern_t * pPat;
-    pPat = ALLOC( Aig_Pattern_t, 1 );
-    memset( pPat, 0, sizeof(Aig_Pattern_t) );
-    pPat->nBits  = nBits;
-    pPat->nWords = Aig_BitWordNum(nBits);
-    pPat->pData  = ALLOC( unsigned, pPat->nWords );
-    return pPat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_PatternClean( Aig_Pattern_t * pPat )
-{
-    memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_PatternFill( Aig_Pattern_t * pPat )
-{
-    memset( pPat->pData, 0xff, sizeof(unsigned) * pPat->nWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the random pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_PatternRandom( Aig_Pattern_t * pPat )
-{
-    int i;
-    for ( i = 0; i < pPat->nWords; i++ )
-        pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in the pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_PatternCount( Aig_Pattern_t * pPat )
-{
-    int i, Counter = 0;
-    for ( i = 0; i < pPat->nBits; i++ )
-        Counter += Aig_InfoHasBit( pPat->pData, i );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_PatternFree( Aig_Pattern_t * pPat )
-{
-    free( pPat->pData );
-    free( pPat );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/fraigSolver.c b/src/sat/aig/fraigSolver.c
deleted file mode 100644
index 12502951..00000000
--- a/src/sat/aig/fraigSolver.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigSolver.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: fraigSolver.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/fraigTrav.c b/src/sat/aig/fraigTrav.c
deleted file mode 100644
index d5a09259..00000000
--- a/src/sat/aig/fraigTrav.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraigTrav.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: fraigTrav.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/rwrMffc.c b/src/sat/aig/rwrMffc.c
deleted file mode 100644
index 663534b3..00000000
--- a/src/sat/aig/rwrMffc.c
+++ /dev/null
@@ -1,303 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [rwrMffc.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Procedures working with Maximum Fanout-Free Cones.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: rwrMffc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern int  Aig_NodeDeref_rec( Aig_Node_t * pNode );
-extern int  Aig_NodeRef_rec( Aig_Node_t * pNode );
-extern void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-extern void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_MffcTest( Aig_Man_t * pMan )
-{
-    Aig_Node_t * pNode, * pNodeA, * pNodeB, * pNodeC, * pLeaf;
-    Vec_Ptr_t * vCone, * vSupp;
-    int i, k;//, nNodes1, nNodes2;
-    int nSizes = 0;
-    int nCones = 0;
-    int nMuxes = 0;
-    int nExors = 0;
-
-    vCone = Vec_PtrAlloc( 100 );
-    vSupp = Vec_PtrAlloc( 100 );
-
-    // mark the multiple-fanout nodes
-    Aig_ManForEachAnd( pMan, pNode, i )
-        if ( pNode->nRefs > 1 )
-            pNode->fMarkA = 1;
-    // unmark the control inputs of MUXes and inputs of EXOR gates
-    Aig_ManForEachAnd( pMan, pNode, i )
-    {
-        if ( !Aig_NodeIsMuxType(pNode) )
-            continue;
-
-        pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
-        // if real children are used, skip
-        if ( Aig_NodeFanin0(pNode)->nRefs > 1 || Aig_NodeFanin1(pNode)->nRefs > 1 )
-            continue;
-/*
-
-        if ( pNodeC->nRefs == 2 )
-            pNodeC->fMarkA = 0;
-        if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) && Aig_Regular(pNodeA)->nRefs == 2 )
-            Aig_Regular(pNodeA)->fMarkA = 0;
-*/
-
-        if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) )
-            nExors++;
-        else
-            nMuxes++;
-    }
-    // mark the PO drivers
-    Aig_ManForEachPo( pMan, pNode, i )
-    {
-        Aig_NodeFanin0(pNode)->fMarkA = 1;
-        Aig_NodeFanin0(pNode)->fMarkB = 1;
-    }
-
-
-    // print sizes of MFFCs
-    Aig_ManForEachAnd( pMan, pNode, i )
-    {
-        if ( !pNode->fMarkA )
-            continue;
-
-//        nNodes1 = Aig_NodeDeref_rec( pNode );
-//        Aig_NodeMffsConeSupp( pNode, vCone, vSupp );
-//        nNodes2 = Aig_NodeRef_rec( pNode );
-//        assert( nNodes1 == nNodes2 );
-
-        Aig_NodeFactorConeSupp( pNode, vCone, vSupp );
-
-        printf( "%6d : Fan = %4d. Co = %5d.  Su = %5d.  %s ", 
-            pNode->Id, pNode->nRefs, Vec_PtrSize(vCone), Vec_PtrSize(vSupp), pNode->fMarkB? "po" : "  " );
-
-        Vec_PtrForEachEntry( vSupp, pLeaf, k )
-            printf( " %d", pLeaf->Id );
-
-        printf( "\n" );
-
-        nSizes += Vec_PtrSize(vCone);
-        nCones++;
-    }
-    printf( "Nodes = %6d.  MFFC sizes = %6d.  Cones = %6d.  nExors = %6d.  Muxes = %6d.\n",
-        Aig_ManAndNum(pMan), nSizes, nCones, nExors, nMuxes );
-
-    // unmark the nodes
-    Aig_ManForEachNode( pMan, pNode, i )
-    {
-        pNode->fMarkA = 0;
-        pNode->fMarkB = 0;
-        pNode->fMarkC = 0;
-    }
-
-    Vec_PtrFree( vCone );
-    Vec_PtrFree( vSupp );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dereferences the node's MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeDeref_rec( Aig_Node_t * pNode )
-{
-    Aig_Node_t * pNode0, * pNode1;
-    int Counter = 1;
-    if ( Aig_NodeIsPi(pNode) )
-        return 0;
-    pNode0 = Aig_NodeFanin0(pNode);
-    pNode1 = Aig_NodeFanin1(pNode);
-    assert( pNode0->nRefs > 0 );
-    assert( pNode1->nRefs > 0 );
-    if ( --pNode0->nRefs == 0 )
-        Counter += Aig_NodeDeref_rec( pNode0 );
-    if ( --pNode1->nRefs == 0 )
-        Counter += Aig_NodeDeref_rec( pNode1 );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [References the node's MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeRef_rec( Aig_Node_t * pNode )
-{
-    Aig_Node_t * pNode0, * pNode1;
-    int Counter = 1;
-    if ( Aig_NodeIsPi(pNode) )
-        return 0;
-    pNode0 = Aig_NodeFanin0(pNode);
-    pNode1 = Aig_NodeFanin1(pNode);
-    if ( pNode0->nRefs++ == 0 )
-        Counter += Aig_NodeRef_rec( pNode0 );
-    if ( pNode1->nRefs++ == 0 )
-        Counter += Aig_NodeRef_rec( pNode1 );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the internal and leaf nodes in the derefed MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_NodeMffsConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
-{
-    // skip visited nodes
-    if ( Aig_NodeIsTravIdCurrent(pNode) )
-        return;
-    Aig_NodeSetTravIdCurrent(pNode);
-    // add to the new support nodes
-    if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->nRefs > 0) )
-    {
-        Vec_PtrPush( vSupp, pNode );
-        return;
-    }
-    // recur on the children
-    Aig_NodeMffsConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
-    Aig_NodeMffsConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
-    // collect the internal node
-    Vec_PtrPush( vCone, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the support of the derefed MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
-{
-    assert( Aig_NodeIsAnd(pNode) );
-    assert( !Aig_IsComplement(pNode) );
-    Vec_PtrClear( vCone );
-    Vec_PtrClear( vSupp );
-    Aig_ManIncrementTravId( pNode->pMan );
-    Aig_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the internal and leaf nodes of the factor-cut of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_NodeFactorConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
-{
-    // skip visited nodes
-    if ( Aig_NodeIsTravIdCurrent(pNode) )
-        return;
-    Aig_NodeSetTravIdCurrent(pNode);
-    // add to the new support nodes
-    if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->fMarkA) )
-    {
-        Vec_PtrPush( vSupp, pNode );
-        return;
-    }
-    // recur on the children
-    Aig_NodeFactorConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
-    Aig_NodeFactorConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
-    // collect the internal node
-    assert( fTopmost || !pNode->fMarkA );
-    Vec_PtrPush( vCone, pNode );
-
-    assert( pNode->fMarkC == 0 );
-    pNode->fMarkC = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the support of the derefed MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
-{
-    assert( Aig_NodeIsAnd(pNode) );
-    assert( !Aig_IsComplement(pNode) );
-    Vec_PtrClear( vCone );
-    Vec_PtrClear( vSupp );
-    Aig_ManIncrementTravId( pNode->pMan );
-    Aig_NodeFactorConeSupp_rec( pNode, vCone, vSupp, 1 );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
deleted file mode 100644
index cb8d03e0..00000000
--- a/src/sat/aig/rwrTruth.c
+++ /dev/null
@@ -1,456 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [rwrTruth.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: rwrTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-/*  The code in this file was written with portability to 64-bits in mind.
-    The type "unsigned" is assumed to be 32-bit on any platform.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define ABCTMAX      8       // the max number of vars
-
-typedef struct Aig_Truth_t_ Aig_Truth_t;
-struct Aig_Truth_t_
-{
-    short        nVars;                   // the number of variables
-    short        nWords;                  // the number of 32-bit words
-    unsigned     Truth[1<<(ABCTMAX-5)];   // the truth table
-    unsigned     Cofs[2][1<<(ABCTMAX-6)]; // the truth table of cofactors
-    unsigned     Data[4][1<<(ABCTMAX-7)]; // the truth table of cofactors
-    short        Counts[ABCTMAX][2];      // the minterm counters
-    Aig_Node_t * pLeaves[ABCTMAX];        // the pointers to leaves
-    Aig_Man_t *  pMan;                    // the AIG manager
-};
-
-static void Aig_TruthCount( Aig_Truth_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the function given the truth table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Truth_t * Aig_TruthCreate( int nVars, unsigned * pTruth, Aig_Node_t ** pLeaves )
-{
-    Aig_Truth_t * p;
-    int i;
-    p = ALLOC( Aig_Truth_t, 1 );
-    memset( p, 0, sizeof(Aig_Truth_t) );
-    p->nVars  = nVars;
-    p->nWords = (nVars < 5)? 1 : (1 << (nVars-5));
-    for ( i = 0; i < p->nWords; i++ )
-        p->Truth[i] = pTruth[i];
-    if ( nVars < 5 )
-        p->Truth[0] &= (~0u >> (32-(1<<nVars)));
-    for ( i = 0; i < p->nVars; i++ )
-        p->pLeaves[i] = pLeaves[i];
-    Aig_TruthCount( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of miterms in the cofactors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Aig_WordCountOnes( unsigned val )
-{
-    val = (val & 0x55555555) + ((val>>1) & 0x55555555);
-    val = (val & 0x33333333) + ((val>>2) & 0x33333333);
-    val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F);
-    val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF);
-    return (val & 0x0000FFFF) + (val>>16);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of miterms in the cofactors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TruthCount( Aig_Truth_t * p )
-{
-    static unsigned Masks[5][2] = {
-        { 0x33333333, 0xAAAAAAAA },
-        { 0x55555555, 0xCCCCCCCC },
-        { 0x0F0F0F0F, 0xF0F0F0F0 },
-        { 0x00FF00FF, 0xFF00FF00 },
-        { 0x0000FFFF, 0xFFFF0000 }
-    };
-
-    int i, k;
-    assert( p->Counts[0][0] == 0 && p->Counts[0][1] == 0 );
-    for ( i = 0; i < p->nVars; i++ )
-    {
-        p->Counts[i][0] = p->Counts[i][1] = 0;
-        if ( i < 5 )
-        {
-            for ( k = 0; k < p->nWords; k++ )
-            {
-                p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] & Masks[i][0] );
-                p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] & Masks[i][1] );
-            }
-        }
-        else
-        {
-            for ( k = 0; k < p->nWords; k++ )
-                if ( i & (1 << (k-5)) )
-                    p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] );
-                else
-                    p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] );
-        }
-    }
-/*
-    // normalize the variables
-    for ( i = 0; i < p->nVars; i++ )
-        if ( p->Counts[i][0] > p->Counts[i][1] )
-        {
-            k = p->Counts[i][0];
-            p->Counts[i][0] = p->Counts[i][1];
-            p->Counts[i][1] = k;
-            p->pLeaves[i] = Aig_Not( p->pLeaves[i] );
-        }
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Extracts one part of the bitstring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
-{
-    return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts one part of the bitstring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
-{
-    p[Start/5] |= (Part << (Start&31));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the cofactor with respect to one variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TruthCofactor( int Var, int Pol, int nVars, unsigned * pTruth, unsigned * pResult )
-{
-    if ( Var < 5 )
-    {
-        int nPartSize = ( 1 << Var );
-        int nParts    = ( 1 << (nVars-Var-1) );
-        unsigned uPart;
-        int i;
-        for ( i = 0; i < nParts; i++ )
-        {
-            uPart = Aig_WordGetPart( pTruth, (2*i+Pol)*nPartSize, nPartSize );
-            Aig_WordSetPart( pResult, i*nPartSize, uPart ); 
-        }
-        if ( nVars <= 5 )
-            pResult[0] &= (~0u >> (32-(1<<(nVars-1))));
-    }
-    else
-    {
-        int nWords = (1 << (nVars-5));
-        int i, k = 0;
-        for ( i = 0; i < nWords; i++ )
-            if ( (i & (1 << (Var-5))) == Pol )
-                pResult[k++] = pTruth[i];
-        assert( k == nWords/2 );
-    }
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the BDD of the truth table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int nVars, int iVar )
-{
-    DdNode * bCof0, * bCof1, * bRes;
-    if ( nVars == 1 )
-        return Cudd_NotCond( Cudd_ReadOne(dd), !Aig_WordGetPart(pTruth, Shift, 1) );
-    if ( nVars == 3 )
-    {
-        unsigned char * pChar = ((char *)pTruth) + Shift/8;
-        assert( Shift % 8 == 0 );
-        if ( *pChar == 0 )
-            return Cudd_ReadLogicZero(dd);
-        if ( *pChar == 0xFF )
-            return Cudd_ReadOne(dd);
-    }
-    if ( nVars == 5 )
-    {
-        unsigned * pWord = pTruth + (Shift>>5);
-        assert( Shift % 32 == 0 );
-        if ( *pWord == 0 )
-            return Cudd_ReadLogicZero(dd);
-        if ( *pWord == 0xFFFFFFFF )
-            return Cudd_ReadOne(dd);
-    }
-    bCof0 = Aig_TruthToBdd_rec( dd, pTruth, Shift,                    nVars-1, iVar+1 );  Cudd_Ref( bCof0 );
-    bCof1 = Aig_TruthToBdd_rec( dd, pTruth, Shift + (1 << (nVars-1)), nVars-1, iVar+1 );  Cudd_Ref( bCof1 );
-    bRes  = Cudd_bddIte( dd, Cudd_bddIthVar(dd, iVar), bCof1, bCof0 );  Cudd_Ref( bRes );
-    Cudd_RecursiveDeref( dd, bCof0 );
-    Cudd_RecursiveDeref( dd, bCof1 );
-    Cudd_Deref( bRes );
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the BDD of the truth table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Aig_TruthToBdd( DdManager * dd, Aig_Truth_t * p )
-{
-    return Aig_TruthToBdd_rec( dd, p->Truth, 0, p->nVars, 0 );
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Compare bistrings.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Aig_WordCompare( unsigned * p0, unsigned * p1, int nWords )
-{
-    int i;
-    for ( i = 0; i < nWords; i++ )
-        if ( p0[i] != p1[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compare bistrings.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Aig_WordCompareCompl( unsigned * p0, unsigned * p1, int nWords )
-{
-    int i;
-    for ( i = 0; i < nWords; i++ )
-        if ( p0[i] != ~p1[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the cofactor with respect to one variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TruthReplaceByCofactor( Aig_Truth_t * p, int iVar, unsigned * pTruth )
-{
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the cofactor with respect to one variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p )
-{
-    Aig_Node_t * pVar;
-    int nOnesCof = ( 1 << (p->nVars-1) );
-    int nWordsCof = (p->nWords == 1 ? 1 : p->nWords/2);
-    int i;
-
-    // check for constant function
-    if ( p->nVars == 0 )
-        return Aig_NotCond( Aig_ManConst1(p->pMan), (p->Truth[0]&1)==0 );
-
-    // count the number of minterms in the cofactors
-    Aig_TruthCount( p );
-
-    // remove redundant variables and EXORs
-    for ( i = p->nVars - 1; i >= 0; i-- )
-    {
-        if ( p->Counts[i][0] == p->Counts[i][1] )
-        {
-            // compute cofactors
-            Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
-            Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
-            if ( Aig_WordCompare( p->Cofs[0], p->Cofs[1], nWordsCof ) )
-            { // equal
-                // remove redundant variable
-                Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
-                return Aig_TruthDecompose( p );
-            }
-        }
-        // check the case of EXOR
-        if ( p->Counts[i][0] == nOnesCof - p->Counts[i][1] )
-        {
-            // compute cofactors
-            Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
-            Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
-            if ( Aig_WordCompareCompl( p->Cofs[0], p->Cofs[1], nWordsCof ) )
-            { // equal
-                pVar = p->pLeaves[i];
-                // remove redundant variable
-                Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
-                // F = x' * F0 + x * F1 = x <+> F0   assuming that F0 == ~F1
-                return Aig_Xor( p->pMan, pVar, Aig_TruthDecompose( p ) );
-            }
-        }
-    }
-
-    // process variables with constant cofactors
-    for ( i = p->nVars - 1; i >= 0; i-- )
-    {
-        if ( p->Counts[i][0] != 0        && p->Counts[i][1] != 0 && 
-             p->Counts[i][0] != nOnesCof && p->Counts[i][1] != nOnesCof ) 
-             continue;
-        pVar = p->pLeaves[i];
-        if ( p->Counts[i][0] == 0 )
-        {
-            Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
-            // remove redundant variable
-            Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
-            // F = x' * 0 + x * F1 = x * F1 
-            return Aig_And( p->pMan, pVar, Aig_TruthDecompose( p ) );
-        }
-        if ( p->Counts[i][1] == 0 )
-        {
-            Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
-            // remove redundant variable
-            Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
-            // F = x' * F0 + x * 0 = x' * F0 
-            return Aig_And( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
-         }
-        if ( p->Counts[i][0] == nOnesCof )
-        {
-            Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
-            // remove redundant variable
-            Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
-            // F = x' * 1 + x * F1 = x' + F1 
-            return Aig_Or( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
-        }
-        if ( p->Counts[i][1] == nOnesCof )
-        {
-            Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
-            // remove redundant variable
-            Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
-            // F = x' * F0 + x * 1 = x + F0 
-            return Aig_Or( p->pMan, pVar, Aig_TruthDecompose( p ) );
-         }
-        assert( 0 );
-    }
-
-
-    return NULL;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/aig/rwr_.c b/src/sat/aig/rwr_.c
deleted file mode 100644
index 45e76f75..00000000
--- a/src/sat/aig/rwr_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [rwr_.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: rwr_.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                                ///
-////////////////////////////////////////////////////////////////////////
-
-