csat_apis.h

Go to the documentation of this file.

 
#ifndef ABC__sat__csat__csat_apis_h
#define ABC__sat__csat__csat_apis_h
 


 
 
 
ABC_NAMESPACE_HEADER_START
 

 
 
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

 
// 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, ABC_UINT64_T num );
extern void                  ABC_SetTotalInspectLimit( ABC_Manager mng, ABC_UINT64_T num );
extern ABC_UINT64_T         ABC_GetTotalBacktracksMade( ABC_Manager mng );
extern ABC_UINT64_T         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);
 
 
 
ABC_NAMESPACE_HEADER_END
 
 
 
#endif