kconfig2sat/picosat-960/picosat.c

   1 /****************************************************************************
   2 Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy
   5 of this software and associated documentation files (the "Software"), to
   6 deal in the Software without restriction, including without limitation the
   7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
   8 sell copies of the Software, and to permit persons to whom the Software is
   9 furnished to do so, subject to the following conditions:
  10
  11 The above copyright notice and this permission notice shall be included in
  12 all copies or substantial portions of the Software.
  13
  14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
  17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
  20 IN THE SOFTWARE.
  21 ****************************************************************************/
  22
  23 #include <stdlib.h>
  24 #include <stdio.h>
  25 #include <string.h>
  26 #include <assert.h>
  27 #include <limits.h>
  28 #include <ctype.h>
  29 #include <stdarg.h>
  30
  31 #include "picosat.h"
  32
  33 /* By default code for 'all different constraints' is disabled, since 'NADC'
  34  * is defined.
  35  */
  36 #define NADC
  37
  38 /* By default we enable failed literals, since 'NFL' is undefined.
  39  *
  40 #define NFL
  41  */
  42
  43 /* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined.
  44  *
  45 #define NDSC
  46  */
  47
  48 /* Do not use luby restart schedule instead of inner/outer.
  49  *
  50 #define NLUBY
  51  */
  52
  53 /* Enabling this define, will use gnuplot to visualize how the scores evolve.
  54  *
  55 #define VISCORES
  56  */
  57 #ifdef VISCORES
  58 // #define WRITEGIF             /* ... to generate a video */
  59 #endif
  60
  61 #ifdef VISCORES
  62 #ifndef WRITEGIF
  63 #include <unistd.h>             /* for 'usleep' */
  64 #endif
  65 #endif
  66
  67 #define MINRESTART      100     /* minimum restart interval */
  68 #define MAXRESTART      1000000 /* maximum restart interval */
  69 #define RDECIDE         1000    /* interval of random decisions */
  70 #define FRESTART        110     /* restart increase factor in percent */
  71 #define FREDUCE         110     /* reduce increase factor in percent  */
  72 #define FREDADJ         121     /* reduce increase adjustment factor */
  73 #define MAXCILS         10      /* maximal number of unrecycled internals */
  74 #define FFLIPPED        10000   /* flipped reduce factor */
  75 #define FFLIPPEDPREC    10000000/* flipped reduce factor precision */
  76
  77 #ifndef TRACE
  78 #define NO_BINARY_CLAUSES       /* store binary clauses more compactly */
  79 #endif
  80
  81 /* For debugging purposes you may want to define 'LOGGING', which actually
  82  * can be enforced by using the '--log' option for the configure script.
  83  */
  84 #ifdef LOGGING
  85 #define LOG(code) do { code; } while (0)
  86 #else
  87 #define LOG(code) do { } while (0)
  88 #endif
  89 #define NOLOG(code) do { } while (0)            /* log exception */
  90 #define ONLYLOG(code) do { code; } while (0)    /* force logging */
  91
  92 #define FALSE ((Val)-1)
  93 #define UNDEF ((Val)0)
  94 #define TRUE ((Val)1)
  95
  96 #define COMPACT_TRACECHECK_TRACE_FMT 0
  97 #define EXTENDED_TRACECHECK_TRACE_FMT 1
  98 #define RUP_TRACE_FMT 2
  99
 100 #define NEWN(p,n) do { (p) = new (ps, sizeof (*(p)) * (n)); } while (0)
 101 #define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0)
 102 #define CLR(p) CLRN(p,1)
 103 #define DELETEN(p,n) \
 104   do { delete (ps, p, sizeof (*(p)) * (n)); (p) = 0; } while (0)
 105
 106 #define RESIZEN(p,old_num,new_num) \
 107   do { \
 108     size_t old_size = sizeof (*(p)) * (old_num); \
 109     size_t new_size = sizeof (*(p)) * (new_num); \
 110     (p) = resize (ps, (p), old_size, new_size) ; \
 111   } while (0)
 112
 113 #define ENLARGE(start,head,end) \
 114   do { \
 115     unsigned old_num = (unsigned)((end) - (start)); \
 116     size_t new_num = old_num ? (2 * old_num) : 1; \
 117     unsigned count = (head) - (start); \
 118     assert ((start) <= (end)); \
 119     RESIZEN((start),old_num,new_num); \
 120     (head) = (start) + count; \
 121     (end) = (start) + new_num; \
 122   } while (0)
 123
 124 #define NOTLIT(l) (ps->lits + (1 ^ ((l) - ps->lits)))
 125
 126 #define LIT2IDX(l) ((unsigned)((l) - ps->lits) / 2)
 127 #define LIT2IMPLS(l) (ps->impls + (unsigned)((l) - ps->lits))
 128 #define LIT2INT(l) ((int)(LIT2SGN(l) * LIT2IDX(l)))
 129 #define LIT2SGN(l) (((unsigned)((l) - ps->lits) & 1) ? -1 : 1)
 130 #define LIT2VAR(l) (ps->vars + LIT2IDX(l))
 131 #define LIT2HTPS(l) (ps->htps + (unsigned)((l) - ps->lits))
 132 #define LIT2JWH(l) (ps->jwh + ((l) - ps->lits))
 133
 134 #ifndef NDSC
 135 #define LIT2DHTPS(l) (ps->dhtps + (unsigned)((l) - ps->lits))
 136 #endif
 137
 138 #ifdef NO_BINARY_CLAUSES
 139 typedef unsigned long Wrd;
 140 #define ISLITREASON(C) (1&(Wrd)C)
 141 #define LIT2REASON(L) \
 142   (assert (L->val==TRUE), ((Cls*)(1 + (2*(L - ps->lits)))))
 143 #define REASON2LIT(C) ((Lit*)(ps->lits + ((Wrd)C)/2))
 144 #endif
 145
 146 #define ENDOFCLS(c) ((void*)((c)->lits + (c)->size))
 147
 148 #define SOC ((ps->oclauses == ps->ohead) ? ps->lclauses : ps->oclauses)
 149 #define EOC (ps->lhead)
 150 #define NXC(p) (((p) + 1 == ps->ohead) ? ps->lclauses : (p) + 1)
 151
 152 #define OIDX2IDX(idx) (2 * ((idx) + 1))
 153 #define LIDX2IDX(idx) (2 * (idx) + 1)
 154
 155 #define ISLIDX(idx) ((idx)&1)
 156
 157 #define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1)
 158 #define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2)
 159
 160 #define EXPORTIDX(idx) \
 161   ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ps->ohead - ps->oclauses)) : IDX2OIDX(idx)) + 1)
 162
 163 #define IDX2CLS(i) \
 164   (assert(i), (ISLIDX(i) ? ps->lclauses : ps->oclauses)[(i)/2 - !ISLIDX(i)])
 165
 166 #define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? ps->zhains[(i)/2] : 0))
 167
 168 #define CLS2TRD(c) (((Trd*)(c)) - 1)
 169 #define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx)
 170
 171 #define CLS2ACT(c) \
 172   ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c)))
 173
 174 #define VAR2LIT(v) (ps->lits + 2 * ((v) - ps->vars))
 175 #define VAR2RNK(v) (ps->rnks + ((v) - ps->vars))
 176
 177 #define RNK2LIT(r) (ps->lits + 2 * ((r) - ps->rnks))
 178 #define RNK2VAR(r) (ps->vars + ((r) - ps->rnks))
 179
 180 #define BLK_FILL_BYTES 8
 181 #define SIZE_OF_BLK (sizeof (Blk) - BLK_FILL_BYTES)
 182
 183 #define PTR2BLK(void_ptr) \
 184   ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - SIZE_OF_BLK) : 0)
 185
 186 #define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0)
 187 #define PERCENT(a,b) (100.0 * AVERAGE(a,b))
 188
 189 #define ABORT(msg) \
 190   do { \
 191     fputs ("*** picosat: " msg "\n", stderr); \
 192     abort (); \
 193   } while (0)
 194
 195 #define ABORTIF(cond,msg) \
 196   do { \
 197     if (!(cond)) break; \
 198     ABORT (msg); \
 199   } while (0)
 200
 201 #define ZEROFLT         (0x00000000u)
 202 #define EPSFLT          (0x00000001u)
 203 #define INFFLT          (0xffffffffu)
 204
 205 #define FLTCARRY        (1u << 25)
 206 #define FLTMSB          (1u << 24)
 207 #define FLTMAXMANTISSA  (FLTMSB - 1)
 208
 209 #define FLTMANTISSA(d)  ((d) & FLTMAXMANTISSA)
 210 #define FLTEXPONENT(d)  ((int)((d) >> 24) - 128)
 211
 212 #define FLTMINEXPONENT  (-128)
 213 #define FLTMAXEXPONENT  (127)
 214
 215 #define CMPSWAPFLT(a,b) \
 216   do { \
 217     Flt tmp; \
 218     if (((a) < (b))) \
 219       { \
 220         tmp = (a); \
 221         (a) = (b); \
 222         (b) = tmp; \
 223       } \
 224   } while (0)
 225
 226 #define UNPACKFLT(u,m,e) \
 227   do { \
 228     (m) = FLTMANTISSA(u); \
 229     (e) = FLTEXPONENT(u); \
 230     (m) |= FLTMSB; \
 231   } while (0)
 232
 233 #define INSERTION_SORT_LIMIT 10
 234
 235 #define SORTING_SWAP(T,p,q) \
 236 do { \
 237   T tmp = *(q); \
 238   *(q) = *(p); \
 239   *(p) = tmp; \
 240 } while (0)
 241
 242 #define SORTING_CMP_SWAP(T,cmp,p,q) \
 243 do { \
 244   if ((cmp) (ps, *(p), *(q)) > 0) \
 245     SORTING_SWAP (T, p, q); \
 246 } while(0)
 247
 248 #define QUICKSORT_PARTITION(T,cmp,a,l,r) \
 249 do { \
 250   T pivot; \
 251   int j; \
 252   i = (l) - 1;                  /* result in 'i' */ \
 253   j = (r); \
 254   pivot = (a)[j]; \
 255   for (;;) \
 256     { \
 257       while ((cmp) (ps, (a)[++i], pivot) < 0) \
 258         ; \
 259       while ((cmp) (ps, pivot, (a)[--j]) < 0) \
 260         if (j == (l)) \
 261           break; \
 262       if (i >= j) \
 263         break; \
 264       SORTING_SWAP (T, (a) + i, (a) + j); \
 265     } \
 266   SORTING_SWAP (T, (a) + i, (a) + (r)); \
 267 } while(0)
 268
 269 #define QUICKSORT(T,cmp,a,n) \
 270 do { \
 271   int l = 0, r = (n) - 1, m, ll, rr, i; \
 272   assert (ps->ihead == ps->indices); \
 273   if (r - l <= INSERTION_SORT_LIMIT) \
 274     break; \
 275   for (;;) \
 276     { \
 277       m = (l + r) / 2; \
 278       SORTING_SWAP (T, (a) + m, (a) + r - 1); \
 279       SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r - 1); \
 280       SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r); \
 281       SORTING_CMP_SWAP (T, cmp, (a) + r - 1, (a) + r); \
 282       QUICKSORT_PARTITION (T, cmp, (a), l + 1, r - 1); \
 283       if (i - l < r - i) \
 284         { \
 285           ll = i + 1; \
 286           rr = r; \
 287           r = i - 1; \
 288         } \
 289       else \
 290         { \
 291           ll = l; \
 292           rr = i - 1; \
 293           l = i + 1; \
 294         } \
 295       if (r - l > INSERTION_SORT_LIMIT) \
 296         { \
 297           assert (rr - ll > INSERTION_SORT_LIMIT); \
 298           if (ps->ihead == ps->eoi) \
 299             ENLARGE (ps->indices, ps->ihead, ps->eoi); \
 300           *ps->ihead++ = ll; \
 301           if (ps->ihead == ps->eoi) \
 302             ENLARGE (ps->indices, ps->ihead, ps->eoi); \
 303           *ps->ihead++ = rr; \
 304         } \
 305       else if (rr - ll > INSERTION_SORT_LIMIT) \
 306         { \
 307           l = ll; \
 308           r = rr; \
 309         } \
 310       else if (ps->ihead > ps->indices) \
 311         { \
 312           r = *--ps->ihead; \
 313           l = *--ps->ihead; \
 314         } \
 315       else \
 316         break; \
 317     } \
 318 } while (0)
 319
 320 #define INSERTION_SORT(T,cmp,a,n) \
 321 do { \
 322   T pivot; \
 323   int l = 0, r = (n) - 1, i, j; \
 324   for (i = r; i > l; i--) \
 325     SORTING_CMP_SWAP (T, cmp, (a) + i - 1, (a) + i); \
 326   for (i = l + 2; i <= r; i++)  \
 327     { \
 328       j = i; \
 329       pivot = (a)[i]; \
 330       while ((cmp) (ps, pivot, (a)[j - 1]) < 0) \
 331         { \
 332           (a)[j] = (a)[j - 1]; \
 333           j--; \
 334         } \
 335       (a)[j] = pivot; \
 336     } \
 337 } while (0)
 338
 339 #ifdef NDEBUG
 340 #define CHECK_SORTED(cmp,a,n) do { } while(0)
 341 #else
 342 #define CHECK_SORTED(cmp,a,n) \
 343 do { \
 344   int i; \
 345   for (i = 0; i < (n) - 1; i++) \
 346     assert ((cmp) (ps, (a)[i], (a)[i + 1]) <= 0); \
 347 } while(0)
 348 #endif
 349
 350 #define SORT(T,cmp,a,n) \
 351 do { \
 352   T * aa = (a); \
 353   int nn = (n); \
 354   QUICKSORT (T, cmp, aa, nn); \
 355   INSERTION_SORT (T, cmp, aa, nn); \
 356   assert (ps->ihead == ps->indices); \
 357   CHECK_SORTED (cmp, aa, nn); \
 358 } while (0)
 359
 360 #define WRDSZ (sizeof (long) * 8)
 361
 362 typedef unsigned Flt;           /* 32 bit deterministic soft float */
 363 typedef Flt Act;                /* clause and variable activity */
 364 typedef struct Blk Blk;         /* allocated memory block */
 365 typedef struct Cls Cls;         /* clause */
 366 typedef struct Lit Lit;         /* literal */
 367 typedef struct Rnk Rnk;         /* variable to score mapping */
 368 typedef signed char Val;        /* TRUE, UNDEF, FALSE */
 369 typedef struct Var Var;         /* variable */
 370 #ifdef TRACE
 371 typedef struct Trd Trd;         /* trace data for clauses */
 372 typedef struct Zhn Zhn;         /* compressed chain (=zain) data */
 373 typedef unsigned char Znt;      /* compressed antecedent data */
 374 #endif
 375
 376 #ifdef NO_BINARY_CLAUSES
 377 typedef struct Ltk Ltk;
 378
 379 struct Ltk
 380 {
 381   Lit ** start;
 382   unsigned count : WRDSZ == 32 ? 27 : 32;
 383   unsigned ldsize : WRDSZ == 32 ? 5 : 32;
 384 };
 385 #endif
 386
 387 struct Lit
 388 {
 389   Val val;
 390 };
 391
 392 struct Var
 393 {
 394   unsigned mark         : 1;    /*bit 1*/
 395   unsigned resolved     : 1;    /*bit 2*/
 396   unsigned phase        : 1;    /*bit 3*/
 397   unsigned assigned     : 1;    /*bit 4*/
 398   unsigned used         : 1;    /*bit 5*/
 399   unsigned failed       : 1;    /*bit 6*/
 400   unsigned internal     : 1;    /*bit 7*/
 401   unsigned usedefphase  : 1;    /*bit 8*/
 402   unsigned defphase     : 1;    /*bit 9*/
 403   unsigned msspos       : 1;    /*bit 10*/
 404   unsigned mssneg       : 1;    /*bit 11*/
 405   unsigned humuspos     : 1;    /*bit 12*/
 406   unsigned humusneg     : 1;    /*bit 13*/
 407   unsigned partial      : 1;    /*bit 14*/
 408 #ifdef TRACE
 409   unsigned core         : 1;    /*bit 15*/
 410 #endif
 411   unsigned level;
 412   Cls *reason;
 413 #ifndef NADC
 414   Lit ** inado;
 415   Lit ** ado;
 416   Lit *** adotabpos;
 417 #endif
 418 };
 419
 420 struct Rnk
 421 {
 422   Act score;
 423   unsigned pos : 30;                    /* 0 iff not on heap */
 424   unsigned moreimportant : 1;
 425   unsigned lessimportant : 1;
 426 };
 427
 428 struct Cls
 429 {
 430   unsigned size;
 431
 432   unsigned collect:1;   /* bit 1 */
 433   unsigned learned:1;   /* bit 2 */
 434   unsigned locked:1;    /* bit 3 */
 435   unsigned used:1;      /* bit 4 */
 436 #ifndef NDEBUG
 437   unsigned connected:1; /* bit 5 */
 438 #endif
 439 #ifdef TRACE
 440   unsigned collected:1; /* bit 6 */
 441   unsigned core:1;      /* bit 7 */
 442 #endif
 443
 444 #define LDMAXGLUE 25    /* 32 - 7 */
 445 #define MAXGLUE         ((1<<LDMAXGLUE)-1)
 446
 447   unsigned glue:LDMAXGLUE;
 448
 449   Cls *next[2];
 450   Lit *lits[2];
 451 };
 452
 453 #ifdef TRACE
 454 struct Zhn
 455 {
 456   unsigned ref:31;
 457   unsigned core:1;
 458   Znt * liz;
 459   Znt znt[0];
 460 };
 461
 462 struct Trd
 463 {
 464   unsigned idx;
 465   Cls cls[0];
 466 };
 467 #endif
 468
 469 struct Blk
 470 {
 471 #ifndef NDEBUG
 472   union
 473   {
 474     size_t size;                /* this is what we really use */
 475     void *as_two_ptrs[2];       /* 2 * sizeof (void*) alignment of data */
 476   }
 477   header;
 478 #endif
 479   char data[BLK_FILL_BYTES];
 480 };
 481
 482 enum State
 483 {
 484   RESET = 0,
 485   READY = 1,
 486   SAT = 2,
 487   UNSAT = 3,
 488   UNKNOWN = 4,
 489 };
 490
 491 enum Phase
 492 {
 493   POSPHASE,
 494   NEGPHASE,
 495   JWLPHASE,
 496   RNDPHASE,
 497 };
 498
 499 struct PicoSAT
 500 {
 501   enum State state;
 502   enum Phase defaultphase;
 503   int last_sat_call_result;
 504
 505   FILE *out;
 506   char * prefix;
 507   int verbosity;
 508   int plain;
 509   unsigned LEVEL;
 510   unsigned max_var;
 511   unsigned size_vars;
 512
 513   Lit *lits;
 514   Var *vars;
 515   Rnk *rnks;
 516   Flt *jwh;
 517   Cls **htps;
 518 #ifndef NDSC
 519   Cls **dhtps;
 520 #endif
 521 #ifdef NO_BINARY_CLAUSES
 522   Ltk *impls;
 523   Cls impl, cimpl;
 524   int implvalid, cimplvalid;
 525 #else
 526   Cls **impls;
 527 #endif
 528   Lit **trail, **thead, **eot, **ttail, ** ttail2;
 529 #ifndef NADC
 530   Lit **ttailado;
 531 #endif
 532   unsigned adecidelevel;
 533   Lit **als, **alshead, **alstail, **eoals;
 534   Lit **CLS, **clshead, **eocls;
 535   int *rils, *rilshead, *eorils;
 536   int *cils, *cilshead, *eocils;
 537   int *fals, *falshead, *eofals;
 538   int *mass, szmass;
 539   int *mssass, szmssass;
 540   int *mcsass, nmcsass, szmcsass;
 541   int *humus, szhumus;
 542   Lit *failed_assumption;
 543   int extracted_all_failed_assumptions;
 544   Rnk **heap, **hhead, **eoh;
 545   Cls **oclauses, **ohead, **eoo;       /* original clauses */
 546   Cls **lclauses, **lhead, ** EOL;      /* learned clauses */
 547   int * soclauses, * sohead, * eoso; /* saved original clauses */
 548   int saveorig;
 549   int partial;
 550 #ifdef TRACE
 551   int trace;
 552   Zhn **zhains, **zhead, **eoz;
 553   int ocore;
 554 #endif
 555   FILE * rup;
 556   int rupstarted;
 557   int rupvariables;
 558   int rupclauses;
 559   Cls *mtcls;
 560   Cls *conflict;
 561   Lit **added, **ahead, **eoa;
 562   Var **marked, **mhead, **eom;
 563   Var **dfs, **dhead, **eod;
 564   Cls **resolved, **rhead, **eor;
 565   unsigned char *levels, *levelshead, *eolevels;
 566   unsigned *dused, *dusedhead, *eodused;
 567   unsigned char *buffer, *bhead, *eob;
 568   Act vinc, lscore, ilvinc, ifvinc;
 569 #ifdef VISCORES
 570   Act fvinc, nvinc;
 571 #endif
 572   Act cinc, lcinc, ilcinc, fcinc;
 573   unsigned srng;
 574   size_t current_bytes;
 575   size_t max_bytes;
 576   size_t recycled;
 577   double seconds, flseconds;
 578   double entered;
 579   unsigned nentered;
 580   int measurealltimeinlib;
 581   char *rline[2];
 582   int szrline, RCOUNT;
 583   double levelsum;
 584   unsigned iterations;
 585   int reports;
 586   int lastrheader;
 587   unsigned calls;
 588   unsigned decisions;
 589   unsigned restarts;
 590   unsigned simps;
 591   unsigned fsimplify;
 592   unsigned isimplify;
 593   unsigned reductions;
 594   unsigned lreduce;
 595   unsigned lreduceadjustcnt;
 596   unsigned lreduceadjustinc;
 597   unsigned lastreduceconflicts;
 598   unsigned llocked;     /* locked large learned clauses */
 599   unsigned lrestart;
 600 #ifdef NLUBY
 601   unsigned drestart;
 602   unsigned ddrestart;
 603 #else
 604   unsigned lubycnt;
 605   unsigned lubymaxdelta;
 606   int waslubymaxdelta;
 607 #endif
 608   unsigned long long lsimplify;
 609   unsigned long long propagations;
 610   unsigned long long lpropagations;
 611   unsigned fixed;               /* top level assignments */
 612 #ifndef NFL
 613   unsigned failedlits;
 614   unsigned ifailedlits;
 615   unsigned efailedlits;
 616   unsigned flcalls;
 617 #ifdef STATS
 618   unsigned flrounds;
 619   unsigned long long flprops;
 620   unsigned long long floopsed, fltried, flskipped;
 621 #endif
 622   unsigned long long fllimit;
 623   int simplifying;
 624   Lit ** saved;
 625   unsigned saved_size;
 626 #endif
 627   unsigned conflicts;
 628   unsigned contexts;
 629   unsigned internals;
 630   unsigned noclauses;   /* current number large original clauses */
 631   unsigned nlclauses;   /* current number large learned clauses */
 632   unsigned olits;               /* current literals in large original clauses */
 633   unsigned llits;               /* current literals in large learned clauses */
 634   unsigned oadded;              /* added original clauses */
 635   unsigned ladded;              /* added learned clauses */
 636   unsigned loadded;     /* added original large clauses */
 637   unsigned lladded;     /* added learned large clauses */
 638   unsigned addedclauses;        /* oadded + ladded */
 639   unsigned vused;               /* used variables */
 640   unsigned llitsadded;  /* added learned literals */
 641   unsigned long long visits;
 642 #ifdef STATS
 643   unsigned loused;              /* used large original clauses */
 644   unsigned llused;              /* used large learned clauses */
 645   unsigned long long bvisits;
 646   unsigned long long tvisits;
 647   unsigned long long lvisits;
 648   unsigned long long othertrue;
 649   unsigned long long othertrue2;
 650   unsigned long long othertruel;
 651   unsigned long long othertrue2u;
 652   unsigned long long othertruelu;
 653   unsigned long long ltraversals;
 654   unsigned long long traversals;
 655 #ifdef TRACE
 656   unsigned long long antecedents;
 657 #endif
 658   unsigned uips;
 659   unsigned znts;
 660   unsigned assumptions;
 661   unsigned rdecisions;
 662   unsigned sdecisions;
 663   size_t srecycled;
 664   size_t rrecycled;
 665   unsigned long long derefs;
 666 #endif
 667   unsigned minimizedllits;
 668   unsigned nonminimizedllits;
 669 #ifndef NADC
 670   Lit *** ados, *** hados, *** eados;
 671   Lit *** adotab;
 672   unsigned nadotab;
 673   unsigned szadotab;
 674   Cls * adoconflict;
 675   unsigned adoconflicts;
 676   unsigned adoconflictlimit;
 677   int addingtoado;
 678   int adodisabled;
 679 #endif
 680   unsigned long long flips;
 681 #ifdef STATS
 682   unsigned long long FORCED;
 683   unsigned long long assignments;
 684   unsigned inclreduces;
 685   unsigned staticphasedecisions;
 686   unsigned skippedrestarts;
 687 #endif
 688   int * indices, * ihead, *eoi;
 689   unsigned sdflips;
 690
 691   unsigned long long saved_flips;
 692   unsigned saved_max_var;
 693   unsigned min_flipped;
 694
 695   void * emgr;
 696   picosat_malloc enew;
 697   picosat_realloc eresize;
 698   picosat_free edelete;
 699
 700 #ifdef VISCORES
 701   FILE * fviscores;
 702 #endif
 703 };
 704
 705 typedef PicoSAT PS;
 706
 707 static Flt
 708 packflt (unsigned m, int e)
 709 {
 710   Flt res;
 711   assert (m < FLTMSB);
 712   assert (FLTMINEXPONENT <= e);
 713   assert (e <= FLTMAXEXPONENT);
 714   res = m | ((e + 128) << 24);
 715   return res;
 716 }
 717
 718 static Flt
 719 base2flt (unsigned m, int e)
 720 {
 721   if (!m)
 722     return ZEROFLT;
 723
 724   if (m < FLTMSB)
 725     {
 726       do
 727         {
 728           if (e <= FLTMINEXPONENT)
 729             return EPSFLT;
 730
 731           e--;
 732           m <<= 1;
 733
 734         }
 735       while (m < FLTMSB);
 736     }
 737   else
 738     {
 739       while (m >= FLTCARRY)
 740         {
 741           if (e >= FLTMAXEXPONENT)
 742             return INFFLT;
 743
 744           e++;
 745           m >>= 1;
 746         }
 747     }
 748
 749   m &= ~FLTMSB;
 750   return packflt (m, e);
 751 }
 752
 753 static Flt
 754 addflt (Flt a, Flt b)
 755 {
 756   unsigned ma, mb, delta;
 757   int ea, eb;
 758
 759   CMPSWAPFLT (a, b);
 760   if (!b)
 761     return a;
 762
 763   UNPACKFLT (a, ma, ea);
 764   UNPACKFLT (b, mb, eb);
 765
 766   assert (ea >= eb);
 767   delta = ea - eb;
 768   mb >>= delta;
 769   if (!mb)
 770     return a;
 771
 772   ma += mb;
 773   if (ma & FLTCARRY)
 774     {
 775       if (ea == FLTMAXEXPONENT)
 776         return INFFLT;
 777
 778       ea++;
 779       ma >>= 1;
 780     }
 781
 782   assert (ma < FLTCARRY);
 783   ma &= FLTMAXMANTISSA;
 784
 785   return packflt (ma, ea);
 786 }
 787
 788 static Flt
 789 mulflt (Flt a, Flt b)
 790 {
 791   unsigned ma, mb;
 792   unsigned long long accu;
 793   int ea, eb;
 794
 795   CMPSWAPFLT (a, b);
 796   if (!b)
 797     return ZEROFLT;
 798
 799   UNPACKFLT (a, ma, ea);
 800   UNPACKFLT (b, mb, eb);
 801
 802   ea += eb;
 803   ea += 24;
 804   if (ea > FLTMAXEXPONENT)
 805     return INFFLT;
 806
 807   if (ea < FLTMINEXPONENT)
 808     return EPSFLT;
 809
 810   accu = ma;
 811   accu *= mb;
 812   accu >>= 24;
 813
 814   if (accu >= FLTCARRY)
 815     {
 816       if (ea == FLTMAXEXPONENT)
 817         return INFFLT;
 818
 819       ea++;
 820       accu >>= 1;
 821
 822       if (accu >= FLTCARRY)
 823         return INFFLT;
 824     }
 825
 826   assert (accu < FLTCARRY);
 827   assert (accu & FLTMSB);
 828
 829   ma = accu;
 830   ma &= ~FLTMSB;
 831
 832   return packflt (ma, ea);
 833 }
 834
 835 static Flt
 836 ascii2flt (const char *str)
 837 {
 838   Flt ten = base2flt (10, 0);
 839   Flt onetenth = base2flt (26843546, -28);
 840   Flt res = ZEROFLT, tmp, base;
 841   const char *p = str;
 842   char ch;
 843
 844   ch = *p++;
 845
 846   if (ch != '.')
 847     {
 848       if (!isdigit (ch))
 849         return INFFLT;  /* better abort ? */
 850
 851       res = base2flt (ch - '0', 0);
 852
 853       while ((ch = *p++))
 854         {
 855           if (ch == '.')
 856             break;
 857
 858           if (!isdigit (ch))
 859             return INFFLT;      /* better abort? */
 860
 861           res = mulflt (res, ten);
 862           tmp = base2flt (ch - '0', 0);
 863           res = addflt (res, tmp);
 864         }
 865     }
 866
 867   if (ch == '.')
 868     {
 869       ch = *p++;
 870       if (!isdigit (ch))
 871         return INFFLT;  /* better abort ? */
 872
 873       base = onetenth;
 874       tmp = mulflt (base2flt (ch - '0', 0), base);
 875       res = addflt (res, tmp);
 876
 877       while ((ch = *p++))
 878         {
 879           if (!isdigit (ch))
 880             return INFFLT;      /* better abort? */
 881
 882           base = mulflt (base, onetenth);
 883           tmp = mulflt (base2flt (ch - '0', 0), base);
 884           res = addflt (res, tmp);
 885         }
 886     }
 887
 888   return res;
 889 }
 890
 891 #if defined(VISCORES)
 892
 893 static double
 894 flt2double (Flt f)
 895 {
 896   double res;
 897   unsigned m;
 898   int e, i;
 899
 900   UNPACKFLT (f, m, e);
 901   res = m;
 902
 903   if (e < 0)
 904     {
 905       for (i = e; i < 0; i++)
 906         res *= 0.5;
 907     }
 908   else
 909     {
 910       for (i = 0; i < e; i++)
 911         res *= 2.0;
 912     }
 913
 914   return res;
 915 }
 916
 917 #endif
 918
 919 static int
 920 log2flt (Flt a)
 921 {
 922   return FLTEXPONENT (a) + 24;
 923 }
 924
 925 static int
 926 cmpflt (Flt a, Flt b)
 927 {
 928   if (a < b)
 929     return -1;
 930
 931   if (a > b)
 932     return 1;
 933
 934   return 0;
 935 }
 936
 937 static void *
 938 new (PS * ps, size_t size)
 939 {
 940   size_t bytes;
 941   Blk *b;
 942
 943   if (!size)
 944     return 0;
 945
 946   bytes = size + SIZE_OF_BLK;
 947
 948   if (ps->enew)
 949     b = ps->enew (ps->emgr, bytes);
 950   else
 951     b = malloc (bytes);
 952
 953   ABORTIF (!b, "out of memory in 'new'");
 954 #ifndef NDEBUG
 955   b->header.size = size;
 956 #endif
 957   ps->current_bytes += size;
 958   if (ps->current_bytes > ps->max_bytes)
 959     ps->max_bytes = ps->current_bytes;
 960   return b->data;
 961 }
 962
 963 static void
 964 delete (PS * ps, void *void_ptr, size_t size)
 965 {
 966   size_t bytes;
 967   Blk *b;
 968
 969   if (!void_ptr)
 970     {
 971       assert (!size);
 972       return;
 973     }
 974
 975   assert (size);
 976   b = PTR2BLK (void_ptr);
 977
 978   assert (size <= ps->current_bytes);
 979   ps->current_bytes -= size;
 980
 981   assert (b->header.size == size);
 982
 983   bytes = size + SIZE_OF_BLK;
 984   if (ps->edelete)
 985     ps->edelete (ps->emgr, b, bytes);
 986   else
 987     free (b);
 988 }
 989
 990 static void *
 991 resize (PS * ps, void *void_ptr, size_t old_size, size_t new_size)
 992 {
 993   size_t old_bytes, new_bytes;
 994   Blk *b;
 995
 996   b = PTR2BLK (void_ptr);
 997
 998   assert (old_size <= ps->current_bytes);
 999   ps->current_bytes -= old_size;
1000
1001   if ((old_bytes = old_size))
1002     {
1003       assert (old_size && b && b->header.size == old_size);
1004       old_bytes += SIZE_OF_BLK;
1005     }
1006   else
1007     assert (!b);
1008
1009   if ((new_bytes = new_size))
1010     new_bytes += SIZE_OF_BLK;
1011
1012   if (ps->eresize)
1013     b = ps->eresize (ps->emgr, b, old_bytes, new_bytes);
1014   else
1015     b = realloc (b, new_bytes);
1016
1017   if (!new_size)
1018     {
1019       assert (!b);
1020       return 0;
1021     }
1022
1023   ABORTIF (!b, "out of memory in 'resize'");
1024 #ifndef NDEBUG
1025   b->header.size = new_size;
1026 #endif
1027
1028   ps->current_bytes += new_size;
1029   if (ps->current_bytes > ps->max_bytes)
1030     ps->max_bytes = ps->current_bytes;
1031
1032   return b->data;
1033 }
1034
1035 static unsigned
1036 int2unsigned (int l)
1037 {
1038   return (l < 0) ? 1 + 2 * -l : 2 * l;
1039 }
1040
1041 static Lit *
1042 int2lit (PS * ps, int l)
1043 {
1044   return ps->lits + int2unsigned (l);
1045 }
1046
1047 static Lit **
1048 end_of_lits (Cls * c)
1049 {
1050   return c->lits + c->size;
1051 }
1052
1053 #if !defined(NDEBUG) || defined(LOGGING)
1054
1055 static void
1056 dumplits (PS * ps, Lit ** l, Lit ** end)
1057 {
1058   int first;
1059   Lit ** p;
1060
1061   if (l == end)
1062     {
1063       /* empty clause */
1064     }
1065   else if (l + 1 == end)
1066     {
1067       fprintf (ps->out, "%d ", LIT2INT (l[0]));
1068     }
1069   else
1070     {
1071       assert (l + 2 <= end);
1072       first = (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1])));
1073       fprintf (ps->out, "%d ", LIT2INT (l[first]));
1074       fprintf (ps->out, "%d ", LIT2INT (l[!first]));
1075       for (p = l + 2; p < end; p++)
1076          fprintf (ps->out, "%d ", LIT2INT (*p));
1077     }
1078
1079   fputc ('0', ps->out);
1080 }
1081
1082 static void
1083 dumpcls (PS * ps, Cls * c)
1084 {
1085   Lit **end;
1086
1087   if (c)
1088     {
1089       end = end_of_lits (c);
1090       dumplits (ps, c->lits, end);
1091 #ifdef TRACE
1092       if (ps->trace)
1093          fprintf (ps->out, " clause(%u)", CLS2IDX (c));
1094 #endif
1095     }
1096   else
1097     fputs ("DECISION", ps->out);
1098 }
1099
1100 static void
1101 dumpclsnl (PS * ps, Cls * c)
1102 {
1103   dumpcls (ps, c);
1104   fputc ('\n', ps->out);
1105 }
1106
1107 void
1108 dumpcnf (PS * ps)
1109 {
1110   Cls **p, *c;
1111
1112   for (p = SOC; p != EOC; p = NXC (p))
1113     {
1114       c = *p;
1115
1116       if (!c)
1117         continue;
1118
1119 #ifdef TRACE
1120       if (c->collected)
1121         continue;
1122 #endif
1123
1124       dumpclsnl (ps, *p);
1125     }
1126 }
1127
1128 #endif
1129
1130 static void
1131 delete_prefix (PS * ps)
1132 {
1133   if (!ps->prefix)
1134     return;
1135
1136   delete (ps, ps->prefix, strlen (ps->prefix) + 1);
1137   ps->prefix = 0;
1138 }
1139
1140 static void
1141 new_prefix (PS * ps, const char * str)
1142 {
1143   delete_prefix (ps);
1144   assert (str);
1145   ps->prefix = new (ps, strlen (str) + 1);
1146   strcpy (ps->prefix, str);
1147 }
1148
1149 static PS *
1150 init (void * pmgr,
1151       picosat_malloc pnew, picosat_realloc presize, picosat_free pdelete)
1152 {
1153   PS * ps;
1154
1155 #if 0
1156   int count = 3 - !pnew - !presize - !pdelete;
1157
1158   ABORTIF (count && !pnew, "API usage: missing 'picosat_set_new'");
1159   ABORTIF (count && !presize, "API usage: missing 'picosat_set_resize'");
1160   ABORTIF (count && !pdelete, "API usage: missing 'picosat_set_delete'");
1161 #endif
1162
1163   ps = pnew ? pnew (pmgr, sizeof *ps) : malloc (sizeof *ps);
1164   ABORTIF (!ps, "failed to allocate memory for PicoSAT manager");
1165   memset (ps, 0, sizeof *ps);
1166
1167   ps->emgr = pmgr;
1168   ps->enew = pnew;
1169   ps->eresize = presize;
1170   ps->edelete = pdelete;
1171
1172   ps->size_vars = 1;
1173   ps->state = RESET;
1174   ps->defaultphase = JWLPHASE;
1175 #ifdef TRACE
1176   ps->ocore = -1;
1177 #endif
1178   ps->lastrheader = -2;
1179 #ifndef NADC
1180   ps->adoconflictlimit = UINT_MAX;
1181 #endif
1182   ps->min_flipped = UINT_MAX;
1183
1184   NEWN (ps->lits, 2 * ps->size_vars);
1185   NEWN (ps->jwh, 2 * ps->size_vars);
1186   NEWN (ps->htps, 2 * ps->size_vars);
1187 #ifndef NDSC
1188   NEWN (ps->dhtps, 2 * ps->size_vars);
1189 #endif
1190   NEWN (ps->impls, 2 * ps->size_vars);
1191   NEWN (ps->vars, ps->size_vars);
1192   NEWN (ps->rnks, ps->size_vars);
1193
1194   /* because '0' pos denotes not on heap
1195    */
1196   ENLARGE (ps->heap, ps->hhead, ps->eoh);
1197   ps->hhead = ps->heap + 1;
1198
1199   ps->vinc = base2flt (1, 0);           /* initial var activity */
1200   ps->ifvinc = ascii2flt ("1.05");      /* var score rescore factor */
1201 #ifdef VISCORES
1202   ps->fvinc = ascii2flt ("0.9523809");  /*     1/f =     1/1.05 */
1203   ps->nvinc = ascii2flt ("0.0476191");  /* 1 - 1/f = 1 - 1/1.05 */
1204 #endif
1205   ps->lscore = base2flt (1, 90);        /* var activity rescore limit */
1206   ps->ilvinc = base2flt (1, -90);       /* inverse of 'lscore' */
1207
1208   ps->cinc = base2flt (1, 0);           /* initial clause activity */
1209   ps->fcinc = ascii2flt ("1.001");      /* cls activity rescore factor */
1210   ps->lcinc = base2flt (1, 90);         /* cls activity rescore limit */
1211   ps->ilcinc = base2flt (1, -90);       /* inverse of 'ilcinc' */
1212
1213   ps->lreduceadjustcnt = ps->lreduceadjustinc = 100;
1214   ps->lpropagations = ~0ull;
1215
1216   ps->out = stdout;
1217   new_prefix (ps, "c ");
1218   ps->verbosity = 0;
1219   ps->plain = 0;
1220
1221 #ifdef NO_BINARY_CLAUSES
1222   memset (&ps->impl, 0, sizeof (ps->impl));
1223   ps->impl.size = 2;
1224
1225   memset (&ps->cimpl, 0, sizeof (ps->impl));
1226   ps->cimpl.size = 2;
1227 #endif
1228
1229 #ifdef VISCORES
1230   ps->fviscores = popen (
1231     "/usr/bin/gnuplot -background black"
1232     " -xrm 'gnuplot*textColor:white'"
1233     " -xrm 'gnuplot*borderColor:white'"
1234     " -xrm 'gnuplot*axisColor:white'"
1235     , "w");
1236   fprintf (ps->fviscores, "unset key\n");
1237   // fprintf (ps->fviscores, "set log y\n");
1238   fflush (ps->fviscores);
1239   system ("rm -rf /tmp/picosat-viscores");
1240   system ("mkdir /tmp/picosat-viscores");
1241   system ("mkdir /tmp/picosat-viscores/data");
1242 #ifdef WRITEGIF
1243   system ("mkdir /tmp/picosat-viscores/gif");
1244   fprintf (ps->fviscores,
1245            "set terminal gif giant animate opt size 1024,768 x000000 xffffff"
1246            "\n");
1247
1248   fprintf (ps->fviscores,
1249            "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n");
1250 #endif
1251 #endif
1252   ps->defaultphase = JWLPHASE;
1253   ps->state = READY;
1254   ps->last_sat_call_result = 0;
1255
1256   return ps;
1257 }
1258
1259 static size_t
1260 bytes_clause (PS * ps, unsigned size, unsigned learned)
1261 {
1262   size_t res;
1263
1264   res = sizeof (Cls);
1265   res += size * sizeof (Lit *);
1266   res -= 2 * sizeof (Lit *);
1267
1268   if (learned && size > 2)
1269     res += sizeof (Act);        /* add activity */
1270
1271 #ifdef TRACE
1272   if (ps->trace)
1273     res += sizeof (Trd);        /* add trace data */
1274 #else
1275   (void) ps;
1276 #endif
1277
1278   return res;
1279 }
1280
1281 static Cls *
1282 new_clause (PS * ps, unsigned size, unsigned learned)
1283 {
1284   size_t bytes;
1285   void * tmp;
1286 #ifdef TRACE
1287   Trd *trd;
1288 #endif
1289   Cls *res;
1290
1291   bytes = bytes_clause (ps, size, learned);
1292   tmp = new (ps, bytes);
1293
1294 #ifdef TRACE
1295   if (ps->trace)
1296     {
1297       trd = tmp;
1298
1299       if (learned)
1300         trd->idx = LIDX2IDX (ps->lhead - ps->lclauses);
1301       else
1302         trd->idx = OIDX2IDX (ps->ohead - ps->oclauses);
1303
1304       res = trd->cls;
1305     }
1306   else
1307 #endif
1308     res = tmp;
1309
1310   res->size = size;
1311   res->learned = learned;
1312
1313   res->collect = 0;
1314 #ifndef NDEBUG
1315   res->connected = 0;
1316 #endif
1317   res->locked = 0;
1318   res->used = 0;
1319 #ifdef TRACE
1320   res->core = 0;
1321   res->collected = 0;
1322 #endif
1323
1324   if (learned && size > 2)
1325     {
1326       Act * p = CLS2ACT (res);
1327       *p = ps->cinc;
1328     }
1329
1330   return res;
1331 }
1332
1333 static void
1334 delete_clause (PS * ps, Cls * c)
1335 {
1336   size_t bytes;
1337 #ifdef TRACE
1338   Trd *trd;
1339 #endif
1340
1341   bytes = bytes_clause (ps, c->size, c->learned);
1342
1343 #ifdef TRACE
1344   if (ps->trace)
1345     {
1346       trd = CLS2TRD (c);
1347       delete (ps, trd, bytes);
1348     }
1349   else
1350 #endif
1351     delete (ps, c, bytes);
1352 }
1353
1354 static void
1355 delete_clauses (PS * ps)
1356 {
1357   Cls **p;
1358   for (p = SOC; p != EOC; p = NXC (p))
1359     if (*p)
1360       delete_clause (ps, *p);
1361
1362   DELETEN (ps->oclauses, ps->eoo - ps->oclauses);
1363   DELETEN (ps->lclauses, ps->EOL - ps->lclauses);
1364
1365   ps->ohead = ps->eoo = ps->lhead = ps->EOL = 0;
1366 }
1367
1368 #ifdef TRACE
1369
1370 static void
1371 delete_zhain (PS * ps, Zhn * zhain)
1372 {
1373   const Znt *p, *znt;
1374
1375   assert (zhain);
1376
1377   znt = zhain->znt;
1378   for (p = znt; *p; p++)
1379     ;
1380
1381   delete (ps, zhain, sizeof (Zhn) + (p - znt) + 1);
1382 }
1383
1384 static void
1385 delete_zhains (PS * ps)
1386 {
1387   Zhn **p, *z;
1388   for (p = ps->zhains; p < ps->zhead; p++)
1389     if ((z = *p))
1390       delete_zhain (ps, z);
1391
1392   DELETEN (ps->zhains, ps->eoz - ps->zhains);
1393   ps->eoz = ps->zhead = 0;
1394 }
1395
1396 #endif
1397
1398 #ifdef NO_BINARY_CLAUSES
1399 static void
1400 lrelease (PS * ps, Ltk * stk)
1401 {
1402   if (stk->start)
1403     DELETEN (stk->start, (1 << (stk->ldsize)));
1404   memset (stk, 0, sizeof (*stk));
1405 }
1406 #endif
1407
1408 #ifndef NADC
1409
1410 static unsigned
1411 llength (Lit ** a)
1412 {
1413   Lit ** p;
1414   for (p = a; *p; p++)
1415     ;
1416   return p - a;
1417 }
1418
1419 static void
1420 resetadoconflict (PS * ps)
1421 {
1422   assert (ps->adoconflict);
1423   delete_clause (ps->adoconflict);
1424   ps->adoconflict = 0;
1425 }
1426
1427 static void
1428 reset_ados (PS * ps)
1429 {
1430   Lit *** p;
1431
1432   for (p = ps->ados; p < ps->hados; p++)
1433     DELETEN (*p, llength (*p) + 1);
1434
1435   DELETEN (ps->ados, ps->eados - ps->ados);
1436   ps->hados = ps->eados = 0;
1437
1438   DELETEN (ps->adotab, ps->szadotab);
1439   ps->szadotab = ps->nadotab = 0;
1440
1441   if (ps->adoconflict)
1442     resetadoconflict (ps);
1443
1444   ps->adoconflicts = 0;
1445   ps->adoconflictlimit = UINT_MAX;
1446   ps->adodisabled = 0;
1447 }
1448
1449 #endif
1450
1451 static void
1452 reset (PS * ps)
1453 {
1454   ABORTIF (!ps ||
1455            ps->state == RESET, "API usage: reset without initialization");
1456
1457   delete_clauses (ps);
1458 #ifdef TRACE
1459   delete_zhains (ps);
1460 #endif
1461 #ifdef NO_BINARY_CLAUSES
1462   {
1463     unsigned i;
1464     for (i = 2; i <= 2 * ps->max_var + 1; i++)
1465       lrelease (ps, ps->impls + i);
1466   }
1467 #endif
1468 #ifndef NADC
1469   reset_ados (ps);
1470 #endif
1471 #ifndef NFL
1472   DELETEN (ps->saved, ps->saved_size);
1473 #endif
1474   DELETEN (ps->htps, 2 * ps->size_vars);
1475 #ifndef NDSC
1476   DELETEN (ps->dhtps, 2 * ps->size_vars);
1477 #endif
1478   DELETEN (ps->impls, 2 * ps->size_vars);
1479   DELETEN (ps->lits, 2 * ps->size_vars);
1480   DELETEN (ps->jwh, 2 * ps->size_vars);
1481   DELETEN (ps->vars, ps->size_vars);
1482   DELETEN (ps->rnks, ps->size_vars);
1483   DELETEN (ps->trail, ps->eot - ps->trail);
1484   DELETEN (ps->heap, ps->eoh - ps->heap);
1485   DELETEN (ps->als, ps->eoals - ps->als);
1486   DELETEN (ps->CLS, ps->eocls - ps->CLS);
1487   DELETEN (ps->rils, ps->eorils - ps->rils);
1488   DELETEN (ps->cils, ps->eocils - ps->cils);
1489   DELETEN (ps->fals, ps->eofals - ps->fals);
1490   DELETEN (ps->mass, ps->szmass);
1491   DELETEN (ps->mssass, ps->szmssass);
1492   DELETEN (ps->mcsass, ps->szmcsass);
1493   DELETEN (ps->humus, ps->szhumus);
1494   DELETEN (ps->added, ps->eoa - ps->added);
1495   DELETEN (ps->marked, ps->eom - ps->marked);
1496   DELETEN (ps->dfs, ps->eod - ps->dfs);
1497   DELETEN (ps->resolved, ps->eor - ps->resolved);
1498   DELETEN (ps->levels, ps->eolevels - ps->levels);
1499   DELETEN (ps->dused, ps->eodused - ps->dused);
1500   DELETEN (ps->buffer, ps->eob - ps->buffer);
1501   DELETEN (ps->indices, ps->eoi - ps->indices);
1502   DELETEN (ps->soclauses, ps->eoso - ps->soclauses);
1503   delete_prefix (ps);
1504   delete (ps, ps->rline[0], ps->szrline);
1505   delete (ps, ps->rline[1], ps->szrline);
1506   assert (getenv ("LEAK") || !ps->current_bytes);       /* found leak if failing */
1507 #ifdef VISCORES
1508   pclose (ps->fviscores);
1509 #endif
1510   if (ps->edelete)
1511     ps->edelete (ps->emgr, ps, sizeof *ps);
1512   else
1513     free (ps);
1514 }
1515
1516 inline static void
1517 tpush (PS * ps, Lit * lit)
1518 {
1519   assert (ps->lits < lit && lit <= ps->lits + 2* ps->max_var + 1);
1520   if (ps->thead == ps->eot)
1521     {
1522       unsigned ttail2count = ps->ttail2 - ps->trail;
1523       unsigned ttailcount = ps->ttail - ps->trail;
1524 #ifndef NADC
1525       unsigned ttailadocount = ps->ttailado - ps->trail;
1526 #endif
1527       ENLARGE (ps->trail, ps->thead, ps->eot);
1528       ps->ttail = ps->trail + ttailcount;
1529       ps->ttail2 = ps->trail + ttail2count;
1530 #ifndef NADC
1531       ps->ttailado = ps->trail + ttailadocount;
1532 #endif
1533     }
1534
1535   *ps->thead++ = lit;
1536 }
1537
1538 static void
1539 assign_reason (PS * ps, Var * v, Cls * reason)
1540 {
1541 #if defined(NO_BINARY_CLAUSES) && !defined(NDEBUG)
1542   assert (reason != &ps->impl);
1543 #else
1544   (void) ps;
1545 #endif
1546   v->reason = reason;
1547 }
1548
1549 static void
1550 assign_phase (PS * ps, Lit * lit)
1551 {
1552   unsigned new_phase, idx;
1553   Var * v = LIT2VAR (lit);
1554
1555 #ifndef NFL
1556   /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if
1557    * we force assignments on the top level.   The other assignments will be
1558    * undone and thus we can keep the old saved value of the phase.
1559    */
1560   if (!ps->LEVEL || !ps->simplifying)
1561 #endif
1562     {
1563       new_phase = (LIT2SGN (lit) > 0);
1564
1565       if (v->assigned)
1566         {
1567           ps->sdflips -= ps->sdflips/FFLIPPED;
1568
1569           if (new_phase != v->phase)
1570             {
1571               assert (FFLIPPEDPREC >= FFLIPPED);
1572               ps->sdflips += FFLIPPEDPREC / FFLIPPED;
1573               ps->flips++;
1574
1575               idx = LIT2IDX (lit);
1576               if (idx < ps->min_flipped)
1577                 ps->min_flipped = idx;
1578
1579               NOLOG (fprintf (ps->out,
1580                               "%sflipped %d\n",
1581                                ps->prefix, LIT2INT (lit)));
1582             }
1583         }
1584
1585       v->phase = new_phase;
1586       v->assigned = 1;
1587     }
1588
1589   lit->val = TRUE;
1590   NOTLIT (lit)->val = FALSE;
1591 }
1592
1593 inline static void
1594 assign (PS * ps, Lit * lit, Cls * reason)
1595 {
1596   Var * v = LIT2VAR (lit);
1597   assert (lit->val == UNDEF);
1598 #ifdef STATS
1599   ps->assignments++;
1600 #endif
1601   v->level = ps->LEVEL;
1602   assign_phase (ps, lit);
1603   assign_reason (ps, v, reason);
1604   tpush (ps, lit);
1605 }
1606
1607 inline static int
1608 cmp_added (PS * ps, Lit * k, Lit * l)
1609 {
1610   Val a = k->val, b = l->val;
1611   Var *u, *v;
1612   int res;
1613
1614   if (a == UNDEF && b != UNDEF)
1615     return -1;
1616
1617   if (a != UNDEF && b == UNDEF)
1618     return 1;
1619
1620   u = LIT2VAR (k);
1621   v = LIT2VAR (l);
1622
1623   if (a != UNDEF)
1624     {
1625       assert (b != UNDEF);
1626       res = v->level - u->level;
1627       if (res)
1628         return res;             /* larger level first */
1629     }
1630
1631   res = cmpflt (VAR2RNK (u)->score, VAR2RNK (v)->score);
1632   if (res)
1633     return res;                 /* smaller activity first */
1634
1635   return u - v;                 /* smaller index first */
1636 }
1637
1638 static void
1639 sorttwolits (Lit ** v)
1640 {
1641   Lit * a = v[0], * b = v[1];
1642
1643   assert (a != b);
1644
1645   if (a < b)
1646     return;
1647
1648   v[0] = b;
1649   v[1] = a;
1650 }
1651
1652 inline static void
1653 sortlits (PS * ps, Lit ** v, unsigned size)
1654 {
1655   if (size == 2)
1656     sorttwolits (v);    /* same order with and with out 'NO_BINARY_CLAUSES' */
1657   else
1658     SORT (Lit *, cmp_added, v, size);
1659 }
1660
1661 #ifdef NO_BINARY_CLAUSES
1662 static Cls *
1663 setimpl (PS * ps, Lit * a, Lit * b)
1664 {
1665   assert (!ps->implvalid);
1666   assert (ps->impl.size == 2);
1667
1668   ps->impl.lits[0] = a;
1669   ps->impl.lits[1] = b;
1670
1671   sorttwolits (ps->impl.lits);
1672   ps->implvalid = 1;
1673
1674   return &ps->impl;
1675 }
1676
1677 static void
1678 resetimpl (PS * ps)
1679 {
1680   ps->implvalid = 0;
1681 }
1682
1683 static Cls *
1684 setcimpl (PS * ps, Lit * a, Lit * b)
1685 {
1686   assert (!ps->cimplvalid);
1687   assert (ps->cimpl.size == 2);
1688
1689   ps->cimpl.lits[0] = a;
1690   ps->cimpl.lits[1] = b;
1691
1692   sorttwolits (ps->cimpl.lits);
1693   ps->cimplvalid = 1;
1694
1695   return &ps->cimpl;
1696 }
1697
1698 static void
1699 resetcimpl (PS * ps)
1700 {
1701   assert (ps->cimplvalid);
1702   ps->cimplvalid = 0;
1703 }
1704
1705 #endif
1706
1707 static int
1708 cmp_ptr (PS * ps, void *l, void *k)
1709 {
1710   (void) ps;
1711   return ((char*)l) - (char*)k;         /* arbitrarily already reverse */
1712 }
1713
1714 static int
1715 cmp_rnk (Rnk * r, Rnk * s)
1716 {
1717   if (!r->moreimportant && s->moreimportant)
1718     return -1;
1719
1720   if (r->moreimportant && !s->moreimportant)
1721     return 1;
1722
1723   if (!r->lessimportant && s->lessimportant)
1724     return 1;
1725
1726   if (r->lessimportant && !s->lessimportant)
1727     return -1;
1728
1729   if (r->score < s->score)
1730     return -1;
1731
1732   if (r->score > s->score)
1733     return 1;
1734
1735   return -cmp_ptr (0, r, s);
1736 }
1737
1738 static void
1739 hup (PS * ps, Rnk * v)
1740 {
1741   int upos, vpos;
1742   Rnk *u;
1743
1744 #ifndef NFL
1745   assert (!ps->simplifying);
1746 #endif
1747
1748   vpos = v->pos;
1749
1750   assert (0 < vpos);
1751   assert (vpos < ps->hhead - ps->heap);
1752   assert (ps->heap[vpos] == v);
1753
1754   while (vpos > 1)
1755     {
1756       upos = vpos / 2;
1757
1758       u = ps->heap[upos];
1759
1760       if (cmp_rnk (u, v) > 0)
1761         break;
1762
1763       ps->heap[vpos] = u;
1764       u->pos = vpos;
1765
1766       vpos = upos;
1767     }
1768
1769   ps->heap[vpos] = v;
1770   v->pos = vpos;
1771 }
1772
1773 static Cls *add_simplified_clause (PS *, int);
1774
1775 inline static void
1776 add_antecedent (PS * ps, Cls * c)
1777 {
1778   assert (c);
1779
1780 #ifdef NO_BINARY_CLAUSES
1781   if (ISLITREASON (c))
1782     return;
1783
1784   if (c == &ps->impl)
1785     return;
1786 #elif defined(STATS) && defined(TRACE)
1787   ps->antecedents++;
1788 #endif
1789   if (ps->rhead == ps->eor)
1790     ENLARGE (ps->resolved, ps->rhead, ps->eor);
1791
1792   assert (ps->rhead < ps->eor);
1793   *ps->rhead++ = c;
1794 }
1795
1796 #ifdef TRACE
1797
1798 #ifdef NO_BINARY_CLAUSES
1799 #error "can not combine TRACE and NO_BINARY_CLAUSES"
1800 #endif
1801
1802 #endif /* TRACE */
1803
1804 static void
1805 add_lit (PS * ps, Lit * lit)
1806 {
1807   assert (lit);
1808
1809   if (ps->ahead == ps->eoa)
1810     ENLARGE (ps->added, ps->ahead, ps->eoa);
1811
1812   *ps->ahead++ = lit;
1813 }
1814
1815 static void
1816 push_var_as_marked (PS * ps, Var * v)
1817 {
1818   if (ps->mhead == ps->eom)
1819     ENLARGE (ps->marked, ps->mhead, ps->eom);
1820
1821   *ps->mhead++ = v;
1822 }
1823
1824 static void
1825 mark_var (PS * ps, Var * v)
1826 {
1827   assert (!v->mark);
1828   v->mark = 1;
1829   push_var_as_marked (ps, v);
1830 }
1831
1832 #ifdef NO_BINARY_CLAUSES
1833
1834 static Cls *
1835 impl2reason (PS * ps, Lit * lit)
1836 {
1837   Lit * other;
1838   Cls * res;
1839   other = ps->impl.lits[0];
1840   if (lit == other)
1841     other = ps->impl.lits[1];
1842   assert (other->val == FALSE);
1843   res = LIT2REASON (NOTLIT (other));
1844   resetimpl (ps);
1845   return res;
1846 }
1847
1848 #endif
1849
1850 /* Whenever we have a top level derived unit we really should derive a unit
1851  * clause otherwise the resolutions in 'add_simplified_clause' become
1852  * incorrect.
1853  */
1854 static Cls *
1855 resolve_top_level_unit (PS * ps, Lit * lit, Cls * reason)
1856 {
1857   unsigned count_resolved;
1858   Lit **p, **eol, *other;
1859   Var *u, *v;
1860
1861   assert (ps->rhead == ps->resolved);
1862   assert (ps->ahead == ps->added);
1863
1864   add_lit (ps, lit);
1865   add_antecedent (ps, reason);
1866   count_resolved = 1;
1867   v = LIT2VAR (lit);
1868
1869   eol = end_of_lits (reason);
1870   for (p = reason->lits; p < eol; p++)
1871     {
1872       other = *p;
1873       u = LIT2VAR (other);
1874       if (u == v)
1875         continue;
1876
1877       add_antecedent (ps, u->reason);
1878       count_resolved++;
1879     }
1880
1881   /* Some of the literals could be assumptions.  If at least one
1882    * variable is not an assumption, we should resolve.
1883    */
1884   if (count_resolved >= 2)
1885     {
1886 #ifdef NO_BINARY_CLAUSES
1887       if (reason == &ps->impl)
1888         resetimpl (ps);
1889 #endif
1890       reason = add_simplified_clause (ps, 1);
1891 #ifdef NO_BINARY_CLAUSES
1892       if (reason->size == 2)
1893         {
1894           assert (reason == &ps->impl);
1895           reason = impl2reason (ps, lit);
1896         }
1897 #endif
1898       assign_reason (ps, v, reason);
1899     }
1900   else
1901     {
1902       ps->ahead = ps->added;
1903       ps->rhead = ps->resolved;
1904     }
1905
1906   return reason;
1907 }
1908
1909 static void
1910 fixvar (PS * ps, Var * v)
1911 {
1912   Rnk * r;
1913
1914   assert (VAR2LIT (v) != UNDEF);
1915   assert (!v->level);
1916
1917   ps->fixed++;
1918
1919   r = VAR2RNK (v);
1920   r->score = INFFLT;
1921
1922 #ifndef NFL
1923   if (ps->simplifying)
1924     return;
1925 #endif
1926
1927   if (!r->pos)
1928     return;
1929
1930   hup (ps, r);
1931 }
1932
1933 static void
1934 use_var (PS * ps, Var * v)
1935 {
1936   if (v->used)
1937     return;
1938
1939   v->used = 1;
1940   ps->vused++;
1941 }
1942
1943 static void
1944 assign_forced (PS * ps, Lit * lit, Cls * reason)
1945 {
1946   Var *v;
1947
1948   assert (reason);
1949   assert (lit->val == UNDEF);
1950
1951 #ifdef STATS
1952   ps->FORCED++;
1953 #endif
1954   assign (ps, lit, reason);
1955
1956 #ifdef NO_BINARY_CLAUSES
1957   assert (reason != &ps->impl);
1958   if (ISLITREASON (reason))
1959     {
1960       reason = setimpl (ps, lit, NOTLIT (REASON2LIT (reason)));
1961       assert (reason);
1962     }
1963 #endif
1964   LOG ( fprintf (ps->out,
1965                 "%sassign %d at level %d by ",
1966                 ps->prefix, LIT2INT (lit), ps->LEVEL);
1967        dumpclsnl (ps, reason));
1968
1969   v = LIT2VAR (lit);
1970   if (!ps->LEVEL)
1971     use_var (ps, v);
1972
1973   if (!ps->LEVEL && reason->size > 1)
1974     {
1975       reason = resolve_top_level_unit (ps, lit, reason);
1976       assert (reason);
1977     }
1978
1979 #ifdef NO_BINARY_CLAUSES
1980   if (ISLITREASON (reason) || reason == &ps->impl)
1981     {
1982       /* DO NOTHING */
1983     }
1984   else
1985 #endif
1986     {
1987       assert (!reason->locked);
1988       reason->locked = 1;
1989       if (reason->learned && reason->size > 2)
1990         ps->llocked++;
1991     }
1992
1993 #ifdef NO_BINARY_CLAUSES
1994   if (reason == &ps->impl)
1995     resetimpl (ps);
1996 #endif
1997
1998   if (!ps->LEVEL)
1999     fixvar (ps, v);
2000 }
2001
2002 #ifdef NO_BINARY_CLAUSES
2003
2004 static void
2005 lpush (PS * ps, Lit * lit, Cls * c)
2006 {
2007   int pos = (c->lits[0] == lit);
2008   Ltk * s = LIT2IMPLS (lit);
2009   unsigned oldsize, newsize;
2010
2011   assert (c->size == 2);
2012
2013   if (!s->start)
2014     {
2015       assert (!s->count);
2016       assert (!s->ldsize);
2017       NEWN (s->start, 1);
2018     }
2019   else
2020     {
2021       oldsize = (1 << (s->ldsize));
2022       assert (s->count <= oldsize);
2023       if (s->count == oldsize)
2024         {
2025           newsize = 2 * oldsize;
2026           RESIZEN (s->start, oldsize, newsize);
2027           s->ldsize++;
2028         }
2029     }
2030
2031   s->start[s->count++] = c->lits[pos];
2032 }
2033
2034 #endif
2035
2036 static void
2037 connect_head_tail (PS * ps, Lit * lit, Cls * c)
2038 {
2039   Cls ** s;
2040   assert (c->size >= 1);
2041   if (c->size == 2)
2042     {
2043 #ifdef NO_BINARY_CLAUSES
2044       lpush (ps, lit, c);
2045       return;
2046 #else
2047       s = LIT2IMPLS (lit);
2048 #endif
2049     }
2050   else
2051     s = LIT2HTPS (lit);
2052
2053   if (c->lits[0] != lit)
2054     {
2055       assert (c->size >= 2);
2056       assert (c->lits[1] == lit);
2057       c->next[1] = *s;
2058     }
2059   else
2060     c->next[0] = *s;
2061
2062   *s = c;
2063 }
2064
2065 #ifdef TRACE
2066 static void
2067 zpush (PS * ps, Zhn * zhain)
2068 {
2069   assert (ps->trace);
2070
2071   if (ps->zhead == ps->eoz)
2072     ENLARGE (ps->zhains, ps->zhead, ps->eoz);
2073
2074   *ps->zhead++ = zhain;
2075 }
2076
2077 static int
2078 cmp_resolved (PS * ps, Cls * c, Cls * d)
2079 {
2080 #ifndef NDEBUG
2081   assert (ps->trace);
2082 #else
2083   (void) ps;
2084 #endif
2085   return CLS2IDX (c) - CLS2IDX (d);
2086 }
2087
2088 static void
2089 bpushc (PS * ps, unsigned char ch)
2090 {
2091   if (ps->bhead == ps->eob)
2092     ENLARGE (ps->buffer, ps->bhead, ps->eob);
2093
2094   *ps->bhead++ = ch;
2095 }
2096
2097 static void
2098 bpushu (PS * ps, unsigned u)
2099 {
2100   while (u & ~0x7f)
2101     {
2102       bpushc (ps, u | 0x80);
2103       u >>= 7;
2104     }
2105
2106   bpushc (ps, u);
2107 }
2108
2109 static void
2110 bpushd (PS * ps, unsigned prev, unsigned this)
2111 {
2112   unsigned delta;
2113   assert (prev < this);
2114   delta = this - prev;
2115   bpushu (ps, delta);
2116 }
2117
2118 static void
2119 add_zhain (PS * ps)
2120 {
2121   unsigned prev, this, count, rcount;
2122   Cls **p, *c;
2123   Zhn *res;
2124
2125   assert (ps->trace);
2126   assert (ps->bhead == ps->buffer);
2127   assert (ps->rhead > ps->resolved);
2128
2129   rcount = ps->rhead - ps->resolved;
2130   SORT (Cls *, cmp_resolved, ps->resolved, rcount);
2131
2132   prev = 0;
2133   for (p = ps->resolved; p < ps->rhead; p++)
2134     {
2135       c = *p;
2136       this = CLS2TRD (c)->idx;
2137       bpushd (ps, prev, this);
2138       prev = this;
2139     }
2140   bpushc (ps, 0);
2141
2142   count = ps->bhead - ps->buffer;
2143
2144   res = new (ps, sizeof (Zhn) + count);
2145   res->core = 0;
2146   res->ref = 0;
2147   memcpy (res->znt, ps->buffer, count);
2148
2149   ps->bhead = ps->buffer;
2150 #ifdef STATS
2151   ps->znts += count - 1;
2152 #endif
2153   zpush (ps, res);
2154 }
2155
2156 #endif
2157
2158 static void
2159 add_resolved (PS * ps, int learned)
2160 {
2161 #if defined(STATS) || defined(TRACE)
2162   Cls **p, *c;
2163
2164   for (p = ps->resolved; p < ps->rhead; p++)
2165     {
2166       c = *p;
2167       if (c->used)
2168         continue;
2169
2170       c->used = 1;
2171
2172       if (c->size <= 2)
2173         continue;
2174
2175 #ifdef STATS
2176       if (c->learned)
2177         ps->llused++;
2178       else
2179         ps->loused++;
2180 #endif
2181     }
2182 #endif
2183
2184 #ifdef TRACE
2185   if (learned && ps->trace)
2186     add_zhain (ps);
2187 #else
2188   (void) learned;
2189 #endif
2190   ps->rhead = ps->resolved;
2191 }
2192
2193 static void
2194 incjwh (PS * ps, Cls * c)
2195 {
2196   Lit **p, *lit, ** eol;
2197   Flt * f, inc, sum;
2198   unsigned size = 0;
2199   Var * v;
2200   Val val;
2201
2202   eol = end_of_lits (c);
2203
2204   for (p = c->lits; p < eol; p++)
2205     {
2206       lit = *p;
2207       val = lit->val;
2208
2209       if (val && ps->LEVEL > 0)
2210         {
2211           v = LIT2VAR (lit);
2212           if (v->level > 0)
2213             val = UNDEF;
2214         }
2215
2216       if (val == TRUE)
2217         return;
2218
2219       if (val != FALSE)
2220         size++;
2221     }
2222
2223   inc = base2flt (1, -size);
2224
2225   for (p = c->lits; p < eol; p++)
2226     {
2227       lit = *p;
2228       f = LIT2JWH (lit);
2229       sum = addflt (*f, inc);
2230       *f = sum;
2231     }
2232 }
2233
2234 static void
2235 write_rup_header (PS * ps, FILE * file)
2236 {
2237   char line[80];
2238   int i;
2239
2240   sprintf (line, "%%RUPD32 %u %u", ps->rupvariables, ps->rupclauses);
2241
2242   fputs (line, file);
2243   for (i = 255 - strlen (line); i >= 0; i--)
2244     fputc (' ', file);
2245
2246   fputc ('\n', file);
2247   fflush (file);
2248 }
2249
2250 static Cls *
2251 add_simplified_clause (PS * ps, int learned)
2252 {
2253   unsigned num_true, num_undef, num_false, size, count_resolved;
2254   Lit **p, **q, *lit, ** end;
2255   unsigned litlevel, glue;
2256   Cls *res, * reason;
2257   int reentered;
2258   Val val;
2259   Var *v;
2260 #if !defined(NDEBUG) && defined(TRACE)
2261   unsigned idx;
2262 #endif
2263
2264   reentered = 0;
2265
2266 REENTER:
2267
2268   size = ps->ahead - ps->added;
2269
2270   add_resolved (ps, learned);
2271
2272   if (learned)
2273     {
2274       ps->ladded++;
2275       ps->llitsadded += size;
2276       if (size > 2)
2277         {
2278           ps->lladded++;
2279           ps->nlclauses++;
2280           ps->llits += size;
2281         }
2282     }
2283   else
2284     {
2285       ps->oadded++;
2286       if (size > 2)
2287         {
2288           ps->loadded++;
2289           ps->noclauses++;
2290           ps->olits += size;
2291         }
2292     }
2293
2294   ps->addedclauses++;
2295   assert (ps->addedclauses == ps->ladded + ps->oadded);
2296
2297 #ifdef NO_BINARY_CLAUSES
2298   if (size == 2)
2299     res = setimpl (ps, ps->added[0], ps->added[1]);
2300   else
2301 #endif
2302     {
2303       sortlits (ps, ps->added, size);
2304
2305       if (learned)
2306         {
2307           if (ps->lhead == ps->EOL)
2308             {
2309               ENLARGE (ps->lclauses, ps->lhead, ps->EOL);
2310
2311               /* A very difficult to find bug, which only occurs if the
2312                * learned clauses stack is immediately allocated before the
2313                * original clauses stack without padding.  In this case, we
2314                * have 'SOC == EOC', which terminates all loops using the
2315                * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately.
2316                * Unfortunately this occurred in 'fix_clause_lits' after
2317                * using a recent version of the memory allocator of 'Google'
2318                * perftools in the context of one large benchmark for
2319                * our SMT solver 'Boolector'.
2320                */
2321               if (ps->EOL == ps->oclauses)
2322                 ENLARGE (ps->lclauses, ps->lhead, ps->EOL);
2323             }
2324
2325 #if !defined(NDEBUG) && defined(TRACE)
2326           idx = LIDX2IDX (ps->lhead - ps->lclauses);
2327 #endif
2328         }
2329       else
2330         {
2331           if (ps->ohead == ps->eoo)
2332             {
2333               ENLARGE (ps->oclauses, ps->ohead, ps->eoo);
2334               if (ps->EOL == ps->oclauses)
2335                 ENLARGE (ps->oclauses, ps->ohead, ps->eoo);     /* ditto */
2336             }
2337
2338 #if !defined(NDEBUG) && defined(TRACE)
2339           idx = OIDX2IDX (ps->ohead - ps->oclauses);
2340 #endif
2341         }
2342
2343       assert (ps->EOL != ps->oclauses);                 /* ditto */
2344
2345       res = new_clause (ps, size, learned);
2346
2347       glue = 0;
2348
2349       if (learned)
2350         {
2351           assert (ps->dusedhead == ps->dused);
2352
2353           for (p = ps->added; p < ps->ahead; p++)
2354             {
2355               lit = *p;
2356               if (lit->val)
2357                 {
2358                   litlevel = LIT2VAR (lit)->level;
2359                   assert (litlevel <= ps->LEVEL);
2360                   while (ps->levels + litlevel >= ps->levelshead)
2361                     {
2362                       if (ps->levelshead >= ps->eolevels)
2363                         ENLARGE (ps->levels, ps->levelshead, ps->eolevels);
2364                       assert (ps->levelshead < ps->eolevels);
2365                       *ps->levelshead++ = 0;
2366                     }
2367                   if (!ps->levels[litlevel])
2368                     {
2369                       if (ps->dusedhead >= ps->eodused)
2370                         ENLARGE (ps->dused, ps->dusedhead, ps->eodused);
2371                       assert (ps->dusedhead < ps->eodused);
2372                       *ps->dusedhead++ = litlevel;
2373                       ps->levels[litlevel] = 1;
2374                       glue++;
2375                     }
2376                 }
2377               else
2378                 glue++;
2379             }
2380
2381           while (ps->dusedhead > ps->dused)
2382             {
2383               litlevel = *--ps->dusedhead;
2384               assert (ps->levels + litlevel < ps->levelshead);
2385               assert (ps->levels[litlevel]);
2386               ps->levels[litlevel] = 0;
2387             }
2388         }
2389
2390       assert (glue <= MAXGLUE);
2391       res->glue = glue;
2392
2393 #if !defined(NDEBUG) && defined(TRACE)
2394       if (ps->trace)
2395         assert (CLS2IDX (res) == idx);
2396 #endif
2397       if (learned)
2398         *ps->lhead++ = res;
2399       else
2400         *ps->ohead++ = res;
2401
2402 #if !defined(NDEBUG) && defined(TRACE)
2403       if (ps->trace && learned)
2404         assert (ps->zhead - ps->zhains == ps->lhead - ps->lclauses);
2405 #endif
2406       assert (ps->lhead != ps->oclauses);               /* ditto */
2407     }
2408
2409   if (learned && ps->rup)
2410     {
2411       if (!ps->rupstarted)
2412         {
2413           write_rup_header (ps, ps->rup);
2414           ps->rupstarted = 1;
2415         }
2416     }
2417
2418   num_true = num_undef = num_false = 0;
2419
2420   q = res->lits;
2421   for (p = ps->added; p < ps->ahead; p++)
2422     {
2423       lit = *p;
2424       *q++ = lit;
2425
2426       if (learned && ps->rup)
2427         fprintf (ps->rup, "%d ", LIT2INT (lit));
2428
2429       val = lit->val;
2430
2431       num_true += (val == TRUE);
2432       num_undef += (val == UNDEF);
2433       num_false += (val == FALSE);
2434     }
2435   assert (num_false + num_true + num_undef == size);
2436
2437   if (learned && ps->rup)
2438     fputs ("0\n", ps->rup);
2439
2440   ps->ahead = ps->added;                /* reset */
2441
2442   if (!reentered)                               // TODO merge
2443   if (size > 0)
2444     {
2445       assert (size <= 2 || !reentered);         // TODO remove
2446       connect_head_tail (ps, res->lits[0], res);
2447       if (size > 1)
2448         connect_head_tail (ps, res->lits[1], res);
2449     }
2450
2451   if (size == 0)
2452     {
2453       if (!ps->mtcls)
2454         ps->mtcls = res;
2455     }
2456
2457 #ifdef NO_BINARY_CLAUSES
2458   if (size != 2)
2459 #endif
2460 #ifndef NDEBUG
2461     res->connected = 1;
2462 #endif
2463
2464   LOG ( fprintf (ps->out, "%s%s ", ps->prefix, learned ? "learned" : "original");
2465         dumpclsnl (ps, res));
2466
2467   /* Shrink clause by resolving it against top level assignments.
2468    */
2469   if (!ps->LEVEL && num_false > 0)
2470     {
2471       assert (ps->ahead == ps->added);
2472       assert (ps->rhead == ps->resolved);
2473
2474       count_resolved = 1;
2475       add_antecedent (ps, res);
2476
2477       end = end_of_lits (res);
2478       for (p = res->lits; p < end; p++)
2479         {
2480           lit = *p;
2481           v = LIT2VAR (lit);
2482           use_var (ps, v);
2483
2484           if (lit->val == FALSE)
2485             {
2486               add_antecedent (ps, v->reason);
2487               count_resolved++;
2488             }
2489           else
2490             add_lit (ps, lit);
2491         }
2492
2493       assert (count_resolved >= 2);
2494
2495       learned = 1;
2496 #ifdef NO_BINARY_CLAUSES
2497       if (res == &ps->impl)
2498         resetimpl (ps);
2499 #endif
2500       reentered = 1;
2501       goto REENTER;             /* and return simplified clause */
2502     }
2503
2504   if (!num_true && num_undef == 1)      /* unit clause */
2505     {
2506       lit = 0;
2507       for (p = res->lits; p < res->lits + size; p++)
2508         {
2509           if ((*p)->val == UNDEF)
2510             lit = *p;
2511
2512           v = LIT2VAR (*p);
2513           use_var (ps, v);
2514         }
2515       assert (lit);
2516
2517       reason = res;
2518 #ifdef NO_BINARY_CLAUSES
2519       if (size == 2)
2520         {
2521           Lit * other = res->lits[0];
2522           if (other == lit)
2523             other = res->lits[1];
2524
2525           assert (other->val == FALSE);
2526           reason = LIT2REASON (NOTLIT (other));
2527         }
2528 #endif
2529       assign_forced (ps, lit, reason);
2530       num_true++;
2531     }
2532
2533   if (num_false == size && !ps->conflict)
2534     {
2535 #ifdef NO_BINARY_CLAUSES
2536       if (res == &ps->impl)
2537         ps->conflict = setcimpl (ps, res->lits[0], res->lits[1]);
2538       else
2539 #endif
2540       ps->conflict = res;
2541     }
2542
2543   if (!learned && !num_true && num_undef)
2544     incjwh (ps, res);
2545
2546 #ifdef NO_BINARY_CLAUSES
2547   if (res == &ps->impl)
2548     resetimpl (ps);
2549 #endif
2550   return res;
2551 }
2552
2553 static int
2554 trivial_clause (PS * ps)
2555 {
2556   Lit **p, **q, *prev;
2557   Var *v;
2558
2559   SORT (Lit *, cmp_ptr, ps->added,  ps->ahead - ps->added);
2560
2561   prev = 0;
2562   q = ps->added;
2563   for (p = q; p < ps->ahead; p++)
2564     {
2565       Lit *this = *p;
2566
2567       v = LIT2VAR (this);
2568
2569       if (prev == this)         /* skip repeated literals */
2570         continue;
2571
2572       /* Top level satisfied ?
2573        */
2574       if (this->val == TRUE && !v->level)
2575          return 1;
2576
2577       if (prev == NOTLIT (this))/* found pair of dual literals */
2578         return 1;
2579
2580       *q++ = prev = this;
2581     }
2582
2583   ps->ahead = q;                        /* shrink */
2584
2585   return 0;
2586 }
2587
2588 static void
2589 simplify_and_add_original_clause (PS * ps)
2590 {
2591 #ifdef NO_BINARY_CLAUSES
2592   Cls * c;
2593 #endif
2594   if (trivial_clause (ps))
2595     {
2596       ps->ahead = ps->added;
2597
2598       if (ps->ohead == ps->eoo)
2599         ENLARGE (ps->oclauses, ps->ohead, ps->eoo);
2600
2601       *ps->ohead++ = 0;
2602
2603       ps->addedclauses++;
2604       ps->oadded++;
2605     }
2606   else
2607     {
2608       if (ps->CLS != ps->clshead)
2609         add_lit (ps, NOTLIT (ps->clshead[-1]));
2610
2611 #ifdef NO_BINARY_CLAUSES
2612       c =
2613 #endif
2614       add_simplified_clause (ps, 0);
2615 #ifdef NO_BINARY_CLAUSES
2616       if (c == &ps->impl) assert (!ps->implvalid);
2617 #endif
2618     }
2619 }
2620
2621 #ifndef NADC
2622
2623 static void
2624 add_ado (PS * ps)
2625 {
2626   unsigned len = ps->ahead - ps->added;
2627   Lit ** ado, ** p, ** q, *lit;
2628   Var * v, * u;
2629
2630 #ifdef TRACE
2631   assert (!ps->trace);
2632 #endif
2633
2634   ABORTIF (ps->ados < ps->hados && llength (ps->ados[0]) != len,
2635            "internal: non matching all different constraint object lengths");
2636
2637   if (ps->hados == ps->eados)
2638     ENLARGE (ps->ados, ps->hados, ps->eados);
2639
2640   NEWN (ado, len + 1);
2641   *hados++ = ado;
2642
2643   p = ps->added;
2644   q = ado;
2645   u = 0;
2646   while (p < ps->ahead)
2647     {
2648       lit = *p++;
2649       v = LIT2VAR (lit);
2650       ABORTIF (v->inado,
2651                "internal: variable in multiple all different objects");
2652       v->inado = ado;
2653       if (!u && !lit->val)
2654         u = v;
2655       *q++ = lit;
2656     }
2657
2658   assert (q == ado + len);
2659   *q++ = 0;
2660
2661   /* TODO simply do a conflict test as in propado */
2662
2663   ABORTIF (!u,
2664     "internal: "
2665     "adding fully instantiated all different object not implemented yet");
2666
2667   assert (u);
2668   assert (u->inado == ado);
2669   assert (!u->ado);
2670   u->ado = ado;
2671
2672   ps->ahead = ps->added;
2673 }
2674
2675 #endif
2676
2677 static void
2678 hdown (PS * ps, Rnk * r)
2679 {
2680   unsigned end, rpos, cpos, opos;
2681   Rnk *child, *other;
2682
2683   assert (r->pos > 0);
2684   assert (ps->heap[r->pos] == r);
2685
2686   end = ps->hhead - ps->heap;
2687   rpos = r->pos;
2688
2689   for (;;)
2690     {
2691       cpos = 2 * rpos;
2692       if (cpos >= end)
2693         break;
2694
2695       opos = cpos + 1;
2696       child = ps->heap[cpos];
2697
2698       if (cmp_rnk (r, child) < 0)
2699         {
2700           if (opos < end)
2701             {
2702               other = ps->heap[opos];
2703
2704               if (cmp_rnk (child, other) < 0)
2705                 {
2706                   child = other;
2707                   cpos = opos;
2708                 }
2709             }
2710         }
2711       else if (opos < end)
2712         {
2713           child = ps->heap[opos];
2714
2715           if (cmp_rnk (r, child) >= 0)
2716             break;
2717
2718           cpos = opos;
2719         }
2720       else
2721         break;
2722
2723       ps->heap[rpos] = child;
2724       child->pos = rpos;
2725       rpos = cpos;
2726     }
2727
2728   r->pos = rpos;
2729   ps->heap[rpos] = r;
2730 }
2731
2732 static Rnk *
2733 htop (PS * ps)
2734 {
2735   assert (ps->hhead > ps->heap + 1);
2736   return ps->heap[1];
2737 }
2738
2739 static Rnk *
2740 hpop (PS * ps)
2741 {
2742   Rnk *res, *last;
2743   unsigned end;
2744
2745   assert (ps->hhead > ps->heap + 1);
2746
2747   res = ps->heap[1];
2748   res->pos = 0;
2749
2750   end = --ps->hhead - ps->heap;
2751   if (end == 1)
2752     return res;
2753
2754   last = ps->heap[end];
2755
2756   ps->heap[last->pos = 1] = last;
2757   hdown (ps, last);
2758
2759   return res;
2760 }
2761
2762 inline static void
2763 hpush (PS * ps, Rnk * r)
2764 {
2765   assert (!r->pos);
2766
2767   if (ps->hhead == ps->eoh)
2768     ENLARGE (ps->heap, ps->hhead, ps->eoh);
2769
2770   r->pos = ps->hhead++ - ps->heap;
2771   ps->heap[r->pos] = r;
2772   hup (ps, r);
2773 }
2774
2775 static void
2776 fix_trail_lits (PS * ps, long delta)
2777 {
2778   Lit **p;
2779   for (p = ps->trail; p < ps->thead; p++)
2780     *p += delta;
2781 }
2782
2783 #ifdef NO_BINARY_CLAUSES
2784 static void
2785 fix_impl_lits (PS * ps, long delta)
2786 {
2787   Ltk * s;
2788   Lit ** p;
2789
2790   for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++)
2791     for (p = s->start; p < s->start + s->count; p++)
2792       *p += delta;
2793 }
2794 #endif
2795
2796 static void
2797 fix_clause_lits (PS * ps, long delta)
2798 {
2799   Cls **p, *clause;
2800   Lit **q, *lit, **eol;
2801
2802   for (p = SOC; p != EOC; p = NXC (p))
2803     {
2804       clause = *p;
2805       if (!clause)
2806         continue;
2807
2808       q = clause->lits;
2809       eol = end_of_lits (clause);
2810       while (q < eol)
2811         {
2812           assert (q - clause->lits <= (int) clause->size);
2813           lit = *q;
2814           lit += delta;
2815           *q++ = lit;
2816         }
2817     }
2818 }
2819
2820 static void
2821 fix_added_lits (PS * ps, long delta)
2822 {
2823   Lit **p;
2824   for (p = ps->added; p < ps->ahead; p++)
2825     *p += delta;
2826 }
2827
2828 static void
2829 fix_assumed_lits (PS * ps, long delta)
2830 {
2831   Lit **p;
2832   for (p = ps->als; p < ps->alshead; p++)
2833     *p += delta;
2834 }
2835
2836 static void
2837 fix_cls_lits (PS * ps, long delta)
2838 {
2839   Lit **p;
2840   for (p = ps->CLS; p < ps->clshead; p++)
2841     *p += delta;
2842 }
2843
2844 static void
2845 fix_heap_rnks (PS * ps, long delta)
2846 {
2847   Rnk **p;
2848
2849   for (p = ps->heap + 1; p < ps->hhead; p++)
2850     *p += delta;
2851 }
2852
2853 #ifndef NADC
2854
2855 static void
2856 fix_ado (long delta, Lit ** ado)
2857 {
2858   Lit ** p;
2859   for (p = ado; *p; p++)
2860     *p += delta;
2861 }
2862
2863 static void
2864 fix_ados (PS * ps, long delta)
2865 {
2866   Lit *** p;
2867
2868   for (p = ps->ados; p < ps->hados; p++)
2869     fix_ado (delta, *p);
2870 }
2871
2872 #endif
2873
2874 static void
2875 enlarge (PS * ps, unsigned new_size_vars)
2876 {
2877   long rnks_delta, lits_delta;
2878   Lit *old_lits = ps->lits;
2879   Rnk *old_rnks = ps->rnks;
2880
2881   RESIZEN (ps->lits, 2 * ps->size_vars, 2 * new_size_vars);
2882   RESIZEN (ps->jwh, 2 * ps->size_vars, 2 * new_size_vars);
2883   RESIZEN (ps->htps, 2 * ps->size_vars, 2 * new_size_vars);
2884 #ifndef NDSC
2885   RESIZEN (ps->dhtps, 2 * ps->size_vars, 2 * new_size_vars);
2886 #endif
2887   RESIZEN (ps->impls, 2 * ps->size_vars, 2 * new_size_vars);
2888   RESIZEN (ps->vars, ps->size_vars, new_size_vars);
2889   RESIZEN (ps->rnks, ps->size_vars, new_size_vars);
2890
2891   if ((lits_delta = ps->lits - old_lits))
2892     {
2893       fix_trail_lits (ps, lits_delta);
2894       fix_clause_lits (ps, lits_delta);
2895       fix_added_lits (ps, lits_delta);
2896       fix_assumed_lits (ps, lits_delta);
2897       fix_cls_lits (ps, lits_delta);
2898 #ifdef NO_BINARY_CLAUSES
2899       fix_impl_lits (ps, lits_delta);
2900 #endif
2901 #ifndef NADC
2902       fix_ados (ps, lits_delta);
2903 #endif
2904     }
2905
2906   if ((rnks_delta = ps->rnks - old_rnks))
2907     {
2908       fix_heap_rnks (ps, rnks_delta);
2909     }
2910
2911   assert (ps->mhead == ps->marked);
2912
2913   ps->size_vars = new_size_vars;
2914 }
2915
2916 static void
2917 unassign (PS * ps, Lit * lit)
2918 {
2919   Cls *reason;
2920   Var *v;
2921   Rnk *r;
2922
2923   assert (lit->val == TRUE);
2924
2925   LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit)));
2926
2927   v = LIT2VAR (lit);
2928   reason = v->reason;
2929
2930 #ifdef NO_BINARY_CLAUSES
2931   assert (reason != &ps->impl);
2932   if (ISLITREASON (reason))
2933     {
2934       /* DO NOTHING */
2935     }
2936   else
2937 #endif
2938   if (reason)
2939     {
2940       assert (reason->locked);
2941       reason->locked = 0;
2942       if (reason->learned && reason->size > 2)
2943         {
2944           assert (ps->llocked > 0);
2945           ps->llocked--;
2946         }
2947     }
2948
2949   lit->val = UNDEF;
2950   NOTLIT (lit)->val = UNDEF;
2951
2952   r = VAR2RNK (v);
2953   if (!r->pos)
2954     hpush (ps, r);
2955
2956 #ifndef NDSC
2957   {
2958     Cls * p, * next, ** q;
2959
2960     q = LIT2DHTPS (lit);
2961     p = *q;
2962     *q = 0;
2963
2964     while (p)
2965       {
2966         Lit * other = p->lits[0];
2967
2968         if (other == lit)
2969           {
2970             other = p->lits[1];
2971             q = p->next + 1;
2972           }
2973         else
2974           {
2975             assert (p->lits[1] == lit);
2976             q = p->next;
2977           }
2978
2979         next = *q;
2980         *q = *LIT2HTPS (other);
2981         *LIT2HTPS (other) = p;
2982         p = next;
2983       }
2984   }
2985 #endif
2986
2987 #ifndef NADC
2988   if (v->adotabpos)
2989     {
2990       assert (ps->nadotab);
2991       assert (*v->adotabpos == v->ado);
2992
2993       *v->adotabpos = 0;
2994       v->adotabpos = 0;
2995
2996       ps->nadotab--;
2997     }
2998 #endif
2999 }
3000
3001 static Cls *
3002 var2reason (PS * ps, Var * var)
3003 {
3004   Cls * res = var->reason;
3005 #ifdef NO_BINARY_CLAUSES
3006   Lit * this, * other;
3007   if (ISLITREASON (res))
3008     {
3009       this = VAR2LIT (var);
3010       if (this->val == FALSE)
3011         this = NOTLIT (this);
3012
3013       other = REASON2LIT (res);
3014       assert (other->val == TRUE);
3015       assert (this->val == TRUE);
3016       res = setimpl (ps, NOTLIT (other), this);
3017     }
3018 #else
3019   (void) ps;
3020 #endif
3021   return res;
3022 }
3023
3024 static void
3025 mark_clause_to_be_collected (Cls * c)
3026 {
3027   assert (!c->collect);
3028   c->collect = 1;
3029 }
3030
3031 static void
3032 undo (PS * ps, unsigned new_level)
3033 {
3034   Lit *lit;
3035   Var *v;
3036
3037   while (ps->thead > ps->trail)
3038     {
3039       lit = *--ps->thead;
3040       v = LIT2VAR (lit);
3041       if (v->level == new_level)
3042         {
3043           ps->thead++;          /* fix pre decrement */
3044           break;
3045         }
3046
3047       unassign (ps, lit);
3048     }
3049
3050   ps->LEVEL = new_level;
3051   ps->ttail = ps->thead;
3052   ps->ttail2 = ps->thead;
3053 #ifndef NADC
3054   ps->ttailado = ps->thead;
3055 #endif
3056
3057 #ifdef NO_BINARY_CLAUSES
3058   if (ps->conflict == &ps->cimpl)
3059     resetcimpl (ps);
3060 #endif
3061 #ifndef NADC
3062   if (ps->conflict && ps->conflict == ps->adoconflict)
3063     resetadoconflict (ps);
3064 #endif
3065   ps->conflict = ps->mtcls;
3066   if (ps->LEVEL < ps->adecidelevel)
3067     {
3068       assert (ps->als < ps->alshead);
3069       ps->adecidelevel = 0;
3070       ps->alstail = ps->als;
3071     }
3072   LOG ( fprintf (ps->out, "%sback to level %u\n", ps->prefix, ps->LEVEL));
3073 }
3074
3075 #ifndef NDEBUG
3076
3077 static int
3078 clause_satisfied (Cls * c)
3079 {
3080   Lit **p, **eol, *lit;
3081
3082   eol = end_of_lits (c);
3083   for (p = c->lits; p < eol; p++)
3084     {
3085       lit = *p;
3086       if (lit->val == TRUE)
3087         return 1;
3088     }
3089
3090   return 0;
3091 }
3092
3093 static void
3094 original_clauses_satisfied (PS * ps)
3095 {
3096   Cls **p, *c;
3097
3098   for (p = ps->oclauses; p < ps->ohead; p++)
3099     {
3100       c = *p;
3101
3102       if (!c)
3103         continue;
3104
3105       if (c->learned)
3106         continue;
3107
3108       assert (clause_satisfied (c));
3109     }
3110 }
3111
3112 static void
3113 assumptions_satisfied (PS * ps)
3114 {
3115   Lit *lit, ** p;
3116
3117   for (p = ps->als; p < ps->alshead; p++)
3118     {
3119       lit = *p;
3120       assert (lit->val == TRUE);
3121     }
3122 }
3123
3124 #endif
3125
3126 static void
3127 sflush (PS * ps)
3128 {
3129   double now = picosat_time_stamp ();
3130   double delta = now - ps->entered;
3131   delta = (delta < 0) ? 0 : delta;
3132   ps->seconds += delta;
3133   ps->entered = now;
3134 }
3135
3136 static double
3137 mb (PS * ps)
3138 {
3139   return ps->current_bytes / (double) (1 << 20);
3140 }
3141
3142 static double
3143 avglevel (PS * ps)
3144 {
3145   return ps->decisions ? ps->levelsum / ps->decisions : 0.0;
3146 }
3147
3148 static void
3149 rheader (PS * ps)
3150 {
3151   assert (ps->lastrheader <= ps->reports);
3152
3153   if (ps->lastrheader == ps->reports)
3154     return;
3155
3156   ps->lastrheader = ps->reports;
3157
3158    fprintf (ps->out, "%s\n", ps->prefix);
3159    fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]);
3160    fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]);
3161    fprintf (ps->out, "%s\n", ps->prefix);
3162 }
3163
3164 static unsigned
3165 dynamic_flips_per_assignment_per_mille (PS * ps)
3166 {
3167   assert (FFLIPPEDPREC >= 1000);
3168   return ps->sdflips / (FFLIPPEDPREC / 1000);
3169 }
3170
3171 #ifdef NLUBY
3172
3173 static int
3174 high_agility (PS * ps)
3175 {
3176   return dynamic_flips_per_assignment_per_mille (ps) >= 200;
3177 }
3178
3179 static int
3180 very_high_agility (PS * ps)
3181 {
3182   return dynamic_flips_per_assignment_per_mille (ps) >= 250;
3183 }
3184
3185 #else
3186
3187 static int
3188 medium_agility (PS * ps)
3189 {
3190   return dynamic_flips_per_assignment_per_mille (ps) >= 230;
3191 }
3192
3193 #endif
3194
3195 static void
3196 relemdata (PS * ps)
3197 {
3198   char *p;
3199   int x;
3200
3201   if (ps->reports < 0)
3202     {
3203       /* strip trailing white space
3204        */
3205       for (x = 0; x <= 1; x++)
3206         {
3207           p = ps->rline[x] + strlen (ps->rline[x]);
3208           while (p-- > ps->rline[x])
3209             {
3210               if (*p != ' ')
3211                 break;
3212
3213               *p = 0;
3214             }
3215         }
3216
3217       rheader (ps);
3218     }
3219   else
3220     fputc ('\n', ps->out);
3221
3222   ps->RCOUNT = 0;
3223 }
3224
3225 static void
3226 relemhead (PS * ps, const char * name, int fp, double val)
3227 {
3228   int x, y, len, size;
3229   const char *fmt;
3230   unsigned tmp, e;
3231
3232   if (ps->reports < 0)
3233     {
3234       x = ps->RCOUNT & 1;
3235       y = (ps->RCOUNT / 2) * 12 + x * 6;
3236
3237       if (ps->RCOUNT == 1)
3238         sprintf (ps->rline[1], "%6s", "");
3239
3240       len = strlen (name);
3241       while (ps->szrline <= len + y + 1)
3242         {
3243           size = ps->szrline ? 2 * ps->szrline : 128;
3244           ps->rline[0] = resize (ps, ps->rline[0], ps->szrline, size);
3245           ps->rline[1] = resize (ps, ps->rline[1], ps->szrline, size);
3246           ps->szrline = size;
3247         }
3248
3249       fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s";
3250       sprintf (ps->rline[x] + y, fmt, name, "");
3251     }
3252   else if (val < 0)
3253     {
3254       assert (fp);
3255
3256       if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0)
3257         {
3258            fprintf (ps->out, "-%4.1f ", -tmp / 10.0);
3259         }
3260       else
3261         {
3262           tmp = -val / 10.0 + 0.5;
3263           e = 1;
3264           while (tmp >= 100)
3265             {
3266               tmp /= 10;
3267               e++;
3268             }
3269
3270            fprintf (ps->out, "-%2ue%u ", tmp, e);
3271         }
3272     }
3273   else
3274     {
3275       if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000)
3276         {
3277            fprintf (ps->out, "%5.1f ", tmp / 10.0);
3278         }
3279       else if (!fp && (tmp = val) < 100000)
3280         {
3281            fprintf (ps->out, "%5u ", tmp);
3282         }
3283       else
3284         {
3285           tmp = val / 10.0 + 0.5;
3286           e = 1;
3287
3288           while (tmp >= 1000)
3289             {
3290               tmp /= 10;
3291               e++;
3292             }
3293
3294            fprintf (ps->out, "%3ue%u ", tmp, e);
3295         }
3296     }
3297
3298   ps->RCOUNT++;
3299 }
3300
3301 inline static void
3302 relem (PS * ps, const char *name, int fp, double val)
3303 {
3304   if (name)
3305     relemhead (ps, name, fp, val);
3306   else
3307     relemdata (ps);
3308 }
3309
3310 static unsigned
3311 reduce_limit_on_lclauses (PS * ps)
3312 {
3313   unsigned res = ps->lreduce;
3314   res += ps->llocked;
3315   return res;
3316 }
3317
3318 static void
3319 report (PS * ps, int replevel, char type)
3320 {
3321   int rounds;
3322
3323   if (ps->verbosity < replevel)
3324     return;
3325
3326   sflush (ps);
3327
3328   if (!ps->reports)
3329     ps->reports = -1;
3330
3331   for (rounds = (ps->reports < 0) ? 2 : 1; rounds; rounds--)
3332     {
3333       if (ps->reports >= 0)
3334          fprintf (ps->out, "%s%c ", ps->prefix, type);
3335
3336       relem (ps, "seconds", 1, ps->seconds);
3337       relem (ps, "level", 1, avglevel (ps));
3338       assert (ps->fixed <=  ps->max_var);
3339       relem (ps, "variables", 0, ps->max_var - ps->fixed);
3340       relem (ps, "used", 1, PERCENT (ps->vused, ps->max_var));
3341       relem (ps, "original", 0, ps->noclauses);
3342       relem (ps, "conflicts", 0, ps->conflicts);
3343       // relem (ps, "decisions", 0, ps->decisions);
3344       // relem (ps, "conf/dec", 1, PERCENT(ps->conflicts,ps->decisions));
3345       // relem (ps, "limit", 0, reduce_limit_on_lclauses (ps));
3346       relem (ps, "learned", 0, ps->nlclauses);
3347       // relem (ps, "limit", 1, PERCENT (ps->nlclauses, reduce_limit_on_lclauses (ps)));
3348       relem (ps, "limit", 0, ps->lreduce);
3349 #ifdef STATS
3350       relem (ps, "learning", 1, PERCENT (ps->llused, ps->lladded));
3351 #endif
3352       relem (ps, "agility", 1, dynamic_flips_per_assignment_per_mille (ps) / 10.0);
3353       // relem (ps, "original", 0, ps->noclauses);
3354       relem (ps, "MB", 1, mb (ps));
3355       // relem (ps, "lladded", 0, ps->lladded);
3356       // relem (ps, "llused", 0, ps->llused);
3357
3358       relem (ps, 0, 0, 0);
3359
3360       ps->reports++;
3361     }
3362
3363   /* Adapt this to the number of rows in your terminal.
3364    */
3365   #define ROWS 25
3366
3367   if (ps->reports % (ROWS - 3) == (ROWS - 4))
3368     rheader (ps);
3369
3370   fflush (ps->out);
3371 }
3372
3373 static int
3374 bcp_queue_is_empty (PS * ps)
3375 {
3376   if (ps->ttail != ps->thead)
3377     return 0;
3378
3379   if (ps->ttail2 != ps->thead)
3380     return 0;
3381
3382 #ifndef NADC
3383   if (ps->ttailado != ps->thead)
3384     return 0;
3385 #endif
3386
3387   return 1;
3388 }
3389
3390 static int
3391 satisfied (PS * ps)
3392 {
3393   assert (!ps->mtcls);
3394   assert (!ps->failed_assumption);
3395   if (ps->alstail < ps->alshead)
3396     return 0;
3397   assert (!ps->conflict);
3398   assert (bcp_queue_is_empty (ps));
3399   return ps->thead == ps->trail + ps->max_var;  /* all assigned */
3400 }
3401
3402 static void
3403 vrescore (PS * ps)
3404 {
3405   Rnk *p, *eor = ps->rnks + ps->max_var;
3406   for (p = ps->rnks + 1; p <= eor; p++)
3407     if (p->score != INFFLT)
3408       p->score = mulflt (p->score, ps->ilvinc);
3409   ps->vinc = mulflt (ps->vinc, ps->ilvinc);;
3410 #ifdef VISCORES
3411   ps->nvinc = mulflt (ps->nvinc, ps->lscore);;
3412 #endif
3413 }
3414
3415 static void
3416 inc_score (PS * ps, Var * v)
3417 {
3418   Flt score;
3419   Rnk *r;
3420
3421 #ifndef NFL
3422   if (ps->simplifying)
3423     return;
3424 #endif
3425
3426   if (!v->level)
3427     return;
3428
3429   if (v->internal)
3430     return;
3431
3432   r = VAR2RNK (v);
3433   score = r->score;
3434
3435   assert (score != INFFLT);
3436
3437   score = addflt (score, ps->vinc);
3438   assert (score < INFFLT);
3439   r->score = score;
3440   if (r->pos > 0)
3441     hup (ps, r);
3442
3443   if (score > ps->lscore)
3444     vrescore (ps);
3445 }
3446
3447 static void
3448 inc_activity (PS * ps, Cls * c)
3449 {
3450   Act *p;
3451
3452   if (!c->learned)
3453     return;
3454
3455   if (c->size <= 2)
3456     return;
3457
3458   p = CLS2ACT (c);
3459   *p = addflt (*p, ps->cinc);
3460 }
3461
3462 static unsigned
3463 hashlevel (unsigned l)
3464 {
3465   return 1u << (l & 31);
3466 }
3467
3468 static void
3469 push (PS * ps, Var * v)
3470 {
3471   if (ps->dhead == ps->eod)
3472     ENLARGE (ps->dfs, ps->dhead, ps->eod);
3473
3474   *ps->dhead++ = v;
3475 }
3476
3477 static Var *
3478 pop (PS * ps)
3479 {
3480   assert (ps->dfs < ps->dhead);
3481   return *--ps->dhead;
3482 }
3483
3484 static void
3485 analyze (PS * ps)
3486 {
3487   unsigned open, minlevel, siglevels, l, old, i, orig;
3488   Lit *this, *other, **p, **q, **eol;
3489   Var *v, *u, **m, *start, *uip;
3490   Cls *c;
3491
3492   assert (ps->conflict);
3493
3494   assert (ps->ahead == ps->added);
3495   assert (ps->mhead == ps->marked);
3496   assert (ps->rhead == ps->resolved);
3497
3498   /* First, search for First UIP variable and mark all resolved variables.
3499    * At the same time determine the minimum decision level involved.
3500    * Increase activities of resolved variables.
3501    */
3502   q = ps->thead;
3503   open = 0;
3504   minlevel = ps->LEVEL;
3505   siglevels = 0;
3506   uip = 0;
3507
3508   c = ps->conflict;
3509
3510   for (;;)
3511     {
3512       add_antecedent (ps, c);
3513       inc_activity (ps, c);
3514       eol = end_of_lits (c);
3515       for (p = c->lits; p < eol; p++)
3516         {
3517           other = *p;
3518
3519           if (other->val == TRUE)
3520             continue;
3521
3522           assert (other->val == FALSE);
3523
3524           u = LIT2VAR (other);
3525           if (u->mark)
3526             continue;
3527
3528           u->mark = 1;
3529           inc_score (ps, u);
3530           use_var (ps, u);
3531
3532           if (u->level == ps->LEVEL)
3533             {
3534               open++;
3535             }
3536           else
3537             {
3538               push_var_as_marked (ps, u);
3539
3540               if (u->level)
3541                 {
3542                   /* The statistics counter 'nonminimizedllits' sums up the
3543                    * number of literals that would be added if only the
3544                    * 'first UIP' scheme for learned clauses would be used
3545                    * and no clause minimization.
3546                    */
3547                   ps->nonminimizedllits++;
3548
3549                   if (u->level < minlevel)
3550                     minlevel = u->level;
3551
3552                   siglevels |= hashlevel (u->level);
3553                 }
3554               else
3555                 {
3556                   assert (!u->level);
3557                   assert (u->reason);
3558                 }
3559             }
3560         }
3561
3562       do
3563         {
3564           if (q == ps->trail)
3565             {
3566               uip = 0;
3567               goto DONE_FIRST_UIP;
3568             }
3569
3570           this = *--q;
3571           uip = LIT2VAR (this);
3572         }
3573       while (!uip->mark);
3574
3575       uip->mark = 0;
3576
3577       c = var2reason (ps, uip);
3578 #ifdef NO_BINARY_CLAUSES
3579       if (c == &ps->impl)
3580         resetimpl (ps);
3581 #endif
3582      open--;
3583      if ((!open && ps->LEVEL) || !c)
3584         break;
3585
3586      assert (c);
3587     }
3588
3589 DONE_FIRST_UIP:
3590
3591   if (uip)
3592     {
3593       assert (ps->LEVEL);
3594       this = VAR2LIT (uip);
3595       this += (this->val == TRUE);
3596       ps->nonminimizedllits++;
3597       ps->minimizedllits++;
3598       add_lit (ps, this);
3599 #ifdef STATS
3600       if (uip->reason)
3601         ps->uips++;
3602 #endif
3603     }
3604   else
3605     assert (!ps->LEVEL);
3606
3607   /* Second, try to mark more intermediate variables, with the goal to
3608    * minimize the conflict clause.  This is a DFS from already marked
3609    * variables backward through the implication graph.  It tries to reach
3610    * other marked variables.  If the search reaches an unmarked decision
3611    * variable or a variable assigned below the minimum level of variables in
3612    * the first uip learned clause or a level on which no variable has been
3613    * marked, then the variable from which the DFS is started is not
3614    * redundant.  Otherwise the start variable is redundant and will
3615    * eventually be removed from the learned clause in step 4.  We initially
3616    * implemented BFS, but then profiling revelead that this step is a bottle
3617    * neck for certain incremental applications.  After switching to DFS this
3618    * hot spot went away.
3619    */
3620   orig = ps->mhead - ps->marked;
3621   for (i = 0; i < orig; i++)
3622     {
3623       start = ps->marked[i];
3624
3625       assert (start->mark);
3626       assert (start != uip);
3627       assert (start->level < ps->LEVEL);
3628
3629       if (!start->reason)
3630         continue;
3631
3632       old = ps->mhead - ps->marked;
3633       assert (ps->dhead == ps->dfs);
3634       push (ps, start);
3635
3636       while (ps->dhead > ps->dfs)
3637         {
3638           u = pop (ps);
3639           assert (u->mark);
3640
3641           c = var2reason (ps, u);
3642 #ifdef NO_BINARY_CLAUSES
3643           if (c == &ps->impl)
3644             resetimpl (ps);
3645 #endif
3646           if (!c ||
3647               ((l = u->level) &&
3648                (l < minlevel || ((hashlevel (l) & ~siglevels)))))
3649             {
3650               while (ps->mhead > ps->marked + old)      /* reset all marked */
3651                 (*--ps->mhead)->mark = 0;
3652
3653               ps->dhead = ps->dfs;              /* and DFS stack */
3654               break;
3655             }
3656
3657           eol = end_of_lits (c);
3658           for (p = c->lits; p < eol; p++)
3659             {
3660               v = LIT2VAR (*p);
3661               if (v->mark)
3662                 continue;
3663
3664               mark_var (ps, v);
3665               push (ps, v);
3666             }
3667         }
3668     }
3669
3670   for (m = ps->marked; m < ps->mhead; m++)
3671     {
3672       v = *m;
3673
3674       assert (v->mark);
3675       assert (!v->resolved);
3676
3677       use_var (ps, v);
3678
3679       c = var2reason (ps, v);
3680       if (!c)
3681         continue;
3682
3683 #ifdef NO_BINARY_CLAUSES
3684       if (c == &ps->impl)
3685         resetimpl (ps);
3686 #endif
3687       eol = end_of_lits (c);
3688       for (p = c->lits; p < eol; p++)
3689         {
3690           other = *p;
3691
3692           u = LIT2VAR (other);
3693           if (!u->level)
3694             continue;
3695
3696           if (!u->mark)         /* 'MARKTEST' */
3697             break;
3698         }
3699
3700       if (p != eol)
3701         continue;
3702
3703       add_antecedent (ps, c);
3704       v->resolved = 1;
3705     }
3706
3707   for (m = ps->marked; m < ps->mhead; m++)
3708     {
3709       v = *m;
3710
3711       assert (v->mark);
3712       v->mark = 0;
3713
3714       if (v->resolved)
3715         {
3716           v->resolved = 0;
3717           continue;
3718         }
3719
3720       this = VAR2LIT (v);
3721       if (this->val == TRUE)
3722         this++;                 /* actually NOTLIT */
3723
3724       add_lit (ps, this);
3725       ps->minimizedllits++;
3726     }
3727
3728   assert (ps->ahead <= ps->eoa);
3729   assert (ps->rhead <= ps->eor);
3730
3731   ps->mhead = ps->marked;
3732 }
3733
3734 static void
3735 fanalyze (PS * ps)
3736 {
3737   Lit ** eol, ** p, * lit;
3738   Cls * c, * reason;
3739   Var * v, * u;
3740   int next;
3741
3742   double start = picosat_time_stamp ();
3743
3744   assert (ps->failed_assumption);
3745   assert (ps->failed_assumption->val == FALSE);
3746
3747   v = LIT2VAR (ps->failed_assumption);
3748   reason = var2reason (ps, v);
3749   if (!reason) return;
3750 #ifdef NO_BINARY_CLAUSES
3751   if (reason == &ps->impl)
3752     resetimpl (ps);
3753 #endif
3754
3755   eol = end_of_lits (reason);
3756   for (p = reason->lits; p != eol; p++)
3757     {
3758       lit = *p;
3759       u = LIT2VAR (lit);
3760       if (u == v) continue;
3761       if (u->reason) break;
3762     }
3763   if (p == eol) return;
3764
3765   assert (ps->ahead == ps->added);
3766   assert (ps->mhead == ps->marked);
3767   assert (ps->rhead == ps->resolved);
3768
3769   next = 0;
3770   mark_var (ps, v);
3771   add_lit (ps, NOTLIT (ps->failed_assumption));
3772
3773   do
3774     {
3775       v = ps->marked[next++];
3776       use_var (ps, v);
3777       if (v->reason)
3778         {
3779           reason = var2reason (ps, v);
3780 #ifdef NO_BINARY_CLAUSES
3781           if (reason == &ps->impl)
3782             resetimpl (ps);
3783 #endif
3784           add_antecedent (ps, reason);
3785           eol = end_of_lits (reason);
3786           for (p = reason->lits; p != eol; p++)
3787             {
3788               lit = *p;
3789               u = LIT2VAR (lit);
3790               if (u == v) continue;
3791               if (u->mark) continue;
3792               mark_var (ps, u);
3793             }
3794         }
3795       else
3796         {
3797           lit = VAR2LIT (v);
3798           if (lit->val == TRUE) lit = NOTLIT (lit);
3799           add_lit (ps, lit);
3800         }
3801     }
3802   while (ps->marked + next < ps->mhead);
3803
3804   c = add_simplified_clause (ps, 1);
3805   v = LIT2VAR (ps->failed_assumption);
3806   reason = v->reason;
3807 #ifdef NO_BINARY_CLAUSES
3808   if (!ISLITREASON (reason))
3809 #endif
3810     {
3811       assert (reason->locked);
3812       reason->locked = 0;
3813       if (reason->learned && reason->size > 2)
3814         {
3815           assert (ps->llocked > 0);
3816           ps->llocked--;
3817         }
3818     }
3819
3820 #ifdef NO_BINARY_CLAUSES
3821   if (c == &ps->impl)
3822     {
3823       c = impl2reason (ps, NOTLIT (ps->failed_assumption));
3824     }
3825   else
3826 #endif
3827     {
3828       assert (c->learned);
3829       assert (!c->locked);
3830       c->locked = 1;
3831       if (c->size > 2)
3832         {
3833           ps->llocked++;
3834           assert (ps->llocked > 0);
3835         }
3836     }
3837
3838   v->reason = c;
3839
3840   while (ps->mhead > ps->marked)
3841     (*--ps->mhead)->mark = 0;
3842
3843   if (ps->verbosity)
3844      fprintf (ps->out, "%sfanalyze took %.1f seconds\n",
3845              ps->prefix, picosat_time_stamp () - start);
3846 }
3847
3848 /* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in
3849  * which 'this' occurs.
3850  */
3851 inline static void
3852 prop2 (PS * ps, Lit * this)
3853 {
3854 #ifdef NO_BINARY_CLAUSES
3855   Lit ** l, ** start;
3856   Ltk * lstk;
3857 #else
3858   Cls * c, ** p;
3859   Cls * next;
3860 #endif
3861   Lit * other;
3862   Val tmp;
3863
3864   assert (this->val == FALSE);
3865
3866 #ifdef NO_BINARY_CLAUSES
3867   lstk = LIT2IMPLS (this);
3868   start = lstk->start;
3869   l = start + lstk->count;
3870   while (l != start)
3871     {
3872       /* The counter 'visits' is the number of clauses that are
3873        * visited during propagations of assignments.
3874        */
3875       ps->visits++;
3876 #ifdef STATS
3877       ps->bvisits++;
3878 #endif
3879       other = *--l;
3880       tmp = other->val;
3881
3882       if (tmp == TRUE)
3883         {
3884 #ifdef STATS
3885           ps->othertrue++;
3886           ps->othertrue2++;
3887           if (LIT2VAR (other)->level < ps->LEVEL)
3888             ps->othertrue2u++;
3889 #endif
3890           continue;
3891         }
3892
3893       if (tmp != FALSE)
3894         {
3895           assign_forced (ps, other, LIT2REASON (NOTLIT(this)));
3896           continue;
3897         }
3898
3899       if (ps->conflict == &ps->cimpl)
3900         resetcimpl (ps);
3901       ps->conflict = setcimpl (ps, this, other);
3902     }
3903 #else
3904   /* Traverse all binary clauses with 'this'.  Head/Tail pointers for binary
3905    * clauses do not have to be modified here.
3906    */
3907   p = LIT2IMPLS (this);
3908   for (c = *p; c; c = next)
3909     {
3910       ps->visits++;
3911 #ifdef STATS
3912       ps->bvisits++;
3913 #endif
3914       assert (!c->collect);
3915 #ifdef TRACE
3916       assert (!c->collected);
3917 #endif
3918       assert (c->size == 2);
3919
3920       other = c->lits[0];
3921       if (other == this)
3922         {
3923           next = c->next[0];
3924           other = c->lits[1];
3925         }
3926       else
3927         next = c->next[1];
3928
3929       tmp = other->val;
3930
3931       if (tmp == TRUE)
3932         {
3933 #ifdef STATS
3934           ps->othertrue++;
3935           ps->othertrue2++;
3936           if (LIT2VAR (other)->level < ps->LEVEL)
3937             ps->othertrue2u++;
3938 #endif
3939           continue;
3940         }
3941
3942       if (tmp == FALSE)
3943         ps->conflict = c;
3944       else
3945         assign_forced (ps, other, c);   /* unit clause */
3946     }
3947 #endif /* !defined(NO_BINARY_CLAUSES) */
3948 }
3949
3950 #ifndef NDSC
3951 static int
3952 should_disconnect_head_tail (PS * ps, Lit * lit)
3953 {
3954   unsigned litlevel;
3955   Var * v;
3956
3957   assert (lit->val == TRUE);
3958
3959   v = LIT2VAR (lit);
3960   litlevel = v->level;
3961
3962   if (!litlevel)
3963     return 1;
3964
3965 #ifndef NFL
3966   if (ps->simplifying)
3967     return 0;
3968 #endif
3969
3970   return litlevel < ps->LEVEL;
3971 }
3972 #endif
3973
3974 inline static void
3975 propl (PS * ps, Lit * this)
3976 {
3977   Lit **l, *other, *prev, *new_lit, **eol;
3978   Cls *next, **htp_ptr, **new_htp_ptr;
3979   Cls *c;
3980 #ifdef STATS
3981   unsigned size;
3982 #endif
3983
3984   htp_ptr = LIT2HTPS (this);
3985   assert (this->val == FALSE);
3986
3987   /* Traverse all non binary clauses with 'this'.  Head/Tail pointers are
3988    * updated as well.
3989    */
3990   for (c = *htp_ptr; c; c = next)
3991     {
3992       ps->visits++;
3993 #ifdef STATS
3994       size = c->size;
3995       assert (size >= 3);
3996       ps->traversals++; /* other is dereferenced at least */
3997
3998       if (size == 3)
3999         ps->tvisits++;
4000       else if (size >= 4)
4001         {
4002           ps->lvisits++;
4003           ps->ltraversals++;
4004         }
4005 #endif
4006 #ifdef TRACE
4007       assert (!c->collected);
4008 #endif
4009       assert (c->size > 0);
4010
4011       other = c->lits[0];
4012       if (other != this)
4013         {
4014           assert (c->size != 1);
4015           c->lits[0] = this;
4016           c->lits[1] = other;
4017           next = c->next[1];
4018           c->next[1] = c->next[0];
4019           c->next[0] = next;
4020         }
4021       else if (c->size == 1)    /* With assumptions we need to
4022                                  * traverse unit clauses as well.
4023                                  */
4024         {
4025           assert (!ps->conflict);
4026           ps->conflict = c;
4027           break;
4028         }
4029       else
4030         {
4031           assert (other == this && c->size > 1);
4032           other = c->lits[1];
4033           next = c->next[0];
4034         }
4035       assert (other == c->lits[1]);
4036       assert (this == c->lits[0]);
4037       assert (next == c->next[0]);
4038       assert (!c->collect);
4039
4040       if (other->val == TRUE)
4041         {
4042 #ifdef STATS
4043           ps->othertrue++;
4044           ps->othertruel++;
4045 #endif
4046 #ifndef NDSC
4047           if (should_disconnect_head_tail (ps, other))
4048             {
4049               new_htp_ptr = LIT2DHTPS (other);
4050               c->next[0] = *new_htp_ptr;
4051               *new_htp_ptr = c;
4052 #ifdef STATS
4053               ps->othertruelu++;
4054 #endif
4055               *htp_ptr = next;
4056               continue;
4057             }
4058 #endif
4059           htp_ptr = c->next;
4060           continue;
4061         }
4062
4063       l = c->lits + 1;
4064       eol = c->lits + c->size;
4065       prev = this;
4066
4067       while (++l != eol)
4068         {
4069 #ifdef STATS
4070           if (size >= 3)
4071             {
4072               ps->traversals++;
4073               if (size > 3)
4074                 ps->ltraversals++;
4075             }
4076 #endif
4077           new_lit = *l;
4078           *l = prev;
4079           prev = new_lit;
4080           if (new_lit->val != FALSE) break;
4081         }
4082
4083       if (l == eol)
4084         {
4085           while (l > c->lits + 2)
4086             {
4087               new_lit = *--l;
4088               *l = prev;
4089               prev = new_lit;
4090             }
4091           assert (c->lits[0] == this);
4092
4093           assert (other == c->lits[1]);
4094           if (other->val == FALSE)      /* found conflict */
4095             {
4096               assert (!ps->conflict);
4097               ps->conflict = c;
4098               return;
4099             }
4100
4101           assign_forced (ps, other, c);         /* unit clause */
4102           htp_ptr = c->next;
4103         }
4104       else
4105         {
4106           assert (new_lit->val == TRUE || new_lit->val == UNDEF);
4107           c->lits[0] = new_lit;
4108           // *l = this;
4109           new_htp_ptr = LIT2HTPS (new_lit);
4110           c->next[0] = *new_htp_ptr;
4111           *new_htp_ptr = c;
4112           *htp_ptr = next;
4113         }
4114     }
4115 }
4116
4117 #ifndef NADC
4118
4119 static unsigned primes[] = { 996293, 330643, 753947, 500873 };
4120
4121 #define PRIMES ((sizeof primes)/sizeof *primes)
4122
4123 static unsigned
4124 hash_ado (Lit ** ado, unsigned salt)
4125 {
4126   unsigned i, res, tmp;
4127   Lit ** p, * lit;
4128
4129   assert (salt < PRIMES);
4130
4131   i = salt;
4132   res = 0;
4133
4134   for (p = ado; (lit = *p); p++)
4135     {
4136       assert (lit->val);
4137
4138       tmp = res >> 31;
4139       res <<= 1;
4140
4141       if (lit->val > 0)
4142         res |= 1;
4143
4144       assert (i < PRIMES);
4145       res *= primes[i++];
4146       if (i == PRIMES)
4147         i = 0;
4148
4149       res += tmp;
4150     }
4151
4152   return res & (ps->szadotab - 1);
4153 }
4154
4155 static unsigned
4156 cmp_ado (Lit ** a, Lit ** b)
4157 {
4158   Lit ** p, ** q, * l, * k;
4159   int res;
4160
4161   for (p = a, q = b; (l = *p); p++, q++)
4162     {
4163       k = *q;
4164       assert (k);
4165       if ((res = (l->val - k->val)))
4166         return res;
4167     }
4168
4169   assert (!*q);
4170
4171   return 0;
4172 }
4173
4174 static Lit ***
4175 find_ado (Lit ** ado)
4176 {
4177   Lit *** res, ** other;
4178   unsigned pos, delta;
4179
4180   pos = hash_ado (ado, 0);
4181   assert (pos < ps->szadotab);
4182   res = ps->adotab + pos;
4183
4184   other = *res;
4185   if (!other || !cmp_ado (other, ado))
4186     return res;
4187
4188   delta = hash_ado (ado, 1);
4189   if (!(delta & 1))
4190     delta++;
4191
4192   assert (delta & 1);
4193   assert (delta < ps->szadotab);
4194
4195   for (;;)
4196     {
4197       pos += delta;
4198       if (pos >= ps->szadotab)
4199         pos -= ps->szadotab;
4200
4201       assert (pos < ps->szadotab);
4202       res = ps->adotab + pos;
4203       other = *res;
4204       if (!other || !cmp_ado (other, ado))
4205         return res;
4206     }
4207 }
4208
4209 static void
4210 enlarge_adotab (PS * ps)
4211 {
4212   /* TODO make this generic */
4213
4214   ABORTIF (ps->szadotab,
4215            "internal: all different objects table needs larger initial size");
4216   assert (!ps->nadotab);
4217   ps->szadotab = 10000;
4218   NEWN (ps->adotab, ps->szadotab);
4219   CLRN (ps->adotab, ps->szadotab);
4220 }
4221
4222 static int
4223 propado (Var * v)
4224 {
4225   Lit ** p, ** q, *** adotabpos, **ado, * lit;
4226   Var * u;
4227
4228   if (ps->level && ps->adodisabled)
4229     return 1;
4230
4231   assert (!ps->conflict);
4232   assert (!ps->adoconflict);
4233   assert (VAR2LIT (v)->val != UNDEF);
4234   assert (!v->adotabpos);
4235
4236   if (!v->ado)
4237     return 1;
4238
4239   assert (v->inado);
4240
4241   for (p = v->ado; (lit = *p); p++)
4242     if (lit->val == UNDEF)
4243       {
4244         u = LIT2VAR (lit);
4245         assert (!u->ado);
4246         u->ado = v->ado;
4247         v->ado = 0;
4248
4249         return 1;
4250       }
4251
4252   if (4 * ps->nadotab >= 3 * ps->szadotab)      /* at least 75% filled */
4253     enlarge_adotab (ps);
4254
4255   adotabpos = find_ado (v->ado);
4256   ado = *adotabpos;
4257
4258   if (!ado)
4259     {
4260       ps->nadotab++;
4261       v->adotabpos = adotabpos;
4262       *adotabpos = v->ado;
4263       return 1;
4264     }
4265
4266   assert (ado != v->ado);
4267
4268   ps->adoconflict = new_clause (2 * llength (ado), 1);
4269   q = ps->adoconflict->lits;
4270
4271   for (p = ado; (lit = *p); p++)
4272     *q++ = lit->val == FALSE ? lit : NOTLIT (lit);
4273
4274   for (p = v->ado; (lit = *p); p++)
4275     *q++ = lit->val == FALSE ? lit : NOTLIT (lit);
4276
4277   assert (q == ENDOFCLS (ps->adoconflict));
4278   ps->conflict = ps->adoconflict;
4279   ps->adoconflicts++;
4280   return 0;
4281 }
4282
4283 #endif
4284
4285 static void
4286 bcp (PS * ps)
4287 {
4288   int props = 0;
4289   assert (!ps->conflict);
4290
4291   if (ps->mtcls)
4292     return;
4293
4294   for (;;)
4295     {
4296       if (ps->ttail2 < ps->thead)       /* prioritize implications */
4297         {
4298           props++;
4299           prop2 (ps, NOTLIT (*ps->ttail2++));
4300         }
4301       else if (ps->ttail < ps->thead)   /* unit clauses or clauses with length > 2 */
4302         {
4303           if (ps->conflict) break;
4304           propl (ps, NOTLIT (*ps->ttail++));
4305           if (ps->conflict) break;
4306         }
4307 #ifndef NADC
4308       else if (ps->ttailado < ps->thead)
4309         {
4310           if (ps->conflict) break;
4311           propado (ps, LIT2VAR (*ps->ttailado++));
4312           if (ps->conflict) break;
4313         }
4314 #endif
4315       else
4316         break;          /* all assignments propagated, so break */
4317     }
4318
4319   ps->propagations += props;
4320 }
4321
4322 static unsigned
4323 drive (PS * ps)
4324 {
4325   unsigned res, vlevel;
4326   Lit **p;
4327   Var *v;
4328
4329   res = 0;
4330   for (p = ps->added; p < ps->ahead; p++)
4331     {
4332       v = LIT2VAR (*p);
4333       vlevel = v->level;
4334       assert (vlevel <= ps->LEVEL);
4335       if (vlevel < ps->LEVEL && vlevel > res)
4336         res = vlevel;
4337     }
4338
4339   return res;
4340 }
4341
4342 #ifdef VISCORES
4343
4344 static void
4345 viscores (PS * ps)
4346 {
4347   Rnk *p, *eor = ps->rnks + ps->max_var;
4348   char name[100], cmd[200];
4349   FILE * data;
4350   Flt s;
4351   int i;
4352
4353   for (p = ps->rnks + 1; p <= ps->eor; p++)
4354     {
4355       s = p->score;
4356       if (s == INFFLT)
4357         continue;
4358       s = mulflt (s, ps->nvinc);
4359       assert (flt2double (s) <= 1.0);
4360     }
4361
4362   sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts);
4363   sprintf (cmd, "sort -n|nl>%s", name);
4364
4365   data = popen (cmd, "w");
4366   for (p = ps->rnks + 1; p <= ps->eor; p++)
4367     {
4368       s = p->score;
4369       if (s == INFFLT)
4370         continue;
4371       s = mulflt (s, ps->nvinc);
4372       fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnks));
4373     }
4374   fflush (data);
4375   pclose (data);
4376
4377   for (i = 0; i < 8; i++)
4378     {
4379       sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i);
4380       system (cmd);
4381     }
4382
4383   fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts);
4384   fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max_var);
4385
4386   for (i = 0; i < 8; i++)
4387     fprintf (ps->fviscores,
4388              ", \"%s.%d\" using 1:2:3 with labels tc lt %d",
4389              name, i, i + 1);
4390
4391   fputc ('\n', ps->fviscores);
4392   fflush (ps->fviscores);
4393 #ifndef WRITEGIF
4394   usleep (50000);               /* refresh rate of 20 Hz */
4395 #endif
4396 }
4397
4398 #endif
4399
4400 static void
4401 crescore (PS * ps)
4402 {
4403   Cls **p, *c;
4404   Act *a;
4405   Flt factor;
4406   int l = log2flt (ps->cinc);
4407   assert (l > 0);
4408   factor = base2flt (1, -l);
4409
4410   for (p = ps->lclauses; p != ps->lhead; p++)
4411     {
4412       c = *p;
4413
4414       if (!c)
4415         continue;
4416
4417 #ifdef TRACE
4418       if (c->collected)
4419         continue;
4420 #endif
4421       assert (c->learned);
4422
4423       if (c->size <= 2)
4424         continue;
4425
4426       a = CLS2ACT (c);
4427       *a = mulflt (*a, factor);
4428     }
4429
4430   ps->cinc = mulflt (ps->cinc, factor);
4431 }
4432
4433 static void
4434 inc_vinc (PS * ps)
4435 {
4436 #ifdef VISCORES
4437   ps->nvinc = mulflt (ps->nvinc, ps->fvinc);
4438 #endif
4439   ps->vinc = mulflt (ps->vinc, ps->ifvinc);
4440 }
4441
4442 inline static void
4443 inc_max_var (PS * ps)
4444 {
4445   Lit *lit;
4446   Rnk *r;
4447   Var *v;
4448
4449   assert (ps->max_var < ps->size_vars);
4450
4451   if (ps->max_var + 1 == ps->size_vars)
4452     enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */
4453
4454   ps->max_var++;                        /* new index of variable */
4455   assert (ps->max_var);                 /* no unsigned overflow */
4456
4457   assert (ps->max_var < ps->size_vars);
4458
4459   lit = ps->lits + 2 * ps->max_var;
4460   lit[0].val = lit[1].val = UNDEF;
4461
4462   memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps);
4463 #ifndef NDSC
4464   memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps);
4465 #endif
4466   memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls);
4467   memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh);
4468
4469   v = ps->vars + ps->max_var;           /* initialize variable components */
4470   CLR (v);
4471
4472   r = ps->rnks + ps->max_var;           /* initialize rank */
4473   CLR (r);
4474
4475   hpush (ps, r);
4476 }
4477
4478 static void
4479 force (PS * ps, Cls * c)
4480 {
4481   Lit ** p, ** eol, * lit, * forced;
4482   Cls * reason;
4483
4484   forced = 0;
4485   reason = c;
4486
4487   eol = end_of_lits (c);
4488   for (p = c->lits; p < eol; p++)
4489     {
4490       lit = *p;
4491       if (lit->val == UNDEF)
4492         {
4493           assert (!forced);
4494           forced = lit;
4495 #ifdef NO_BINARY_CLAUSES
4496           if (c == &ps->impl)
4497             reason = LIT2REASON (NOTLIT (p[p == c->lits ? 1 : -1]));
4498 #endif
4499         }
4500       else
4501         assert (lit->val == FALSE);
4502     }
4503
4504 #ifdef NO_BINARY_CLAUSES
4505   if (c == &ps->impl)
4506     resetimpl (ps);
4507 #endif
4508   if (!forced)
4509     return;
4510
4511   assign_forced (ps, forced, reason);
4512 }
4513
4514 static void
4515 inc_lreduce (PS * ps)
4516 {
4517 #ifdef STATS
4518   ps->inclreduces++;
4519 #endif
4520   ps->lreduce *= FREDUCE;
4521   ps->lreduce /= 100;
4522   report (ps, 1, '+');
4523 }
4524
4525 static void
4526 backtrack (PS * ps)
4527 {
4528   unsigned new_level;
4529   Cls * c;
4530
4531   ps->conflicts++;
4532   LOG ( fprintf (ps->out, "%sconflict ", ps->prefix); dumpclsnl (ps, ps->conflict));
4533
4534   analyze (ps);
4535   new_level = drive (ps);
4536   // TODO: why not? assert (new_level != 1  || (ps->ahead - ps->added) == 2);
4537   c = add_simplified_clause (ps, 1);
4538   undo (ps, new_level);
4539   force (ps, c);
4540
4541   if (
4542 #ifndef NFL
4543       !ps->simplifying &&
4544 #endif
4545       !--ps->lreduceadjustcnt)
4546     {
4547       /* With FREDUCE==110 and FREDADJ=121 we stir 'lreduce' to be
4548        * proportional to 'sqrt(conflicts)'.  In earlier version we actually
4549        * used  'FREDADJ=150', which results in 'lreduce' to approximate
4550        * 'conflicts^(log(1.1)/log(1.5))' which is close to the fourth root
4551        * of 'conflicts', since log(1.1)/log(1.5)=0.235 (as observed by
4552        * Donald Knuth). The square root is the same we get by a Glucose
4553        * style increase, which simply adds a constant at every reduction.
4554        * This would be way simpler to implement but for now we keep the more
4555        * complicated code using the adjust increments and counters.
4556        */
4557       ps->lreduceadjustinc *= FREDADJ; ps->lreduceadjustinc /= 100; ps->lreduceadjustcnt
4558       = ps->lreduceadjustinc;
4559       inc_lreduce (ps);
4560     }
4561
4562   if (ps->verbosity >= 4 && !(ps->conflicts % 1000))
4563     report (ps, 4, 'C');
4564 }
4565
4566 static void
4567 inc_cinc (PS * ps)
4568 {
4569   ps->cinc = mulflt (ps->cinc, ps->fcinc);
4570   if (ps->lcinc < ps->cinc)
4571     crescore (ps);
4572 }
4573
4574 static void
4575 incincs (PS * ps)
4576 {
4577   inc_vinc (ps);
4578   inc_cinc (ps);
4579 #ifdef VISCORES
4580   viscores (ps);
4581 #endif
4582 }
4583
4584 static void
4585 disconnect_clause (PS * ps, Cls * c)
4586 {
4587   assert (c->connected);
4588
4589   if (c->size > 2)
4590     {
4591       if (c->learned)
4592         {
4593           assert (ps->nlclauses > 0);
4594           ps->nlclauses--;
4595
4596           assert (ps->llits >= c->size);
4597           ps->llits -= c->size;
4598         }
4599       else
4600         {
4601           assert (ps->noclauses > 0);
4602           ps->noclauses--;
4603
4604           assert (ps->olits >= c->size);
4605           ps->olits -= c->size;
4606         }
4607     }
4608
4609 #ifndef NDEBUG
4610   c->connected = 0;
4611 #endif
4612 }
4613
4614 static int
4615 clause_is_toplevel_satisfied (PS * ps, Cls * c)
4616 {
4617   Lit *lit, **p, **eol = end_of_lits (c);
4618   Var *v;
4619
4620   for (p = c->lits; p < eol; p++)
4621     {
4622       lit = *p;
4623       if (lit->val == TRUE)
4624         {
4625           v = LIT2VAR (lit);
4626           if (!v->level)
4627             return 1;
4628         }
4629     }
4630
4631   return 0;
4632 }
4633
4634 static int
4635 collect_clause (PS * ps, Cls * c)
4636 {
4637   assert (c->collect);
4638   c->collect = 0;
4639
4640 #ifdef TRACE
4641   assert (!c->collected);
4642   c->collected = 1;
4643 #endif
4644   disconnect_clause (ps, c);
4645
4646 #ifdef TRACE
4647   if (ps->trace && (!c->learned || c->used))
4648     return 0;
4649 #endif
4650   delete_clause (ps, c);
4651
4652   return 1;
4653 }
4654
4655 static size_t
4656 collect_clauses (PS * ps)
4657 {
4658   Cls *c, **p, **q, * next;
4659   Lit * lit, * eol;
4660   size_t res;
4661   int i;
4662
4663   res = ps->current_bytes;
4664
4665   eol = ps->lits + 2 * ps->max_var + 1;
4666   for (lit = ps->lits + 2; lit <= eol; lit++)
4667     {
4668       for (i = 0; i <= 1; i++)
4669         {
4670           if (i)
4671             {
4672 #ifdef NO_BINARY_CLAUSES
4673               Ltk * lstk = LIT2IMPLS (lit);
4674               Lit ** r, ** s;
4675               r = lstk->start;
4676               if (lit->val != TRUE || LIT2VAR (lit)->level)
4677                 for (s = r; s < lstk->start + lstk->count; s++)
4678                   {
4679                     Lit * other = *s;
4680                     Var *v = LIT2VAR (other);
4681                     if (v->level ||
4682                         other->val != TRUE)
4683                       *r++ = other;
4684                   }
4685               lstk->count = r - lstk->start;
4686               continue;
4687 #else
4688               p = LIT2IMPLS (lit);
4689 #endif
4690             }
4691           else
4692             p = LIT2HTPS (lit);
4693
4694           for (c = *p; c; c = next)
4695             {
4696               q = c->next;
4697               if (c->lits[0] != lit)
4698                 q++;
4699
4700               next = *q;
4701               if (c->collect)
4702                 *p = next;
4703               else
4704                 p = q;
4705             }
4706         }
4707     }
4708
4709 #ifndef NDSC
4710   for (lit = ps->lits + 2; lit <= eol; lit++)
4711     {
4712       p = LIT2DHTPS (lit);
4713       while ((c = *p))
4714         {
4715           Lit * other = c->lits[0];
4716           if (other == lit)
4717             {
4718               q = c->next + 1;
4719             }
4720           else
4721             {
4722               assert (c->lits[1] == lit);
4723               q = c->next;
4724             }
4725
4726           if (c->collect)
4727             *p = *q;
4728           else
4729             p = q;
4730         }
4731     }
4732 #endif
4733
4734   for (p = SOC; p != EOC; p = NXC (p))
4735     {
4736       c = *p;
4737
4738       if (!c)
4739         continue;
4740
4741       if (!c->collect)
4742         continue;
4743
4744       if (collect_clause (ps, c))
4745         *p = 0;
4746     }
4747
4748 #ifdef TRACE
4749   if (!ps->trace)
4750 #endif
4751     {
4752       q = ps->oclauses;
4753       for (p = q; p < ps->ohead; p++)
4754         if ((c = *p))
4755           *q++ = c;
4756       ps->ohead = q;
4757
4758       q = ps->lclauses;
4759       for (p = q; p < ps->lhead; p++)
4760         if ((c = *p))
4761           *q++ = c;
4762       ps->lhead = q;
4763     }
4764
4765   assert (ps->current_bytes <= res);
4766   res -= ps->current_bytes;
4767   ps->recycled += res;
4768
4769   LOG ( fprintf (ps->out, "%scollected %ld bytes\n", ps->prefix, (long)res));
4770
4771   return res;
4772 }
4773
4774 static int
4775 need_to_reduce (PS * ps)
4776 {
4777   return ps->nlclauses >= reduce_limit_on_lclauses (ps);
4778 }
4779
4780 #ifdef NLUBY
4781
4782 static void
4783 inc_drestart (PS * ps)
4784 {
4785   ps->drestart *= FRESTART;
4786   ps->drestart /= 100;
4787
4788   if (ps->drestart >= MAXRESTART)
4789     ps->drestart = MAXRESTART;
4790 }
4791
4792 static void
4793 inc_ddrestart (PS * ps)
4794 {
4795   ps->ddrestart *= FRESTART;
4796   ps->ddrestart /= 100;
4797
4798   if (ps->ddrestart >= MAXRESTART)
4799     ps->ddrestart = MAXRESTART;
4800 }
4801
4802 #else
4803
4804 static int
4805 luby (int i)
4806 {
4807   int k;
4808   for (k = 1; k < 32; k++)
4809     if (i == (1 << k) - 1)
4810       return 1 << (k - 1);
4811
4812   for (k = 1;; k++)
4813     if ((1 << (k - 1)) <= i && i < (1 << k) - 1)
4814       return luby (i - (1 << (k-1)) + 1);
4815 }
4816
4817 #endif
4818
4819 #ifndef NLUBY
4820 static void
4821 inc_lrestart (PS * ps, int skip)
4822 {
4823   unsigned delta;
4824
4825   delta = 100 * luby (++ps->lubycnt);
4826   ps->lrestart = ps->conflicts + delta;
4827
4828   if (ps->waslubymaxdelta)
4829     report (ps, 1, skip ? 'N' : 'R');
4830   else
4831     report (ps, 2, skip ? 'n' : 'r');
4832
4833   if (delta > ps->lubymaxdelta)
4834     {
4835       ps->lubymaxdelta = delta;
4836       ps->waslubymaxdelta = 1;
4837     }
4838   else
4839     ps->waslubymaxdelta = 0;
4840 }
4841 #endif
4842
4843 static void
4844 init_restart (PS * ps)
4845 {
4846 #ifdef NLUBY
4847   /* TODO: why is it better in incremental usage to have smaller initial
4848    * outer restart interval?
4849    */
4850   ps->ddrestart = ps->calls > 1 ? MINRESTART : 1000;
4851   ps->drestart = MINRESTART;
4852   ps->lrestart = ps->conflicts + ps->drestart;
4853 #else
4854   ps->lubycnt = 0;
4855   ps->lubymaxdelta = 0;
4856   ps->waslubymaxdelta = 0;
4857   inc_lrestart (ps, 0);
4858 #endif
4859 }
4860
4861 static void
4862 restart (PS * ps)
4863 {
4864   int skip;
4865 #ifdef NLUBY
4866   char kind;
4867   int outer;
4868
4869   inc_drestart (ps);
4870   outer = (ps->drestart >= ps->ddrestart);
4871
4872   if (outer)
4873     skip = very_high_agility (ps);
4874   else
4875     skip = high_agility (ps);
4876 #else
4877   skip = medium_agility (ps);
4878 #endif
4879
4880 #ifdef STATS
4881   if (skip)
4882     ps->skippedrestarts++;
4883 #endif
4884
4885   assert (ps->conflicts >= ps->lrestart);
4886
4887   if (!skip)
4888     {
4889       ps->restarts++;
4890       assert (ps->LEVEL > 1);
4891       LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts));
4892       undo (ps, 0);
4893     }
4894
4895 #ifdef NLUBY
4896   if (outer)
4897     {
4898       kind = skip ? 'N' : 'R';
4899       inc_ddrestart (ps);
4900       ps->drestart = MINRESTART;
4901     }
4902   else  if (skip)
4903     {
4904       kind = 'n';
4905     }
4906   else
4907     {
4908       kind = 'r';
4909     }
4910
4911   assert (ps->drestart <= MAXRESTART);
4912   ps->lrestart = ps->conflicts + ps->drestart;
4913   assert (ps->lrestart > ps->conflicts);
4914
4915   report (outer ? 1 : 2, kind);
4916 #else
4917   inc_lrestart (ps, skip);
4918 #endif
4919 }
4920
4921 inline static void
4922 assign_decision (PS * ps, Lit * lit)
4923 {
4924   assert (!ps->conflict);
4925
4926   ps->LEVEL++;
4927
4928   LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL));
4929   LOG ( fprintf (ps->out,
4930                  "%sassign %d at level %d <= DECISION\n",
4931                  ps->prefix, LIT2INT (lit), ps->LEVEL));
4932
4933   assign (ps, lit, 0);
4934 }
4935
4936 #ifndef NFL
4937
4938 static int
4939 lit_has_binary_clauses (PS * ps, Lit * lit)
4940 {
4941 #ifdef NO_BINARY_CLAUSES
4942   Ltk* lstk = LIT2IMPLS (lit);
4943   return lstk->count != 0;
4944 #else
4945   return *LIT2IMPLS (lit) != 0;
4946 #endif
4947 }
4948
4949 static void
4950 flbcp (PS * ps)
4951 {
4952 #ifdef STATS
4953   unsigned long long propagaions_before_bcp = ps->propagations;
4954 #endif
4955   bcp (ps);
4956 #ifdef STATS
4957   ps->flprops += ps->propagations - propagaions_before_bcp;
4958 #endif
4959 }
4960
4961 inline static int
4962 cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b)
4963 {
4964   (void) ps;
4965   return -cmp_rnk (a, b);
4966 }
4967
4968 inline static Flt
4969 rnk2jwh (PS * ps, Rnk * r)
4970 {
4971   Flt res, sum, pjwh, njwh;
4972   Lit * plit, * nlit;
4973
4974   plit = RNK2LIT (r);
4975   nlit = plit + 1;
4976
4977   pjwh = *LIT2JWH (plit);
4978   njwh = *LIT2JWH (nlit);
4979
4980   res = mulflt (pjwh, njwh);
4981
4982   sum = addflt (pjwh, njwh);
4983   sum = mulflt (sum, base2flt (1, -10));
4984   res = addflt (res, sum);
4985
4986   return res;
4987 }
4988
4989 static int
4990 cmp_inverse_jwh_rnk (PS * ps, Rnk * r, Rnk * s)
4991 {
4992   Flt a = rnk2jwh (ps, r);
4993   Flt b = rnk2jwh (ps, s);
4994   int res = cmpflt (a, b);
4995
4996   if (res)
4997     return -res;
4998
4999   return cmp_inverse_rnk (ps, r, s);
5000 }
5001
5002 static void
5003 faillits (PS * ps)
5004 {
5005   unsigned i, j, old_trail_count, common, saved_count;
5006   unsigned new_saved_size, oldladded = ps->ladded;
5007   unsigned long long limit, delta;
5008   Lit * lit, * other, * pivot;
5009   Rnk * r, ** p, ** q;
5010   int new_trail_count;
5011   double started;
5012
5013   if (ps->plain)
5014     return;
5015
5016   if (ps->heap + 1 >= ps->hhead)
5017     return;
5018
5019   if (ps->propagations < ps->fllimit)
5020     return;
5021
5022   sflush (ps);
5023   started = ps->seconds;
5024
5025   ps->flcalls++;
5026 #ifdef STATSA
5027   ps->flrounds++;
5028 #endif
5029   delta = ps->propagations/10;
5030   if (delta >= 100*1000*1000) delta = 100*1000*1000;
5031   else if (delta <= 100*1000) delta = 100*1000;
5032
5033   limit = ps->propagations + delta;
5034   ps->fllimit = ps->propagations;
5035
5036   assert (!ps->LEVEL);
5037   assert (ps->simplifying);
5038
5039   if (ps->flcalls <= 1)
5040     SORT (Rnk *, cmp_inverse_jwh_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5041   else
5042     SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5043
5044   i = 1;                /* NOTE: heap starts at position '1' */
5045
5046   while (ps->propagations < limit)
5047     {
5048       if (ps->heap + i == ps->hhead)
5049         {
5050           if (ps->ladded == oldladded)
5051             break;
5052
5053           i = 1;
5054 #ifdef STATS
5055           ps->flrounds++;
5056 #endif
5057           oldladded = ps->ladded;
5058         }
5059
5060       assert (ps->heap + i < ps->hhead);
5061
5062       r = ps->heap[i++];
5063       lit = RNK2LIT (r);
5064
5065       if (lit->val)
5066         continue;
5067
5068       if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
5069         {
5070 #ifdef STATS
5071           ps->flskipped++;
5072 #endif
5073           continue;
5074         }
5075
5076 #ifdef STATS
5077       ps->fltried++;
5078 #endif
5079       LOG ( fprintf (ps->out, "%strying %d as failed literal\n",
5080             ps->prefix, LIT2INT (lit)));
5081
5082       assign_decision (ps, lit);
5083       old_trail_count = ps->thead - ps->trail;
5084       flbcp (ps);
5085
5086       if (ps->conflict)
5087         {
5088 EXPLICITLY_FAILED_LITERAL:
5089           LOG ( fprintf (ps->out, "%sfound explicitly failed literal %d\n",
5090                 ps->prefix, LIT2INT (lit)));
5091
5092           ps->failedlits++;
5093           ps->efailedlits++;
5094
5095           backtrack (ps);
5096           flbcp (ps);
5097
5098           if (!ps->conflict)
5099             continue;
5100
5101 CONTRADICTION:
5102           assert (!ps->LEVEL);
5103           backtrack (ps);
5104           assert (ps->mtcls);
5105
5106           goto RETURN;
5107         }
5108
5109       if (ps->propagations >= limit)
5110         {
5111           undo (ps, 0);
5112           break;
5113         }
5114
5115       lit = NOTLIT (lit);
5116
5117       if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
5118         {
5119 #ifdef STATS
5120           ps->flskipped++;
5121 #endif
5122           undo (ps, 0);
5123           continue;
5124         }
5125
5126 #ifdef STATS
5127       ps->fltried++;
5128 #endif
5129       LOG ( fprintf (ps->out, "%strying %d as failed literals\n",
5130             ps->prefix, LIT2INT (lit)));
5131
5132       new_trail_count = ps->thead - ps->trail;
5133       saved_count = new_trail_count - old_trail_count;
5134
5135       if (saved_count > ps->saved_size)
5136         {
5137           new_saved_size = ps->saved_size ? 2 * ps->saved_size : 1;
5138           while (saved_count > new_saved_size)
5139             new_saved_size *= 2;
5140
5141           RESIZEN (ps->saved, ps->saved_size, new_saved_size);
5142           ps->saved_size = new_saved_size;
5143         }
5144
5145       for (j = 0; j < saved_count; j++)
5146         ps->saved[j] = ps->trail[old_trail_count + j];
5147
5148       undo (ps, 0);
5149
5150       assign_decision (ps, lit);
5151       flbcp (ps);
5152
5153       if (ps->conflict)
5154         goto EXPLICITLY_FAILED_LITERAL;
5155
5156       pivot = (ps->thead - ps->trail <= new_trail_count) ? lit : NOTLIT (lit);
5157
5158       common = 0;
5159       for (j = 0; j < saved_count; j++)
5160         if ((other = ps->saved[j])->val == TRUE)
5161           ps->saved[common++] = other;
5162
5163       undo (ps, 0);
5164
5165       LOG (if (common)
5166              fprintf (ps->out,
5167                       "%sfound %d literals implied by %d and %d\n",
5168                       ps->prefix, common,
5169                       LIT2INT (NOTLIT (lit)), LIT2INT (lit)));
5170
5171 #if 1 // set to zero to disable 'lifting'
5172       for (j = 0;
5173            j < common
5174           /* TODO: For some Velev benchmarks, extracting the common implicit
5175            * failed literals took quite some time.  This needs to be fixed by
5176            * a dedicated analyzer.  Up to then we bound the number of
5177            * propagations in this loop as well.
5178            */
5179            && ps->propagations < limit + delta
5180            ; j++)
5181         {
5182           other = ps->saved[j];
5183
5184           if (other->val == TRUE)
5185             continue;
5186
5187           assert (!other->val);
5188
5189           LOG ( fprintf (ps->out,
5190                         "%sforcing %d as forced implicitly failed literal\n",
5191                         ps->prefix, LIT2INT (other)));
5192
5193           assert (pivot != NOTLIT (other));
5194           assert (pivot != other);
5195
5196           assign_decision (ps, NOTLIT (other));
5197           flbcp (ps);
5198
5199           assert (ps->LEVEL == 1);
5200
5201           if (ps->conflict)
5202             {
5203               backtrack (ps);
5204               assert (!ps->LEVEL);
5205             }
5206           else
5207             {
5208               assign_decision (ps, pivot);
5209               flbcp (ps);
5210
5211               backtrack (ps);
5212
5213               if (ps->LEVEL)
5214                 {
5215                   assert (ps->LEVEL == 1);
5216
5217                   flbcp (ps);
5218
5219                   if (ps->conflict)
5220                     {
5221                       backtrack (ps);
5222                       assert (!ps->LEVEL);
5223                     }
5224                   else
5225                     {
5226                       assign_decision (ps, NOTLIT (pivot));
5227                       flbcp (ps);
5228                       backtrack (ps);
5229
5230                       if (ps->LEVEL)
5231                         {
5232                           assert (ps->LEVEL == 1);
5233                           flbcp (ps);
5234
5235                           if (!ps->conflict)
5236                             {
5237 #ifdef STATS
5238                               ps->floopsed++;
5239 #endif
5240                               undo (ps, 0);
5241                               continue;
5242                             }
5243
5244                           backtrack (ps);
5245                         }
5246
5247                       assert (!ps->LEVEL);
5248                     }
5249
5250                   assert (!ps->LEVEL);
5251                 }
5252             }
5253           assert (!ps->LEVEL);
5254           flbcp (ps);
5255
5256           ps->failedlits++;
5257           ps->ifailedlits++;
5258
5259           if (ps->conflict)
5260             goto CONTRADICTION;
5261         }
5262 #endif
5263     }
5264
5265   ps->fllimit += 9 * (ps->propagations - ps->fllimit);  /* 10% for failed literals */
5266
5267 RETURN:
5268
5269   /* First flush top level assigned literals.  Those are prohibited from
5270    * being pushed up the heap during 'faillits' since 'simplifying' is set.
5271    */
5272   assert (ps->heap < ps->hhead);
5273   for (p = q = ps->heap + 1; p < ps->hhead; p++)
5274     {
5275       r = *p;
5276       lit = RNK2LIT (r);
5277       if (lit->val)
5278         r->pos = 0;
5279       else
5280         *q++ = r;
5281     }
5282
5283   /* Then resort with respect to EVSIDS score and fix positions.
5284    */
5285   SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5286   for (p = ps->heap + 1; p < ps->hhead; p++)
5287     (*p)->pos = p - ps->heap;
5288
5289   sflush (ps);
5290   ps->flseconds += ps->seconds - started;
5291 }
5292
5293 #endif
5294
5295 static void
5296 simplify (PS * ps, int forced)
5297 {
5298   Lit * lit, * notlit, ** t;
5299   unsigned collect, delta;
5300 #ifdef STATS
5301   size_t bytes_collected;
5302 #endif
5303   int * q, ilit;
5304   Cls **p, *c;
5305   Var * v;
5306
5307 #ifndef NDEDBUG
5308   (void) forced;
5309 #endif
5310
5311   assert (!ps->mtcls);
5312   assert (!satisfied (ps));
5313   assert (forced || ps->lsimplify <= ps->propagations);
5314   assert (forced || ps->fsimplify <= ps->fixed);
5315
5316   if (ps->LEVEL)
5317     undo (ps, 0);
5318 #ifndef NFL
5319   ps->simplifying = 1;
5320   faillits (ps);
5321   ps->simplifying = 0;
5322
5323   if (ps->mtcls)
5324     return;
5325 #endif
5326
5327   if (ps->cils != ps->cilshead)
5328     {
5329       assert (ps->ttail == ps->thead);
5330       assert (ps->ttail2 == ps->thead);
5331       ps->ttail = ps->trail;
5332       for (t = ps->trail; t < ps->thead; t++)
5333         {
5334           lit = *t;
5335           v = LIT2VAR (lit);
5336           if (v->internal)
5337             {
5338               assert (LIT2INT (lit) < 0);
5339               assert (lit->val == TRUE);
5340               unassign (ps, lit);
5341             }
5342           else
5343             *ps->ttail++ = lit;
5344         }
5345       ps->ttail2 = ps->thead = ps->ttail;
5346
5347       for (q = ps->cils; q != ps->cilshead; q++)
5348         {
5349           ilit = *q;
5350           assert (0 < ilit && ilit <= (int) ps->max_var);
5351           v = ps->vars + ilit;
5352           assert (v->internal);
5353           v->level = 0;
5354           v->reason = 0;
5355           lit = int2lit (ps, -ilit);
5356           assert (lit->val == UNDEF);
5357           lit->val = TRUE;
5358           notlit = NOTLIT (lit);
5359           assert (notlit->val == UNDEF);
5360           notlit->val = FALSE;
5361         }
5362     }
5363
5364   collect = 0;
5365   for (p = SOC; p != EOC; p = NXC (p))
5366     {
5367       c = *p;
5368       if (!c)
5369         continue;
5370
5371 #ifdef TRACE
5372       if (c->collected)
5373         continue;
5374 #endif
5375
5376       if (c->locked)
5377         continue;
5378
5379       assert (!c->collect);
5380       if (clause_is_toplevel_satisfied (ps, c))
5381         {
5382           mark_clause_to_be_collected (c);
5383           collect++;
5384         }
5385     }
5386
5387   LOG ( fprintf (ps->out, "%scollecting %d clauses\n", ps->prefix, collect));
5388 #ifdef STATS
5389   bytes_collected =
5390 #endif
5391   collect_clauses (ps);
5392 #ifdef STATS
5393   ps->srecycled += bytes_collected;
5394 #endif
5395
5396   if (ps->cils != ps->cilshead)
5397     {
5398       for (q = ps->cils; q != ps->cilshead; q++)
5399         {
5400           ilit = *q;
5401           assert (0 < ilit && ilit <= (int) ps->max_var);
5402           assert (ps->vars[ilit].internal);
5403           if (ps->rilshead == ps->eorils)
5404             ENLARGE (ps->rils, ps->rilshead, ps->eorils);
5405           *ps->rilshead++ = ilit;
5406           lit = int2lit (ps, -ilit);
5407           assert (lit->val == TRUE);
5408           lit->val = UNDEF;
5409           notlit = NOTLIT (lit);
5410           assert (notlit->val == FALSE);
5411           notlit->val = UNDEF;
5412         }
5413       ps->cilshead = ps->cils;
5414     }
5415
5416   delta = 10 * (ps->olits + ps->llits) + 100000;
5417   if (delta > 2000000)
5418     delta = 2000000;
5419   ps->lsimplify = ps->propagations + delta;
5420   ps->fsimplify = ps->fixed;
5421   ps->simps++;
5422
5423   report (ps, 1, 's');
5424 }
5425
5426 static void
5427 iteration (PS * ps)
5428 {
5429   assert (!ps->LEVEL);
5430   assert (bcp_queue_is_empty (ps));
5431   assert (ps->isimplify < ps->fixed);
5432
5433   ps->iterations++;
5434   report (ps, 2, 'i');
5435 #ifdef NLUBY
5436   ps->drestart = MINRESTART;
5437   ps->lrestart = ps->conflicts + ps->drestart;
5438 #else
5439   init_restart (ps);
5440 #endif
5441   ps->isimplify = ps->fixed;
5442 }
5443
5444 static int
5445 cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
5446 {
5447   Act a, b, * p, * q;
5448
5449   (void) ps;
5450
5451   assert (c->learned);
5452   assert (d->learned);
5453
5454   if (c->glue < d->glue)                // smaller glue preferred
5455     return 1;
5456
5457   if (c->glue > d->glue)
5458     return -1;
5459
5460   p = CLS2ACT (c);
5461   q = CLS2ACT (d);
5462   a = *p;
5463   b = *q;
5464
5465   if (a < b)                            // then higher activity
5466     return -1;
5467
5468   if (b < a)
5469     return 1;
5470
5471   if (c->size < d->size)                // then smaller size
5472     return 1;
5473
5474   if (c->size > d->size)
5475     return -1;
5476
5477   return 0;
5478 }
5479
5480 static void
5481 reduce (PS * ps, unsigned percentage)
5482 {
5483   unsigned redcount, lcollect, collect, target;
5484 #ifdef STATS
5485   size_t bytes_collected;
5486 #endif
5487   Cls **p, *c;
5488
5489   assert (ps->rhead == ps->resolved);
5490
5491   ps->lastreduceconflicts = ps->conflicts;
5492
5493   assert (percentage <= 100);
5494   LOG ( fprintf (ps->out,
5495                 "%sreducing %u%% learned clauses\n",
5496                 ps->prefix, percentage));
5497
5498   while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved))
5499     ENLARGE (ps->resolved, ps->rhead, ps->eor);
5500
5501   collect = 0;
5502   lcollect = 0;
5503
5504   for (p = ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p != EOC; p = NXC (p))
5505     {
5506       c = *p;
5507       if (!c)
5508         continue;
5509
5510 #ifdef TRACE
5511       if (c->collected)
5512         continue;
5513 #endif
5514
5515       if (c->locked)
5516         continue;
5517
5518       assert (!c->collect);
5519       if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c))
5520         {
5521           mark_clause_to_be_collected (c);
5522           collect++;
5523
5524           if (c->learned && c->size > 2)
5525             lcollect++;
5526
5527           continue;
5528         }
5529
5530       if (!c->learned)
5531         continue;
5532
5533       if (c->size <= 2)
5534         continue;
5535
5536       assert (ps->rhead < ps->eor);
5537       *ps->rhead++ = c;
5538     }
5539   assert (ps->rhead <= ps->eor);
5540
5541   ps->fsimplify = ps->fixed;
5542
5543   redcount = ps->rhead - ps->resolved;
5544   SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount);
5545
5546   assert (ps->nlclauses >= lcollect);
5547   target = ps->nlclauses - lcollect + 1;
5548
5549   target = (percentage * target + 99) / 100;
5550
5551   if (target >= redcount)
5552     target = redcount;
5553
5554   ps->rhead = ps->resolved + target;
5555   while (ps->rhead > ps->resolved)
5556     {
5557       c = *--ps->rhead;
5558       mark_clause_to_be_collected (c);
5559
5560       collect++;
5561       if (c->learned && c->size > 2)    /* just for consistency */
5562         lcollect++;
5563     }
5564
5565   if (collect)
5566     {
5567       ps->reductions++;
5568 #ifdef STATS
5569       bytes_collected =
5570 #endif
5571       collect_clauses (ps);
5572 #ifdef STATS
5573       ps->rrecycled += bytes_collected;
5574 #endif
5575       report (ps, 2, '-');
5576     }
5577
5578   if (!lcollect)
5579     inc_lreduce (ps);           /* avoid dead lock */
5580
5581   assert (ps->rhead == ps->resolved);
5582 }
5583
5584 static void
5585 init_reduce (PS * ps)
5586 {
5587   // lreduce = loadded / 2;
5588   ps->lreduce = 1000;
5589
5590   if (ps->lreduce < 100)
5591     ps->lreduce = 100;
5592
5593   if (ps->verbosity)
5594      fprintf (ps->out,
5595              "%s\n%sinitial reduction limit %u clauses\n%s\n",
5596              ps->prefix, ps->prefix, ps->lreduce, ps->prefix);
5597 }
5598
5599 static unsigned
5600 rng (PS * ps)
5601 {
5602   unsigned res = ps->srng;
5603   ps->srng *= 1664525u;
5604   ps->srng += 1013904223u;
5605   NOLOG ( fprintf (ps->out, "%srng () = %u\n", ps->prefix, res));
5606   return res;
5607 }
5608
5609 static unsigned
5610 rrng (PS * ps, unsigned low, unsigned high)
5611 {
5612   unsigned long long tmp;
5613   unsigned res, elements;
5614   assert (low <= high);
5615   elements = high - low + 1;
5616   tmp = rng (ps);
5617   tmp *= elements;
5618   tmp >>= 32;
5619   tmp += low;
5620   res = tmp;
5621   NOLOG ( fprintf (ps->out, "%srrng (ps, %u, %u) = %u\n", ps->prefix, low, high, res));
5622   assert (low <= res);
5623   assert (res <= high);
5624   return res;
5625 }
5626
5627 static Lit *
5628 decide_phase (PS * ps, Lit * lit)
5629 {
5630   Lit * not_lit = NOTLIT (lit);
5631   Var *v = LIT2VAR (lit);
5632
5633   assert (LIT2SGN (lit) > 0);
5634   if (v->usedefphase)
5635     {
5636       if (v->defphase)
5637         {
5638           /* assign to TRUE */
5639         }
5640       else
5641         {
5642           /* assign to FALSE */
5643           lit = not_lit;
5644         }
5645     }
5646   else if (!v->assigned)
5647     {
5648 #ifdef STATS
5649       ps->staticphasedecisions++;
5650 #endif
5651       if (ps->defaultphase == POSPHASE)
5652         {
5653           /* assign to TRUE */
5654         }
5655       else if (ps->defaultphase == NEGPHASE)
5656         {
5657           /* assign to FALSE */
5658           lit = not_lit;
5659         }
5660       else if (ps->defaultphase == RNDPHASE)
5661         {
5662           /* randomly assign default phase */
5663           if (rrng (ps, 1, 2) != 2)
5664             lit = not_lit;
5665         }
5666       else if (*LIT2JWH(lit) <= *LIT2JWH (not_lit))
5667         {
5668           /* assign to FALSE (Jeroslow-Wang says there are more short
5669            * clauses with negative occurence of this variable, so satisfy
5670            * those, to minimize BCP)
5671            */
5672           lit = not_lit;
5673         }
5674       else
5675         {
5676           /* assign to TRUE (... but strictly more positive occurrences) */
5677         }
5678     }
5679   else
5680     {
5681       /* repeat last phase: phase saving heuristic */
5682
5683       if (v->phase)
5684         {
5685           /* assign to TRUE (last phase was TRUE as well) */
5686         }
5687       else
5688         {
5689           /* assign to FALSE (last phase was FALSE as well) */
5690           lit = not_lit;
5691         }
5692     }
5693
5694   return lit;
5695 }
5696
5697 static unsigned
5698 gcd (unsigned a, unsigned b)
5699 {
5700   unsigned tmp;
5701
5702   assert (a);
5703   assert (b);
5704
5705   if (a < b)
5706     {
5707       tmp = a;
5708       a = b;
5709       b = tmp;
5710     }
5711
5712   while (b)
5713     {
5714       assert (a >= b);
5715       tmp = b;
5716       b = a % b;
5717       a = tmp;
5718     }
5719
5720   return a;
5721 }
5722
5723 static Lit *
5724 rdecide (PS * ps)
5725 {
5726   unsigned idx, delta, spread;
5727   Lit * res;
5728
5729   spread = RDECIDE;
5730   if (rrng (ps, 1, spread) != 2)
5731     return 0;
5732
5733   assert (1 <= ps->max_var);
5734   idx = rrng (ps, 1, ps->max_var);
5735   res = int2lit (ps, idx);
5736
5737   if (res->val != UNDEF)
5738     {
5739       delta = rrng (ps, 1, ps->max_var);
5740       while (gcd (delta, ps->max_var) != 1)
5741         delta--;
5742
5743       assert (1 <= delta);
5744       assert (delta <= ps->max_var);
5745
5746       do {
5747         idx += delta;
5748         if (idx > ps->max_var)
5749           idx -= ps->max_var;
5750         res = int2lit (ps, idx);
5751       } while (res->val != UNDEF);
5752     }
5753
5754 #ifdef STATS
5755   ps->rdecisions++;
5756 #endif
5757   res = decide_phase (ps, res);
5758   LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res)));
5759
5760   return res;
5761 }
5762
5763 static Lit *
5764 sdecide (PS * ps)
5765 {
5766   Lit *res;
5767   Rnk *r;
5768
5769   for (;;)
5770     {
5771       r = htop (ps);
5772       res = RNK2LIT (r);
5773       if (res->val == UNDEF) break;
5774       (void) hpop (ps);
5775       NOLOG ( fprintf (ps->out,
5776                       "%shpop %u %u %u\n",
5777                       ps->prefix, r - ps->rnks,
5778                       FLTMANTISSA(r->score),
5779                       FLTEXPONENT(r->score)));
5780     }
5781
5782 #ifdef STATS
5783   ps->sdecisions++;
5784 #endif
5785   res = decide_phase (ps, res);
5786
5787   LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res)));
5788
5789   return res;
5790 }
5791
5792 static Lit *
5793 adecide (PS * ps)
5794 {
5795   Lit *lit;
5796   Var * v;
5797
5798   assert (ps->als < ps->alshead);
5799   assert (!ps->failed_assumption);
5800
5801   while (ps->alstail < ps->alshead)
5802     {
5803       lit = *ps->alstail++;
5804
5805       if (lit->val == FALSE)
5806         {
5807           ps->failed_assumption = lit;
5808           v = LIT2VAR (lit);
5809
5810           use_var (ps, v);
5811
5812           LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n",
5813                         ps->prefix, LIT2INT (ps->failed_assumption)));
5814           fanalyze (ps);
5815           return 0;
5816         }
5817
5818       if (lit->val == TRUE)
5819         {
5820           v = LIT2VAR (lit);
5821           if (v->level > ps->adecidelevel)
5822             ps->adecidelevel = v->level;
5823           continue;
5824         }
5825
5826 #ifdef STATS
5827       ps->assumptions++;
5828 #endif
5829       LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit)));
5830       ps->adecidelevel = ps->LEVEL + 1;
5831
5832       return lit;
5833     }
5834
5835   return 0;
5836 }
5837
5838 static void
5839 decide (PS * ps)
5840 {
5841   Lit * lit;
5842
5843   assert (!satisfied (ps));
5844   assert (!ps->conflict);
5845
5846   if (ps->alstail < ps->alshead && (lit = adecide (ps)))
5847     ;
5848   else if (ps->failed_assumption)
5849     return;
5850   else if (satisfied (ps))
5851     return;
5852   else if (!(lit = rdecide (ps)))
5853     lit = sdecide (ps);
5854
5855   assert (lit);
5856   assign_decision (ps, lit);
5857
5858   ps->levelsum += ps->LEVEL;
5859   ps->decisions++;
5860 }
5861
5862 static int
5863 sat (PS * ps, int l)
5864 {
5865   int count = 0, backtracked;
5866
5867   if (!ps->conflict)
5868     bcp (ps);
5869
5870   if (ps->conflict)
5871     backtrack (ps);
5872
5873   if (ps->mtcls)
5874     return PICOSAT_UNSATISFIABLE;
5875
5876   if (satisfied (ps))
5877     goto SATISFIED;
5878
5879   if (ps->lsimplify <= ps->propagations)
5880     simplify (ps, 0);
5881
5882   if (ps->mtcls)
5883     return PICOSAT_UNSATISFIABLE;
5884
5885   if (satisfied (ps))
5886     goto SATISFIED;
5887
5888   init_restart (ps);
5889
5890   if (!ps->lreduce)
5891     init_reduce (ps);
5892
5893   ps->isimplify = ps->fixed;
5894   backtracked = 0;
5895
5896   for (;;)
5897     {
5898       if (!ps->conflict)
5899         bcp (ps);
5900
5901       if (ps->conflict)
5902         {
5903           incincs (ps);
5904           backtrack (ps);
5905
5906           if (ps->mtcls)
5907             return PICOSAT_UNSATISFIABLE;
5908           backtracked = 1;
5909           continue;
5910         }
5911
5912       if (satisfied (ps))
5913         {
5914 SATISFIED:
5915 #ifndef NDEBUG
5916           original_clauses_satisfied (ps);
5917           assumptions_satisfied (ps);
5918 #endif
5919           return PICOSAT_SATISFIABLE;
5920         }
5921
5922       if (backtracked)
5923         {
5924           backtracked = 0;
5925           if (!ps->LEVEL && ps->isimplify < ps->fixed)
5926             iteration (ps);
5927         }
5928
5929       if (l >= 0 && count >= l)         /* decision limit reached ? */
5930         return PICOSAT_UNKNOWN;
5931
5932       if (ps->propagations >= ps->lpropagations)/* propagation limit reached ? */
5933         return PICOSAT_UNKNOWN;
5934
5935 #ifndef NADC
5936       if (!ps->adodisabled && ps->adoconflicts >= ps->adoconflictlimit)
5937         {
5938           assert (bcp_queue_is_empty (ps));
5939           return PICOSAT_UNKNOWN;
5940         }
5941 #endif
5942
5943       if (ps->fsimplify < ps->fixed && ps->lsimplify <= ps->propagations)
5944         {
5945           simplify (ps, 0);
5946           if (!bcp_queue_is_empty (ps))
5947             continue;
5948 #ifndef NFL
5949           if (ps->mtcls)
5950             return PICOSAT_UNSATISFIABLE;
5951
5952           if (satisfied (ps))
5953             return PICOSAT_SATISFIABLE;
5954
5955           assert (!ps->LEVEL);
5956 #endif
5957         }
5958
5959       if (need_to_reduce (ps))
5960         reduce (ps, 50);
5961
5962       if (ps->conflicts >= ps->lrestart && ps->LEVEL > 2)
5963         restart (ps);
5964
5965       decide (ps);
5966       if (ps->failed_assumption)
5967         return PICOSAT_UNSATISFIABLE;
5968       count++;
5969     }
5970 }
5971
5972 static void
5973 rebias (PS * ps)
5974 {
5975   Cls ** p, * c;
5976   Var * v;
5977
5978   for (v = ps->vars + 1; v <= ps->vars + ps->max_var; v++)
5979     v->assigned = 0;
5980
5981   memset (ps->jwh, 0, 2 * (ps->max_var + 1) * sizeof *ps->jwh);
5982
5983   for (p = ps->oclauses; p < ps->ohead; p++)
5984     {
5985       c = *p;
5986
5987       if (!c)
5988         continue;
5989
5990       if (c->learned)
5991         continue;
5992
5993       incjwh (ps, c);
5994     }
5995 }
5996
5997 #ifdef TRACE
5998
5999 static unsigned
6000 core (PS * ps)
6001 {
6002   unsigned idx, prev, this, delta, i, lcore, vcore;
6003   unsigned *stack, *shead, *eos;
6004   Lit **q, **eol, *lit;
6005   Cls *c, *reason;
6006   Znt *p, byte;
6007   Zhn *zhain;
6008   Var *v;
6009
6010   assert (ps->trace);
6011
6012   assert (ps->mtcls || ps->failed_assumption);
6013   if (ps->ocore >= 0)
6014     return ps->ocore;
6015
6016   lcore = ps->ocore = vcore = 0;
6017
6018   stack = shead = eos = 0;
6019   ENLARGE (stack, shead, eos);
6020
6021   if (ps->mtcls)
6022     {
6023       idx = CLS2IDX (ps->mtcls);
6024       *shead++ = idx;
6025     }
6026   else
6027     {
6028       assert (ps->failed_assumption);
6029       v = LIT2VAR (ps->failed_assumption);
6030       reason = v->reason;
6031       assert (reason);
6032       idx = CLS2IDX (reason);
6033       *shead++ = idx;
6034     }
6035
6036   while (shead > stack)
6037     {
6038       idx = *--shead;
6039       zhain = IDX2ZHN (idx);
6040
6041       if (zhain)
6042         {
6043           if (zhain->core)
6044             continue;
6045
6046           zhain->core = 1;
6047           lcore++;
6048
6049           c = IDX2CLS (idx);
6050           if (c)
6051             {
6052               assert (!c->core);
6053               c->core = 1;
6054             }
6055
6056           i = 0;
6057           delta = 0;
6058           prev = 0;
6059           for (p = zhain->znt; (byte = *p); p++, i += 7)
6060             {
6061               delta |= (byte & 0x7f) << i;
6062               if (byte & 0x80)
6063                 continue;
6064
6065               this = prev + delta;
6066               assert (prev < this);     /* no overflow */
6067
6068               if (shead == eos)
6069                 ENLARGE (stack, shead, eos);
6070               *shead++ = this;
6071
6072               prev = this;
6073               delta = 0;
6074               i = -7;
6075             }
6076         }
6077       else
6078         {
6079           c = IDX2CLS (idx);
6080
6081           assert (c);
6082           assert (!c->learned);
6083
6084           if (c->core)
6085             continue;
6086
6087           c->core = 1;
6088           ps->ocore++;
6089
6090           eol = end_of_lits (c);
6091           for (q = c->lits; q < eol; q++)
6092             {
6093               lit = *q;
6094               v = LIT2VAR (lit);
6095               if (v->core)
6096                 continue;
6097
6098               v->core = 1;
6099               vcore++;
6100
6101               if (!ps->failed_assumption) continue;
6102               if (lit != ps->failed_assumption) continue;
6103
6104               reason = v->reason;
6105               if (!reason) continue;
6106               if (reason->core) continue;
6107
6108               idx = CLS2IDX (reason);
6109               if (shead == eos)
6110                 ENLARGE (stack, shead, eos);
6111               *shead++ = idx;
6112             }
6113         }
6114     }
6115
6116   DELETEN (stack, eos - stack);
6117
6118   if (ps->verbosity)
6119      fprintf (ps->out,
6120              "%s%u core variables out of %u (%.1f%%)\n"
6121              "%s%u core original clauses out of %u (%.1f%%)\n"
6122              "%s%u core learned clauses out of %u (%.1f%%)\n",
6123              ps->prefix, vcore, ps->max_var, PERCENT (vcore, ps->max_var),
6124              ps->prefix, ps->ocore, ps->oadded, PERCENT (ps->ocore, ps->oadded),
6125              ps->prefix, lcore, ps->ladded, PERCENT (lcore, ps->ladded));
6126
6127   return ps->ocore;
6128 }
6129
6130 static void
6131 trace_lits (PS * ps, Cls * c, FILE * file)
6132 {
6133   Lit **p, **eol = end_of_lits (c);
6134
6135   assert (c);
6136   assert (c->core);
6137
6138   for (p = c->lits; p < eol; p++)
6139     fprintf (file, "%d ", LIT2INT (*p));
6140
6141   fputc ('0', file);
6142 }
6143
6144 static void
6145 write_idx (PS * ps, unsigned idx, FILE * file)
6146 {
6147   fprintf (file, "%ld", EXPORTIDX (idx));
6148 }
6149
6150 static void
6151 trace_clause (PS * ps, unsigned idx, Cls * c, FILE * file, int fmt)
6152 {
6153   assert (c);
6154   assert (c->core);
6155   assert (fmt == RUP_TRACE_FMT || !c->learned);
6156   assert (CLS2IDX (c) == idx);
6157
6158   if (fmt != RUP_TRACE_FMT)
6159     {
6160       write_idx (ps, idx, file);
6161       fputc (' ', file);
6162     }
6163
6164   trace_lits (ps, c, file);
6165
6166   if (fmt != RUP_TRACE_FMT)
6167     fputs (" 0", file);
6168
6169   fputc ('\n', file);
6170 }
6171
6172 static void
6173 trace_zhain (PS * ps, unsigned idx, Zhn * zhain, FILE * file, int fmt)
6174 {
6175   unsigned prev, this, delta, i;
6176   Znt *p, byte;
6177   Cls * c;
6178
6179   assert (zhain);
6180   assert (zhain->core);
6181
6182   write_idx (ps, idx, file);
6183   fputc (' ', file);
6184
6185   if (fmt == EXTENDED_TRACECHECK_TRACE_FMT)
6186     {
6187       c = IDX2CLS (idx);
6188       assert (c);
6189       trace_lits (ps, c, file);
6190     }
6191   else
6192     {
6193       assert (fmt == COMPACT_TRACECHECK_TRACE_FMT);
6194       putc ('*', file);
6195     }
6196
6197   i = 0;
6198   delta = 0;
6199   prev = 0;
6200
6201   for (p = zhain->znt; (byte = *p); p++, i += 7)
6202     {
6203       delta |= (byte & 0x7f) << i;
6204       if (byte & 0x80)
6205         continue;
6206
6207       this = prev + delta;
6208
6209       putc (' ', file);
6210       write_idx (ps, this, file);
6211
6212       prev = this;
6213       delta = 0;
6214       i = -7;
6215     }
6216
6217   fputs (" 0\n", file);
6218 }
6219
6220 static void
6221 write_core (PS * ps, FILE * file)
6222 {
6223   Lit **q, **eol;
6224   Cls **p, *c;
6225
6226   fprintf (file, "p cnf %u %u\n", ps->max_var, core (ps));
6227
6228   for (p = SOC; p != EOC; p = NXC (p))
6229     {
6230       c = *p;
6231
6232       if (!c || c->learned || !c->core)
6233         continue;
6234
6235       eol = end_of_lits (c);
6236       for (q = c->lits; q < eol; q++)
6237         fprintf (file, "%d ", LIT2INT (*q));
6238
6239       fputs ("0\n", file);
6240     }
6241 }
6242
6243 #endif
6244
6245 static void
6246 write_trace (PS * ps, FILE * file, int fmt)
6247 {
6248 #ifdef TRACE
6249   Cls *c, ** p;
6250   Zhn *zhain;
6251   unsigned i;
6252
6253   core (ps);
6254
6255   if (fmt == RUP_TRACE_FMT)
6256     {
6257       ps->rupvariables = picosat_variables (ps),
6258       ps->rupclauses = picosat_added_original_clauses (ps);
6259       write_rup_header (ps, file);
6260     }
6261
6262   for (p = SOC; p != EOC; p = NXC (p))
6263     {
6264       c = *p;
6265
6266       if (ps->oclauses <= p && p < ps->eoo)
6267         {
6268           i = OIDX2IDX (p - ps->oclauses);
6269           assert (!c || CLS2IDX (c) == i);
6270         }
6271       else
6272         {
6273           assert (ps->lclauses <= p && p < ps->EOL);
6274           i = LIDX2IDX (p - ps->lclauses);
6275         }
6276
6277       zhain = IDX2ZHN (i);
6278
6279       if (zhain)
6280         {
6281           if (zhain->core)
6282             {
6283               if (fmt == RUP_TRACE_FMT)
6284                 trace_clause (ps,i, c, file, fmt);
6285               else
6286                 trace_zhain (ps, i, zhain, file, fmt);
6287             }
6288         }
6289       else if (c)
6290         {
6291           if (fmt != RUP_TRACE_FMT && c)
6292             {
6293               if (c->core)
6294                 trace_clause (ps, i, c, file, fmt);
6295             }
6296         }
6297     }
6298 #else
6299   (void) file;
6300   (void) fmt;
6301   (void) ps;
6302 #endif
6303 }
6304
6305 static void
6306 write_core_wrapper (PS * ps, FILE * file, int fmt)
6307 {
6308   (void) fmt;
6309 #ifdef TRACE
6310   write_core (ps, file);
6311 #else
6312   (void) ps;
6313   (void) file;
6314 #endif
6315 }
6316
6317 static Lit *
6318 import_lit (PS * ps, int lit, int nointernal)
6319 {
6320   Lit * res;
6321   Var * v;
6322
6323   ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal");
6324   ABORTIF (abs (lit) > (int) ps->max_var && ps->CLS != ps->clshead,
6325            "API usage: new variable index after 'picosat_push'");
6326
6327   if (abs (lit) <= (int) ps->max_var)
6328     {
6329       res = int2lit (ps, lit);
6330       v = LIT2VAR (res);
6331       if (nointernal && v->internal)
6332         ABORT ("API usage: trying to import invalid literal");
6333       else if (!nointernal && !v->internal)
6334         ABORT ("API usage: trying to import invalid context");
6335     }
6336   else
6337     {
6338       while (abs (lit) > (int) ps->max_var)
6339         inc_max_var (ps);
6340       res = int2lit (ps, lit);
6341     }
6342
6343   return res;
6344 }
6345
6346 #ifdef TRACE
6347 static void
6348 reset_core (PS * ps)
6349 {
6350   Cls ** p, * c;
6351   Zhn ** q, * z;
6352   unsigned i;
6353
6354   for (i = 1; i <= ps->max_var; i++)
6355     ps->vars[i].core = 0;
6356
6357   for (p = SOC; p != EOC; p = NXC (p))
6358     if ((c = *p))
6359       c->core = 0;
6360
6361   for (q = ps->zhains; q != ps->zhead; q++)
6362     if ((z = *q))
6363       z->core = 0;
6364
6365   ps->ocore = -1;
6366 }
6367 #endif
6368
6369 static void
6370 reset_assumptions (PS * ps)
6371 {
6372   Lit ** p;
6373
6374   ps->failed_assumption = 0;
6375
6376   if (ps->extracted_all_failed_assumptions)
6377     {
6378       for (p = ps->als; p < ps->alshead; p++)
6379         LIT2VAR (*p)->failed = 0;
6380
6381       ps->extracted_all_failed_assumptions = 0;
6382     }
6383
6384   ps->alstail = ps->alshead = ps->als;
6385   ps->adecidelevel = 0;
6386 }
6387
6388 static void
6389 check_ready (PS * ps)
6390 {
6391   ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized");
6392 }
6393
6394 static void
6395 check_sat_state (PS * ps)
6396 {
6397   ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state");
6398 }
6399
6400 static void
6401 check_unsat_state (PS * ps)
6402 {
6403   ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state");
6404 }
6405
6406 static void
6407 check_sat_or_unsat_or_unknown_state (PS * ps)
6408 {
6409   ABORTIF (ps->state != SAT && ps->state != UNSAT && ps->state != UNKNOWN,
6410            "API usage: expected to be in SAT, UNSAT, or UNKNOWN state");
6411 }
6412
6413 static void
6414 reset_partial (PS * ps)
6415 {
6416   unsigned idx;
6417   if (!ps->partial)
6418     return;
6419   for (idx = 1; idx <= ps->max_var; idx++)
6420     ps->vars[idx].partial = 0;
6421   ps->partial = 0;
6422 }
6423
6424 static void
6425 reset_incremental_usage (PS * ps)
6426 {
6427   unsigned num_non_false;
6428   Lit * lit, ** q;
6429
6430   check_sat_or_unsat_or_unknown_state (ps);
6431
6432   LOG ( fprintf (ps->out, "%sRESET incremental usage\n", ps->prefix));
6433
6434   if (ps->LEVEL)
6435     undo (ps, 0);
6436
6437   reset_assumptions (ps);
6438
6439   if (ps->conflict)
6440     {
6441       num_non_false = 0;
6442       for (q = ps->conflict->lits; q < end_of_lits (ps->conflict); q++)
6443         {
6444           lit = *q;
6445           if (lit->val != FALSE)
6446             num_non_false++;
6447         }
6448
6449       // assert (num_non_false >= 2); // TODO: why this assertion?
6450 #ifdef NO_BINARY_CLAUSES
6451       if (ps->conflict == &ps->cimpl)
6452         resetcimpl (ps);
6453 #endif
6454 #ifndef NADC
6455       if (ps->conflict == ps->adoconflict)
6456         resetadoconflict (ps);
6457 #endif
6458       ps->conflict = 0;
6459     }
6460
6461 #ifdef TRACE
6462   reset_core (ps);
6463 #endif
6464
6465   reset_partial (ps);
6466
6467   ps->saved_flips = ps->flips;
6468   ps->min_flipped = UINT_MAX;
6469   ps->saved_max_var = ps->max_var;
6470
6471   ps->state = READY;
6472 }
6473
6474 static void
6475 enter (PS * ps)
6476 {
6477   if (ps->nentered++)
6478     return;
6479
6480   check_ready (ps);
6481   ps->entered = picosat_time_stamp ();
6482 }
6483
6484 static void
6485 leave (PS * ps)
6486 {
6487   assert (ps->nentered);
6488   if (--ps->nentered)
6489     return;
6490
6491   sflush (ps);
6492 }
6493
6494 static void
6495 check_trace_support_and_execute (PS * ps,
6496                                  FILE * file,
6497                                  void (*f)(PS*,FILE*,int), int fmt)
6498 {
6499   check_ready (ps);
6500   check_unsat_state (ps);
6501 #ifdef TRACE
6502   ABORTIF (!ps->trace, "API usage: tracing disabled");
6503   enter (ps);
6504   f (ps, file, fmt);
6505   leave (ps);
6506 #else
6507   (void) file;
6508   (void) fmt;
6509   (void) f;
6510   ABORT ("compiled without trace support");
6511 #endif
6512 }
6513
6514 static void
6515 extract_all_failed_assumptions (PS * ps)
6516 {
6517   Lit ** p, ** eol;
6518   Var * v, * u;
6519   int pos;
6520   Cls * c;
6521
6522   assert (!ps->extracted_all_failed_assumptions);
6523
6524   assert (ps->failed_assumption);
6525   assert (ps->mhead == ps->marked);
6526
6527   if (ps->marked == ps->eom)
6528     ENLARGE (ps->marked, ps->mhead, ps->eom);
6529
6530   v = LIT2VAR (ps->failed_assumption);
6531   mark_var (ps, v);
6532   pos = 0;
6533
6534   while (pos < ps->mhead - ps->marked)
6535     {
6536       v = ps->marked[pos++];
6537       assert (v->mark);
6538       c = var2reason (ps, v);
6539       if (!c)
6540         continue;
6541       eol = end_of_lits (c);
6542       for (p = c->lits; p < eol; p++)
6543         {
6544           u = LIT2VAR (*p);
6545           if (!u->mark)
6546             mark_var (ps, u);
6547         }
6548 #ifdef NO_BINARY_CLAUSES
6549       if (c == &ps->impl)
6550         resetimpl (ps);
6551 #endif
6552     }
6553
6554   for (p = ps->als; p < ps->alshead; p++)
6555     {
6556       u = LIT2VAR (*p);
6557       if (!u->mark) continue;
6558       u->failed = 1;
6559       LOG ( fprintf (ps->out,
6560                      "%sfailed assumption %d\n",
6561                      ps->prefix, LIT2INT (*p)));
6562     }
6563
6564   while (ps->mhead > ps->marked)
6565     (*--ps->mhead)->mark = 0;
6566
6567   ps->extracted_all_failed_assumptions = 1;
6568 }
6569
6570 const char *
6571 picosat_copyright (void)
6572 {
6573   return "Copyright (c) 2006 - 2014 Armin Biere JKU Linz";
6574 }
6575
6576 PicoSAT *
6577 picosat_init (void)
6578 {
6579   return init (0, 0, 0, 0);
6580 }
6581
6582 PicoSAT *
6583 picosat_minit (void * pmgr,
6584                picosat_malloc pnew,
6585                picosat_realloc presize,
6586                picosat_free pfree)
6587 {
6588   ABORTIF (!pnew, "API usage: zero 'picosat_malloc' argument");
6589   ABORTIF (!presize, "API usage: zero 'picosat_realloc' argument");
6590   ABORTIF (!pfree, "API usage: zero 'picosat_free' argument");
6591   return init (pmgr, pnew, presize, pfree);
6592 }
6593
6594
6595 void
6596 picosat_adjust (PS * ps, int new_max_var)
6597 {
6598   unsigned new_size_vars;
6599
6600   ABORTIF (abs (new_max_var) > (int) ps->max_var && ps->CLS != ps->clshead,
6601            "API usage: adjusting variable index after 'picosat_push'");
6602   enter (ps);
6603
6604   new_max_var = abs (new_max_var);
6605   new_size_vars = new_max_var + 1;
6606
6607   if (ps->size_vars < new_size_vars)
6608     enlarge (ps, new_size_vars);
6609
6610   while (ps->max_var < (unsigned) new_max_var)
6611     inc_max_var (ps);
6612
6613   leave (ps);
6614 }
6615
6616 int
6617 picosat_inc_max_var (PS * ps)
6618 {
6619   if (ps->measurealltimeinlib)
6620     enter (ps);
6621   else
6622     check_ready (ps);
6623
6624   inc_max_var (ps);
6625
6626   if (ps->measurealltimeinlib)
6627     leave (ps);
6628
6629   return ps->max_var;
6630 }
6631
6632 int
6633 picosat_context (PS * ps)
6634 {
6635   return ps->clshead == ps->CLS ? 0 : LIT2INT (ps->clshead[-1]);
6636 }
6637
6638 int
6639 picosat_push (PS * ps)
6640 {
6641   int res;
6642   Lit *lit;
6643   Var * v;
6644
6645   if (ps->measurealltimeinlib)
6646     enter (ps);
6647   else
6648     check_ready (ps);
6649
6650   if (ps->state != READY)
6651     reset_incremental_usage (ps);
6652
6653   if (ps->rils != ps->rilshead)
6654     {
6655       res = *--ps->rilshead;
6656       assert (ps->vars[res].internal);
6657     }
6658   else
6659     {
6660       inc_max_var (ps);
6661       res = ps->max_var;
6662       v = ps->vars + res;
6663       assert (!v->internal);
6664       v->internal = 1;
6665       ps->internals++;
6666       LOG ( fprintf (ps->out, "%snew internal variable index %d\n", ps->prefix, res));
6667     }
6668
6669   lit = int2lit (ps, res);
6670
6671   if (ps->clshead == ps->eocls)
6672     ENLARGE (ps->CLS, ps->clshead, ps->eocls);
6673   *ps->clshead++ = lit;
6674
6675   ps->contexts++;
6676
6677   LOG ( fprintf (ps->out, "%snew context %d at depth %ld after push\n",
6678                  ps->prefix, res, (long)(ps->clshead - ps->CLS)));
6679
6680   if (ps->measurealltimeinlib)
6681     leave (ps);
6682
6683   return res;
6684 }
6685
6686 int
6687 picosat_pop (PS * ps)
6688 {
6689   Lit * lit;
6690   int res;
6691   ABORTIF (ps->CLS == ps->clshead, "API usage: too many 'picosat_pop'");
6692   ABORTIF (ps->added != ps->ahead, "API usage: incomplete clause");
6693
6694   if (ps->measurealltimeinlib)
6695     enter (ps);
6696   else
6697     check_ready (ps);
6698
6699   if (ps->state != READY)
6700     reset_incremental_usage (ps);
6701
6702   assert (ps->CLS < ps->clshead);
6703   lit = *--ps->clshead;
6704   LOG ( fprintf (ps->out, "%sclosing context %d at depth %ld after pop\n",
6705                  ps->prefix, LIT2INT (lit), (long)(ps->clshead - ps->CLS) + 1));
6706
6707   if (ps->cilshead == ps->eocils)
6708     ENLARGE (ps->cils, ps->cilshead, ps->eocils);
6709   *ps->cilshead++ = LIT2INT (lit);
6710
6711   if (ps->cilshead - ps->cils > MAXCILS) {
6712     LOG ( fprintf (ps->out,
6713                   "%srecycling %ld interals with forced simplification\n",
6714                   ps->prefix, (long)(ps->cilshead - ps->cils)));
6715     simplify (ps, 1);
6716   }
6717
6718   res = picosat_context (ps);
6719   if (res)
6720     LOG ( fprintf (ps->out, "%snew context %d at depth %ld after pop\n",
6721                    ps->prefix, res, (long)(ps->clshead - ps->CLS)));
6722   else
6723     LOG ( fprintf (ps->out, "%souter most context reached after pop\n", ps->prefix));
6724
6725   if (ps->measurealltimeinlib)
6726     leave (ps);
6727
6728   return res;
6729 }
6730
6731 void
6732 picosat_set_verbosity (PS * ps, int new_verbosity_level)
6733 {
6734   check_ready (ps);
6735   ps->verbosity = new_verbosity_level;
6736 }
6737
6738 void
6739 picosat_set_plain (PS * ps, int new_plain_value)
6740 {
6741   check_ready (ps);
6742   ps->plain = new_plain_value;
6743 }
6744
6745 int
6746 picosat_enable_trace_generation (PS * ps)
6747 {
6748   int res = 0;
6749   check_ready (ps);
6750 #ifdef TRACE
6751   ABORTIF (ps->addedclauses,
6752            "API usage: trace generation enabled after adding clauses");
6753   res = ps->trace = 1;
6754 #endif
6755   return res;
6756 }
6757
6758 void
6759 picosat_set_incremental_rup_file (PS * ps, FILE * rup_file, int m, int n)
6760 {
6761   check_ready (ps);
6762   assert (!ps->rupstarted);
6763   ps->rup = rup_file;
6764   ps->rupvariables = m;
6765   ps->rupclauses = n;
6766 }
6767
6768 void
6769 picosat_set_output (PS * ps, FILE * output_file)
6770 {
6771   check_ready (ps);
6772   ps->out = output_file;
6773 }
6774
6775 void
6776 picosat_measure_all_calls (PS * ps)
6777 {
6778   check_ready (ps);
6779   ps->measurealltimeinlib = 1;
6780 }
6781
6782 void
6783 picosat_set_prefix (PS * ps, const char * str)
6784 {
6785   check_ready (ps);
6786   new_prefix (ps, str);
6787 }
6788
6789 void
6790 picosat_set_seed (PS * ps, unsigned s)
6791 {
6792   check_ready (ps);
6793   ps->srng = s;
6794 }
6795
6796 void
6797 picosat_reset (PS * ps)
6798 {
6799   check_ready (ps);
6800   reset (ps);
6801 }
6802
6803 int
6804 picosat_add (PS * ps, int int_lit)
6805 {
6806   int res = ps->oadded;
6807   Lit *lit;
6808
6809   if (ps->measurealltimeinlib)
6810     enter (ps);
6811   else
6812     check_ready (ps);
6813
6814   ABORTIF (ps->rup && ps->rupstarted && ps->oadded >= (unsigned)ps->rupclauses,
6815            "API usage: adding too many clauses after RUP header written");
6816 #ifndef NADC
6817   ABORTIF (ps->addingtoado,
6818            "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6819 #endif
6820   if (ps->state != READY)
6821     reset_incremental_usage (ps);
6822
6823   if (ps->saveorig)
6824     {
6825       if (ps->sohead == ps->eoso)
6826         ENLARGE (ps->soclauses, ps->sohead, ps->eoso);
6827
6828       *ps->sohead++ = int_lit;
6829     }
6830
6831   if (int_lit)
6832     {
6833       lit = import_lit (ps, int_lit, 1);
6834       add_lit (ps, lit);
6835     }
6836   else
6837     simplify_and_add_original_clause (ps);
6838
6839   if (ps->measurealltimeinlib)
6840     leave (ps);
6841
6842   return res;
6843 }
6844
6845 int
6846 picosat_add_arg (PS * ps, ...)
6847 {
6848   int lit;
6849   va_list ap;
6850   va_start (ap, ps);
6851   while ((lit = va_arg (ap, int)))
6852     (void) picosat_add (ps, lit);
6853   va_end (ap);
6854   return picosat_add (ps, 0);
6855 }
6856
6857 int
6858 picosat_add_lits (PS * ps, int * lits)
6859 {
6860   const int * p;
6861   int lit;
6862   for (p = lits; (lit = *p); p++)
6863     (void) picosat_add (ps, lit);
6864   return picosat_add (ps, 0);
6865 }
6866
6867 void
6868 picosat_add_ado_lit (PS * ps, int external_lit)
6869 {
6870 #ifndef NADC
6871   Lit * internal_lit;
6872
6873   if (ps->measurealltimeinlib)
6874     enter (ps);
6875   else
6876     check_ready (ps);
6877
6878   if (ps->state != READY)
6879     reset_incremental_usage (ps);
6880
6881   ABORTIF (!ps->addingtoado && ps->ahead > ps->added,
6882            "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6883
6884   if (external_lit)
6885     {
6886       ps->addingtoado = 1;
6887       internal_lit = import_lit (external_lit, 1);
6888       add_lit (internal_lit);
6889     }
6890   else
6891     {
6892       ps->addingtoado = 0;
6893       add_ado (ps);
6894     }
6895   if (ps->measurealltimeinlib)
6896     leave (ps);
6897 #else
6898   (void) ps;
6899   (void) external_lit;
6900   ABORT ("compiled without all different constraint support");
6901 #endif
6902 }
6903
6904 static void
6905 assume (PS * ps, Lit * lit)
6906 {
6907   if (ps->alshead == ps->eoals)
6908     {
6909       assert (ps->alstail == ps->als);
6910       ENLARGE (ps->als, ps->alshead, ps->eoals);
6911       ps->alstail = ps->als;
6912     }
6913
6914   *ps->alshead++ = lit;
6915   LOG ( fprintf (ps->out, "%sassumption %d\n", ps->prefix, LIT2INT (lit)));
6916 }
6917
6918 static void
6919 assume_contexts (PS * ps)
6920 {
6921   Lit ** p;
6922   if (ps->als != ps->alshead)
6923     return;
6924   for (p = ps->CLS; p != ps->clshead; p++)
6925     assume (ps, *p);
6926 }
6927
6928 static const char * enumstr (int i) {
6929   int last = i % 10;
6930   if (last == 1) return "st";
6931   if (last == 2) return "nd";
6932   if (last == 3) return "rd";
6933   return "th";
6934 }
6935
6936 static int
6937 tderef (PS * ps, int int_lit)
6938 {
6939   Lit * lit;
6940   Var * v;
6941
6942   assert (abs (int_lit) <= (int) ps->max_var);
6943
6944   lit = int2lit (ps, int_lit);
6945
6946   v = LIT2VAR (lit);
6947   if (v->level > 0)
6948     return 0;
6949
6950   if (lit->val == TRUE)
6951     return 1;
6952
6953   if (lit->val == FALSE)
6954     return -1;
6955
6956   return 0;
6957 }
6958
6959 static int
6960 pderef (PS * ps, int int_lit)
6961 {
6962   Lit * lit;
6963   Var * v;
6964
6965   assert (abs (int_lit) <= (int) ps->max_var);
6966
6967   v = ps->vars + abs (int_lit);
6968   if (!v->partial)
6969     return 0;
6970
6971   lit = int2lit (ps, int_lit);
6972
6973   if (lit->val == TRUE)
6974     return 1;
6975
6976   if (lit->val == FALSE)
6977     return -1;
6978
6979   return 0;
6980 }
6981
6982 static void
6983 minautarky (PS * ps)
6984 {
6985   unsigned * occs, maxoccs, tmpoccs, npartial;
6986   int * p, * c, lit, best, val;
6987 #ifdef LOGGING
6988   int tl;
6989 #endif
6990
6991   assert (!ps->partial);
6992
6993   npartial = 0;
6994
6995   NEWN (occs, 2*ps->max_var + 1);
6996   CLRN (occs, 2*ps->max_var + 1);
6997   occs += ps->max_var;
6998   for (p = ps->soclauses; p < ps->sohead; p++)
6999     occs[*p]++;
7000   assert (occs[0] == ps->oadded);
7001
7002   for (c = ps->soclauses; c < ps->sohead; c = p + 1)
7003     {
7004 #ifdef LOGGING
7005       tl = 0;
7006 #endif
7007       best = 0;
7008       maxoccs = 0;
7009       for (p = c; (lit = *p); p++)
7010         {
7011           val = tderef (ps, lit);
7012           if (val < 0)
7013             continue;
7014           if (val > 0)
7015             {
7016 #ifdef LOGGING
7017               tl = 1;
7018 #endif
7019               best = lit;
7020               maxoccs = occs[lit];
7021             }
7022
7023           val = pderef (ps, lit);
7024           if (val > 0)
7025             break;
7026           if (val < 0)
7027             continue;
7028           val = int2lit (ps, lit)->val;
7029           assert (val);
7030           if (val < 0)
7031             continue;
7032           tmpoccs = occs[lit];
7033           if (best && tmpoccs <= maxoccs)
7034             continue;
7035           best = lit;
7036           maxoccs = tmpoccs;
7037         }
7038       if (!lit)
7039         {
7040           assert (best);
7041           LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n",
7042                ps->prefix, best, maxoccs, tl ? " (top)" : ""));
7043           ps->vars[abs (best)].partial = 1;
7044           npartial++;
7045         }
7046       for (p = c; (lit = *p); p++)
7047         {
7048           assert (occs[lit] > 0);
7049           occs[lit]--;
7050         }
7051     }
7052   occs -= ps->max_var;
7053   DELETEN (occs, 2*ps->max_var + 1);
7054   ps->partial = 1;
7055
7056   if (ps->verbosity)
7057      fprintf (ps->out,
7058       "%sautarky of size %u out of %u satisfying all clauses (%.1f%%)\n",
7059       ps->prefix, npartial, ps->max_var, PERCENT (npartial, ps->max_var));
7060 }
7061
7062 void
7063 picosat_assume (PS * ps, int int_lit)
7064 {
7065   Lit *lit;
7066
7067   if (ps->measurealltimeinlib)
7068     enter (ps);
7069   else
7070     check_ready (ps);
7071
7072   if (ps->state != READY)
7073     reset_incremental_usage (ps);
7074
7075   assume_contexts (ps);
7076   lit = import_lit (ps, int_lit, 1);
7077   assume (ps, lit);
7078
7079   if (ps->measurealltimeinlib)
7080     leave (ps);
7081 }
7082
7083 int
7084 picosat_sat (PS * ps, int l)
7085 {
7086   int res;
7087   char ch;
7088
7089   enter (ps);
7090
7091   ps->calls++;
7092   LOG ( fprintf (ps->out, "%sSTART call %u\n", ps->prefix, ps->calls));
7093
7094   if (ps->added < ps->ahead)
7095     {
7096 #ifndef NADC
7097       if (ps->addingtoado)
7098         ABORT ("API usage: incomplete all different constraint");
7099       else
7100 #endif
7101         ABORT ("API usage: incomplete clause");
7102     }
7103
7104   if (ps->state != READY)
7105     reset_incremental_usage (ps);
7106
7107   assume_contexts (ps);
7108
7109   res = sat (ps, l);
7110
7111   assert (ps->state == READY);
7112
7113   switch (res)
7114     {
7115     case PICOSAT_UNSATISFIABLE:
7116       ch = '0';
7117       ps->state = UNSAT;
7118       break;
7119     case PICOSAT_SATISFIABLE:
7120       ch = '1';
7121       ps->state = SAT;
7122       break;
7123     default:
7124       ch = '?';
7125       ps->state = UNKNOWN;
7126       break;
7127     }
7128
7129   if (ps->verbosity)
7130     {
7131       report (ps, 1, ch);
7132       rheader (ps);
7133     }
7134
7135   leave (ps);
7136   LOG ( fprintf (ps->out, "%sEND call %u result %d\n", ps->prefix, ps->calls, res));
7137
7138   ps->last_sat_call_result = res;
7139
7140   return res;
7141 }
7142
7143 int
7144 picosat_res (PS * ps)
7145 {
7146   return ps->last_sat_call_result;
7147 }
7148
7149 int
7150 picosat_deref (PS * ps, int int_lit)
7151 {
7152   Lit *lit;
7153
7154   check_ready (ps);
7155   check_sat_state (ps);
7156   ABORTIF (!int_lit, "API usage: can not deref zero literal");
7157   ABORTIF (ps->mtcls, "API usage: deref after empty clause generated");
7158
7159 #ifdef STATS
7160   ps->derefs++;
7161 #endif
7162
7163   if (abs (int_lit) > (int) ps->max_var)
7164     return 0;
7165
7166   lit = int2lit (ps, int_lit);
7167
7168   if (lit->val == TRUE)
7169     return 1;
7170
7171   if (lit->val == FALSE)
7172     return -1;
7173
7174   return 0;
7175 }
7176
7177 int
7178 picosat_deref_toplevel (PS * ps, int int_lit)
7179 {
7180   check_ready (ps);
7181   ABORTIF (!int_lit, "API usage: can not deref zero literal");
7182
7183 #ifdef STATS
7184   ps->derefs++;
7185 #endif
7186   if (abs (int_lit) > (int) ps->max_var)
7187     return 0;
7188
7189   return tderef (ps, int_lit);
7190 }
7191
7192 int
7193 picosat_inconsistent (PS * ps)
7194 {
7195   check_ready (ps);
7196   return ps->mtcls != 0;
7197 }
7198
7199 int
7200 picosat_corelit (PS * ps, int int_lit)
7201 {
7202   check_ready (ps);
7203   check_unsat_state (ps);
7204   ABORTIF (!int_lit, "API usage: zero literal can not be in core");
7205
7206   assert (ps->mtcls || ps->failed_assumption);
7207
7208 #ifdef TRACE
7209   {
7210     int res = 0;
7211     ABORTIF (!ps->trace, "tracing disabled");
7212     if (ps->measurealltimeinlib)
7213       enter (ps);
7214     core (ps);
7215     if (abs (int_lit) <= (int) ps->max_var)
7216       res = ps->vars[abs (int_lit)].core;
7217     assert (!res || ps->failed_assumption || ps->vars[abs (int_lit)].used);
7218     if (ps->measurealltimeinlib)
7219       leave (ps);
7220     return res;
7221   }
7222 #else
7223   ABORT ("compiled without trace support");
7224   return 0;
7225 #endif
7226 }
7227
7228 int
7229 picosat_coreclause (PS * ps, int ocls)
7230 {
7231   check_ready (ps);
7232   check_unsat_state (ps);
7233
7234   ABORTIF (ocls < 0, "API usage: negative original clause index");
7235   ABORTIF (ocls >= (int)ps->oadded, "API usage: original clause index exceeded");
7236
7237   assert (ps->mtcls || ps->failed_assumption);
7238
7239 #ifdef TRACE
7240   {
7241     Cls ** clsptr, * c;
7242     int res  = 0;
7243
7244     ABORTIF (!ps->trace, "tracing disabled");
7245     if (ps->measurealltimeinlib)
7246       enter (ps);
7247     core (ps);
7248     clsptr = ps->oclauses + ocls;
7249     assert (clsptr < ps->ohead);
7250     c = *clsptr;
7251     if (c)
7252       res = c->core;
7253     if (ps->measurealltimeinlib)
7254       leave (ps);
7255
7256     return res;
7257   }
7258 #else
7259   ABORT ("compiled without trace support");
7260   return 0;
7261 #endif
7262 }
7263
7264 int
7265 picosat_failed_assumption (PS * ps, int int_lit)
7266 {
7267   Lit * lit;
7268   Var * v;
7269   ABORTIF (!int_lit, "API usage: zero literal as assumption");
7270   check_ready (ps);
7271   check_unsat_state (ps);
7272   if (ps->mtcls)
7273     return 0;
7274   assert (ps->failed_assumption);
7275   if (abs (int_lit) > (int) ps->max_var)
7276     return 0;
7277   if (!ps->extracted_all_failed_assumptions)
7278     extract_all_failed_assumptions (ps);
7279   lit = import_lit (ps, int_lit, 1);
7280   v = LIT2VAR (lit);
7281   return v->failed;
7282 }
7283
7284 int
7285 picosat_failed_context (PS * ps, int int_lit)
7286 {
7287   Lit * lit;
7288   Var * v;
7289   ABORTIF (!int_lit, "API usage: zero literal as context");
7290   ABORTIF (abs (int_lit) > (int) ps->max_var, "API usage: invalid context");
7291   check_ready (ps);
7292   check_unsat_state (ps);
7293   assert (ps->failed_assumption);
7294   if (!ps->extracted_all_failed_assumptions)
7295     extract_all_failed_assumptions (ps);
7296   lit = import_lit (ps, int_lit, 0);
7297   v = LIT2VAR (lit);
7298   return v->failed;
7299 }
7300
7301 const int *
7302 picosat_failed_assumptions (PS * ps)
7303 {
7304   Lit ** p, * lit;
7305   Var * v;
7306   int ilit;
7307
7308   ps->falshead = ps->fals;
7309   check_ready (ps);
7310   check_unsat_state (ps);
7311   if (!ps->mtcls)
7312     {
7313       assert (ps->failed_assumption);
7314       if (!ps->extracted_all_failed_assumptions)
7315         extract_all_failed_assumptions (ps);
7316
7317       for (p = ps->als; p < ps->alshead; p++)
7318         {
7319           lit = *p;
7320           v = LIT2VAR (*p);
7321           if (!v->failed)
7322             continue;
7323           ilit = LIT2INT (lit);
7324           if (ps->falshead == ps->eofals)
7325             ENLARGE (ps->fals, ps->falshead, ps->eofals);
7326           *ps->falshead++ = ilit;
7327         }
7328     }
7329   if (ps->falshead == ps->eofals)
7330     ENLARGE (ps->fals, ps->falshead, ps->eofals);
7331   *ps->falshead++ = 0;
7332   return ps->fals;
7333 }
7334
7335 const int *
7336 picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fix)
7337 {
7338   int i, j, ilit, len, norig = ps->alshead - ps->als, nwork, * work, res;
7339   signed char * redundant;
7340   Lit ** p, * lit;
7341   int failed;
7342   Var * v;
7343 #ifndef NDEBUG
7344   int oldlen;
7345 #endif
7346
7347   check_ready (ps);
7348   check_unsat_state (ps);
7349   len = 0;
7350   if (!ps->mtcls)
7351     {
7352       assert (ps->failed_assumption);
7353       if (!ps->extracted_all_failed_assumptions)
7354         extract_all_failed_assumptions (ps);
7355
7356       for (p = ps->als; p < ps->alshead; p++)
7357         if (LIT2VAR (*p)->failed)
7358           len++;
7359     }
7360
7361   if (ps->mass)
7362     DELETEN (ps->mass, ps->szmass);
7363   ps->szmass = len + 1;
7364   NEWN (ps->mass, ps->szmass);
7365
7366   i = 0;
7367   for (p = ps->als; p < ps->alshead; p++)
7368     {
7369       lit = *p;
7370       v = LIT2VAR (lit);
7371       if (!v->failed)
7372         continue;
7373       ilit = LIT2INT (lit);
7374       assert (i < len);
7375       ps->mass[i++] = ilit;
7376     }
7377   assert (i == len);
7378   ps->mass[i] = 0;
7379   if (ps->verbosity)
7380      fprintf (ps->out,
7381       "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n",
7382       ps->prefix, len, norig, PERCENT (len, norig));
7383   if (cb)
7384     cb (s, ps->mass);
7385
7386   nwork = len;
7387   NEWN (work, nwork);
7388   for (i = 0; i < len; i++)
7389     work[i] = ps->mass[i];
7390
7391   NEWN (redundant, nwork);
7392   CLRN (redundant, nwork);
7393
7394   for (i = 0; i < nwork; i++)
7395     {
7396       if (redundant[i])
7397         continue;
7398
7399       if (ps->verbosity > 1)
7400          fprintf (ps->out,
7401                  "%strying to drop %d%s assumption %d\n",
7402                  ps->prefix, i, enumstr (i), work[i]);
7403       for (j = 0; j < nwork; j++)
7404         {
7405           if (i == j) continue;
7406           if (j < i && fix) continue;
7407           if (redundant[j]) continue;
7408           picosat_assume (ps, work[j]);
7409         }
7410
7411       res = picosat_sat (ps, -1);
7412       if (res == 10)
7413         {
7414           if (ps->verbosity > 1)
7415              fprintf (ps->out,
7416                      "%sfailed to drop %d%s assumption %d\n",
7417                      ps->prefix, i, enumstr (i), work[i]);
7418
7419           if (fix)
7420             {
7421               picosat_add (ps, work[i]);
7422               picosat_add (ps, 0);
7423             }
7424         }
7425       else
7426         {
7427           assert (res == 20);
7428           if (ps->verbosity > 1)
7429              fprintf (ps->out,
7430                      "%ssuceeded to drop %d%s assumption %d\n",
7431                      ps->prefix, i, enumstr (i), work[i]);
7432           redundant[i] = 1;
7433           for (j = 0; j < nwork; j++)
7434             {
7435               failed = picosat_failed_assumption (ps, work[j]);
7436               if (j <= i)
7437                 {
7438                   assert ((j < i && fix) || redundant[j] == !failed);
7439                   continue;
7440                 }
7441
7442               if (!failed)
7443                 {
7444                   redundant[j] = -1;
7445                   if (ps->verbosity > 1)
7446                      fprintf (ps->out,
7447                              "%salso suceeded to drop %d%s assumption %d\n",
7448                              ps->prefix, j, enumstr (j), work[j]);
7449                 }
7450             }
7451
7452 #ifndef NDEBUG
7453             oldlen = len;
7454 #endif
7455             len = 0;
7456             for (j = 0; j < nwork; j++)
7457               if (!redundant[j])
7458                 ps->mass[len++] = work[j];
7459             ps->mass[len] = 0;
7460             assert (len < oldlen);
7461
7462             if (fix)
7463               {
7464                 picosat_add (ps, -work[i]);
7465                 picosat_add (ps, 0);
7466               }
7467
7468 #ifndef NDEBUG
7469             for (j = 0; j <= i; j++)
7470               assert (redundant[j] >= 0);
7471 #endif
7472             for (j = i + 1; j < nwork; j++)
7473               {
7474                 if (redundant[j] >= 0)
7475                   continue;
7476
7477                 if (fix)
7478                   {
7479                     picosat_add (ps, -work[j]);
7480                     picosat_add (ps, 0);
7481                   }
7482
7483                 redundant[j] = 1;
7484               }
7485
7486             if (ps->verbosity)
7487                fprintf (ps->out,
7488         "%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n",
7489                 ps->prefix, len, norig, PERCENT (len, norig));
7490             if (cb)
7491               cb (s, ps->mass);
7492         }
7493     }
7494
7495   DELETEN (work, nwork);
7496   DELETEN (redundant, nwork);
7497
7498   if (ps->verbosity)
7499     {
7500        fprintf (ps->out, "%sreinitializing unsat state\n", ps->prefix);
7501       fflush (ps->out);
7502     }
7503
7504   for (i = 0; i < len; i++)
7505     picosat_assume (ps, ps->mass[i]);
7506
7507 #ifndef NDEBUG
7508   res =
7509 #endif
7510   picosat_sat (ps, -1);
7511   assert (res == 20);
7512
7513   if (!ps->mtcls)
7514     {
7515       assert (!ps->extracted_all_failed_assumptions);
7516       extract_all_failed_assumptions (ps);
7517     }
7518
7519   return ps->mass;
7520 }
7521
7522 static const int *
7523 mss (PS * ps, int * a, int size)
7524 {
7525   int i, j, k, res;
7526
7527   assert (!ps->mtcls);
7528
7529   if (ps->szmssass)
7530     DELETEN (ps->mssass, ps->szmssass);
7531
7532   ps->szmssass = 0;
7533   ps->mssass = 0;
7534
7535   ps->szmssass = size + 1;
7536   NEWN (ps->mssass, ps->szmssass);
7537
7538   LOG ( fprintf (ps->out, "%ssearch MSS over %d assumptions\n", ps->prefix, size));
7539
7540   k = 0;
7541   for (i = k; i < size; i++)
7542     {
7543       for (j = 0; j < k; j++)
7544         picosat_assume (ps, ps->mssass[j]);
7545
7546       LOG ( fprintf (ps->out,
7547              "%strying to add assumption %d to MSS : %d\n",
7548              ps->prefix, i, a[i]));
7549
7550       picosat_assume (ps, a[i]);
7551
7552       res = picosat_sat (ps, -1);
7553       if (res == 10)
7554         {
7555           LOG ( fprintf (ps->out,
7556                  "%sadding assumption %d to MSS : %d\n", ps->prefix, i, a[i]));
7557
7558           ps->mssass[k++] = a[i];
7559
7560           for (j = i + 1; j < size; j++)
7561             {
7562               if (picosat_deref (ps, a[j]) <= 0)
7563                 continue;
7564
7565               LOG ( fprintf (ps->out,
7566                      "%salso adding assumption %d to MSS : %d\n",
7567                      ps->prefix, j, a[j]));
7568
7569               ps->mssass[k++] = a[j];
7570
7571               if (++i != j)
7572                 {
7573                   int tmp = a[i];
7574                   a[i] = a[j];
7575                   a[j] = tmp;
7576                 }
7577             }
7578         }
7579       else
7580         {
7581           assert (res == 20);
7582
7583           LOG ( fprintf (ps->out,
7584                  "%signoring assumption %d in MSS : %d\n", ps->prefix, i, a[i]));
7585         }
7586     }
7587   ps->mssass[k] = 0;
7588   LOG ( fprintf (ps->out, "%sfound MSS of size %d\n", ps->prefix, k));
7589
7590   return ps->mssass;
7591 }
7592
7593 static void
7594 reassume (PS * ps, const int * a, int size)
7595 {
7596   int i;
7597   LOG ( fprintf (ps->out, "%sreassuming all assumptions\n", ps->prefix));
7598   for (i = 0; i < size; i++)
7599     picosat_assume (ps, a[i]);
7600 }
7601
7602 const int *
7603 picosat_maximal_satisfiable_subset_of_assumptions (PS * ps)
7604 {
7605   const int * res;
7606   int i, *a, size;
7607
7608   ABORTIF (ps->mtcls,
7609            "API usage: CNF inconsistent (use 'picosat_inconsistent')");
7610
7611   enter (ps);
7612
7613   size = ps->alshead - ps->als;
7614   NEWN (a, size);
7615
7616   for (i = 0; i < size; i++)
7617     a[i] = LIT2INT (ps->als[i]);
7618
7619   res = mss (ps, a, size);
7620   reassume (ps, a, size);
7621
7622   DELETEN (a, size);
7623
7624   leave (ps);
7625
7626   return res;
7627 }
7628
7629 static void
7630 check_mss_flags_clean (PS * ps)
7631 {
7632 #ifndef NDEBUG
7633   unsigned i;
7634   for (i = 1; i <= ps->max_var; i++)
7635     {
7636       assert (!ps->vars[i].msspos);
7637       assert (!ps->vars[i].mssneg);
7638     }
7639 #else
7640   (void) ps;
7641 #endif
7642 }
7643
7644 static void
7645 push_mcsass (PS * ps, int lit)
7646 {
7647   if (ps->nmcsass == ps->szmcsass)
7648     {
7649       ps->szmcsass = ps->szmcsass ? 2*ps->szmcsass : 1;
7650       RESIZEN (ps->mcsass, ps->nmcsass, ps->szmcsass);
7651     }
7652
7653   ps->mcsass[ps->nmcsass++] = lit;
7654 }
7655
7656 static const int *
7657 next_mss (PS * ps, int mcs)
7658 {
7659   int i, *a, size, mssize, mcsize, lit, inmss;
7660   const int * res, * p;
7661   Var * v;
7662
7663   if (ps->mtcls) return 0;
7664
7665   check_mss_flags_clean (ps);
7666
7667   if (mcs && ps->mcsass)
7668     {
7669       DELETEN (ps->mcsass, ps->szmcsass);
7670       ps->nmcsass = ps->szmcsass = 0;
7671       ps->mcsass = 0;
7672     }
7673
7674   size = ps->alshead - ps->als;
7675   NEWN (a, size);
7676
7677   for (i = 0; i < size; i++)
7678     a[i] = LIT2INT (ps->als[i]);
7679
7680   (void) picosat_sat (ps, -1);
7681
7682   //TODO short cut for 'picosat_res () == 10'?
7683
7684   if (ps->mtcls)
7685     {
7686       assert (picosat_res (ps) == 20);
7687       res = 0;
7688       goto DONE;
7689     }
7690
7691   res = mss (ps, a, size);
7692
7693   if (ps->mtcls)
7694     {
7695       res = 0;
7696       goto DONE;
7697     }
7698
7699   for (p = res; (lit = *p); p++)
7700     {
7701       v = ps->vars + abs (lit);
7702       if (lit < 0)
7703         {
7704           assert (!v->msspos);
7705           v->mssneg = 1;
7706         }
7707       else
7708         {
7709           assert (!v->mssneg);
7710           v->msspos = 1;
7711         }
7712     }
7713
7714   mssize = p - res;
7715   mcsize = INT_MIN;
7716
7717   for (i = 0; i < size; i++)
7718     {
7719       lit = a[i];
7720       v = ps->vars + abs (lit);
7721       if (lit > 0 && v->msspos)
7722         inmss = 1;
7723       else if (lit < 0 && v->mssneg)
7724         inmss = 1;
7725       else
7726         inmss = 0;
7727
7728       if (mssize < mcsize)
7729         {
7730           if (inmss)
7731             picosat_add (ps, -lit);
7732         }
7733       else
7734         {
7735           if (!inmss)
7736             picosat_add (ps, lit);
7737         }
7738
7739       if (!inmss && mcs)
7740         push_mcsass (ps, lit);
7741     }
7742   picosat_add (ps, 0);
7743   if (mcs)
7744     push_mcsass (ps, 0);
7745
7746   for (i = 0; i < size; i++)
7747     {
7748       lit = a[i];
7749       v = ps->vars + abs (lit);
7750       v->msspos = 0;
7751       v->mssneg = 0;
7752     }
7753
7754 DONE:
7755
7756   reassume (ps, a, size);
7757   DELETEN (a, size);
7758
7759   return res;
7760 }
7761
7762 const int *
7763 picosat_next_maximal_satisfiable_subset_of_assumptions (PS * ps)
7764 {
7765   const int * res;
7766   enter (ps);
7767   res = next_mss (ps, 0);
7768   leave (ps);
7769   return  res;
7770 }
7771
7772 const int *
7773 picosat_next_minimal_correcting_subset_of_assumptions (PS * ps)
7774 {
7775   const int * res, * tmp;
7776   enter (ps);
7777   tmp = next_mss (ps, 1);
7778   res = tmp ? ps->mcsass : 0;
7779   leave (ps);
7780   return res;
7781 }
7782
7783 const int *
7784 picosat_humus (PS * ps,
7785                void (*callback)(void*state,int nmcs,int nhumus),
7786                void * state)
7787 {
7788   int lit, nmcs, j, nhumus;
7789   const int * mcs, * p;
7790   unsigned i;
7791   Var * v;
7792   enter (ps);
7793 #ifndef NDEBUG
7794   for (i = 1; i <= ps->max_var; i++)
7795     {
7796       v = ps->vars + i;
7797       assert (!v->humuspos);
7798       assert (!v->humusneg);
7799     }
7800 #endif
7801   nhumus = nmcs = 0;
7802   while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps)))
7803     {
7804       for (p = mcs; (lit = *p); p++)
7805         {
7806           v = ps->vars + abs (lit);
7807           if (lit < 0)
7808             {
7809               if (!v->humusneg)
7810                 {
7811                   v->humusneg = 1;
7812                   nhumus++;
7813                 }
7814             }
7815           else
7816             {
7817               if (!v->humuspos)
7818                 {
7819                   v->humuspos = 1;
7820                   nhumus++;
7821                 }
7822             }
7823         }
7824       nmcs++;
7825       LOG ( fprintf (ps->out,
7826              "%smcs %d of size %d humus %d\n",
7827              ps->prefix, nmcs, (int)(p - mcs), nhumus));
7828       if (callback)
7829         callback (state, nmcs, nhumus);
7830     }
7831   assert (!ps->szhumus);
7832   ps->szhumus = 1;
7833   for (i = 1; i <= ps->max_var; i++)
7834     {
7835       v = ps->vars + i;
7836       if (v->humuspos)
7837         ps->szhumus++;
7838       if (v->humusneg)
7839         ps->szhumus++;
7840     }
7841   assert (nhumus + 1 == ps->szhumus);
7842   NEWN (ps->humus, ps->szhumus);
7843   j = 0;
7844   for (i = 1; i <= ps->max_var; i++)
7845     {
7846       v = ps->vars + i;
7847       if (v->humuspos)
7848         {
7849           assert (j < nhumus);
7850           ps->humus[j++] = (int) i;
7851         }
7852       if (v->humusneg)
7853         {
7854           assert (j < nhumus);
7855           assert (i < INT_MAX);
7856           ps->humus[j++] = - (int) i;
7857         }
7858     }
7859   assert (j == nhumus);
7860   assert (j < ps->szhumus);
7861   ps->humus[j] = 0;
7862   leave (ps);
7863   return ps->humus;
7864 }
7865
7866 int
7867 picosat_usedlit (PS * ps, int int_lit)
7868 {
7869   int res;
7870   check_ready (ps);
7871   check_sat_or_unsat_or_unknown_state (ps);
7872   ABORTIF (!int_lit, "API usage: zero literal can not be used");
7873   int_lit = abs (int_lit);
7874   res = (int_lit <= (int) ps->max_var) ? ps->vars[int_lit].used : 0;
7875   return res;
7876 }
7877
7878 void
7879 picosat_write_clausal_core (PS * ps, FILE * file)
7880 {
7881   check_trace_support_and_execute (ps, file, write_core_wrapper, 0);
7882 }
7883
7884 void
7885 picosat_write_compact_trace (PS * ps, FILE * file)
7886 {
7887   check_trace_support_and_execute (ps, file, write_trace,
7888                                    COMPACT_TRACECHECK_TRACE_FMT);
7889 }
7890
7891 void
7892 picosat_write_extended_trace (PS * ps, FILE * file)
7893 {
7894   check_trace_support_and_execute (ps, file, write_trace,
7895                                    EXTENDED_TRACECHECK_TRACE_FMT);
7896 }
7897
7898 void
7899 picosat_write_rup_trace (PS * ps, FILE * file)
7900 {
7901   check_trace_support_and_execute (ps, file, write_trace, RUP_TRACE_FMT);
7902 }
7903
7904 size_t
7905 picosat_max_bytes_allocated (PS * ps)
7906 {
7907   check_ready (ps);
7908   return ps->max_bytes;
7909 }
7910
7911 void
7912 picosat_set_propagation_limit (PS * ps, unsigned long long l)
7913 {
7914   ps->lpropagations = l;
7915 }
7916
7917 unsigned long long
7918 picosat_propagations (PS * ps)
7919 {
7920   return ps->propagations;
7921 }
7922
7923 unsigned long long
7924 picosat_visits (PS * ps)
7925 {
7926   return ps->visits;
7927 }
7928
7929 unsigned long long
7930 picosat_decisions (PS * ps)
7931 {
7932   return ps->decisions;
7933 }
7934
7935 int
7936 picosat_variables (PS * ps)
7937 {
7938   check_ready (ps);
7939   return (int) ps->max_var;
7940 }
7941
7942 int
7943 picosat_added_original_clauses (PS * ps)
7944 {
7945   check_ready (ps);
7946   return (int) ps->oadded;
7947 }
7948
7949 void
7950 picosat_stats (PS * ps)
7951 {
7952   unsigned redlits;
7953 #ifdef STATS
7954   check_ready (ps);
7955   assert (ps->sdecisions + ps->rdecisions + ps->assumptions == ps->decisions);
7956 #endif
7957   if (ps->calls > 1)
7958      fprintf (ps->out, "%s%u calls\n", ps->prefix, ps->calls);
7959   if (ps->contexts)
7960     {
7961        fprintf (ps->out, "%s%u contexts", ps->prefix, ps->contexts);
7962 #ifdef STATS
7963        fprintf (ps->out, " %u internal variables", ps->internals);
7964 #endif
7965        fprintf (ps->out, "\n");
7966     }
7967    fprintf (ps->out, "%s%u iterations\n", ps->prefix, ps->iterations);
7968    fprintf (ps->out, "%s%u restarts", ps->prefix, ps->restarts);
7969 #ifdef STATS
7970    fprintf (ps->out, " (%u skipped)", ps->skippedrestarts);
7971 #endif
7972   fputc ('\n', ps->out);
7973 #ifndef NFL
7974    fprintf (ps->out, "%s%u failed literals", ps->prefix, ps->failedlits);
7975 #ifdef STATS
7976    fprintf (ps->out,
7977            ", %u calls, %u rounds, %llu propagations",
7978            ps->flcalls, ps->flrounds, ps->flprops);
7979 #endif
7980   fputc ('\n', ps->out);
7981 #ifdef STATS
7982    fprintf (ps->out,
7983     "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n",
7984     ps->prefix,
7985     ps->ifailedlits, PERCENT (ps->ifailedlits, ps->failedlits),
7986     ps->floopsed, ps->fltried, ps->flskipped);
7987 #endif
7988 #endif
7989    fprintf (ps->out, "%s%u conflicts", ps->prefix, ps->conflicts);
7990 #ifdef STATS
7991    fprintf (ps->out, " (%u uips = %.1f%%)\n", ps->uips, PERCENT(ps->uips,ps->conflicts));
7992 #else
7993   fputc ('\n', ps->out);
7994 #endif
7995 #ifndef NADC
7996    fprintf (ps->out, "%s%u adc conflicts\n", ps->prefix, ps->adoconflicts);
7997 #endif
7998 #ifdef STATS
7999    fprintf (ps->out, "%s%llu dereferenced literals\n", ps->prefix, ps->derefs);
8000 #endif
8001    fprintf (ps->out, "%s%u decisions", ps->prefix, ps->decisions);
8002 #ifdef STATS
8003    fprintf (ps->out, " (%u random = %.2f%%",
8004            ps->rdecisions, PERCENT (ps->rdecisions, ps->decisions));
8005    fprintf (ps->out, ", %u assumptions", ps->assumptions);
8006   fputc (')', ps->out);
8007 #endif
8008   fputc ('\n', ps->out);
8009 #ifdef STATS
8010    fprintf (ps->out,
8011            "%s%u static phase decisions (%.1f%% of all variables)\n",
8012            ps->prefix,
8013            ps->staticphasedecisions, PERCENT (ps->staticphasedecisions, ps->max_var));
8014 #endif
8015    fprintf (ps->out, "%s%u fixed variables\n", ps->prefix, ps->fixed);
8016   assert (ps->nonminimizedllits >= ps->minimizedllits);
8017   redlits = ps->nonminimizedllits - ps->minimizedllits;
8018    fprintf (ps->out, "%s%u learned literals\n", ps->prefix, ps->llitsadded);
8019    fprintf (ps->out, "%s%.1f%% deleted literals\n",
8020      ps->prefix, PERCENT (redlits, ps->nonminimizedllits));
8021
8022 #ifdef STATS
8023 #ifdef TRACE
8024    fprintf (ps->out,
8025            "%s%llu antecedents (%.1f antecedents per clause",
8026            ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts));
8027   if (ps->trace)
8028      fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents));
8029   fputs (")\n", ps->out);
8030 #endif
8031
8032    fprintf (ps->out, "%s%llu propagations (%.1f propagations per decision)\n",
8033            ps->prefix, ps->propagations, AVERAGE (ps->propagations, ps->decisions));
8034    fprintf (ps->out, "%s%llu visits (%.1f per propagation)\n",
8035            ps->prefix, ps->visits, AVERAGE (ps->visits, ps->propagations));
8036    fprintf (ps->out,
8037            "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n",
8038            ps->prefix, ps->bvisits,
8039            PERCENT (ps->bvisits, ps->visits),
8040            AVERAGE (ps->bvisits, ps->propagations));
8041    fprintf (ps->out,
8042            "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n",
8043            ps->prefix, ps->tvisits,
8044            PERCENT (ps->tvisits, ps->visits),
8045            AVERAGE (ps->tvisits, ps->propagations));
8046    fprintf (ps->out,
8047            "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n",
8048            ps->prefix, ps->lvisits,
8049            PERCENT (ps->lvisits, ps->visits),
8050            AVERAGE (ps->lvisits, ps->propagations));
8051    fprintf (ps->out, "%s%llu other true (%.1f%% of visited clauses)\n",
8052            ps->prefix, ps->othertrue, PERCENT (ps->othertrue, ps->visits));
8053    fprintf (ps->out,
8054            "%s%llu other true in binary clauses (%.1f%%)"
8055            ", %llu upper (%.1f%%)\n",
8056            ps->prefix, ps->othertrue2, PERCENT (ps->othertrue2, ps->othertrue),
8057            ps->othertrue2u, PERCENT (ps->othertrue2u, ps->othertrue2));
8058    fprintf (ps->out,
8059            "%s%llu other true in large clauses (%.1f%%)"
8060            ", %llu upper (%.1f%%)\n",
8061            ps->prefix, ps->othertruel, PERCENT (ps->othertruel, ps->othertrue),
8062            ps->othertruelu, PERCENT (ps->othertruelu, ps->othertruel));
8063    fprintf (ps->out, "%s%llu ternary and large traversals (%.1f per visit)\n",
8064            ps->prefix, ps->traversals, AVERAGE (ps->traversals, ps->visits));
8065    fprintf (ps->out, "%s%llu large traversals (%.1f per large visit)\n",
8066            ps->prefix, ps->ltraversals, AVERAGE (ps->ltraversals, ps->lvisits));
8067    fprintf (ps->out, "%s%llu assignments\n", ps->prefix, ps->assignments);
8068 #else
8069    fprintf (ps->out, "%s%llu propagations\n", ps->prefix, picosat_propagations (ps));
8070    fprintf (ps->out, "%s%llu visits\n", ps->prefix, picosat_visits (ps));
8071 #endif
8072    fprintf (ps->out, "%s%.1f%% variables used\n", ps->prefix, PERCENT (ps->vused, ps->max_var));
8073
8074   sflush (ps);
8075    fprintf (ps->out, "%s%.1f seconds in library\n", ps->prefix, ps->seconds);
8076    fprintf (ps->out, "%s%.1f megaprops/second\n",
8077            ps->prefix, AVERAGE (ps->propagations / 1e6f, ps->seconds));
8078    fprintf (ps->out, "%s%.1f megavisits/second\n",
8079            ps->prefix, AVERAGE (ps->visits / 1e6f, ps->seconds));
8080    fprintf (ps->out, "%sprobing %.1f seconds %.0f%%\n",
8081            ps->prefix, ps->flseconds, PERCENT (ps->flseconds, ps->seconds));
8082 #ifdef STATS
8083    fprintf (ps->out,
8084            "%srecycled %.1f MB in %u reductions\n",
8085            ps->prefix, ps->rrecycled / (double) (1 << 20), ps->reductions);
8086    fprintf (ps->out,
8087            "%srecycled %.1f MB in %u simplifications\n",
8088            ps->prefix, ps->srecycled / (double) (1 << 20), ps->simps);
8089 #else
8090    fprintf (ps->out, "%s%u simplifications\n", ps->prefix, ps->simps);
8091    fprintf (ps->out, "%s%u reductions\n", ps->prefix, ps->reductions);
8092    fprintf (ps->out, "%s%.1f MB recycled\n", ps->prefix, ps->recycled / (double) (1 << 20));
8093 #endif
8094    fprintf (ps->out, "%s%.1f MB maximally allocated\n",
8095             ps->prefix, picosat_max_bytes_allocated (ps) / (double) (1 << 20));
8096 }
8097
8098 #ifndef NGETRUSAGE
8099 #include <sys/time.h>
8100 #include <sys/resource.h>
8101 #include <sys/unistd.h>
8102 #endif
8103
8104 double
8105 picosat_time_stamp (void)
8106 {
8107   double res = -1;
8108 #ifndef NGETRUSAGE
8109   struct rusage u;
8110   res = 0;
8111   if (!getrusage (RUSAGE_SELF, &u))
8112     {
8113       res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec;
8114       res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec;
8115     }
8116 #endif
8117   return res;
8118 }
8119
8120 double
8121 picosat_seconds (PS * ps)
8122 {
8123   check_ready (ps);
8124   return ps->seconds;
8125 }
8126
8127 void
8128 picosat_print (PS * ps, FILE * file)
8129 {
8130 #ifdef NO_BINARY_CLAUSES
8131   Lit * lit, *other, * last;
8132   Ltk * stack;
8133 #endif
8134   Lit **q, **eol;
8135   Cls **p, *c;
8136   unsigned n;
8137
8138   if (ps->measurealltimeinlib)
8139     enter (ps);
8140   else
8141     check_ready (ps);
8142
8143   n = 0;
8144   n +=  ps->alshead - ps->als;
8145
8146   for (p = SOC; p != EOC; p = NXC (p))
8147     {
8148       c = *p;
8149
8150       if (!c)
8151         continue;
8152
8153 #ifdef TRACE
8154       if (c->collected)
8155         continue;
8156 #endif
8157       n++;
8158     }
8159
8160 #ifdef NO_BINARY_CLAUSES
8161   last = int2lit (ps, -ps->max_var);
8162   for (lit = int2lit (ps, 1); lit <= last; lit++)
8163     {
8164       stack = LIT2IMPLS (lit);
8165       eol = stack->start + stack->count;
8166       for (q = stack->start; q < eol; q++)
8167         if (*q >= lit)
8168           n++;
8169     }
8170 #endif
8171
8172   fprintf (file, "p cnf %d %u\n", ps->max_var, n);
8173
8174   for (p = SOC; p != EOC; p = NXC (p))
8175     {
8176       c = *p;
8177       if (!c)
8178         continue;
8179
8180 #ifdef TRACE
8181       if (c->collected)
8182         continue;
8183 #endif
8184
8185       eol = end_of_lits (c);
8186       for (q = c->lits; q < eol; q++)
8187         fprintf (file, "%d ", LIT2INT (*q));
8188
8189       fputs ("0\n", file);
8190     }
8191
8192 #ifdef NO_BINARY_CLAUSES
8193   last = int2lit (ps, -ps->max_var);
8194   for (lit = int2lit (ps, 1); lit <= last; lit++)
8195     {
8196       stack = LIT2IMPLS (lit);
8197       eol = stack->start + stack->count;
8198       for (q = stack->start; q < eol; q++)
8199         if ((other = *q) >= lit)
8200           fprintf (file, "%d %d 0\n", LIT2INT (lit), LIT2INT (other));
8201     }
8202 #endif
8203
8204   {
8205     Lit **r;
8206     for (r = ps->als; r < ps->alshead; r++)
8207       fprintf (file, "%d 0\n", LIT2INT (*r));
8208   }
8209
8210   fflush (file);
8211
8212   if (ps->measurealltimeinlib)
8213     leave (ps);
8214 }
8215
8216 void
8217 picosat_enter (PS * ps)
8218 {
8219   enter (ps);
8220 }
8221
8222 void
8223 picosat_leave (PS * ps)
8224 {
8225   leave (ps);
8226 }
8227
8228 void
8229 picosat_message (PS * ps, int vlevel, const char * fmt, ...)
8230 {
8231   va_list ap;
8232
8233   if (vlevel > ps->verbosity)
8234     return;
8235
8236   fputs (ps->prefix, ps->out);
8237   va_start (ap, fmt);
8238   vfprintf (ps->out, fmt, ap);
8239   va_end (ap);
8240   fputc ('\n', ps->out);
8241 }
8242
8243 int
8244 picosat_changed (PS * ps)
8245 {
8246   int res;
8247
8248   check_ready (ps);
8249   check_sat_state (ps);
8250
8251   res = (ps->min_flipped <= ps->saved_max_var);
8252   assert (!res || ps->saved_flips != ps->flips);
8253
8254   return res;
8255 }
8256
8257 void
8258 picosat_reset_phases (PS * ps)
8259 {
8260   rebias (ps);
8261 }
8262
8263 void
8264 picosat_reset_scores (PS * ps)
8265 {
8266   Rnk * r;
8267   ps->hhead = ps->heap + 1;
8268   for (r = ps->rnks + 1; r <= ps->rnks + ps->max_var; r++)
8269     {
8270       CLR (r);
8271       hpush (ps, r);
8272     }
8273 }
8274
8275 void
8276 picosat_remove_learned (PS * ps, unsigned percentage)
8277 {
8278   enter (ps);
8279   reset_incremental_usage (ps);
8280   reduce (ps, percentage);
8281   leave (ps);
8282 }
8283
8284 void
8285 picosat_set_global_default_phase (PS * ps, int phase)
8286 {
8287   check_ready (ps);
8288   ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' "
8289                       "with negative argument");
8290   ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' "
8291                       "with argument > 3");
8292   ps->defaultphase = phase;
8293 }
8294
8295 void
8296 picosat_set_default_phase_lit (PS * ps, int int_lit, int phase)
8297 {
8298   unsigned newphase;
8299   Lit * lit;
8300   Var * v;
8301
8302   check_ready (ps);
8303
8304   lit = import_lit (ps, int_lit, 1);
8305   v = LIT2VAR (lit);
8306
8307   if (phase)
8308     {
8309       newphase = (int_lit < 0) == (phase < 0);
8310       v->defphase = v->phase = newphase;
8311       v->usedefphase = v->assigned = 1;
8312     }
8313   else
8314     {
8315       v->usedefphase = v->assigned = 0;
8316     }
8317 }
8318
8319 void
8320 picosat_set_more_important_lit (PS * ps, int int_lit)
8321 {
8322   Lit * lit;
8323   Var * v;
8324   Rnk * r;
8325
8326   check_ready (ps);
8327
8328   lit = import_lit (ps, int_lit, 1);
8329   v = LIT2VAR (lit);
8330   r = VAR2RNK (v);
8331
8332   ABORTIF (r->lessimportant, "can not mark variable more and less important");
8333
8334   if (r->moreimportant)
8335     return;
8336
8337   r->moreimportant = 1;
8338
8339   if (r->pos)
8340     hup (ps, r);
8341 }
8342
8343 void
8344 picosat_set_less_important_lit (PS * ps, int int_lit)
8345 {
8346   Lit * lit;
8347   Var * v;
8348   Rnk * r;
8349
8350   check_ready (ps);
8351
8352   lit = import_lit (ps, int_lit, 1);
8353   v = LIT2VAR (lit);
8354   r = VAR2RNK (v);
8355
8356   ABORTIF (r->moreimportant, "can not mark variable more and less important");
8357
8358   if (r->lessimportant)
8359     return;
8360
8361   r->lessimportant = 1;
8362
8363   if (r->pos)
8364     hdown (ps, r);
8365 }
8366
8367 #ifndef NADC
8368
8369 unsigned
8370 picosat_ado_conflicts (PS * ps)
8371 {
8372   check_ready (ps);
8373   return ps->adoconflicts;
8374 }
8375
8376 void
8377 picosat_disable_ado (PS * ps)
8378 {
8379   check_ready (ps);
8380   assert (!ps->adodisabled);
8381   ps->adodisabled = 1;
8382 }
8383
8384 void
8385 picosat_enable_ado (PS * ps)
8386 {
8387   check_ready (ps);
8388   assert (ps->adodisabled);
8389   ps->adodisabled = 0;
8390 }
8391
8392 void
8393 picosat_set_ado_conflict_limit (unsigned newadoconflictlimit)
8394 {
8395   check_ready (ps);
8396   ps->adoconflictlimit = newadoconflictlimit;
8397 }
8398
8399 #endif
8400
8401 void
8402 picosat_simplify (PS * ps)
8403 {
8404   enter (ps);
8405   reset_incremental_usage (ps);
8406   simplify (ps, 1);
8407   leave (ps);
8408 }
8409
8410 int
8411 picosat_haveados (void)
8412 {
8413 #ifndef NADC
8414   return 1;
8415 #else
8416   return 0;
8417 #endif
8418 }
8419
8420 void
8421 picosat_save_original_clauses (PS * ps)
8422 {
8423   if (ps->saveorig) return;
8424   ABORTIF (ps->oadded, "API usage: 'picosat_save_original_clauses' too late");
8425   ps->saveorig = 1;
8426 }
8427
8428 int
8429 picosat_deref_partial (PS * ps, int int_lit)
8430 {
8431   check_ready (ps);
8432   check_sat_state (ps);
8433   ABORTIF (!int_lit, "API usage: can not partial deref zero literal");
8434   ABORTIF (ps->mtcls, "API usage: deref partial after empty clause generated");
8435   ABORTIF (!ps->saveorig, "API usage: 'picosat_save_original_clauses' missing");
8436
8437 #ifdef STATS
8438   ps->derefs++;
8439 #endif
8440
8441   if (!ps->partial)
8442     minautarky (ps);
8443
8444   return pderef (ps, int_lit);
8445 }