lemon-project-template-glpk

annotate deps/glpk/src/minisat/minisat.h @ 9:33de93886c88

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