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
|
/* minisat.h */
/* Modified by Andrew Makhorin <mao@gnu.org>, August 2011 */
/***********************************************************************
* MiniSat -- Copyright (c) 2005, Niklas Sorensson
* http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation files
* (the "Software"), to deal in the Software without restriction,
* including without limitation the rights to use, copy, modify, merge,
* publish, distribute, sublicense, and/or sell copies of the Software,
* and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
* BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
* ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
***********************************************************************/
/* Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko */
#ifndef MINISAT_H
#define MINISAT_H
/*====================================================================*/
/* Simple types: */
typedef int bool;
#define true 1
#define false 0
typedef int lit;
#if 0 /* by mao */
typedef char lbool;
#else
typedef int lbool;
#endif
#define var_Undef (int)(-1)
#define lit_Undef (lit)(-2)
#define l_Undef (lbool)0
#define l_True (lbool)1
#define l_False (lbool)(-1)
#define toLit(v) (lit)((v) + (v))
#define lit_neg(l) (lit)((l) ^ 1)
#define lit_var(l) (int)((l) >> 1)
#define lit_sign(l) (int)((l) & 1)
/*====================================================================*/
/* Vectors: */
/* vector of 32-bit intergers (added for 64-bit portability) */
typedef struct /* veci_t */ {
int size;
int cap;
int* ptr;
} veci;
#define veci_new(v) \
{ (v)->size = 0; \
(v)->cap = 4; \
(v)->ptr = (int*)malloc(sizeof(int)*(v)->cap); \
}
#define veci_delete(v) free((v)->ptr)
#define veci_begin(v) ((v)->ptr)
#define veci_size(v) ((v)->size)
#define veci_resize(v, k) (void)((v)->size = (k))
/* only safe to shrink !! */
#define veci_push(v, e) \
{ if ((v)->size == (v)->cap) \
{ int newsize = (v)->cap * 2+1; \
(v)->ptr = (int*)realloc((v)->ptr,sizeof(int)*newsize); \
(v)->cap = newsize; \
} \
(v)->ptr[(v)->size++] = (e); \
}
/* vector of 32- or 64-bit pointers */
typedef struct /* vecp_t */ {
int size;
int cap;
void** ptr;
} vecp;
#define vecp_new(v) \
{ (v)->size = 0; \
(v)->cap = 4; \
(v)->ptr = (void**)malloc(sizeof(void*)*(v)->cap); \
}
#define vecp_delete(v) free((v)->ptr)
#define vecp_begin(v) ((v)->ptr)
#define vecp_size(v) ((v)->size)
#define vecp_resize(v, k) (void)((v)->size = (k))
/* only safe to shrink !! */
#define vecp_push(v, e) \
{ if ((v)->size == (v)->cap) \
{ int newsize = (v)->cap * 2+1; \
(v)->ptr = (void**)realloc((v)->ptr,sizeof(void*)*newsize); \
(v)->cap = newsize; \
} \
(v)->ptr[(v)->size++] = (e); \
}
/*====================================================================*/
/* Solver representation: */
typedef struct /* clause_t */
{
int size_learnt;
lit lits[1];
} clause;
typedef struct /* stats_t */
{
double starts, decisions, propagations, inspects, conflicts;
double clauses, clauses_literals, learnts, learnts_literals,
max_literals, tot_literals;
} stats;
typedef struct /* solver_t */
{
int size; /* nof variables */
int cap; /* size of varmaps */
int qhead; /* Head index of queue. */
int qtail; /* Tail index of queue. */
/* clauses */
vecp clauses; /* List of problem constraints.
(contains: clause*) */
vecp learnts; /* List of learnt clauses.
(contains: clause*) */
/* activities */
double var_inc; /* Amount to bump next variable with. */
double var_decay; /* INVERSE decay factor for variable
activity: stores 1/decay. */
float cla_inc; /* Amount to bump next clause with. */
float cla_decay; /* INVERSE decay factor for clause
activity: stores 1/decay. */
vecp* wlists;
double* activity; /* A heuristic measurement of the activity
of a variable. */
lbool* assigns; /* Current values of variables. */
int* orderpos; /* Index in variable order. */
clause** reasons;
int* levels;
lit* trail;
clause* binary; /* A temporary binary clause */
lbool* tags;
veci tagged; /* (contains: var) */
veci stack; /* (contains: var) */
veci order; /* Variable order. (heap) (contains: var) */
veci trail_lim; /* Separator indices for different decision
levels in 'trail'. (contains: int) */
veci model; /* If problem is solved, this vector
contains the model (contains: lbool). */
int root_level; /* Level of first proper decision. */
int simpdb_assigns;/* Number of top-level assignments at last
'simplifyDB()'. */
int simpdb_props; /* Number of propagations before next
'simplifyDB()'. */
double random_seed;
double progress_estimate;
int verbosity; /* Verbosity level.
0=silent,
1=some progress report,
2=everything */
stats stats;
} solver;
/*====================================================================*/
/* Public interface: */
#if 1 /* by mao; to keep namespace clean */
#define solver_new _glp_minisat_new
#define solver_delete _glp_minisat_delete
#define solver_addclause _glp_minisat_addclause
#define solver_simplify _glp_minisat_simplify
#define solver_solve _glp_minisat_solve
#define solver_nvars _glp_minisat_nvars
#define solver_nclauses _glp_minisat_nclauses
#define solver_nconflicts _glp_minisat_nconflicts
#define solver_setnvars _glp_minisat_setnvars
#define solver_propagate _glp_minisat_propagate
#define solver_reducedb _glp_minisat_reducedb
#endif
solver* solver_new(void);
void solver_delete(solver* s);
bool solver_addclause(solver* s, lit* begin, lit* end);
bool solver_simplify(solver* s);
bool solver_solve(solver* s, lit* begin, lit* end);
int solver_nvars(solver* s);
int solver_nclauses(solver* s);
int solver_nconflicts(solver* s);
void solver_setnvars(solver* s,int n);
#endif
/* eof */
|
