lingeling/code/lglib.c

   1 /*-------------------------------------------------------------------------*/
   2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
   3 /*-------------------------------------------------------------------------*/
   4
   5 #include "lglib.h"
   6
   7 /*-------------------------------------------------------------------------*/
   8
   9 #include <assert.h>
  10 #include <ctype.h>
  11 #include <limits.h>
  12 #include <math.h>
  13 #include <stdarg.h>
  14 #include <stdint.h>
  15 #include <stdio.h>
  16 #include <stdlib.h>
  17 #include <string.h>
  18 #include <sys/resource.h>
  19 #include <sys/time.h>
  20 #include <unistd.h>
  21
  22 /*-------------------------------------------------------------------------*/
  23
  24 #ifndef NLGLPICOSAT
  25 #include "picosat.h"
  26 #endif
  27
  28 #ifndef NLGLYALSAT
  29 #include "yals.h"
  30 #endif
  31
  32 #ifndef NLGLDRUPLIG
  33 #include "druplig.h"
  34 #endif
  35
  36 /*-------------------------------------------------------------------------*/
  37
  38 #define REMOVED         INT_MAX
  39 #define NOTALIT         ((INT_MAX >> RMSHFT))
  40 #define MAXVAR          ((INT_MAX >> RMSHFT) - 2)
  41
  42 #define GLUESHFT        4
  43 #define POW2GLUE        (1 << GLUESHFT)
  44 #define MAXGLUE         (POW2GLUE - 1)
  45 #define GLUEMASK        (POW2GLUE - 1)
  46 #define MAXREDLIDX      ((1 << (31 - GLUESHFT)) - 2)
  47 #define MAXIRRLIDX      ((1 << (31 - RMSHFT)) - 2)
  48
  49 #define MAXLDFW         31
  50 #define REPMOD          22
  51
  52 #define FUNVAR          10
  53 #define FUNQUADS        (1<<(FUNVAR - 6))
  54 #define FALSECNF        (1ll<<32)
  55 #define TRUECNF         0ll
  56
  57 #define FLTPRC          32
  58 #define EXPMIN          (0x0000 ## 0000)
  59 #define EXPZRO          (0x1000 ## 0000)
  60 #define EXPMAX          (0x7fff ## ffff)
  61 #define MNTBIT          (0x0000 ## 0001 ## 0000 ## 0000 ## ull)
  62 #define MNTMAX          (0x0000 ## 0001 ## ffff ## ffff ## ull)
  63 #define FLTMIN          (0x0000 ## 0000 ## 0000 ## 0000 ## ll)
  64 #define FLTMAX          (0x7fff ## ffff ## ffff ## ffff ## ll)
  65
  66 #define LGL_SCORE_AVG           4
  67 #define LGL_SCORE_EVSIDS        5
  68 #define LGL_SCORE_VSIDS256      6
  69 #define LGL_SCORE_FAVG          7
  70
  71 #ifdef NDBLSCR
  72 #define MAXSCOREXP      (1<<30)
  73 #else
  74 #define MAXSCOREXP      (1<<9)
  75 #endif
  76
  77 #define DEFSCOREXP      500
  78
  79 #define LLMAX           FLTMAX
  80
  81 #define MAXFLTSTR       6
  82 #define MAXPHN          10
  83
  84 /*------------------------------------------------------------------------*/
  85 #ifndef NLGLOG
  86 /*------------------------------------------------------------------------*/
  87
  88 #define MAPLOGLEVEL(LEVEL) (LEVEL)
  89
  90 #define LOG(LEVEL,FMT,ARGS...) \
  91 do { \
  92   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
  93   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
  94   lglogend (lgl); \
  95 } while (0)
  96
  97 #define LOGCLS(LEVEL,CLS,FMT,ARGS...) \
  98 do { \
  99   const int * P; \
 100   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 101   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
 102   for (P = (CLS); *P; P++) fprintf (lgl->out, " %d", *P); \
 103   lglogend (lgl); \
 104 } while (0)
 105
 106 #define LOGMCLS(LEVEL,CLS,FMT,ARGS...) \
 107 do { \
 108   const int * P; \
 109   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 110   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
 111   for (P = (CLS); *P; P++) fprintf (lgl->out, " %d", lglm2i (lgl, *P)); \
 112   lglogend (lgl); \
 113 } while (0)
 114
 115 #define LOGRESOLVENT(LEVEL,FMT,ARGS...) \
 116 do { \
 117   const int * P; \
 118   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 119   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
 120   for (P = lgl->resolvent.start; P < lgl->resolvent.top; P++) \
 121     fprintf (lgl->out, " %d", *P); \
 122   lglogend (lgl); \
 123 } while (0)
 124
 125 #define LOGREASON(LEVEL,LIT,REASON0,REASON1,FMT,ARGS...) \
 126 do { \
 127   int TAG, TMP, RED, G; \
 128   const int * C, * P; \
 129   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 130   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
 131   TMP = (REASON0 >> RMSHFT); \
 132   RED = (REASON0 & REDCS); \
 133   TAG = (REASON0 & MASKCS); \
 134   if (TAG == DECISION) fputs (" decision", lgl->out); \
 135   else if (TAG == UNITCS) fprintf (lgl->out, " unit %d", LIT); \
 136   else if (TAG == BINCS) { \
 137     fprintf (lgl->out, \
 138        " %s binary clause %d %d", lglred2str (RED), LIT, TMP); \
 139   } else if (TAG == TRNCS) { \
 140     fprintf (lgl->out, " %s ternary clause %d %d %d", \
 141             lglred2str (RED), LIT, TMP, REASON1); \
 142   } else { \
 143     assert (TAG == LRGCS); \
 144     C = lglidx2lits (lgl, RED, REASON1); \
 145     for (P = C; *P; P++) \
 146       ; \
 147     fprintf (lgl->out, " size %ld", (long)(P - C)); \
 148     if (RED) { \
 149       G = (REASON1 & GLUEMASK); \
 150       fprintf (lgl->out, " glue %d redundant", G); \
 151     } else fputs (" irredundant", lgl->out); \
 152     fputs (" clause", lgl->out); \
 153     for (P = C; *P; P++) { \
 154       fprintf (lgl->out, " %d", *P); \
 155     } \
 156   } \
 157   lglogend (lgl); \
 158 } while (0)
 159
 160 #define LOGDSCHED(LEVEL,LIT,FMT,ARGS...) \
 161   do { \
 162     int POS; \
 163     if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 164     POS = *lgldpos (lgl, LIT); \
 165     lglogstart (lgl, MAPLOGLEVEL(LEVEL), "dsched[%d] = %d ", POS, LIT); \
 166     printf (FMT, ##ARGS); \
 167     printf (" score %s", lglscr2str (lgl, lglqvar (lgl, LIT)->score)); \
 168     lglogend (lgl); \
 169   } while (0)
 170
 171 #define LOGESCHED(LEVEL,LIT,FMT,ARGS...) \
 172 do { \
 173   int POS; \
 174   EVar * EV; \
 175   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 176   POS = *lglepos (lgl, LIT); \
 177   EV = lglevar (lgl, LIT); \
 178   lglogstart (lgl, MAPLOGLEVEL(LEVEL), "esched[%d] = %d ", POS, LIT); \
 179   fprintf (lgl->out, FMT, ##ARGS); \
 180   fprintf (lgl->out, " score"); \
 181   fprintf (lgl->out, " occ %d %d", EV->occ[0], EV->occ[1]); \
 182   lglogend (lgl); \
 183 } while (0)
 184
 185 #define LOGEQN(LEVEL,EQN,FMT,ARGS...) \
 186 do { \
 187   const int * P, * START; \
 188   if (MAPLOGLEVEL(LEVEL) > lgl->opts->log.val) break; \
 189   lglogstart (lgl, MAPLOGLEVEL(LEVEL), FMT, ##ARGS); \
 190   START = lgl->gauss->xors.start + (EQN); \
 191   assert (START < lgl->gauss->xors.top); \
 192   for (P = START; *P > 1; P++) fprintf (lgl->out, " %d", *P); \
 193   fprintf (lgl->out, " = %d", *P); \
 194   lglogend (lgl); \
 195 } while (0)
 196
 197 /*------------------------------------------------------------------------*/
 198 #else /* end of then start of else part of 'ifndef NLGLOG' */
 199 /*------------------------------------------------------------------------*/
 200
 201 #define LOG(ARGS...) do { } while (0)
 202 #define LOGCLS(ARGS...) do { } while (0)
 203 #define LOGMCLS(ARGS...) do { } while (0)
 204 #define LOGRESOLVENT(ARGS...) do { } while (0)
 205 #define LOGREASON(ARGS...) do { } while (0)
 206 #define LOGDSCHED(ARGS...) do { } while (0)
 207 #define LOGESCHED(ARGS...) do { } while (0)
 208 #define LOGEQN(ARGS...) do { } while (0)
 209
 210 /*------------------------------------------------------------------------*/
 211 #endif /* end of else part of 'ifndef NLGLOG' */
 212 /*------------------------------------------------------------------------*/
 213
 214 #define ABORTIF(COND,FMT,ARGS...) \
 215 do { \
 216   if (!(COND)) break; \
 217   fprintf (stderr, "*** API usage error of '%s' in '%s'", \
 218            __FILE__, __FUNCTION__); \
 219   if (lgl && lgl->tid >= 0) fprintf (stderr, " (tid %d)", lgl->tid); \
 220   fputs (": ", stderr); \
 221   fprintf (stderr, FMT, ##ARGS); \
 222   fputc ('\n', stderr); \
 223   fflush (stderr); \
 224   lglabort (lgl); \
 225   exit (1); \
 226 } while (0)
 227
 228 // Useful for using our 'sleeponabort' and other hooks 'on abort' ...
 229
 230 #ifndef NDEBUG
 231 #define ASSERT(COND) \
 232 do { \
 233   if ((COND)) break; \
 234   fprintf (stderr, \
 235     "liblgl.a: %s:%d: %s: Lingeling Assertion `%s' failed.", \
 236     __FUNCTION__, __LINE__, __FILE__, # COND); \
 237   if (lgl && lgl->tid >= 0) fprintf (stderr, " (tid %d)", lgl->tid); \
 238   fputc ('\n', stderr); \
 239   fflush (stderr); \
 240   lglabort (lgl); \
 241   exit (1); \
 242 } while (0)
 243 #else
 244 #define ASSERT(COND) do { } while (0)
 245 #endif
 246
 247 #define COVER(COND) \
 248 do { \
 249   if (!(COND)) break; \
 250   fprintf (stderr, \
 251     "liblgl.a: %s:%d: %s: Coverage target `%s' reached.", \
 252     __FUNCTION__, __LINE__, __FILE__, # COND); \
 253   if (lgl && lgl->tid >= 0) fprintf (stderr, " (tid %d)", lgl->tid); \
 254   fputc ('\n', stderr); \
 255   fflush (stderr); \
 256   abort (); /* TODO: why not 'lglabort' */ \
 257 } while (0)
 258
 259 #define REQINIT() \
 260 do { \
 261   ABORTIF (!lgl, "uninitialized manager"); \
 262 } while (0)
 263
 264 #define REQINITNOTFORKED() \
 265 do { \
 266   REQINIT (); \
 267   ABORTIF (lgl->forked, "forked manager"); \
 268 } while (0)
 269
 270 #define REQUIRE(STATE) \
 271 do { \
 272   REQINIT (); \
 273   ABORTIF(!(lgl->state & (STATE)), "!(%s)", #STATE); \
 274 } while (0)
 275
 276 #define TRANS(STATE) \
 277 do { \
 278   assert (lgl->state != STATE); \
 279   LOG (1, "transition to state " #STATE); \
 280   lgl->state = STATE; \
 281 } while (0)
 282
 283 /*------------------------------------------------------------------------*/
 284
 285 #if !defined(NDEBUG) || !defined(NLGLOG)
 286 #define RESOLVENT
 287 #endif
 288
 289 /*------------------------------------------------------------------------*/
 290
 291 #define TRAPI(MSG,ARGS...) \
 292 do { \
 293   if (!lgl->apitrace) break; \
 294   lgltrapi (lgl, MSG, ##ARGS); \
 295 } while (0)
 296
 297 #define LGLCHKACT(ACT) \
 298 do { assert (NOTALIT <= (ACT) && (ACT) < REMOVED - 1); } while (0)
 299
 300 /*------------------------------------------------------------------------*/
 301
 302 #define OPT(SHRT,LNG,VAL,MIN,MAX,DESCRP) \
 303 do { \
 304   Opt * opt = &lgl->opts->LNG; \
 305   opt->shrt = SHRT; \
 306   opt->lng = #LNG; \
 307   opt->dflt = opt->val = VAL; \
 308   assert (MIN <= VAL); \
 309   opt->min = MIN; \
 310   assert (VAL <= MAX); \
 311   opt->max = MAX; \
 312   opt->descrp = DESCRP; \
 313   lglgetenv (lgl, opt, #LNG); \
 314 } while (0)
 315
 316 /*------------------------------------------------------------------------*/
 317
 318 #define NEW(P,N) \
 319 do { (P) = lglnew (lgl, (N) * sizeof *(P)); } while (0)
 320
 321 #define DEL(P,N) \
 322 do { lgldel (lgl, (P), (N) * sizeof *(P)); (P) = 0; } while (0)
 323
 324 #define RSZ(P,O,N) \
 325 do { (P) = lglrsz (lgl, (P), (O)*sizeof*(P), (N)*sizeof*(P)); } while (0)
 326
 327 #define CLN(P,N) \
 328 do { memset ((P), 0, (N) * sizeof *(P)); } while (0)
 329
 330 #define CLRPTR(P) \
 331 do { memset ((P), 0, sizeof *(P)); } while (0)
 332
 333 #define CLR(P) \
 334 do { memset (&(P), 0, sizeof (P)); } while (0)
 335
 336 /*------------------------------------------------------------------------*/
 337
 338 #define SWAP(TYPE,A,B) \
 339 do { TYPE TMP = (A); (A) = (B); (B) = TMP; } while (0)
 340
 341 #define ISORTLIM 10
 342
 343 #define CMPSWAP(TYPE,CMP,P,Q) \
 344 do { if (CMP (&(P), &(Q)) > 0) SWAP (TYPE, P, Q); } while(0)
 345
 346 #define QPART(TYPE,CMP,A,L,R) \
 347 do { \
 348   TYPE PIVOT; \
 349   int J = (R); \
 350   I = (L) - 1; \
 351   PIVOT = (A)[J]; \
 352   for (;;) { \
 353     while (CMP (&(A)[++I], &PIVOT) < 0) \
 354       ; \
 355     while (CMP (&PIVOT, &(A)[--J]) < 0) \
 356       if (J == (L)) break; \
 357     if (I >= J) break; \
 358     SWAP (TYPE, (A)[I], (A)[J]); \
 359   } \
 360   SWAP (TYPE, (A)[I], (A)[R]); \
 361 } while(0)
 362
 363 #define QSORT(TYPE,CMP,A,N) \
 364 do { \
 365   int L = 0, R = (N) - 1, M, LL, RR, I; \
 366   assert (lglmtstk (&lgl->sortstk)); \
 367   if (R - L <= ISORTLIM) break; \
 368   for (;;) { \
 369     M = (L + R) / 2; \
 370     SWAP (TYPE, (A)[M], (A)[R - 1]); \
 371     CMPSWAP (TYPE, CMP, (A)[L], (A)[R - 1]); \
 372     CMPSWAP (TYPE, CMP, (A)[L], (A)[R]); \
 373     CMPSWAP (TYPE, CMP, (A)[R - 1], (A)[R]); \
 374     QPART (TYPE, CMP, (A), L + 1, R - 1); \
 375     if (I - L < R - I) { LL = I + 1; RR = R; R = I - 1; } \
 376     else { LL = L; RR = I - 1; L = I + 1; } \
 377     if (R - L > ISORTLIM) { \
 378       assert (RR - LL > ISORTLIM); \
 379       lglpushstk (lgl, &lgl->sortstk, LL); \
 380       lglpushstk (lgl, &lgl->sortstk, RR); \
 381     } else if (RR - LL > ISORTLIM) L = LL, R = RR; \
 382     else if (!lglmtstk (&lgl->sortstk)) { \
 383       R = lglpopstk (&lgl->sortstk); \
 384       L = lglpopstk (&lgl->sortstk); \
 385     } else break; \
 386   } \
 387 } while (0)
 388
 389 #define ISORT(TYPE,CMP,A,N) \
 390 do { \
 391   TYPE PIVOT; \
 392   int L = 0, R = (N) - 1, I, J; \
 393   for (I = R; I > L; I--) \
 394     CMPSWAP (TYPE, CMP, (A)[I - 1], (A)[I]); \
 395   for (I = L + 2; I <= R; I++) { \
 396     J = I; \
 397     PIVOT = (A)[I]; \
 398     while (CMP (&PIVOT, &(A)[J - 1]) < 0) { \
 399       (A)[J] = (A)[J - 1]; \
 400       J--; \
 401     } \
 402     (A)[J] = PIVOT; \
 403   } \
 404 } while (0)
 405
 406 #ifdef NDEBUG
 407 #define CHKSORT(CMP,A,N) do { } while(0)
 408 #else
 409 #define CHKSORT(CMP,A,N) \
 410 do { \
 411   int I; \
 412   for (I = 0; I < (N) - 1; I++) \
 413     assert (CMP (&(A)[I], &(A)[I + 1]) <= 0); \
 414 } while(0)
 415 #endif
 416
 417 #define SORT(TYPE,A,N,CMP) \
 418 do { \
 419   TYPE * AA = (A); \
 420   int NN = (N); \
 421   QSORT (TYPE, CMP, AA, NN); \
 422   ISORT (TYPE, CMP, AA, NN); \
 423   CHKSORT (CMP, AA, NN); \
 424 } while (0)
 425
 426 /*------------------------------------------------------------------------*/
 427
 428 #define LGLPOPWTK(WTK,WRAG,LIT,OTHER,RED,REMOVED) \
 429 do { \
 430   assert (!lglmtwtk (WTK)); \
 431   (WTK)->top--; \
 432   (WRAG) = (WTK)->top->wrag; \
 433   (LIT) = (WTK)->top->lit; \
 434   (OTHER) = (WTK)->top->other; \
 435   (RED) = (WTK)->top->red ? REDCS : 0; \
 436   (REMOVED) = (WTK)->top->removed; \
 437 } while (0)
 438
 439 /*------------------------------------------------------------------------*/
 440
 441 #define CLONE(FIELD,SIZE) \
 442 do { \
 443   NEW (lgl->FIELD, (SIZE)); \
 444   memcpy (lgl->FIELD, orig->FIELD, (SIZE) * sizeof *(lgl->FIELD)); \
 445 } while (0)
 446
 447 #define CLONESTK(NAME) \
 448 do { \
 449   size_t COUNT = orig->NAME.top - orig->NAME.start; \
 450   size_t SIZE = orig->NAME.end - orig->NAME.start; \
 451   size_t BYTES = SIZE * sizeof *lgl->NAME.start; \
 452   NEW (lgl->NAME.start, SIZE); \
 453   memcpy (lgl->NAME.start, orig->NAME.start, BYTES); \
 454   lgl->NAME.top = lgl->NAME.start + COUNT; \
 455   lgl->NAME.end = lgl->NAME.start + SIZE; \
 456 } while (0)
 457
 458 /*------------------------------------------------------------------------*/
 459
 460 #define INCSTEPS(NAME) \
 461  ((lgl->stats->steps++), (lgl->stats->NAME++))
 462
 463 #define ADDSTEPS(NAME,INC) \
 464  ((lgl->stats->steps += INC), (lgl->stats->NAME += INC))
 465
 466 /*------------------------------------------------------------------------*/
 467
 468 #define LGLUPDPEN(NAME,SUCCESS) \
 469 do { \
 470   assert (!lgl->limits->NAME.del.rem); \
 471   if ((SUCCESS) && lgl->limits->NAME.pen) \
 472     lgl->limits->NAME.pen--; \
 473   if (!(SUCCESS) && lgl->limits->NAME.pen < lgl->opts->penmax.val) \
 474     lgl->limits->NAME.pen++; \
 475   if ((SUCCESS) && lgl->limits->NAME.del.cur) \
 476     lgl->limits->NAME.del.cur /= 2; \
 477   if (!(SUCCESS) && lgl->limits->NAME.del.cur < lgl->opts->delmax.val) \
 478     lgl->limits->NAME.del.cur++; \
 479   lgl->limits->NAME.del.rem = lgl->limits->NAME.del.cur; \
 480 } while (0)
 481
 482 /*-------------------------------------------------------------------------*/
 483
 484 #define LGLL long long
 485
 486 /*-------------------------------------------------------------------------*/
 487
 488 typedef enum Tag {
 489   FREEVAR = 0,
 490   FIXEDVAR = 1,
 491   EQUIVAR = 2,
 492   ELIMVAR = 3,
 493
 494   DECISION = 0,
 495   UNITCS = 1,
 496   OCCS = 1,
 497   BINCS = 2,
 498   TRNCS = 3,
 499   LRGCS = 4,
 500   MASKCS = 7,
 501
 502   REDCS = 8,
 503   RMSHFT = 4,
 504 } Tag;
 505
 506 typedef enum State {
 507   UNUSED        = (1<<0),
 508   OPTSET        = (1<<1),
 509   USED          = (1<<2),
 510   READY         = (1<<3),
 511   UNKNOWN       = (1<<4),
 512   SATISFIED     = (1<<5),
 513   EXTENDED      = (1<<6),
 514   UNSATISFIED   = (1<<7),
 515   FAILED        = (1<<8),
 516   LOOKED        = (1<<9),
 517   RESET         = (1<<10),
 518 } State;
 519
 520 typedef enum Wrag {
 521   PREFIX = 0,
 522   BEFORE = 1,
 523   AFTER = 2,
 524   POSTFIX = 3,
 525 } Wrag;
 526
 527 typedef enum GTag { ANDTAG, ITETAG, XORTAG } GTag;
 528
 529 /*------------------------------------------------------------------------*/
 530
 531 typedef struct Opt {
 532   char shrt;
 533   const char * lng, * descrp;
 534   int val, min, max, dflt;
 535 } Opt;
 536
 537 typedef struct Opts {
 538
 539   Opt beforefirst;
 540
 541   Opt abstime;
 542   Opt actavgmax;
 543   Opt actdblarithlim;
 544   Opt actgeomlim;
 545   Opt actgsdul;
 546   Opt acts;
 547   Opt actstdmax;
 548   Opt actstdmin;
 549   Opt actvlim;
 550   Opt agile;
 551   Opt agilelim;
 552   Opt agilesinint;
 553   Opt bate;
 554   Opt batewait;
 555   Opt bca;
 556   Opt bcamaxeff;
 557   Opt bcaminuse;
 558   Opt bcawait;
 559   Opt bva;
 560   Opt bias;
 561   Opt binlocsdel;
 562   Opt binsimpdel;
 563   Opt bkwdscale;
 564   Opt blkboost;
 565   Opt blkboostvlim;
 566   Opt blkclslim;
 567   Opt blklarge;
 568   Opt blkmaxeff;
 569   Opt blkmineff;
 570   Opt blkocclim;
 571   Opt blkocclim1;
 572   Opt blkocclim2;
 573   Opt blkreleff;
 574   Opt blkrtc;
 575   Opt blksched2b2;
 576   Opt blkschedmin;
 577   Opt blkschedprod;
 578   Opt blkschedpure;
 579   Opt blkschedsum;
 580   Opt blksmall;
 581   Opt blksuccesslim;
 582   Opt blksuccessrat;
 583   Opt block;
 584   Opt blockwait;
 585   Opt boost;
 586   Opt bumpbcplits;
 587   Opt bumpclslits;
 588   Opt bumpseenaftermin;
 589   Opt bumpseenbeforemin;
 590   Opt bumpseenlits;
 591   Opt bumpseenminsize;
 592   Opt card;
 593   Opt cardcut;
 594   Opt cardexpam1;
 595   Opt cardglue;
 596   Opt cardignused;
 597   Opt cardmaxeff;
 598   Opt cardmaxlen;
 599   Opt cardmineff;
 600   Opt cardminlen;
 601   Opt cardocclim1;
 602   Opt cardocclim2;
 603   Opt cardreleff;
 604   Opt cardreschedint;
 605   Opt carduse;
 606   Opt cardwait;
 607   Opt cce;
 608   Opt cceboost;
 609   Opt cceboostvlim;
 610   Opt cce2wait;
 611   Opt cce3wait;
 612   Opt ccemaxeff;
 613   Opt ccemineff;
 614   Opt cceonlyifstuck;
 615   Opt ccereleff;
 616   Opt ccertc;
 617   Opt ccesuccesslim;
 618   Opt ccesuccessrat;
 619   Opt ccewait;
 620   Opt cgrclsr;
 621   Opt cgrclsrwait;
 622   Opt cgreleff;
 623   Opt cgrextand;
 624   Opt cgrexteq;
 625   Opt cgrextite;
 626   Opt cgrextunits;
 627   Opt cgrextxor;
 628   Opt cgrmaxeff;
 629   Opt cgrmaxority;
 630   Opt cgrmineff;
 631   Opt cintinc;
 632   Opt cintincdiv;
 633   Opt cintmaxhard;
 634   Opt cintmaxsoft;
 635   Opt cliff;
 636   Opt cliffmaxeff;
 637   Opt cliffmineff;
 638   Opt cliffreleff;
 639   Opt cliffwait;
 640   Opt clim;
 641   Opt compact;
 642   Opt deco;
 643   Opt decolim;
 644   Opt decompose;
 645   Opt defragfree;
 646   Opt defragint;
 647   Opt delmax;
 648   Opt dlim;
 649   Opt drup;
 650   Opt druplig;
 651   Opt elim;
 652   Opt elmaxeff;
 653   Opt elmblk;
 654   Opt elmblkwait;
 655   Opt elmboost;
 656   Opt elmclslim;
 657   Opt elmfull;
 658   Opt elmineff;
 659   Opt elmlitslim;
 660   Opt elmocclim;
 661   Opt elmocclim1;
 662   Opt elmocclim2;
 663   Opt elmreleff;
 664   Opt elmroundlim;
 665   Opt elmrtc;
 666   Opt elmsched2b2;
 667   Opt elmschediff;
 668   Opt elmschedmin;
 669   Opt elmschedprod;
 670   Opt elmschedpure;
 671   Opt elmschedsum;
 672   Opt elmsuccesslim;
 673   Opt elmsuccessrat;
 674   Opt exitonabort;
 675   Opt factmax;
 676   Opt factor;
 677   Opt flipdur;
 678   Opt flipint;
 679   Opt flipldmod;
 680   Opt fliplevels;
 681   Opt flipping;
 682   Opt fliptop;
 683   Opt flipvlim;
 684   Opt force;
 685   Opt gauss;
 686   Opt gaussexptrn;
 687   Opt gaussextrall;
 688   Opt gaussmaxeff;
 689   Opt gaussmaxor;
 690   Opt gaussmineff;
 691   Opt gaussreleff;
 692   Opt gausswait;
 693   Opt gluekeep;
 694   Opt gluescale;
 695   Opt import;
 696   Opt incredcint;
 697   Opt incredconfslim;
 698   Opt incsavevisits;
 699   Opt inprocessing;
 700   Opt irrlim;
 701   Opt itlocsdel;
 702   Opt itsimpdel;
 703   Opt jwhred;
 704   Opt keepmaxglue;
 705   Opt lftmaxeff;
 706   Opt lftmineff;
 707   Opt lftreleff;
 708   Opt lftroundlim;
 709   Opt lhbr;
 710   Opt lift;
 711   Opt liftlrg;
 712   Opt liftwait;
 713   Opt lkhd;
 714   Opt lkhdmisifelmrtc;
 715   Opt locs;
 716   Opt locsboost;
 717   Opt locscint;
 718   Opt locsdec;
 719   Opt locset;
 720   Opt locsexport;
 721   Opt locsmaxeff;
 722   Opt locsmineff;
 723   Opt locsclim;
 724   Opt locsred;
 725   Opt locsreleff;
 726   Opt locsrtc;
 727   Opt locsvared;
 728   Opt locswait;
 729   Opt maxglue;
 730   Opt maxscorexp;
 731   Opt mega;
 732   Opt megaint;
 733   Opt megawait;
 734   Opt memlim;
 735   Opt minimize;
 736   Opt minlocalgluelim;
 737   Opt minrecgluelim;
 738   Opt mocint;
 739   Opt move;
 740   Opt otfs;
 741   Opt otfsbump;
 742   Opt otfsconf;
 743   Opt penmax;
 744   Opt phase;
 745   Opt phaseflip;
 746   Opt phasegluebit;
 747   Opt phaseneginit;
 748   Opt plain;
 749   Opt plim;
 750   Opt prbasic;
 751   Opt prbasicmaxeff;
 752   Opt prbasicmineff;
 753   Opt prbasicreleff;
 754   Opt prbasicroundlim;
 755   Opt prbasicrtc;
 756   Opt prbrtc;
 757   Opt prbsimple;
 758   Opt prbsimpleboost;
 759   Opt prbsimpleliftdepth;
 760   Opt prbsimplemaxeff;
 761   Opt prbsimplemineff;
 762   Opt prbsimplereleff;
 763   Opt prbsimplertc;
 764   Opt probe;
 765   Opt psm;
 766   Opt pure;
 767   Opt randec;
 768   Opt randecflipint;
 769   Opt randecint;
 770   Opt rdp;
 771   Opt rdpclslim;
 772   Opt rdplim;
 773   Opt rdpmaxeff;
 774   Opt rdpmineff;
 775   Opt rdpmodelm;
 776   Opt rdpreleff;
 777   Opt rdpwait;
 778   Opt redfixed;
 779   Opt redinoutinc;
 780   Opt redlbound;
 781   Opt redlexpfac;
 782   Opt redlinc;
 783   Opt redlinit;
 784   Opt redlmaxabs;
 785   Opt redlmaxinc;
 786   Opt redlmaxrel;
 787   Opt redlminabs;
 788   Opt redlmininc;
 789   Opt redlminrel;
 790   Opt redloutinc;
 791   Opt redoutclim;
 792   Opt redoutvlim;
 793   Opt reduce;
 794   Opt rephase;
 795   Opt rephaseinc;
 796   Opt restart;
 797   Opt restartinit;
 798   Opt restartint;
 799   Opt restartintscale;
 800   Opt reusetrail;
 801   Opt rmincpen;
 802   Opt rstinoutinc;
 803   Opt saturating;
 804   Opt scincinc;
 805   Opt score;
 806   Opt seed;
 807   Opt simpdelay;
 808   Opt simpen;
 809   Opt simpidiv;
 810   Opt simpinterdelay;
 811   Opt simpiscale;
 812   Opt simplify;
 813   Opt simprtc;
 814   Opt simpvarchg;
 815   Opt simpvarlim;
 816   Opt sizemaxpen;
 817   Opt sizepen;
 818   Opt sleeponabort;
 819   Opt smallirr;
 820   Opt smallve;
 821   Opt smallvevars;
 822   Opt smallvewait;
 823   Opt sortlits;
 824   Opt subl;
 825   Opt synclsall;
 826   Opt synclsglue;
 827   Opt synclsint;
 828   Opt synclslen;
 829   Opt syncunint;
 830   Opt tabr;
 831   Opt tabrcfactor;
 832   Opt tabrkeep;
 833   Opt tabrvfactor;
 834   Opt termint;
 835   Opt ternres;
 836   Opt ternresboost;
 837   Opt ternresrtc;
 838   Opt ternreswait;
 839   Opt transred;
 840   Opt transredwait;
 841   Opt trdmaxeff;
 842   Opt trdmineff;
 843   Opt trdreleff;
 844   Opt treelook;
 845   Opt treelookboost;
 846   Opt treelookfull;
 847   Opt treelooklrg;
 848   Opt treelookmaxeff;
 849   Opt treelookmineff;
 850   Opt treelookreleff;
 851   Opt treelookrtc;
 852   Opt trep;
 853   Opt trepint;
 854   Opt trnreleff;
 855   Opt trnrmaxeff;
 856   Opt trnrmineff;
 857   Opt unhdatrn;
 858   Opt unhdextstamp;
 859   Opt unhdhbr;
 860   Opt unhdlnpr;
 861   Opt unhdmaxeff;
 862   Opt unhdmineff;
 863   Opt unhdreleff;
 864   Opt unhdroundlim;
 865   Opt unhide;
 866   Opt unhidewait;
 867   Opt wait;
 868   Opt waitmax;
 869   Opt witness;
 870
 871   Opt check;
 872   Opt log;
 873   Opt verbose;
 874
 875   Opt afterlast;
 876
 877 } Opts;
 878
 879 #define FIRSTOPT(lgl) (&(lgl)->opts->beforefirst + 1)
 880 #define LASTOPT(lgl) (&(lgl)->opts->afterlast - 1)
 881
 882 /*------------------------------------------------------------------------*/
 883
 884 typedef int Exp;
 885 typedef uint64_t Mnt;
 886 typedef int64_t Flt;
 887 typedef int64_t Cnf;
 888 typedef uint64_t Fun[FUNQUADS];
 889 typedef signed char Val;
 890 typedef Flt LKHD;
 891
 892 /*------------------------------------------------------------------------*/
 893 #ifdef NDBLSCR
 894 typedef Flt Scr;
 895 #else
 896 typedef double Scr;
 897 #endif
 898 /*------------------------------------------------------------------------*/
 899
 900 typedef struct Conf { int lit, rsn[2]; } Conf;
 901 typedef struct Ctk { struct Ctr * start, * top, * end; } Ctk;
 902 typedef struct DFOPF { int observed, pushed, flag; } DFOPF;
 903 typedef struct DFPR { int discovered, finished, parent, root; } DFPR;
 904 typedef struct EVar { int occ[2], pos, score; } EVar;
 905 typedef struct Ftk { Flt * start, * top, * end; } Ftk;
 906 typedef struct HTS { int offset, count; }  HTS;
 907 typedef struct ITEC { int other, other2; } ITEC;
 908 typedef struct Lim { int64_t confs, decs, props; } Lim;
 909 typedef struct PASL { int psm, act, size, lidx; } PASL;
 910 typedef struct PSz { int pos, size; } PSz;
 911 typedef struct Qnd { int prev, next; struct Qln * line; } Qnd;
 912 typedef struct RNG { unsigned z, w; } RNG;
 913 typedef struct Stk { int * start, * top, * end; } Stk;
 914 typedef struct Tmrs { double phase[MAXPHN]; int idx[MAXPHN], nest; } Tmrs;
 915 typedef struct Trv { void * state; void (*trav)(void *, int); } Trv;
 916 typedef struct TVar { signed int val : 30; unsigned mark : 2; } TVar;
 917 typedef struct Wtk { struct Work * start, * top, * end; } Wtk;
 918
 919 /*------------------------------------------------------------------------*/
 920
 921 typedef struct Ctr {
 922   signed int decision : 31;
 923   unsigned used : 1;
 924 } Ctr;
 925
 926 typedef struct DVar { HTS hts[2]; } DVar;
 927
 928 typedef struct QVar { Scr score; int pos; } QVar;
 929
 930 typedef struct TD {
 931   signed int level:30;
 932   unsigned lrglue:1, irr:1;
 933   int rsn[2];
 934 } TD;
 935
 936 typedef struct ID { int level, lit, rsn[2]; } ID;
 937
 938 typedef struct Impls { ID * start, * top, * end; } Impls;
 939
 940 typedef struct AVar {
 941   unsigned type : 4;
 942 #ifndef NDEBUG
 943   unsigned simp:1, wasfalse:1;
 944 #endif
 945   unsigned equiv:1, lcamark:4;
 946   signed int phase:2, bias:2, fase:2;
 947   unsigned inred:2, poisoned:1, assumed:2, failed:2, gate:1;
 948   unsigned donotelm:1, donotblk:1, donotcgrcls:1, donotlft:1, donoternres:1;
 949   unsigned donotbasicprobe:1, donotsimpleprobe:1, donotreelook:1, mega:2;
 950 #ifndef NLGLYALSAT
 951   signed int locsval:2;
 952 #endif
 953   int mark, trail;
 954 } AVar;
 955
 956 typedef struct Ext {
 957   unsigned equiv:1,melted:1,blocking:2,eliminated:1,tmpfrozen:1,imported:1;
 958   unsigned assumed:2,failed:2,internal:1,defined:1;
 959   signed int val:2, oldval:2;
 960   int repr, frozen;
 961 } Ext;
 962
 963 typedef struct Work {
 964   unsigned wrag : 2;
 965   signed int lit : 30, other : 30;
 966   unsigned red : 1, removed : 1;
 967 } Work;
 968
 969 typedef struct DFL {
 970   int discovered, finished;
 971   union { int lit, sign; };
 972 #ifndef NLGLOG
 973   int lit4logging;
 974 #endif
 975 } DFL;
 976
 977 typedef struct Gat {
 978   int lhs, minrhs;
 979   unsigned tag : 2;
 980   unsigned mark : 1;
 981   signed int size : 29;
 982   union {
 983     int lits[2];
 984     struct { int * cls, origlhs; };
 985     struct { int cond, pos, neg; };
 986   };
 987 } Gat;
 988
 989 /*------------------------------------------------------------------------*/
 990
 991 typedef struct Stats {
 992   int64_t steps, trims;
 993   int defrags, iterations, acts, reported, repcntdown, gcs, decomps;
 994   int cutwidths;
 995   struct { int64_t count, steps; struct { int max, min; } mincut; } force;
 996   struct { int clauses, vars; } rescored;
 997   struct { int count;
 998            struct {int64_t scaled, orig; } intsum;
 999            struct { int count, saturating, agile, reuse; } skipped;
1000            struct { int count; int64_t sum; } kept; } restarts;
1001   struct { int count, reset, geom, gul, arith, arith2, memlim; } reduced;
1002   int64_t prgss, irrprgss, enlwchs, pshwchs, height, dense, sparse;
1003   int64_t confs, decisions, randecs, randecsflipped, flipped, fliphases;
1004   int64_t uips, decflipped;
1005   struct { struct { int cur, max; int64_t add; } clauses, lits; } irr;
1006   struct { int64_t sat, mosat, simp, deref, fixed, freeze, lkhd;
1007            int64_t melt, add, assume, cassume, failed, repr; } calls;
1008   struct { int64_t search, hits; } poison;
1009   struct { int64_t search, simp, lkhd; } props, visits, travs;
1010   struct { size_t current, max; } bytes;
1011   struct { int bin, trn, lrg; } red;
1012   struct { int cnt, simple, trn, lrg, sub; } hbr;
1013   struct { int current, sum; } fixed, equiv;
1014   struct { int count, bin, trn; int64_t steps; } trnr;
1015   struct { int count, clauses, lits, pure; int64_t res, steps; } blk;
1016   struct { int count, eq, units; int64_t esteps, csteps;
1017            struct { int all, and, xor, ite; } matched;
1018            struct { int all, and, xor, ite; } simplified;
1019            struct { int64_t all, and, xor, ite; } extracted; } cgr;
1020   struct {
1021     struct { int count, failed, eqs; int64_t probed, steps; } simple;
1022     struct { int count, failed, lifted;
1023              int64_t probed, steps, lastate;
1024              struct { int trnr, lrg, count; } ate; } basic;
1025     struct { int count, failed, lifted; int64_t probed, steps; } treelook;
1026   } prb;
1027   struct { int count, eqs, units, impls; int64_t probed0, probed1; } lift;
1028   struct { int count, red, failed; int64_t lits, bins, steps; } trd;
1029   struct { int removed, red; } bindup;
1030   struct { int count, rounds;
1031            struct { int trds, failed, sccs; int64_t sumsccsizes; } stamp;
1032            struct { int lits, bin, trn, lrg; } failed;
1033            struct { int bin, trn, lrg, red; } tauts;
1034            struct { int bin, trn, lrg; } units;
1035            struct { int trn, lrg, red; } hbrs;
1036            struct { int trn, lrg, red; } str;
1037            int64_t steps; } unhd;
1038   struct {
1039     int count, elmd, large, sub, str, blkd, rounds;
1040     struct { int elm, tried, failed; } small;
1041     int64_t resolutions, copies, subchks, strchks, ipos, steps; } elm;
1042   struct {
1043     int sub2, sub3, subl, str2, str3, str3self, strl, strlself;
1044     struct { int64_t lits, clauses, occs; } tried;
1045     int64_t steps;
1046   } bkwd;
1047   struct {
1048     struct { struct { int irr, red; } dyn; } sub, str;
1049     int64_t driving, restarting; } otfs;
1050   struct { int64_t nonmin, learned; } lits;
1051   struct {
1052     int64_t learned, glue, realglue, nonmaxglue, maxglue, scglue; }
1053   clauses;
1054   struct {
1055     int clauses;
1056     int64_t added, reduced, resolved, forcing, conflicts, saved;
1057   } lir[POW2GLUE];
1058   struct { int64_t sum; int count; } glues;
1059   struct { int count; int64_t set, pos, neg; } phase;
1060   struct { int count; struct { int confs, irr, vars; } limhit; } simp;
1061   struct { int count; int64_t steps; } luby, inout;
1062   struct { int count, gcs, units, equivs, trneqs;
1063            struct { int max; int64_t sum; } arity;
1064            struct { int64_t extr, elim; } steps;
1065            int64_t extracted; } gauss;
1066   struct { int count, eliminated, ate, abce, failed, lifted;
1067            int64_t steps, probed;
1068            struct { int64_t search, hits, cols, ins, rsz; } cache; } cce;
1069   struct { int count, failed, lifted; int64_t decisions, steps; } cliff;
1070   struct {
1071     int count, units, expam1, resched;
1072     int64_t steps, eliminated, resolved, subsumed;
1073     struct { struct { int64_t sum, cnt; } found, used; } am1, am2; } card;
1074   struct { int64_t bin, trn, lrg; } moved;
1075   struct { int count, inc; } rephase;
1076   struct { int count; int64_t added, skipped, steps; } bca;
1077   struct { int count; int64_t added, removed; } bva;
1078   struct {
1079     struct {
1080       int64_t produced;
1081       struct { int64_t actual, tried, calls; } consumed;
1082     } cls, units;
1083   } sync;
1084   struct { struct { int64_t orig, red; } sum; } deco;
1085   struct { int64_t min, bin, size, deco; } mincls;
1086   int64_t drupped, druplig;
1087   struct {
1088     int64_t count, units, bin, trn, steps, elim, res;
1089     struct { int64_t bound, len, model; } limhit; } rdp;
1090   struct { int64_t count, tried, cands, sub; } subl;
1091   struct { int count; int64_t flips, mems; int min; } locs;
1092   struct { int count; } tabr;
1093   struct { int count, failed, lifted, eqs, rounds; } mega;
1094 } Stats;
1095
1096 /*------------------------------------------------------------------------*/
1097
1098 typedef struct Times {
1099   double all, dcp, elm, trd, gc, dfg, red, blk, ana, unhd, dec, lkhd;
1100   double rsts, lft, trn, cgr, phs, srch, prep, inpr, bump, mcls, gauss;
1101   double card, cce, cliff, ctw, force, bca, rdp, locs, bkwd, bva, tabr;
1102   double mega;
1103   struct { double all, simple, basic, treelook; } prb;
1104 } Times;
1105
1106 /*------------------------------------------------------------------------*/
1107
1108 typedef struct Del { int cur, rem; } Del;
1109
1110 typedef struct Limits {
1111   int flipint, lkhdpen;
1112   int64_t randec, dfg;
1113   struct {
1114     int64_t visits;
1115     struct { int64_t add; int start; } clauses;
1116     struct { int start; } vars;
1117   } inc;
1118   struct { int clauses, vars; } tabr;
1119   struct { int inner, outer, extra; } reduce;
1120   struct { struct { int64_t otfs, confs; } vars; } rescore;
1121   struct { int pen; Del del; int64_t esteps, csteps; } cgr;
1122   struct { int pen; Del del; int64_t steps, irrprgss; } elm, blk, cliff;
1123   struct { int pen; Del del; int64_t steps; }
1124     rdp, trd, unhd, trnr, lft, cce, card;
1125   struct { int pen; Del del; struct { int64_t extr, elim; } steps; } gauss;
1126   struct { int64_t confs; } rephase;
1127   struct { int64_t confs; int wasmaxdelta, maxdelta, luby, inout; } restart;
1128   struct { int64_t steps;
1129            struct { int pen; Del del; } simple, basic, treelook; } prb;
1130   struct { int64_t vars, confs; int pen, cinc; } simp;
1131   struct { int64_t steps, confs; } sync;
1132   struct { int64_t steps; } term;
1133   struct { int64_t fixed; } gc;
1134   struct { Del del; int64_t steps; } bca;
1135   struct { int64_t steps, time; } trep;
1136   struct { int64_t confs, inc; int vars; } locs;
1137 } Limits;
1138
1139 /*------------------------------------------------------------------------*/
1140
1141 typedef struct Cbs {
1142   struct { int (*fun)(void*); void * state; int done; } term;
1143   struct {
1144     struct { void (*fun)(void*,int); void * state; } produce, consumed;
1145     struct { void(*fun)(void*,int**,int**); void*state; } consume;
1146   } units;
1147   struct {
1148     struct { void (*fun)(void*,int*,int); void * state; } produce;
1149     struct { void(*fun)(void*,int**,int*); void*state; } consume;
1150     struct { void (*fun)(void*,int); void * state; } consumed;
1151   } cls;
1152   struct {
1153     struct { int * (*fun)(void*); void * state; } lock;
1154     struct { void (*fun)(void*,int,int); void * state; } unlock;
1155   } eqs;
1156   struct { void(*lock)(void*); void (*unlock)(void*); void*state; } msglock;
1157   double (*getime)(void);
1158   void (*onabort)(void *); void * abortstate;
1159 } Cbs;
1160
1161 typedef struct Cgr {
1162   struct { int units, eq, all, and, xor, ite, org; } extracted;
1163   struct { int all, and, xor, ite, org; } simplified;
1164   struct { int all, and, xor, ite, org; } matched;
1165   Stk * goccs, units; Gat * gates; int szgates;
1166 } Cgr;
1167
1168 typedef struct Cliff { Stk lift, lits; } Cliff;
1169
1170 typedef struct BCA { Stk covered; } BCA;
1171
1172 typedef struct Dis { struct { Stk bin, trn; } red, irr; } Dis;
1173
1174 typedef struct Elm {
1175   int64_t oldsteps;
1176   int pivot, negcls, necls, neglidx, round, oldelmd;
1177   Stk lits, next, clv, csigs, sizes, occs, noccs, mark, m2i;
1178 } Elm;
1179
1180 typedef struct RDP {
1181   int * count, eliminated;
1182   Stk lits, * occs;
1183   double start;
1184 } RDP;
1185
1186 typedef struct Card {
1187   Stk atmost1, atmost2, cards, elim, * occs, units, expam1;
1188   char * eliminated, * lit2used, * marked;
1189   signed char * count;
1190   int * lit2count;
1191 } Card;
1192
1193 typedef struct FltStr { int current; char str[MAXFLTSTR][100]; } FltStr;
1194
1195 typedef struct SPE { signed int count : 31; unsigned mark : 1, sum; } SPE;
1196
1197 typedef struct SPrb {
1198   Stk units, impls, eqs, counted, marked;
1199   SPE * spes;
1200 } SPrb;
1201
1202 typedef struct Gauss {
1203   Stk xors, order, * occs;
1204   signed char * eliminated;
1205   int garbage, next;
1206 } Gauss;
1207
1208 typedef struct CCE {
1209   Stk cla, extend, clauses;
1210   int * rem, bin, trn;
1211 } CCE;
1212
1213 typedef struct Tlk { Stk stk, seen; TVar * tvars; LKHD * lkhd; } Tlk;
1214
1215 typedef struct Mem {
1216   void * state;
1217   lglalloc alloc; lglrealloc realloc; lgldealloc dealloc;
1218 } Mem;
1219
1220 typedef struct Wchs { Stk stk; int start[MAXLDFW], free; } Wchs;
1221
1222 typedef struct Wrk {
1223   Stk queue;
1224   int count, head, size, posonly, fifo, * pos;
1225 } Wrk;
1226
1227 /*------------------------------------------------------------------------*/
1228
1229 struct LGL {
1230   State state;
1231
1232   int probing, flipping, notflipped, tid, tids, bias, phaseneg;
1233   int nvars, szvars, maxext, szext, maxdef, szdef, changed, mt, repcntdown;
1234   int szdrail, bnext, next, next2, flushed, level, alevel, wait;
1235   int unassigned, lrgluereasons, failed, assumed, cassumed, ncassumed;
1236
1237   Scr scinc, scincf, maxscore;
1238
1239   char lifting, cceing, gaussing, cliffing, bcaing, forcerephead;
1240   char cgrclosing, searching, simp, allphaseset, flushphases, occs;
1241   char unhiding, basicprobing, simpleprobing, treelooking, setuponce;
1242   char eliminating, donotsched, blocking, ternresing, lkhd, allfrozen;
1243   char blkall, blkrem, blkrtc, elmall, elmrem, elmrtc, decomposing;
1244   char frozen, dense, notfullyconnected, forcegc, allowforce;
1245   char ccertc, elmstuck, blkstuck;
1246
1247   LGL * parent;
1248   int forked;
1249
1250   unsigned long long flips;
1251
1252   Conf conf;
1253   RNG rng;
1254
1255   // the state above this line is copied during 'clone' with 'memcpy'
1256
1257   Mem * mem;
1258   Opts * opts;
1259   Stats * stats;
1260   Times * times;
1261   Tmrs * timers;
1262   Limits * limits;
1263   Ext * ext, * def;
1264   int * i2e;
1265   int * doms;
1266   DVar * dvars;
1267   QVar * qvars;
1268   AVar * avars;
1269   Val * vals;
1270   Flt * jwh;
1271   TD * drail;
1272   Stk * red;
1273   Wchs * wchs;
1274
1275   Ctk control;
1276   Stk clause, eclause, extend, irr, trail, frames;
1277   Stk dsched, eassume, assume, cassume, fassume, learned;
1278 #ifndef NCHKSOL
1279   Stk orig;
1280 #endif
1281
1282   union {
1283     Elm * elm; Cgr * cgr; SPrb * sprb; Tlk * tlk; Gauss * gauss;
1284     CCE * cce; Cliff * cliff; BCA * bca; Card * card; RDP * rdp;
1285   };
1286   union { Stk lcaseen, sortstk, resolvent; };
1287   Stk poisoned, seen, esched, minstk;
1288   EVar * evars;
1289   Dis * dis;
1290   Wrk * wrk;
1291   int * repr;
1292
1293   char closeapitrace;
1294   FILE * out, * apitrace;
1295   char * prefix;
1296   Cbs * cbs;
1297
1298   LGL * clone;
1299
1300   FltStr * fltstr;
1301 #if !defined(NLGLPICOSAT)
1302   struct { PicoSAT * solver; int res; char chk; } picosat;
1303 #endif
1304 #if !defined(NLGLDRUPLIG)
1305   Druplig * druplig;
1306 #endif
1307 };
1308
1309 /*-------------------------------------------------------------------------*/
1310
1311 #define LT(n) n, n, n, n, n, n, n, n, n, n, n, n, n, n, n, n
1312
1313 static const char lglfloorldtab[256] =
1314 {
1315 // 0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15
1316   -1, 0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3,
1317   LT(4), LT(5), LT(5), LT(6), LT(6), LT(6), LT(6),
1318   LT(7), LT(7), LT(7), LT(7), LT(7), LT(7), LT(7), LT(7)
1319 };
1320
1321 static const uint64_t lglbasevar2funtab[6] = {
1322   0xaaaaaaaaaaaaaaaaull, 0xccccccccccccccccull, 0xf0f0f0f0f0f0f0f0ull,
1323   0xff00ff00ff00ff00ull, 0xffff0000ffff0000ull, 0xffffffff00000000ull,
1324 };
1325
1326 /*-------------------------------------------------------------------------*/
1327
1328 static int lglfloorld (int n) {
1329   assert (n >= 0);
1330   if (n < (1<<8)) return lglfloorldtab[n];
1331   if (n < (1<<16)) return 8 + lglfloorldtab[n>>8];
1332   if (n < (1<<24)) return 16 + lglfloorldtab[n>>16];
1333   return 24 + lglfloorldtab[n>>24];
1334 }
1335
1336 static int lglispow2 (int n) {
1337   assert (0 <= n && n <= INT_MAX);
1338   return !(n & (n - 1));
1339 }
1340
1341 static int lglceilld (int n) {
1342   int res = lglfloorld (n);
1343   if (!lglispow2 (n)) res++;
1344   return res;
1345 }
1346
1347 static int lglceilsqrt32 (int x) {
1348   int l = 0, m, r, mm, rr;
1349 #ifndef NDEBUG
1350   int ll = 0;
1351 #endif
1352   if (x <= 0) return 0;
1353   r = 46340; rr = r*r;
1354   if (x >= rr) return r;
1355   for (;;) {
1356     assert (l < r);
1357     assert (ll < x && x < rr);
1358     if (r - l == 1) return r;
1359     m = (l + r)/2;
1360     mm = m*m;
1361     if (mm == x) return m;
1362     if (mm < x) {
1363       l = m;
1364 #ifndef NDEBUG
1365       ll = mm;
1366 #endif
1367     } else r = m, rr = mm;
1368   }
1369 }
1370
1371 static int lglceilsqrt64 (int x) {
1372   int64_t l = 0, m, r, mm, rr;
1373 #ifndef NDEBUG
1374   int64_t ll = 0;
1375 #endif
1376   if (x <= 0) return 0;
1377   r = 3037000499ll; rr = r*r;
1378   if (x >= rr) return r;
1379   for (;;) {
1380     assert (l < r);
1381     assert (ll < x && x < rr);
1382     if (r - l == 1) return r;
1383     m = (l + r)/2;
1384     mm = m*m;
1385     if (mm == x) return m;
1386     if (mm < x) {
1387       l = m;
1388 #ifndef NDEBUG
1389       ll = mm;
1390 #endif
1391     } else r = m, rr = mm;
1392   }
1393 }
1394
1395 static void lglchkflt (Flt a) {
1396 #ifndef NDEBUG
1397   assert (a >= 0);
1398   assert (FLTMAX >= (uint64_t) a);
1399 #else
1400   (void) a;
1401 #endif
1402 }
1403
1404 static Exp lglexp (Flt a) {
1405   Exp res = a >> FLTPRC;
1406   assert (0 <= res && res <= EXPMAX);
1407   res -= EXPZRO;
1408   return res;
1409 }
1410
1411 static Mnt lglmnt (Flt a) {
1412   Mnt res = a & MNTMAX;
1413   res |= MNTBIT;
1414   assert (res <= MNTMAX);
1415   return res;
1416 }
1417
1418 static Flt lglflt (Exp e, Mnt m) {
1419   Flt res;
1420   if (!m) return FLTMIN;
1421   if (m < MNTBIT) {
1422     while (!(m & MNTBIT)) {
1423       m <<= 1;
1424       if (e > INT_MIN) e--;
1425       else break;
1426     }
1427   } else {
1428     while (m > MNTMAX) {
1429        m >>= 1;
1430        if (e > INT_MIN) e++;
1431        else break;
1432     }
1433   }
1434   if (e < -EXPZRO) return FLTMIN;
1435   if (e > EXPMAX - EXPZRO) return FLTMAX;
1436   e += EXPZRO;
1437   assert (0 <= e && e <= EXPMAX);
1438   assert (m <= MNTMAX);
1439   assert (m & MNTBIT);
1440   res = m & ~MNTBIT;
1441   res |= ((Flt)e) << FLTPRC;
1442   return res;
1443 }
1444
1445 #ifdef NDBLSCR
1446 static Flt lglrat (unsigned n, unsigned d) {
1447   Mnt m;
1448   Exp e;
1449   if (!n) return FLTMIN;
1450   if (!d) return FLTMAX;
1451   m = n;
1452   e = 0;
1453   while (!(m & (1ull << 63))) m <<= 1, e--;
1454   m /= d;
1455   return lglflt (e, m);
1456 }
1457 #endif
1458
1459 #ifndef NDEBUG
1460 double lglflt2dbl (Flt a) {
1461   return lglmnt (a) * pow (2.0, lglexp (a));
1462 }
1463 #endif
1464
1465 #ifdef NDBLSCR
1466 static const char * lgll2str (LGL * lgl, Flt a) {
1467   assert (lgl->fltstr);
1468   lgl->fltstr->current++;
1469   if (lgl->fltstr->current == MAXFLTSTR) lgl->fltstr->current = 0;
1470   sprintf (lgl->fltstr->str[lgl->fltstr->current], "%lld", (LGLL) a);
1471   return lgl->fltstr->str[lgl->fltstr->current];
1472 }
1473 #endif
1474
1475 static const char * lglflt2str (LGL * lgl, Flt a) {
1476   double d, e;
1477   assert (lgl->fltstr);
1478   if (a == FLTMIN) return "0";
1479   if (a == FLTMAX) return "inf";
1480   d = lglmnt (a);
1481   d /= 4294967296ll;
1482   e = lglexp (a);
1483   e += 32;
1484   lgl->fltstr->current++;
1485   if (lgl->fltstr->current == MAXFLTSTR) lgl->fltstr->current = 0;
1486   sprintf (lgl->fltstr->str[lgl->fltstr->current], "%.6fd%+03.0f", d, e);
1487   return lgl->fltstr->str[lgl->fltstr->current];
1488 }
1489
1490 static Flt lgladdflt (Flt a, Flt b) {
1491   Exp e, f, g;
1492   Mnt m, n, o;
1493   lglchkflt (a);
1494   lglchkflt (b);
1495   if (a == FLTMAX) return FLTMAX;
1496   if (b == FLTMAX) return FLTMAX;
1497   if (a == FLTMIN) return b;
1498   if (b == FLTMIN) return a;
1499   e = lglexp (a);
1500   f = lglexp (b);
1501   if (e < f) g = e, e = f, f = g, o = a, a = b, b = o;
1502   m = lglmnt (a);
1503   n = lglmnt (b);
1504   m += n >> (e - f);
1505   return lglflt (e, m);
1506 }
1507
1508 static Flt lglmulflt (Flt a, Flt b) {
1509   Exp e, ea, eb;
1510   Mnt m, ma, mb;
1511   lglchkflt (a);
1512   lglchkflt (b);
1513   if (a == FLTMAX) return FLTMAX;
1514   if (b == FLTMAX) return FLTMAX;
1515   if (a == FLTMIN) return FLTMIN;
1516   if (b == FLTMIN) return FLTMIN;
1517   ea = lglexp (a); eb = lglexp (b);
1518   if (ea > 0 && eb > 0 && (INT_MAX - ea < eb)) return FLTMAX;
1519   e = ea + eb;
1520   if (e > EXPMAX - EXPZRO - 32) return FLTMAX;
1521   e += 32;
1522   ma = lglmnt (a); mb = lglmnt (b);
1523   ma >>= 1; mb >>= 1;
1524   m = ma * mb;
1525   assert (3ull << 62);
1526   m >>= 30;
1527   return lglflt (e, m);
1528 }
1529
1530 #ifdef NDBLSCR
1531 static Flt lglshflt (Flt a, int s) {
1532   Exp e;
1533   Mnt m;
1534   if (a == FLTMAX) return FLTMAX;
1535   if (a == FLTMIN) return FLTMIN;
1536   assert (0 <= s);
1537   e = lglexp (a);
1538   if (e < INT_MIN + s) return FLTMIN;
1539   e -= s;
1540   m = lglmnt (a);
1541   return lglflt (e, m);
1542 }
1543 #endif
1544
1545 /*------------------------------------------------------------------------*/
1546 #ifdef NDBLSCR
1547
1548 static const char * lglscr2str (LGL * lgl, Scr scr) {
1549   if (lgl->opts->score.val == LGL_SCORE_EVSIDS ||
1550       lgl->opts->score.val == LGL_SCORE_AVG) return lglflt2str (lgl, scr);
1551   else return lgll2str (lgl, scr);
1552 }
1553
1554 static Scr lgladdscr (Scr a, Scr b) { return lgladdflt (a, b); }
1555 static Scr lglmulscr (Scr a, Scr b) { return lglmulflt (a, b); }
1556
1557 #else /* !NDBLSCR */
1558
1559 static const char * lgldbl2str (LGL * lgl, double d) {
1560   assert (lgl->fltstr);
1561   lgl->fltstr->current++;
1562   if (lgl->fltstr->current == MAXFLTSTR) lgl->fltstr->current = 0;
1563   sprintf (lgl->fltstr->str[lgl->fltstr->current], "%g", d);
1564   return lgl->fltstr->str[lgl->fltstr->current];
1565 }
1566
1567 static const char * lglscr2str (LGL * lgl, Scr scr) {
1568   return lgldbl2str (lgl, scr);
1569 }
1570
1571 static Scr lgladdscr (Scr a, Scr b) { return a + b; }
1572 static Scr lglmulscr (Scr a, Scr b) { return a * b; }
1573
1574 #endif
1575 /*------------------------------------------------------------------------*/
1576
1577 static void lglwrn (LGL * lgl, const char * msg, ...) {
1578   va_list ap;
1579   fprintf (lgl->out, "*** warning in '%s': ", __FILE__);
1580   va_start (ap, msg);
1581   vfprintf (lgl->out, msg, ap);
1582   va_end (ap);
1583   fputc ('\n', lgl->out);
1584   fflush (lgl->out);
1585 }
1586
1587 static void lgldie (LGL * lgl, const char * msg, ...) {
1588   va_list ap;
1589   fprintf (lgl->out, "*** internal error in '%s': ", __FILE__);
1590   va_start (ap, msg);
1591   vfprintf (lgl->out, msg, ap);
1592   va_end (ap);
1593   fputc ('\n', lgl->out);
1594   fflush (lgl->out);
1595   exit (0);
1596 }
1597
1598 static void lglabort (LGL * lgl) {
1599   if (!lgl) exit (1);
1600   if (lgl->opts && lgl->opts->sleeponabort.val) {
1601     fprintf (stderr,
1602 "liblgl.a: Process %d will sleep for %d seconds "
1603 " before continuing with 'lglabort' procedure.\n",
1604       getpid (), lgl->opts->sleeponabort.val);
1605     sleep (lgl->opts->sleeponabort.val);
1606   }
1607   if (lgl->cbs && lgl->cbs->onabort)
1608     lgl->cbs->onabort (lgl->cbs->abortstate);
1609   if (lgl->opts && lgl->opts->exitonabort.val) exit (1);
1610   abort ();
1611 }
1612
1613 static const char * lglprefix (LGL * lgl) {
1614   return lgl && lgl->prefix ? lgl->prefix : "c (LGL HAS NO PREFIX YET) ";
1615 }
1616
1617 static int lglmsgstart (LGL * lgl, int level) {
1618 #ifndef NLGLOG
1619   if (lgl->opts->log.val <= 0)
1620 #endif
1621   if (lgl->opts->verbose.val < level) return 0;
1622   if (lgl->cbs && lgl->cbs->msglock.lock)
1623     lgl->cbs->msglock.lock (lgl->cbs->msglock.state);
1624   fputs (lglprefix (lgl), lgl->out);
1625   if (lgl->tid >= 0) fprintf (lgl->out, "%d ", lgl->tid);
1626   return 1;
1627 }
1628
1629 static void lglmsgend (LGL * lgl) {
1630   fputc ('\n', lgl->out);
1631   fflush (lgl->out);
1632   if (lgl->cbs && lgl->cbs->msglock.unlock)
1633     lgl->cbs->msglock.unlock (lgl->cbs->msglock.state);
1634 }
1635
1636 static void lglprt (LGL * lgl, int level, const char * msg, ...) {
1637   va_list ap;
1638 #ifndef NLGLOG
1639   if (lgl->opts->log.val <= 0)
1640 #endif
1641   if (lgl->opts->verbose.val < level) return;
1642   lglmsgstart (lgl, level);
1643   va_start (ap, msg);
1644   vfprintf (lgl->out, msg, ap);
1645   va_end (ap);
1646   lglmsgend (lgl);
1647 }
1648
1649 #ifndef NLGLOG
1650 static void lglogstart (LGL * lgl, int level, const char * msg, ...) {
1651   va_list ap;
1652   assert (lgl->opts->log.val >= level);
1653   if (lgl->cbs && lgl->cbs->msglock.lock)
1654     lgl->cbs->msglock.lock (lgl->cbs->msglock.state);
1655   fputs (lglprefix (lgl), lgl->out);
1656   if (lgl->tid >= 0) fprintf (lgl->out, "%d ", lgl->tid);
1657   fprintf (lgl->out, "LOG%d %d ", level, lgl->level);
1658   va_start (ap, msg);
1659   vfprintf (lgl->out, msg, ap);
1660   va_end (ap);
1661 }
1662
1663 #define lglogend lglmsgend
1664 #endif
1665
1666 /*------------------------------------------------------------------------*/
1667
1668 void lglsetid (LGL * lgl, int tid, int tids) {
1669   REQINITNOTFORKED ();
1670   ABORTIF (tid < 0, "negative id");
1671   ABORTIF (tid >= tids, "id exceed number of ids");
1672   lgl->tid = tid;
1673   lgl->tids = tids;
1674 }
1675
1676 /*------------------------------------------------------------------------*/
1677
1678 static void lglinc (LGL * lgl, size_t bytes) {
1679   lgl->stats->bytes.current += bytes;
1680   if (lgl->stats->bytes.max < lgl->stats->bytes.current) {
1681     lgl->stats->bytes.max = lgl->stats->bytes.current;
1682     LOG (5, "maximum allocated %ld bytes", lgl->stats->bytes.max);
1683   }
1684 }
1685
1686 static void lgldec (LGL * lgl, size_t bytes) {
1687   assert (lgl->stats->bytes.current >= bytes);
1688   lgl->stats->bytes.current -= bytes;
1689 }
1690
1691 static void * lglnew (LGL * lgl, size_t bytes) {
1692   void * res;
1693   if (!bytes) return 0;
1694   if (lgl->mem->alloc) res = lgl->mem->alloc (lgl->mem->state, bytes);
1695   else res = malloc (bytes);
1696   if (!res) lgldie (lgl, "out of memory allocating %ld bytes", bytes);
1697   assert (res);
1698   LOG (5, "allocating %p with %ld bytes", res, bytes);
1699   lglinc (lgl, bytes);
1700   if (res) memset (res, 0, bytes);
1701   return res;
1702 }
1703
1704 static void lgldel (LGL * lgl, void * ptr, size_t bytes) {
1705   if (!ptr) { assert (!bytes); return; }
1706   lgldec (lgl, bytes);
1707   LOG (5, "freeing %p with %ld bytes", ptr, bytes);
1708   if (lgl->mem->dealloc) lgl->mem->dealloc (lgl->mem->state, ptr, bytes);
1709   else free (ptr);
1710 }
1711
1712 static void * lglrsz (LGL * lgl, void * ptr, size_t old, size_t new) {
1713   void * res;
1714   assert (!ptr == !old);
1715   if (!ptr) return lglnew (lgl, new);
1716   if (!new) { lgldel (lgl, ptr, old); return 0; }
1717   if (old == new) return ptr;
1718   lgldec (lgl, old);
1719   if (lgl->mem->realloc)
1720     res = lgl->mem->realloc (lgl->mem->state, ptr, old, new);
1721   else res = realloc (ptr, new);
1722   if (!res)
1723     lgldie (lgl, "out of memory reallocating %ld to %ld bytes", old, new);
1724   assert (res);
1725   LOG (5, "reallocating %p to %p from %ld to %ld bytes", ptr, res, old, new);
1726   lglinc (lgl, new);
1727   if (new > old) memset (res + old, 0, new - old);
1728   return res;
1729 }
1730
1731 /*------------------------------------------------------------------------*/
1732
1733 static char * lglstrdup (LGL * lgl, const char * str) {
1734   char * res;
1735   NEW (res, strlen (str) + 1);
1736   return strcpy (res, str);
1737 }
1738
1739 static void lgldelstr (LGL * lgl, char * str) {
1740   DEL (str, strlen (str) + 1);
1741 }
1742
1743 /*------------------------------------------------------------------------*/
1744
1745 static void lglinitcbs (LGL * lgl) {
1746   if (!lgl->cbs) NEW (lgl->cbs, 1);
1747 }
1748
1749 void lglonabort (LGL * lgl, void * abortstate, void (*onabort)(void*)) {
1750   REQINITNOTFORKED ();
1751   lglinitcbs (lgl);
1752   lgl->cbs->abortstate = abortstate;
1753   lgl->cbs->onabort = onabort;
1754 }
1755
1756 void lglseterm (LGL * lgl, int (*fun)(void*), void * state) {
1757   REQINITNOTFORKED ();
1758   lglinitcbs (lgl);
1759   lgl->cbs->term.fun = fun;
1760   lgl->cbs->term.state = state;
1761 }
1762
1763 void lglsetproduceunit (LGL * lgl, void (*fun) (void*, int), void * state) {
1764   REQINITNOTFORKED ();
1765   lglinitcbs (lgl);
1766   lgl->cbs->units.produce.fun = fun;
1767   lgl->cbs->units.produce.state = state;
1768 }
1769
1770 void lglsetconsumeunits (LGL * lgl,
1771                          void (*fun) (void*, int **, int **),
1772                          void * state) {
1773   REQINITNOTFORKED ();
1774   lglinitcbs (lgl);
1775   lgl->cbs->units.consume.fun =  fun;
1776   lgl->cbs->units.consume.state = state;
1777 }
1778
1779 void lglsetconsumedunits (LGL * lgl,
1780                           void (*fun) (void*, int), void * state) {
1781   REQINITNOTFORKED ();
1782   lglinitcbs (lgl);
1783   lgl->cbs->units.consumed.fun = fun;
1784   lgl->cbs->units.consumed.state = state;
1785 }
1786
1787 void lglsetproducecls (LGL * lgl,
1788                        void (*fun) (void*, int *, int), void * state) {
1789   REQINITNOTFORKED ();
1790   lglinitcbs (lgl);
1791   lgl->cbs->cls.produce.fun = fun;
1792   lgl->cbs->cls.produce.state = state;
1793 }
1794
1795 void lglsetconsumecls (LGL * lgl,
1796                        void (*fun) (void*, int **, int *),
1797                        void * state) {
1798   REQINITNOTFORKED ();
1799   lglinitcbs (lgl);
1800   lgl->cbs->cls.consume.fun =  fun;
1801   lgl->cbs->cls.consume.state = state;
1802 }
1803
1804 void lglsetconsumedcls (LGL * lgl,
1805                         void (*fun) (void*, int), void * state) {
1806   REQINITNOTFORKED ();
1807   lglinitcbs (lgl);
1808   lgl->cbs->cls.consumed.fun = fun;
1809   lgl->cbs->cls.consumed.state = state;
1810 }
1811
1812 void lglsetlockeq (LGL * lgl, int * (*fun)(void*), void * state) {
1813   REQINITNOTFORKED ();
1814   lglinitcbs (lgl);
1815   lgl->cbs->eqs.lock.fun = fun;
1816   lgl->cbs->eqs.lock.state = state;
1817 }
1818
1819 void lglsetunlockeq (LGL * lgl, void (*fun)(void*,int,int), void * state) {
1820   REQINITNOTFORKED ();
1821   lglinitcbs (lgl);
1822   lgl->cbs->eqs.unlock.fun = fun;
1823   lgl->cbs->eqs.unlock.state = state;
1824 }
1825
1826 void lglsetmsglock (LGL * lgl,
1827                     void (*lock)(void*), void (*unlock)(void*),
1828                     void * state) {
1829   REQINITNOTFORKED ();
1830   lglinitcbs (lgl);
1831   lgl->cbs->msglock.lock = lock;
1832   lgl->cbs->msglock.unlock = unlock;
1833   lgl->cbs->msglock.state = state;
1834 }
1835
1836 void lglsetime (LGL * lgl, double (*time)(void)) {
1837   REQINITNOTFORKED ();
1838   lglinitcbs (lgl);
1839   lgl->cbs->getime = time;
1840 }
1841
1842 /*------------------------------------------------------------------------*/
1843
1844 static int lglfullstk (Stk * s) { return s->top == s->end; }
1845 static int lglmtstk (Stk * s) { return s->top == s->start; }
1846 static size_t lglcntstk (Stk * s) { return s->top - s->start; }
1847 static size_t lglszstk (Stk * s) { return s->end - s->start; }
1848
1849 static int lglpeek (Stk * s, int pos) {
1850   assert (0 <= pos && pos < lglszstk (s));
1851   return s->start[pos];
1852 }
1853
1854 static void lglpoke (Stk * s, int pos, int val) {
1855   assert (0 <= pos && pos <= lglszstk (s));
1856   s->start[pos] = val;
1857 }
1858
1859 static void lglenlstk (LGL * lgl, Stk * s) {
1860   size_t old_size = lglszstk (s);
1861   size_t new_size = old_size ? 2 * old_size : 1;
1862   size_t count = lglcntstk (s);
1863   RSZ (s->start, old_size, new_size);
1864   s->top = s->start + count;
1865   s->end = s->start + new_size;
1866 }
1867
1868 static void lglrelstk (LGL * lgl, Stk * s) {
1869   DEL (s->start, lglszstk (s));
1870   CLRPTR (s);
1871 }
1872
1873 static void lglshrstk (LGL * lgl, Stk * s, int new_size) {
1874   size_t old_size, count = lglcntstk (s);
1875   assert (new_size >= 0);
1876   assert (count <= new_size);
1877   if (new_size > 0) {
1878     old_size = lglszstk (s);
1879     RSZ (s->start, old_size, new_size);
1880     s->top = s->start + count;
1881     s->end = s->start + new_size;
1882   } else lglrelstk (lgl, s);
1883 }
1884
1885 static void lglfitstk (LGL * lgl, Stk * s) {
1886   lglshrstk (lgl, s, lglcntstk (s));
1887 }
1888
1889 static void lglpushstk (LGL * lgl, Stk * s, int elem) {
1890   if (lglfullstk (s)) lglenlstk (lgl, s);
1891   *s->top++ = elem;
1892 }
1893
1894 static void lglrmstk (Stk * s, int elem) {
1895   int * p, * q;
1896   for (p = s->start; p < s->top; p++)
1897     if (*p == elem) break;
1898   assert (p < s->top);
1899   q = p++;
1900   while (p < s->top)
1901     *q++ = *p++;
1902   s->top = q;
1903 }
1904
1905 static int lglpopstk (Stk * s) { assert (!lglmtstk (s)); return *--s->top; }
1906
1907 static int lgltopstk (Stk * s) { assert (!lglmtstk (s)); return s->top[-1]; }
1908
1909 static void lglrststk (Stk * s, int newsz) {
1910   assert (0 <= newsz && newsz <= lglcntstk (s));
1911   s->top = s->start + newsz;
1912 }
1913
1914 static void lglclnstk (Stk * s) { lglrststk (s, 0); }
1915
1916 /*------------------------------------------------------------------------*/
1917
1918 static void lgltrapi (LGL * lgl, const char * msg, ...) {
1919   va_list ap;
1920   assert (lgl->apitrace);
1921   va_start (ap, msg);
1922   vfprintf (lgl->apitrace, msg, ap);
1923   va_end (ap);
1924   fputc ('\n', lgl->apitrace);
1925 }
1926
1927 static void lglopenapitrace (LGL * lgl, const char * name) {
1928   FILE * file;
1929   char * cmd;
1930   int len;
1931   len = strlen (name);
1932   if (len >= 3 && !strcmp (name + len - 3, ".gz")) {
1933     len += 20;
1934     NEW (cmd, len);
1935     sprintf (cmd, "gzip -c > %s", name);
1936     file = popen (cmd, "w");
1937     DEL (cmd, len);
1938     if (file) lgl->closeapitrace = 2;
1939   } else {
1940     file = fopen (name, "w");
1941     if (file) lgl->closeapitrace = 1;
1942   }
1943   if (file) lgl->apitrace = file;
1944   else lglwrn (lgl, "can not write API trace to '%s'", name);
1945   TRAPI ("init");
1946 }
1947
1948 void lglwtrapi (LGL * lgl, FILE * apitrace) {
1949   REQUIRE (UNUSED);
1950   ABORTIF (lgl->apitrace, "can only write one API trace");
1951   lgl->apitrace = apitrace;
1952   TRAPI ("init");
1953 }
1954
1955 /*------------------------------------------------------------------------*/
1956 #if !defined(NLGLPICOSAT) && !defined(NDEBUG)
1957
1958 static void lglpicosatinit (LGL * lgl) {
1959   if (lgl->picosat.solver) return;
1960   lgl->picosat.solver = picosat_init ();
1961   picosat_set_prefix (lgl->picosat.solver, "c PST ");
1962   lgl->picosat.chk = 1;
1963   picosat_add (lgl->picosat.solver, 1);
1964   picosat_add (lgl->picosat.solver, 0);
1965   LOG (1, "PicoSAT initialized");
1966 }
1967
1968 #endif
1969 /*------------------------------------------------------------------------*/
1970
1971 static unsigned lglrand (LGL * lgl) {
1972   unsigned res;
1973   lgl->rng.z = 36969 * (lgl->rng.z & 65535) + (lgl->rng.z >> 16);
1974   lgl->rng.w = 18000 * (lgl->rng.w & 65535) + (lgl->rng.w >> 16);
1975   res = (lgl->rng.z << 16) + lgl->rng.w;
1976   LOG (5, "rng %u", res);
1977   return res;
1978 }
1979
1980 /*------------------------------------------------------------------------*/
1981
1982 static int lglmtftk (Ftk * ftk) { return ftk->top == ftk->start; }
1983
1984 static int lglfullftk (Ftk * ftk) { return ftk->top == ftk->end; }
1985
1986 static int lglsizeftk (Ftk * ftk) { return ftk->end - ftk->start; }
1987
1988 static int lglcntftk (Ftk * ftk) { return ftk->top - ftk->start; }
1989
1990 static void lglrelftk (LGL * lgl, Ftk * ftk) {
1991   DEL (ftk->start, lglsizeftk (ftk));
1992   memset (ftk, 0, sizeof *ftk);
1993 }
1994
1995 static void lglenlftk (LGL * lgl, Ftk * ftk) {
1996   int oldsize = lglsizeftk (ftk);
1997   int newsize = oldsize ? 2*oldsize : 1;
1998   int count = lglcntftk (ftk);
1999   RSZ (ftk->start, oldsize, newsize);
2000   ftk->top = ftk->start + count;
2001   ftk->end = ftk->start + newsize;
2002 }
2003
2004 static void lglpushftk (LGL * lgl, Ftk * ftk, Flt f) {
2005   if (lglfullftk (ftk)) lglenlftk (lgl, ftk);
2006   *ftk->top++ = f;
2007 }
2008
2009 static Flt lgltopftk (Ftk * ftk) {
2010   assert (!lglmtftk (ftk));
2011   return ftk->top[-1];
2012 }
2013
2014 static Flt lglpopftk (Ftk * ftk) {
2015   assert (!lglmtftk (ftk));
2016   return *--ftk->top;
2017 }
2018
2019 /*------------------------------------------------------------------------*/
2020
2021 static int lglfullctk (Ctk * ctk) { return ctk->top == ctk->end; }
2022
2023 static int lglsizectk (Ctk * ctk) { return ctk->end - ctk->start; }
2024
2025 static int lglcntctk (Ctk * ctk) { return ctk->top - ctk->start; }
2026
2027 static void lglrelctk (LGL * lgl, Ctk * ctk) {
2028   DEL (ctk->start, lglsizectk (ctk));
2029   memset (ctk, 0, sizeof *ctk);
2030 }
2031
2032 static void lglenlctk (LGL * lgl, Ctk * ctk) {
2033   int oldsize = lglsizectk (ctk);
2034   int newsize = oldsize ? 2*oldsize : 1;
2035   int count = lglcntctk (ctk);
2036   RSZ (ctk->start, oldsize, newsize);
2037   ctk->top = ctk->start + count;
2038   ctk->end = ctk->start + newsize;
2039 }
2040
2041 static void lglpushcontrol (LGL * lgl, int decision) {
2042   Ctk * ctk = &lgl->control;
2043   Ctr * ctr;
2044   if (lglfullctk (ctk)) lglenlctk (lgl, ctk);
2045   ctr = ctk->top++;
2046   ctr->decision = decision;
2047   ctr->used = 0;
2048 }
2049
2050 static void lglpopcontrol (LGL * lgl) {
2051   assert (lgl->control.top > lgl->control.start);
2052   --lgl->control.top;
2053 }
2054
2055 static void lglrstcontrol (LGL * lgl, int count) {
2056   while (lglcntctk (&lgl->control) > count)
2057     lglpopcontrol (lgl);
2058 }
2059
2060 static int lglevelused (LGL * lgl, int level) {
2061   Ctk * ctk = &lgl->control;
2062   Ctr * ctr;
2063   assert (0 < level && level < lglsizectk (ctk));
2064   ctr = ctk->start + level;
2065   return ctr->used;
2066 }
2067
2068 static void lgluselevel (LGL * lgl, int level) {
2069   Ctk * ctk = &lgl->control;
2070   Ctr * ctr;
2071   assert (0 < level && level < lglsizectk (ctk));
2072   ctr = ctk->start + level;
2073   ctr->used = 1;
2074 }
2075
2076 static void lglunuselevel (LGL * lgl, int level) {
2077   Ctk * ctk = &lgl->control;
2078   Ctr * ctr;
2079   assert (0 < level);
2080   assert (level < lglcntctk (ctk));
2081   assert (0 < level);
2082   ctr = ctk->start + level;
2083   assert (ctr->used);
2084   ctr->used = 0;
2085 }
2086
2087 /*------------------------------------------------------------------------*/
2088
2089 static void lglgetenv (LGL * lgl, Opt * opt, const char * lname) {
2090   const char * q, * valstr;
2091   char uname[40], * p;
2092   int newval, oldval;
2093   assert (strlen (lname) + 3 + 1 < sizeof (uname));
2094   uname[0] = 'L'; uname[1] = 'G'; uname[2] = 'L';
2095   p = uname + 3;
2096   for (q = lname; *q; q++) {
2097     assert (p < uname + sizeof uname);
2098     *p++ = toupper (*q);
2099   }
2100   assert (p < uname + sizeof uname);
2101   *p = 0;
2102   valstr = getenv (uname);
2103   if (!valstr) return;
2104   oldval = opt->val;
2105   newval = atoi (valstr);
2106   if (newval < opt->min) newval = opt->min;
2107   if (newval > opt->max) newval = opt->max;
2108   if (newval == oldval) return;
2109   opt->val = newval;
2110   TRAPI ("option %s %d", lname, newval);
2111   COVER (lgl->clone);
2112   if (lgl->clone) lglsetopt (lgl->clone, lname, newval);
2113 }
2114
2115 static void lglchkenv (LGL * lgl) {
2116   extern char ** environ;
2117   char * src, *eos, * dst;
2118   char ** p, * s, * d;
2119   int len;
2120   for (p = environ; (src = *p); p++) {
2121     if (src[0] != 'L' || src[1] != 'G' || src[2] != 'L') continue;
2122     for (eos = src; *eos && *eos != '='; eos++)
2123       ;
2124     len = eos - (src + 3);
2125     NEW (dst, len + 1);
2126     d = dst;
2127     for (s = src + 3; s < eos; s++) *d++ = tolower (*s);
2128     *d = 0;
2129     if (!lglhasopt (lgl, dst) && strcmp (dst, "apitrace"))
2130       lglwrn (lgl, "invalid 'LGL...' environment '%s'", src);
2131     DEL (dst, len + 1);
2132   }
2133 }
2134
2135 #define SETPLAIN(NAME) \
2136 do { \
2137   if (val) lgl->opts->NAME.val = 0; \
2138   else lgl->opts->NAME.val = lgl->opts->NAME.dflt; \
2139 } while (0)
2140
2141 #define SETDRUP SETPLAIN
2142
2143 static void lglsetdrup (LGL * lgl, int val) {
2144   SETDRUP (bca);
2145   SETDRUP (card);
2146   SETDRUP (decompose);
2147   SETDRUP (probe);
2148   SETDRUP (lift);
2149   SETDRUP (cgrclsr);
2150   SETDRUP (gauss);
2151   SETDRUP (mega);
2152   SETDRUP (rdp);
2153   SETDRUP (smallve);
2154   lglprt (lgl, 1, "[drup] drup solving switched %s", val ? "on" : "off");
2155 }
2156
2157 #define SETDRUPLIG SETPLAIN
2158
2159 static void lglsetdruplig (LGL * lgl, int val) {
2160   SETDRUPLIG (bca);
2161   SETDRUPLIG (card);
2162   SETDRUPLIG (decompose);
2163   SETDRUPLIG (probe);
2164   SETDRUPLIG (lift);
2165   SETDRUPLIG (cgrclsr);
2166   SETDRUPLIG (gauss);
2167   SETDRUPLIG (mega);
2168   SETDRUPLIG (rdp);
2169   SETDRUPLIG (smallve);
2170   lglprt (lgl, 1,
2171     "[druplig] druplig checking switched %s",
2172     val ? "on" : "off");
2173 }
2174
2175 static void lglsetplain (LGL * lgl, int val) {
2176   SETPLAIN (bca);
2177   SETPLAIN (bva);
2178   SETPLAIN (block);
2179   SETPLAIN (card);
2180   SETPLAIN (cce);
2181   SETPLAIN (cgrclsr);
2182   SETPLAIN (cliff);
2183   SETPLAIN (decompose);
2184   SETPLAIN (elim);
2185   SETPLAIN (gauss);
2186   SETPLAIN (lift);
2187   SETPLAIN (locs);
2188   SETPLAIN (mega);
2189   SETPLAIN (probe);
2190   SETPLAIN (rdp);
2191   SETPLAIN (ternres);
2192   SETPLAIN (transred);
2193   SETPLAIN (unhide);
2194   lglprt (lgl, 1, "[plain] plain solving switched %s", val ? "on" : "off");
2195 }
2196
2197 #define SETWAIT(NAME) \
2198 do { \
2199   if (val) lgl->opts->NAME.val = lgl->opts->NAME.dflt; \
2200   else lgl->opts->NAME.val = 0; \
2201 } while (0)
2202
2203 static void lglsetwait (LGL * lgl, int val) {
2204   SETWAIT (batewait);
2205   SETWAIT (bcawait);
2206   SETWAIT (blockwait);
2207   SETWAIT (ccewait);
2208   SETWAIT (cgrclsrwait);
2209   SETWAIT (cliffwait);
2210   SETWAIT (elmblkwait);
2211   SETWAIT (gausswait);
2212   SETWAIT (liftwait);
2213   SETWAIT (smallvewait);
2214   SETWAIT (ternreswait);
2215   SETWAIT (transredwait);
2216   SETWAIT (unhidewait);
2217   lglprt (lgl, 1, "[wait] waiting %s", val ? "enabled" : "disabled");
2218 }
2219
2220 static LGL * lglnewlgl (void * mem,
2221                         lglalloc alloc,
2222                         lglrealloc realloc,
2223                         lgldealloc dealloc) {
2224   LGL * lgl = alloc ? alloc (mem, sizeof *lgl) : malloc (sizeof *lgl);
2225   ABORTIF (!lgl, "out of memory allocating main solver object");
2226   CLRPTR (lgl);
2227
2228   lgl->mem = alloc ? alloc (mem, sizeof *lgl->mem) : malloc (sizeof *lgl->mem);
2229   ABORTIF (!lgl->mem, "out of memory allocating memory manager object");
2230
2231   lgl->mem->state = mem;
2232   lgl->mem->alloc = alloc;
2233   lgl->mem->realloc = realloc;
2234   lgl->mem->dealloc = dealloc;
2235
2236   lgl->opts = alloc ? alloc (mem, sizeof (Opts)) : malloc (sizeof (Opts));
2237   ABORTIF (!lgl->opts, "out of memory allocating option manager object");
2238   CLRPTR (lgl->opts);
2239
2240   lgl->stats = alloc ? alloc (mem, sizeof (Stats)) : malloc (sizeof (Stats));
2241   ABORTIF (!lgl->stats, "out of memory allocating statistic counters");
2242   CLRPTR (lgl->stats);
2243
2244   lglinc (lgl, sizeof *lgl);
2245   lglinc (lgl, sizeof *lgl->mem);
2246   lglinc (lgl, sizeof *lgl->opts);
2247   lglinc (lgl, sizeof *lgl->stats);
2248
2249   return lgl;
2250 }
2251
2252 static void lglinitscores (LGL * lgl) {
2253   Scr oldscincf, oldmaxscore = lgl->maxscore;
2254   if (lgl->opts->score.val != LGL_SCORE_EVSIDS) {
2255     lgl->maxscore = (1ll << 60);
2256     if (oldmaxscore != lgl->maxscore)
2257       lglprt (lgl, 1,
2258         "[init-scores] fixed maxium score %s",
2259         lglscr2str (lgl, lgl->maxscore));
2260   } else {
2261     oldscincf = lgl->scincf;
2262 #ifdef NDBLSCR
2263     lgl->scincf = lglrat (1000 + lgl->opts->scincinc.val, 1000);
2264     lgl->maxscore = lglflt (lgl->opts->maxscorexp.val, 1);
2265 #else
2266     lgl->scincf = (1000.0 + lgl->opts->scincinc.val) / 1000.0;
2267     lgl->maxscore = scalbln (1.0, lgl->opts->maxscorexp.val);
2268 #endif
2269     if (oldscincf != lgl->scincf)
2270       lglprt (lgl, 1,
2271         "[init-scores] score increment factor %s (--scincinc=%d)",
2272         lglscr2str (lgl, lgl->scincf), lgl->opts->scincinc.val);
2273
2274     if (oldmaxscore != lgl->maxscore)
2275       lglprt (lgl, 1,
2276         "[init-scores] maxium score limit %s (--maxscorexp=%d)",
2277         lglscr2str (lgl, lgl->maxscore), lgl->opts->maxscorexp.val);
2278   }
2279 }
2280
2281 LGL * lglminit (void * mem,
2282                 lglalloc alloc,
2283                 lglrealloc realloc,
2284                 lgldealloc dealloc) {
2285   const int K = 1000, M = K*K, I = INT_MAX;
2286   const int MG = MAXGLUE, MG0 = MG*10;
2287   const char * apitracename;
2288   LGL * lgl;
2289   int i;
2290
2291   lgl = 0;
2292   ABORTIF (!alloc+!realloc+!dealloc != 0 && !alloc+!realloc+!dealloc != 3,
2293            "inconsistent set of external memory handlers");
2294
2295   assert (sizeof (long) == sizeof (void*));
2296
2297   assert (REMOVED > ((MAXVAR << RMSHFT) | MASKCS | REDCS));
2298   assert (REMOVED > MAXREDLIDX);
2299   assert (REMOVED > MAXIRRLIDX);
2300
2301   assert (MAXREDLIDX == MAXIRRLIDX);
2302   assert (GLUESHFT == RMSHFT);
2303
2304   assert (INT_MAX > ((MAXREDLIDX << GLUESHFT) | GLUEMASK));
2305   assert (INT_MAX > ((MAXIRRLIDX << RMSHFT) | MASKCS | REDCS));
2306
2307   assert (MAXGLUE < POW2GLUE);
2308
2309   lgl = lglnewlgl (mem, alloc, realloc, dealloc);
2310   lgl->tid = -1;
2311
2312   lglpushcontrol (lgl, 0);
2313   assert (lglcntctk (&lgl->control) == lgl->level + 1);
2314
2315   lgl->out = stdout;
2316   lgl->prefix = lglstrdup (lgl, "c ");
2317
2318   apitracename = getenv ("LGLAPITRACE");
2319   if (apitracename) lglopenapitrace (lgl, apitracename);
2320
2321   OPT(0,abstime,0,0,1,"print absolute time when reporting");
2322   OPT(0,actavgmax,3*MG0/4,0,MG0,"glue average max limit for dyn acts");
2323   OPT(0,actdblarithlim,3,0,MG,"glue lim for dbl arith increase");
2324   OPT(0,actgeomlim,2,0,MG,"glue limit for geometric increase");
2325   OPT(0,actgsdul,7,0,MG0,"glue useless standard deviation limit");
2326   OPT(0,acts,2,0,2,"activity based reduction: 0=no,1=enable,2=dyn");
2327   OPT(0,actstdmax,3*MG0/4,0,MG0,"glue std dev max limit for dyn acts");
2328   OPT(0,actstdmin,10,0,MG0,"glue std dev min limit for dyn acts");
2329   OPT(0,actvlim,200*K,0,I,"activity based reduction variable limit");
2330   OPT(0,agile,1,0,2,"agility based restart skipping, 1=std, 2=sinus");
2331   OPT(0,agilelim,30,0,100,"agility limit for restarts");
2332   OPT(0,agilesinint,100*K,1,I,"agility limit sinus interval");
2333   OPT(0,bate,1,0,1,"basic ATE removal during probing");
2334   OPT(0,batewait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2335   OPT(0,bca,1,0,2,"enable blocked clause addition (1=week,2=strong)");
2336   OPT(0,bcamaxeff,10*M,0,I,"BCA maximum number of steps");
2337   OPT(0,bcaminuse,100,0,I,"min number of literals required to be usable");
2338   OPT(0,bcawait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2339   OPT(0,bva,0,0,1,"enable bounded variable addition (BVA)");
2340   OPT(0,bias,2,-1,2,"decision order initial bias (0=no,2=cw)");
2341   OPT(0,binlocsdel,10,0,1000,"delay local seach after learning binary clause");
2342   OPT(0,binsimpdel,2,0,1000,"delay simp after learning binary clause");
2343   OPT(0,bkwdscale,2,1,1000,"backward steps scaled vs elimination steps");
2344   OPT(0,blkboost,10,1,10000,"initial BCE boost");
2345   OPT(0,blkboostvlim,1000000,0,I,"init BCE boost variable limit");
2346   OPT(0,blkclslim,1*M,3,I,"max blocked clause size");
2347   OPT(0,blklarge,1,0,1,"BCE of large clauses");
2348   OPT(0,blkmaxeff,800*M,-1,I,"max effort in BCE (-1=unlimited)");
2349   OPT(0,blkmineff,50*M,0,I,"min effort in BCE");
2350   OPT(0,blkocclim1,100*K,1,I,"one-sided max occ of BCE");
2351   OPT(0,blkocclim,1*M,3,I,"max occ in BCE");
2352   OPT(0,blkocclim2,10*K,2,I,"two-sided max occ of BCE");
2353   OPT(0,blkreleff,100,0,K,"rel effort in BCE");
2354   OPT(0,blkrtc,0,0,1,"run BCE until completion");
2355   OPT(0,blksched2b2,0,0,1,"BCE schedule 2x2 first");
2356   OPT(0,blkschedmin,0,0,1,"BCE schedule based on minimum of occurrences");
2357   OPT(0,blkschedprod,0,0,1,"BCE schedule based on product too");
2358   OPT(0,blkschedpure,1,0,1,"BCE schedule pure literals first");
2359   OPT(0,blkschedsum,1,0,1,"BCE schedule based on sum of occurrences too");
2360   OPT(0,blksmall,1,0,1,"BCE of small clauses");
2361   OPT(0,blksuccesslim,10*K,0,I,"BCE success limit");
2362   OPT(0,blksuccessrat,1000,1,I,"BCE success ratio");
2363   OPT(0,block,1,0,1,"blocked clause elimination (BCE)");
2364   OPT(0,blockwait,1,0,1,"wait for BVE");
2365   OPT(0,boost,1,0,1,"enable boosting of preprocessors");
2366   OPT(0,bumpbcplits,0,0,1,"bump unseen but propagated literals");
2367   OPT(0,bumpclslits,0,0,1,"bump literals in minimized clause");
2368   OPT(0,bumpseenaftermin,0,0,1,"bump seen after minimization");
2369   OPT(0,bumpseenbeforemin,1,0,1,"bump seen before minimization");
2370   OPT(0,bumpseenlits,1,0,1,"bump seen literals");
2371   OPT(0,bumpseenminsize,3,0,I,"minimum 1st UIP clause for bumping seen");
2372   OPT(0,card,1,0,1,"cardinality constraint reasoning");
2373   OPT(0,cardcut,2,0,2,"1=gomoroy-cuts,2=strengthen");
2374   OPT(0,cardexpam1,3,2,I,"min length of exported at-most-one constraint");
2375   OPT(0,cardglue,0,-1,MAXGLUE,"use lrg red cls too (-1=irr,0=moved,...)");
2376   OPT(0,cardignused,0,0,1,"ignored already used literals in extraction");
2377   OPT(0,cardmaxeff,300*M,-1,I,"max effort for cardmineff reasoning");
2378   OPT(0,cardmaxlen,1000,0,I,"maximal length of cardinality constraints");
2379   OPT(0,cardmineff,2*M,0,I,"min effort for cardmineff reasoning");
2380   OPT(0,cardminlen,3,0,I,"minimal length of (initial) card constraints");
2381   OPT(0,cardocclim1,300,0,I,"one-sided cardinality constraints occ limit");
2382   OPT(0,cardocclim2,15,0,I,"two-sided cardinality constraints occ limit");
2383   OPT(0,cardreleff,5,0,10*K,"rel effort for cardinality reasoning");
2384   OPT(0,cardreschedint,10,1,I,"reschedule variable for card reasoning");
2385   OPT(0,carduse,2,0,3,"use clauses (1=oneside,2=bothsidetoo,3=anyside)");
2386   OPT(0,cardwait,0,0,2,"wait for BCE (1) and/or BVE (2)");
2387   OPT(0,cce2wait,1,0,I,"wait for ATE to finish before doing ABCE");
2388   OPT(0,cce,3,0,3,"covered clause elimination (1=ate,2=abce,3=acce)");
2389   OPT(0,cceboost,10,1,1000,"initial CCE boost");
2390   OPT(0,cceboostvlim,1000000,0,I,"initial CCE boost variable limit");
2391   OPT(0,cce3wait,2,0,I,"wait for ABCE to finish before doing ACCE");
2392   OPT(0,ccemaxeff,I,-1,I,"max effort in covered clause elimination");
2393   OPT(0,ccemineff,30*M,0,I,"min effort in covered clause elimination");
2394   OPT(0,cceonlyifstuck,0,0,1,"ABCE+ACCE only if elm+blk stuck");
2395   OPT(0,ccereleff,20,0,K,"rel effort in covered clause elimination");
2396   OPT(0,ccertc,0,0,1,"run CCE until completition");
2397   OPT(0,ccesuccesslim,10*K,0,I,"CCE success limit");
2398   OPT(0,ccesuccessrat,1000,1,I,"CCE success ratio");
2399   OPT(0,ccewait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2400   OPT(0,cgrclsr,1,0,1,"gate extraction and congruence closure");
2401   OPT(0,cgrclsrwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2402   OPT(0,cgreleff,1,0,10*K,"rel effort in congruence closure");
2403   OPT(0,cgrextand,1,0,1,"extract and gates");
2404   OPT(0,cgrexteq,1,0,1,"extract equivalences");
2405   OPT(0,cgrextite,1,0,1,"extract ite gates");
2406   OPT(0,cgrextunits,1,0,1,"extract units");
2407   OPT(0,cgrextxor,1,0,1,"extract xor gates");
2408   OPT(0,cgrmaxeff,8*M,-1,I,"max effort in congruence closure");
2409   OPT(0,cgrmaxority,20,2,30,"maximum xor arity to be extracted");
2410   OPT(0,cgrmineff,200*K,0,I,"min effort in congruence closure");
2411   OPT(0,cintinc,20*K,10,M,"inprocessing conflict interval increment");
2412   OPT(0,cintincdiv,1,0,3,"cintinc reduce policy: 0=no,1=div1,2=div2,3=heur");
2413   OPT(0,cintmaxhard,10*M,-1,I,"hard max conflict interval limit");
2414   OPT(0,cintmaxsoft,1*M,-1,I,"soft max conflict interval limit");
2415   OPT(0,cliff,1,0,1,"cliffing");
2416   OPT(0,cliffmaxeff,100*M,-1,I,"max effort in cliffing");
2417   OPT(0,cliffmineff,10*M,0,I,"min effort in cliffing");
2418   OPT(0,cliffreleff,8,0,10*K,"rel effort in cliffing");
2419   OPT(0,cliffwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2420   OPT(0,clim,-1,-1,I,"conflict limit");
2421   OPT(0,compact,0,0,2,"compactify after 'lglsat/lglsimp' (1=UNS,2=SAT)");
2422   OPT(0,deco,1,0,2,"learn decision-only clauses too (2=all-decisions)");
2423   OPT(0,decolim,30,0,I,"decision-only clauses glue limit");
2424   OPT(0,decompose,1,0,1,"enable decompose");
2425   OPT(0,defragfree,50,10,K,"defragmentation free watches limit");
2426   OPT(0,defragint,10*M,100,I,"defragmentation pushed watches interval");
2427   OPT(0,delmax,10,0,10,"maximum delay");
2428   OPT(0,dlim,-1,-1,I,"decision limit");
2429   OPT(0,drup,0,0,1,"print DRUP proof");
2430 #if 1
2431   OPT(0,druplig,0,0,1,"check proof through Druplig internally");
2432 #else
2433   OPT(0,druplig,1,1,1,"check proof through Druplig internally");
2434 #endif
2435   OPT(0,elim,1,0,1,"bounded variable eliminiation (BVE)");
2436   OPT(0,elmaxeff,800*M,-1,I,"max effort in BVE (-1=unlimited)");
2437   OPT(0,elmblk,1,0,1,"enable BCE during BVE");
2438   OPT(0,elmblkwait,1,0,1,"wait for BVE to be completed once");
2439   OPT(0,elmboost,40,1,1000,"initial elimination boost");
2440   OPT(0,elmclslim,1*M,3,I,"max antecendent size in elimination");
2441   OPT(0,elmfull,0,0,1,"no elimination limits");
2442   OPT(0,elmineff,20*M,0,I,"min effort in BVE");
2443   OPT(0,elmlitslim,200,0,I,"one side literals limit for elimination");
2444   OPT(0,elmocclim1,1000,1,I,"one-sided max occ of BVE");
2445   OPT(0,elmocclim,1*M,3,I,"max occurrences in BVE");
2446   OPT(0,elmocclim2,100,2,I,"two-sided max occ of BVE");
2447   OPT(0,elmreleff,200,0,10*K,"rel effort in BVE");
2448   OPT(0,elmroundlim,3,1,I,"variable elimination rounds limit");
2449   OPT(0,elmrtc,0,0,1,"run BVE until completion");
2450   OPT(0,elmsched2b2,0,0,1,"BVE schedule 2x2 first");
2451   OPT(0,elmschediff,0,0,1,"BVE schedule based on diff of occurrences too");
2452   OPT(0,elmschedmin,0,0,1,"BVE schedule based on minimum of occurrences");
2453   OPT(0,elmschedprod,0,0,1,"BVE schedule based on product too");
2454   OPT(0,elmschedpure,1,0,1,"BVE schedule pure literals first");
2455   OPT(0,elmschedsum,1,0,1,"BVE schedule based on sum of occurrences too");
2456   OPT(0,elmsuccesslim,1000,0,I,"BVE success limit");
2457   OPT(0,elmsuccessrat,1000,1,I,"BVE success ratio");
2458   OPT(0,exitonabort,0,0,1,"exit instead abort after internal error");
2459   OPT(0,factmax,100000,1,I,"maximum factor");
2460   OPT(0,factor,3,0,3,"{cls,occ}lim factors (0=const1,1=ld,2=lin,3=sqr)");
2461   OPT(0,flipdur,10,1,I,"flipping duration in number of conflicts");
2462   OPT(0,flipint,10,0,I,"flipping interval in number top level decision");
2463   OPT(0,flipldmod,4,0,30,"flipping phase log2 of mod");
2464   OPT(0,fliplevels,6,0,30,"flipping decision levels");
2465   OPT(0,flipping,1,0,1,"enable point flipping");
2466   OPT(0,fliptop,1,0,1,"flipping only at the top level");
2467   OPT(0,flipvlim,100*K,0,I,"no flipping beyond this number vars");
2468   OPT(0,force,0,0,I,"reorder variables with force algorithm");
2469   OPT(0,gauss,1,0,1,"enable gaussian elimination");
2470   OPT(0,gaussexptrn,1,0,1,"export trn cls from gaussian elimination");
2471   OPT(0,gaussextrall,1,0,1,"extract all xors (with duplicates)");
2472   OPT(0,gaussmaxeff,50*M,-1,I,"max effort in gaussian elimination");
2473   OPT(0,gaussmaxor,20,2,64,"maximum xor size in gaussian elimination");
2474   OPT(0,gaussmineff,2*M,0,I,"min effort in gaussian elimination");
2475   OPT(0,gaussreleff,2,0,10*K,"rel effort in gaussian elimination");
2476   OPT(0,gausswait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2477   OPT(0,gluekeep,3,0,I,"keep clauses with this original glue");
2478   OPT(0,gluescale,4,1,4,"glue scaling: 1=linear,2=sqrt,3=ld,4=hybrid");
2479   OPT(0,import,1,0,1,"import external indices and map them");
2480   OPT(0,incredcint,1,1,I,"incremental reduce conflict interval");
2481   OPT(0,incredconfslim,0,0,100,"incremental reduce conflict limit");
2482   OPT(0,incsavevisits,0,0,1,"incremental start new visits counter");
2483   OPT(0,inprocessing,1,0,1,"enable inprocessing");
2484   OPT(0,irrlim,1,0,1,"use irredundant clauses as limit for simps");
2485   OPT(0,itlocsdel,100,0,100*K,"local search delay after iteration");
2486   OPT(0,itsimpdel,20,0,100*K,"simplification delay after iteration");
2487   OPT(0,jwhred,1,0,1,"compute JWH score based on redundant clauses too");
2488   OPT(0,keepmaxglue,1,0,1,"keep maximum glue clauses");
2489   OPT(0,lftmaxeff,20*M,-1,I,"max effort in lifting");
2490   OPT(0,lftmineff,500*K,0,I,"min effort in lifting");
2491   OPT(0,lftreleff,6,0,10*K,"rel effort in lifting");
2492   OPT(0,lftroundlim,5,0,I,"lifting round limit");
2493   OPT(0,lhbr,1,0,1, "enable lazy hyber binary reasoning");
2494   OPT(0,lift,1,0,1,"enable double lookahead lifting");
2495   OPT(0,liftlrg,3,0,I,"consider large clauses with this many unassigned");
2496   OPT(0,liftwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2497   OPT(0,lkhd,2,-1,3, "-1=LOCS,0=LIS,1=JWH,2=TREELOOK,3=LENSUM");
2498   OPT(0,lkhdmisifelmrtc,0,0,1,"MIS if elimination ran to completion");
2499   OPT(0,locs,0,-1,I,"use local search (-1=always otherwise how often)");
2500   OPT(0,locsclim,1*M,0,(I>>8),"clause limit for local search");
2501   OPT(0,locsboost,2,0,100,"initial local search boost");
2502   OPT(0,locscint,10*K,1,I,"conflict interval for LOCS");
2503   OPT(0,locsdec,2,0,2,"bump 1=mostflipped 2=minlits");
2504   OPT(0,locset,2,0,2,"initialize local search phases (1=prev,2=cur)");
2505   OPT(0,locsexport,1,0,1,"export phases from local search");
2506   OPT(0,locsmaxeff,100000,0,I,"max effort in local search");
2507   OPT(0,locsmineff,1000,0,I,"min effort in local search");
2508   OPT(0,locsred,0,0,4,"apply local search on redundant clauses too");
2509   OPT(0,locsreleff,5,0,100,"rel effort in local search");
2510   OPT(0,locsrtc,0,0,1,"run local search until completion");
2511   OPT(0,locsvared,100,0,1000,"max variable reduction for LOCS");
2512   OPT(0,locswait,2,0,2,"wait for BCE(1) and/or BVE(2)");
2513   OPT(0,maxglue,I,0,I,"min glue which is considered as MAXGLUE");
2514   OPT(0,maxscorexp,DEFSCOREXP,7,MAXSCOREXP,"maximum score exponent");
2515   OPT(0,mega,0,0,1,"mega probing through preprocessor look-ahead");
2516   OPT(0,megaint,4,1,I,"mega probing interval");
2517   OPT(0,megawait,2,0,2,"mega probing waiting for BCE / BVE");
2518   OPT(0,memlim,-1,-1,I,"memory limit in MB (-1=no limit)");
2519   OPT(0,minimize,2,0,2,"minimize learned clauses (1=local,2=recursive)");
2520   OPT(0,minlocalgluelim,30,0,I,"glue limit for using local minimization");
2521   OPT(0,minrecgluelim,20,0,I,"glue limit for using recursive minimization");
2522   OPT(0,mocint,1000,1,I,"multiple objectives conflict limit interval");
2523   OPT(0,move,2,0,3,"move redundant cls (1=only-binary,2=ternary,3=all)");
2524   OPT(0,otfs,1,0,1,"enable on-the-fly subsumption");
2525   OPT(0,otfsbump,0,0,2,"bump literals during OTFS (1=conflict,2=drive)");
2526   OPT(0,otfsconf,0,0,1,"count on-the-fly restart as conflict");
2527   OPT(0,penmax,4,0,16,"maximum penalty");
2528   OPT(0,phase,0,-1,1,"default phase (-1=neg,0=JeroslowWang,1=pos)");
2529   OPT(0,phaseflip,0,0,1,"flip Jeroslow Wang phase");
2530   OPT(0,phasegluebit,0,0,I,"Glue-Bit phase selection on these levels");
2531   OPT(0,phaseneginit,0,0,I,"initial zero phase conflict interval");
2532   OPT(0,plain,0,0,1,"plain mode disables all preprocessing");
2533   OPT(0,plim,-1,-1,I,"propagation limit (thousands)");
2534   OPT(0,prbasic,1,0,2,"enable basic probing procedure (1=roots-only)");
2535   OPT(0,prbasicmaxeff,100*M,-1,I,"max effort in basic probing");
2536   OPT(0,prbasicmineff,M,0,I,"min effort in basic probing");
2537   OPT(0,prbasicreleff,10,0,10*K,"rel effort in basic probing");
2538   OPT(0,prbasicroundlim,9,1,I,"basic probing round limit");
2539   OPT(0,prbasicrtc,0,0,1,"run basic probing until completion");
2540   OPT(0,prbrtc,0,0,1,"run all probing until completion");
2541   OPT(0,prbsimple,2,0,3,"simple probing (1=shallow,2=deep,3=touchall)");
2542   OPT(0,prbsimpleboost,10,1,1000,"initial simple probing boost");
2543   OPT(0,prbsimpleliftdepth,2,1,4,"simple probing lifting depth");
2544   OPT(0,prbsimplemaxeff,200*M,-1,I,"max effort in simple probing");
2545   OPT(0,prbsimplemineff,2*M,0,I,"min effort in simple probing");
2546   OPT(0,prbsimplereleff,40,0,10*K,"rel effort in simple probing");
2547   OPT(0,prbsimplertc,0,0,1,"run simple probing until completion");
2548   OPT(0,probe,1,0,1,"enable probing");
2549   OPT(0,psm,3,0,3,"use PSM metric (1=afteract,2=afterglue,3=first");
2550   OPT(0,pure,1,0,1,"enable pure literal elimination during BCE");
2551   OPT(0,randec,0,0,1,"enable random decisions");
2552   OPT(0,randecflipint,0,0,I,"random decision flip phase interval");
2553   OPT(0,randecint,1000,2,I/2,"random decision interval");
2554   OPT(0,rdp,0,0,3,"random DP (2=redbin,3=redtrn");
2555   OPT(0,rdpclslim,3,0,I,"random DP resolvent size limit");
2556   OPT(0,rdplim,100,0,200,"limit #resolvents in percent original clauses");
2557   OPT(0,rdpmaxeff,10*M,-1,I,"max effort in RDP");
2558   OPT(0,rdpmineff,10*K,0,I,"min effort in RDP");
2559   OPT(0,rdpmodelm,0,0,1,"use model elimination in RDP");
2560   OPT(0,rdpreleff,2,0,10*K,"rel effort in RDP");
2561   OPT(0,rdpwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2562   OPT(0,redfixed,0,0,1,"keep a fixed size of learned clauses");
2563   OPT(0,redinoutinc,100,1,1000,"reduce inner/outer relative increment");
2564   OPT(0,redlbound,0,0,1,"relative and absolute bounds on learned clauses");
2565   OPT(0,redlexpfac,10,0,1000,"exponential reduce limit increment factor");
2566   OPT(0,redlinc,1000,1,10*M,"reduce limit increment");
2567   OPT(0,redlinit,4*K,1,100*M,"initial reduce limit");
2568   OPT(0,redlmaxabs,1000000,10,I/2,"maximum absolute reduce limit");
2569   OPT(0,redlmaxinc,200,1,100*K,"rel max reduce limit increment");
2570   OPT(0,redlmaxrel,300,10,10000,"maximum relative reduce limit");
2571   OPT(0,redlminabs,500,10,1000000,"minimum absolute reduce limit");
2572   OPT(0,redlmininc,10,1,100*K,"rel min reduce limit increment");
2573   OPT(0,redlminrel,10,10,1000,"minimum relative reduce limit");
2574   OPT(0,redloutinc,10000,0,1000000,"outer arithmetic reduce increment");
2575   OPT(0,redoutclim,5000,0,I,"clause limit for outer reduce schedule");
2576   OPT(0,redoutvlim,1000,0,I,"variable limit for outer reduce schedule");
2577   OPT(0,reduce,2,0,4,"clause reduction (1=noouter,2=luby,3=inout,4=arith)");
2578   OPT(0,rephase,1,0,2,"enable flushing and recomputation of phases (2=full)");
2579   OPT(0,rephaseinc,10000,1,I,"rephasing increment");
2580   OPT(0,restart,2,0,3,"enable restarting (0=no,1=fixed,2=luby,3=inout)");
2581   OPT(0,restartinit,0,0,I,"initial restart interval");
2582   OPT(0,restartint,5,1,I,"restart interval");
2583   OPT(0,restartintscale,0,-1,1,"scale restart interval");
2584   OPT(0,reusetrail,1,0,1,"reuse trail");
2585   OPT(0,rmincpen,4,0,32,"logarithm of watcher removal penalty");
2586   OPT(0,rstinoutinc,110,1,1000,"restart inner/outer relative increment");
2587   OPT(0,saturating,70,0,1000,"saturating level (no restart)");
2588   OPT(0,scincinc,200,0,10*K,"score increment increment in per mille");
2589   OPT(0,score,5,0,6,"0=static,1=inc,2=vmtf,3=sum,4=avg,5=evsids,6=vsids256");
2590   OPT(0,seed,0,0,I,"random number generator seed");
2591   OPT(0,simpdelay,0,0,I,"initial simplification delay");
2592   OPT(0,simpen,0,0,24,"logarithmic initial simplification penalty");
2593   OPT(0,simpidiv,3,1,100,"simplification inter delay divisor");
2594   OPT(0,simpinterdelay,2000,0,I,"inprocessing simplification delay");
2595   OPT(0,simpiscale,100,1,10000,"relative simplification inter delay scale");
2596   OPT(0,simplify,2,0,2,"enable simplification");
2597   OPT(0,simprtc,5,1,100,"min var reduction for simplification RTC");
2598   OPT(0,simpvarchg,100,1,1000, "simp remaining vars percentage change lim");
2599   OPT(0,simpvarlim,100,0,I, "simp remaining vars min limit");
2600   OPT(0,sizemaxpen,5,0,20,"maximum logarithmic size penalty");
2601   OPT(0,sizepen,1*M,1,I,"number of clauses size penalty starting point");
2602   OPT(0,sleeponabort,0,0,I,"sleep this seconds before abort/exit");
2603   OPT(0,smallirr,90,0,100,"max percentage irr lits for BCE and VE");
2604   OPT(0,smallve,1,0,1,"enable small number variables elimination");
2605   OPT(0,smallvevars,FUNVAR,4,FUNVAR, "variables small variable elimination");
2606   OPT(0,smallvewait,0,0,1,"wait with small variable elimination");
2607   OPT(0,sortlits,0,0,1,"sort lits of cls during garbage collection");
2608   OPT(0,subl,9,0,10*K,"try to subsume this many recent learned clauses");
2609   OPT(0,synclsall,1,0,1,"always synchronize all unconsumed clauses");
2610   OPT(0,synclsglue,8,0,I,"clause synchronization glue limit");
2611   OPT(0,synclsint,100,0,1000,"clause synchronization confs interval");
2612   OPT(0,synclslen,40,0,I,"clause synchronization length limit");
2613   OPT(0,syncunint,111111,0,M,"unit synchronization steps interval");
2614   OPT(0,tabr,3,0,4,"tabula rasa (1=red,2=phases,3=cinc,4=scores");
2615   OPT(0,tabrcfactor,2,1,I,"tabula rasa clause factor");
2616   OPT(0,tabrkeep,3,1,4,"1=none,2=bin,3=bin+trn,4=bin+trn+glue0");
2617   OPT(0,tabrvfactor,4,1,I,"tabula rasa variable factor");
2618   OPT(0,termint,122222,0,M,"termination check interval");
2619   OPT(0,ternres,1,0,1,"generate ternary resolvents");
2620   OPT(0,ternresboost,5,1,100,"initial ternary reslution boost");
2621   OPT(0,ternresrtc,0,0,1,"run ternary resolvents until completion");
2622   OPT(0,ternreswait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2623   OPT(0,transred,1,0,1,"enable transitive reduction");
2624   OPT(0,transredwait,2,0,2,"wait for BCE (1) and/or BVE (2)");
2625   OPT(0,trdmaxeff,2*M,-1,I,"max effort in transitive reduction");
2626   OPT(0,trdmineff,100*K,0,I,"min effort in transitive reduction");
2627   OPT(0,trdreleff,10,0,10*K,"rel effort in transitive reduction");
2628   OPT(0,treelook,1,0,2,"enable tree-based look-ahead (2=scheduleprobing)");
2629   OPT(0,treelookboost,20,1,100000,"tree-based look-head boost factor");
2630   OPT(0,treelookfull,0,0,1,"do not limit tree-based look-head");
2631   OPT(0,treelooklrg,1,0,1,"use large clauses during tree-look");
2632   OPT(0,treelookmaxeff,50*M,-1,I,"max effort in tree-look based probing");
2633   OPT(0,treelookmineff,300*K,0,I,"min effort in tree-look based probing");
2634   OPT(0,treelookreleff,1,0,10*K,"rel effort in tree-look based probing");
2635   OPT(0,treelookrtc,0,0,1,"run tree-based look-ahead until completion");
2636   OPT(0,trep,0,0,1,"enable time based interval reporting");
2637   OPT(0,trepint,55555,1,I,"interval for time based reporting");
2638   OPT(0,trnreleff,10,0,K,"rel effort in ternary resolutions");
2639   OPT(0,trnrmaxeff,200*M,-1,I,"max effort in ternary resolutions");
2640   OPT(0,trnrmineff,4*M,0,I,"min effort in ternary resolutions");
2641   OPT(0,unhdatrn,2,0,2,"unhide redundant ternary clauses (1=move,2=force)");
2642   OPT(0,unhdextstamp,1,0,1,"used extended stamping features");
2643   OPT(0,unhdhbr,0,0,1,"enable unhiding hyper binary resolution");
2644   OPT(0,unhdlnpr,3,0,I,"unhide no progress round limit");
2645   OPT(0,unhdmaxeff,20*M,-1,I,"max effort in unhiding");
2646   OPT(0,unhdmineff,100*K,0,I,"min effort in unhiding");
2647   OPT(0,unhdreleff,2,0,10*K,"rel effort in unhiding");
2648   OPT(0,unhdroundlim,20,0,100,"unhide round limit");
2649   OPT(0,unhide,1,0,1,"enable unhiding");
2650   OPT(0,unhidewait,0,0,2,"wait for BCE (1) and/or BVE (2)");
2651   OPT(0,wait,1,0,1,"enable or disable all waiting");
2652   OPT(0,waitmax,4,-1,I,"max simps to wait (-1=nomax)");
2653   OPT(0,witness,1,0,1,"print witness");
2654
2655   OPT('c',check,0,0,3,"check level");
2656   OPT('l',log,-1,-1,5,"log level");
2657   OPT('v',verbose,0,-1,4,"verbosity level");
2658
2659   if (lgl->opts->plain.val) lglsetplain (lgl, 1);
2660   if (lgl->opts->drup.val) lglsetdrup (lgl, 1);
2661   if (lgl->opts->druplig.val) lglsetdruplig (lgl, 1);
2662   if (!lgl->opts->wait.val) lglsetwait (lgl, 0);
2663
2664   if (abs (lgl->opts->bias.val) <= 1) lgl->bias = lgl->opts->bias.val;
2665   else lgl->bias = 1;
2666
2667   NEW (lgl->times, 1);
2668   NEW (lgl->timers, 1);
2669   NEW (lgl->limits, 1);
2670   NEW (lgl->fltstr, 1);
2671   NEW (lgl->red, MAXGLUE+1);
2672   NEW (lgl->wchs, 1);
2673   for (i = 0; i < MAXLDFW; i++) lgl->wchs->start[i] = INT_MAX;
2674   lglpushstk (lgl, &lgl->wchs->stk, INT_MAX);
2675   lglpushstk (lgl, &lgl->wchs->stk, INT_MAX);
2676
2677 #ifdef NDBLSCR
2678   lgl->scinc = lglflt (0, 1);
2679 #else
2680   lgl->scinc = 1;
2681 #endif
2682
2683   TRANS (UNUSED);
2684
2685   return lgl;
2686 }
2687
2688 static void lglcopyclonenfork (LGL * dst, LGL * src) {
2689   memcpy (dst->opts, src->opts, sizeof *src->opts);
2690   dst->out = src->out;
2691   if (dst->prefix) lgldelstr (dst, dst->prefix);
2692   dst->prefix = lglstrdup (dst, src->prefix);
2693   if (src->cbs) {
2694     lglinitcbs (dst);
2695     if (src->cbs->onabort) {
2696       dst->cbs->abortstate = src->cbs->abortstate;
2697       dst->cbs->onabort = src->cbs->onabort;
2698     }
2699     if (src->cbs->getime) dst->cbs->getime = src->cbs->getime;
2700   }
2701 }
2702
2703 static void lglcompact (LGL *);
2704
2705 LGL * lglmclone (LGL * orig,
2706                  void * mem,
2707                  lglalloc alloc,
2708                  lglrealloc realloc,
2709                  lgldealloc dealloc) {
2710   size_t max_bytes, current_bytes;
2711   LGL * lgl = orig;
2712   int glue;
2713
2714   if (!orig) return 0;
2715   lglcompact (orig);
2716   LOG (1, "cloning");
2717   lgl = lglnewlgl (mem, alloc, realloc, dealloc);
2718   memcpy (lgl, orig, ((char*)&orig->mem) - (char*) orig);
2719   max_bytes = lgl->stats->bytes.max;
2720   current_bytes = lgl->stats->bytes.current;
2721   memcpy (lgl->stats, orig->stats, sizeof *orig->stats);
2722   lgl->stats->bytes.current = current_bytes;
2723   lgl->stats->bytes.max = max_bytes;
2724
2725   lglcopyclonenfork (lgl, orig);
2726
2727   CLONE (limits, 1);
2728   CLONE (times, 1);
2729   CLONE (timers, 1);            assert (!lgl->timers->nest);
2730   CLONE (fltstr, 1);
2731   CLONE (ext, orig->szext);
2732   CLONE (i2e, orig->szvars);
2733   CLONE (doms, 2*orig->szvars);
2734   CLONE (dvars, orig->szvars);
2735   CLONE (qvars, orig->szvars);
2736   CLONE (avars, orig->szvars);
2737   CLONE (vals, orig->szvars);
2738   CLONE (jwh, 2*orig->szvars);
2739   CLONE (drail, orig->szdrail);
2740
2741   NEW (lgl->red, MAXGLUE+1);
2742   for (glue = 0; glue <= MAXGLUE; glue++) CLONESTK (red[glue]);
2743
2744   NEW (lgl->wchs, 1);
2745   memcpy (lgl->wchs, orig->wchs, sizeof *orig->wchs);
2746   CLONESTK (wchs->stk);
2747
2748   CLONESTK (control);
2749   CLONESTK (clause);
2750   CLONESTK (eclause);
2751   CLONESTK (extend);
2752   CLONESTK (irr);
2753   CLONESTK (trail);
2754   CLONESTK (frames);
2755   CLONESTK (eassume);
2756   CLONESTK (assume);
2757   CLONESTK (fassume);
2758   CLONESTK (learned);
2759   CLONESTK (cassume);
2760   CLONESTK (dsched);
2761 #ifndef NCHKSOL
2762   CLONESTK (orig);
2763 #endif
2764 #ifndef NDEBUG
2765   {
2766     const char * p;
2767     for (p = (char*)&orig->elm; p < (char*)(&orig->repr+1); p++) assert (!*p);
2768   }
2769 #endif
2770   assert (lgl->stats->bytes.current == orig->stats->bytes.current);
2771   assert (lgl->stats->bytes.max <= orig->stats->bytes.max);
2772   lgl->stats->bytes.max = orig->stats->bytes.max;
2773   return lgl;
2774 }
2775
2776 LGL * lglclone (LGL * lgl) {
2777   REQINIT ();
2778   return lglmclone (lgl,
2779                     lgl->mem->state,
2780                     lgl->mem->alloc,
2781                     lgl->mem->realloc,
2782                     lgl->mem->dealloc);
2783 }
2784
2785 void lglchkclone (LGL * lgl) {
2786   REQINITNOTFORKED ();
2787   TRAPI ("chkclone");
2788 #ifdef NLGLPICOSAT
2789   if (!lgl->opts->druplig.val) {
2790     if (lgl->clone) lglrelease (lgl->clone);
2791     lgl->clone = lglclone (lgl);
2792   }
2793 #endif
2794 }
2795
2796 LGL * lglinit (void) { return lglminit (0, 0, 0, 0); }
2797
2798 static int lglmaxoptnamelen (LGL * lgl) {
2799   int res = 0, len;
2800   Opt * o;
2801   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++)
2802     if ((len = strlen (o->lng)) > res)
2803       res = len;
2804   return res;
2805 }
2806
2807 void lglusage (LGL * lgl) {
2808   char fmt[20];
2809   int len;
2810   Opt * o;
2811   REQINITNOTFORKED ();
2812   len = lglmaxoptnamelen (lgl);
2813   sprintf (fmt, "--%%-%ds", len);
2814   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
2815     if (o->shrt) fprintf (lgl->out, "-%c|", o->shrt);
2816     else fprintf (lgl->out, "   ");
2817     fprintf (lgl->out, fmt, o->lng);
2818     fprintf (lgl->out, " %s [%d]\n", o->descrp, o->val);
2819   }
2820 }
2821
2822 static int lglignopt (const char * name) {
2823   if (!strcmp (name, "abstime")) return 1;
2824   if (!strcmp (name, "check")) return 1;
2825   if (!strcmp (name, "drup")) return 1;
2826   if (!strcmp (name, "exitonabort")) return 1;
2827   if (!strcmp (name, "log")) return 1;
2828   if (!strcmp (name, "sleeponabort")) return 1;
2829   if (!strcmp (name, "verbose")) return 1;
2830   if (!strcmp (name, "witness")) return 1;
2831   return 0;
2832 }
2833
2834 void lglopts (LGL * lgl, const char * prefix, int ignsome) {
2835   Opt * o;
2836   REQINITNOTFORKED ();
2837   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
2838     if (ignsome && lglignopt (o->lng)) continue;
2839     fprintf (lgl->out, "%s--%s=%d\n", prefix, o->lng, o->val);
2840   }
2841 }
2842
2843 void lglrgopts (LGL * lgl) {
2844   Opt * o;
2845   REQINITNOTFORKED ();
2846   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++)
2847     fprintf (lgl->out, "%s %d %d %d\n", o->lng, o->val, o->min, o->max);
2848 }
2849
2850 void lglpcs (LGL * lgl, int mixed) {
2851   int i, printi, printl;
2852   int64_t range;
2853   Opt * o;
2854   REQINITNOTFORKED ();
2855   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
2856     if (lglignopt (o->lng)) continue;
2857     range = o->max; range -= o->min;
2858     if (range >= 7 && mixed < 0) continue;
2859     printi = printl = 0;
2860     printf ("%s ", o->lng);
2861     if (range < 7) {
2862       printf ("{%d", o->min);
2863       for (i = o->min + 1; i <= o->max; i++) printf (",%d", i);
2864       printf ("}");
2865     } else if (!mixed) {
2866       printf ("[%d,%d]", o->min, o->max);
2867       printi = 1;
2868       printl = (o->min > 0 && range >= 100);
2869     } else if (o->dflt == o->min || o->dflt == o->max) {
2870       printf ("{%d,%d,%d,%d,%d}",
2871         o->min,
2872         (int)(o->min + (1*range + 3)/4),
2873         (int)(o->min + (2*range + 3)/4),
2874         (int)(o->min + (3*range + 3)/4),
2875         o->max);
2876     } else if (o->dflt == o->min + 1) {
2877       printf ("{%d,%d,%d,%d}",
2878         o->min,
2879         o->dflt,
2880         (int)(o->dflt + (o->max - (int64_t) o->dflt)/2),
2881         o->max);
2882     } else if (o->dflt + 1 == o->max) {
2883       printf ("{%d,%d,%d,%d}",
2884         o->min,
2885         (int)(o->min + (o->dflt - (int64_t) o->min)/2),
2886         o->dflt,
2887         o->max);
2888     } else {
2889       assert (o->dflt - o->min >= 2);
2890       assert (o->max - o->dflt >= 2);
2891       printf ("{%d,%d,%d,%d,%d}",
2892         o->min,
2893         (int)(o->min + (o->dflt - (int64_t) o->min)/2),
2894         o->dflt,
2895         (int)(o->dflt + (o->max - (int64_t) o->min)/2),
2896         o->max);
2897     }
2898     printf ("[%d]", o->dflt);
2899     if (printi) printf ("i");
2900     if (printl) printf ("l");
2901     printf (" # %s\n",o->descrp);
2902   }
2903 }
2904
2905 int lglhasopt (LGL * lgl, const char * opt) {
2906   Opt * o;
2907   REQINITNOTFORKED ();
2908   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
2909     if (!opt[1] && o->shrt == opt[0]) return 1;
2910     if (!strcmp (o->lng, opt)) return 1;
2911   }
2912   return 0;
2913 }
2914
2915 void * lglfirstopt (LGL * lgl) { return FIRSTOPT (lgl); }
2916
2917 void * lglnextopt (LGL * lgl,
2918                    void * current,
2919                    const char **nameptr,
2920                    int *valptr, int *minptr, int *maxptr) {
2921   Opt * opt = current, * res = opt + 1;
2922   if (res > LASTOPT (lgl)) return 0;
2923   if (nameptr) *nameptr = opt->lng;
2924   if (valptr) *valptr = opt->val;
2925   if (minptr) *minptr = opt->min;
2926   if (maxptr) *maxptr = opt->max;
2927   return res;
2928 }
2929
2930 void lglsetopt (LGL * lgl, const char * opt, int val) {
2931   int oldval;
2932   Opt * o;
2933   REQINITNOTFORKED ();
2934   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
2935     if (!opt[1] && o->shrt == opt[0]) break;
2936     if (!strcmp (o->lng, opt)) break;
2937   }
2938   if (o > LASTOPT (lgl)) return;
2939   if (val < o->min) val = o->min;
2940   if (o->max < val) val = o->max;
2941   oldval = o->val;
2942   o->val = val;
2943   if (o == &lgl->opts->flipping && !oldval)
2944     lgl->flipping = lgl->notflipped = 0;
2945   if (o == &lgl->opts->plain) {
2946     if (val > 0 && !oldval) lglsetplain (lgl, 1);
2947     if (!val && oldval) lglsetplain (lgl, 0);
2948   }
2949   if (o == &lgl->opts->drup) {
2950     if (val > 0 && !oldval) lglsetdrup (lgl, 1);
2951     if (!val && oldval) lglsetdrup (lgl, 0);
2952   }
2953   if (o == &lgl->opts->druplig) {
2954     if (val > 0 && !oldval) lglsetdruplig (lgl, 1);
2955     if (!val && oldval) lglsetdruplig (lgl, 0);
2956   }
2957   if (o == &lgl->opts->wait) {
2958     if (val > 0 && !oldval) lglsetwait (lgl, 1);
2959     if (!val && oldval) lglsetwait (lgl, 0);
2960   }
2961   if (o == &lgl->opts->phase && val != oldval) lgl->flushphases = 1;
2962   if (lgl->state == UNUSED) TRANS (OPTSET);
2963   TRAPI ("option %s %d", opt, val);
2964 }
2965
2966 static int lglws (int ch) {
2967   return ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r';
2968 }
2969
2970 int lglreadopts (LGL * lgl, FILE * file) {
2971   int res, ch, val, nvalbuf, noptbuf;
2972   char optbuf[40], valbuf[40];
2973   const char * opt;
2974   res = 0;
2975   for (;;) {
2976     while (lglws (ch = getc (file)))
2977       ;
2978     if (ch == EOF) break;
2979     noptbuf = 0;
2980     optbuf[noptbuf++] = ch;
2981     while ((ch = getc (file)) != EOF && !lglws (ch)) {
2982       if (noptbuf + 1 >= sizeof optbuf) { ch = EOF; break; }
2983       optbuf[noptbuf++] = ch;
2984     }
2985     if (ch == EOF) break;
2986     assert (noptbuf < sizeof optbuf);
2987     optbuf[noptbuf++] = 0;
2988     assert (lglws (ch));
2989     while (lglws (ch = getc (file)))
2990       ;
2991     if (ch == EOF) break;
2992     nvalbuf = 0;
2993     valbuf[nvalbuf++] = ch;
2994     while ((ch = getc (file)) != EOF && !lglws (ch)) {
2995       if (nvalbuf + 1 >= sizeof valbuf) break;
2996       valbuf[nvalbuf++] = ch;
2997     }
2998     assert (nvalbuf < sizeof valbuf);
2999     valbuf[nvalbuf++] = 0;
3000     opt = optbuf;
3001     val = atoi (valbuf);
3002     lglprt (lgl, 1, "read option --%s=%d", opt, val);
3003     lglsetopt (lgl, opt, val);
3004     res++;
3005   }
3006   return res;
3007 }
3008
3009 void lglsetout (LGL * lgl, FILE * out) { lgl->out = out; }
3010
3011 FILE * lglgetout (LGL * lgl) { return lgl->out; }
3012
3013 void lglsetprefix (LGL * lgl, const char * prefix) {
3014   lgldelstr (lgl, lgl->prefix);
3015   lgl->prefix = lglstrdup (lgl, prefix);
3016 }
3017
3018 const char * lglgetprefix (LGL * lgl) { return lgl->prefix; }
3019
3020 static Opt * lgligetopt (LGL * lgl, const char * opt) {
3021   Opt * o;
3022   REQINITNOTFORKED ();
3023   for (o = FIRSTOPT (lgl); o <= LASTOPT (lgl); o++) {
3024     if (!opt[1] && o->shrt == opt[0]) return o;
3025     if (!strcmp (o->lng, opt)) return o;
3026   }
3027   return 0;
3028 }
3029
3030 int lglgetopt (LGL * lgl, const char * opt) {
3031   Opt * o = lgligetopt (lgl, opt);
3032   return o ? o->val : 0;
3033 }
3034
3035 int lglgetoptminmax (LGL * lgl, const char * opt,
3036                      int * min_ptr, int * max_ptr) {
3037   Opt * o = lgligetopt (lgl, opt);
3038   if (!o) return 0;
3039   if (min_ptr) *min_ptr = o->min;
3040   if (max_ptr) *max_ptr = o->max;
3041   return o->val;
3042 }
3043
3044 /*------------------------------------------------------------------------*/
3045
3046 static void lglrszvars (LGL * lgl, int new_size) {
3047   int old_size = lgl->szvars;
3048   assert (lgl->nvars <= new_size);
3049   RSZ (lgl->vals, old_size, new_size);
3050   RSZ (lgl->i2e, old_size, new_size);
3051   RSZ (lgl->doms, 2*old_size, 2*new_size);
3052   RSZ (lgl->dvars, old_size, new_size);
3053   RSZ (lgl->avars, old_size, new_size);
3054   RSZ (lgl->qvars, old_size, new_size);
3055   RSZ (lgl->jwh, 2*old_size, 2*new_size);
3056   lgl->szvars = new_size;
3057 }
3058
3059 static void lglenlvars (LGL * lgl) {
3060   size_t old_size, new_size;
3061   old_size = lgl->szvars;
3062   new_size = old_size ? 2 * old_size : 4;
3063   LOG (3, "enlarging internal variables from %ld to %ld", old_size, new_size);
3064   lglrszvars (lgl, new_size);
3065 }
3066
3067 static void lglredvars (LGL * lgl) {
3068   size_t old_size, new_size;
3069   old_size = lgl->szvars;
3070   new_size = lgl->nvars;
3071   if (new_size == old_size) return;
3072   LOG (3, "reducing variables from %ld to %ld", old_size, new_size);
3073   lglrszvars (lgl, new_size);
3074 }
3075
3076 static int lglmax (int a, int b) { return a > b ? a : b; }
3077
3078 static int lglmin (int a, int b) { return a < b ? a : b; }
3079
3080 /*------------------------------------------------------------------------*/
3081
3082 static DVar * lgldvar (LGL * lgl, int lit) {
3083   assert (2 <= abs (lit) && abs (lit) < lgl->nvars);
3084   return lgl->dvars + abs (lit);
3085 }
3086
3087 /*------------------------------------------------------------------------*/
3088
3089 static AVar * lglavar (LGL * lgl, int lit) {
3090   assert (2 <= abs (lit) && abs (lit) < lgl->nvars);
3091   return lgl->avars + abs (lit);
3092 }
3093
3094 static Val lglval (LGL * lgl, int lit) {
3095   int idx = abs (lit);
3096   Val res;
3097   ASSERT (2 <= idx && idx < lgl->nvars);
3098   res = lgl->vals[idx];
3099   if (lit < 0) res = -res;
3100   return res;
3101 }
3102
3103 static int lgltrail (LGL * lgl, int lit) { return lglavar (lgl, lit)->trail; }
3104
3105 static TD * lgltd (LGL * lgl, int lit) {
3106   int pos = lgltrail (lgl, lit);
3107   assert (0 <= pos && pos < lgl->szdrail);
3108   return lgl->drail + pos;
3109 }
3110
3111 static int lglevel (LGL * lgl, int lit) { return lgltd (lgl, lit)->level; }
3112
3113 static int lglisfree (LGL * lgl, int lit) {
3114   return lglavar (lgl, lit)->type == FREEVAR;
3115 }
3116
3117 /*------------------------------------------------------------------------*/
3118
3119 static QVar * lglqvar (LGL * lgl, int lit) {
3120   assert (2 <= abs (lit) && abs (lit) < lgl->nvars);
3121   return lgl->qvars + abs (lit);
3122 }
3123
3124 static int * lgldpos (LGL * lgl, int lit) {
3125   QVar * qv;
3126   int * res;
3127   qv = lglqvar (lgl, lit);
3128   res = &qv->pos;
3129   return res;
3130 }
3131
3132 static int lglscrcmp (Scr a, Scr b) {
3133   if (a < b) return -1;
3134   if (a > b) return 1;
3135   return 0;
3136 }
3137
3138 static int lgldcmp (LGL * lgl, int l, int k) {
3139   QVar * pv = lglqvar (lgl, l);
3140   QVar * qv = lglqvar (lgl, k);
3141   int res;
3142   if ((res = lglscrcmp (pv->score, qv->score))) return res;
3143   res = lgl->bias * (l - k);
3144   return res;
3145 }
3146
3147 #ifndef NDEBUG
3148 static void lglchkdsched (LGL * lgl) {
3149   int * p, parent, child, ppos, cpos, size, i, tmp;
3150   Stk * s = &lgl->dsched;
3151   size = lglcntstk (s);
3152   p = s->start;
3153   for (ppos = 0; ppos < size; ppos++) {
3154     parent = p[ppos];
3155     tmp = *lgldpos (lgl, parent);
3156     assert (ppos == tmp);
3157     for (i = 0; i <= 1; i++) {
3158       cpos = 2*ppos + 1 + i;
3159       if (cpos >= size) continue;
3160       child = p[cpos];
3161       tmp = *lgldpos (lgl, child);
3162       assert (cpos == tmp);
3163       assert (lgldcmp (lgl, parent, child) >= 0);
3164     }
3165   }
3166 }
3167 #endif
3168
3169 static void lgldup (LGL * lgl, int lit) {
3170   int child = lit, parent, cpos, ppos, * p, * cposptr, * pposptr;
3171   Stk * s = &lgl->dsched;
3172   p = s->start;
3173   cposptr = lgldpos (lgl, child);
3174   cpos = *cposptr;
3175   assert (cpos >= 0);
3176   while (cpos > 0) {
3177     ppos = (cpos - 1)/2;
3178     parent = p[ppos];
3179     if (lgldcmp (lgl, parent, lit) >= 0) break;
3180     pposptr = lgldpos (lgl, parent);
3181     assert (*pposptr == ppos);
3182     p[cpos] = parent;
3183     *pposptr = cpos;
3184     LOGDSCHED (5, parent, "down from %d", ppos);
3185     cpos = ppos;
3186   }
3187   if (*cposptr == cpos) return;
3188 #ifndef NLGLOG
3189   ppos = *cposptr;
3190 #endif
3191   *cposptr = cpos;
3192   p[cpos] = lit;
3193   LOGDSCHED (5, lit, "up from %d", ppos);
3194 #ifndef NDEBUG
3195   if (lgl->opts->check.val >= 2) lglchkdsched (lgl);
3196 #endif
3197 }
3198
3199 static void lglddown (LGL * lgl, int lit) {
3200   int parent = lit, child, right, ppos, cpos;
3201   int * p, * pposptr, * cposptr, size;
3202   Stk * s = &lgl->dsched;
3203   size = lglcntstk (s);
3204   p = s->start;
3205   pposptr = lgldpos (lgl, parent);
3206   ppos = *pposptr;
3207   assert (0 <= ppos);
3208   for (;;) {
3209     cpos = 2*ppos + 1;
3210     if (cpos >= size) break;
3211     child = p[cpos];
3212     if (cpos + 1 < size) {
3213       right = p[cpos + 1];
3214       if (lgldcmp (lgl, child, right) < 0) cpos++, child = right;
3215     }
3216     if (lgldcmp (lgl, child, lit) <= 0) break;
3217     cposptr = lgldpos (lgl, child);
3218     assert (*cposptr = cpos);
3219     p[ppos] = child;
3220     *cposptr = ppos;
3221     LOGDSCHED (5, child, "up from %d", cpos);
3222     ppos = cpos;
3223   }
3224   if (*pposptr == ppos) return;
3225 #ifndef NLGLOG
3226   cpos = *pposptr;
3227 #endif
3228   *pposptr = ppos;
3229   p[ppos] = lit;
3230   LOGDSCHED (5, lit, "down from %d", cpos);
3231 #ifndef NDEBUG
3232   if (lgl->opts->check.val >= 2) lglchkdsched (lgl);
3233 #endif
3234 }
3235
3236 static void lgldsched (LGL * lgl, int lit) {
3237   int * p = lgldpos (lgl, lit);
3238   Stk * s = &lgl->dsched;
3239   assert (*p < 0);
3240   *p = lglcntstk (s);
3241   lglpushstk (lgl, s, lit);
3242   lgldup (lgl, lit);
3243   lglddown (lgl, lit);
3244   LOGDSCHED (4, lit, "pushed");
3245 }
3246
3247 static int lgltopdsched (LGL * lgl) {
3248   assert (!lglmtstk (&lgl->dsched));
3249   return lgl->dsched.start[0];
3250 }
3251
3252 static int lglpopdsched (LGL * lgl) {
3253   Stk * s = &lgl->dsched;
3254   int res, last, cnt, * p;
3255   QVar * qv;
3256   assert (!lglmtstk (s));
3257   res = *s->start;
3258   LOGDSCHED (4, res, "popped");
3259   qv = lglqvar (lgl, res);
3260   assert (!qv->pos);
3261   qv->pos = -1;
3262   last = lglpopstk (s);
3263   cnt = lglcntstk (s);
3264   if (!cnt) { assert (last == res); return res; }
3265   p = lgldpos (lgl, last);
3266   assert (*p == cnt);
3267   *p = 0;
3268   *s->start = last;
3269   lglddown (lgl, last);
3270   return res;
3271 }
3272
3273 static void lgldreschedule (LGL * lgl) {
3274   Stk * s = &lgl->dsched;
3275   int idx, i, pos, cnt = lglcntstk (s);
3276   QVar * qv;
3277   LOG (1, "rescheduling %d variables", cnt);
3278   for (idx = 2; idx < lgl->nvars; idx++) lglqvar (lgl, idx)->pos = -1;
3279   pos = 0;
3280   s->top = s->start;
3281   for (i = 0; i < cnt; i++) {
3282     assert (pos <= i);
3283     assert (s->start + pos == s->top);
3284     idx = s->start[i];
3285     if (abs (idx) <= 1) continue;
3286     qv = lglqvar (lgl, idx);
3287     if (!lglisfree (lgl, idx)) { qv->pos = -1; continue; }
3288     assert (qv->pos == -1);
3289     s->start[pos] = idx;
3290     qv->pos = pos++;
3291     s->top++;
3292     lgldup (lgl, idx);
3293     lglddown (lgl, idx);
3294   }
3295   LOG (1, "new schedule with %d variables", lglcntstk (s));
3296   lglfitstk (lgl, s);
3297 #ifndef NDEBUG
3298   if (lgl->opts->check.val >= 1) lglchkdsched (lgl);
3299 #endif
3300 }
3301
3302 #define RVL 2
3303
3304 static void lglrescorevars (LGL * lgl) {
3305   Scr oldscinc, oldscore, newscore, oldmaxscore = 0, newmaxscore = 0;
3306   int64_t newotfs;
3307   QVar * qv;
3308   int idx;
3309   lgl->stats->rescored.vars++;
3310   for (idx = 2; idx < lgl->nvars; idx++) {
3311     qv = lglqvar (lgl, idx);
3312     oldscore = qv->score;
3313     if (oldscore > oldmaxscore) oldmaxscore = oldscore;
3314 #ifdef NDBLSCR
3315     if (lgl->opts->score.val == LGL_SCORE_EVSIDS ||
3316         lgl->opts->score.val == LGL_SCORE_AVG)
3317       newscore = lglshflt (oldscore, lgl->opts->maxscorexp.val);
3318     else newscore = (oldscore >> 32);
3319 #else
3320     newscore = oldscore / lgl->maxscore;
3321 #endif
3322     qv->score = newscore;
3323     if (qv->score > newmaxscore) newmaxscore = qv->score;
3324     LOG (3, "rescored variable %d from %s to %s",
3325          idx, lglscr2str (lgl, oldscore), lglscr2str (lgl, qv->score));
3326   }
3327   lgldreschedule (lgl);
3328   newotfs = lgl->stats->otfs.driving + lgl->stats->otfs.restarting;
3329   assert (newotfs >= lgl->limits->rescore.vars.otfs);
3330   assert (lgl->stats->confs >= lgl->limits->rescore.vars.confs);
3331   lglprt (lgl, RVL,
3332     "[rescored-vars-%d] after %lld conflicts and %lld OTFS",
3333     lgl->stats->rescored.vars,
3334     lgl->stats->confs - lgl->limits->rescore.vars.confs,
3335     newotfs - lgl->limits->rescore.vars.otfs);
3336   lgl->limits->rescore.vars.confs = lgl->stats->confs;
3337   lgl->limits->rescore.vars.otfs = newotfs;
3338   lglprt (lgl, RVL,
3339     "[rescored-vars-%d] old maximum score %s",
3340     lgl->stats->rescored.vars, lglscr2str (lgl, oldmaxscore));
3341   lglprt (lgl, RVL,
3342     "[rescored-vars-%d] new maximum score %s",
3343     lgl->stats->rescored.vars, lglscr2str (lgl, newmaxscore));
3344   if (lgl->opts->score.val == LGL_SCORE_EVSIDS) {
3345     oldscinc = lgl->scinc;
3346 #ifdef NDBLSCR
3347     lgl->scinc = lglshflt (oldscinc, lgl->opts->maxscorexp.val);
3348 #else
3349     lgl->scinc = oldscinc / lgl->maxscore;
3350 #endif
3351     assert (lgl->scinc > 0);
3352     lglprt (lgl, RVL,
3353       "[rescored-vars-%d] old score increment %s",
3354       lgl->stats->rescored.vars, lglscr2str (lgl, oldscinc));
3355     lglprt (lgl, RVL,
3356       "[rescored-vars-%d] new score increment %s",
3357       lgl->stats->rescored.vars, lglscr2str (lgl, lgl->scinc));
3358   }
3359 }
3360
3361 static void lglbumpscinc (LGL * lgl) {
3362   Scr oldscinc;
3363   if (lgl->opts->score.val == LGL_SCORE_VSIDS256) {
3364     if (!(lgl->stats->confs & 255)) {
3365       int idx;
3366       for (idx = 2; idx < lgl->nvars; idx++) {
3367         QVar * qv = lglqvar (lgl, idx);
3368         qv->score /= 2;
3369         if (qv->pos < 0) continue;
3370         lglddown (lgl, idx);
3371       }
3372     }
3373   } else if (lgl->opts->score.val == LGL_SCORE_EVSIDS) {
3374     oldscinc = lgl->scinc;
3375     lgl->scinc = lglmulscr (oldscinc, lgl->scincf);
3376     LOG (3, "bumped variable score increment from %s to %s",
3377          lglscr2str (lgl, oldscinc), lglscr2str (lgl, lgl->scinc));
3378     if (lgl->scinc < lgl->maxscore) return;
3379     LOG (2, "variable max score %s hit", lglscr2str (lgl, lgl->maxscore));
3380     lglrescorevars (lgl);
3381   }
3382 }
3383
3384 /*------------------------------------------------------------------------*/
3385
3386 static int lglnewvar (LGL * lgl) {
3387   AVar * av;
3388   DVar * dv;
3389   QVar * qv;
3390   int res;
3391   assert (!lgl->dense);
3392   if (lgl->nvars == lgl->szvars) lglenlvars (lgl);
3393   if (lgl->nvars) res = lgl->nvars++;
3394   else res = 2, lgl->nvars = 3;
3395   assert (res < lgl->szvars);
3396   if (res > MAXVAR) lgldie (lgl, "more than %d variables", MAXVAR - 1);
3397   assert (res <= MAXVAR);
3398   assert (((res << RMSHFT) >> RMSHFT) == res);
3399   assert (((-res << RMSHFT) >> RMSHFT) == -res);
3400   LOG (3, "new internal variable %d", res);
3401   dv = lgl->dvars + res;
3402   CLRPTR (dv);
3403   av = lgl->avars + res;
3404   CLRPTR (av);
3405   qv = lgl->qvars + res;
3406   CLRPTR (qv);
3407   qv->pos = -1;
3408   lgldsched (lgl, res);
3409   lgl->unassigned++;
3410   lgl->allphaseset = 0;
3411   return res;
3412 }
3413
3414 static int lglsgn (int lit) { return (lit < 0) ? -1 : 1; }
3415
3416 static Ext * lglelit2ext (LGL * lgl, int elit) {
3417   int idx = abs (elit);
3418   assert (0 < idx), assert (idx <= lgl->maxext);
3419   return lgl->ext + idx;
3420 }
3421
3422 #if 0
3423 static Ext * lgldlit2ext (LGL * lgl, int dlit) {
3424   int idx = abs (dlit);
3425   assert (0 < idx), assert (idx <= lgl->maxdef);
3426   return lgl->def + idx;
3427 }
3428 #endif
3429
3430 static int lglerepr (LGL * lgl, int elit) {
3431   int res, next, tmp;
3432   Ext * ext;
3433   assert (0 < abs (elit)), assert (abs (elit) <= lgl->maxext);
3434   res = elit;
3435   for (;;) {
3436     ext = lglelit2ext (lgl, res);
3437     if (!ext->equiv) break;
3438     next = ext->repr;
3439     if (res < 0) next = -next;
3440     res = next;
3441   }
3442   tmp = elit;
3443   for (;;) {
3444     ext = lglelit2ext (lgl, tmp);
3445     if (!ext->equiv) { assert (tmp == res); break; }
3446     next = ext->repr;
3447     ext->repr = (tmp < 0) ? -res : res;
3448     if (tmp < 0) next = -next;
3449     tmp = next;
3450   }
3451   return res;
3452 }
3453
3454 static void lgladjext (LGL * lgl, int eidx) {
3455   size_t old, new;
3456   assert (eidx >= lgl->szext);
3457   assert (eidx > lgl->maxext);
3458   assert (lgl->szext >= lgl->maxext);
3459   old = lgl->szext;
3460   new = old ? 2*old : 2;
3461   while (eidx >= new) new *= 2;
3462   assert (eidx < new), assert (new >= lgl->szext);
3463   LOG (3, "enlarging external variables from %ld to %ld", old, new);
3464   RSZ (lgl->ext, old, new);
3465   lgl->szext = new;
3466 }
3467
3468 #if 0
3469 static void lgladjdef (LGL * lgl, int didx) {
3470   size_t old, new;
3471   assert (didx);
3472   assert (didx >= lgl->szdef);
3473   assert (didx > lgl->maxdef);
3474   assert (lgl->szdef > lgl->maxdef);
3475   old = lgl->szdef;
3476   new = old ? 2*old : 2;
3477   while (didx >= new) new *= 2;
3478   assert (didx < new), assert (new >= lgl->szdef);
3479   LOG (3, "enlarging defined variables from %ld to %ld", old, new);
3480   RSZ (lgl->def, old, new);
3481   lgl->szdef = new;
3482 }
3483 #endif
3484
3485 static void lglmelter (LGL * lgl) {
3486   if (lgl->allfrozen) {
3487     lglprt (lgl, 1,
3488       "[melter] not all literals assumed to be frozen anymore");
3489     lgl->allfrozen = 0;
3490   }
3491   if (lgl->limits->elm.pen || lgl->limits->blk.pen || lgl->limits->cce.pen) {
3492     lglprt (lgl, 1,
3493       "[melter] reset penalties: %d elm, %d blk, %d cce",
3494       lgl->limits->elm.pen, lgl->limits->blk.pen, lgl->limits->cce.pen);
3495     lgl->limits->elm.pen = lgl->limits->blk.pen = lgl->limits->cce.pen = 0;
3496   }
3497   lgl->frozen = lgl->allfrozen = 0;
3498   LOG (2, "melted solver");
3499 }
3500
3501 static int lglimportaux (LGL * lgl, int elit) {
3502   int res, repr, eidx = abs (elit);
3503   Ext * ext;
3504   assert (elit);
3505   if (eidx >= lgl->szext) lgladjext (lgl, eidx);
3506   if (eidx > lgl->maxext) {
3507     lgl->maxext = eidx;
3508     lglmelter (lgl);
3509   }
3510   repr = lglerepr (lgl, elit);
3511   ext = lglelit2ext (lgl, repr);
3512   assert (!ext->equiv);
3513   res = ext->repr;
3514   if (!ext->imported) {
3515     res = lglnewvar (lgl);
3516     assert (!ext->equiv);
3517     ext->repr = res;
3518     ext->imported = 1;
3519     assert (eidx <= INT_MAX/2);
3520     lgl->i2e[res] = 2*eidx;
3521     LOG (3, "mapping external variable %d to %d", eidx, res);
3522     lglmelter (lgl);
3523   }
3524   if (repr < 0) res = -res;
3525   LOG (2, "importing %d as %d", elit, res);
3526   return res;
3527 }
3528
3529 static int lglimport (LGL * lgl, int elit) {
3530   assert (elit);
3531   if (!lgl->opts->import.val) {
3532     if (!lgl->maxext) (void) lglimportaux (lgl, 1);
3533     while (lgl->maxext < abs (elit))
3534       (void) lglimportaux (lgl, lgl->maxext + 1);
3535   }
3536   return lglimportaux (lgl, elit);
3537 }
3538
3539 static Stk * lglidx2stk (LGL * lgl, int red, int lidx) {
3540   int glue = 0;
3541   Stk * s;
3542   assert (red == 0 || red == REDCS);
3543   assert (0 <= lidx);
3544   if (!red) s = &lgl->irr;
3545   else {
3546     glue = lidx & GLUEMASK;
3547     lidx >>= GLUESHFT;
3548     assert (lidx <= MAXREDLIDX);
3549     s = &lgl->red[glue];
3550   }
3551   return s;
3552 }
3553
3554 static int * lglidx2lits (LGL * lgl, int red, int lidx) {
3555   Stk * s = lglidx2stk (lgl, red, lidx);
3556   int * res;
3557   assert (red == 0 || red == REDCS);
3558   assert (0 <= lidx);
3559   res = s->start + (red ? (lidx >> GLUESHFT) : lidx);
3560 #ifndef NDEBUG
3561   if (red && (lidx & GLUEMASK) == MAXGLUE) assert (res < s->end);
3562   else assert (res < s->top);
3563 #endif
3564   return res;
3565 }
3566
3567 #ifndef NLGLOG
3568 static const char * lglred2str (int red) {
3569   assert (!red || red == REDCS);
3570   return red ? "redundant" : "irredundant";
3571 }
3572 #endif
3573
3574 static int lgliselim (LGL * lgl, int lit) {
3575   Tag tag = lglavar (lgl, lit)->type;
3576   return tag == ELIMVAR;
3577 }
3578
3579 #if 0
3580 static int lglisdef (LGL * lgl, int ilit) {
3581   int iidx = abs (ilit), tidx, res;
3582   assert (2 <= iidx), assert (iidx < lgl->nvars);
3583   tidx = lgl->i2e[iidx];
3584   res = tidx & 1;
3585   return res;
3586 }
3587 #endif
3588
3589 static int lglexport (LGL * lgl, int ilit) {
3590   int iidx, tidx, eidx, def, res;
3591   iidx = abs (ilit);
3592   assert (2 <= iidx), assert (iidx < lgl->nvars);
3593   tidx = lgl->i2e[iidx];
3594   def = tidx & 1;
3595   tidx >>= 1;
3596   assert (tidx);
3597   eidx = tidx;
3598   if (def) eidx += lgl->maxext;
3599   res = eidx;
3600   if (ilit < 0) res = -res;
3601   return res;
3602 }
3603
3604 static int * lglrsn (LGL * lgl, int lit) { return lgltd (lgl, lit)->rsn; }
3605
3606 static int lglulit (int lit) { return 2*abs (lit) + (lit < 0); }
3607
3608 static void lglsetdom (LGL * lgl, int lit, int dom) {
3609   assert (2 <= abs (lit)  && abs (lit) < lgl->nvars);
3610   assert (2 <= abs (dom)  && abs (dom) < lgl->nvars);
3611   ASSERT (lglval (lgl, lit) >= 0);
3612   ASSERT (lglval (lgl, dom) >= 0);
3613   lgl->doms[lglulit (lit)] = dom;
3614   LOG (3, "literal %d dominated by %d", lit, dom);
3615 }
3616
3617 static int lglgetdom (LGL * lgl, int lit) {
3618   int res;
3619   assert (2 <= abs (lit)  && abs (lit) < lgl->nvars);
3620   assert (lglval (lgl, lit) >= 0);
3621   res = lgl->doms[lglulit (lit)];
3622   return res;
3623 }
3624
3625 static HTS * lglhts (LGL * lgl, int lit) {
3626   return lgldvar (lgl, lit)->hts + (lit < 0);
3627 }
3628
3629 static int * lglhts2wchs (LGL * lgl, HTS * hts) {
3630   int * res = lgl->wchs->stk.start + hts->offset;
3631   assert (res < lgl->wchs->stk.top);
3632   assert (res + hts->count < lgl->wchs->stk.top);
3633   assert (res + hts->count < lgl->wchs->stk.top);
3634   return res;
3635 }
3636
3637 static void lglassign (LGL * lgl, int lit, int r0, int r1) {
3638   int * p, other, other2, * c, lidx, found;
3639   int idx, phase, glue, tag, dom, red, irr;
3640   AVar * av = lglavar (lgl, lit);
3641   TD * td;
3642   LOGREASON (2, lit, r0, r1, "assign %d through", lit);
3643   av->trail = lglcntstk (&lgl->trail);
3644   if (av->trail >= lgl->szdrail) {
3645     int newszdrail = lgl->szdrail ? 2*lgl->szdrail : 1;
3646     RSZ (lgl->drail, lgl->szdrail, newszdrail);
3647     lgl->szdrail = newszdrail;
3648   }
3649   td = lgltd (lgl, lit);
3650   tag = r0 & MASKCS;
3651   dom = (tag == BINCS) ? lglgetdom (lgl, -(r0 >> RMSHFT)) : lit;
3652   lglsetdom (lgl, lit, dom);
3653 #ifndef NDEBUG
3654   {
3655     if (tag == BINCS || tag == TRNCS) {
3656       other = r0 >> RMSHFT;
3657       assert (lglval (lgl, other) < 0);
3658       if (tag == TRNCS) {
3659         other2 = r1;
3660         assert (lglval (lgl, other2) < 0);
3661       }
3662     } else if (tag == LRGCS) {
3663       red = r0 & REDCS;
3664       lidx = r1;
3665       c = lglidx2lits (lgl, red, lidx);
3666       found = 0;
3667       for (p = c; (other = *p); p++)
3668         if (other == lit) found++;
3669         else assert (lglval (lgl, other) < 0);
3670       assert (found == 1);
3671     } else assert (tag == DECISION || tag == UNITCS);
3672   }
3673   assert (!lglval (lgl, lit));
3674   assert (lgl->unassigned > 0);
3675   assert (!lgliselim (lgl, lit));
3676 #endif
3677   idx = abs (lit);
3678   phase = lglsgn (lit);
3679   lgl->vals[idx] = phase;
3680   if (!lgl->simp && !lgl->flipping && !lgl->phaseneg) {
3681     lgl->flips -= lgl->flips/100000ull;
3682     if (av->phase != phase) lgl->flips += 10000ull;
3683     av->phase = phase;
3684   }
3685 #ifndef NDEBUG
3686   if (phase < 0) av->wasfalse = 1; else av->wasfalse = 0;
3687 #endif
3688   td->level = lgl->level;
3689   if (!lgl->level) {
3690     td->irr = 1;
3691     if (av->type == EQUIVAR) {
3692       assert (lgl->stats->equiv.current > 0);
3693       lgl->stats->equiv.current--;
3694       assert (lgl->stats->equiv.sum > 0);
3695       lgl->stats->equiv.sum--;
3696     } else {
3697       assert (av->type == FREEVAR);
3698       av->type = FIXEDVAR;
3699     }
3700     lgl->stats->fixed.sum++;
3701     lgl->stats->fixed.current++;
3702     lgl->stats->prgss++;
3703     lgl->stats->irrprgss++;
3704     td->rsn[0] = UNITCS | (lit << RMSHFT);
3705     td->rsn[1] = 0;
3706     if (lgl->cbs && lgl->cbs->units.produce.fun) {
3707       LOG (2, "trying to export internal unit %d external %d\n",
3708            lgl->tid, lit, lglexport (lgl, lit));
3709       lgl->stats->sync.units.produced++;
3710       lgl->cbs->units.produce.fun (lgl->cbs->units.produce.state,
3711                                   lglexport (lgl, lit));
3712       LOG (2, "exporting internal unit %d external %d\n",
3713               lgl->tid, lit, lglexport (lgl, lit));
3714     }
3715   } else {
3716     td->rsn[0] = r0;
3717     td->rsn[1] = r1;
3718     if (lgl->level == 1) {
3719       assert (tag != UNITCS);
3720       if (tag == DECISION) irr = 1;
3721       else if ((irr = !(red = (r0 & REDCS)))) {
3722         if (tag == BINCS) {
3723           other = r0 >> RMSHFT;
3724           irr = lgltd (lgl, other)->irr;
3725         } else if (tag == TRNCS) {
3726           other = r0 >> RMSHFT;
3727           if ((irr = lgltd (lgl, other)->irr)) {
3728             other2 = r1;
3729             irr = lgltd (lgl, other2)->irr;
3730           }
3731         } else {
3732           assert (tag == LRGCS);
3733           lidx = r1;
3734           c = lglidx2lits (lgl, red, lidx);
3735           found = 0;
3736           for (p = c; irr && (other = *p); p++)
3737             if (other == lit) found++;
3738             else irr = lgltd (lgl, other)->irr;
3739           assert (!irr || found == 1);
3740         }
3741       }
3742     } else irr = 0;
3743     td->irr = irr;
3744   }
3745
3746   lglpushstk (lgl, &lgl->trail, lit);
3747   if (!lgl->failed && (av->assumed & (1u << (lit > 0)))) {
3748     LOG (2, "failed assumption %d", -lit);
3749     lgl->failed = -lit;
3750   }
3751   lgl->unassigned--;
3752   td->lrglue = 0;
3753   if ((r0 & REDCS) && (r0 & MASKCS) == LRGCS) {
3754     glue = r1 & GLUEMASK;
3755     lgl->stats->lir[glue].forcing++;
3756     assert (lgl->stats->lir[glue].forcing > 0);
3757     if (lgl->level && 0 < glue && glue < MAXGLUE) {
3758       lgl->lrgluereasons++;
3759       assert (lgl->lrgluereasons > 0);
3760       td->lrglue = 1;
3761     }
3762 #ifndef NDEBUG
3763     if (glue == MAXGLUE)
3764       assert ((r1 >> GLUESHFT) + 4 < lglcntstk (&lgl->red[MAXGLUE]));
3765 #endif
3766   }
3767 }
3768
3769 static void lglf2rce (LGL * lgl, int lit, int other, int red) {
3770   assert (lglval (lgl, other) < 0);
3771   assert (!red || red == REDCS);
3772   assert (!lgliselim (lgl, other));
3773   lglassign (lgl, lit, ((other << RMSHFT) | BINCS | red), 0);
3774 }
3775
3776 static void lglf3rce (LGL * lgl, int lit, int other, int other2, int red) {
3777   assert (lglval (lgl, other) < 0);
3778   assert (lglval (lgl, other2) < 0);
3779   assert (!lgliselim (lgl, other));
3780   assert (!lgliselim (lgl, other2));
3781   assert (!red || red == REDCS);
3782   lglassign (lgl, lit, ((other << RMSHFT) | TRNCS | red), other2);
3783 }
3784
3785 static void lglflrce (LGL * lgl, int lit, int red, int lidx) {
3786 #ifndef NDEBUG
3787   int * p = lglidx2lits (lgl, red, lidx), other;
3788   while ((other = *p++)) {
3789     assert (!lgliselim (lgl, other));
3790     if (other != lit) assert (lglval (lgl, other) < 0);
3791   }
3792   assert (red == 0 || red == REDCS);
3793 #endif
3794   lglassign (lgl, lit, red | LRGCS, lidx);
3795 }
3796
3797 static int lgldscheduled (LGL * lgl, int lit) {
3798   return lglqvar (lgl, lit)->pos >= 0;
3799 }
3800
3801 static void lglunassign (LGL * lgl, int lit) {
3802   int idx = abs (lit), r0, r1, tag, lidx, glue;
3803   TD *  td;
3804   LOG (2, "unassign %d", lit);
3805   assert (lglval (lgl, lit) > 0);
3806   assert (lgl->vals[idx] == lglsgn (lit));
3807   lgl->vals[idx] = 0;
3808   lgl->unassigned++;
3809   assert (lgl->unassigned > 0);
3810   if (!lgldscheduled (lgl, lit)) lgldsched (lgl, idx);
3811   td = lgltd (lgl, idx);
3812   r0 = td->rsn[0];
3813   if (!(r0 & REDCS)) return;
3814   tag = r0 & MASKCS;
3815   if (tag != LRGCS) return;
3816   r1 = td->rsn[1];
3817   glue = r1 & GLUEMASK;
3818   if (td->lrglue) {
3819     assert (lgl->lrgluereasons > 0);
3820     lgl->lrgluereasons--;
3821   }
3822   if (glue < MAXGLUE) return;
3823   lidx = r1 >> GLUESHFT;
3824   LOG (2, "eagerly deleting maximum glue clause at %d", lidx);
3825   lglrststk (&lgl->red[glue], lidx);
3826 }
3827
3828 static Val lglifixed (LGL * lgl, int lit) {
3829   int res;
3830   if (!(res = lglval (lgl, lit))) return 0;
3831   if (lglevel (lgl, lit) > 0) return 0;
3832   return res;
3833 }
3834
3835 static void lglbacktrack (LGL * lgl, int level) {
3836   int lit;
3837   assert (level >= 0);
3838   assert (lgl->level > level);
3839   LOG (2, "backtracking to level %d", level);
3840   assert (level <= lgl->level);
3841   assert (abs (lgl->failed) != 1 || lgl->failed == -1);
3842   if (lgl->failed &&
3843       lgl->failed != -1 &&
3844       lglevel (lgl, lgl->failed) > level) {
3845     LOG (2, "resetting failed assumption %d", lgl->failed);
3846     lgl->failed = 0;
3847   }
3848   while (!lglmtstk (&lgl->trail)) {
3849     lit = lgltopstk (&lgl->trail);
3850     assert (abs (lit) > 1);
3851     if (lglevel (lgl, lit) <= level) break;
3852     lglunassign (lgl, lit);
3853     lgl->trail.top--;
3854   }
3855   if (!level) {
3856     assert (!lgl->lrgluereasons);
3857     while (!lglmtstk (&lgl->red[MAXGLUE])) {
3858       int tmp = lglpopstk (&lgl->red[MAXGLUE]);
3859       assert (tmp >= NOTALIT);
3860       (void) tmp;
3861     }
3862   }
3863   if (lgl->alevel > level) {
3864     LOG (2,
3865          "resetting assumption decision level to %d from %d",
3866        &