backends/precosat/precosat.hh

   1 /***************************************************************************
   2 Copyright (c) 2009, Armin Biere, Johannes Kepler University.
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy
   5 of this software and associated documentation files (the "Software"), to
   6 deal in the Software without restriction, including without limitation the
   7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
   8 sell copies of the Software, and to permit persons to whom the Software is
   9 furnished to do so, subject to the following conditions:
  10
  11 The above copyright notice and this permission notice shall be included in
  12 all copies or substantial portions of the Software.
  13
  14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
  17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
  20 IN THE SOFTWARE.
  21 ****************************************************************************/
  22
  23 #ifndef PrecoSat_hh_INCLUDED
  24 #define PrecoSat_hh_INCLUDED
  25
  26 #include <cassert>
  27 #include <cstdlib>
  28 #include <climits>
  29 #include <cstdarg>
  30 #include <cstring>
  31 #include <cstdio>
  32
  33 namespace PrecoSat {
  34
  35 void die (const char *, ...);
  36
  37 class Mem {
  38 public:
  39   typedef void * (*NewFun)(void *, size_t);
  40   typedef void (*DeleteFun)(void *, void*, size_t);
  41   typedef void * (*ResizeFun)(void *, void *, size_t, size_t);
  42 private:
  43   size_t cur, max;
  44   void * emgr; NewFun newfun; DeleteFun deletefun; ResizeFun resizefun;
  45   void operator += (size_t b) { if ((cur += b) > max) max = cur; }
  46   void operator -= (size_t b) { assert (cur >= b); cur -= b; }
  47 public:
  48   Mem () : cur(0), max(0), emgr(0), newfun(0), deletefun(0), resizefun(0) { }
  49   void set (void * e, NewFun n, DeleteFun d, ResizeFun r) {
  50     assert (e && n && d && r);
  51     emgr = e; newfun = n; deletefun = d; resizefun = r;
  52   }
  53   operator size_t () const { return cur; }
  54   size_t getCurrent () const { return cur; }
  55   size_t getMax () const { return max; }
  56   void * allocate (size_t bytes) {
  57     size_t mb = bytes >> 20;
  58     void * res;
  59     res = newfun ? newfun (emgr, bytes) : malloc (bytes);
  60     if (!res) die ("out of memory allocating %d MB", mb);
  61     *this += bytes;
  62     return res;
  63   }
  64   void * callocate (size_t bytes) {
  65     void * res = allocate (bytes);
  66     memset (res, 0, bytes);
  67     return res;
  68   }
  69   void * reallocate (void * ptr, size_t old_bytes, size_t new_bytes) {
  70     size_t mb = new_bytes >> 20;
  71     *this -= old_bytes;
  72     void * res  = resizefun ? resizefun (emgr, ptr, old_bytes, new_bytes) :
  73                               realloc (ptr, new_bytes);
  74     if (!res) die ("out of memory reallocating %ld MB", (long) mb);
  75     *this += new_bytes;
  76     return res;
  77   }
  78   void * recallocate (void * ptr, size_t o, size_t n) {
  79     char * res = (char*) reallocate (ptr, o, n);
  80     if (n > o) memset (res + o, 0, n - o);
  81     return (void*) res;
  82   }
  83   void deallocate (void * ptr, size_t bytes) {
  84     *this -= bytes;
  85     if (deletefun) deletefun (emgr, ptr, bytes);
  86     else free (ptr);
  87   }
  88 };
  89
  90 template<class T> class Stack {
  91   T * a, * t, * e;
  92   int size () const { return e - a; }
  93 public:
  94   size_t bytes () const { return size () * sizeof (T); }
  95 private:
  96   void enlarge (Mem & m) {
  97     assert (t == e);
  98     size_t ob = bytes ();
  99     int o = size ();
 100     int s = o ? 2 * o : 1;
 101     size_t nb = s * sizeof (T);
 102     a = (T*) m.reallocate (a, ob, nb);
 103     t = a + o;
 104     e = a + s;
 105   }
 106 public:
 107   Stack () : a (0), t (0), e (0) { }
 108   ~Stack () { free (a); }
 109   operator int () const { return t - a; }
 110   void push (Mem & m, const T & d) { if (t == e) enlarge (m); *t++ = d; }
 111   const T & pop () { assert (a < t); return *--t; }
 112   const T & top () { assert (a < t); return t[-1]; }
 113   T & operator [] (int i) { assert (i < *this); return a[i]; }
 114   void shrink (int m = 0) { assert (m <= *this); t = a + m; }
 115   void shrink (T * nt) { assert (a <= nt); assert (nt <= t); t = nt; }
 116   void release (Mem & m) { m.deallocate (a, bytes ()); a = t = e = 0; }
 117   const T * begin () const { return a; }
 118   const T * end () const { return t; }
 119   T * begin () { return a; }
 120   T * end () { return t; }
 121   void remove (const T & d) {
 122     assert (t > a);
 123     T prev = *--t;
 124     if (prev == d) return;
 125     T * p = t;
 126     for (;;) {
 127       assert (p > a);
 128       T next = *--p;
 129       *p = prev;
 130       if (next == d) return;
 131       prev = next;
 132     }
 133   }
 134 };
 135
 136 template<class T, class L> class Heap {
 137   Stack<T *> stack;
 138   static int left (int p) { return 2 * p + 1; }
 139   static int right (int p) { return 2 * p + 2; }
 140   static int parent (int c) { return (c - 1) / 2; }
 141   static void fix (T * & ptr, ptrdiff_t diff) {
 142     char * charptr = (char *) ptr;
 143     charptr -= diff;
 144     ptr = (T *) charptr;
 145   }
 146 public:
 147   void release (Mem & mem) { stack.release (mem); }
 148   operator int () const { return stack; }
 149   T * operator [] (int i) { return stack[i]; }
 150   bool contains (T * e) const { return e->pos >= 0; }
 151   void up (T * e) {
 152     int epos = e->pos;
 153     while (epos > 0) {
 154       int ppos = parent (epos);
 155       T * p = stack [ppos];
 156       if (L (p, e)) break;
 157       stack [epos] = p, stack [ppos] = e;
 158       p->pos = epos, epos = ppos;
 159     }
 160     e->pos = epos;
 161   }
 162   void down (T * e) {
 163     assert (contains (e));
 164     int epos = e->pos, size = stack;
 165     for (;;) {
 166       int cpos = left (epos);
 167       if (cpos >= size) break;
 168       T * c = stack [cpos], * o;
 169       int opos = right (epos);
 170       if (L (e, c)) {
 171         if (opos >= size) break;
 172         o = stack [opos];
 173         if (L (e, o)) break;
 174         cpos = opos, c = o;
 175       } else if (opos < size) {
 176         o = stack [opos];
 177         if (!L (c, o)) { cpos = opos; c = o; }
 178       }
 179       stack [cpos] = e, stack [epos] = c;
 180       c->pos = epos, epos = cpos;
 181     }
 182     e->pos = epos;
 183   }
 184   void check () {
 185 #ifndef NDEBUG
 186     for (int ppos = 0; ppos < stack; ppos++) {
 187       T * p = stack[ppos];
 188       int lpos = left (ppos);
 189       if (lpos < stack) {
 190         T * l = stack[lpos];
 191         assert (!L (l, p));
 192       } else break;
 193       int rpos = right (ppos);
 194       if (rpos < stack) {
 195         T * r = stack[rpos];
 196         assert (!L (r, p));
 197       } else break;
 198     }
 199 #endif
 200   }
 201   void construct () {
 202     for (int cpos = parent (stack-1); cpos >= 0; cpos--) {
 203       T * e = stack[cpos]; assert (cpos >= 0); down (e);
 204     }
 205     check ();
 206   }
 207   T * max () { assert (stack); return stack[0]; }
 208   void push (Mem & mem, T * e) {
 209     assert (!contains (e));
 210     e->pos = stack;
 211     stack.push (mem, e);
 212     up (e);
 213   }
 214   T * pop () {
 215     int size = stack;
 216     assert (size);
 217     T * res = stack[0];
 218     assert (!res->pos);
 219     if (--size) {
 220       T * other = stack[size];
 221       assert (other->pos == size);
 222       stack[0] = other, other->pos = 0;
 223       stack.shrink (size);
 224       down (other);
 225     } else
 226       stack.shrink ();
 227     res->pos = -1;
 228     return res;
 229   }
 230   void remove (T * e) {
 231     int size = stack;
 232     assert (size > 0);
 233     assert (contains (e));
 234     int epos = e->pos;
 235     e->pos = -1;
 236     if (--size == epos) {
 237       stack.shrink (size);
 238     } else {
 239       T * last = stack[size];
 240       if (size == epos) return;
 241       stack[last->pos = epos] = last;
 242       stack.shrink (size);
 243       up (last);
 244       down (last);
 245     }
 246   }
 247   void fix (ptrdiff_t diff) {
 248     for (T ** p = stack.begin (); p < stack.end (); p++)
 249       fix (*p, diff);
 250   }
 251 };
 252
 253 template<class A, class E>
 254 void dequeue (A & anchor, E * e) {
 255   if (anchor.head == e) { assert (!e->next); anchor.head = e->prev; }
 256   else { assert (e->next); e->next->prev = e->prev; }
 257   if (anchor.tail == e) { assert (!e->prev); anchor.tail = e->next; }
 258   else { assert (e->prev); e->prev->next = e->next; }
 259   e->prev = e->next = 0;
 260   assert (anchor.count > 0);
 261   anchor.count--;
 262 }
 263
 264 template<class A, class E>
 265 bool connected (A & anchor, E * e) {
 266   if (e->prev) return true;
 267   if (e->next) return true;
 268   return anchor.head == e;
 269 }
 270
 271 template<class A, class E>
 272 void push (A & anchor, E * e) {
 273   e->next = 0;
 274   if (anchor.head) anchor.head->next = e;
 275   e->prev = anchor.head;
 276   anchor.head = e;
 277   if (!anchor.tail) anchor.tail = e;
 278   anchor.count++;
 279 }
 280
 281 template<class A, class E>
 282 void enqueue (A & anchor, E * e) {
 283   e->prev = 0;
 284   if (anchor.tail) anchor.tail->prev = e;
 285   e->next = anchor.tail;
 286   anchor.tail = e;
 287   if (!anchor.head) anchor.head = e;
 288   anchor.count++;
 289 }
 290
 291 template<class A, class E>
 292 void mtf (A & a, E * e) { dequeue (a, e); push (a, e); }
 293
 294 struct Cls;
 295
 296 template<class E> struct Anchor {
 297   E * head, * tail;
 298   long count;
 299   Anchor () : head (0), tail (0), count (0) { }
 300 };
 301
 302 struct Rnk { int heat; int pos; };
 303
 304 struct Hotter {
 305   Rnk * a, * b;
 306   Hotter (Rnk * r, Rnk * s) : a (r), b (s) { }
 307   operator bool () const {
 308     if (a->heat > b->heat) return true;
 309     if (a->heat < b->heat) return false;
 310     return a < b;
 311   }
 312 };
 313
 314 typedef signed char Val;
 315
 316 enum Vrt {
 317   FREE = 0,
 318   ZOMBIE = 1,
 319   PURE = 2,
 320   ELIM = 3,
 321   EQUIV = 4,
 322   FIXED = 5,
 323 };
 324
 325 typedef enum Vrt Vrt;
 326
 327 struct Var {
 328   Val phase:2, mark:2;
 329   bool onstack:1,removable:1,poison:1;
 330   bool binary:1;
 331   bool onplits:1;
 332   Vrt type : 3;
 333   int tlevel, dlevel, dominator;
 334   union { Cls * cls; int lit; } reason;
 335 };
 336
 337 struct Cls {
 338   static const unsigned LDMAXGLUE = 4, MAXGLUE = (1<<LDMAXGLUE)-1;
 339   bool locked:1,lnd:1,garbage:1;
 340   bool binary:1,trash:1,dirty:1;
 341   bool gate:1,str:1,fresh:1;
 342   static const int LDMAXSZ = 32 - 10 - LDMAXGLUE, MAXSZ = (1<<LDMAXSZ)-1;
 343   bool glued:1;
 344   unsigned glue:LDMAXGLUE, size:LDMAXSZ, sig;
 345   Cls * prev, * next;
 346   int lits[4];
 347   static size_t bytes (int n);
 348   size_t bytes () const;
 349   Cls (int l0 = 0, int l1 = 0, int l2 = 0)
 350     { lits[0] = l0; lits[1] = l1; lits[2] = l2; lits[3] = 0; }
 351   int minlit () const;
 352   bool contains (int) const;
 353   void print (const char * prefix = "") const;
 354 };
 355
 356 struct Frame {
 357   bool pulled : 1, contained:1;
 358   int tlevel : 30;
 359   Frame (int t) : pulled (false), contained (false), tlevel (t) { }
 360 };
 361
 362 struct GateStats { int count, len; };
 363
 364 struct Stats {
 365   struct { int fixed, equiv, elim, subst, zombies, pure, merged; } vars;
 366   struct { int orig, bin, lnd, irr, lckd, gc; } clauses;
 367   struct { long long added; int bssrs, ssrs; } lits;
 368   struct { long long deleted, strong, inverse; int depth; } mins;
 369   int conflicts, decisions, random, enlarged, shrunken, rescored, iter;
 370   struct { int count, skipped, maxdelta; } restart;
 371   struct { int count, level1, probing; } doms;
 372   struct { GateStats nots, ites, ands, xors; } subst;
 373   struct { int fw, bw, dyn, org, doms, red; } subs;
 374   struct { long long resolutions; int impl, expl, phases, rounds; } blkd;
 375   struct { int fw, bw, dyn, org, asym; } str;
 376   struct { struct { int bin, trn, large; } dyn, stat; } otfs;
 377   struct { long long slimmed, sum, count; } glue;
 378   struct { int count, maxdelta; } rebias;
 379   struct { int variables, phases, rounds, failed, lifted, merged; } probe;
 380   struct { int nontriv, fixed, merged; } sccs;
 381   struct { int forced, assumed, flipped; } extend;
 382   struct { long long resolutions; int phases, rounds; } elim;
 383   struct { struct { struct { long long srch,hits; } l1,l2;} fw,bw;} sigs;
 384   struct { int expl, elim, blkd; } pure;
 385   struct { int expl, elim, blkd; } zombies;
 386   struct { long long srch, simp; } props;
 387   long long visits, ternaryvisits, blocked, sumheight, collected;
 388   int simps, reductions, gcs, reports, maxdepth, printed;
 389   double entered, time, simptime, srchtime, entered2;
 390   static double now ();
 391   double seconds ();
 392   double height ();
 393   void sw2srch ();
 394   void sw2simp ();
 395   Stats ();
 396 };
 397
 398 struct Limit {
 399   int decisions, simp, strength;
 400   struct { int conflicts, inc, init; } enlarge;
 401   struct { int conflicts, lcnt, inner, outer; } restart;
 402   struct { int conflicts, lcnt; } rebias;
 403   struct { int learned, fresh, init; } reduce;
 404   struct { int iter, reduce, probe, elim, block, simp; } fixed;
 405   struct { long long simp, probe, elim, block, asym; } props;
 406   struct {
 407     struct { int sub, str; } fw;
 408     struct { int sub, str; } bw;
 409     int red;
 410   } budget;
 411   Limit ();
 412 };
 413
 414 struct Opt {
 415   const char * name;
 416   int * valptr, min, max;
 417   Opt (const char * n, int v, int * vp, int mi, int ma);
 418 };
 419
 420 struct Opts {
 421   int quiet, verbose, print;
 422   int dominate, maxdoms;
 423   int plain, rtc;
 424   int merge;
 425   int otfs;
 426   int redsub;
 427   int block,blockimpl,blockprd,blockint,blockrtc,blockclim,blockotfs;
 428   int blockreward,blockboost;
 429   int simprd, simpinc, simprtc;
 430   int probe,probeprd,probeint,probertc,probereward,probeboost;
 431   int decompose;
 432   int inverse,inveager,mtfall,mtfrev;
 433   int bumpuip,bumpsort,bumprev,bumpbulk,bumpturbo;
 434   int glue, slim, sticky;
 435   int elim,elimgain,elimin,elimprd,elimint,elimrtc,elimclim;
 436   int elimreward,elimboost,elimasym,elimasymint,elimasymreward;
 437   int subst, ands, xors, ites;
 438   int fwmaxlen,bwmaxlen,reslim,blkmaxlen;
 439   int heatinc;
 440   int restart, restartint, luby, restartinner, restartouter;
 441   int rebias, rebiasint;
 442   int minlimit, maxlimit;
 443   int dynred;
 444   int liminitmode;//0=constant,1=relative
 445   int liminitmax, liminitconst, liminitpercent;
 446   int limincmode;//0=constant,1=relative
 447   int liminconst1, liminconst2;
 448   int limincpercent;
 449   int enlinc;
 450   int shrink,shrinkfactor;
 451   int fresh;
 452   int random, spread, seed;
 453   int order;
 454   enum MinMode { NONE=0, LOCAL=1, RECUR=2, STRONG=3, STRONGER=4 };
 455   int minimize, maxdepth, strength;
 456   int check;
 457   int skip;
 458   const char * output;//for 'print'
 459   bool fixed;
 460   Stack<Opt> opts;
 461   Opts () : fixed (false) { }
 462   bool set (const char *, int);
 463   bool set (const char *, const char *);
 464   void add (Mem &, const char * name, int, int *, int, int);
 465   void printoptions (FILE *, const char *prfx) const;
 466 };
 467
 468 struct SCC { unsigned idx, min : 31; bool done : 1; };
 469
 470 class RNG {
 471   unsigned state;
 472 public:
 473   RNG () : state (0) { }
 474   unsigned next ();
 475   bool oneoutof (unsigned);
 476   void init (unsigned seed) { state = seed; }
 477 };
 478
 479 struct Occ {
 480   int blit;
 481   Cls * cls;
 482   Occ (int b, Cls * c) : blit (b), cls (c) { }
 483   bool operator == (const Occ & o) const
 484     { return cls ? o.cls == cls : o.blit == blit; }
 485 };
 486
 487 struct Occs {
 488   Stack<int> bins;
 489   Stack<Occ> large;
 490 };
 491
 492 typedef Stack<Cls*> Orgs;
 493 typedef Stack<Cls*> Fwds;
 494
 495 class Solver {
 496   bool initialized;
 497   Val * vals;
 498   Var * vars;
 499   int * jwhs, * repr, * iirfs;
 500   Occs * occs;
 501   Orgs * orgs;
 502   Fwds * fwds;
 503   unsigned * bwsigs, * fwsigs;
 504   Rnk * rnks, * prbs, * elms, * blks;
 505   struct { Heap<Rnk,Hotter> decide, probe, elim, block; } schedule;
 506   int maxvar, size, queue, queue2, level, jlevel, uip, open, resolved;
 507   Stack<int> trail, lits, units, levels, saved, elits, plits, check;
 508   Stack<Frame> frames;
 509   Stack<Var *> seen;
 510   Stack<Cls *> trash, gate, strnd;
 511   Cls * conflict, empty, dummy;
 512   Anchor<Cls> original, binary, fresh, learned[Cls::MAXGLUE+1];
 513   int hinc, simprd, agility, spread, posgate, gatepivot, gatelen, typecount;
 514   int elimvar, blklit;
 515   char lastype;
 516   GateStats * gatestats;
 517   bool terminal, iterating, blkmode, extending;
 518   bool resotfs, reslimhit, simplified, needrescore;
 519   bool measure, elimode, bkdmode, puremode, asymode;
 520   RNG rng;
 521   Stats stats;
 522   Limit limit;
 523   char * prfx;
 524   FILE * out;
 525   Opts opts;
 526   Mem mem;
 527
 528   Rnk * prb (const Rnk *);
 529   Rnk * rnk (const Var *);
 530   Var * var (const Rnk *);
 531
 532   int & iirf (Var *, int);
 533
 534   Val fixed (int lit) const;
 535
 536   void initerm ();
 537   void initfwds ();
 538   void initfwsigs ();
 539   void initbwsigs ();
 540   void initorgs ();
 541   void initiirfs ();
 542   void clrbwsigs ();
 543   void rszbwsigs (int newsize);
 544   void rsziirfs (int newsize);
 545   void delorgs ();
 546   void delfwds ();
 547   void delfwsigs ();
 548   void delbwsigs ();
 549   void deliirfs ();
 550   void delclauses (Anchor<Cls> &);
 551   Anchor<Cls> & anchor (Cls *);
 552
 553   void initprfx (const char *);
 554   void delprfx ();
 555
 556   void resize (int);
 557
 558   void initreduce ();
 559   void initfresh ();
 560   void initbias ();
 561   void initrestart ();
 562   void initlimit (int);
 563   void initsearch (int);
 564
 565   long long clauses () const;
 566   int recyclelimit () const;
 567   bool recycling () const;
 568   bool reducing () const;
 569   bool eliminating () const;
 570   bool blocking () const;
 571   bool simplifying () const;
 572   bool restarting () const;
 573   bool rebiasing () const;
 574   bool probing () const;
 575   bool enlarging () const;
 576   bool exhausted () const;
 577
 578   int remvars () const;
 579
 580   void marklits (Cls *);
 581   void marklits ();
 582   void unmarklits ();
 583   void unmarklits (Cls *);
 584   bool fworgs ();
 585   void bworgs ();
 586   bool fwoccs ();
 587   void bwoccs (bool & learned);
 588   Cls * clause (bool learned, unsigned glue);
 589   unsigned litsig ();
 590   int redundant (Cls *);
 591   void recycle (Cls *);
 592   void recycle (int);
 593   void setsig (Cls *);
 594   void slim (Cls *);
 595   unsigned gluelits ();
 596   bool clt (int, int) const;
 597   void connect (Cls *);
 598   void connect (Anchor<Cls>&, bool orgonly = false);
 599   void disconnect (Cls *);
 600   void disconnect ();
 601   void collect (Cls *);
 602   int bwstr (unsigned sig, Cls *);
 603   int fwstr (unsigned sig, Cls *);
 604   void remove (int lit, Cls *);
 605   bool fwsub (unsigned sig, Cls *);
 606   bool bwsub (unsigned sig, Cls *);
 607   void assign (int l);
 608   void assume (int l, bool inclevel = true);
 609   void imply (int l, int reason);
 610   int dominator (int l, Cls * reason, bool &);
 611   void force (int l, Cls * reason);
 612   void unit (int l);
 613   bool min2 (int lit, int other, int depth);
 614   bool minl (int lit, Cls *, int depth);
 615   bool strengthen (int lit, int depth);
 616   bool inverse (int lit);
 617   bool minimize (Var *, int depth);
 618   int luby (int);
 619   void report (int v, char ch);
 620   void prop2 (int lit);
 621   void propl (int lit);
 622   void flushunits ();
 623   bool bcp ();
 624   bool needtoflush () const;
 625   bool flush ();
 626   void touchpure (int lit);
 627   void touchelim (int lit);
 628   void touchblkd (int lit);
 629   void touch (int lit);
 630   void touch (Cls *);
 631   void rescore ();
 632   void bump (Cls *);
 633   void bump (Var *, int add);
 634   void bump ();
 635   int phase (Var *);
 636   bool decide ();
 637   void extend ();
 638   void increp ();
 639   void probe ();
 640   int find (int lit);
 641   void merge (int, int, int & merged);
 642   void shrink (int);
 643   void enlarge ();
 644   void checkvarstats ();
 645   void decompose ();
 646   bool resolve (int l, int pivot, int k, bool tryonly);
 647   bool resolve (int l, int pivot, Cls *, bool tryonly);
 648   bool resolve (Cls *, int pivot, Cls *, bool tryonly);
 649   bool andgate (int lit);
 650   Cls * find (int a, int b, int c);
 651   int itegate (int lit, int cond, int t);
 652   bool itegate (int lit);
 653   bool xorgate (int lit);
 654   bool hasgate (int idx);
 655   bool trelim (int idx);
 656   void elim (int idx);
 657   void elim ();
 658   void block (Cls *, int lit);
 659   void block (int lit);
 660   void block ();
 661   void zombie (Var*);
 662   void pure (int lit);
 663   void pure ();
 664   void cleantrash ();
 665   void cleangate ();
 666   void cleanlevels ();
 667   void cleanseen ();
 668   void jump ();
 669   void dump (Cls *);
 670   void gcls (Cls *);
 671   void strcls (Cls *c);
 672   void gc (Anchor<Cls> &, const char*);
 673   void gc ();
 674   void jwh (Cls *);
 675   void jwh ();
 676   void reduce ();
 677   void simplify ();
 678   void iteration ();
 679   void restart ();
 680   void rebias ();
 681   void undo (int newlevel, bool save = false);
 682   void pull (int lit);
 683   bool analyze ();
 684
 685   void checkeliminated ();
 686   void cleans ();
 687   void checkclean ();
 688
 689   void import ();
 690   int search ();
 691   bool satisfied (const Cls*);
 692   bool satisfied (Anchor<Cls> &);
 693
 694   void print ();
 695
 696   void dbgprint (const char *, Cls *);
 697   void dbgprint (const char *, Anchor<Cls> &);
 698   void dbgprint ();
 699   void dbgprintgate ();
 700
 701   void checkgate ();
 702
 703 public:
 704
 705   Solver () : initialized (false) { }
 706
 707   void set (void * e, Mem::NewFun n, Mem::DeleteFun d, Mem::ResizeFun r) {
 708     mem.set (e, n, d, r);
 709   }
 710   void setprfx (const char* newprfx) { delprfx (); initprfx (newprfx); }
 711   bool set (const char * option, int arg) { return opts.set (option, arg); }
 712   bool set (const char * o, const char * a) { return opts.set (o, a); }
 713   void set (FILE * file) { out = file; initerm (); }
 714
 715   void init (int initial_maxvar = 0);
 716   void fxopts ();
 717
 718   void add (int lit) { if (lit) lits.push (mem, lit); else import (); }
 719   int next () { int res = maxvar + 1; resize (res); return res; }
 720   int solve (int decision_limit = INT_MAX);
 721   int val (int l) { return vals[find (l)]; }
 722   double seconds () { return stats.seconds (); }
 723   bool satisfied ();
 724   void prstats ();
 725   void propts ();
 726   void reset ();
 727   int getMaxVar () const { return maxvar; }
 728 };
 729
 730 };
 731
 732 #endif