lemon-project-template-glpk
comparison deps/glpk/src/minisat/minisat.h @ 11:4fc6ad2fb8a6
Test GLPK in src/main.cc
author | Alpar Juttner <alpar@cs.elte.hu> |
---|---|
date | Sun, 06 Nov 2011 21:43:29 +0100 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:423fad3d1698 |
---|---|
1 /* minisat.h */ | |
2 | |
3 /* Modified by Andrew Makhorin <mao@gnu.org>, August 2011 */ | |
4 | |
5 /*********************************************************************** | |
6 * MiniSat -- Copyright (c) 2005, Niklas Sorensson | |
7 * http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ | |
8 * | |
9 * Permission is hereby granted, free of charge, to any person | |
10 * obtaining a copy of this software and associated documentation files | |
11 * (the "Software"), to deal in the Software without restriction, | |
12 * including without limitation the rights to use, copy, modify, merge, | |
13 * publish, distribute, sublicense, and/or sell copies of the Software, | |
14 * and to permit persons to whom the Software is furnished to do so, | |
15 * subject to the following conditions: | |
16 * | |
17 * The above copyright notice and this permission notice shall be | |
18 * included in all copies or substantial portions of the Software. | |
19 * | |
20 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, | |
21 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF | |
22 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND | |
23 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS | |
24 * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN | |
25 * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN | |
26 * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE | |
27 * SOFTWARE. | |
28 ***********************************************************************/ | |
29 /* Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko */ | |
30 | |
31 #ifndef MINISAT_H | |
32 #define MINISAT_H | |
33 | |
34 /*====================================================================*/ | |
35 /* Simple types: */ | |
36 | |
37 typedef int bool; | |
38 | |
39 #define true 1 | |
40 #define false 0 | |
41 | |
42 typedef int lit; | |
43 #if 0 /* by mao */ | |
44 typedef char lbool; | |
45 #else | |
46 typedef int lbool; | |
47 #endif | |
48 | |
49 #define var_Undef (int)(-1) | |
50 #define lit_Undef (lit)(-2) | |
51 | |
52 #define l_Undef (lbool)0 | |
53 #define l_True (lbool)1 | |
54 #define l_False (lbool)(-1) | |
55 | |
56 #define toLit(v) (lit)((v) + (v)) | |
57 #define lit_neg(l) (lit)((l) ^ 1) | |
58 #define lit_var(l) (int)((l) >> 1) | |
59 #define lit_sign(l) (int)((l) & 1) | |
60 | |
61 /*====================================================================*/ | |
62 /* Vectors: */ | |
63 | |
64 /* vector of 32-bit intergers (added for 64-bit portability) */ | |
65 typedef struct /* veci_t */ { | |
66 int size; | |
67 int cap; | |
68 int* ptr; | |
69 } veci; | |
70 | |
71 #define veci_new(v) \ | |
72 { (v)->size = 0; \ | |
73 (v)->cap = 4; \ | |
74 (v)->ptr = (int*)malloc(sizeof(int)*(v)->cap); \ | |
75 } | |
76 | |
77 #define veci_delete(v) free((v)->ptr) | |
78 | |
79 #define veci_begin(v) ((v)->ptr) | |
80 | |
81 #define veci_size(v) ((v)->size) | |
82 | |
83 #define veci_resize(v, k) (void)((v)->size = (k)) | |
84 /* only safe to shrink !! */ | |
85 | |
86 #define veci_push(v, e) \ | |
87 { if ((v)->size == (v)->cap) \ | |
88 { int newsize = (v)->cap * 2+1; \ | |
89 (v)->ptr = (int*)realloc((v)->ptr,sizeof(int)*newsize); \ | |
90 (v)->cap = newsize; \ | |
91 } \ | |
92 (v)->ptr[(v)->size++] = (e); \ | |
93 } | |
94 | |
95 /* vector of 32- or 64-bit pointers */ | |
96 typedef struct /* vecp_t */ { | |
97 int size; | |
98 int cap; | |
99 void** ptr; | |
100 } vecp; | |
101 | |
102 #define vecp_new(v) \ | |
103 { (v)->size = 0; \ | |
104 (v)->cap = 4; \ | |
105 (v)->ptr = (void**)malloc(sizeof(void*)*(v)->cap); \ | |
106 } | |
107 | |
108 #define vecp_delete(v) free((v)->ptr) | |
109 | |
110 #define vecp_begin(v) ((v)->ptr) | |
111 | |
112 #define vecp_size(v) ((v)->size) | |
113 | |
114 #define vecp_resize(v, k) (void)((v)->size = (k)) | |
115 /* only safe to shrink !! */ | |
116 | |
117 #define vecp_push(v, e) \ | |
118 { if ((v)->size == (v)->cap) \ | |
119 { int newsize = (v)->cap * 2+1; \ | |
120 (v)->ptr = (void**)realloc((v)->ptr,sizeof(void*)*newsize); \ | |
121 (v)->cap = newsize; \ | |
122 } \ | |
123 (v)->ptr[(v)->size++] = (e); \ | |
124 } | |
125 | |
126 /*====================================================================*/ | |
127 /* Solver representation: */ | |
128 | |
129 typedef struct /* clause_t */ | |
130 { | |
131 int size_learnt; | |
132 lit lits[1]; | |
133 } clause; | |
134 | |
135 typedef struct /* stats_t */ | |
136 { | |
137 double starts, decisions, propagations, inspects, conflicts; | |
138 double clauses, clauses_literals, learnts, learnts_literals, | |
139 max_literals, tot_literals; | |
140 } stats; | |
141 | |
142 typedef struct /* solver_t */ | |
143 { | |
144 int size; /* nof variables */ | |
145 int cap; /* size of varmaps */ | |
146 int qhead; /* Head index of queue. */ | |
147 int qtail; /* Tail index of queue. */ | |
148 | |
149 /* clauses */ | |
150 vecp clauses; /* List of problem constraints. | |
151 (contains: clause*) */ | |
152 vecp learnts; /* List of learnt clauses. | |
153 (contains: clause*) */ | |
154 | |
155 /* activities */ | |
156 double var_inc; /* Amount to bump next variable with. */ | |
157 double var_decay; /* INVERSE decay factor for variable | |
158 activity: stores 1/decay. */ | |
159 float cla_inc; /* Amount to bump next clause with. */ | |
160 float cla_decay; /* INVERSE decay factor for clause | |
161 activity: stores 1/decay. */ | |
162 | |
163 vecp* wlists; | |
164 double* activity; /* A heuristic measurement of the activity | |
165 of a variable. */ | |
166 lbool* assigns; /* Current values of variables. */ | |
167 int* orderpos; /* Index in variable order. */ | |
168 clause** reasons; | |
169 int* levels; | |
170 lit* trail; | |
171 | |
172 clause* binary; /* A temporary binary clause */ | |
173 lbool* tags; | |
174 veci tagged; /* (contains: var) */ | |
175 veci stack; /* (contains: var) */ | |
176 | |
177 veci order; /* Variable order. (heap) (contains: var) */ | |
178 veci trail_lim; /* Separator indices for different decision | |
179 levels in 'trail'. (contains: int) */ | |
180 veci model; /* If problem is solved, this vector | |
181 contains the model (contains: lbool). */ | |
182 | |
183 int root_level; /* Level of first proper decision. */ | |
184 int simpdb_assigns;/* Number of top-level assignments at last | |
185 'simplifyDB()'. */ | |
186 int simpdb_props; /* Number of propagations before next | |
187 'simplifyDB()'. */ | |
188 double random_seed; | |
189 double progress_estimate; | |
190 int verbosity; /* Verbosity level. | |
191 0=silent, | |
192 1=some progress report, | |
193 2=everything */ | |
194 | |
195 stats stats; | |
196 } solver; | |
197 | |
198 /*====================================================================*/ | |
199 /* Public interface: */ | |
200 | |
201 #if 1 /* by mao; to keep namespace clean */ | |
202 #define solver_new _glp_minisat_new | |
203 #define solver_delete _glp_minisat_delete | |
204 #define solver_addclause _glp_minisat_addclause | |
205 #define solver_simplify _glp_minisat_simplify | |
206 #define solver_solve _glp_minisat_solve | |
207 #define solver_nvars _glp_minisat_nvars | |
208 #define solver_nclauses _glp_minisat_nclauses | |
209 #define solver_nconflicts _glp_minisat_nconflicts | |
210 #define solver_setnvars _glp_minisat_setnvars | |
211 #define solver_propagate _glp_minisat_propagate | |
212 #define solver_reducedb _glp_minisat_reducedb | |
213 #endif | |
214 | |
215 solver* solver_new(void); | |
216 void solver_delete(solver* s); | |
217 | |
218 bool solver_addclause(solver* s, lit* begin, lit* end); | |
219 bool solver_simplify(solver* s); | |
220 bool solver_solve(solver* s, lit* begin, lit* end); | |
221 | |
222 int solver_nvars(solver* s); | |
223 int solver_nclauses(solver* s); | |
224 int solver_nconflicts(solver* s); | |
225 | |
226 void solver_setnvars(solver* s,int n); | |
227 | |
228 #endif | |
229 | |
230 /* eof */ |