Version abc60118

26 files changed, 1757 insertions, 245 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 259187bf..5f5c4b49 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3782,8 +3782,9 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3807,19 +3808,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Only works for strashed networks.\n" );
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
         return 1;
     }
 
 //    Abc_NtkTestEsop( pNtk );
 //    Abc_NtkTestSop( pNtk );
 //    printf( "This command is currently not used.\n" );
-
-/*
     // run the command
-    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
+//    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
+    pNtkRes = Abc_NtkNewAig( pNtk );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -3827,7 +3827,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
     return 0;
 
 usage:
diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c
new file mode 100644
index 00000000..33f58135
--- /dev/null
+++ b/src/base/abci/abcNewAig.c
@@ -0,0 +1,376 @@
+/**CFile****************************************************************
+
+  FileName    [aigNewAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Strashing of the current network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigNewAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "extra.h"
+#include "dec.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
+static Aig_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
+
+static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan );
+static Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode );
+static Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+extern char *       Mio_GateReadSop( void * pGate );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
+{
+    Aig_Man_t * pMan;
+    Abc_Ntk_t * pNtkAig;
+    Aig_ProofType_t RetValue;
+    int fCleanup = 1;
+    int nNodes;
+
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    assert( !Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+    // print warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
+
+    // convert to the AIG manager
+    pMan = Abc_NtkToAig( pNtk );
+    // execute a command in the AIG manager
+    RetValue = Aig_FraigProve( pMan );
+    if ( RetValue == AIG_PROOF_SAT )
+        printf( "Satisfiable.\n" );
+    else if ( RetValue == AIG_PROOF_UNSAT )
+        printf( "Unsatisfiable.\n" );
+    else if ( RetValue == AIG_PROOF_TIMEOUT )
+        printf( "Undecided.\n" );
+    else
+        assert( 0 );
+
+    // convert from the AIG manager
+    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+    Aig_ManStop( pMan );
+
+    // report the cleanup results
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Aig_Node_t * pAnd;
+    int i;
+    // perform strashing
+    pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Aig_ManConst1(pMan)->Data = Abc_NtkConst1(pNtk)->Id;
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        Aig_ManPi(pMan, i)->Data = pObj->pCopy->Id;
+    // rebuild the AIG
+    Aig_ManForEachAnd( pMan, pAnd, i )
+    {
+        // add the first fanins
+        pFaninNew0 = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data );
+        pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Aig_NodeFaninC0(pAnd) );
+        // add the first second
+        pFaninNew1 = Abc_NtkObj( pNtk, Aig_NodeFanin1(pAnd)->Data );
+        pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Aig_NodeFaninC1(pAnd) );
+        // create the new node
+        pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+        pAnd->Data = pObjNew->Id;
+    }
+    // connect the PO nodes
+    Abc_NtkForEachCo( pNtkOld, pObj, i )
+    {
+        pAnd = Aig_ManPo( pMan, i );
+        pFaninNew = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data );
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Aig_NodeFaninC0(pAnd) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
+{
+    Aig_Param_t Params;
+    Aig_Man_t * pMan;
+    Abc_Obj_t * pObj;
+    Aig_Node_t * pFanin;
+    int i;
+    // create the manager
+    Aig_ManSetDefaultParams( &Params );
+    pMan = Aig_ManStart( &Params );
+    // create the PIs
+    Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan);
+    // perform the conversion of the internal nodes
+    Abc_NtkStrashPerformAig( pNtkOld, pMan );
+    // create the POs
+    Abc_NtkForEachCo( pNtkOld, pObj, i )
+    {
+        pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy;
+        pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
+        pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin );
+    }
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the network for strashing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan )
+{
+//    ProgressBar * pProgress;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+//    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+//        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode );
+    }
+//    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode )
+{
+    int fUseFactor = 1;
+    char * pSop;
+    Aig_Node_t * pFanin0, * pFanin1;
+    extern int Abc_SopIsExorType( char * pSop );
+
+    assert( Abc_ObjIsNode(pNode) );
+
+    // consider the case when the graph is an AIG
+    if ( Abc_NtkIsStrash(pNode->pNtk) )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            return Aig_ManConst1(pMan);
+        pFanin0 = (Aig_Node_t *)Abc_ObjFanin0(pNode)->pCopy;
+        pFanin0 = Aig_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
+        pFanin1 = (Aig_Node_t *)Abc_ObjFanin1(pNode)->pCopy;
+        pFanin1 = Aig_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
+        return Aig_And( pMan, pFanin0, pFanin1 );
+    }
+
+    // get the SOP of the node
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
+        pSop = Mio_GateReadSop(pNode->pData);
+    else
+        pSop = pNode->pData;
+
+    // consider the constant node
+    if ( Abc_NodeIsConst(pNode) )
+        return Aig_NotCond( Aig_ManConst1(pMan), Abc_SopIsConst0(pSop) );
+
+    // consider the special case of EXOR function
+    if ( Abc_SopIsExorType(pSop) )
+        return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
+
+    // decide when to use factoring
+    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+        return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
+    return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Obj_t * pFanin;
+    Aig_Node_t * pAnd, * pSum;
+    char * pCube;
+    int i, nFanins;
+
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Aig_Not( Aig_ManConst1(pMan) );
+    Abc_SopForEachCube( pSop, nFanins, pCube )
+    {
+        // create the AND of literals
+        pAnd = Aig_ManConst1(pMan);
+        Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
+        {
+            if ( pCube[i] == '1' )
+                pAnd = Aig_And( pMan, pAnd, (Aig_Node_t *)pFanin->pCopy );
+            else if ( pCube[i] == '0' )
+                pAnd = Aig_And( pMan, pAnd, Aig_Not((Aig_Node_t *)pFanin->pCopy) );
+        }
+        // add to the sum of cubes
+        pSum = Aig_Or( pMan, pSum, pAnd );
+    }
+    // decide whether to complement the result
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Aig_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashed n-input XOR function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Obj_t * pFanin;
+    Aig_Node_t * pSum;
+    int i, nFanins;
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Aig_Not( Aig_ManConst1(pMan) );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pFanin = Abc_ObjFanin( pNode, i );
+        pSum = Aig_Xor( pMan, pSum, (Aig_Node_t *)pFanin->pCopy );
+    }
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Aig_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop )
+{
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Aig_Node_t * pAnd;
+    int i;
+    extern Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph );
+
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
+    // collect the fanins
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    // perform strashing
+    pAnd = Dec_GraphToNetworkAig( pMan, pFForm );
+    Dec_GraphFree( pFForm );
+    return pAnd;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 8c8636c5..f7b9892e 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -534,10 +534,10 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_
     Vec_IntPush( vVars, toLitCond(VarF,  1) );
     if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
         return 0;
-
+ 
     if ( VarT == VarE )
     {
-        assert( fCompT == !fCompE );
+//        assert( fCompT == !fCompE );
         return 1;
     }
 
@@ -774,7 +774,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
     RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->fMarkA = 0;
-    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+//    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
     if ( RetValue == 0 )
     {
         solver_delete(pSat);
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 865cd830..58b824d2 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
 
 /**Function********************************************************************
 
-  Synopsis    [Delocates the local cache.]
+  Synopsis    [Deallocates the local cache.]
 
   Description []
 
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 474f663f..358402b0 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -223,7 +223,7 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
 
 /**Function********************************************************************
 
-  Synopsis    [Delocates symmetry information structure.]
+  Synopsis    [Deallocates symmetry information structure.]
 
   Description []
 
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index af1128ac..c9137c56 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -257,7 +257,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 1416cf0d..b24773be 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,6 +18,7 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -201,6 +202,40 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
     assert( nGain <= nNodesOld - nNodesNew );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+    Dec_Node_t * pNode;
+    Aig_Node_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
+    }
+    // complement the result if necessary
+    return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 9da34fde..169fb218 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -159,7 +159,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
     if ( pData->nNodesNew )
         Fxu_CreateCovers( p, pData );
     Fxu_MatrixDelete( p );
-//    printf( "Memory usage after delocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+//    printf( "Memory usage after deallocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
     if ( pData->nNodesNew == pData->nNodesExt )
         printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
     return pData->nNodesNew;
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 009a17bb..55a75cf5 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -48,6 +48,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
+#include "solver.h"
 #include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -70,6 +71,7 @@ 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 { 
@@ -79,12 +81,25 @@ typedef enum {
     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 
@@ -127,6 +142,13 @@ struct Aig_Man_t_
     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
@@ -136,6 +158,7 @@ struct Aig_Man_t_
     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
     // simulation patterns
     int              nPiWords;      // the number of words in the PI info
@@ -148,6 +171,14 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vToReplace;    // the nodes to replace
 };
 
+// the simulation patter
+struct Aig_Pattern_t_  
+{
+    int              nBits;
+    int              nWords;
+    unsigned *       pData;
+};
+
 // the AIG simulation info
 struct Aig_SimInfo_t_  
 {
@@ -166,9 +197,9 @@ struct Aig_SimInfo_t_
     for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
 #define Aig_ManForEachPo( pMan, pNode, i )                                                    \
     for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
-#define Aig_ManForEachAnd( pNtk, pNode, i )                                                   \
+#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
+        if ( !Aig_NodeIsAnd(pNode) ) {} else
 
 // maximum/minimum operators
 #define AIG_MIN(a,b)  (((a) < (b))? (a) : (b))
@@ -178,8 +209,12 @@ struct Aig_SimInfo_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 0);    }
+static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 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);    }
@@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode )   { return Aig_N
 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_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_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;       }
@@ -268,6 +304,7 @@ 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 );
@@ -287,18 +324,33 @@ extern void                Aig_TableResize( Aig_Man_t * pMan );
 extern void                Aig_TableRehash( Aig_Man_t * pMan );
 /*=== aigUtil.c ==========================================================*/
 extern void                Aig_ManIncrementTravId( Aig_Man_t * pMan );
-extern void                Aig_PrintNode( Aig_Node_t * pNode );
+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 void                Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses );
+/*=== fraigCnf.c ==========================================================*/
+extern Aig_ProofType_t     Aig_ClauseSolverStart( Aig_Man_t * pMan );
+/*=== fraigEngine.c ==========================================================*/
+extern void                Aig_EngineSimulateFirst( Aig_Man_t * p );
+extern int                 Aig_EngineSimulate( Aig_Man_t * p );
+extern void                Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
 /*=== fraigSim.c ==========================================================*/
 extern Aig_SimInfo_t *     Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
 extern void                Aig_SimInfoClean( Aig_SimInfo_t * p );
 extern void                Aig_SimInfoRandom( Aig_SimInfo_t * p );
+extern void                Aig_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 Aig_SimInfo_t *     Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
+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_PatternRandom( Aig_Pattern_t * pPat );
+extern void                Aig_PatternFree( Aig_Pattern_t * pPat );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
index 2058f6b0..3807d28a 100644
--- a/src/sat/aig/aigMan.c
+++ b/src/sat/aig/aigMan.c
@@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
     // start the manager
     p = ALLOC( Aig_Man_t, 1 );
     memset( p, 0, sizeof(Aig_Man_t) );
-    p->pParam = &p->Param;
-    p->nTravIds = 1;
+    p->pParam     = &p->Param;
+    p->nTravIds   = 1;
+    p->nPatsMax   = 20;
     // set the defaults
-    *p->pParam = *pParam;
+    *p->pParam    = *pParam;
     // start memory managers
     p->mmNodes    = Aig_MemFixedStart( sizeof(Aig_Node_t) );
     // allocate node arrays
@@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan )
 ***********************************************************************/
 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 );
+    // 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 );
     Aig_TableFree( p->pTable );
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
index 280cf98b..32709bf6 100644
--- a/src/sat/aig/aigMem.c
+++ b/src/sat/aig/aigMem.c
@@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
index afccd985..991cc7e5 100644
--- a/src/sat/aig/aigNode.c
+++ b/src/sat/aig/aigNode.c
@@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
     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;
@@ -66,6 +67,7 @@ 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;
 }
@@ -86,7 +88,8 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
     Aig_Node_t * pNode;
     pNode = Aig_NodeCreate( p );
     Vec_PtrPush( p->vPis, pNode );
-    pNode->fPhase  =  0;  // sim value for 000... pattern
+    pNode->Type   = AIG_PI;
+    pNode->fPhase =  0;  // sim value for 000... pattern
     return pNode;
 }
 
@@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
 {
     Aig_Node_t * pNode;
     pNode = Aig_NodeCreate( p );
+    pNode->Type = AIG_PO;
     Vec_PtrPush( p->vPos, pNode );
     // connect to the fanin
     pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
@@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t
 {
     Aig_Node_t * pNode;
     pNode = Aig_NodeCreate( p );
+    pNode->Type = AIG_AND;
     Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
     return pNode;
 }
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
index cfc94f6b..e6fe87d6 100644
--- a/src/sat/aig/aigTable.c
+++ b/src/sat/aig/aigTable.c
@@ -36,7 +36,7 @@ struct Aig_Table_t_
 #define Aig_TableBinForEachEntry( pBin, pEnt )                 \
     for ( pEnt = pBin;                                         \
           pEnt;                                                \
-          pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
+          pEnt = Aig_NodeNextH(pEnt) )
 #define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 )      \
     for ( pEnt = pBin,                                         \
           pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL;            \
@@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
     Aig_Node_t * pAnd;
     unsigned Key;
     assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
-    assert( p0->pMan == p1->pMan );
     // get the hash key for these two nodes
-    Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+    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) )
@@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
         Aig_TableResize( pMan );
     // add the node to the corresponding linked list in the table
     Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
-    pAnd->NextH = pMan->pTable->pBins[Key]->Id;
-    pMan->pTable->pBins[Key]->NextH = pAnd->Id;
+    pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0;
+    pMan->pTable->pBins[Key] = pAnd;
     pMan->pTable->nEntries++;
     return pAnd;
 }
@@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
         if ( pPlace == NULL )
             pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
         else
-            pPlace->NextH = pThis->Id;
+            pPlace->NextH = pThis->NextH;
         break;
     }
     assert( pThis == pAnd );
@@ -232,8 +231,8 @@ clk = clock();
         Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
         {
             Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
-            pEnt->NextH = pBinsNew[Key]->Id;
-            pBinsNew[Key]->NextH = pEnt->Id;
+            pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+            pBinsNew[Key] = pEnt;
             Counter++;
         }
     assert( Counter == pMan->pTable->nEntries );
@@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan )
            }
             // rehash the node
             Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
-            pEnt->NextH = pBinsNew[Key]->Id;
-            pBinsNew[Key]->NextH = pEnt->Id;
+            pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+            pBinsNew[Key] = pEnt;
             Counter++;
         }
     assert( Counter == pMan->pTable->nEntries );
diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c
index a1c9ca44..40f7aba1 100644
--- a/src/sat/aig/aigUtil.c
+++ b/src/sat/aig/aigUtil.c
@@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan )
 }
 
 
+/**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
index b3040e2a..2f2d3e0c 100644
--- a/src/sat/aig/fraigClass.c
+++ b/src/sat/aig/fraigClass.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [aigFraig.c]
+  FileName    [fraigClass.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
+static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
 ***********************************************************************/
 Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
 {
-    Vec_Vec_t * vClasses;     // equivalence classes
+    Vec_Vec_t * vClasses;    // equivalence classes
     stmm_table * tSim2Node;  // temporary hash table hashing key into the class number
     Aig_Node_t * pNode;       
     unsigned uKey;
-    int i, * pSpot, ClassNum;
+    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 );
-    Aig_ManForEachNode( p, pNode, i )
+    // 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 );
+        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
@@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
         }
         else // this is a class
         {
-            ClassNum = (*pSpot) >> 1;
+            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" );
+    }
     return vClasses;
 }
 
@@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Aig_ManHashKey( unsigned * pData, int nWords )
+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;
-    for ( i = 0; i < nWords; i++ )
-        uKey ^= pData[i] * Primes[i%10];
+    if ( fPhase )
+        for ( i = 0; i < nWords; i++ )
+            uKey ^= Primes[i%10] * pData[i];
+    else
+        for ( i = 0; i < nWords; i++ )
+            uKey ^= Primes[i%10] * ~pData[i];
     return uKey;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the equivalence classes using the simulation info.]
+
+  Description [Records successful simulation patterns into the pattern
+  storage.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses )
+{
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c
new file mode 100644
index 00000000..913165b2
--- /dev/null
+++ b/src/sat/aig/fraigCnf.c
@@ -0,0 +1,476 @@
+/**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
index 6187538b..e7df1335 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [aigFraig.c]
+  FileName    [fraigCore.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -24,13 +24,56 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  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 );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Top-level equivalence checking procedure.]
 
   Description []
                
@@ -39,6 +82,43 @@
   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, pMan->pParam->nSeconds );
+    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
new file mode 100644
index 00000000..6214bf3b
--- /dev/null
+++ b/src/sat/aig/fraigEngine.c
@@ -0,0 +1,131 @@
+/**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    [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;
+    assert( Vec_PtrSize(p->vPats) == 0 );
+    for ( i = 0; i < p->nPatsMax; i++ )
+    {
+        pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
+        Aig_PatternRandom( pPat );
+        Vec_PtrPush( p->vPats, pPat );
+        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);
+        // create the new siminfo
+        Aig_SimInfoFromPattern( p->pInfoPi, pPat );
+        // free the patter
+        Aig_PatternFree( pPat );
+
+        // simulate this info
+        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+        // split the classes and collect the new patterns
+        Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
+    }
+    return Vec_VecSize(p->vClasses) > 0;
+}
+
+/**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( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
+    Aig_SimInfoRandom( pInfoPi );
+    // allocate sim info for all nodes
+    pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 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( p->vPis->nSize,   Aig_BitWordNum(p->vPis->nSize),  0 );
+    p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize),  1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
index b5cce582..901f2fe2 100644
--- a/src/sat/aig/fraigProve.c
+++ b/src/sat/aig/fraigProve.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [aigProve.c]
+  FileName    [fraigProve.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
index 1d547621..415b6918 100644
--- a/src/sat/aig/fraigSim.c
+++ b/src/sat/aig/fraigSim.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [aigSim.c]
+  FileName    [fraigSim.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -30,59 +30,28 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Simulates all nodes using random simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
-{
-    Aig_SimInfo_t * pInfoPi, * pInfoAll;
-    assert( p->pInfo && p->pInfoTemp );
-    // create random PI info
-    pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
-    Aig_SimInfoRandom( pInfoPi );
-    // simulate it though the circuit
-    pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
-    // detect classes
-    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
-    Aig_SimInfoFree( pInfoAll );
-    // save simulation info
-    p->pInfo = pInfoPi;
-    p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Simulates all nodes using the given simulation info.]
 
-  Description []
+  Description [Returns the simulation info for all nodes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
+void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
 {
-    Aig_SimInfo_t * pInfoAll;
     Aig_Node_t * pNode;
-    unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
+    unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
     int i, k, fComp0, fComp1;
 
     assert( !pInfoPi->Type ); // PI siminfo
-    // allocate sim info for all nodes
-    pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
     // set the constant sim info
     pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
     for ( k = 0; k < pInfoPi->nWords; k++ )
         pData1[k] = ~((unsigned)0);
-    // copy the PI siminfo
-    Vec_PtrForEachEntry( p->vPis, pNode, i )
+    // set the PI siminfo
+    Aig_ManForEachPi( p, pNode, i )
     {
         pDataPi  = Aig_SimInfoForPi( pInfoPi, i );
         pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
@@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
             pDataAnd[k] = pDataPi[k];
     }
     // simulate the nodes
-    Vec_PtrForEachEntry( p->vNodes, pNode, i )
+    Aig_ManForEachAnd( p, pNode, i )
     {
-        if ( !Aig_NodeIsAnd(pNode) )
-            continue;
         pData0   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
         pData1   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
         pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode                 );
@@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
             for ( k = 0; k < pInfoPi->nWords; k++ )
                 pDataAnd[k] =  pData0[k] &  pData1[k];
     }
-    return pInfoAll;
+    // derive the PO siminfo
+    Aig_ManForEachPi( 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    []
+  Synopsis    [Allocates the simulation info.]
 
   Description []
                
@@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Sets the simulation info to zero.]
 
   Description []
                
@@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Sets the random simulation info.]
 
   Description []
                
@@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  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->nNodes == pPat->nBits );
+    for ( i = 0; i < p->nNodes; 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
+        Aig_InfoXorBit( pData, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the simulation info.]
 
   Description []
                
@@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p )
         for ( k = 0; k < p->nWords; k++ )
             pData[2 * p->nWords * i + k + p->nWords] = 0;
     }
-    p->nPatsMax *= 2;
     p->nWords   *= 2;
+    p->nPatsMax *= 2;
+    free( p->pData );
+    p->pData = pData;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Deallocates the simulation info.]
 
   Description []
                
@@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * 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    [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    [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
new file mode 100644
index 00000000..12502951
--- /dev/null
+++ b/src/sat/aig/fraigSolver.c
@@ -0,0 +1,47 @@
+/**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
new file mode 100644
index 00000000..d5a09259
--- /dev/null
+++ b/src/sat/aig/fraigTrav.c
@@ -0,0 +1,47 @@
+/**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/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index eb1c5374..3fadd457 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -26,7 +26,7 @@
 
 #define ABC_DEFAULT_TIMEOUT     60   // 60 seconds
 
-struct CSAT_ManagerStruct_t
+struct ABC_ManagerStruct_t
 {
     // information about the problem
     stmm_table *          tName2Node;    // the hash table mapping names to nodes
@@ -43,11 +43,11 @@ struct CSAT_ManagerStruct_t
     Vec_Ptr_t *           vNodes;        // the gates in the target
     Vec_Int_t *           vValues;       // the values of gate's outputs in the target
     // solution
-    CSAT_Target_ResultT * pResult;       // the result of solving the target
+    ABC_Target_ResultT *  pResult;       // the result of solving the target
 };
 
-static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
-static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );
+static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars );
+static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode );
 
 // some external procedures
 extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
@@ -67,11 +67,11 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
   SeeAlso     []
 
 ***********************************************************************/
-CSAT_Manager CSAT_InitManager()
+ABC_Manager ABC_InitManager()
 {
-    CSAT_Manager_t * mng;
-    mng = ALLOC( CSAT_Manager_t, 1 );
-    memset( mng, 0, sizeof(CSAT_Manager_t) );
+    ABC_Manager_t * mng;
+    mng = ALLOC( ABC_Manager_t, 1 );
+    memset( mng, 0, sizeof(ABC_Manager_t) );
     mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
     mng->pNtk->pName = util_strsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
@@ -93,7 +93,7 @@ CSAT_Manager CSAT_InitManager()
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_QuitManager( CSAT_Manager mng )
+void ABC_QuitManager( ABC_Manager mng )
 {
     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
@@ -116,15 +116,15 @@ void CSAT_QuitManager( CSAT_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
+void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option )
 {
     mng->mode = option;
     if ( option == 0 )
-        printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" );
+        printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" );
     else if ( option == 1 )
-        printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
+        printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
     else
-        printf( "CSAT_SetSolveOption: Unknown solving mode.\n" );
+        printf( "ABC_SetSolveOption: Unknown solving mode.\n" );
 }
 
 
@@ -143,7 +143,7 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
   SeeAlso     []
 
 ***********************************************************************/
-int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
+int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
 {
     Abc_Obj_t * pObj, * pFanin;
     char * pSop;
@@ -151,82 +151,82 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
 
     switch( type )
     {
-    case CSAT_BPI:
-    case CSAT_BPPI:
+    case ABC_BPI:
+    case ABC_BPPI:
         if ( nofi != 0 )
-            { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
+            { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
         // create the PI
         pObj = Abc_NtkCreatePi( mng->pNtk );
         stmm_insert( mng->tNode2Name, (char *)pObj, name );
         break;
-    case CSAT_CONST:
-    case CSAT_BAND:
-    case CSAT_BNAND:
-    case CSAT_BOR:
-    case CSAT_BNOR:
-    case CSAT_BXOR:
-    case CSAT_BXNOR:
-    case CSAT_BINV:
-    case CSAT_BBUF:
+    case ABC_CONST:
+    case ABC_BAND:
+    case ABC_BNAND:
+    case ABC_BOR:
+    case ABC_BNOR:
+    case ABC_BXOR:
+    case ABC_BXNOR:
+    case ABC_BINV:
+    case ABC_BBUF:
         // create the node
         pObj = Abc_NtkCreateNode( mng->pNtk );
         // create the fanins
         for ( i = 0; i < nofi; i++ )
         {
             if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
-                { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
+                { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
             Abc_ObjAddFanin( pObj, pFanin );
         }
         // create the node function
         switch( type )
         {
-            case CSAT_CONST:
+            case ABC_CONST:
                 if ( nofi != 0 )
-                    { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
                 break;
-            case CSAT_BAND:
+            case ABC_BAND:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
                 break;
-            case CSAT_BNAND:
+            case ABC_BNAND:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
                 break;
-            case CSAT_BOR:
+            case ABC_BOR:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
                 break;
-            case CSAT_BNOR:
+            case ABC_BNOR:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
                 break;
-            case CSAT_BXOR:
+            case ABC_BXOR:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
-                    { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi );
                 break;
-            case CSAT_BXNOR:
+            case ABC_BXNOR:
                 if ( nofi < 1 )
-                    { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
-                    { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi );
                 break;
-            case CSAT_BINV:
+            case ABC_BINV:
                 if ( nofi != 1 )
-                    { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
                 pSop = Abc_SopCreateInv( mng->pNtk->pManFunc );
                 break;
-            case CSAT_BBUF:
+            case ABC_BBUF:
                 if ( nofi != 1 )
-                    { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+                    { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
                 pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
                 break;
             default :
@@ -234,24 +234,24 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
         }
         Abc_ObjSetData( pObj, pSop );
         break;
-    case CSAT_BPPO:
-    case CSAT_BPO:
+    case ABC_BPPO:
+    case ABC_BPO:
         if ( nofi != 1 )
-            { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+            { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
         // create the PO
         pObj = Abc_NtkCreatePo( mng->pNtk );
         stmm_insert( mng->tNode2Name, (char *)pObj, name );
         // connect to the PO fanin
         if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
-            { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
+            { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
         Abc_ObjAddFanin( pObj, pFanin );
         break;
     default:
-        printf( "CSAT_AddGate: Unknown gate type.\n" );
+        printf( "ABC_AddGate: Unknown gate type.\n" );
         break;
     }
     if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
-        { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
+        { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
     return 1;
 }
 
@@ -267,7 +267,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
   SeeAlso     []
 
 ***********************************************************************/
-int CSAT_Check_Integrity( CSAT_Manager mng )
+int ABC_Check_Integrity( ABC_Manager mng )
 {
     Abc_Ntk_t * pNtk = mng->pNtk;
     Abc_Obj_t * pObj;
@@ -276,15 +276,15 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
     // this procedure also finalizes construction of the ABC network
     Abc_NtkFixNonDrivenNets( pNtk );
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
+        Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) );
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
+        Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     // make sure everything is okay with the network structure
     if ( !Abc_NtkDoCheck( pNtk ) )
     {
-        printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
+        printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
         return 0;
     }
 
@@ -295,7 +295,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
             continue;
         if ( Abc_ObjFanoutNum(pObj) == 0 )
         {
-            printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );
+            printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
             return 0;
         }
     }
@@ -313,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
+void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
 {
     mng->nSeconds = runtime;
 }
@@ -329,9 +329,9 @@ void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
+void ABC_SetLearnLimit( ABC_Manager mng, int num )
 {
-    printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+    printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -345,9 +345,9 @@ void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
+void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
 {
-    printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
+    printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -361,9 +361,9 @@ void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
+void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
 {
-    printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -377,7 +377,7 @@ void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
+void ABC_EnableDump( ABC_Manager mng, char * dump_file )
 {
     FREE( mng->pDumpFileName );
     mng->pDumpFileName = util_strsav( dump_file );
@@ -398,12 +398,12 @@ void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
   SeeAlso     []
 
 ***********************************************************************/
-int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
+int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values )
 {
     Abc_Obj_t * pObj;
     int i;
     if ( nog < 1 )
-        { printf( "CSAT_AddTarget: The target has no gates.\n" ); return 0; }
+        { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; }
     // clear storage for the target
     mng->nog = 0;
     Vec_PtrClear( mng->vNodes );
@@ -412,10 +412,10 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
     for ( i = 0; i < nog; i++ )
     {
         if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
-            { printf( "CSAT_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
+            { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
         Vec_PtrPush( mng->vNodes, pObj );
         if ( values[i] < 0 || values[i] > 1 )
-            { printf( "CSAT_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
+            { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
         Vec_IntPush( mng->vValues, values[i] );
     }
     mng->nog = nog;
@@ -427,14 +427,14 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
   Synopsis    [Initialize the solver internal data structure.]
 
   Description [Prepares the solver to work on one specific target
-  set by calling CSAT_AddTarget before.]
+  set by calling ABC_AddTarget before.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_SolveInit( CSAT_Manager mng )
+void ABC_SolveInit( ABC_Manager mng )
 {
     Fraig_Params_t * pParams = &mng->Params;
     int nWords1, nWords2, nWordsMin;
@@ -442,7 +442,7 @@ void CSAT_SolveInit( CSAT_Manager mng )
     // check if the target is available
     assert( mng->nog == Vec_PtrSize(mng->vNodes) );
     if ( mng->nog == 0 )
-        { printf( "CSAT_SolveInit: Target is not specified by CSAT_AddTarget().\n" ); return; }
+        { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
 
     // free the previous target network if present
     if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
@@ -485,13 +485,13 @@ void CSAT_SolveInit( CSAT_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_AnalyzeTargets( CSAT_Manager mng )
+void ABC_AnalyzeTargets( ABC_Manager mng )
 {
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Solves the targets added by CSAT_AddTarget().]
+  Synopsis    [Solves the targets added by ABC_AddTarget().]
 
   Description []
                
@@ -500,7 +500,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
+enum ABC_StatusT ABC_Solve( ABC_Manager mng )
 {
     Fraig_Man_t * pMan;
     Abc_Ntk_t * pCnf;
@@ -509,7 +509,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
 
     // check if the target network is available
     if ( mng->pTarget == NULL )
-        { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; }
+        { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
 
     // optimizations of the target go here
     // for example, to enable one pass of rewriting, uncomment this line
@@ -522,7 +522,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
         RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );
 
         // analyze the result
-        mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+        mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
         if ( RetValue == -1 )
             mng->pResult->status = UNDETERMINED;
         else if ( RetValue == 1 )
@@ -533,7 +533,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
             // create the array of PI names and values
             for ( i = 0; i < mng->pResult->no_sig; i++ )
             {
-                mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+                mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
                 mng->pResult->values[i] = pCnf->pModel[i];
             }
             FREE( mng->pTarget->pModel );
@@ -549,7 +549,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
         RetValue = Fraig_ManCheckMiter( pMan );
 
         // analyze the result
-        mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+        mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
         if ( RetValue == -1 )
             mng->pResult->status = UNDETERMINED;
         else if ( RetValue == 1 )
@@ -562,7 +562,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
             // create the array of PI names and values
             for ( i = 0; i < mng->pResult->no_sig; i++ )
             {
-                mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+                mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
                 mng->pResult->values[i] = pModel[i];
             }
         }
@@ -584,14 +584,14 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
 
   Synopsis    [Gets the solve status of a target.]
 
-  Description [TargetID: the target id returned by CSAT_AddTarget().]
+  Description [TargetID: the target id returned by ABC_AddTarget().]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
+ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
 {
     return mng->pResult;
 }
@@ -607,7 +607,7 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_Dump_Bench_File( CSAT_Manager mng )
+void ABC_Dump_Bench_File( ABC_Manager mng )
 {
     Abc_Ntk_t * pNtkTemp, * pNtkAig;
     char * pFileName;
@@ -617,7 +617,7 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng )
     pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig );
     Abc_NtkDelete( pNtkAig );
     if ( pNtkTemp == NULL ) 
-        { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
+        { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
     pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
     Io_WriteBench( pNtkTemp, pFileName );
     Abc_NtkDelete( pNtkTemp );
@@ -636,11 +636,11 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
+ABC_Target_ResultT * ABC_TargetResAlloc( int nVars )
 {
-    CSAT_Target_ResultT * p;
-    p = ALLOC( CSAT_Target_ResultT, 1 );
-    memset( p, 0, sizeof(CSAT_Target_ResultT) );
+    ABC_Target_ResultT * p;
+    p = ALLOC( ABC_Target_ResultT, 1 );
+    memset( p, 0, sizeof(ABC_Target_ResultT) );
     p->no_sig = nVars;
     p->names = ALLOC( char *, nVars );
     p->values = ALLOC( int, nVars );
@@ -660,7 +660,7 @@ CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void CSAT_TargetResFree( CSAT_Target_ResultT * p )
+void ABC_TargetResFree( ABC_Target_ResultT * p )
 {
     if ( p == NULL )
         return;
@@ -680,7 +680,7 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p )
   SeeAlso     []
 
 ***********************************************************************/
-char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode )
+char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode )
 {
     char * pName = NULL;
     if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index e567241f..3e04c7df 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -16,8 +16,8 @@
 
 ***********************************************************************/
 
-#ifndef __CSAT_APIS_H__
-#define __CSAT_APIS_H__
+#ifndef __ABC_APIS_H__
+#define __ABC_APIS_H__
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
@@ -32,37 +32,37 @@
 ////////////////////////////////////////////////////////////////////////
 
 
-typedef struct CSAT_ManagerStruct_t     CSAT_Manager_t;
-typedef struct CSAT_ManagerStruct_t *   CSAT_Manager;
+typedef struct ABC_ManagerStruct_t     ABC_Manager_t;
+typedef struct ABC_ManagerStruct_t *   ABC_Manager;
 
 
 // GateType defines the gate type that can be added to circuit by
-// CSAT_AddGate();
-#ifndef _CSAT_GATE_TYPE_
-#define _CSAT_GATE_TYPE_
+// ABC_AddGate();
+#ifndef _ABC_GATE_TYPE_
+#define _ABC_GATE_TYPE_
 enum GateType
 {
-    CSAT_CONST = 0,  // constant gate
-    CSAT_BPI,        // boolean PI
-    CSAT_BPPI,       // bit level PSEUDO PRIMARY INPUT
-    CSAT_BAND,       // bit level AND
-    CSAT_BNAND,      // bit level NAND
-    CSAT_BOR,        // bit level OR
-    CSAT_BNOR,       // bit level NOR
-    CSAT_BXOR,       // bit level XOR
-    CSAT_BXNOR,      // bit level XNOR
-    CSAT_BINV,       // bit level INVERTER
-    CSAT_BBUF,       // bit level BUFFER
-    CSAT_BPPO,       // bit level PSEUDO PRIMARY OUTPUT
-    CSAT_BPO         // boolean PO
+    ABC_CONST = 0,  // constant gate
+    ABC_BPI,        // boolean PI
+    ABC_BPPI,       // bit level PSEUDO PRIMARY INPUT
+    ABC_BAND,       // bit level AND
+    ABC_BNAND,      // bit level NAND
+    ABC_BOR,        // bit level OR
+    ABC_BNOR,       // bit level NOR
+    ABC_BXOR,       // bit level XOR
+    ABC_BXNOR,      // bit level XNOR
+    ABC_BINV,       // bit level INVERTER
+    ABC_BBUF,       // bit level BUFFER
+    ABC_BPPO,       // bit level PSEUDO PRIMARY OUTPUT
+    ABC_BPO         // boolean PO
 };
 #endif
 
 
-//CSAT_StatusT defines the return value by CSAT_Solve();
-#ifndef _CSAT_STATUS_
-#define _CSAT_STATUS_
-enum CSAT_StatusT 
+//ABC_StatusT defines the return value by ABC_Solve();
+#ifndef _ABC_STATUS_
+#define _ABC_STATUS_
+enum ABC_StatusT 
 {
     UNDETERMINED = 0,
     UNSATISFIABLE,
@@ -76,11 +76,11 @@ enum CSAT_StatusT
 #endif
 
 
-// CSAT_OptionT defines the solver option about learning
-// which is used by CSAT_SetSolveOption();
-#ifndef _CSAT_OPTION_
-#define _CSAT_OPTION_
-enum CSAT_OptionT
+// ABC_OptionT defines the solver option about learning
+// which is used by ABC_SetSolveOption();
+#ifndef _ABC_OPTION_
+#define _ABC_OPTION_
+enum ABC_OptionT
 {
     BASE_LINE = 0,
     IMPLICT_LEARNING, //default
@@ -89,12 +89,12 @@ enum CSAT_OptionT
 #endif
 
 
-#ifndef _CSAT_Target_Result
-#define _CSAT_Target_Result
-typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
-struct _CSAT_Target_ResultT
+#ifndef _ABC_Target_Result
+#define _ABC_Target_Result
+typedef struct _ABC_Target_ResultT ABC_Target_ResultT;
+struct _ABC_Target_ResultT
 {
-    enum CSAT_StatusT status; // solve status of the target
+    enum ABC_StatusT status; // solve status of the target
     int num_dec;              // num of decisions to solve the target
     int num_imp;              // num of implications to solve the target
     int num_cftg;             // num of conflict gates learned 
@@ -118,10 +118,10 @@ struct _CSAT_Target_ResultT
 ////////////////////////////////////////////////////////////////////////
 
 // create a new manager
-extern CSAT_Manager          CSAT_InitManager(void);
+extern ABC_Manager           ABC_InitManager(void);
 
 // set solver options for learning
-extern void                  CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
+extern void                  ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option);
 
 // add a gate to the circuit
 // the meaning of the parameters are:
@@ -129,7 +129,7 @@ extern void                  CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt
 // name: the name of the gate to be added, name should be unique in a circuit.
 // nofi: number of fanins of the gate to be added;
 // fanins: the name array of fanins of the gate to be added
-extern int                   CSAT_AddGate(CSAT_Manager mng,
+extern int                   ABC_AddGate(ABC_Manager mng,
                                       enum GateType type,
                                       char* name,
                                       int nofi,
@@ -138,38 +138,38 @@ extern int                   CSAT_AddGate(CSAT_Manager mng,
 
 // check if there are gates that are not used by any primary ouput.
 // if no such gates exist, return 1 else return 0;
-extern int                   CSAT_Check_Integrity(CSAT_Manager mng);
+extern int                   ABC_Check_Integrity(ABC_Manager mng);
 
 // set time limit for solving a target.
 // runtime: time limit (in second).
-extern void                  CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
-extern void                  CSAT_SetLearnLimit(CSAT_Manager mng, int num);
-extern void                  CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
-extern void                  CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
-extern void                  CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
+extern void                  ABC_SetTimeLimit(ABC_Manager mng, int runtime);
+extern void                  ABC_SetLearnLimit(ABC_Manager mng, int num);
+extern void                  ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num);
+extern void                  ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
+extern void                  ABC_EnableDump(ABC_Manager mng, char* dump_file);
 
 // the meaning of the parameters are:
 // nog: number of gates that are in the targets
 // names: name array of gates
 // values: value array of the corresponding gates given in "names" to be
 // solved. the relation of them is AND.
-extern int                   CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
+extern int                   ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values);
 
 // initialize the solver internal data structure.
-extern void                  CSAT_SolveInit(CSAT_Manager mng);
-extern void                  CSAT_AnalyzeTargets(CSAT_Manager mng);
+extern void                  ABC_SolveInit(ABC_Manager mng);
+extern void                  ABC_AnalyzeTargets(ABC_Manager mng);
 
-// solve the targets added by CSAT_AddTarget()
-extern enum CSAT_StatusT     CSAT_Solve(CSAT_Manager mng);
+// solve the targets added by ABC_AddTarget()
+extern enum ABC_StatusT      ABC_Solve(ABC_Manager mng);
 
 // get the solve status of a target
-// TargetID: the target id returned by  CSAT_AddTarget().
-extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
-extern void                  CSAT_Dump_Bench_File(CSAT_Manager mng);
+// TargetID: the target id returned by  ABC_AddTarget().
+extern ABC_Target_ResultT *  ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
+extern void                  ABC_Dump_Bench_File(ABC_Manager mng);
 
 // ADDED PROCEDURES:
-extern void                  CSAT_QuitManager( CSAT_Manager mng );
-extern void                  CSAT_TargetResFree( CSAT_Target_ResultT * p );
+extern void                  ABC_QuitManager( ABC_Manager mng );
+extern void                  ABC_TargetResFree( ABC_Target_ResultT * p );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c
index 7dc46430..500431c6 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 40aa223b..30bf4a96 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;