diff options
Diffstat (limited to 'src/sat/csat/csat_apis.h')
| -rw-r--r-- | src/sat/csat/csat_apis.h | 106 |
1 files changed, 53 insertions, 53 deletions
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index e567241f..3e04c7df 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -16,8 +16,8 @@ ***********************************************************************/ -#ifndef __CSAT_APIS_H__ -#define __CSAT_APIS_H__ +#ifndef __ABC_APIS_H__ +#define __ABC_APIS_H__ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// @@ -32,37 +32,37 @@ //////////////////////////////////////////////////////////////////////// -typedef struct CSAT_ManagerStruct_t CSAT_Manager_t; -typedef struct CSAT_ManagerStruct_t * CSAT_Manager; +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 -// CSAT_AddGate(); -#ifndef _CSAT_GATE_TYPE_ -#define _CSAT_GATE_TYPE_ +// 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_BPPO, // bit level PSEUDO PRIMARY OUTPUT - CSAT_BPO // boolean PO + ABC_CONST = 0, // constant gate + ABC_BPI, // boolean PI + ABC_BPPI, // bit level PSEUDO PRIMARY INPUT + ABC_BAND, // bit level AND + ABC_BNAND, // bit level NAND + ABC_BOR, // bit level OR + ABC_BNOR, // bit level NOR + ABC_BXOR, // bit level XOR + ABC_BXNOR, // bit level XNOR + ABC_BINV, // bit level INVERTER + ABC_BBUF, // bit level BUFFER + ABC_BPPO, // bit level PSEUDO PRIMARY OUTPUT + ABC_BPO // boolean PO }; #endif -//CSAT_StatusT defines the return value by CSAT_Solve(); -#ifndef _CSAT_STATUS_ -#define _CSAT_STATUS_ -enum CSAT_StatusT +//ABC_StatusT defines the return value by ABC_Solve(); +#ifndef _ABC_STATUS_ +#define _ABC_STATUS_ +enum ABC_StatusT { UNDETERMINED = 0, UNSATISFIABLE, @@ -76,11 +76,11 @@ enum CSAT_StatusT #endif -// CSAT_OptionT defines the solver option about learning -// which is used by CSAT_SetSolveOption(); -#ifndef _CSAT_OPTION_ -#define _CSAT_OPTION_ -enum CSAT_OptionT +// ABC_OptionT defines the solver option about learning +// which is used by ABC_SetSolveOption(); +#ifndef _ABC_OPTION_ +#define _ABC_OPTION_ +enum ABC_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, //default @@ -89,12 +89,12 @@ enum CSAT_OptionT #endif -#ifndef _CSAT_Target_Result -#define _CSAT_Target_Result -typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; -struct _CSAT_Target_ResultT +#ifndef _ABC_Target_Result +#define _ABC_Target_Result +typedef struct _ABC_Target_ResultT ABC_Target_ResultT; +struct _ABC_Target_ResultT { - enum CSAT_StatusT status; // solve status of the target + enum ABC_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 @@ -118,10 +118,10 @@ struct _CSAT_Target_ResultT //////////////////////////////////////////////////////////////////////// // create a new manager -extern CSAT_Manager CSAT_InitManager(void); +extern ABC_Manager ABC_InitManager(void); // set solver options for learning -extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option); +extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option); // add a gate to the circuit // the meaning of the parameters are: @@ -129,7 +129,7 @@ extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt // 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 CSAT_AddGate(CSAT_Manager mng, +extern int ABC_AddGate(ABC_Manager mng, enum GateType type, char* name, int nofi, @@ -138,38 +138,38 @@ extern int CSAT_AddGate(CSAT_Manager mng, // 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 CSAT_Check_Integrity(CSAT_Manager mng); +extern int ABC_Check_Integrity(ABC_Manager mng); // set time limit for solving a target. // runtime: time limit (in second). -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); +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); // 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 CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values); +extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values); // initialize the solver internal data structure. -extern void CSAT_SolveInit(CSAT_Manager mng); -extern void CSAT_AnalyzeTargets(CSAT_Manager mng); +extern void ABC_SolveInit(ABC_Manager mng); +extern void ABC_AnalyzeTargets(ABC_Manager mng); -// solve the targets added by CSAT_AddTarget() -extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng); +// solve the targets added by ABC_AddTarget() +extern enum ABC_StatusT ABC_Solve(ABC_Manager mng); // get the solve status of a target -// 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); +// TargetID: the target id returned by ABC_AddTarget(). +extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID); +extern void ABC_Dump_Bench_File(ABC_Manager mng); // ADDED PROCEDURES: -extern void CSAT_QuitManager( CSAT_Manager mng ); -extern void CSAT_TargetResFree( CSAT_Target_ResultT * p ); +extern void ABC_QuitManager( ABC_Manager mng ); +extern void ABC_TargetResFree( ABC_Target_ResultT * p ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |