backends/picosat/picosat.c

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