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