Version abc60220

15 files changed, 1232 insertions, 286 deletions

diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index ee029789..c83af527 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -300,8 +300,9 @@ extern void                Aig_ManStop( Aig_Man_t * p );
 /*=== aigNode.c =============================================================*/
 extern Aig_Node_t *        Aig_NodeCreateConst( Aig_Man_t * p );
 extern Aig_Node_t *        Aig_NodeCreatePi( Aig_Man_t * p );
-extern Aig_Node_t *        Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin );
+extern Aig_Node_t *        Aig_NodeCreatePo( Aig_Man_t * p );
 extern Aig_Node_t *        Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
+extern Aig_Node_t *        Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin );
 extern void                Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode );
 extern void                Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
 extern void                Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
index 991cc7e5..ce458353 100644
--- a/src/sat/aig/aigNode.c
+++ b/src/sat/aig/aigNode.c
@@ -104,12 +104,30 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
+Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p )
 {
     Aig_Node_t * pNode;
     pNode = Aig_NodeCreate( p );
     pNode->Type = AIG_PO;
     Vec_PtrPush( p->vPos, pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary output node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin )
+{
+    assert( Aig_NodeIsPo(pNode) );
+    assert( !Aig_IsComplement(pNode) );
     // connect to the fanin
     pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
     pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id;
@@ -224,13 +242,14 @@ void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot )
     assert( !Aig_IsComplement(pRoot) );
     assert( pRoot->nRefs == 0 );
     assert( Aig_NodeIsAnd(pRoot) );
-    // save the children
+    // remember the children
     pNode0 = Aig_NodeFanin0(pRoot);
     pNode1 = Aig_NodeFanin1(pRoot);
     // disconnect the node
     Aig_NodeDisconnectAnd( pRoot );
     // recycle the node
     Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL );
+    memset( pRoot, 0, sizeof(Aig_Node_t) ); // this is a temporary hack to skip dead children below!!!
     Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot );
     // call recursively
     if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 )
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index decf05ee..525d4a14 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
     // solve the miter
     clk = clock();
     pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
-    status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
+    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
diff --git a/src/sat/aig/rwrMffc.c b/src/sat/aig/rwrMffc.c
new file mode 100644
index 00000000..663534b3
--- /dev/null
+++ b/src/sat/aig/rwrMffc.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+  FileName    [rwrMffc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Procedures working with Maximum Fanout-Free Cones.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrMffc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int  Aig_NodeDeref_rec( Aig_Node_t * pNode );
+extern int  Aig_NodeRef_rec( Aig_Node_t * pNode );
+extern void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+extern void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MffcTest( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pNode, * pNodeA, * pNodeB, * pNodeC, * pLeaf;
+    Vec_Ptr_t * vCone, * vSupp;
+    int i, k;//, nNodes1, nNodes2;
+    int nSizes = 0;
+    int nCones = 0;
+    int nMuxes = 0;
+    int nExors = 0;
+
+    vCone = Vec_PtrAlloc( 100 );
+    vSupp = Vec_PtrAlloc( 100 );
+
+    // mark the multiple-fanout nodes
+    Aig_ManForEachAnd( pMan, pNode, i )
+        if ( pNode->nRefs > 1 )
+            pNode->fMarkA = 1;
+    // unmark the control inputs of MUXes and inputs of EXOR gates
+    Aig_ManForEachAnd( pMan, pNode, i )
+    {
+        if ( !Aig_NodeIsMuxType(pNode) )
+            continue;
+
+        pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
+        // if real children are used, skip
+        if ( Aig_NodeFanin0(pNode)->nRefs > 1 || Aig_NodeFanin1(pNode)->nRefs > 1 )
+            continue;
+/*
+
+        if ( pNodeC->nRefs == 2 )
+            pNodeC->fMarkA = 0;
+        if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) && Aig_Regular(pNodeA)->nRefs == 2 )
+            Aig_Regular(pNodeA)->fMarkA = 0;
+*/
+
+        if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) )
+            nExors++;
+        else
+            nMuxes++;
+    }
+    // mark the PO drivers
+    Aig_ManForEachPo( pMan, pNode, i )
+    {
+        Aig_NodeFanin0(pNode)->fMarkA = 1;
+        Aig_NodeFanin0(pNode)->fMarkB = 1;
+    }
+
+
+    // print sizes of MFFCs
+    Aig_ManForEachAnd( pMan, pNode, i )
+    {
+        if ( !pNode->fMarkA )
+            continue;
+
+//        nNodes1 = Aig_NodeDeref_rec( pNode );
+//        Aig_NodeMffsConeSupp( pNode, vCone, vSupp );
+//        nNodes2 = Aig_NodeRef_rec( pNode );
+//        assert( nNodes1 == nNodes2 );
+
+        Aig_NodeFactorConeSupp( pNode, vCone, vSupp );
+
+        printf( "%6d : Fan = %4d. Co = %5d.  Su = %5d.  %s ", 
+            pNode->Id, pNode->nRefs, Vec_PtrSize(vCone), Vec_PtrSize(vSupp), pNode->fMarkB? "po" : "  " );
+
+        Vec_PtrForEachEntry( vSupp, pLeaf, k )
+            printf( " %d", pLeaf->Id );
+
+        printf( "\n" );
+
+        nSizes += Vec_PtrSize(vCone);
+        nCones++;
+    }
+    printf( "Nodes = %6d.  MFFC sizes = %6d.  Cones = %6d.  nExors = %6d.  Muxes = %6d.\n",
+        Aig_ManAndNum(pMan), nSizes, nCones, nExors, nMuxes );
+
+    // unmark the nodes
+    Aig_ManForEachNode( pMan, pNode, i )
+    {
+        pNode->fMarkA = 0;
+        pNode->fMarkB = 0;
+        pNode->fMarkC = 0;
+    }
+
+    Vec_PtrFree( vCone );
+    Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeDeref_rec( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pNode0, * pNode1;
+    int Counter = 1;
+    if ( Aig_NodeIsPi(pNode) )
+        return 0;
+    pNode0 = Aig_NodeFanin0(pNode);
+    pNode1 = Aig_NodeFanin1(pNode);
+    assert( pNode0->nRefs > 0 );
+    assert( pNode1->nRefs > 0 );
+    if ( --pNode0->nRefs == 0 )
+        Counter += Aig_NodeDeref_rec( pNode0 );
+    if ( --pNode1->nRefs == 0 )
+        Counter += Aig_NodeDeref_rec( pNode1 );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeRef_rec( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pNode0, * pNode1;
+    int Counter = 1;
+    if ( Aig_NodeIsPi(pNode) )
+        return 0;
+    pNode0 = Aig_NodeFanin0(pNode);
+    pNode1 = Aig_NodeFanin1(pNode);
+    if ( pNode0->nRefs++ == 0 )
+        Counter += Aig_NodeRef_rec( pNode0 );
+    if ( pNode1->nRefs++ == 0 )
+        Counter += Aig_NodeRef_rec( pNode1 );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal and leaf nodes in the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeMffsConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
+{
+    // skip visited nodes
+    if ( Aig_NodeIsTravIdCurrent(pNode) )
+        return;
+    Aig_NodeSetTravIdCurrent(pNode);
+    // add to the new support nodes
+    if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->nRefs > 0) )
+    {
+        Vec_PtrPush( vSupp, pNode );
+        return;
+    }
+    // recur on the children
+    Aig_NodeMffsConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
+    Aig_NodeMffsConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
+    // collect the internal node
+    Vec_PtrPush( vCone, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the support of the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
+{
+    assert( Aig_NodeIsAnd(pNode) );
+    assert( !Aig_IsComplement(pNode) );
+    Vec_PtrClear( vCone );
+    Vec_PtrClear( vSupp );
+    Aig_ManIncrementTravId( pNode->pMan );
+    Aig_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal and leaf nodes of the factor-cut of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeFactorConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
+{
+    // skip visited nodes
+    if ( Aig_NodeIsTravIdCurrent(pNode) )
+        return;
+    Aig_NodeSetTravIdCurrent(pNode);
+    // add to the new support nodes
+    if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->fMarkA) )
+    {
+        Vec_PtrPush( vSupp, pNode );
+        return;
+    }
+    // recur on the children
+    Aig_NodeFactorConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
+    Aig_NodeFactorConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
+    // collect the internal node
+    assert( fTopmost || !pNode->fMarkA );
+    Vec_PtrPush( vCone, pNode );
+
+    assert( pNode->fMarkC == 0 );
+    pNode->fMarkC = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the support of the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
+{
+    assert( Aig_NodeIsAnd(pNode) );
+    assert( !Aig_IsComplement(pNode) );
+    Vec_PtrClear( vCone );
+    Vec_PtrClear( vSupp );
+    Aig_ManIncrementTravId( pNode->pMan );
+    Aig_NodeFactorConeSupp_rec( pNode, vCone, vSupp, 1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
index 2c402184..63a437ce 100644
--- a/src/sat/aig/rwrTruth.c
+++ b/src/sat/aig/rwrTruth.c
@@ -444,6 +444,8 @@ Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p )
         assert( 0 );
     }
 
+
+    return NULL;
 }
 
 
diff --git a/src/sat/aig/rwr_.c b/src/sat/aig/rwr_.c
new file mode 100644
index 00000000..45e76f75
--- /dev/null
+++ b/src/sat/aig/rwr_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [rwr_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwr_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/asat/asatmem.c b/src/sat/asat/asatmem.c
new file mode 100644
index 00000000..24c1b1a8
--- /dev/null
+++ b/src/sat/asat/asatmem.c
@@ -0,0 +1,527 @@
+/**CFile****************************************************************
+
+  FileName    [asatmem.c]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: asatmem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "asatmem.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Asat_MmFixed_t_
+{
+    // information about individual entries
+    int           nEntrySize;    // the size of one entry
+    int           nEntriesAlloc; // the total number of entries allocated
+    int           nEntriesUsed;  // the number of entries in use
+    int           nEntriesMax;   // the max number of entries in use
+    char *        pEntriesFree;  // the linked list of free entries
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+struct Asat_MmFlex_t_
+{
+    // information about individual entries
+    int           nEntriesUsed;  // the number of entries allocated
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+struct Asat_MmStep_t_
+{
+    int                nMems;    // the number of fixed memory managers employed
+    Asat_MmFixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
+    int                nMapSize; // the size of the memory array
+    Asat_MmFixed_t **  pMap;     // maps the number of bytes into its memory manager
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory pieces of fixed size.]
+
+  Description [The size of the chunk is computed as the minimum of
+  1024 entries and 64K. Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize )
+{
+    Asat_MmFixed_t * p;
+
+    p = ALLOC( Asat_MmFixed_t, 1 );
+    memset( p, 0, sizeof(Asat_MmFixed_t) );
+
+    p->nEntrySize    = nEntrySize;
+    p->nEntriesAlloc = 0;
+    p->nEntriesUsed  = 0;
+    p->pEntriesFree  = NULL;
+
+    if ( nEntrySize * (1 << 10) < (1<<16) )
+        p->nChunkSize = (1 << 10);
+    else
+        p->nChunkSize = (1<<16) / nEntrySize;
+    if ( p->nChunkSize < 8 )
+        p->nChunkSize = 8;
+
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+            p->nEntrySize, p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p )
+{
+    char * pTemp;
+    int i;
+
+    // check if there are still free entries
+    if ( p->nEntriesUsed == p->nEntriesAlloc )
+    { // need to allocate more entries
+        assert( p->pEntriesFree == NULL );
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+        // transform these entries into a linked list
+        pTemp = p->pEntriesFree;
+        for ( i = 1; i < p->nChunkSize; i++ )
+        {
+            *((char **)pTemp) = pTemp + p->nEntrySize;
+            pTemp += p->nEntrySize;
+        }
+        // set the last link
+        *((char **)pTemp) = NULL;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+        // add to the number of entries allocated
+        p->nEntriesAlloc += p->nChunkSize;
+    }
+    // incrememt the counter of used entries
+    p->nEntriesUsed++;
+    if ( p->nEntriesMax < p->nEntriesUsed )
+        p->nEntriesMax = p->nEntriesUsed;
+    // return the first entry in the free entry list
+    pTemp = p->pEntriesFree;
+    p->pEntriesFree = *((char **)pTemp);
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry )
+{
+    // decrement the counter of used entries
+    p->nEntriesUsed--;
+    // add the entry to the linked list of free entries
+    *((char **)pEntry) = p->pEntriesFree;
+    p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmFixedRestart( Asat_MmFixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // deallocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    p->nChunks = 1;
+    // transform these entries into a linked list
+    pTemp = p->pChunks[0];
+    for ( i = 1; i < p->nChunkSize; i++ )
+    {
+        *((char **)pTemp) = pTemp + p->nEntrySize;
+        pTemp += p->nEntrySize;
+    }
+    // set the last link
+    *((char **)pTemp) = NULL;
+    // set the free entry list
+    p->pEntriesFree  = p->pChunks[0];
+    // set the correct statistics
+    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
+    p->nMemoryUsed   = 0;
+    p->nEntriesAlloc = p->nChunkSize;
+    p->nEntriesUsed  = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates entries of flexible size.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Asat_MmFlex_t * Asat_MmFlexStart()
+{
+    Asat_MmFlex_t * p;
+
+    p = ALLOC( Asat_MmFlex_t, 1 );
+    memset( p, 0, sizeof(Asat_MmFlex_t) );
+
+    p->nEntriesUsed  = 0;
+    p->pCurrent      = NULL;
+    p->pEnd          = NULL;
+
+    p->nChunkSize    = (1 << 12);
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
+            p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
+            p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes )
+{
+    char * pTemp;
+    // check if there are still free entries
+    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
+    { // need to allocate more entries
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        if ( nBytes > p->nChunkSize )
+        {
+            // resize the chunk size if more memory is requested than it can give
+            // (ideally, this should never happen)
+            p->nChunkSize = 2 * nBytes;
+        }
+        p->pCurrent = ALLOC( char, p->nChunkSize );
+        p->pEnd     = p->pCurrent + p->nChunkSize;
+        p->nMemoryAlloc += p->nChunkSize;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pCurrent;
+    }
+    assert( p->pCurrent + nBytes <= p->pEnd );
+    // increment the counter of used entries
+    p->nEntriesUsed++;
+    // keep track of the memory used
+    p->nMemoryUsed += nBytes;
+    // return the next entry
+    pTemp = p->pCurrent;
+    p->pCurrent += nBytes;
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the hierarchical memory manager.]
+
+  Description [This manager can allocate entries of any size.
+  Iternally they are mapped into the entries with the number of bytes
+  equal to the power of 2. The smallest entry size is 8 bytes. The
+  next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 
+  8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
+  The input parameters "nSteps" says how many fixed memory managers
+  are employed internally. Calling this procedure with nSteps equal
+  to 10 results in 10 hierarchically arranged internal memory managers, 
+  which can allocate up to 4096 (1Kb) entries. Requests for larger 
+  entries are handed over to malloc() and then free()ed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Asat_MmStep_t * Asat_MmStepStart( int nSteps )
+{
+    Asat_MmStep_t * p;
+    int i, k;
+    p = ALLOC( Asat_MmStep_t, 1 );
+    p->nMems = nSteps;
+    // start the fixed memory managers
+    p->pMems = ALLOC( Asat_MmFixed_t *, p->nMems );
+    for ( i = 0; i < p->nMems; i++ )
+        p->pMems[i] = Asat_MmFixedStart( (8<<i) );
+    // set up the mapping of the required memory size into the corresponding manager
+    p->nMapSize = (4<<p->nMems);
+    p->pMap = ALLOC( Asat_MmFixed_t *, p->nMapSize+1 );
+    p->pMap[0] = NULL;
+    for ( k = 1; k <= 4; k++ )
+        p->pMap[k] = p->pMems[0];
+    for ( i = 0; i < p->nMems; i++ )
+        for ( k = (4<<i)+1; k <= (8<<i); k++ )
+            p->pMap[k] = p->pMems[i];
+//for ( i = 1; i < 100; i ++ )
+//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose )
+{
+    int i;
+    for ( i = 0; i < p->nMems; i++ )
+        Asat_MmFixedStop( p->pMems[i], fVerbose );
+    free( p->pMems );
+    free( p->pMap );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes )
+{
+    if ( nBytes == 0 )
+        return NULL;
+    if ( nBytes > p->nMapSize )
+    {
+//        printf( "Allocating %d bytes.\n", nBytes );
+        return ALLOC( char, nBytes );
+    }
+    return Asat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes )
+{
+    if ( nBytes == 0 )
+        return;
+    if ( nBytes > p->nMapSize )
+    {
+        free( pEntry );
+        return;
+    }
+    Asat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Asat_MmStepReadMemUsage( Asat_MmStep_t * p )
+{
+    int i, nMemTotal = 0;
+    for ( i = 0; i < p->nMems; i++ )
+        nMemTotal += p->pMems[i]->nMemoryAlloc;
+    return nMemTotal;
+}
diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h
new file mode 100644
index 00000000..56115e7d
--- /dev/null
+++ b/src/sat/asat/asatmem.h
@@ -0,0 +1,76 @@
+/**CFile****************************************************************
+
+  FileName    [asatmem.h]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: asatmem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __ASAT_MEM_H__
+#define __ASAT_MEM_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"       
+#include <stdio.h>
+#include <stdlib.h>
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Asat_MmFixed_t_ Asat_MmFixed_t;
+typedef struct Asat_MmFlex_t_  Asat_MmFlex_t;
+typedef struct Asat_MmStep_t_  Asat_MmStep_t;
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+// fixed-size-block memory manager
+extern Asat_MmFixed_t *    Asat_MmFixedStart( int nEntrySize );
+extern void                Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose );
+extern char *              Asat_MmFixedEntryFetch( Asat_MmFixed_t * p );
+extern void                Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry );
+extern void                Asat_MmFixedRestart( Asat_MmFixed_t * p );
+extern int                 Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Asat_MmFlex_t *     Asat_MmFlexStart();
+extern void                Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose );
+extern char *              Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes );
+extern int                 Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p );
+// hierarchical memory manager
+extern Asat_MmStep_t *     Asat_MmStepStart( int nSteps );
+extern void                Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose );
+extern char *              Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes );
+extern void                Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes );
+extern int                 Asat_MmStepReadMemUsage( Asat_MmStep_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make
index 882176fa..d5cf69bf 100644
--- a/src/sat/asat/module.make
+++ b/src/sat/asat/module.make
@@ -1,2 +1,3 @@
 SRC +=  src/sat/asat/added.c \
+    src/sat/asat/asatmem.c \
     src/sat/asat/solver.c
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 3927fac3..1130d437 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "solver.h"
 
+//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+
 //=================================================================================================
 // Simple (var/literal) helpers:
 
@@ -275,7 +277,14 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
     size           = end - begin;
-    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+
+//    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+    c = (clause*)Asat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
     c->size_learnt = (size << 1) | learnt;
     assert(((unsigned int)c & 1) == 0);
 
@@ -324,7 +333,12 @@ static void clause_remove(solver* s, clause* c)
         s->solver_stats.clauses_literals -= clause_size(c);
     }
 
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
     free(c);
+#else
+    Asat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+
 }
 
 
@@ -829,12 +843,24 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
             // NO CONFLICT
             int next;
 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts)
+            {
                 // Reached bound on number of conflicts:
                 s->progress_estimate = solver_progress(s);
                 solver_canceluntil(s,s->root_level);
                 vec_delete(&learnt_clause);
-                return l_Undef; }
+                return l_Undef; 
+            }
+
+            if ( s->nConfLimit && s->solver_stats.conflicts    > s->nConfLimit ||
+                 s->nImpLimit  && s->solver_stats.propagations > s->nImpLimit )
+            {
+                // Reached bound on number of conflicts:
+                s->progress_estimate = solver_progress(s);
+                solver_canceluntil(s,s->root_level);
+                vec_delete(&learnt_clause);
+                return l_Undef; 
+            }
 
             if (solver_dlevel(s) == 0)
                 // Simplify the set of problem clauses:
@@ -922,18 +948,28 @@ solver* solver_new(void)
     s->solver_stats.max_literals     = 0;
     s->solver_stats.tot_literals     = 0;
 
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    s->pMem = NULL;
+#else
+    s->pMem = Asat_MmStepStart( 10 );
+#endif
+
     return s;
 }
 
 
 void solver_delete(solver* s)
 {
+
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
     int i;
     for (i = 0; i < vec_size(&s->clauses); i++)
         free(vec_begin(&s->clauses)[i]);
-
     for (i = 0; i < vec_size(&s->learnts); i++)
         free(vec_begin(&s->learnts)[i]);
+#else
+    Asat_MmStepStop( s->pMem, 0 );
+#endif
 
     // delete vectors
     vec_delete(&s->clauses);
@@ -1056,14 +1092,18 @@ bool   solver_simplify(solver* s)
 }
 
 
-bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
+bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit )
 {
     double  nof_conflicts = 100;
     double  nof_learnts   = solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
     lit*    i;
-    int     timeStart     = clock();
+
+    // set the external limits
+    s->nConfLimit = nConfLimit;    // external limit on the number of conflicts
+    s->nImpLimit  = nImpLimit;     // external limit on the number of implications
+  
 
     for (i = begin; i < end; i++)
         if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
@@ -1098,9 +1138,18 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
         status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
-        // if the runtime limit is exceeded, quit the restart loop
-        if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) )
+
+        // quit the loop if reached an external limit
+        if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit )
+        {
+//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
+        }
+        if ( s->nImpLimit  && s->solver_stats.propagations > s->nImpLimit )
+        {
+//            printf( "Reached the limit on the number of implications (%d).\n", s->nImpLimit );
+            break;
+        }
     }
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 9618603c..d798a7a9 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #endif
 
 #include "solver_vec.h"
+#include "asatmem.h"
 
 //=================================================================================================
 // Simple types:
@@ -67,7 +68,7 @@ extern void    solver_delete(solver* s);
 
 extern bool    solver_addclause(solver* s, lit* begin, lit* end);
 extern bool    solver_simplify(solver* s);
-extern int     solver_solve(solver* s, lit* begin, lit* end, int nSeconds);
+extern int     solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit );
 extern int *   solver_get_model( solver * p, int * pVars, int nVars );
 
 extern int     solver_nvars(solver* s);
@@ -132,6 +133,12 @@ struct solver_t
     double   progress_estimate;
     int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
 
+    int      nConfLimit;    // external limit on the number of conflicts
+    int      nImpLimit;     // external limit on the number of implications
+
+    // the memory manager
+    Asat_MmStep_t *     pMem;
+
     stats    solver_stats;
 };
 
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index d25e42db..d286ea9c 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -17,14 +17,15 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "fraig.h"
 #include "csat_apis.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_DEFAULT_TIMEOUT     60   // 60 seconds
+#define ABC_DEFAULT_CONF_LIMIT     0   // limit on conflicts
+#define ABC_DEFAULT_IMP_LIMIT      0   // limit on implications
+
 
 struct ABC_ManagerStruct_t
 {
@@ -37,19 +38,24 @@ struct ABC_ManagerStruct_t
     Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
     // solving parameters
     int                   mode;          // 0 = brute-force SAT;  1 = resource-aware FRAIG
-    int                   nSeconds;      // time limit for pure SAT solving
-    Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
+    int                   nConfLimit;    // time limit for pure SAT solving
+    int                   nImpLimit;     // time limit for pure SAT solving
+//    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
-    ABC_Target_ResultT *  pResult;       // the result of solving the target
+    CSAT_Target_ResultT *  pResult;       // the result of solving the target
 };
 
-static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars );
+static CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars );
 static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode );
 
+// procedures to start and stop the ABC framework
+extern void  Abc_Start();
+extern void  Abc_Stop();
+
 // some external procedures
 extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 
@@ -71,16 +77,18 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 ABC_Manager ABC_InitManager()
 {
     ABC_Manager_t * mng;
+    Abc_Start();
     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->pNtk->pName = Extra_UtilStrsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
     mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
     mng->pMmNames   = Extra_MmFlexStart();
     mng->vNodes     = Vec_PtrAlloc( 100 );
     mng->vValues    = Vec_IntAlloc( 100 );
-    mng->nSeconds   = ABC_DEFAULT_TIMEOUT;
+    mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT;
+    mng->nImpLimit  = ABC_DEFAULT_IMP_LIMIT;
     return mng;
 }
 
@@ -95,7 +103,7 @@ ABC_Manager ABC_InitManager()
   SeeAlso     []
 
 ***********************************************************************/
-void ABC_QuitManager( ABC_Manager mng )
+void ABC_ReleaseManager( ABC_Manager mng )
 {
     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
@@ -106,6 +114,7 @@ void ABC_QuitManager( ABC_Manager mng )
     if ( mng->vValues )    Vec_IntFree( mng->vValues );
     FREE( mng->pDumpFileName );
     free( mng );
+    Abc_Stop();
 }
 
 /**Function*************************************************************
@@ -119,7 +128,7 @@ void ABC_QuitManager( ABC_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option )
+void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option )
 {
     mng->mode = option;
     if ( option == 0 )
@@ -160,23 +169,23 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
     // consider different cases, create the node, and map the node into the name
     switch( type )
     {
-    case ABC_BPI:
-    case ABC_BPPI:
+    case CSAT_BPI:
+    case CSAT_BPPI:
         if ( nofi != 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 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:
+    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
@@ -189,51 +198,51 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
         // create the node function
         switch( type )
         {
-            case ABC_CONST:
+            case CSAT_CONST:
                 if ( nofi != 0 )
                     { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
                 break;
-            case ABC_BAND:
+            case CSAT_BAND:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
                 break;
-            case ABC_BNAND:
+            case CSAT_BNAND:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
                 break;
-            case ABC_BOR:
+            case CSAT_BOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
                 break;
-            case ABC_BNOR:
+            case CSAT_BNOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
                 pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
                 break;
-            case ABC_BXOR:
+            case CSAT_BXOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
                     { 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 ABC_BXNOR:
+            case CSAT_BXNOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
                     { 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 ABC_BINV:
+            case CSAT_BINV:
                 if ( nofi != 1 )
                     { 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 ABC_BBUF:
+            case CSAT_BBUF:
                 if ( nofi != 1 )
                     { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
                 pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
@@ -243,8 +252,8 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
         }
         Abc_ObjSetData( pObj, pSop );
         break;
-    case ABC_BPPO:
-    case ABC_BPO:
+    case CSAT_BPPO:
+    case CSAT_BPO:
         if ( nofi != 1 )
             { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
         // create the PO
@@ -268,38 +277,46 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
 
 /**Function*************************************************************
 
-  Synopsis    [Checks integraty of the manager.]
+  Synopsis    [This procedure also finalizes construction of the ABC network.]
 
-  Description [Checks if there are gates that are not used by any primary output.
-  If no such gates exist, return 1 else return 0.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int ABC_Check_Integrity( ABC_Manager mng )
+void ABC_Network_Finalize( ABC_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, ABC_GetNodeName(mng, pObj) );
     Abc_NtkForEachPo( pNtk, pObj, i )
         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( "ABC_Check_Integrity: The internal network check has failed.\n" );
-        return 0;
-    }
+/**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     []
 
-    // check that there is no dangling nodes
+***********************************************************************/
+int ABC_Check_Integrity( ABC_Manager mng )
+{
+    Abc_Ntk_t * pNtk = mng->pNtk;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // check that there are no dangling nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) 
@@ -310,6 +327,13 @@ int ABC_Check_Integrity( ABC_Manager mng )
             return 0;
         }
     }
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkDoCheck( pNtk ) )
+    {
+        printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
+        return 0;
+    }
     return 1;
 }
 
@@ -326,7 +350,7 @@ int ABC_Check_Integrity( ABC_Manager mng )
 ***********************************************************************/
 void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
 {
-    mng->nSeconds = runtime;
+    printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -356,9 +380,25 @@ void ABC_SetLearnLimit( ABC_Manager mng, int num )
   SeeAlso     []
 
 ***********************************************************************/
+void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
+{
+    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
 {
-    printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
+    mng->nConfLimit = num;
 }
 
 /**Function*************************************************************
@@ -372,9 +412,9 @@ void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
   SeeAlso     []
 
 ***********************************************************************/
-void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
+void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num )
 {
-    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+    mng->nImpLimit = num;
 }
 
 /**Function*************************************************************
@@ -391,7 +431,7 @@ void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
 void ABC_EnableDump( ABC_Manager mng, char * dump_file )
 {
     FREE( mng->pDumpFileName );
-    mng->pDumpFileName = util_strsav( dump_file );
+    mng->pDumpFileName = Extra_UtilStrsav( dump_file );
 }
 
 /**Function*************************************************************
@@ -447,9 +487,6 @@ int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values )
 ***********************************************************************/
 void ABC_SolveInit( ABC_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 )
@@ -459,30 +496,8 @@ void ABC_SolveInit( ABC_Manager mng )
     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   = 10;             // the max number of backtracks to perform at a node
-    pParams->nSeconds   = mng->nSeconds;  // the time out for the final proof
-    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
+    mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
+
 }
 
 /**Function*************************************************************
@@ -511,78 +526,35 @@ void ABC_AnalyzeTargets( ABC_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-enum ABC_StatusT ABC_Solve( ABC_Manager mng )
+enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 {
-    Fraig_Man_t * pMan;
-    Abc_Ntk_t * pCnf;
-    int * pModel;
     int RetValue, i;
 
     // check if the target network is available
     if ( mng->pTarget == NULL )
         { 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
-//    Abc_NtkRewrite( mng->pTarget, 0, 1, 0 );
+    // try to prove the miter using a number of techniques
+    RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
 
-    if ( mng->mode == 0 ) // brute-force SAT
-    {
-        // transform the AIG into a logic network for efficient CNF construction
-        pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 );
-        RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );
-
-        // analyze the result
-        mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
-        if ( RetValue == -1 )
-            mng->pResult->status = UNDETERMINED;
-        else if ( RetValue == 1 )
-            mng->pResult->status = UNSATISFIABLE;
-        else if ( RetValue == 0 )
-        {
-            mng->pResult->status = SATISFIABLE;
-            // create the array of PI names and values
-            for ( i = 0; i < mng->pResult->no_sig; i++ )
-            {
-                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 );
-        }
-        else assert( 0 );
-        Abc_NtkDelete( pCnf );
-    }
-    else if ( mng->mode == 1 ) // resource-aware fraiging
+    // analyze the result
+    mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+    if ( RetValue == -1 )
+        mng->pResult->status = UNDETERMINED;
+    else if ( RetValue == 1 )
+        mng->pResult->status = UNSATISFIABLE;
+    else if ( RetValue == 0 )
     {
-        // transform the target into a fraig
-        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0, 0 ); 
-        Fraig_ManProveMiter( pMan );
-        RetValue = Fraig_ManCheckMiter( pMan );
-
-        // analyze the result
-        mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
-        if ( RetValue == -1 )
-            mng->pResult->status = UNDETERMINED;
-        else if ( RetValue == 1 )
-            mng->pResult->status = UNSATISFIABLE;
-        else if ( RetValue == 0 )
+        mng->pResult->status = SATISFIABLE;
+        // create the array of PI names and values
+        for ( i = 0; i < mng->pResult->no_sig; i++ )
         {
-            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] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
-                mng->pResult->values[i] = pModel[i];
-            }
+            mng->pResult->names[i]  = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) ); 
+            mng->pResult->values[i] = mng->pTarget->pModel[i];
         }
-        else assert( 0 );
-        // delete the fraig manager
-        Fraig_ManFree( pMan );
+        FREE( mng->pTarget->pModel );
     }
-    else
-        assert( 0 );
+    else assert( 0 );
 
     // delete the target
     Abc_NtkDelete( mng->pTarget );
@@ -602,7 +574,7 @@ enum ABC_StatusT ABC_Solve( ABC_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
+CSAT_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
 {
     return mng->pResult;
 }
@@ -615,7 +587,7 @@ ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
                
   SideEffects []
 
-  SeeAlso     []
+  SeeAlso     [] 
 
 ***********************************************************************/
 void ABC_Dump_Bench_File( ABC_Manager mng )
@@ -647,11 +619,11 @@ void ABC_Dump_Bench_File( ABC_Manager mng )
   SeeAlso     []
 
 ***********************************************************************/
-ABC_Target_ResultT * ABC_TargetResAlloc( int nVars )
+CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars )
 {
-    ABC_Target_ResultT * p;
-    p = ALLOC( ABC_Target_ResultT, 1 );
-    memset( p, 0, sizeof(ABC_Target_ResultT) );
+    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 );
@@ -671,7 +643,7 @@ ABC_Target_ResultT * ABC_TargetResAlloc( int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void ABC_TargetResFree( ABC_Target_ResultT * p )
+void ABC_TargetResFree( CSAT_Target_ResultT * p )
 {
     if ( p == NULL )
         return;
@@ -702,100 +674,6 @@ char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode )
 }
 
 
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure applies a rewriting script to the network.]
-
-  Description [Rewriting is performed without regard for the number of 
-  logic levels. This corresponds to "circuit compression for formal 
-  verification" (Per Bjesse et al, ICCAD 2004) but implemented in a more 
-  exhaustive way than in the above paper.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_PerformRewriting( ABC_Manager mng )
-{
-    void * pAbc;
-    char Command[1000];
-    int clkBalan, clkResyn, clk;
-    int fPrintStats = 1;
-    int fUseResyn   = 1;
-
-    // procedures to get the ABC framework and execute commands in it
-    extern void * Abc_FrameGetGlobalFrame();
-    extern void Abc_FrameReplaceCurrentNetwork( void * p, Abc_Ntk_t * pNtk );
-    extern int  Cmd_CommandExecute( void * p, char * sCommand );
-    extern Abc_Ntk_t * Abc_FrameReadNtk( void * p );
-
-
-    // get the pointer to the ABC framework
-    pAbc = Abc_FrameGetGlobalFrame();
-    assert( pAbc != NULL );
-
-    // replace the current network by the target network
-    Abc_FrameReplaceCurrentNetwork( pAbc, mng->pTarget );
-
-clk = clock();
-    //////////////////////////////////////////////////////////////////////////
-    // balance
-    sprintf( Command, "balance" );
-    if ( Cmd_CommandExecute( pAbc, Command ) )
-    {
-        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
-        return;
-    }
-clkBalan = clock() - clk;
-
-    //////////////////////////////////////////////////////////////////////////
-    // print stats
-    if ( fPrintStats )
-    {
-        sprintf( Command, "print_stats" );
-        if ( Cmd_CommandExecute( pAbc, Command ) )
-        {
-            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
-            return;
-        }
-    }
-
-clk = clock();
-    //////////////////////////////////////////////////////////////////////////
-    // synthesize
-    if ( fUseResyn )
-    {
-        sprintf( Command, "balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance" );
-        if ( Cmd_CommandExecute( pAbc, Command ) )
-        {
-            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
-            return;
-        }
-    }
-clkResyn = clock() - clk;
-
-    //////////////////////////////////////////////////////////////////////////
-    // print stats
-    if ( fPrintStats )
-    {
-        sprintf( Command, "print_stats" );
-        if ( Cmd_CommandExecute( pAbc, Command ) )
-        {
-            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
-            return;
-        }
-    }
-    printf( "Balancing = %6.2f sec   ",   (float)(clkBalan)/(float)(CLOCKS_PER_SEC) );
-    printf( "Rewriting = %6.2f sec   ",   (float)(clkResyn)/(float)(CLOCKS_PER_SEC) );
-    printf( "\n" );
-
-    // read the target network from the current network
-    mng->pTarget = Abc_NtkDup( Abc_FrameReadNtk(pAbc) );
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index a6179710..faba9ee4 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -12,13 +12,17 @@
 
   Date        [Ver. 1.0. Started - August 28, 2005]
 
-  Revision    [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
+  Revision    [$Id: csat_apis.h,v 1.5 2005/12/30 10:54:40 rmukherj Exp $]
 
 ***********************************************************************/
 
 #ifndef __ABC_APIS_H__
 #define __ABC_APIS_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,27 +46,35 @@ typedef struct ABC_ManagerStruct_t *   ABC_Manager;
 #define _ABC_GATE_TYPE_
 enum GateType
 {
-    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
+    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_BMUX,   // bit level MUX --not supported 
+    CSAT_BDFF,   // bit level D-type FF
+    CSAT_BSDFF,  // bit level scan FF --not supported 
+    CSAT_BTRIH,  // bit level TRISTATE gate with active high control --not supported 
+    CSAT_BTRIL,  // bit level TRISTATE gate with active low control --not supported 
+    CSAT_BBUS,   // bit level BUS --not supported 
+    CSAT_BPPO,   // bit level PSEUDO PRIMARY OUTPUT
+    CSAT_BPO,    // boolean PO
+    CSAT_BCNF,   // boolean constraint
+    CSAT_BDC,    // boolean don't care gate (2 input)
 };
 #endif
 
 
-//ABC_StatusT defines the return value by ABC_Solve();
+//CSAT_StatusT defines the return value by ABC_Solve();
 #ifndef _ABC_STATUS_
 #define _ABC_STATUS_
-enum ABC_StatusT 
+enum CSAT_StatusT 
 {
     UNDETERMINED = 0,
     UNSATISFIABLE,
@@ -76,11 +88,23 @@ enum ABC_StatusT
 #endif
 
 
-// ABC_OptionT defines the solver option about learning
+// to identify who called the CSAT solver
+#ifndef _ABC_CALLER_
+#define _ABC_CALLER_
+enum CSAT_CallerT
+{
+    BLS = 0,
+    SATORI,
+    NONE
+};
+#endif
+
+
+// CSAT_OptionT defines the solver option about learning
 // which is used by ABC_SetSolveOption();
 #ifndef _ABC_OPTION_
 #define _ABC_OPTION_
-enum ABC_OptionT
+enum CSAT_OptionT
 {
     BASE_LINE = 0,
     IMPLICT_LEARNING, //default
@@ -91,10 +115,10 @@ enum ABC_OptionT
 
 #ifndef _ABC_Target_Result
 #define _ABC_Target_Result
-typedef struct _ABC_Target_ResultT ABC_Target_ResultT;
-struct _ABC_Target_ResultT
+typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
+struct _CSAT_Target_ResultT
 {
-    enum ABC_StatusT status; // solve status of the target
+    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 
@@ -118,10 +142,13 @@ struct _ABC_Target_ResultT
 ////////////////////////////////////////////////////////////////////////
 
 // create a new manager
-extern ABC_Manager           ABC_InitManager(void);
+extern ABC_Manager          ABC_InitManager(void);
+
+// release a manager
+extern void ABC_ReleaseManager(ABC_Manager mng);
 
 // set solver options for learning
-extern void                  ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option);
+extern void                  ABC_SetSolveOption(ABC_Manager mng, enum CSAT_OptionT option);
 
 // add a gate to the circuit
 // the meaning of the parameters are:
@@ -130,16 +157,19 @@ extern void                  ABC_SetSolveOption(ABC_Manager mng, enum ABC_Option
 // nofi: number of fanins of the gate to be added;
 // fanins: the name array of fanins of the gate to be added
 extern int                   ABC_AddGate(ABC_Manager mng,
-                                      enum GateType type,
-                                      char* name,
-                                      int nofi,
-                                      char** fanins,
-                                      int dc_attr);
+                     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                   ABC_Check_Integrity(ABC_Manager mng);
 
+// THIS PROCEDURE SHOULD BE CALLED AFTER THE NETWORK IS CONSTRUCTED!!!
+extern void                  ABC_Network_Finalize( ABC_Manager mng );
+
 // set time limit for solving a target.
 // runtime: time limit (in second).
 extern void                  ABC_SetTimeLimit(ABC_Manager mng, int runtime);
@@ -160,21 +190,24 @@ extern void                  ABC_SolveInit(ABC_Manager mng);
 extern void                  ABC_AnalyzeTargets(ABC_Manager mng);
 
 // solve the targets added by ABC_AddTarget()
-extern enum ABC_StatusT      ABC_Solve(ABC_Manager mng);
+extern enum CSAT_StatusT     ABC_Solve(ABC_Manager mng);
 
 // get the solve status of a target
 // TargetID: the target id returned by  ABC_AddTarget().
-extern ABC_Target_ResultT *  ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
+extern CSAT_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
 extern void                  ABC_Dump_Bench_File(ABC_Manager mng);
 
 // ADDED PROCEDURES:
-extern void                  ABC_QuitManager( ABC_Manager mng );
-extern void                  ABC_TargetResFree( ABC_Target_ResultT * p );
+extern void                  ABC_TargetResFree( CSAT_Target_ResultT * p );
 
-extern void                  ABC_PerformRewriting( ABC_Manager mng );
+extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller);
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 237030af..4637c030 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -44,6 +44,8 @@ struct Fraig_ParamsStruct_t_
     int  nPatsDyna;     // the number of words of dynamic simulation info
     int  nBTLimit;      // the max number of backtracks to perform
     int  nSeconds;      // the timeout for the final proof
+    int  nConfLimit;
+    int  nImpLimit;
     int  fFuncRed;      // performs only one level hashing
     int  fFeedBack;     // enables solver feedback
     int  fDist1Pats;    // enables distance-1 patterns
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index fab01368..4ebb9a9f 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -49,7 +49,7 @@
 Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 )
 {
     Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
-    int RetValue;
+//    int RetValue;
 
     // check for trivial cases
     if ( p1 == p2 )