src/sat/csat/csat_apis.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  _CSAT_Target_ResultT

Typedefs

typedef struct ABC_ManagerStruct_t ABC_Manager_t
typedef struct
ABC_ManagerStruct_t * 		ABC_Manager
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT

Enumerations

enum  GateType {
  CSAT_CONST = 0, CSAT_BPI, CSAT_BPPI, CSAT_BAND,
  CSAT_BNAND, CSAT_BOR, CSAT_BNOR, CSAT_BXOR,
  CSAT_BXNOR, CSAT_BINV, CSAT_BBUF, CSAT_BMUX,
  CSAT_BDFF, CSAT_BSDFF, CSAT_BTRIH, CSAT_BTRIL,
  CSAT_BBUS, CSAT_BPPO, CSAT_BPO, CSAT_BCNF,
  CSAT_BDC
}
enum  CSAT_StatusT {
  UNDETERMINED = 0, UNSATISFIABLE, SATISFIABLE, TIME_OUT,
  FRAME_OUT, NO_TARGET, ABORTED, SEQ_SATISFIABLE
}
enum  CSAT_CallerT { BLS = 0, SATORI, NONE }
enum  CSAT_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, EXPLICT_LEARNING }

Functions

ABC_Manager ABC_InitManager (void)
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)
int ABC_Check_Integrity (ABC_Manager mng)
void ABC_Network_Finalize (ABC_Manager mng)
void ABC_SetTimeLimit (ABC_Manager mng, int runtime)
void ABC_SetLearnLimit (ABC_Manager mng, int num)
void ABC_SetSolveBacktrackLimit (ABC_Manager mng, int num)
void ABC_SetLearnBacktrackLimit (ABC_Manager mng, int num)
void ABC_EnableDump (ABC_Manager mng, char *dump_file)
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)
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)
void CSAT_SetCaller (ABC_Manager mng, enum CSAT_CallerT caller)

Typedef Documentation

typedef struct ABC_ManagerStruct_t* ABC_Manager

Definition at line 40 of file csat_apis.h.

typedef struct ABC_ManagerStruct_t ABC_Manager_t

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

] INCLUDES /// PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 39 of file csat_apis.h.

typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT

Definition at line 118 of file csat_apis.h.

Enumeration Type Documentation

enum CSAT_CallerT
Enumerator:
BLS 
SATORI 
NONE 

Definition at line 94 of file csat_apis.h.

00095 {
00096     BLS = 0,
00097     SATORI,
00098     NONE
00099 };

enum CSAT_OptionT
Enumerator:
BASE_LINE 
IMPLICT_LEARNING 
EXPLICT_LEARNING 

Definition at line 107 of file csat_apis.h.

00108 {
00109     BASE_LINE = 0,
00110     IMPLICT_LEARNING, //default
00111     EXPLICT_LEARNING
00112 };

enum CSAT_StatusT
Enumerator:
UNDETERMINED 
UNSATISFIABLE 
SATISFIABLE 
TIME_OUT 
FRAME_OUT 
NO_TARGET 
ABORTED 
SEQ_SATISFIABLE 

Definition at line 77 of file csat_apis.h.

00078 {
00079     UNDETERMINED = 0,
00080     UNSATISFIABLE,
00081     SATISFIABLE,
00082     TIME_OUT,
00083     FRAME_OUT,
00084     NO_TARGET,
00085     ABORTED,
00086     SEQ_SATISFIABLE     
00087 };

enum GateType
Enumerator:
CSAT_CONST 
CSAT_BPI 
CSAT_BPPI 
CSAT_BAND 
CSAT_BNAND 
CSAT_BOR 
CSAT_BNOR 
CSAT_BXOR 
CSAT_BXNOR 
CSAT_BINV 
CSAT_BBUF 
CSAT_BMUX 
CSAT_BDFF 
CSAT_BSDFF 
CSAT_BTRIH 
CSAT_BTRIL 
CSAT_BBUS 
CSAT_BPPO 
CSAT_BPO 
CSAT_BCNF 
CSAT_BDC 

Definition at line 47 of file csat_apis.h.

00048 {
00049     CSAT_CONST = 0,  // constant gate
00050     CSAT_BPI,    // boolean PI
00051     CSAT_BPPI,   // bit level PSEUDO PRIMARY INPUT
00052     CSAT_BAND,   // bit level AND
00053     CSAT_BNAND,  // bit level NAND
00054     CSAT_BOR,    // bit level OR
00055     CSAT_BNOR,   // bit level NOR
00056     CSAT_BXOR,   // bit level XOR
00057     CSAT_BXNOR,  // bit level XNOR
00058     CSAT_BINV,   // bit level INVERTER
00059     CSAT_BBUF,   // bit level BUFFER
00060     CSAT_BMUX,   // bit level MUX --not supported 
00061     CSAT_BDFF,   // bit level D-type FF
00062     CSAT_BSDFF,  // bit level scan FF --not supported 
00063     CSAT_BTRIH,  // bit level TRISTATE gate with active high control --not supported 
00064     CSAT_BTRIL,  // bit level TRISTATE gate with active low control --not supported 
00065     CSAT_BBUS,   // bit level BUS --not supported 
00066     CSAT_BPPO,   // bit level PSEUDO PRIMARY OUTPUT
00067     CSAT_BPO,    // boolean PO
00068     CSAT_BCNF,   // boolean constraint
00069     CSAT_BDC,    // boolean don't care gate (2 input)
00070 };

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 }

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 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_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_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 }

void CSAT_SetCaller ( ABC_Manager  mng,
enum CSAT_CallerT  caller 
)
Generated on Tue Jan 5 12:19:37 2010 for abc70930 by  doxygen 1.6.1