Version abc70930

1 files changed, 0 insertions, 222 deletions

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 <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 $]
-
-***********************************************************************/
-
-#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                                ///
-////////////////////////////////////////////////////////////////////////