summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatInt.h
blob: 03903abea1b44db8f63b4190d0dd502ad449b787 (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
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