From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/sat/csat/csat_apis.h | 222 ----------------------------------------------- 1 file changed, 222 deletions(-) delete mode 100644 src/sat/csat/csat_apis.h (limited to 'src/sat/csat/csat_apis.h') diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h deleted file mode 100644 index b80eddbf..00000000 --- a/src/sat/csat/csat_apis.h +++ /dev/null @@ -1,222 +0,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 ] - - 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 $] - -***********************************************************************/ - -#ifndef __ABC_APIS_H__ -#define __ABC_APIS_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - - -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 -// 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_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) -}; -#endif - - -//CSAT_StatusT defines the return value by ABC_Solve(); -#ifndef _ABC_STATUS_ -#define _ABC_STATUS_ -enum CSAT_StatusT -{ - UNDETERMINED = 0, - UNSATISFIABLE, - SATISFIABLE, - TIME_OUT, - FRAME_OUT, - NO_TARGET, - ABORTED, - SEQ_SATISFIABLE -}; -#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_ -enum CSAT_OptionT -{ - BASE_LINE = 0, - IMPLICT_LEARNING, //default - EXPLICT_LEARNING -}; -#endif - - -#ifndef _ABC_Target_Result -#define _ABC_Target_Result -typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; -struct _CSAT_Target_ResultT -{ - enum CSAT_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 - int num_cfts; // num of conflict signals in conflict gates - double time; // time(in second) used to solve the target - int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of - // primary inputs, if the "status" is TIME_OUT, "no_sig" is the - // number of constant signals found. - char** names; // if the "status" is SATISFIABLE, "names" is the name array of - // primary inputs, "values" is the value array of primary - // inputs that satisfy the target. - // if the "status" is TIME_OUT, "names" is the name array of - // constant signals found (signals at the root of decision - // tree), "values" is the value array of constant signals found. - int* values; -}; -#endif - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -// create a new manager -extern ABC_Manager ABC_InitManager(void); - -// release a manager -extern void ABC_ReleaseManager(ABC_Manager mng); - -// 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); - - -// add a gate to the circuit -// 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 -extern int ABC_AddGate(ABC_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 ); - -// 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 ); - -// 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); - -// initialize the solver internal data structure. -extern void ABC_SolveInit(ABC_Manager mng); -extern void ABC_AnalyzeTargets(ABC_Manager mng); - -// solve the targets added by ABC_AddTarget() -extern enum CSAT_StatusT ABC_Solve(ABC_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 - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// -- cgit v1.2.3