lemon-project-template-glpk
view deps/glpk/src/minisat/minisat.h @ 9:33de93886c88
Import GLPK 4.47
| author | Alpar Juttner <alpar@cs.elte.hu> |
|---|---|
| date | Sun, 06 Nov 2011 20:59:10 +0100 |
| parents | |
| children |
line source
1 /* minisat.h */
3 /* Modified by Andrew Makhorin <mao@gnu.org>, August 2011 */
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 */
31 #ifndef MINISAT_H
32 #define MINISAT_H
34 /*====================================================================*/
35 /* Simple types: */
37 typedef int bool;
39 #define true 1
40 #define false 0
42 typedef int lit;
43 #if 0 /* by mao */
44 typedef char lbool;
45 #else
46 typedef int lbool;
47 #endif
49 #define var_Undef (int)(-1)
50 #define lit_Undef (lit)(-2)
52 #define l_Undef (lbool)0
53 #define l_True (lbool)1
54 #define l_False (lbool)(-1)
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)
61 /*====================================================================*/
62 /* Vectors: */
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;
71 #define veci_new(v) \
72 { (v)->size = 0; \
73 (v)->cap = 4; \
74 (v)->ptr = (int*)malloc(sizeof(int)*(v)->cap); \
75 }
77 #define veci_delete(v) free((v)->ptr)
79 #define veci_begin(v) ((v)->ptr)
81 #define veci_size(v) ((v)->size)
83 #define veci_resize(v, k) (void)((v)->size = (k))
84 /* only safe to shrink !! */
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 }
95 /* vector of 32- or 64-bit pointers */
96 typedef struct /* vecp_t */ {
97 int size;
98 int cap;
99 void** ptr;
100 } vecp;
102 #define vecp_new(v) \
103 { (v)->size = 0; \
104 (v)->cap = 4; \
105 (v)->ptr = (void**)malloc(sizeof(void*)*(v)->cap); \
106 }
108 #define vecp_delete(v) free((v)->ptr)
110 #define vecp_begin(v) ((v)->ptr)
112 #define vecp_size(v) ((v)->size)
114 #define vecp_resize(v, k) (void)((v)->size = (k))
115 /* only safe to shrink !! */
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 }
126 /*====================================================================*/
127 /* Solver representation: */
129 typedef struct /* clause_t */
130 {
131 int size_learnt;
132 lit lits[1];
133 } clause;
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;
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. */
149 /* clauses */
150 vecp clauses; /* List of problem constraints.
151 (contains: clause*) */
152 vecp learnts; /* List of learnt clauses.
153 (contains: clause*) */
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. */
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;
172 clause* binary; /* A temporary binary clause */
173 lbool* tags;
174 veci tagged; /* (contains: var) */
175 veci stack; /* (contains: var) */
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). */
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 */
195 stats stats;
196 } solver;
198 /*====================================================================*/
199 /* Public interface: */
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
215 solver* solver_new(void);
216 void solver_delete(solver* s);
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);
222 int solver_nvars(solver* s);
223 int solver_nclauses(solver* s);
224 int solver_nconflicts(solver* s);
226 void solver_setnvars(solver* s,int n);
228 #endif
230 /* eof */