diff options
Diffstat (limited to 'src/sat/csat/csat_apis.h')
| -rw-r--r-- | src/sat/csat/csat_apis.h | 154 |
1 files changed, 53 insertions, 101 deletions
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index b80eddbf..124ca266 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -12,16 +12,12 @@ Date [Ver. 1.0. Started - August 28, 2005] - Revision [$Id: csat_apis.h,v 1.5 2005/12/30 10:54:40 rmukherj Exp $] + Revision [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $] ***********************************************************************/ -#ifndef __ABC_APIS_H__ -#define __ABC_APIS_H__ - -#ifdef __cplusplus -extern "C" { -#endif +#ifndef __CSAT_APIS_H__ +#define __CSAT_APIS_H__ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// @@ -36,44 +32,36 @@ extern "C" { //////////////////////////////////////////////////////////////////////// -typedef struct ABC_ManagerStruct_t ABC_Manager_t; -typedef struct ABC_ManagerStruct_t * ABC_Manager; +typedef struct CSAT_ManagerStruct_t CSAT_Manager_t; +typedef struct CSAT_ManagerStruct_t * CSAT_Manager; // GateType defines the gate type that can be added to circuit by -// ABC_AddGate(); -#ifndef _ABC_GATE_TYPE_ -#define _ABC_GATE_TYPE_ +// CSAT_AddGate(); +#ifndef _CSAT_GATE_TYPE_ +#define _CSAT_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) + 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_BPPO, // bit level PSEUDO PRIMARY OUTPUT + CSAT_BPO // boolean PO }; #endif -//CSAT_StatusT defines the return value by ABC_Solve(); -#ifndef _ABC_STATUS_ -#define _ABC_STATUS_ +//CSAT_StatusT defines the return value by CSAT_Solve(); +#ifndef _CSAT_STATUS_ +#define _CSAT_STATUS_ enum CSAT_StatusT { UNDETERMINED = 0, @@ -88,22 +76,10 @@ enum CSAT_StatusT #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_ +// which is used by CSAT_SetSolveOption(); +#ifndef _CSAT_OPTION_ +#define _CSAT_OPTION_ enum CSAT_OptionT { BASE_LINE = 0, @@ -113,8 +89,8 @@ enum CSAT_OptionT #endif -#ifndef _ABC_Target_Result -#define _ABC_Target_Result +#ifndef _CSAT_Target_Result +#define _CSAT_Target_Result typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; struct _CSAT_Target_ResultT { @@ -138,21 +114,14 @@ struct _CSAT_Target_ResultT #endif //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// // create a new manager -extern ABC_Manager ABC_InitManager(void); - -// release a manager -extern void ABC_ReleaseManager(ABC_Manager mng); +extern CSAT_Manager CSAT_InitManager(void); // 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); - +extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option); // add a gate to the circuit // the meaning of the parameters are: @@ -160,63 +129,46 @@ extern void ABC_UseOnlyCoreSatSolver(ABC_Manager mng); // 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); +extern int CSAT_AddGate(CSAT_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 ); +extern int CSAT_Check_Integrity(CSAT_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 ); +extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime); +extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num); +extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num); +extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num); +extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file); // 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); +extern int CSAT_AddTarget(CSAT_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); +extern void CSAT_SolveInit(CSAT_Manager mng); +extern void CSAT_AnalyzeTargets(CSAT_Manager mng); -// solve the targets added by ABC_AddTarget() -extern enum CSAT_StatusT ABC_Solve(ABC_Manager mng); +// solve the targets added by CSAT_AddTarget() +extern enum CSAT_StatusT CSAT_Solve(CSAT_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 +// TargetID: the target id returned by CSAT_AddTarget(). +extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID); +extern void CSAT_Dump_Bench_File(CSAT_Manager mng); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + +#endif |