23 files changed, 1078 insertions, 184 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index c2b739b5..f8871ba9 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -1065,6 +1065,11 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
+        return 1;
+    }
 
     // modify the current network
     Abc_NtkCleanup( pNtk, 0 );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 200d2501..2366aa10 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -406,6 +406,7 @@ extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -532,10 +533,13 @@ extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
+extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
+extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
 extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
@@ -559,6 +563,7 @@ extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_Obj_t *        Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
 extern int                Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d42fdac0..2200bea1 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -172,6 +172,10 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
         Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
         Abc_ObjSetFaninL1( pObj->pCopy, Abc_ObjFaninL1(pObj) );
     }
+    // relink the choice nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( pObj->pData )
+            pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
     Vec_PtrFree( vNodes );
     // relink the CO nodes
     Abc_NtkForEachCo( pMan->pNtkAig, pObj, i )
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index ee77cd02..e8b00271 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -361,7 +361,8 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
 bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin, * pFanout;
-    int i, k, Value = 1;
+    int i, Value = 1;
+//    int k;
 
     // check the network
     if ( pObj->pNtk != pNtk )
@@ -395,7 +396,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
-
+/*
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -417,7 +418,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
             }
-
+*/
     return Value;
 }
 
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9f192979..7de9ea3e 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -333,7 +333,64 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
 
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
+    int i;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    
+    // start the network
+    Abc_NtkCleanCopy( pNtk );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkNew->pName = util_strsav(pNtk->pName);
+
+    // collect the nodes in the TFI of the output
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
+    Vec_PtrFree( vNodes );
+
+    // add the PO
+    pFinal = Abc_AigConst1( pNtkNew->pManFunc );
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        pOther = pObj->pCopy;
+        if ( Vec_IntEntry(vValues, i) == 0 )
+            pOther = Abc_ObjNot(pOther);
+        pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
+    }
+
+    // add the PO corresponding to this output
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pFinal );
+    Abc_NtkLogicStoreName( pNodePo, "miter" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index c0eb1c0a..724c3877 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -89,7 +89,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     ProgressBar * pProgress;
     Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1;
+    Abc_Obj_t * pNode, * pConst1, * pReset;
     int i;
 
     assert( Abc_NtkIsAig(pNtk) );
@@ -102,6 +102,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
+    pReset  = Abc_AigReset( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -111,6 +112,8 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
+        else if ( pNode == pReset )
+            continue;
         else
             pNodeFraig = Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index bfa41842..8e10b391 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -254,23 +254,26 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         if ( !Abc_NodeIsAigChoice(pObj) )
             continue;
         // create an OR gate
-        pNodeNew = Abc_NtkCreateNode(pNtk);
+        pNodeNew = Abc_NtkCreateNode(pNtkNew);
         // add fanins
         Vec_IntClear( pNtk->vIntTemp );
-        for ( k = 0, pFanin = pObj; pFanin; pFanin = pFanin->pData, k++ )
+        for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
         {
             Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOr( pNtk->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
         // set the new node
-        pObj->pCopy = pNodeNew;
+        pObj->pCopy->pCopy = pNodeNew;
     }
     // connect the internal nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+            if ( pFanin->pCopy->pCopy )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // connect the COs
     Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index b6972d58..28e92889 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -92,7 +92,39 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 1\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 0\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AND2 cover.]
 
   Description []
                
@@ -115,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input AND cover.]
 
   Description []
                
@@ -136,7 +168,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input NAND cover.]
 
   Description []
                
@@ -158,7 +190,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
 
   Description []
                
@@ -180,7 +212,32 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+{
+    char * pSop, * pCube;
+    int i;
+    pSop = Abc_SopStart( pMan, nVars, nVars );
+    i = 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        pCube[i] = '1' - (pfCompl? pfCompl[i] : 0);
+        i++;
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the multi-input NOR cover.]
 
   Description []
                
@@ -201,7 +258,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XOR cover.]
 
   Description []
                
@@ -218,7 +275,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XNOR cover.]
 
   Description []
                
@@ -235,7 +292,7 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the inv cover.]
 
   Description []
                
@@ -251,7 +308,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the buf cover.]
 
   Description []
                
@@ -367,18 +424,11 @@ int Abc_SopGetPhase( char * pSop )
 int Abc_SopGetIthCareLit( char * pSop, int i )
 {
     char * pCube;
-    int nVars, c;
+    int nVars;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
-    {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
-        // get the literal
+    Abc_SopForEachCube( pSop, nVars, pCube )
         if ( pCube[i] != '-' )
             return pCube[i] - '0';
-    }
     return -1;
 }
 
@@ -520,6 +570,8 @@ bool Abc_SopIsAndType( char * pSop )
     for ( pCur = pSop; *pCur != ' '; pCur++ )
         if ( *pCur == '-' )
             return 0;
+    if ( pCur[1] != '1' )
+        return 0;
     return 1;
 }
 
@@ -537,14 +589,12 @@ bool Abc_SopIsAndType( char * pSop )
 bool Abc_SopIsOrType( char * pSop )
 {
     char * pCube, * pCur;
-    int nVars, nLits, c;
+    int nVars, nLits;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
+    if ( nVars != Abc_SopGetCubeNum(pSop) )
+        return 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
     {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
         // count the number of literals in the cube
         nLits = 0;
         for ( pCur = pCube; *pCur != ' '; pCur++ )
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 961e6c5f..bf97c5bf 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -28,7 +28,6 @@
 
 // static functions
 static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
-static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index aa15c0af..255791a7 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -335,7 +335,7 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
     int i, num;
     int size;
     int c;
-    num = 30;
+    num = 50;
 
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index ed1e929d..a3fd979a 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -209,7 +209,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-    
+     
     // if the memory should be freed, quit packages
     if ( fStatus == -2 ) 
     {
diff --git a/src/csat_apis.h b/src/csat_apis.h
deleted file mode 100644
index 0b009167..00000000
--- a/src/csat_apis.h
+++ /dev/null
@@ -1,125 +0,0 @@
-//These are the APIs, enums and data structures that we use 
-//and expect from our use of CSAT.
-
-enum GateType
-{
-// GateType defines the gate type that can be added to circuit by
-// CSAT_AddGate();
-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
-};
-#endif
-
-//CSAT_StatusT defines the return value by CSAT_Solve();
-#ifndef _CSAT_STATUS_
-#define _CSAT_STATUS_
-enum CSAT_StatusT 
-{
-UNDETERMINED = 0,
-UNSATISFIABLE,
-SATISFIABLE,
-TIME_OUT,
-FRAME_OUT,
-NO_TARGET,
-ABORTED,
-SEQ_SATISFIABLE        
-};
-#endif
-
-
-// CSAT_OptionT defines the solver option about learning
-// which is used by CSAT_SetSolveOption();
-#ifndef _CSAT_OPTION_
-#define _CSAT_OPTION_
-enum CSAT_OptionT
-{
-BASE_LINE = 0,
-IMPLICT_LEARNING, //default
-EXPLICT_LEARNING
-};
-#endif
-
-#ifndef _CSAT_Target_Result
-#define _CSAT_Target_Result
-typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
-/*
-struct _CSAT_Target_ResultT
-{
-enum CSAT_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 
-int num_cfts;    //num of conflict signals in conflict gates
-double time;    //time(in second) used to solver the target
-int no_sig;        // if "status" is SATISFIABLE, "no_sig" is the number of 
-                // primary inputs, if the "status" is TIME_OUT, "no_sig" is the
-                // number of constant signals found.
-char** names;    // if the "status" is SATISFIABLE, "names" is the name array of
-                // primary inputs, "values" is the value array of primary 
-                // inputs that satisfy the target. 
-                // if the "status" is TIME_OUT, "names" is the name array of
-                // constant signals found (signals at the root of decision 
-                // tree),"values" is the value array of constant signals found.
-int* values;
-};
-*/
-
-// create a new manager
-CSAT_Manager CSAT_InitManager(void);
-
-// set solver options for learning
-void CSAT_SetSolveOption(CSAT_Manager mng,enum CSAT_OptionT option);
-
-// add a gate to the circuit
-// the meaning of the parameters are:
-// type: the type of the gate to be added
-// 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
-int CSAT_AddGate(CSAT_Manager mng,
-            enum GateType type,
-            char* name,
-            int nofi,
-            char** fanins,
-            int dc_attr=0);
-
-// check if there are gates that are not used by any primary ouput.
-// if no such gates exist, return 1 else return 0;
-int CSAT_Check_Integrity(CSAT_Manager mng);
-
-// set time limit for solving a target.
-// runtime: time limit (in second).
-void CSAT_SetTimeLimit(CSAT_Manager mng ,int runtime);
-void CSAT_SetLearnLimit   (CSAT_Manager mng ,int num);
-void CSAT_SetSolveBacktrackLimit   (CSAT_Manager mng ,int num);
-void CSAT_SetLearnBacktrackLimit   (CSAT_Manager mng ,int num);
-void CSAT_EnableDump(CSAT_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.
-int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
-// initialize the solver internal data structure.
-void CSAT_SolveInit(CSAT_Manager mng);
-void CSAT_AnalyzeTargets(CSAT_Manager mng);
-// solve the targets added by CSAT_AddTarget()
-enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
-// get the solve status of a target
-// TargetID: the target id returned by  CSAT_AddTarget().
-CSAT_Target_ResultT*
-CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
-void CSAT_Dump_Bench_File(CSAT_Manager mng);
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 6e127b27..1c291b33 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -125,7 +125,6 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
 extern void              Rwr_ManStop( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
-extern void              Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *       Rwr_ManReadFanins( Rwr_Man_t * p );
 extern Vec_Int_t *       Rwr_ManReadDecs( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 71db4b20..d4772812 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -164,27 +164,6 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns elementary cuts to the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    // save the fanout counters for all internal nodes
-//    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
-    // precompute the required times for all internal nodes
-//    p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
-    // start the cut computation
-//    Rwr_NtkStartCuts( p, pNtk );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Stops the resynthesis manager.]
 
   Description []
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
new file mode 100644
index 00000000..eddd7270
--- /dev/null
+++ b/src/sat/csat/csat_apis.c
@@ -0,0 +1,630 @@
+/**CFile****************************************************************
+
+  FileName    [csat_apis.h]
+
+  PackageName [Interface to CSAT.]
+
+  Synopsis    [APIs, enums, and data structures expected from the use of CSAT.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 28, 2005]
+
+  Revision    [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "csat_apis.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct CSAT_ManagerStruct_t
+{
+    // information about the problem
+    stmm_table *          tName2Node;    // the hash table mapping names to nodes
+    Abc_Ntk_t *           pNtk;          // the starting ABC network
+    Abc_Ntk_t *           pTarget;       // the AIG of the target
+    char *                pDumpFileName; // the name of the file to dump the target network
+    // solving parameters
+    int                   mode;          // 0 = baseline;  1 = resource-aware fraiging
+    Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
+    // information about the target 
+    int                   nog;           // the numbers of gates in the target
+    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
+};
+
+static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
+static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
+
+// some external procedures
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Manager CSAT_InitManager()
+{
+    CSAT_Manager_t * mng;
+    mng = ALLOC( CSAT_Manager_t, 1 );
+    memset( mng, 0, sizeof(CSAT_Manager_t) );
+    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC_SOP );
+    mng->pNtk->pName = util_strsav("csat_network");
+    mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
+    mng->vNodes  = Vec_PtrAlloc( 100 );
+    mng->vValues = Vec_IntAlloc( 100 );
+    return mng;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_QuitManager( CSAT_Manager mng )
+{
+    if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
+    if ( mng->pNtk )       Abc_NtkDelete( mng->pNtk );
+    if ( mng->pTarget )    Abc_NtkDelete( mng->pTarget );
+    if ( mng->vNodes )     Vec_PtrFree( mng->vNodes );
+    if ( mng->vValues )    Vec_IntFree( mng->vValues );
+    FREE( mng->pDumpFileName );
+    free( mng );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets solver options for learning.]
+
+  Description [0 = baseline; 1 = resource-aware solving.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
+{
+    mng->mode = option;
+    if ( option == 0 )
+        printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" );
+    else if ( option == 1 )
+        printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" );
+    else
+        printf( "CSAT_SetSolveOption: Unknown option.\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a gate to the circuit.]
+
+  Description [The meaning of the parameters are:
+    type: the type of the gate to be added
+    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.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    char * pSop;
+    int i;
+
+    switch( type )
+    {
+    case CSAT_BPI:
+    case CSAT_BPPI:
+        if ( nofi != 0 )
+            { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
+        // create the PI
+        pObj = Abc_NtkCreatePi( mng->pNtk );
+        pObj->pNext = (Abc_Obj_t *)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:
+        // 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; }
+            Abc_ObjAddFanin( pObj, pFanin );
+        }
+        // create the node function
+        switch( type )
+        {
+            case CSAT_CONST:
+                if ( nofi != 0 )
+                    { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
+                break;
+            case CSAT_BAND:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BNAND:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
+                break;
+            case CSAT_BNOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BXOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_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; }
+                pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BXNOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_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; }
+                pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BINV:
+                if ( nofi != 1 )
+                    { printf( "CSAT_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:
+                if ( nofi != 1 )
+                    { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+                pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
+                break;
+            default :
+                break;
+        }
+        Abc_ObjSetData( pObj, pSop );
+        break;
+    case CSAT_BPPO:
+    case CSAT_BPO:
+        if ( nofi != 1 )
+            { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+        // create the PO
+        pObj = Abc_NtkCreatePo( mng->pNtk );
+        pObj->pNext = (Abc_Obj_t *)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; }
+        Abc_ObjAddFanin( pObj, pFanin );
+        break;
+    default:
+        printf( "CSAT_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; }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks integraty of the manager.]
+
+  Description [Checks if there are gates that are not used by any primary output.
+  If no such gates exist, return 1 else return 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_Check_Integrity( CSAT_Manager mng )
+{
+    Abc_Ntk_t * pNtk = mng->pNtk;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // this procedure also finalizes construction of the ABC network
+    Abc_NtkFixNonDrivenNets( pNtk );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
+        return 0;
+    }
+
+    // check that there is no dangling nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+        {
+            printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets time limit for solving a target.]
+
+  Description [Runtime: time limit (in second).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
+{
+    printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the file name to dump the structurally hashed network used for solving.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
+{
+    FREE( mng->pDumpFileName );
+    mng->pDumpFileName = util_strsav( dump_file );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a new target to the manager.]
+
+  Description [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.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_AddTarget( CSAT_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; }
+    // clear storage for the target
+    mng->nog = 0;
+    Vec_PtrClear( mng->vNodes );
+    Vec_IntClear( mng->vValues );
+    // save the target
+    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; }
+        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; }
+        Vec_IntPush( mng->vValues, values[i] );
+    }
+    mng->nog = nog;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initialize the solver internal data structure.]
+
+  Description [Prepares the solver to work on one specific target
+  set by calling CSAT_AddTarget before.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SolveInit( CSAT_Manager mng )
+{
+    Fraig_Params_t * pParams = &mng->Params;
+    int nWords1, nWords2, nWordsMin;
+
+    // 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; }
+
+    // free the previous target network if present
+    if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
+
+    // set the new target network
+    mng->pTarget = Abc_NtkCreateCone( mng->pNtk, mng->vNodes, mng->vValues );
+
+    // to determine the number of simulation patterns
+    // use the following strategy
+    // at least 64 words (32 words random and 32 words dynamic)
+    // no more than 256M for one circuit (128M + 128M)
+    nWords1 = 32;
+    nWords2 = (1<<27) / (Abc_NtkNodeNum(mng->pTarget) + Abc_NtkCiNum(mng->pTarget));
+    nWordsMin = ABC_MIN( nWords1, nWords2 );
+
+    // set parameters for fraiging
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
+    pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
+    pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
+    pParams->nBTLimit   = 99;             // the max number of backtracks to perform at a node
+    pParams->fFuncRed   = mng->mode;      // performs only one level hashing
+    pParams->fFeedBack  = 1;              // enables solver feedback
+    pParams->fDist1Pats = 1;              // enables distance-1 patterns
+    pParams->fDoSparse  = 0;              // performs equiv tests for sparse functions 
+    pParams->fChoicing  = 0;              // enables recording structural choices
+    pParams->fTryProve  = 1;              // tries to solve the final miter
+    pParams->fVerbose   = 0;              // the verbosiness flag
+    pParams->fVerboseP  = 0;              // the verbosiness flag for proof reporting
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Currently not implemented.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_AnalyzeTargets( CSAT_Manager mng )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the targets added by CSAT_AddTarget().]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
+{
+    Fraig_Man_t * pMan;
+    int * pModel;
+    int RetValue, i;
+
+    // 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; }
+
+    // transform the target into a fraig
+    pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
+    Fraig_ManProveMiter( pMan );
+
+    // analyze the result
+    mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+    RetValue = Fraig_ManCheckMiter( pMan );
+    if ( RetValue == -1 )
+        mng->pResult->status = UNDETERMINED;
+    else if ( RetValue == 1 )
+        mng->pResult->status = UNSATISFIABLE;
+    else if ( RetValue == 0 )
+    {
+        mng->pResult->status = SATISFIABLE;
+        pModel = Fraig_ManReadModel( pMan );
+        assert( pModel != NULL );
+        // create the array of PI names and values
+        for ( i = 0; i < mng->pResult->no_sig; i++ )
+        {
+            mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given
+            mng->pResult->values[i] = pModel[i];
+        }
+    }
+    else 
+        assert( 0 );
+
+    // delete the fraig manager
+    Fraig_ManFree( pMan );
+    // delete the target
+    Abc_NtkDelete( mng->pTarget );
+    mng->pTarget = NULL;
+    // return the status
+    return mng->pResult->status;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the solve status of a target.]
+
+  Description [TargetID: the target id returned by CSAT_AddTarget().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
+{
+    return mng->pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumps the target AIG into the BENCH file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_Dump_Bench_File( CSAT_Manager mng )
+{
+    Abc_Ntk_t * pNtkTemp;
+    char * pFileName;
+
+    // derive the netlist
+    pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget );
+    if ( pNtkTemp == NULL ) 
+        { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
+    pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
+    Io_WriteBench( pNtkTemp, pFileName );
+    Abc_NtkDelete( pNtkTemp );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the target result.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
+{
+    CSAT_Target_ResultT * p;
+    p = ALLOC( CSAT_Target_ResultT, 1 );
+    memset( p, 0, sizeof(CSAT_Target_ResultT) );
+    p->no_sig = nVars;
+    p->names = ALLOC( char *, nVars );
+    p->values = ALLOC( int, nVars );
+    memset( p->names, 0, sizeof(char *) * nVars );
+    memset( p->values, 0, sizeof(int) * nVars );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the target result.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_TargetResFree( CSAT_Target_ResultT * p )
+{
+    if ( p == NULL )
+        return;
+    FREE( p->names );
+    FREE( p->values );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
new file mode 100644
index 00000000..124ca266
--- /dev/null
+++ b/src/sat/csat/csat_apis.h
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [csat_apis.h]
+
+  PackageName [Interface to CSAT.]
+
+  Synopsis    [APIs, enums, and data structures expected from the use of CSAT.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 28, 2005]
+
+  Revision    [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CSAT_APIS_H__
+#define __CSAT_APIS_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct CSAT_ManagerStruct_t     CSAT_Manager_t;
+typedef struct CSAT_ManagerStruct_t *   CSAT_Manager;
+
+
+// GateType defines the gate type that can be added to circuit by
+// CSAT_AddGate();
+#ifndef _CSAT_GATE_TYPE_
+#define _CSAT_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
+};
+#endif
+
+
+//CSAT_StatusT defines the return value by CSAT_Solve();
+#ifndef _CSAT_STATUS_
+#define _CSAT_STATUS_
+enum CSAT_StatusT 
+{
+    UNDETERMINED = 0,
+    UNSATISFIABLE,
+    SATISFIABLE,
+    TIME_OUT,
+    FRAME_OUT,
+    NO_TARGET,
+    ABORTED,
+    SEQ_SATISFIABLE     
+};
+#endif
+
+
+// CSAT_OptionT defines the solver option about learning
+// which is used by CSAT_SetSolveOption();
+#ifndef _CSAT_OPTION_
+#define _CSAT_OPTION_
+enum CSAT_OptionT
+{
+    BASE_LINE = 0,
+    IMPLICT_LEARNING, //default
+    EXPLICT_LEARNING
+};
+#endif
+
+
+#ifndef _CSAT_Target_Result
+#define _CSAT_Target_Result
+typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
+struct _CSAT_Target_ResultT
+{
+    enum CSAT_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 
+    int num_cfts;             // num of conflict signals in conflict gates
+    double time;              // time(in second) used to solve the target
+    int no_sig;               // if "status" is SATISFIABLE, "no_sig" is the number of 
+                              // primary inputs, if the "status" is TIME_OUT, "no_sig" is the
+                              // number of constant signals found.
+    char** names;             // if the "status" is SATISFIABLE, "names" is the name array of
+                              // primary inputs, "values" is the value array of primary 
+                              // inputs that satisfy the target. 
+                              // if the "status" is TIME_OUT, "names" is the name array of
+                              // constant signals found (signals at the root of decision 
+                              // tree), "values" is the value array of constant signals found.
+    int* values;
+};
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// create a new manager
+extern CSAT_Manager          CSAT_InitManager(void);
+
+// set solver options for learning
+extern void                  CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
+
+// add a gate to the circuit
+// the meaning of the parameters are:
+// type: the type of the gate to be added
+// 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,
+                                      enum GateType type,
+                                      char* name,
+                                      int nofi,
+                                      char** fanins,
+                                      int dc_attr);
+
+// 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);
+
+// 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);
+
+// 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);
+
+// initialize the solver internal data structure.
+extern void                  CSAT_SolveInit(CSAT_Manager mng);
+extern void                  CSAT_AnalyzeTargets(CSAT_Manager mng);
+
+// solve the targets added by CSAT_AddTarget()
+extern enum CSAT_StatusT     CSAT_Solve(CSAT_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);
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 53a46584..946ed56b 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -97,6 +97,7 @@ extern int                 Fraig_ManReadFeedBack( Fraig_Man_t * p );
 extern int                 Fraig_ManReadDoSparse( Fraig_Man_t * p );      
 extern int                 Fraig_ManReadChoicing( Fraig_Man_t * p );      
 extern int                 Fraig_ManReadVerbose( Fraig_Man_t * p );       
+extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
 
 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@@ -157,6 +158,7 @@ extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );
 extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index d60c7168..0194f3b4 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -57,6 +57,7 @@ int               Fraig_ManReadFeedBack( Fraig_Man_t * p )                    {
 int               Fraig_ManReadDoSparse( Fraig_Man_t * p )                    { return p->fDoSparse;  }
 int               Fraig_ManReadChoicing( Fraig_Man_t * p )                    { return p->fChoicing;  }
 int               Fraig_ManReadVerbose( Fraig_Man_t * p )                     { return p->fVerbose;   }
+int *             Fraig_ManReadModel( Fraig_Man_t * p )                       { return p->pModel;     }
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 0a950aba..b46f6c41 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -765,6 +765,47 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
     p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Doubles the size of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
+{
+    int * pModel = NULL;
+    int iPattern;
+    int i;
+
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 );
+    if ( iPattern >= 0 )
+    {
+        pModel = ALLOC( int, p->vInputs->nSize );
+        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 );
+    if ( iPattern >= 0 )
+    {
+        pModel = ALLOC( int, p->vInputs->nSize );
+        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    return pModel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 1139bdc0..5f8b3496 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -178,6 +178,7 @@ struct Fraig_ManStruct_t_
     Msat_Solver_t *       pSat;          // the SAT solver
     Msat_IntVec_t *       vProj;         // the temporary array of projection vars 
     int                   nSatNums;      // the counter of SAT variables
+    int *                 pModel;        // the assignment, which satisfies the miter
     // these arrays belong to the solver
     Msat_IntVec_t *       vVarsInt;      // the temporary array of variables
     Msat_ClauseVec_t *    vAdjacents;    // the temporary storage for connectivity
@@ -378,6 +379,7 @@ extern void                Fraig_FeedBackInit( Fraig_Man_t * p );
 extern void                Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
+extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
@@ -404,6 +406,7 @@ extern Fraig_Node_t *      Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No
 extern void                Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern int                 Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
+extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern void                Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
 extern void                Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
 extern void                Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index d41f5d0b..65716340 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -171,6 +171,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
     if ( p->vProj )      Msat_IntVecFree( p->vProj );
     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
+    if ( p->pModel )     free( p->pModel );
 
     Fraig_MemFixedStop( p->mmNodes, 0 );
     Fraig_MemFixedStop( p->mmSims, 0 );
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index ba22cfad..13c09a9e 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -111,6 +111,31 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckMiter( Fraig_Man_t * p )
+{
+    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+        return 1;
+    // save the counter example
+    FREE( p->pModel );
+    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    // if the model is not found, return undecided
+    if ( p->pModel == NULL )
+        return -1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Checks whether two nodes are functinally equivalent.]
 
   Description [The flag (fComp) tells whether the nodes to be checked
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 5318c41e..4dc6afdc 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -373,6 +373,43 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
 
 /**Function*************************************************************
 
+  Synopsis    [Find the number of the different pattern.]
+
+  Description [Returns -1 if there is no such pattern]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
+{
+    int i, v;
+    assert( !Fraig_IsComplement(pNode1) );
+    assert( !Fraig_IsComplement(pNode2) );
+    if ( fUseRand )
+    {
+        // check the simulation info
+        for ( i = 0; i < iWordLast; i++ )
+            if ( pNode1->puSimR[i] !=  pNode2->puSimR[i] )
+                for ( v = 0; v < 32; v++ )
+                    if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
+                        return i * 32 + v;
+    }
+    else
+    {
+        // check the simulation info
+        for ( i = 0; i < iWordLast; i++ )
+            if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
+                for ( v = 0; v < 32; v++ )
+                    if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
+                        return i * 32 + v;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Compares two pieces of simulation info.]
 
   Description [Returns 1 if they are equal.]