1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/deps/glpk/src/minisat/minisat.c	Sun Nov 06 20:59:10 2011 +0100
     1.3 @@ -0,0 +1,1299 @@
     1.4 +/* minisat.c */
     1.5 +
     1.6 +/* Modified by Andrew Makhorin <mao@gnu.org>, August 2011 */
     1.7 +
     1.8 +/***********************************************************************
     1.9 +*  MiniSat -- Copyright (c) 2005, Niklas Sorensson
    1.10 +*  http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
    1.11 +*
    1.12 +*  Permission is hereby granted, free of charge, to any person
    1.13 +*  obtaining a copy of this software and associated documentation files
    1.14 +*  (the "Software"), to deal in the Software without restriction,
    1.15 +*  including without limitation the rights to use, copy, modify, merge,
    1.16 +*  publish, distribute, sublicense, and/or sell copies of the Software,
    1.17 +*  and to permit persons to whom the Software is furnished to do so,
    1.18 +*  subject to the following conditions:
    1.19 +*
    1.20 +*  The above copyright notice and this permission notice shall be
    1.21 +*  included in all copies or substantial portions of the Software.
    1.22 +*
    1.23 +*  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
    1.24 +*  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
    1.25 +*  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
    1.26 +*  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
    1.27 +*  BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
    1.28 +*  ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
    1.29 +*  CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
    1.30 +*  SOFTWARE.
    1.31 +***********************************************************************/
    1.32 +/* Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko */
    1.33 +
    1.34 +#include "glpenv.h"
    1.35 +#include "minisat.h"
    1.36 +
    1.37 +#if 1 /* by mao */
    1.38 +static void *ymalloc(int size)
    1.39 +{     void *ptr;
    1.40 +      xassert(size > 0);
    1.41 +      ptr = malloc(size);
    1.42 +      if (ptr == NULL)
    1.43 +         xerror("MiniSat: no memory available\n");
    1.44 +      return ptr;
    1.45 +}
    1.46 +
    1.47 +static void *yrealloc(void *ptr, int size)
    1.48 +{     xassert(size > 0);
    1.49 +      if (ptr == NULL)
    1.50 +         ptr = malloc(size);
    1.51 +      else
    1.52 +         ptr = realloc(ptr, size);
    1.53 +      if (ptr == NULL)
    1.54 +         xerror("MiniSat: no memory available\n");
    1.55 +      return ptr;
    1.56 +}
    1.57 +
    1.58 +static void yfree(void *ptr)
    1.59 +{     xassert(ptr != NULL);
    1.60 +      free(ptr);
    1.61 +      return;
    1.62 +}
    1.63 +
    1.64 +#define assert  xassert
    1.65 +#define printf  xprintf
    1.66 +#define fflush(f) /* nop */
    1.67 +#define malloc  ymalloc
    1.68 +#define realloc yrealloc
    1.69 +#define free    yfree
    1.70 +#define inline  /* empty */
    1.71 +#endif
    1.72 +
    1.73 +/*====================================================================*/
    1.74 +/* Debug: */
    1.75 +
    1.76 +#if 0
    1.77 +#define VERBOSEDEBUG 1
    1.78 +#endif
    1.79 +
    1.80 +/* For derivation output (verbosity level 2) */
    1.81 +#define L_IND    "%-*d"
    1.82 +#define L_ind    solver_dlevel(s)*3+3,solver_dlevel(s)
    1.83 +#define L_LIT    "%sx%d"
    1.84 +#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
    1.85 +
    1.86 +#if 0 /* by mao */
    1.87 +/* Just like 'assert()' but expression will be evaluated in the release
    1.88 +   version as well. */
    1.89 +static inline void check(int expr) { assert(expr); }
    1.90 +#endif
    1.91 +
    1.92 +#if 0 /* by mao */
    1.93 +static void printlits(lit* begin, lit* end)
    1.94 +{
    1.95 +    int i;
    1.96 +    for (i = 0; i < end - begin; i++)
    1.97 +        printf(L_LIT" ",L_lit(begin[i]));
    1.98 +}
    1.99 +#endif
   1.100 +
   1.101 +/*====================================================================*/
   1.102 +/* Random numbers: */
   1.103 +
   1.104 +/* Returns a random float 0 <= x < 1. Seed must never be 0. */
   1.105 +static inline double drand(double* seed) {
   1.106 +    int q;
   1.107 +    *seed *= 1389796;
   1.108 +    q = (int)(*seed / 2147483647);
   1.109 +    *seed -= (double)q * 2147483647;
   1.110 +    return *seed / 2147483647; }
   1.111 +
   1.112 +/* Returns a random integer 0 <= x < size. Seed must never be 0. */
   1.113 +static inline int irand(double* seed, int size) {
   1.114 +    return (int)(drand(seed) * size); }
   1.115 +
   1.116 +/*====================================================================*/
   1.117 +/* Predeclarations: */
   1.118 +
   1.119 +static void sort(void** array, int size,
   1.120 +    int(*comp)(const void *, const void *));
   1.121 +
   1.122 +/*====================================================================*/
   1.123 +/* Clause datatype + minor functions: */
   1.124 +
   1.125 +#if 0 /* by mao; see minisat.h */
   1.126 +struct clause_t
   1.127 +{
   1.128 +    int size_learnt;
   1.129 +    lit lits[0];
   1.130 +};
   1.131 +#endif
   1.132 +
   1.133 +#define clause_size(c) ((c)->size_learnt >> 1)
   1.134 +
   1.135 +#define clause_begin(c) ((c)->lits)
   1.136 +
   1.137 +#define clause_learnt(c) ((c)->size_learnt & 1)
   1.138 +
   1.139 +#define clause_activity(c) \
   1.140 +    (*((float*)&(c)->lits[(c)->size_learnt>>1]))
   1.141 +
   1.142 +#define clause_setactivity(c, a) \
   1.143 +    (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a))
   1.144 +
   1.145 +/*====================================================================*/
   1.146 +/* Encode literals in clause pointers: */
   1.147 +
   1.148 +#define clause_from_lit(l) \
   1.149 +      (clause*)((unsigned long)(l) + (unsigned long)(l) + 1)
   1.150 +
   1.151 +#define clause_is_lit(c) \
   1.152 +      ((unsigned long)(c) & 1)
   1.153 +
   1.154 +#define clause_read_lit(c) \
   1.155 +      (lit)((unsigned long)(c) >> 1)
   1.156 +
   1.157 +/*====================================================================*/
   1.158 +/* Simple helpers: */
   1.159 +
   1.160 +#define solver_dlevel(s) \
   1.161 +    (int)veci_size(&(s)->trail_lim)
   1.162 +
   1.163 +#define solver_read_wlist(s, l) \
   1.164 +    (vecp *)(&(s)->wlists[l])
   1.165 +
   1.166 +static inline void    vecp_remove(vecp* v, void* e)
   1.167 +{
   1.168 +    void** ws = vecp_begin(v);
   1.169 +    int    j  = 0;
   1.170 +
   1.171 +    for (; ws[j] != e  ; j++);
   1.172 +    assert(j < vecp_size(v));
   1.173 +    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
   1.174 +    vecp_resize(v,vecp_size(v)-1);
   1.175 +}
   1.176 +
   1.177 +/*====================================================================*/
   1.178 +/* Variable order functions: */
   1.179 +
   1.180 +static inline void order_update(solver* s, int v)
   1.181 +{   /* updateorder */
   1.182 +    int*    orderpos = s->orderpos;
   1.183 +    double* activity = s->activity;
   1.184 +    int*    heap     = veci_begin(&s->order);
   1.185 +    int     i        = orderpos[v];
   1.186 +    int     x        = heap[i];
   1.187 +    int     parent   = (i - 1) / 2;
   1.188 +
   1.189 +    assert(s->orderpos[v] != -1);
   1.190 +
   1.191 +    while (i != 0 && activity[x] > activity[heap[parent]]){
   1.192 +        heap[i]           = heap[parent];
   1.193 +        orderpos[heap[i]] = i;
   1.194 +        i                 = parent;
   1.195 +        parent            = (i - 1) / 2;
   1.196 +    }
   1.197 +    heap[i]     = x;
   1.198 +    orderpos[x] = i;
   1.199 +}
   1.200 +
   1.201 +#define order_assigned(s, v) /* nop */
   1.202 +
   1.203 +static inline void order_unassigned(solver* s, int v)
   1.204 +{   /* undoorder */
   1.205 +    int* orderpos = s->orderpos;
   1.206 +    if (orderpos[v] == -1){
   1.207 +        orderpos[v] = veci_size(&s->order);
   1.208 +        veci_push(&s->order,v);
   1.209 +        order_update(s,v);
   1.210 +    }
   1.211 +}
   1.212 +
   1.213 +static int order_select(solver* s, float random_var_freq)
   1.214 +{   /* selectvar */
   1.215 +    int*    heap;
   1.216 +    double* activity;
   1.217 +    int*    orderpos;
   1.218 +
   1.219 +    lbool* values = s->assigns;
   1.220 +
   1.221 +    /* Random decision: */
   1.222 +    if (drand(&s->random_seed) < random_var_freq){
   1.223 +        int next = irand(&s->random_seed,s->size);
   1.224 +        assert(next >= 0 && next < s->size);
   1.225 +        if (values[next] == l_Undef)
   1.226 +            return next;
   1.227 +    }
   1.228 +
   1.229 +    /* Activity based decision: */
   1.230 +
   1.231 +    heap     = veci_begin(&s->order);
   1.232 +    activity = s->activity;
   1.233 +    orderpos = s->orderpos;
   1.234 +
   1.235 +    while (veci_size(&s->order) > 0){
   1.236 +        int    next  = heap[0];
   1.237 +        int    size  = veci_size(&s->order)-1;
   1.238 +        int    x     = heap[size];
   1.239 +
   1.240 +        veci_resize(&s->order,size);
   1.241 +
   1.242 +        orderpos[next] = -1;
   1.243 +
   1.244 +        if (size > 0){
   1.245 +            double act   = activity[x];
   1.246 +
   1.247 +            int    i     = 0;
   1.248 +            int    child = 1;
   1.249 +
   1.250 +            while (child < size){
   1.251 +                if (child+1 < size
   1.252 +                    && activity[heap[child]] < activity[heap[child+1]])
   1.253 +                    child++;
   1.254 +
   1.255 +                assert(child < size);
   1.256 +
   1.257 +                if (act >= activity[heap[child]])
   1.258 +                    break;
   1.259 +
   1.260 +                heap[i]           = heap[child];
   1.261 +                orderpos[heap[i]] = i;
   1.262 +                i                 = child;
   1.263 +                child             = 2 * child + 1;
   1.264 +            }
   1.265 +            heap[i]           = x;
   1.266 +            orderpos[heap[i]] = i;
   1.267 +        }
   1.268 +
   1.269 +        if (values[next] == l_Undef)
   1.270 +            return next;
   1.271 +    }
   1.272 +
   1.273 +    return var_Undef;
   1.274 +}
   1.275 +
   1.276 +/*====================================================================*/
   1.277 +/* Activity functions: */
   1.278 +
   1.279 +static inline void act_var_rescale(solver* s) {
   1.280 +    double* activity = s->activity;
   1.281 +    int i;
   1.282 +    for (i = 0; i < s->size; i++)
   1.283 +        activity[i] *= 1e-100;
   1.284 +    s->var_inc *= 1e-100;
   1.285 +}
   1.286 +
   1.287 +static inline void act_var_bump(solver* s, int v) {
   1.288 +    double* activity = s->activity;
   1.289 +    if ((activity[v] += s->var_inc) > 1e100)
   1.290 +        act_var_rescale(s);
   1.291 +
   1.292 +    /* printf("bump %d %f\n", v-1, activity[v]); */
   1.293 +
   1.294 +    if (s->orderpos[v] != -1)
   1.295 +        order_update(s,v);
   1.296 +
   1.297 +}
   1.298 +
   1.299 +static inline void act_var_decay(solver* s)
   1.300 +    { s->var_inc *= s->var_decay; }
   1.301 +
   1.302 +static inline void act_clause_rescale(solver* s) {
   1.303 +    clause** cs = (clause**)vecp_begin(&s->learnts);
   1.304 +    int i;
   1.305 +    for (i = 0; i < vecp_size(&s->learnts); i++){
   1.306 +        float a = clause_activity(cs[i]);
   1.307 +        clause_setactivity(cs[i], a * (float)1e-20);
   1.308 +    }
   1.309 +    s->cla_inc *= (float)1e-20;
   1.310 +}
   1.311 +
   1.312 +static inline void act_clause_bump(solver* s, clause *c) {
   1.313 +    float a = clause_activity(c) + s->cla_inc;
   1.314 +    clause_setactivity(c,a);
   1.315 +    if (a > 1e20) act_clause_rescale(s);
   1.316 +}
   1.317 +
   1.318 +static inline void act_clause_decay(solver* s)
   1.319 +    { s->cla_inc *= s->cla_decay; }
   1.320 +
   1.321 +/*====================================================================*/
   1.322 +/* Clause functions: */
   1.323 +
   1.324 +/* pre: size > 1 && no variable occurs twice
   1.325 + */
   1.326 +static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
   1.327 +{
   1.328 +    int size;
   1.329 +    clause* c;
   1.330 +    int i;
   1.331 +
   1.332 +    assert(end - begin > 1);
   1.333 +    assert(learnt >= 0 && learnt < 2);
   1.334 +    size           = end - begin;
   1.335 +    c              = (clause*)malloc(sizeof(clause)
   1.336 +                     + sizeof(lit) * size + learnt * sizeof(float));
   1.337 +    c->size_learnt = (size << 1) | learnt;
   1.338 +#if 0 /* by mao; meaningless non-portable check */
   1.339 +    assert(((unsigned int)c & 1) == 0);
   1.340 +#endif
   1.341 +
   1.342 +    for (i = 0; i < size; i++)
   1.343 +        c->lits[i] = begin[i];
   1.344 +
   1.345 +    if (learnt)
   1.346 +        *((float*)&c->lits[size]) = 0.0;
   1.347 +
   1.348 +    assert(begin[0] >= 0);
   1.349 +    assert(begin[0] < s->size*2);
   1.350 +    assert(begin[1] >= 0);
   1.351 +    assert(begin[1] < s->size*2);
   1.352 +
   1.353 +    assert(lit_neg(begin[0]) < s->size*2);
   1.354 +    assert(lit_neg(begin[1]) < s->size*2);
   1.355 +
   1.356 +    /* vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c); */
   1.357 +    /* vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c); */
   1.358 +
   1.359 +    vecp_push(solver_read_wlist(s,lit_neg(begin[0])),
   1.360 +        (void*)(size > 2 ? c : clause_from_lit(begin[1])));
   1.361 +    vecp_push(solver_read_wlist(s,lit_neg(begin[1])),
   1.362 +        (void*)(size > 2 ? c : clause_from_lit(begin[0])));
   1.363 +
   1.364 +    return c;
   1.365 +}
   1.366 +
   1.367 +static void clause_remove(solver* s, clause* c)
   1.368 +{
   1.369 +    lit* lits = clause_begin(c);
   1.370 +    assert(lit_neg(lits[0]) < s->size*2);
   1.371 +    assert(lit_neg(lits[1]) < s->size*2);
   1.372 +
   1.373 +    /* vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c); */
   1.374 +    /* vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c); */
   1.375 +
   1.376 +    assert(lits[0] < s->size*2);
   1.377 +    vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),
   1.378 +        (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
   1.379 +    vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),
   1.380 +        (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
   1.381 +
   1.382 +    if (clause_learnt(c)){
   1.383 +        s->stats.learnts--;
   1.384 +        s->stats.learnts_literals -= clause_size(c);
   1.385 +    }else{
   1.386 +        s->stats.clauses--;
   1.387 +        s->stats.clauses_literals -= clause_size(c);
   1.388 +    }
   1.389 +
   1.390 +    free(c);
   1.391 +}
   1.392 +
   1.393 +static lbool clause_simplify(solver* s, clause* c)
   1.394 +{
   1.395 +    lit*   lits   = clause_begin(c);
   1.396 +    lbool* values = s->assigns;
   1.397 +    int i;
   1.398 +
   1.399 +    assert(solver_dlevel(s) == 0);
   1.400 +
   1.401 +    for (i = 0; i < clause_size(c); i++){
   1.402 +        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
   1.403 +        if (values[lit_var(lits[i])] == sig)
   1.404 +            return l_True;
   1.405 +    }
   1.406 +    return l_False;
   1.407 +}
   1.408 +
   1.409 +/*====================================================================*/
   1.410 +/* Minor (solver) functions: */
   1.411 +
   1.412 +void solver_setnvars(solver* s,int n)
   1.413 +{
   1.414 +    int var;
   1.415 +
   1.416 +    if (s->cap < n){
   1.417 +
   1.418 +        while (s->cap < n) s->cap = s->cap*2+1;
   1.419 +
   1.420 +        s->wlists    = (vecp*)   realloc(s->wlists,
   1.421 +                                 sizeof(vecp)*s->cap*2);
   1.422 +        s->activity  = (double*) realloc(s->activity,
   1.423 +                                 sizeof(double)*s->cap);
   1.424 +        s->assigns   = (lbool*)  realloc(s->assigns,
   1.425 +                                 sizeof(lbool)*s->cap);
   1.426 +        s->orderpos  = (int*)    realloc(s->orderpos,
   1.427 +                                 sizeof(int)*s->cap);
   1.428 +        s->reasons   = (clause**)realloc(s->reasons,
   1.429 +                                 sizeof(clause*)*s->cap);
   1.430 +        s->levels    = (int*)    realloc(s->levels,
   1.431 +                                 sizeof(int)*s->cap);
   1.432 +        s->tags      = (lbool*)  realloc(s->tags,
   1.433 +                                 sizeof(lbool)*s->cap);
   1.434 +        s->trail     = (lit*)    realloc(s->trail,
   1.435 +                                 sizeof(lit)*s->cap);
   1.436 +    }
   1.437 +
   1.438 +    for (var = s->size; var < n; var++){
   1.439 +        vecp_new(&s->wlists[2*var]);
   1.440 +        vecp_new(&s->wlists[2*var+1]);
   1.441 +        s->activity [var] = 0;
   1.442 +        s->assigns  [var] = l_Undef;
   1.443 +        s->orderpos [var] = veci_size(&s->order);
   1.444 +        s->reasons  [var] = (clause*)0;
   1.445 +        s->levels   [var] = 0;
   1.446 +        s->tags     [var] = l_Undef;
   1.447 +
   1.448 +        /* does not hold because variables enqueued at top level will
   1.449 +           not be reinserted in the heap
   1.450 +           assert(veci_size(&s->order) == var);
   1.451 +         */
   1.452 +        veci_push(&s->order,var);
   1.453 +        order_update(s, var);
   1.454 +    }
   1.455 +
   1.456 +    s->size = n > s->size ? n : s->size;
   1.457 +}
   1.458 +
   1.459 +static inline bool enqueue(solver* s, lit l, clause* from)
   1.460 +{
   1.461 +    lbool* values = s->assigns;
   1.462 +    int    v      = lit_var(l);
   1.463 +    lbool  val    = values[v];
   1.464 +    lbool  sig;
   1.465 +#ifdef VERBOSEDEBUG
   1.466 +    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
   1.467 +#endif
   1.468 +
   1.469 +    /* lbool */ sig = !lit_sign(l); sig += sig - 1;
   1.470 +    if (val != l_Undef){
   1.471 +        return val == sig;
   1.472 +    }else{
   1.473 +        /* New fact -- store it. */
   1.474 +        int*     levels;
   1.475 +        clause** reasons;
   1.476 +#ifdef VERBOSEDEBUG
   1.477 +        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
   1.478 +#endif
   1.479 +        /* int*     */ levels  = s->levels;
   1.480 +        /* clause** */ reasons = s->reasons;
   1.481 +
   1.482 +        values [v] = sig;
   1.483 +        levels [v] = solver_dlevel(s);
   1.484 +        reasons[v] = from;
   1.485 +        s->trail[s->qtail++] = l;
   1.486 +
   1.487 +        order_assigned(s, v);
   1.488 +        return true;
   1.489 +    }
   1.490 +}
   1.491 +
   1.492 +static inline void assume(solver* s, lit l){
   1.493 +    assert(s->qtail == s->qhead);
   1.494 +    assert(s->assigns[lit_var(l)] == l_Undef);
   1.495 +#ifdef VERBOSEDEBUG
   1.496 +    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
   1.497 +#endif
   1.498 +    veci_push(&s->trail_lim,s->qtail);
   1.499 +    enqueue(s,l,(clause*)0);
   1.500 +}
   1.501 +
   1.502 +static inline void solver_canceluntil(solver* s, int level) {
   1.503 +    lit*     trail;
   1.504 +    lbool*   values;
   1.505 +    clause** reasons;
   1.506 +    int      bound;
   1.507 +    int      c;
   1.508 +
   1.509 +    if (solver_dlevel(s) <= level)
   1.510 +        return;
   1.511 +
   1.512 +    trail   = s->trail;
   1.513 +    values  = s->assigns;
   1.514 +    reasons = s->reasons;
   1.515 +    bound   = (veci_begin(&s->trail_lim))[level];
   1.516 +
   1.517 +    for (c = s->qtail-1; c >= bound; c--) {
   1.518 +        int     x  = lit_var(trail[c]);
   1.519 +        values [x] = l_Undef;
   1.520 +        reasons[x] = (clause*)0;
   1.521 +    }
   1.522 +
   1.523 +    for (c = s->qhead-1; c >= bound; c--)
   1.524 +        order_unassigned(s,lit_var(trail[c]));
   1.525 +
   1.526 +    s->qhead = s->qtail = bound;
   1.527 +    veci_resize(&s->trail_lim,level);
   1.528 +}
   1.529 +
   1.530 +static void solver_record(solver* s, veci* cls)
   1.531 +{
   1.532 +    lit*    begin = veci_begin(cls);
   1.533 +    lit*    end   = begin + veci_size(cls);
   1.534 +    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1)
   1.535 +                                         : (clause*)0;
   1.536 +    enqueue(s,*begin,c);
   1.537 +
   1.538 +    assert(veci_size(cls) > 0);
   1.539 +
   1.540 +    if (c != 0) {
   1.541 +        vecp_push(&s->learnts,c);
   1.542 +        act_clause_bump(s,c);
   1.543 +        s->stats.learnts++;
   1.544 +        s->stats.learnts_literals += veci_size(cls);
   1.545 +    }
   1.546 +}
   1.547 +
   1.548 +static double solver_progress(solver* s)
   1.549 +{
   1.550 +    lbool*  values = s->assigns;
   1.551 +    int*    levels = s->levels;
   1.552 +    int     i;
   1.553 +
   1.554 +    double  progress = 0;
   1.555 +    double  F        = 1.0 / s->size;
   1.556 +    for (i = 0; i < s->size; i++)
   1.557 +        if (values[i] != l_Undef)
   1.558 +            progress += pow(F, levels[i]);
   1.559 +    return progress / s->size;
   1.560 +}
   1.561 +
   1.562 +/*====================================================================*/
   1.563 +/* Major methods: */
   1.564 +
   1.565 +static bool solver_lit_removable(solver* s, lit l, int minl)
   1.566 +{
   1.567 +    lbool*   tags    = s->tags;
   1.568 +    clause** reasons = s->reasons;
   1.569 +    int*     levels  = s->levels;
   1.570 +    int      top     = veci_size(&s->tagged);
   1.571 +
   1.572 +    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
   1.573 +    assert(reasons[lit_var(l)] != 0);
   1.574 +    veci_resize(&s->stack,0);
   1.575 +    veci_push(&s->stack,lit_var(l));
   1.576 +
   1.577 +    while (veci_size(&s->stack) > 0){
   1.578 +        clause* c;
   1.579 +        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
   1.580 +        assert(v >= 0 && v < s->size);
   1.581 +        veci_resize(&s->stack,veci_size(&s->stack)-1);
   1.582 +        assert(reasons[v] != 0);
   1.583 +        c    = reasons[v];
   1.584 +
   1.585 +        if (clause_is_lit(c)){
   1.586 +            int v = lit_var(clause_read_lit(c));
   1.587 +            if (tags[v] == l_Undef && levels[v] != 0){
   1.588 +                if (reasons[v] != 0
   1.589 +                    && ((1 << (levels[v] & 31)) & minl)){
   1.590 +                    veci_push(&s->stack,v);
   1.591 +                    tags[v] = l_True;
   1.592 +                    veci_push(&s->tagged,v);
   1.593 +                }else{
   1.594 +                    int* tagged = veci_begin(&s->tagged);
   1.595 +                    int j;
   1.596 +                    for (j = top; j < veci_size(&s->tagged); j++)
   1.597 +                        tags[tagged[j]] = l_Undef;
   1.598 +                    veci_resize(&s->tagged,top);
   1.599 +                    return false;
   1.600 +                }
   1.601 +            }
   1.602 +        }else{
   1.603 +            lit*    lits = clause_begin(c);
   1.604 +            int     i, j;
   1.605 +
   1.606 +            for (i = 1; i < clause_size(c); i++){
   1.607 +                int v = lit_var(lits[i]);
   1.608 +                if (tags[v] == l_Undef && levels[v] != 0){
   1.609 +                    if (reasons[v] != 0
   1.610 +                        && ((1 << (levels[v] & 31)) & minl)){
   1.611 +
   1.612 +                        veci_push(&s->stack,lit_var(lits[i]));
   1.613 +                        tags[v] = l_True;
   1.614 +                        veci_push(&s->tagged,v);
   1.615 +                    }else{
   1.616 +                        int* tagged = veci_begin(&s->tagged);
   1.617 +                        for (j = top; j < veci_size(&s->tagged); j++)
   1.618 +                            tags[tagged[j]] = l_Undef;
   1.619 +                        veci_resize(&s->tagged,top);
   1.620 +                        return false;
   1.621 +                    }
   1.622 +                }
   1.623 +            }
   1.624 +        }
   1.625 +    }
   1.626 +
   1.627 +    return true;
   1.628 +}
   1.629 +
   1.630 +static void solver_analyze(solver* s, clause* c, veci* learnt)
   1.631 +{
   1.632 +    lit*     trail   = s->trail;
   1.633 +    lbool*   tags    = s->tags;
   1.634 +    clause** reasons = s->reasons;
   1.635 +    int*     levels  = s->levels;
   1.636 +    int      cnt     = 0;
   1.637 +    lit      p       = lit_Undef;
   1.638 +    int      ind     = s->qtail-1;
   1.639 +    lit*     lits;
   1.640 +    int      i, j, minl;
   1.641 +    int*     tagged;
   1.642 +
   1.643 +    veci_push(learnt,lit_Undef);
   1.644 +
   1.645 +    do{
   1.646 +        assert(c != 0);
   1.647 +
   1.648 +        if (clause_is_lit(c)){
   1.649 +            lit q = clause_read_lit(c);
   1.650 +            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
   1.651 +            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
   1.652 +                tags[lit_var(q)] = l_True;
   1.653 +                veci_push(&s->tagged,lit_var(q));
   1.654 +                act_var_bump(s,lit_var(q));
   1.655 +                if (levels[lit_var(q)] == solver_dlevel(s))
   1.656 +                    cnt++;
   1.657 +                else
   1.658 +                    veci_push(learnt,q);
   1.659 +            }
   1.660 +        }else{
   1.661 +
   1.662 +            if (clause_learnt(c))
   1.663 +                act_clause_bump(s,c);
   1.664 +
   1.665 +            lits = clause_begin(c);
   1.666 +            /* printlits(lits,lits+clause_size(c)); printf("\n"); */
   1.667 +            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
   1.668 +                lit q = lits[j];
   1.669 +                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
   1.670 +                if (tags[lit_var(q)] == l_Undef
   1.671 +                    && levels[lit_var(q)] > 0){
   1.672 +                    tags[lit_var(q)] = l_True;
   1.673 +                    veci_push(&s->tagged,lit_var(q));
   1.674 +                    act_var_bump(s,lit_var(q));
   1.675 +                    if (levels[lit_var(q)] == solver_dlevel(s))
   1.676 +                        cnt++;
   1.677 +                    else
   1.678 +                        veci_push(learnt,q);
   1.679 +                }
   1.680 +            }
   1.681 +        }
   1.682 +
   1.683 +        while (tags[lit_var(trail[ind--])] == l_Undef);
   1.684 +
   1.685 +        p = trail[ind+1];
   1.686 +        c = reasons[lit_var(p)];
   1.687 +        cnt--;
   1.688 +
   1.689 +    }while (cnt > 0);
   1.690 +
   1.691 +    *veci_begin(learnt) = lit_neg(p);
   1.692 +
   1.693 +    lits = veci_begin(learnt);
   1.694 +    minl = 0;
   1.695 +    for (i = 1; i < veci_size(learnt); i++){
   1.696 +        int lev = levels[lit_var(lits[i])];
   1.697 +        minl    |= 1 << (lev & 31);
   1.698 +    }
   1.699 +
   1.700 +    /* simplify (full) */
   1.701 +    for (i = j = 1; i < veci_size(learnt); i++){
   1.702 +        if (reasons[lit_var(lits[i])] == 0
   1.703 +            || !solver_lit_removable(s,lits[i],minl))
   1.704 +            lits[j++] = lits[i];
   1.705 +    }
   1.706 +
   1.707 +    /* update size of learnt + statistics */
   1.708 +    s->stats.max_literals += veci_size(learnt);
   1.709 +    veci_resize(learnt,j);
   1.710 +    s->stats.tot_literals += j;
   1.711 +
   1.712 +    /* clear tags */
   1.713 +    tagged = veci_begin(&s->tagged);
   1.714 +    for (i = 0; i < veci_size(&s->tagged); i++)
   1.715 +        tags[tagged[i]] = l_Undef;
   1.716 +    veci_resize(&s->tagged,0);
   1.717 +
   1.718 +#ifdef DEBUG
   1.719 +    for (i = 0; i < s->size; i++)
   1.720 +        assert(tags[i] == l_Undef);
   1.721 +#endif
   1.722 +
   1.723 +#ifdef VERBOSEDEBUG
   1.724 +    printf(L_IND"Learnt {", L_ind);
   1.725 +    for (i = 0; i < veci_size(learnt); i++)
   1.726 +        printf(" "L_LIT, L_lit(lits[i]));
   1.727 +#endif
   1.728 +    if (veci_size(learnt) > 1){
   1.729 +        int max_i = 1;
   1.730 +        int max   = levels[lit_var(lits[1])];
   1.731 +        lit tmp;
   1.732 +
   1.733 +        for (i = 2; i < veci_size(learnt); i++)
   1.734 +            if (levels[lit_var(lits[i])] > max){
   1.735 +                max   = levels[lit_var(lits[i])];
   1.736 +                max_i = i;
   1.737 +            }
   1.738 +
   1.739 +        tmp         = lits[1];
   1.740 +        lits[1]     = lits[max_i];
   1.741 +        lits[max_i] = tmp;
   1.742 +    }
   1.743 +#ifdef VERBOSEDEBUG
   1.744 +    {
   1.745 +        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
   1.746 +        printf(" } at level %d\n", lev);
   1.747 +    }
   1.748 +#endif
   1.749 +}
   1.750 +
   1.751 +clause* solver_propagate(solver* s)
   1.752 +{
   1.753 +    lbool*  values = s->assigns;
   1.754 +    clause* confl  = (clause*)0;
   1.755 +    lit*    lits;
   1.756 +
   1.757 +    /* printf("solver_propagate\n"); */
   1.758 +    while (confl == 0 && s->qtail - s->qhead > 0){
   1.759 +        lit  p  = s->trail[s->qhead++];
   1.760 +        vecp* ws = solver_read_wlist(s,p);
   1.761 +        clause **begin = (clause**)vecp_begin(ws);
   1.762 +        clause **end   = begin + vecp_size(ws);
   1.763 +        clause **i, **j;
   1.764 +
   1.765 +        s->stats.propagations++;
   1.766 +        s->simpdb_props--;
   1.767 +
   1.768 +        /* printf("checking lit %d: "L_LIT"\n", veci_size(ws),
   1.769 +               L_lit(p)); */
   1.770 +        for (i = j = begin; i < end; ){
   1.771 +            if (clause_is_lit(*i)){
   1.772 +                *j++ = *i;
   1.773 +                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
   1.774 +                    confl = s->binary;
   1.775 +                    (clause_begin(confl))[1] = lit_neg(p);
   1.776 +                    (clause_begin(confl))[0] = clause_read_lit(*i++);
   1.777 +
   1.778 +                    /* Copy the remaining watches: */
   1.779 +                    while (i < end)
   1.780 +                        *j++ = *i++;
   1.781 +                }
   1.782 +            }else{
   1.783 +                lit false_lit;
   1.784 +                lbool sig;
   1.785 +
   1.786 +                lits = clause_begin(*i);
   1.787 +
   1.788 +                /* Make sure the false literal is data[1]: */
   1.789 +                false_lit = lit_neg(p);
   1.790 +                if (lits[0] == false_lit){
   1.791 +                    lits[0] = lits[1];
   1.792 +                    lits[1] = false_lit;
   1.793 +                }
   1.794 +                assert(lits[1] == false_lit);
   1.795 +                /* printf("checking clause: ");
   1.796 +                   printlits(lits, lits+clause_size(*i));
   1.797 +                   printf("\n"); */
   1.798 +
   1.799 +                /* If 0th watch is true, then clause is already
   1.800 +                   satisfied. */
   1.801 +                sig = !lit_sign(lits[0]); sig += sig - 1;
   1.802 +                if (values[lit_var(lits[0])] == sig){
   1.803 +                    *j++ = *i;
   1.804 +                }else{
   1.805 +                    /* Look for new watch: */
   1.806 +                    lit* stop = lits + clause_size(*i);
   1.807 +                    lit* k;
   1.808 +                    for (k = lits + 2; k < stop; k++){
   1.809 +                        lbool sig = lit_sign(*k); sig += sig - 1;
   1.810 +                        if (values[lit_var(*k)] != sig){
   1.811 +                            lits[1] = *k;
   1.812 +                            *k = false_lit;
   1.813 +                            vecp_push(solver_read_wlist(s,
   1.814 +                                lit_neg(lits[1])),*i);
   1.815 +                            goto next; }
   1.816 +                    }
   1.817 +
   1.818 +                    *j++ = *i;
   1.819 +                    /* Clause is unit under assignment: */
   1.820 +                    if (!enqueue(s,lits[0], *i)){
   1.821 +                        confl = *i++;
   1.822 +                        /* Copy the remaining watches: */
   1.823 +                        while (i < end)
   1.824 +                            *j++ = *i++;
   1.825 +                    }
   1.826 +                }
   1.827 +            }
   1.828 +        next:
   1.829 +            i++;
   1.830 +        }
   1.831 +
   1.832 +        s->stats.inspects += j - (clause**)vecp_begin(ws);
   1.833 +        vecp_resize(ws,j - (clause**)vecp_begin(ws));
   1.834 +    }
   1.835 +
   1.836 +    return confl;
   1.837 +}
   1.838 +
   1.839 +static inline int clause_cmp (const void* x, const void* y) {
   1.840 +    return clause_size((clause*)x) > 2
   1.841 +           && (clause_size((clause*)y) == 2
   1.842 +               || clause_activity((clause*)x)
   1.843 +                  < clause_activity((clause*)y)) ? -1 : 1; }
   1.844 +
   1.845 +void solver_reducedb(solver* s)
   1.846 +{
   1.847 +    int      i, j;
   1.848 +    double   extra_lim = s->cla_inc / vecp_size(&s->learnts);
   1.849 +             /* Remove any clause below this activity */
   1.850 +    clause** learnts = (clause**)vecp_begin(&s->learnts);
   1.851 +    clause** reasons = s->reasons;
   1.852 +
   1.853 +    sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), clause_cmp);
   1.854 +
   1.855 +    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
   1.856 +        if (clause_size(learnts[i]) > 2
   1.857 +            && reasons[lit_var(*clause_begin(learnts[i]))]
   1.858 +               != learnts[i])
   1.859 +            clause_remove(s,learnts[i]);
   1.860 +        else
   1.861 +            learnts[j++] = learnts[i];
   1.862 +    }
   1.863 +    for (; i < vecp_size(&s->learnts); i++){
   1.864 +        if (clause_size(learnts[i]) > 2
   1.865 +            && reasons[lit_var(*clause_begin(learnts[i]))]
   1.866 +               != learnts[i]
   1.867 +            && clause_activity(learnts[i]) < extra_lim)
   1.868 +            clause_remove(s,learnts[i]);
   1.869 +        else
   1.870 +            learnts[j++] = learnts[i];
   1.871 +    }
   1.872 +
   1.873 +    /* printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); */
   1.874 +
   1.875 +    vecp_resize(&s->learnts,j);
   1.876 +}
   1.877 +
   1.878 +static lbool solver_search(solver* s, int nof_conflicts,
   1.879 +                           int nof_learnts)
   1.880 +{
   1.881 +    int*    levels          = s->levels;
   1.882 +    double  var_decay       = 0.95;
   1.883 +    double  clause_decay    = 0.999;
   1.884 +    double  random_var_freq = 0.02;
   1.885 +
   1.886 +    int     conflictC       = 0;
   1.887 +    veci    learnt_clause;
   1.888 +
   1.889 +    assert(s->root_level == solver_dlevel(s));
   1.890 +
   1.891 +    s->stats.starts++;
   1.892 +    s->var_decay = (float)(1 / var_decay   );
   1.893 +    s->cla_decay = (float)(1 / clause_decay);
   1.894 +    veci_resize(&s->model,0);
   1.895 +    veci_new(&learnt_clause);
   1.896 +
   1.897 +    for (;;){
   1.898 +        clause* confl = solver_propagate(s);
   1.899 +        if (confl != 0){
   1.900 +            /* CONFLICT */
   1.901 +            int blevel;
   1.902 +
   1.903 +#ifdef VERBOSEDEBUG
   1.904 +            printf(L_IND"**CONFLICT**\n", L_ind);
   1.905 +#endif
   1.906 +            s->stats.conflicts++; conflictC++;
   1.907 +            if (solver_dlevel(s) == s->root_level){
   1.908 +                veci_delete(&learnt_clause);
   1.909 +                return l_False;
   1.910 +            }
   1.911 +
   1.912 +            veci_resize(&learnt_clause,0);
   1.913 +            solver_analyze(s, confl, &learnt_clause);
   1.914 +            blevel = veci_size(&learnt_clause) > 1
   1.915 +                     ? levels[lit_var(veci_begin(&learnt_clause)[1])]
   1.916 +                     : s->root_level;
   1.917 +            blevel = s->root_level > blevel ? s->root_level : blevel;
   1.918 +            solver_canceluntil(s,blevel);
   1.919 +            solver_record(s,&learnt_clause);
   1.920 +            act_var_decay(s);
   1.921 +            act_clause_decay(s);
   1.922 +
   1.923 +        }else{
   1.924 +            /* NO CONFLICT */
   1.925 +            int next;
   1.926 +
   1.927 +            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
   1.928 +                /* Reached bound on number of conflicts: */
   1.929 +                s->progress_estimate = solver_progress(s);
   1.930 +                solver_canceluntil(s,s->root_level);
   1.931 +                veci_delete(&learnt_clause);
   1.932 +                return l_Undef; }
   1.933 +
   1.934 +            if (solver_dlevel(s) == 0)
   1.935 +                /* Simplify the set of problem clauses: */
   1.936 +                solver_simplify(s);
   1.937 +
   1.938 +            if (nof_learnts >= 0
   1.939 +                && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
   1.940 +                /* Reduce the set of learnt clauses: */
   1.941 +                solver_reducedb(s);
   1.942 +
   1.943 +            /* New variable decision: */
   1.944 +            s->stats.decisions++;
   1.945 +            next = order_select(s,(float)random_var_freq);
   1.946 +
   1.947 +            if (next == var_Undef){
   1.948 +                /* Model found: */
   1.949 +                lbool* values = s->assigns;
   1.950 +                int i;
   1.951 +                for (i = 0; i < s->size; i++)
   1.952 +                    veci_push(&s->model,(int)values[i]);
   1.953 +                solver_canceluntil(s,s->root_level);
   1.954 +                veci_delete(&learnt_clause);
   1.955 +
   1.956 +                /*
   1.957 +                veci apa; veci_new(&apa);
   1.958 +                for (i = 0; i < s->size; i++)
   1.959 +                    veci_push(&apa,(int)(s->model.ptr[i] == l_True
   1.960 +                        ? toLit(i) : lit_neg(toLit(i))));
   1.961 +                printf("model: ");
   1.962 +                printlits((lit*)apa.ptr,
   1.963 +                    (lit*)apa.ptr + veci_size(&apa)); printf("\n");
   1.964 +                veci_delete(&apa);
   1.965 +                */
   1.966 +
   1.967 +                return l_True;
   1.968 +            }
   1.969 +
   1.970 +            assume(s,lit_neg(toLit(next)));
   1.971 +        }
   1.972 +    }
   1.973 +
   1.974 +#if 0 /* by mao; unreachable code */
   1.975 +    return l_Undef; /* cannot happen */
   1.976 +#endif
   1.977 +}
   1.978 +
   1.979 +/*====================================================================*/
   1.980 +/* External solver functions: */
   1.981 +
   1.982 +solver* solver_new(void)
   1.983 +{
   1.984 +    solver* s = (solver*)malloc(sizeof(solver));
   1.985 +
   1.986 +    /* initialize vectors */
   1.987 +    vecp_new(&s->clauses);
   1.988 +    vecp_new(&s->learnts);
   1.989 +    veci_new(&s->order);
   1.990 +    veci_new(&s->trail_lim);
   1.991 +    veci_new(&s->tagged);
   1.992 +    veci_new(&s->stack);
   1.993 +    veci_new(&s->model);
   1.994 +
   1.995 +    /* initialize arrays */
   1.996 +    s->wlists    = 0;
   1.997 +    s->activity  = 0;
   1.998 +    s->assigns   = 0;
   1.999 +    s->orderpos  = 0;
  1.1000 +    s->reasons   = 0;
  1.1001 +    s->levels    = 0;
  1.1002 +    s->tags      = 0;
  1.1003 +    s->trail     = 0;
  1.1004 +
  1.1005 +    /* initialize other vars */
  1.1006 +    s->size                   = 0;
  1.1007 +    s->cap                    = 0;
  1.1008 +    s->qhead                  = 0;
  1.1009 +    s->qtail                  = 0;
  1.1010 +    s->cla_inc                = 1;
  1.1011 +    s->cla_decay              = 1;
  1.1012 +    s->var_inc                = 1;
  1.1013 +    s->var_decay              = 1;
  1.1014 +    s->root_level             = 0;
  1.1015 +    s->simpdb_assigns         = 0;
  1.1016 +    s->simpdb_props           = 0;
  1.1017 +    s->random_seed            = 91648253;
  1.1018 +    s->progress_estimate      = 0;
  1.1019 +    s->binary                 = (clause*)malloc(sizeof(clause)
  1.1020 +                                                + sizeof(lit)*2);
  1.1021 +    s->binary->size_learnt    = (2 << 1);
  1.1022 +    s->verbosity              = 0;
  1.1023 +
  1.1024 +    s->stats.starts           = 0;
  1.1025 +    s->stats.decisions        = 0;
  1.1026 +    s->stats.propagations     = 0;
  1.1027 +    s->stats.inspects         = 0;
  1.1028 +    s->stats.conflicts        = 0;
  1.1029 +    s->stats.clauses          = 0;
  1.1030 +    s->stats.clauses_literals = 0;
  1.1031 +    s->stats.learnts          = 0;
  1.1032 +    s->stats.learnts_literals = 0;
  1.1033 +    s->stats.max_literals     = 0;
  1.1034 +    s->stats.tot_literals     = 0;
  1.1035 +
  1.1036 +    return s;
  1.1037 +}
  1.1038 +
  1.1039 +void solver_delete(solver* s)
  1.1040 +{
  1.1041 +    int i;
  1.1042 +    for (i = 0; i < vecp_size(&s->clauses); i++)
  1.1043 +        free(vecp_begin(&s->clauses)[i]);
  1.1044 +
  1.1045 +    for (i = 0; i < vecp_size(&s->learnts); i++)
  1.1046 +        free(vecp_begin(&s->learnts)[i]);
  1.1047 +
  1.1048 +    /* delete vectors */
  1.1049 +    vecp_delete(&s->clauses);
  1.1050 +    vecp_delete(&s->learnts);
  1.1051 +    veci_delete(&s->order);
  1.1052 +    veci_delete(&s->trail_lim);
  1.1053 +    veci_delete(&s->tagged);
  1.1054 +    veci_delete(&s->stack);
  1.1055 +    veci_delete(&s->model);
  1.1056 +    free(s->binary);
  1.1057 +
  1.1058 +    /* delete arrays */
  1.1059 +    if (s->wlists != 0){
  1.1060 +        int i;
  1.1061 +        for (i = 0; i < s->size*2; i++)
  1.1062 +            vecp_delete(&s->wlists[i]);
  1.1063 +
  1.1064 +        /* if one is different from null, all are */
  1.1065 +        free(s->wlists);
  1.1066 +        free(s->activity );
  1.1067 +        free(s->assigns  );
  1.1068 +        free(s->orderpos );
  1.1069 +        free(s->reasons  );
  1.1070 +        free(s->levels   );
  1.1071 +        free(s->trail    );
  1.1072 +        free(s->tags     );
  1.1073 +    }
  1.1074 +
  1.1075 +    free(s);
  1.1076 +}
  1.1077 +
  1.1078 +bool solver_addclause(solver* s, lit* begin, lit* end)
  1.1079 +{
  1.1080 +    lit *i,*j;
  1.1081 +    int maxvar;
  1.1082 +    lbool* values;
  1.1083 +    lit last;
  1.1084 +
  1.1085 +    if (begin == end) return false;
  1.1086 +
  1.1087 +    /* printlits(begin,end); printf("\n"); */
  1.1088 +    /* insertion sort */
  1.1089 +    maxvar = lit_var(*begin);
  1.1090 +    for (i = begin + 1; i < end; i++){
  1.1091 +        lit l = *i;
  1.1092 +        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
  1.1093 +        for (j = i; j > begin && *(j-1) > l; j--)
  1.1094 +            *j = *(j-1);
  1.1095 +        *j = l;
  1.1096 +    }
  1.1097 +    solver_setnvars(s,maxvar+1);
  1.1098 +
  1.1099 +    /* printlits(begin,end); printf("\n"); */
  1.1100 +    values = s->assigns;
  1.1101 +
  1.1102 +    /* delete duplicates */
  1.1103 +    last = lit_Undef;
  1.1104 +    for (i = j = begin; i < end; i++){
  1.1105 +        /* printf("lit: "L_LIT", value = %d\n", L_lit(*i),
  1.1106 +        (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); */
  1.1107 +        lbool sig = !lit_sign(*i); sig += sig - 1;
  1.1108 +        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
  1.1109 +            return true;   /* tautology */
  1.1110 +        else if (*i != last && values[lit_var(*i)] == l_Undef)
  1.1111 +            last = *j++ = *i;
  1.1112 +    }
  1.1113 +
  1.1114 +    /* printf("final: "); printlits(begin,j); printf("\n"); */
  1.1115 +
  1.1116 +    if (j == begin)          /* empty clause */
  1.1117 +        return false;
  1.1118 +    else if (j - begin == 1) /* unit clause */
  1.1119 +        return enqueue(s,*begin,(clause*)0);
  1.1120 +
  1.1121 +    /* create new clause */
  1.1122 +    vecp_push(&s->clauses,clause_new(s,begin,j,0));
  1.1123 +
  1.1124 +    s->stats.clauses++;
  1.1125 +    s->stats.clauses_literals += j - begin;
  1.1126 +
  1.1127 +    return true;
  1.1128 +}
  1.1129 +
  1.1130 +bool   solver_simplify(solver* s)
  1.1131 +{
  1.1132 +    clause** reasons;
  1.1133 +    int type;
  1.1134 +
  1.1135 +    assert(solver_dlevel(s) == 0);
  1.1136 +
  1.1137 +    if (solver_propagate(s) != 0)
  1.1138 +        return false;
  1.1139 +
  1.1140 +    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
  1.1141 +        return true;
  1.1142 +
  1.1143 +    reasons = s->reasons;
  1.1144 +    for (type = 0; type < 2; type++){
  1.1145 +        vecp*    cs  = type ? &s->learnts : &s->clauses;
  1.1146 +        clause** cls = (clause**)vecp_begin(cs);
  1.1147 +
  1.1148 +        int i, j;
  1.1149 +        for (j = i = 0; i < vecp_size(cs); i++){
  1.1150 +            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
  1.1151 +                clause_simplify(s,cls[i]) == l_True)
  1.1152 +                clause_remove(s,cls[i]);
  1.1153 +            else
  1.1154 +                cls[j++] = cls[i];
  1.1155 +        }
  1.1156 +        vecp_resize(cs,j);
  1.1157 +    }
  1.1158 +
  1.1159 +    s->simpdb_assigns = s->qhead;
  1.1160 +    /* (shouldn't depend on 'stats' really, but it will do for now) */
  1.1161 +    s->simpdb_props   = (int)(s->stats.clauses_literals
  1.1162 +                              + s->stats.learnts_literals);
  1.1163 +
  1.1164 +    return true;
  1.1165 +}
  1.1166 +
  1.1167 +bool   solver_solve(solver* s, lit* begin, lit* end)
  1.1168 +{
  1.1169 +    double  nof_conflicts = 100;
  1.1170 +    double  nof_learnts   = solver_nclauses(s) / 3;
  1.1171 +    lbool   status        = l_Undef;
  1.1172 +    lbool*  values        = s->assigns;
  1.1173 +    lit*    i;
  1.1174 +
  1.1175 +    /* printf("solve: "); printlits(begin, end); printf("\n"); */
  1.1176 +    for (i = begin; i < end; i++){
  1.1177 +        switch (lit_sign(*i) ? -values[lit_var(*i)]
  1.1178 +                             : values[lit_var(*i)]){
  1.1179 +        case 1: /* l_True: */
  1.1180 +            break;
  1.1181 +        case 0: /* l_Undef */
  1.1182 +            assume(s, *i);
  1.1183 +            if (solver_propagate(s) == NULL)
  1.1184 +                break;
  1.1185 +            /* falltrough */
  1.1186 +        case -1: /* l_False */
  1.1187 +            solver_canceluntil(s, 0);
  1.1188 +            return false;
  1.1189 +        }
  1.1190 +    }
  1.1191 +
  1.1192 +    s->root_level = solver_dlevel(s);
  1.1193 +
  1.1194 +    if (s->verbosity >= 1){
  1.1195 +        printf("==================================[MINISAT]============"
  1.1196 +               "=======================\n");
  1.1197 +        printf("| Conflicts |     ORIGINAL     |              LEARNT   "
  1.1198 +               "           | Progress |\n");
  1.1199 +        printf("|           | Clauses Literals |   Limit Clauses Litera"
  1.1200 +               "ls  Lit/Cl |          |\n");
  1.1201 +        printf("======================================================="
  1.1202 +               "=======================\n");
  1.1203 +    }
  1.1204 +
  1.1205 +    while (status == l_Undef){
  1.1206 +        double Ratio = (s->stats.learnts == 0)? 0.0 :
  1.1207 +            s->stats.learnts_literals / (double)s->stats.learnts;
  1.1208 +
  1.1209 +        if (s->verbosity >= 1){
  1.1210 +            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %"
  1.1211 +                   "6.3f %% |\n",
  1.1212 +                (double)s->stats.conflicts,
  1.1213 +                (double)s->stats.clauses,
  1.1214 +                (double)s->stats.clauses_literals,
  1.1215 +                (double)nof_learnts,
  1.1216 +                (double)s->stats.learnts,
  1.1217 +                (double)s->stats.learnts_literals,
  1.1218 +                Ratio,
  1.1219 +                s->progress_estimate*100);
  1.1220 +            fflush(stdout);
  1.1221 +        }
  1.1222 +        status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
  1.1223 +        nof_conflicts *= 1.5;
  1.1224 +        nof_learnts   *= 1.1;
  1.1225 +    }
  1.1226 +    if (s->verbosity >= 1)
  1.1227 +        printf("======================================================="
  1.1228 +               "=======================\n");
  1.1229 +
  1.1230 +    solver_canceluntil(s,0);
  1.1231 +    return status != l_False;
  1.1232 +}
  1.1233 +
  1.1234 +int solver_nvars(solver* s)
  1.1235 +{
  1.1236 +    return s->size;
  1.1237 +}
  1.1238 +
  1.1239 +int solver_nclauses(solver* s)
  1.1240 +{
  1.1241 +    return vecp_size(&s->clauses);
  1.1242 +}
  1.1243 +
  1.1244 +int solver_nconflicts(solver* s)
  1.1245 +{
  1.1246 +    return (int)s->stats.conflicts;
  1.1247 +}
  1.1248 +
  1.1249 +/*====================================================================*/
  1.1250 +/* Sorting functions (sigh): */
  1.1251 +
  1.1252 +static inline void selectionsort(void** array, int size,
  1.1253 +                                 int(*comp)(const void *, const void *))
  1.1254 +{
  1.1255 +    int     i, j, best_i;
  1.1256 +    void*   tmp;
  1.1257 +
  1.1258 +    for (i = 0; i < size-1; i++){
  1.1259 +        best_i = i;
  1.1260 +        for (j = i+1; j < size; j++){
  1.1261 +            if (comp(array[j], array[best_i]) < 0)
  1.1262 +                best_i = j;
  1.1263 +        }
  1.1264 +        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
  1.1265 +    }
  1.1266 +}
  1.1267 +
  1.1268 +static void sortrnd(void** array, int size,
  1.1269 +                    int(*comp)(const void *, const void *),
  1.1270 +                    double* seed)
  1.1271 +{
  1.1272 +    if (size <= 15)
  1.1273 +        selectionsort(array, size, comp);
  1.1274 +
  1.1275 +    else{
  1.1276 +        void*       pivot = array[irand(seed, size)];
  1.1277 +        void*       tmp;
  1.1278 +        int         i = -1;
  1.1279 +        int         j = size;
  1.1280 +
  1.1281 +        for(;;){
  1.1282 +            do i++; while(comp(array[i], pivot)<0);
  1.1283 +            do j--; while(comp(pivot, array[j])<0);
  1.1284 +
  1.1285 +            if (i >= j) break;
  1.1286 +
  1.1287 +            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
  1.1288 +        }
  1.1289 +
  1.1290 +        sortrnd(array    , i     , comp, seed);
  1.1291 +        sortrnd(&array[i], size-i, comp, seed);
  1.1292 +    }
  1.1293 +}
  1.1294 +
  1.1295 +static void sort(void** array, int size,
  1.1296 +          int(*comp)(const void *, const void *))
  1.1297 +{
  1.1298 +    double seed = 91648253;
  1.1299 +    sortrnd(array,size,comp,&seed);
  1.1300 +}
  1.1301 +
  1.1302 +/* eof */