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
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
|
/**CFile****************************************************************
FileName [msatInt.c]
PackageName [A C version of SAT solver MINISAT, originally developed
in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
Synopsis [Internal definitions of the solver.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 1, 2004.]
Revision [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __MSAT_INT_H__
#define __MSAT_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
//#include "leaks.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include <math.h>
#include "msat.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef _MSC_VER
typedef __int64 int64;
#else
typedef long long int64;
#endif
// outputs the runtime in seconds
#define PRT(a,t) \
printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
// memory management macros
#define ALLOC(type, num) \
((type *) malloc(sizeof(type) * (num)))
#define REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#define FREE(obj) \
((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
// By default, custom memory management is used
// which guarantees constant time allocation/deallocation
// for SAT clauses and other frequently modified objects.
// For debugging, it is possible use system memory management
// directly. In which case, uncomment the macro below.
//#define USE_SYSTEM_MEMORY_MANAGEMENT
// internal data structures
typedef struct Msat_Clause_t_ Msat_Clause_t;
typedef struct Msat_Queue_t_ Msat_Queue_t;
typedef struct Msat_Order_t_ Msat_Order_t;
// memory managers (duplicated from Extra for stand-aloneness)
typedef struct Msat_MmFixed_t_ Msat_MmFixed_t;
typedef struct Msat_MmFlex_t_ Msat_MmFlex_t;
typedef struct Msat_MmStep_t_ Msat_MmStep_t;
// variables and literals
typedef int Msat_Lit_t;
typedef int Msat_Var_t;
// the type of return value
#define MSAT_VAR_UNASSIGNED (-1)
#define MSAT_LIT_UNASSIGNED (-2)
#define MSAT_ORDER_UNKNOWN (-3)
// printing the search tree
#define L_IND "%-*d"
#define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
#define L_LIT "%s%d"
#define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
typedef struct Msat_SolverStats_t_ Msat_SolverStats_t;
struct Msat_SolverStats_t_
{
int64 nStarts; // the number of restarts
int64 nDecisions; // the number of decisions
int64 nPropagations; // the number of implications
int64 nInspects; // the number of times clauses are vising while watching them
int64 nConflicts; // the number of conflicts
int64 nSuccesses; // the number of sat assignments found
};
typedef struct Msat_SearchParams_t_ Msat_SearchParams_t;
struct Msat_SearchParams_t_
{
double dVarDecay;
double dClaDecay;
};
// sat solver data structure visible through all the internal files
struct Msat_Solver_t_
{
int nClauses; // the total number of clauses
int nClausesStart; // the number of clauses before adding
Msat_ClauseVec_t * vClauses; // problem clauses
Msat_ClauseVec_t * vLearned; // learned clauses
double dClaInc; // Amount to bump next clause with.
double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay.
double * pdActivity; // A heuristic measurement of the activity of a variable.
float * pFactors; // the multiplicative factors of variable activity
double dVarInc; // Amount to bump next variable with.
double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
Msat_Order_t * pOrder; // Keeps track of the decision variable order.
Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
Msat_Queue_t * pQueue; // Propagation queue.
int nVars; // the current number of variables
int nVarsAlloc; // the maximum allowed number of variables
int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN)
int * pModel; // The satisfying assignment
Msat_IntVec_t * vTrail; // List of assignments made.
Msat_IntVec_t * vTrailLim; // Separator indices for different decision levels in 'trail'.
Msat_Clause_t ** pReasons; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
int * pLevel; // 'level[var]' is the decision level at which assignment was made.
int nLevelRoot; // Level of first proper decision.
double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms).
bool fVerbose; // the verbosity flag
double dProgress; // Set by 'search()'.
// the variable cone and variable connectivity
Msat_IntVec_t * vConeVars;
Msat_IntVec_t * vVarsUsed;
Msat_ClauseVec_t * vAdjacents;
// internal data used during conflict analysis
int * pSeen; // time when a lit was seen for the last time
int nSeenId; // the id of current seeing
Msat_IntVec_t * vReason; // the temporary array of literals
Msat_IntVec_t * vTemp; // the temporary array of literals
int * pFreq; // the number of times each var participated in conflicts
// the memory manager
Msat_MmStep_t * pMem;
// statistics
Msat_SolverStats_t Stats;
int nTwoLits;
int nTwoLitsL;
int nClausesInit;
int nClausesAlloc;
int nClausesAllocL;
int nBackTracks;
};
struct Msat_ClauseVec_t_
{
Msat_Clause_t ** pArray;
int nSize;
int nCap;
};
struct Msat_IntVec_t_
{
int * pArray;
int nSize;
int nCap;
};
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== satActivity.c ===========================================================*/
extern void Msat_SolverVarDecayActivity( Msat_Solver_t * p );
extern void Msat_SolverVarRescaleActivity( Msat_Solver_t * p );
extern void Msat_SolverClaDecayActivity( Msat_Solver_t * p );
extern void Msat_SolverClaRescaleActivity( Msat_Solver_t * p );
/*=== satSolverApi.c ===========================================================*/
extern Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num );
/*=== satSolver.c ===========================================================*/
extern int Msat_SolverReadDecisionLevel( Msat_Solver_t * p );
extern int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p );
extern Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p );
extern Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var );
extern Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p );
extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p );
extern int * Msat_SolverReadSeenArray( Msat_Solver_t * p );
extern int Msat_SolverIncrementSeenId( Msat_Solver_t * p );
extern Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p );
extern void Msat_SolverClausesIncrement( Msat_Solver_t * p );
extern void Msat_SolverClausesDecrement( Msat_Solver_t * p );
extern void Msat_SolverClausesIncrementL( Msat_Solver_t * p );
extern void Msat_SolverClausesDecrementL( Msat_Solver_t * p );
extern void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit );
extern void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC );
extern bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
extern double Msat_SolverProgressEstimate( Msat_Solver_t * p );
/*=== satSolverSearch.c ===========================================================*/
extern bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
extern Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p );
extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
/*=== satQueue.c ===========================================================*/
extern Msat_Queue_t * Msat_QueueAlloc( int nVars );
extern void Msat_QueueFree( Msat_Queue_t * p );
extern int Msat_QueueReadSize( Msat_Queue_t * p );
extern void Msat_QueueInsert( Msat_Queue_t * p, int Lit );
extern int Msat_QueueExtract( Msat_Queue_t * p );
extern void Msat_QueueClear( Msat_Queue_t * p );
/*=== satOrder.c ===========================================================*/
extern Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat );
extern void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax );
extern void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone );
extern int Msat_OrderCheck( Msat_Order_t * p );
extern void Msat_OrderFree( Msat_Order_t * p );
extern int Msat_OrderVarSelect( Msat_Order_t * p );
extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
extern void Msat_OrderUpdate( Msat_Order_t * p, int Var );
/*=== satClause.c ===========================================================*/
extern bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out );
extern Msat_Clause_t * Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits );
extern Msat_Clause_t * Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit );
extern bool Msat_ClauseReadLearned( Msat_Clause_t * pC );
extern int Msat_ClauseReadSize( Msat_Clause_t * pC );
extern int * Msat_ClauseReadLits( Msat_Clause_t * pC );
extern bool Msat_ClauseReadMark( Msat_Clause_t * pC );
extern void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark );
extern int Msat_ClauseReadNum( Msat_Clause_t * pC );
extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
extern bool Msat_ClauseReadTypeA( Msat_Clause_t * pC );
extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA );
extern bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
extern float Msat_ClauseReadActivity( Msat_Clause_t * pC );
extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched );
extern bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
extern bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
extern void Msat_ClausePrint( Msat_Clause_t * pC );
extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC );
extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement );
extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
/*=== satSort.c ===========================================================*/
extern void Msat_SolverSortDB( Msat_Solver_t * p );
/*=== satClauseVec.c ===========================================================*/
extern Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap );
extern void Msat_ClauseVecFree( Msat_ClauseVec_t * p );
extern Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p );
extern int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p );
extern void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin );
extern void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew );
extern void Msat_ClauseVecClear( Msat_ClauseVec_t * p );
extern void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry );
extern Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p );
extern void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry );
extern Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i );
/*=== satMem.c ===========================================================*/
// fixed-size-block memory manager
extern Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize );
extern void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose );
extern char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p );
extern void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry );
extern void Msat_MmFixedRestart( Msat_MmFixed_t * p );
extern int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p );
// flexible-size-block memory manager
extern Msat_MmFlex_t * Msat_MmFlexStart();
extern void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose );
extern char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes );
extern int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p );
// hierarchical memory manager
extern Msat_MmStep_t * Msat_MmStepStart( int nSteps );
extern void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose );
extern char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes );
extern void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes );
extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
|
