csat_apis.c File Reference

#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "csat_apis.h"
#include "misc/st/stmm.h"
#include "base/main/main.h"

Include dependency graph for csat_apis.c:

Go to the source code of this file.

Classes
struct	ABC_ManagerStruct_t

Macros
#define	ABC_DEFAULT_CONF_LIMIT   0
	DECLARATIONS ///.
#define	ABC_DEFAULT_IMP_LIMIT   0

Functions
void	Abc_Start ()
	DECLARATIONS ///.
void	Abc_Stop ()
int	Io_WriteBench (Abc_Ntk_t *pNtk, const char *FileName)
	FUNCTION DEFINITIONS ///.
ABC_Manager	ABC_InitManager ()
	FUNCTION DEFINITIONS ///.
void	ABC_ReleaseManager (ABC_Manager mng)
void	ABC_SetSolveOption (ABC_Manager mng, enum CSAT_OptionT option)
void	ABC_UseOnlyCoreSatSolver (ABC_Manager mng)
int	ABC_AddGate (ABC_Manager mng, enum GateType type, char *name, int nofi, char **fanins, int dc_attr)
void	ABC_Network_Finalize (ABC_Manager mng)
int	ABC_Check_Integrity (ABC_Manager mng)
void	ABC_SetTimeLimit (ABC_Manager mng, int runtime)
void	ABC_SetLearnLimit (ABC_Manager mng, int num)
void	ABC_SetLearnBacktrackLimit (ABC_Manager mng, int num)
void	ABC_SetSolveBacktrackLimit (ABC_Manager mng, int num)
void	ABC_SetSolveImplicationLimit (ABC_Manager mng, int num)
void	ABC_SetTotalBacktrackLimit (ABC_Manager mng, ABC_UINT64_T num)
void	ABC_SetTotalInspectLimit (ABC_Manager mng, ABC_UINT64_T num)
ABC_UINT64_T	ABC_GetTotalBacktracksMade (ABC_Manager mng)
ABC_UINT64_T	ABC_GetTotalInspectsMade (ABC_Manager mng)
void	ABC_EnableDump (ABC_Manager mng, char *dump_file)
int	ABC_AddTarget (ABC_Manager mng, int nog, char **names, int *values)
void	ABC_SolveInit (ABC_Manager mng)
void	ABC_AnalyzeTargets (ABC_Manager mng)
enum CSAT_StatusT	ABC_Solve (ABC_Manager mng)
CSAT_Target_ResultT *	ABC_Get_Target_Result (ABC_Manager mng, int TargetID)
void	ABC_Dump_Bench_File (ABC_Manager mng)
void	ABC_TargetResFree (CSAT_Target_ResultT *p)

Macro Definition Documentation

ABC_DEFAULT_CONF_LIMIT

#define ABC_DEFAULT_CONF_LIMIT   0

DECLARATIONS ///.

CFile****************************************************************

FileName [csat_apis.h]

PackageName [Interface to CSAT.]

Synopsis [APIs, enums, and data structures expected from the use of CSAT.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

]

Definition at line 32 of file csat_apis.c.

ABC_DEFAULT_IMP_LIMIT

#define ABC_DEFAULT_IMP_LIMIT   0

Definition at line 33 of file csat_apis.c.

Function Documentation

ABC_AddGate()

int ABC_AddGate	(	ABC_Manager	mng,
		enum GateType	type,
		char *	name,
		int	nofi,
		char **	fanins,
		int	dc_attr )

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 []

Definition at line 175 of file csat_apis.c.

{
    Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
    Abc_Obj_t * pFanin;
    char * pSop = NULL; // Suppress "might be used uninitialized"
    char * pNewName;
    int i;
 
    // save the name in the local memory manager
    pNewName = Mem_FlexEntryFetch( 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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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( (Mem_Flex_t *)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;
}

Here is the call graph for this function:

ABC_AddTarget()

int ABC_AddTarget	(	ABC_Manager	mng,
		int	nog,
		char **	names,
		int *	values )

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 []

Definition at line 534 of file csat_apis.c.

{
    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;
}

Here is the call graph for this function:

ABC_AnalyzeTargets()

void ABC_AnalyzeTargets

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [Currently not implemented.]

Description []

SideEffects []

SeeAlso []

Definition at line 596 of file csat_apis.c.

{
}

ABC_Check_Integrity()

int ABC_Check_Integrity

(

ABC_Manager

mng

)

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 []

Definition at line 332 of file csat_apis.c.

{
    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;
}

Here is the call graph for this function:

ABC_Dump_Bench_File()

void ABC_Dump_Bench_File

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [Dumps the original network into the BENCH file.]

Description [This procedure should be modified to dump the target.]

SideEffects []

SeeAlso []

Definition at line 680 of file csat_apis.c.

{
    Abc_Ntk_t * pNtkTemp, * pNtkAig;
    const 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 );
}

Here is the call graph for this function:

ABC_EnableDump()

void ABC_EnableDump	(	ABC_Manager	mng,
		char *	dump_file )

Function*************************************************************

Synopsis [Sets the file name to dump the structurally hashed network used for solving.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file csat_apis.c.

{
    ABC_FREE( mng->pDumpFileName );
    mng->pDumpFileName = Extra_UtilStrsav( dump_file );
}

Here is the call graph for this function:

ABC_Get_Target_Result()

CSAT_Target_ResultT * ABC_Get_Target_Result	(	ABC_Manager	mng,
		int	TargetID )

Function*************************************************************

Synopsis [Gets the solve status of a target.]

Description [TargetID: the target id returned by ABC_AddTarget().]

SideEffects []

SeeAlso []

Definition at line 664 of file csat_apis.c.

{
    return mng->pResult;
}

Here is the caller graph for this function:

ABC_GetTotalBacktracksMade()

ABC_UINT64_T ABC_GetTotalBacktracksMade

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file csat_apis.c.

{
    return mng->Params.nTotalBacktracksMade;
}

ABC_GetTotalInspectsMade()

ABC_UINT64_T ABC_GetTotalInspectsMade

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file csat_apis.c.

{
    return mng->Params.nTotalInspectsMade;
}

ABC_InitManager()

ABC_Manager ABC_InitManager

(

void

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file csat_apis.c.

{
    ABC_Manager_t * mng;
    Abc_Start();
    mng = ABC_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   = Mem_FlexStart();
    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;
}

Here is the call graph for this function:

ABC_Network_Finalize()

void ABC_Network_Finalize

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [This procedure also finalizes construction of the ABC network.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file csat_apis.c.

{
    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 );
}

Here is the call graph for this function:

ABC_ReleaseManager()

void ABC_ReleaseManager

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [Deletes the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file csat_apis.c.

{
    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 )   Mem_FlexStop( mng->pMmNames, 0 );
    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 );
    ABC_FREE( mng->pDumpFileName );
    ABC_FREE( mng );
    Abc_Stop();
}

Here is the call graph for this function:

ABC_SetLearnBacktrackLimit()

void ABC_SetLearnBacktrackLimit	(	ABC_Manager	mng,
		int	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file csat_apis.c.

{
//    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
}

ABC_SetLearnLimit()

void ABC_SetLearnLimit	(	ABC_Manager	mng,
		int	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file csat_apis.c.

{
//    printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
}

ABC_SetSolveBacktrackLimit()

void ABC_SetSolveBacktrackLimit	(	ABC_Manager	mng,
		int	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 418 of file csat_apis.c.

{
    mng->Params.nMiteringLimitLast = num;
}

ABC_SetSolveImplicationLimit()

void ABC_SetSolveImplicationLimit	(	ABC_Manager	mng,
		int	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 434 of file csat_apis.c.

{
//    printf( "ABC_SetSolveImplicationLimit: The resource limit is not implemented (warning).\n" );
}

ABC_SetSolveOption()

void ABC_SetSolveOption	(	ABC_Manager	mng,
		enum CSAT_OptionT	option )

Function*************************************************************

Synopsis [Sets solver options for learning.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file csat_apis.c.

{
}

ABC_SetTimeLimit()

void ABC_SetTimeLimit	(	ABC_Manager	mng,
		int	runtime )

Function*************************************************************

Synopsis [Sets time limit for solving a target.]

Description [Runtime: time limit (in second).]

SideEffects []

SeeAlso []

Definition at line 370 of file csat_apis.c.

{
//    printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
}

Here is the call graph for this function:

ABC_SetTotalBacktrackLimit()

void ABC_SetTotalBacktrackLimit	(	ABC_Manager	mng,
		ABC_UINT64_T	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file csat_apis.c.

{
    mng->Params.nTotalBacktrackLimit = num;
}

ABC_SetTotalInspectLimit()

void ABC_SetTotalInspectLimit	(	ABC_Manager	mng,
		ABC_UINT64_T	num )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 466 of file csat_apis.c.

{
    mng->Params.nTotalInspectLimit = num;
}

ABC_Solve()

enum CSAT_StatusT ABC_Solve

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [Solves the targets added by ABC_AddTarget().]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file csat_apis.c.

{
    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, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)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];
        }
        ABC_FREE( mng->pTarget->pModel );
    }
    else assert( 0 );
 
    // delete the target
    Abc_NtkDelete( mng->pTarget );
    mng->pTarget = NULL;
    // return the status
    return mng->pResult->status;
}

Here is the call graph for this function:

ABC_SolveInit()

void ABC_SolveInit

(

ABC_Manager

mng

)

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 []

Definition at line 570 of file csat_apis.c.

{
    // 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 );
}

Here is the call graph for this function:

Abc_Start()

void Abc_Start ( )

extern

DECLARATIONS ///.

INCLUDES ///.

FUNCTION DECLARATIONS ///.

CFile****************************************************************

FileName [main.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The main package.]

Synopsis [Here everything starts.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Initialization procedure for the library project.]

Description [Note that when Abc_Start() is run in a static library project, it does not load the resource file by default. As a result, ABC is not set up the same way, as when it is run on a command line. For example, some error messages while parsing files will not be produced, and intermediate networks will not be checked for consistancy. One possibility is to load the resource file after Abc_Start() as follows: Abc_UtilsSource( Abc_FrameGetGlobalFrame() );]

SideEffects []

SeeAlso []

Definition at line 52 of file mainLib.c.

{
    Abc_Frame_t * pAbc;
    // added to detect memory leaks:
#if defined(_DEBUG) && defined(_MSC_VER) 
    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
    // start the glocal frame
    pAbc = Abc_FrameGetGlobalFrame();
    // source the resource file
//    Abc_UtilsSource( pAbc );
}

Here is the caller graph for this function:

Abc_Stop()

void Abc_Stop ( )

extern

Function*************************************************************

Synopsis [Deallocation procedure for the library project.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file mainLib.c.

{
    Abc_Frame_t * pAbc;
    pAbc = Abc_FrameGetGlobalFrame();
    // perform uninitializations
    Abc_FrameEnd( pAbc );
    // stop the framework
    Abc_FrameDeallocate( pAbc );
}

Here is the caller graph for this function:

ABC_TargetResFree()

void ABC_TargetResFree

(

CSAT_Target_ResultT *

p

)

Function*************************************************************

Synopsis [Deallocates the target result.]

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file csat_apis.c.

{
    if ( p == NULL )
        return;
    if( p->names )
    {
        int i = 0;
        for ( i = 0; i < p->no_sig; i++ )
        {
            ABC_FREE(p->names[i]);
        }
    }
    ABC_FREE( p->names );
    ABC_FREE( p->values );
    ABC_FREE( p );
}

Here is the caller graph for this function:

ABC_UseOnlyCoreSatSolver()

void ABC_UseOnlyCoreSatSolver

(

ABC_Manager

mng

)

Function*************************************************************

Synopsis [Sets solving mode by brute-force SAT.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file csat_apis.c.

{
    mng->mode = 1;  // switch to "brute-force SAT" as the solving option
}

Io_WriteBench()

int Io_WriteBench ( Abc_Ntk_t * pNtk, const char * pFileName )

extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Writes the network in BENCH format.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file ioWriteBench.c.

{
    Abc_Ntk_t * pExdc;
    FILE * pFile;
    assert( Abc_NtkIsSopNetlist(pNtk) );
    if ( !Io_WriteBenchCheckNames(pNtk) )
    {
        fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parentheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
        return 0;
    }
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
        return 0;
    }
    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
    // write the network
    Io_WriteBenchOne( pFile, pNtk );
    // write EXDC network if it exists
    pExdc = Abc_NtkExdc( pNtk );
    if ( pExdc )
        printf( "Io_WriteBench: EXDC is not written (warning).\n" );
    // finalize the file
    fclose( pFile );
    return 1;
}

Here is the caller graph for this function: