src/sat/csat/csat_apis.c File Reference

#include "abc.h"
#include "fraig.h"
#include "csat_apis.h"
Include dependency graph for csat_apis.c:

Go to the source code of this file.

Data Structures

struct  ABC_ManagerStruct_t

Defines

#define ABC_DEFAULT_CONF_LIMIT   0
#define ABC_DEFAULT_IMP_LIMIT   0

Functions

static CSAT_Target_ResultT * ABC_TargetResAlloc (int nVars)
static char * ABC_GetNodeName (ABC_Manager mng, Abc_Obj_t *pNode)
void Abc_Start ()
void Abc_Stop ()
int Io_WriteBench (Abc_Ntk_t *pNtk, char *FileName)
ABC_Manager ABC_InitManager ()
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, uint64 num)
void ABC_SetTotalInspectLimit (ABC_Manager mng, uint64 num)
uint64 ABC_GetTotalBacktracksMade (ABC_Manager mng)
uint64 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)

Define Documentation

#define ABC_DEFAULT_CONF_LIMIT   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

] DECLARATIONS ///

Definition at line 27 of file csat_apis.c.

#define ABC_DEFAULT_IMP_LIMIT   0

Definition at line 28 of file csat_apis.c.

Function Documentation

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 170 of file csat_apis.c.

00171 {
00172     Abc_Obj_t * pObj, * pFanin;
00173     char * pSop, * pNewName;
00174     int i;
00175 
00176     // save the name in the local memory manager
00177     pNewName = Extra_MmFlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
00178     strcpy( pNewName, name );
00179     name = pNewName;
00180 
00181     // consider different cases, create the node, and map the node into the name
00182     switch( type )
00183     {
00184     case CSAT_BPI:
00185     case CSAT_BPPI:
00186         if ( nofi != 0 )
00187             { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
00188         // create the PI
00189         pObj = Abc_NtkCreatePi( mng->pNtk );
00190         stmm_insert( mng->tNode2Name, (char *)pObj, name );
00191         break;
00192     case CSAT_CONST:
00193     case CSAT_BAND:
00194     case CSAT_BNAND:
00195     case CSAT_BOR:
00196     case CSAT_BNOR:
00197     case CSAT_BXOR:
00198     case CSAT_BXNOR:
00199     case CSAT_BINV:
00200     case CSAT_BBUF:
00201         // create the node
00202         pObj = Abc_NtkCreateNode( mng->pNtk );
00203         // create the fanins
00204         for ( i = 0; i < nofi; i++ )
00205         {
00206             if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
00207                 { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
00208             Abc_ObjAddFanin( pObj, pFanin );
00209         }
00210         // create the node function
00211         switch( type )
00212         {
00213             case CSAT_CONST:
00214                 if ( nofi != 0 )
00215                     { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
00216                 pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
00217                 break;
00218             case CSAT_BAND:
00219                 if ( nofi < 1 )
00220                     { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
00221                 pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
00222                 break;
00223             case CSAT_BNAND:
00224                 if ( nofi < 1 )
00225                     { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
00226                 pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
00227                 break;
00228             case CSAT_BOR:
00229                 if ( nofi < 1 )
00230                     { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
00231                 pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
00232                 break;
00233             case CSAT_BNOR:
00234                 if ( nofi < 1 )
00235                     { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
00236                 pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
00237                 break;
00238             case CSAT_BXOR:
00239                 if ( nofi < 1 )
00240                     { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
00241                 if ( nofi > 2 )
00242                     { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
00243                 pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi );
00244                 break;
00245             case CSAT_BXNOR:
00246                 if ( nofi < 1 )
00247                     { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
00248                 if ( nofi > 2 )
00249                     { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
00250                 pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi );
00251                 break;
00252             case CSAT_BINV:
00253                 if ( nofi != 1 )
00254                     { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
00255                 pSop = Abc_SopCreateInv( mng->pNtk->pManFunc );
00256                 break;
00257             case CSAT_BBUF:
00258                 if ( nofi != 1 )
00259                     { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
00260                 pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
00261                 break;
00262             default :
00263                 break;
00264         }
00265         Abc_ObjSetData( pObj, pSop );
00266         break;
00267     case CSAT_BPPO:
00268     case CSAT_BPO:
00269         if ( nofi != 1 )
00270             { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
00271         // create the PO
00272         pObj = Abc_NtkCreatePo( mng->pNtk );
00273         stmm_insert( mng->tNode2Name, (char *)pObj, name );
00274         // connect to the PO fanin
00275         if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
00276             { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
00277         Abc_ObjAddFanin( pObj, pFanin );
00278         break;
00279     default:
00280         printf( "ABC_AddGate: Unknown gate type.\n" );
00281         break;
00282     }
00283 
00284     // map the name into the node
00285     if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
00286         { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
00287     return 1;
00288 }

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 527 of file csat_apis.c.

00528 {
00529     Abc_Obj_t * pObj;
00530     int i;
00531     if ( nog < 1 )
00532         { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; }
00533     // clear storage for the target
00534     mng->nog = 0;
00535     Vec_PtrClear( mng->vNodes );
00536     Vec_IntClear( mng->vValues );
00537     // save the target
00538     for ( i = 0; i < nog; i++ )
00539     {
00540         if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
00541             { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
00542         Vec_PtrPush( mng->vNodes, pObj );
00543         if ( values[i] < 0 || values[i] > 1 )
00544             { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
00545         Vec_IntPush( mng->vValues, values[i] );
00546     }
00547     mng->nog = nog;
00548     return 1;
00549 }

void ABC_AnalyzeTargets ( ABC_Manager  mng  ) 

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

Synopsis [Currently not implemented.]

Description []

SideEffects []

SeeAlso []

Definition at line 589 of file csat_apis.c.

00590 {
00591 }

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 325 of file csat_apis.c.

00326 {
00327     Abc_Ntk_t * pNtk = mng->pNtk;
00328     Abc_Obj_t * pObj;
00329     int i;
00330 
00331     // check that there are no dangling nodes
00332     Abc_NtkForEachNode( pNtk, pObj, i )
00333     {
00334         if ( i == 0 ) 
00335             continue;
00336         if ( Abc_ObjFanoutNum(pObj) == 0 )
00337         {
00338 //            printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
00339             return 0;
00340         }
00341     }
00342 
00343     // make sure everything is okay with the network structure
00344     if ( !Abc_NtkDoCheck( pNtk ) )
00345     {
00346         printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
00347         return 0;
00348     }
00349     return 1;
00350 }

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 673 of file csat_apis.c.

00674 {
00675     Abc_Ntk_t * pNtkTemp, * pNtkAig;
00676     char * pFileName;
00677  
00678     // derive the netlist
00679     pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 );
00680     pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
00681     Abc_NtkDelete( pNtkAig );
00682     if ( pNtkTemp == NULL ) 
00683         { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
00684     pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
00685     Io_WriteBench( pNtkTemp, pFileName );
00686     Abc_NtkDelete( pNtkTemp );
00687 }

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 506 of file csat_apis.c.

00507 {
00508     FREE( mng->pDumpFileName );
00509     mng->pDumpFileName = Extra_UtilStrsav( dump_file );
00510 }

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 657 of file csat_apis.c.

00658 {
00659     return mng->pResult;
00660 }

char * ABC_GetNodeName ( ABC_Manager  mng,
Abc_Obj_t *  pNode 
) [static]

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

Synopsis [Dumps the target AIG into the BENCH file.]

Description []

SideEffects []

SeeAlso []

Definition at line 754 of file csat_apis.c.

00755 {
00756     char * pName = NULL;
00757     if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
00758     {
00759         assert( 0 );
00760     }
00761     return pName;
00762 }

uint64 ABC_GetTotalBacktracksMade ( ABC_Manager  mng  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 474 of file csat_apis.c.

00475 {
00476     return mng->Params.nTotalBacktracksMade;
00477 }

uint64 ABC_GetTotalInspectsMade ( ABC_Manager  mng  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 490 of file csat_apis.c.

00491 {
00492     return mng->Params.nTotalInspectsMade;
00493 }

ABC_Manager ABC_InitManager ( void   ) 

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file csat_apis.c.

00077 {
00078     ABC_Manager_t * mng;
00079     Abc_Start();
00080     mng = ALLOC( ABC_Manager_t, 1 );
00081     memset( mng, 0, sizeof(ABC_Manager_t) );
00082     mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
00083     mng->pNtk->pName = Extra_UtilStrsav("csat_network");
00084     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
00085     mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
00086     mng->pMmNames   = Extra_MmFlexStart();
00087     mng->vNodes     = Vec_PtrAlloc( 100 );
00088     mng->vValues    = Vec_IntAlloc( 100 );
00089     mng->mode       = 0; // set "resource-aware integration" as the default mode
00090     // set default parameters for CEC
00091     Prove_ParamsSetDefault( &mng->Params );
00092     // set infinite resource limit for the final mitering
00093 //    mng->Params.nMiteringLimitLast = ABC_INFINITY;
00094     return mng;
00095 }

void ABC_Network_Finalize ( ABC_Manager  mng  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file csat_apis.c.

00302 {
00303     Abc_Ntk_t * pNtk = mng->pNtk;
00304     Abc_Obj_t * pObj;
00305     int i;
00306     Abc_NtkForEachPi( pNtk, pObj, i )
00307         Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
00308     Abc_NtkForEachPo( pNtk, pObj, i )
00309         Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
00310     assert( Abc_NtkLatchNum(pNtk) == 0 );
00311 }

void ABC_ReleaseManager ( ABC_Manager  mng  ) 

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

Synopsis [Deletes the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file csat_apis.c.

00109 {
00110     CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
00111     ABC_TargetResFree(p_res);
00112     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
00113     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
00114     if ( mng->pMmNames )   Extra_MmFlexStop( mng->pMmNames );
00115     if ( mng->pNtk )       Abc_NtkDelete( mng->pNtk );
00116     if ( mng->pTarget )    Abc_NtkDelete( mng->pTarget );
00117     if ( mng->vNodes )     Vec_PtrFree( mng->vNodes );
00118     if ( mng->vValues )    Vec_IntFree( mng->vValues );
00119     FREE( mng->pDumpFileName );
00120     free( mng );
00121     Abc_Stop();
00122 }

void ABC_SetLearnBacktrackLimit ( ABC_Manager  mng,
int  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 395 of file csat_apis.c.

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

void ABC_SetLearnLimit ( ABC_Manager  mng,
int  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file csat_apis.c.

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

void ABC_SetSolveBacktrackLimit ( ABC_Manager  mng,
int  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 411 of file csat_apis.c.

00412 {
00413     mng->Params.nMiteringLimitLast = num;
00414 }

void ABC_SetSolveImplicationLimit ( ABC_Manager  mng,
int  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file csat_apis.c.

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

void ABC_SetSolveOption ( ABC_Manager  mng,
enum CSAT_OptionT  option 
)

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

Synopsis [Sets solver options for learning.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file csat_apis.c.

00136 {
00137 }

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 363 of file csat_apis.c.

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

void ABC_SetTotalBacktrackLimit ( ABC_Manager  mng,
uint64  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file csat_apis.c.

00444 {
00445     mng->Params.nTotalBacktrackLimit = num;
00446 }

void ABC_SetTotalInspectLimit ( ABC_Manager  mng,
uint64  num 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 459 of file csat_apis.c.

00460 {
00461     mng->Params.nTotalInspectLimit = num;
00462 }

enum CSAT_StatusT ABC_Solve ( ABC_Manager  mng  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 604 of file csat_apis.c.

00605 {
00606     Prove_Params_t * pParams = &mng->Params;
00607     int RetValue, i;
00608 
00609     // check if the target network is available
00610     if ( mng->pTarget == NULL )
00611         { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
00612 
00613     // try to prove the miter using a number of techniques
00614     if ( mng->mode )
00615         RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
00616     else
00617 //        RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
00618         RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
00619 
00620     // analyze the result
00621     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
00622     if ( RetValue == -1 )
00623         mng->pResult->status = UNDETERMINED;
00624     else if ( RetValue == 1 )
00625         mng->pResult->status = UNSATISFIABLE;
00626     else if ( RetValue == 0 )
00627     {
00628         mng->pResult->status = SATISFIABLE;
00629         // create the array of PI names and values
00630         for ( i = 0; i < mng->pResult->no_sig; i++ )
00631         {
00632             mng->pResult->names[i]  = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) ); 
00633             mng->pResult->values[i] = mng->pTarget->pModel[i];
00634         }
00635         FREE( mng->pTarget->pModel );
00636     }
00637     else assert( 0 );
00638 
00639     // delete the target
00640     Abc_NtkDelete( mng->pTarget );
00641     mng->pTarget = NULL;
00642     // return the status
00643     return mng->pResult->status;
00644 }

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 563 of file csat_apis.c.

00564 {
00565     // check if the target is available
00566     assert( mng->nog == Vec_PtrSize(mng->vNodes) );
00567     if ( mng->nog == 0 )
00568         { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
00569 
00570     // free the previous target network if present
00571     if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
00572 
00573     // set the new target network
00574 //    mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
00575     mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1, 0 );
00576 }

void Abc_Start (  ) 

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 253 of file main.c.

00254 {
00255     Abc_Frame_t * pAbc;
00256     // added to detect memory leaks:
00257 #ifdef _DEBUG
00258     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
00259 #endif
00260     // start the glocal frame
00261     pAbc = Abc_FrameGetGlobalFrame();
00262     // source the resource file
00263 //    Abc_UtilsSource( pAbc );
00264 }

void Abc_Stop (  ) 

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

Synopsis [Deallocation procedure for the library project.]

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file main.c.

00278 {
00279     Abc_Frame_t * pAbc;
00280     pAbc = Abc_FrameGetGlobalFrame();
00281     // perform uninitializations
00282     Abc_FrameEnd( pAbc );
00283     // stop the framework
00284     Abc_FrameDeallocate( pAbc );
00285 }

CSAT_Target_ResultT * ABC_TargetResAlloc ( int  nVars  )  [static]

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

Synopsis [Allocates the target result.]

Description []

SideEffects []

SeeAlso []

Definition at line 702 of file csat_apis.c.

00703 {
00704     CSAT_Target_ResultT * p;
00705     p = ALLOC( CSAT_Target_ResultT, 1 );
00706     memset( p, 0, sizeof(CSAT_Target_ResultT) );
00707     p->no_sig = nVars;
00708     p->names = ALLOC( char *, nVars );
00709     p->values = ALLOC( int, nVars );
00710     memset( p->names, 0, sizeof(char *) * nVars );
00711     memset( p->values, 0, sizeof(int) * nVars );
00712     return p;
00713 }

void ABC_TargetResFree ( CSAT_Target_ResultT *  p  ) 

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

Synopsis [Deallocates the target result.]

Description []

SideEffects []

SeeAlso []

Definition at line 726 of file csat_apis.c.

00727 {
00728     if ( p == NULL )
00729         return;
00730     if( p->names )
00731     {
00732         int i = 0;
00733         for ( i = 0; i < p->no_sig; i++ )
00734         {
00735             FREE(p->names[i]);
00736         }
00737     }
00738     FREE( p->names );
00739     FREE( p->values );
00740     free( p );
00741 }

void ABC_UseOnlyCoreSatSolver ( ABC_Manager  mng  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file csat_apis.c.

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

int Io_WriteBench ( Abc_Ntk_t *  pNtk,
char *  pFileName 
)

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

Synopsis [Writes the network in BENCH format.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file ioWriteBench.c.

00051 {
00052     Abc_Ntk_t * pExdc;
00053     FILE * pFile;
00054     assert( Abc_NtkIsSopNetlist(pNtk) );
00055     if ( !Io_WriteBenchCheckNames(pNtk) )
00056     {
00057         fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
00058         return 0;
00059     }
00060     pFile = fopen( pFileName, "w" );
00061     if ( pFile == NULL )
00062     {
00063         fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
00064         return 0;
00065     }
00066     fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
00067     // write the network
00068     Io_WriteBenchOne( pFile, pNtk );
00069     // write EXDC network if it exists
00070     pExdc = Abc_NtkExdc( pNtk );
00071     if ( pExdc )
00072         printf( "Io_WriteBench: EXDC is not written (warning).\n" );
00073     // finalize the file
00074     fclose( pFile );
00075     return 1;
00076 }

Generated on Tue Jan 5 12:19:37 2010 for abc70930 by  doxygen 1.6.1