summaryrefslogtreecommitdiffstats
path: root/src/sat/csat/csat_apis.h
blob: b80eddbf3c2bd125519154d6e3407847d94f3c3d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
/**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                                ///
////////////////////////////////////////////////////////////////////////