Version abc70930

3 files changed, 0 insertions, 992 deletions

diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
deleted file mode 100644
index 5872f5bc..00000000
--- a/src/sat/csat/csat_apis.c
+++ /dev/null
@@ -1,769 +0,0 @@
-/**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                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define ABC_DEFAULT_CONF_LIMIT     0   // limit on conflicts
-#define ABC_DEFAULT_IMP_LIMIT      0   // limit on implications
-
-
-struct ABC_ManagerStruct_t
-{
-    // information about the problem
-    stmm_table *          tName2Node;    // the hash table mapping names to nodes
-    stmm_table *          tNode2Name;    // the hash table mapping nodes to names
-    Abc_Ntk_t *           pNtk;          // the starting ABC network
-    Abc_Ntk_t *           pTarget;       // the AIG representing the target
-    char *                pDumpFileName; // the name of the file to dump the target network
-    Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
-    // solving parameters
-    int                   mode;          // 0 = resource-aware integration; 1 = brute-force SAT
-    Prove_Params_t        Params;        // integrated CEC parameters
-    // 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 * 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 );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates a new manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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, 1 );
-    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->mode       = 0; // set "resource-aware integration" as the default mode
-    // set default parameters for CEC
-    Prove_ParamsSetDefault( &mng->Params );
-    // set infinite resource limit for the final mitering
-//    mng->Params.nMiteringLimitLast = ABC_INFINITY;
-    return mng;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_ReleaseManager( ABC_Manager mng )
-{
-    CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
-    ABC_TargetResFree(p_res);
-    if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
-    if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
-    if ( mng->pMmNames )   Extra_MmFlexStop( mng->pMmNames );
-    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 );
-    Abc_Stop();
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets solver options for learning.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option )
-{
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets solving mode by brute-force SAT.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_UseOnlyCoreSatSolver( ABC_Manager mng )
-{
-    mng->mode = 1;  // switch to "brute-force SAT" as the solving option
-}
-
-/**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 ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
-{
-    Abc_Obj_t * pObj, * pFanin;
-    char * pSop, * pNewName;
-    int i;
-
-    // save the name in the local memory manager
-    pNewName = Extra_MmFlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
-    strcpy( pNewName, name );
-    name = pNewName;
-
-    // consider different cases, create the node, and map the node into the name
-    switch( type )
-    {
-    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 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( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
-            Abc_ObjAddFanin( pObj, pFanin );
-        }
-        // create the node function
-        switch( type )
-        {
-            case CSAT_CONST:
-                if ( nofi != 0 )
-                    { printf( "ABC_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( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
-                break;
-            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 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 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 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 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 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 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 );
-                break;
-            default :
-                break;
-        }
-        Abc_ObjSetData( pObj, pSop );
-        break;
-    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
-        pObj = Abc_NtkCreatePo( mng->pNtk );
-        stmm_insert( mng->tNode2Name, (char *)pObj, name );
-        // connect to the PO fanin
-        if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
-            { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
-        Abc_ObjAddFanin( pObj, pFanin );
-        break;
-    default:
-        printf( "ABC_AddGate: Unknown gate type.\n" );
-        break;
-    }
-
-    // map the name into the node
-    if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
-        { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure also finalizes construction of the ABC network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_Network_Finalize( ABC_Manager mng )
-{
-    Abc_Ntk_t * pNtk = mng->pNtk;
-    Abc_Obj_t * pObj;
-    int i;
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
-    assert( Abc_NtkLatchNum(pNtk) == 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     []
-
-***********************************************************************/
-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 ) 
-            continue;
-        if ( Abc_ObjFanoutNum(pObj) == 0 )
-        {
-//            printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
-            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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets time limit for solving a target.]
-
-  Description [Runtime: time limit (in second).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
-{
-//    printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetLearnLimit( ABC_Manager mng, int num )
-{
-//    printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  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 )
-{
-    mng->Params.nMiteringLimitLast = num;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num )
-{
-//    printf( "ABC_SetSolveImplicationLimit: The resource limit is not implemented (warning).\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num )
-{
-    mng->Params.nTotalBacktrackLimit = num;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num )
-{
-    mng->Params.nTotalInspectLimit = num;
-}
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng )
-{
-    return mng->Params.nTotalBacktracksMade;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-uint64 ABC_GetTotalInspectsMade( ABC_Manager mng )
-{
-    return mng->Params.nTotalInspectsMade;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the file name to dump the structurally hashed network used for solving.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_EnableDump( ABC_Manager mng, char * dump_file )
-{
-    FREE( mng->pDumpFileName );
-    mng->pDumpFileName = Extra_UtilStrsav( 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 ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    if ( nog < 1 )
-        { printf( "ABC_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( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
-        Vec_PtrPush( mng->vNodes, pObj );
-        if ( values[i] < 0 || values[i] > 1 )
-            { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
-        Vec_IntPush( mng->vValues, values[i] );
-    }
-    mng->nog = nog;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Initialize the solver internal data structure.]
-
-  Description [Prepares the solver to work on one specific target
-  set by calling ABC_AddTarget before.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_SolveInit( ABC_Manager mng )
-{
-    // check if the target is available
-    assert( mng->nog == Vec_PtrSize(mng->vNodes) );
-    if ( mng->nog == 0 )
-        { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
-
-    // free the previous target network if present
-    if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
-
-    // set the new target network
-//    mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
-    mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Currently not implemented.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void ABC_AnalyzeTargets( ABC_Manager mng )
-{
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Solves the targets added by ABC_AddTarget().]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
-{
-    Prove_Params_t * pParams = &mng->Params;
-    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; }
-
-    // try to prove the miter using a number of techniques
-    if ( mng->mode )
-        RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
-    else
-//        RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
-        RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
-
-    // 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]  = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) ); 
-            mng->pResult->values[i] = mng->pTarget->pModel[i];
-        }
-        FREE( mng->pTarget->pModel );
-    }
-    else assert( 0 );
-
-    // 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 ABC_AddTarget().]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-CSAT_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
-{
-    return mng->pResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dumps the original network into the BENCH file.]
-
-  Description [This procedure should be modified to dump the target.]
-               
-  SideEffects []
-
-  SeeAlso     [] 
-
-***********************************************************************/
-void ABC_Dump_Bench_File( ABC_Manager mng )
-{
-    Abc_Ntk_t * pNtkTemp, * pNtkAig;
-    char * pFileName;
- 
-    // derive the netlist
-    pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 );
-    pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
-    Abc_NtkDelete( pNtkAig );
-    if ( pNtkTemp == NULL ) 
-        { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
-    pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
-    Io_WriteBench( pNtkTemp, pFileName );
-    Abc_NtkDelete( pNtkTemp );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the target result.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-CSAT_Target_ResultT * ABC_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 ABC_TargetResFree( CSAT_Target_ResultT * p )
-{
-    if ( p == NULL )
-        return;
-    if( p->names )
-    {
-        int i = 0;
-        for ( i = 0; i < p->no_sig; i++ )
-        {
-            FREE(p->names[i]);
-        }
-    }
-    FREE( p->names );
-    FREE( p->values );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dumps the target AIG into the BENCH file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode )
-{
-    char * pName = NULL;
-    if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
-    {
-        assert( 0 );
-    }
-    return pName;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
deleted file mode 100644
index b80eddbf..00000000
--- a/src/sat/csat/csat_apis.h
+++ /dev/null
@@ -1,222 +0,0 @@
-/**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.5 2005/12/30 10:54:40 rmukherj Exp $]
-
-***********************************************************************/
-
-#ifndef __ABC_APIS_H__
-#define __ABC_APIS_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-
-typedef struct ABC_ManagerStruct_t     ABC_Manager_t;
-typedef struct ABC_ManagerStruct_t *   ABC_Manager;
-
-
-// GateType defines the gate type that can be added to circuit by
-// ABC_AddGate();
-#ifndef _ABC_GATE_TYPE_
-#define _ABC_GATE_TYPE_
-enum GateType
-{
-    CSAT_CONST = 0,  // constant gate
-    CSAT_BPI,    // boolean PI
-    CSAT_BPPI,   // bit level PSEUDO PRIMARY INPUT
-    CSAT_BAND,   // bit level AND
-    CSAT_BNAND,  // bit level NAND
-    CSAT_BOR,    // bit level OR
-    CSAT_BNOR,   // bit level NOR
-    CSAT_BXOR,   // bit level XOR
-    CSAT_BXNOR,  // bit level XNOR
-    CSAT_BINV,   // bit level INVERTER
-    CSAT_BBUF,   // bit level BUFFER
-    CSAT_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
-
-
-//CSAT_StatusT defines the return value by ABC_Solve();
-#ifndef _ABC_STATUS_
-#define _ABC_STATUS_
-enum CSAT_StatusT 
-{
-    UNDETERMINED = 0,
-    UNSATISFIABLE,
-    SATISFIABLE,
-    TIME_OUT,
-    FRAME_OUT,
-    NO_TARGET,
-    ABORTED,
-    SEQ_SATISFIABLE     
-};
-#endif
-
-
-// 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 CSAT_OptionT
-{
-    BASE_LINE = 0,
-    IMPLICT_LEARNING, //default
-    EXPLICT_LEARNING
-};
-#endif
-
-
-#ifndef _ABC_Target_Result
-#define _ABC_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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-// create a new manager
-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 CSAT_OptionT option);
-
-// enable checking by brute-force SAT solver (MiniSat-1.14)
-extern void                  ABC_UseOnlyCoreSatSolver(ABC_Manager mng);
-
-
-// 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                   ABC_AddGate(ABC_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                   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);
-extern void                  ABC_SetLearnLimit(ABC_Manager mng, int num);
-extern void                  ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num);
-extern void                  ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
-extern void                  ABC_EnableDump(ABC_Manager mng, char* dump_file);
-
-extern void                  ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num );
-extern void                  ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num );
-extern uint64                ABC_GetTotalBacktracksMade( ABC_Manager mng );
-extern uint64                ABC_GetTotalInspectsMade( ABC_Manager mng );
-
-// 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                   ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values);
-
-// initialize the solver internal data structure.
-extern void                  ABC_SolveInit(ABC_Manager mng);
-extern void                  ABC_AnalyzeTargets(ABC_Manager mng);
-
-// solve the targets added by ABC_AddTarget()
-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 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_TargetResFree( CSAT_Target_ResultT * p );
-
-extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/csat/module.make b/src/sat/csat/module.make
deleted file mode 100644
index 5b71a03c..00000000
--- a/src/sat/csat/module.make
+++ /dev/null
@@ -1 +0,0 @@
-SRC +=  src/sat/csat/csat_apis.c