picosat.c

/****************************************************************************
Copyright (c) 2006 - 2015, Armin Biere, Johannes Kepler University.

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal in the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.
****************************************************************************/

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <assert.h>
#include <limits.h>
#include <ctype.h>
#include <stdarg.h>
#include <stdint.h>

#include "picosat.h"

/* Initialization of global feature variables */
enum Phase GLOBAL_DEFAULT_PHASE = 0;
int ALLSAT = 0;
int PARTIAL = 0;
int PLAIN = 0;
const char * COMPACT_TRACE_NAME = 0;
const char * EXTENDED_TRACE_NAME = 0;
const char * RUP_TRACE_NAME = 0;
FILE * INCREMENTAL_RUP_FILE = 0;

/* By default code for 'all different constraints' is disabled, since 'NADC'
 * is defined.
 */
#define NADC

/* By default we enable failed literals, since 'NFL' is undefined.
 *
#define NFL
 */

/* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined.
 *
#define NDSC
 */

/* Do not use luby restart schedule instead of inner/outer.
 *
#define NLUBY
 */

/* Enabling this define, will use gnuplot to visualize how the scores evolve.
 *
#define VISCORES 
 */
#ifdef VISCORES
// #define WRITEGIF		/* ... to generate a video */
#endif

#ifdef VISCORES
#ifndef WRITEGIF
#include <unistd.h>		/* for 'usleep' */
#endif
#endif

#ifdef RCODE
#include <R.h>
#endif

#define MINRESTART	100	/* minimum restart interval */
#define MAXRESTART	1000000 /* maximum restart interval */
#define RDECIDE		1000	/* interval of random decisions */
#define FRESTART	110	/* restart increase factor in percent */
#define FREDUCE		110	/* reduce increase factor in percent  */
#define FREDADJ		121	/* reduce increase adjustment factor */
#define MAXCILS		10	/* maximal number of unrecycled internals */
#define FFLIPPED	10000	/* flipped reduce factor */
#define FFLIPPEDPREC	10000000/* flipped reduce factor precision */
#define INTERRUPTLIM	1024	/* check interrupt after that many decisions */

#ifndef TRACE
#define NO_BINARY_CLAUSES	/* store binary clauses more compactly */
#endif

/* For debugging purposes you may want to define 'LOGGING', which actually
 * can be enforced by using './configure.sh --log'.
 */
#ifdef LOGGING
#define LOG(code) do { code; } while (0)
#else
#define LOG(code) do { } while (0)
#endif
#define NOLOG(code) do { } while (0)		/* log exception */
#define ONLYLOG(code) do { code; } while (0)	/* force logging */

#define FALSE ((Val)-1)
#define UNDEF ((Val)0)
#define TRUE ((Val)1)

#define COMPACT_TRACECHECK_TRACE_FMT 0
#define EXTENDED_TRACECHECK_TRACE_FMT 1
#define RUP_TRACE_FMT 2

#define NEWN(p,n) do { (p) = new (ps, sizeof (*(p)) * (n)); } while (0)
#define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0)
#define CLR(p) CLRN(p,1)
#define DELETEN(p,n) \
  do { delete (ps, p, sizeof (*(p)) * (n)); (p) = 0; } while (0)

#define RESIZEN(p,old_num,new_num) \
  do { \
    size_t old_size = sizeof (*(p)) * (old_num); \
    size_t new_size = sizeof (*(p)) * (new_num); \
    (p) = resize (ps, (p), old_size, new_size) ; \
  } while (0)

#define ENLARGE(start,head,end) \
  do { \
    unsigned old_num = (ptrdiff_t)((end) - (start)); \
    size_t new_num = old_num ? (2 * old_num) : 1; \
    unsigned count = (head) - (start); \
    assert ((start) <= (end)); \
    RESIZEN((start),old_num,new_num); \
    (head) = (start) + count; \
    (end) = (start) + new_num; \
  } while (0)

#define NOTLIT(l) (ps->lits + (1 ^ ((l) - ps->lits)))

#define LIT2IDX(l) ((ptrdiff_t)((l) - ps->lits) / 2)
#define LIT2IMPLS(l) (ps->impls + (ptrdiff_t)((l) - ps->lits))
#define LIT2INT(l) ((int)(LIT2SGN(l) * LIT2IDX(l)))
#define LIT2SGN(l) (((ptrdiff_t)((l) - ps->lits) & 1) ? -1 : 1)
#define LIT2VAR(l) (ps->vars + LIT2IDX(l))
#define LIT2HTPS(l) (ps->htps + (ptrdiff_t)((l) - ps->lits))
#define LIT2JWH(l) (ps->jwh + ((l) - ps->lits))

#ifndef NDSC
#define LIT2DHTPS(l) (ps->dhtps + (ptrdiff_t)((l) - ps->lits))
#endif

#ifdef NO_BINARY_CLAUSES
typedef uintptr_t Wrd;
#define ISLITREASON(C) (1&(Wrd)C)
#define LIT2REASON(L) \
  (assert (L->val==TRUE), ((Cls*)(1 + (2*(L - ps->lits)))))
#define REASON2LIT(C) ((Lit*)(ps->lits + ((Wrd)C)/2))
#endif

#define ENDOFCLS(c) ((void*)((Lit**)(c)->lits + (c)->size))

#define SOC ((ps->oclauses == ps->ohead) ? ps->lclauses : ps->oclauses)
#define EOC (ps->lhead)
#define NXC(p) (((p) + 1 == ps->ohead) ? ps->lclauses : (p) + 1)

#define OIDX2IDX(idx) (2 * ((idx) + 1))
#define LIDX2IDX(idx) (2 * (idx) + 1)

#define ISLIDX(idx) ((idx)&1)

#define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1)
#define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2)

#define EXPORTIDX(idx) \
  ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ps->ohead - ps->oclauses)) : IDX2OIDX(idx)) + 1)

#define IDX2CLS(i) \
  (assert(i), (ISLIDX(i) ? ps->lclauses : ps->oclauses)[(i)/2 - !ISLIDX(i)])

#define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? ps->zhains[(i)/2] : 0))

#define CLS2TRD(c) (((Trd*)(c)) - 1)
#define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx)

#define CLS2ACT(c) \
  ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c)))

#define VAR2LIT(v) (ps->lits + 2 * ((v) - ps->vars))
#define VAR2RNK(v) (ps->rnks + ((v) - ps->vars))

#define RNK2LIT(r) (ps->lits + 2 * ((r) - ps->rnks))
#define RNK2VAR(r) (ps->vars + ((r) - ps->rnks))

#define BLK_FILL_BYTES 8
#define SIZE_OF_BLK (sizeof (Blk) - BLK_FILL_BYTES)

#define PTR2BLK(void_ptr) \
  ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - SIZE_OF_BLK) : 0)

#define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0)
#define PERCENT(a,b) (100.0 * AVERAGE(a,b))

#ifndef RCODE
#define ABORT(msg) \
  do { \
    fputs ("*** picosat: " msg "\n", stderr); \
    abort (); \
  } while (0)
#else
#define ABORT(msg) \
  do { \
    Rf_error (msg); \
  } while (0)
#endif

#define ABORTIF(cond,msg) \
  do { \
    if (!(cond)) break; \
    ABORT (msg); \
  } while (0)

#define ZEROFLT		(0x00000000u)
#define EPSFLT		(0x00000001u)
#define INFFLT		(0xffffffffu)

#define FLTCARRY	(1u << 25)
#define FLTMSB		(1u << 24)
#define FLTMAXMANTISSA	(FLTMSB - 1)

#define FLTMANTISSA(d)	((d) & FLTMAXMANTISSA)
#define FLTEXPONENT(d)	((int)((d) >> 24) - 128)

#define FLTMINEXPONENT	(-128)
#define FLTMAXEXPONENT	(127)

#define CMPSWAPFLT(a,b) \
  do { \
    Flt tmp; \
    if (((a) < (b))) \
      { \
	tmp = (a); \
	(a) = (b); \
	(b) = tmp; \
      } \
  } while (0)

#define UNPACKFLT(u,m,e) \
  do { \
    (m) = FLTMANTISSA(u); \
    (e) = FLTEXPONENT(u); \
    (m) |= FLTMSB; \
  } while (0)

#define INSERTION_SORT_LIMIT 10

#define SORTING_SWAP(T,p,q) \
do { \
  T tmp = *(q); \
  *(q) = *(p); \
  *(p) = tmp; \
} while (0)

#define SORTING_CMP_SWAP(T,cmp,p,q) \
do { \
  if ((cmp) (ps, *(p), *(q)) > 0) \
    SORTING_SWAP (T, p, q); \
} while(0)

#define QUICKSORT_PARTITION(T,cmp,a,l,r) \
do { \
  T pivot; \
  int j; \
  i = (l) - 1; 			/* result in 'i' */ \
  j = (r); \
  pivot = (a)[j]; \
  for (;;) \
    { \
      while ((cmp) (ps, (a)[++i], pivot) < 0) \
	; \
      while ((cmp) (ps, pivot, (a)[--j]) < 0) \
        if (j == (l)) \
	  break; \
      if (i >= j) \
	break; \
      SORTING_SWAP (T, (a) + i, (a) + j); \
    } \
  SORTING_SWAP (T, (a) + i, (a) + (r)); \
} while(0)

#define QUICKSORT(T,cmp,a,n) \
do { \
  int l = 0, r = (n) - 1, m, ll, rr, i; \
  assert (ps->ihead == ps->indices); \
  if (r - l <= INSERTION_SORT_LIMIT) \
    break; \
  for (;;) \
    { \
      m = (l + r) / 2; \
      SORTING_SWAP (T, (a) + m, (a) + r - 1); \
      SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r - 1); \
      SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r); \
      SORTING_CMP_SWAP (T, cmp, (a) + r - 1, (a) + r); \
      QUICKSORT_PARTITION (T, cmp, (a), l + 1, r - 1); \
      if (i - l < r - i) \
	{ \
	  ll = i + 1; \
	  rr = r; \
	  r = i - 1; \
	} \
      else \
	{ \
	  ll = l; \
	  rr = i - 1; \
	  l = i + 1; \
	} \
      if (r - l > INSERTION_SORT_LIMIT) \
	{ \
	  assert (rr - ll > INSERTION_SORT_LIMIT); \
	  if (ps->ihead == ps->eoi) \
	    ENLARGE (ps->indices, ps->ihead, ps->eoi); \
	  *ps->ihead++ = ll; \
	  if (ps->ihead == ps->eoi) \
	    ENLARGE (ps->indices, ps->ihead, ps->eoi); \
	  *ps->ihead++ = rr; \
	} \
      else if (rr - ll > INSERTION_SORT_LIMIT) \
        { \
	  l = ll; \
	  r = rr; \
	} \
      else if (ps->ihead > ps->indices) \
	{ \
	  r = *--ps->ihead; \
	  l = *--ps->ihead; \
	} \
      else \
	break; \
    } \
} while (0)

#define INSERTION_SORT(T,cmp,a,n) \
do { \
  T pivot; \
  int l = 0, r = (n) - 1, i, j; \
  for (i = r; i > l; i--) \
    SORTING_CMP_SWAP (T, cmp, (a) + i - 1, (a) + i); \
  for (i = l + 2; i <= r; i++)  \
    { \
      j = i; \
      pivot = (a)[i]; \
      while ((cmp) (ps, pivot, (a)[j - 1]) < 0) \
        { \
	  (a)[j] = (a)[j - 1]; \
	  j--; \
	} \
      (a)[j] = pivot; \
    } \
} while (0)

#ifdef NDEBUG
#define CHECK_SORTED(cmp,a,n) do { } while(0)
#else
#define CHECK_SORTED(cmp,a,n) \
do { \
  int i; \
  for (i = 0; i < (n) - 1; i++) \
    assert ((cmp) (ps, (a)[i], (a)[i + 1]) <= 0); \
} while(0)
#endif

#define SORT(T,cmp,a,n) \
do { \
  T * aa = (a); \
  int nn = (n); \
  QUICKSORT (T, cmp, aa, nn); \
  INSERTION_SORT (T, cmp, aa, nn); \
  assert (ps->ihead == ps->indices); \
  CHECK_SORTED (cmp, aa, nn); \
} while (0)

#define WRDSZ (sizeof (long) * 8)

#ifdef RCODE
#define fprintf(...) do { } while (0)
#define vfprintf(...) do { } while (0)
#define fputs(...) do { } while (0)
#define fputc(...) do { } while (0)
#endif

typedef unsigned Flt;		/* 32 bit deterministic soft float */
typedef Flt Act;		/* clause and variable activity */
typedef struct Blk Blk;		/* allocated memory block */
typedef struct Cls Cls;		/* clause */
typedef struct Lit Lit;		/* literal */
typedef struct Rnk Rnk;		/* variable to score mapping */
typedef signed char Val;	/* TRUE, UNDEF, FALSE */
typedef struct Var Var;		/* variable */
#ifdef TRACE
typedef struct Trd Trd;		/* trace data for clauses */
typedef struct Zhn Zhn;		/* compressed chain (=zain) data */
typedef unsigned char Znt;	/* compressed antecedent data */
#endif

#ifdef NO_BINARY_CLAUSES
typedef struct Ltk Ltk;

struct Ltk
{
  Lit ** start;
  unsigned count : WRDSZ == 32 ? 27 : 32;
  unsigned ldsize : WRDSZ == 32 ? 5 : 32;
};
#endif

struct Lit
{
  Val val;
};

struct Var
{
  unsigned mark		: 1;	/*bit 1*/
  unsigned resolved	: 1;	/*bit 2*/
  unsigned phase	: 1;	/*bit 3*/
  unsigned assigned	: 1;	/*bit 4*/
  unsigned used		: 1;	/*bit 5*/
  unsigned failed	: 1;	/*bit 6*/
  unsigned internal	: 1;	/*bit 7*/
  unsigned usedefphase  : 1;    /*bit 8*/
  unsigned defphase     : 1;    /*bit 9*/
  unsigned msspos       : 1;    /*bit 10*/
  unsigned mssneg       : 1;    /*bit 11*/
  unsigned humuspos     : 1;    /*bit 12*/
  unsigned humusneg     : 1;    /*bit 13*/
  unsigned partial      : 1;    /*bit 14*/
#ifdef TRACE
  unsigned core		: 1;	/*bit 15*/
#endif
  unsigned level;
  Cls *reason;
#ifndef NADC
  Lit ** inado;
  Lit ** ado;
  Lit *** adotabpos;
#endif
};

struct Rnk
{
  Act score;
  unsigned pos : 30;			/* 0 iff not on heap */
  unsigned moreimportant : 1;
  unsigned lessimportant : 1;
};

struct Cls
{
  unsigned size;

  unsigned collect:1;	/* bit 1 */
  unsigned learned:1;	/* bit 2 */
  unsigned locked:1;	/* bit 3 */
  unsigned used:1;	/* bit 4 */
#ifndef NDEBUG
  unsigned connected:1;	/* bit 5 */
#endif
#ifdef TRACE
  unsigned collected:1;	/* bit 6 */
  unsigned core:1;	/* bit 7 */
#endif

#define LDMAXGLUE 25	/* 32 - 7 */
#define MAXGLUE 	((1<<LDMAXGLUE)-1)

  unsigned glue:LDMAXGLUE;

  Cls *next[2];
  Lit *lits[2];
};

#ifdef TRACE
struct Zhn
{
  unsigned ref:31;
  unsigned core:1;
  Znt * liz;
  Znt znt[0];
};

struct Trd
{
  unsigned idx;
  Cls cls[0];
};
#endif

struct Blk
{
#ifndef NDEBUG
  union
  {
    size_t size;		/* this is what we really use */
    void *as_two_ptrs[2];	/* 2 * sizeof (void*) alignment of data */
  }
  header;
#endif
  char data[BLK_FILL_BYTES];
};

enum State
{
  RESET = 0,
  READY = 1,
  SAT = 2,
  UNSAT = 3,
  UNKNOWN = 4,
};


struct PicoSAT 
{
  enum State state;
  int last_sat_call_result;

  FILE *out;
  char * prefix;
  int verbosity;
  unsigned LEVEL;
  unsigned max_var;
  unsigned size_vars;

  Lit *lits;
  Var *vars;
  Rnk *rnks;
  Flt *jwh;
  Cls **htps;
#ifndef NDSC
  Cls **dhtps;
#endif
#ifdef NO_BINARY_CLAUSES
  Ltk *impls;
  Cls impl, cimpl;
  int implvalid, cimplvalid;
#else
  Cls **impls;
#endif
  Lit **trail, **thead, **eot, **ttail, ** ttail2;
#ifndef NADC
  Lit **ttailado;
#endif
  unsigned adecidelevel;
  Lit **als, **alshead, **alstail, **eoals;
  Lit **CLS, **clshead, **eocls;
  int *rils, *rilshead, *eorils;
  int *cils, *cilshead, *eocils;
  int *fals, *falshead, *eofals;
  int *mass, szmass;
  int *mssass, szmssass;
  int *mcsass, nmcsass, szmcsass;
  int *humus, szhumus;
  Lit *failed_assumption;
  int extracted_all_failed_assumptions;
  Rnk **heap, **hhead, **eoh;
  Cls **oclauses, **ohead, **eoo;	/* original clauses */
  Cls **lclauses, **lhead, ** EOL;	/* learned clauses */
  int * soclauses, * sohead, * eoso; /* saved original clauses */
  int saveorig;
  int partial;
#ifdef TRACE
  int trace;
  Zhn **zhains, **zhead, **eoz;
  int ocore;
#endif
  int rupstarted;
  int rupvariables;
  int rupclauses;
  Cls *mtcls;
  Cls *conflict;
  Lit **added, **ahead, **eoa;
  Var **marked, **mhead, **eom;
  Var **dfs, **dhead, **eod;
  Cls **resolved, **rhead, **eor;
  unsigned char *levels, *levelshead, *eolevels;
  unsigned *dused, *dusedhead, *eodused;
  unsigned char *buffer, *bhead, *eob;
  Act vinc, lscore, ilvinc, ifvinc;
#ifdef VISCORES
  Act fvinc, nvinc;
#endif
  Act cinc, lcinc, ilcinc, fcinc;
  unsigned srng;
  size_t current_bytes;
  size_t max_bytes;
  size_t recycled;
  double seconds, flseconds;
  double entered;
  unsigned nentered;
  int measurealltimeinlib;
  char *rline[2];
  int szrline, RCOUNT;
  double levelsum;
  unsigned iterations;
  int reports;
  int lastrheader;
  unsigned calls;
  unsigned decisions;
  unsigned restarts;
  unsigned simps;
  unsigned fsimplify;
  unsigned isimplify;
  unsigned reductions;
  unsigned lreduce;
  unsigned lreduceadjustcnt;
  unsigned lreduceadjustinc;
  unsigned lastreduceconflicts;
  unsigned llocked;	/* locked large learned clauses */
  unsigned lrestart;
#ifdef NLUBY
  unsigned drestart;
  unsigned ddrestart;
#else
  unsigned lubycnt;
  unsigned lubymaxdelta;
  int waslubymaxdelta;
#endif
  unsigned long long lsimplify;
  unsigned long long propagations;
  unsigned long long lpropagations;
  unsigned fixed;		/* top level assignments */
#ifndef NFL
  unsigned failedlits;
  unsigned ifailedlits;
  unsigned efailedlits;
  unsigned flcalls;
#ifdef STATS
  unsigned flrounds;
  unsigned long long flprops;
  unsigned long long floopsed, fltried, flskipped;
#endif
  unsigned long long fllimit;
  int simplifying;
  Lit ** saved;
  unsigned saved_size;
#endif
  unsigned conflicts;
  unsigned contexts;
  unsigned internals;
  unsigned noclauses;	/* current number large original clauses */
  unsigned nlclauses;	/* current number large learned clauses */
  unsigned olits;		/* current literals in large original clauses */
  unsigned llits;		/* current literals in large learned clauses */
  unsigned oadded;		/* added original clauses */
  unsigned ladded;		/* added learned clauses */
  unsigned loadded;	/* added original large clauses */
  unsigned lladded;	/* added learned large clauses */
  unsigned addedclauses;	/* oadded + ladded */
  unsigned vused;		/* used variables */
  unsigned llitsadded;	/* added learned literals */
  unsigned long long visits;
#ifdef STATS
  unsigned loused;		/* used large original clauses */
  unsigned llused;		/* used large learned clauses */
  unsigned long long bvisits;
  unsigned long long tvisits;
  unsigned long long lvisits;
  unsigned long long othertrue;
  unsigned long long othertrue2;
  unsigned long long othertruel;
  unsigned long long othertrue2u;
  unsigned long long othertruelu;
  unsigned long long ltraversals;
  unsigned long long traversals;
#ifdef TRACE
  unsigned long long antecedents;
#endif
  unsigned uips;
  unsigned znts;
  unsigned assumptions;
  unsigned rdecisions;
  unsigned sdecisions;
  size_t srecycled;
  size_t rrecycled;
  unsigned long long derefs;
#endif
  unsigned minimizedllits;
  unsigned nonminimizedllits;
#ifndef NADC
  Lit *** ados, *** hados, *** eados;
  Lit *** adotab;
  unsigned nadotab;
  unsigned szadotab;
  Cls * adoconflict;
  unsigned adoconflicts;
  unsigned adoconflictlimit;
  int addingtoado;
  int adodisabled;
#endif
  unsigned long long flips;
#ifdef STATS
  unsigned long long FORCED;
  unsigned long long assignments;
  unsigned inclreduces;
  unsigned staticphasedecisions;
  unsigned skippedrestarts;
#endif
  int * indices, * ihead, *eoi; 
  unsigned sdflips;

  unsigned long long saved_flips;
  unsigned saved_max_var;
  unsigned min_flipped;

  void * emgr;
  picosat_malloc enew;
  picosat_realloc eresize;
  picosat_free edelete;

  struct {
    void * state;
    int (*function) (void *);
  } interrupt;

#ifdef VISCORES
  FILE * fviscores;
#endif
};

typedef PicoSAT PS;

static Flt
packflt (unsigned m, int e)
{
  Flt res;
  assert (m < FLTMSB);
  assert (FLTMINEXPONENT <= e);
  assert (e <= FLTMAXEXPONENT);
  res = m | ((unsigned)(e + 128) << 24);
  return res;
}

static Flt
base2flt (unsigned m, int e)
{
  if (!m)
    return ZEROFLT;

  if (m < FLTMSB)
    {
      do
	{
	  if (e <= FLTMINEXPONENT)
	    return EPSFLT;

	  e--;
	  m <<= 1;

	}
      while (m < FLTMSB);
    }
  else
    {
      while (m >= FLTCARRY)
	{
	  if (e >= FLTMAXEXPONENT)
	    return INFFLT;

	  e++;
	  m >>= 1;
	}
    }

  m &= ~FLTMSB;
  return packflt (m, e);
}

static Flt
addflt (Flt a, Flt b)
{
  unsigned ma, mb, delta;
  int ea, eb;

  CMPSWAPFLT (a, b);
  if (!b)
    return a;

  UNPACKFLT (a, ma, ea);
  UNPACKFLT (b, mb, eb);

  assert (ea >= eb);
  delta = ea - eb;
  if (delta < 32) mb >>= delta; else mb = 0;
  if (!mb)
    return a;

  ma += mb;
  if (ma & FLTCARRY)
    {
      if (ea == FLTMAXEXPONENT)
	return INFFLT;

      ea++;
      ma >>= 1;
    }

  assert (ma < FLTCARRY);
  ma &= FLTMAXMANTISSA;

  return packflt (ma, ea);
}

static Flt
mulflt (Flt a, Flt b)
{
  unsigned ma, mb;
  unsigned long long accu;
  int ea, eb;

  CMPSWAPFLT (a, b);
  if (!b)
    return ZEROFLT;

  UNPACKFLT (a, ma, ea);
  UNPACKFLT (b, mb, eb);

  ea += eb;
  ea += 24;
  if (ea > FLTMAXEXPONENT)
    return INFFLT;

  if (ea < FLTMINEXPONENT)
    return EPSFLT;

  accu = ma;
  accu *= mb;
  accu >>= 24;

  if (accu >= FLTCARRY)
    {
      if (ea == FLTMAXEXPONENT)
	return INFFLT;

      ea++;
      accu >>= 1;

      if (accu >= FLTCARRY)
	return INFFLT;
    }

  assert (accu < FLTCARRY);
  assert (accu & FLTMSB);

  ma = accu;
  ma &= ~FLTMSB;

  return packflt (ma, ea);
}

static Flt
ascii2flt (const char *str)
{
  Flt ten = base2flt (10, 0);
  Flt onetenth = base2flt (26843546, -28);
  Flt res = ZEROFLT, tmp, base;
  const char *p = str;
  int ch;

  ch = *p++;

  if (ch != '.')
    {
      if (!isdigit (ch))
	return INFFLT;	/* better abort ? */

      res = base2flt (ch - '0', 0);

      while ((ch = *p++))
	{
	  if (ch == '.')
	    break;

	  if (!isdigit (ch))
	    return INFFLT;	/* better abort? */

	  res = mulflt (res, ten);
	  tmp = base2flt (ch - '0', 0);
	  res = addflt (res, tmp);
	}
    }

  if (ch == '.')
    {
      ch = *p++;
      if (!isdigit (ch))
	return INFFLT;	/* better abort ? */

      base = onetenth;
      tmp = mulflt (base2flt (ch - '0', 0), base);
      res = addflt (res, tmp);

      while ((ch = *p++))
	{
	  if (!isdigit (ch))
	    return INFFLT;	/* better abort? */

	  base = mulflt (base, onetenth);
	  tmp = mulflt (base2flt (ch - '0', 0), base);
	  res = addflt (res, tmp);
	}
    }

  return res;
}

#if defined(VISCORES)

static double
flt2double (Flt f)
{
  double res;
  unsigned m;
  int e, i;

  UNPACKFLT (f, m, e);
  res = m;

  if (e < 0)
    {
      for (i = e; i < 0; i++)
	res *= 0.5;
    }
  else
    {
      for (i = 0; i < e; i++)
	res *= 2.0;
    }

  return res;
}

#endif

static int
log2flt (Flt a)
{
  return FLTEXPONENT (a) + 24;
}

static int
cmpflt (Flt a, Flt b)
{
  if (a < b)
    return -1;

  if (a > b)
    return 1;

  return 0;
}

static void *
new (PS * ps, size_t size)
{
  size_t bytes;
  Blk *b;
  
  if (!size)
    return 0;

  bytes = size + SIZE_OF_BLK;

  if (ps->enew)
    b = ps->enew (ps->emgr, bytes);
  else
    b = malloc (bytes);

  ABORTIF (!b, "out of memory in 'new'");
#ifndef NDEBUG
  b->header.size = size;
#endif
  ps->current_bytes += size;
  if (ps->current_bytes > ps->max_bytes)
    ps->max_bytes = ps->current_bytes;
  return b->data;
}

static void
delete (PS * ps, void *void_ptr, size_t size)
{
  size_t bytes;
  Blk *b;

  if (!void_ptr)
    {
      assert (!size);
      return;
    }

  assert (size);
  b = PTR2BLK (void_ptr);

  assert (size <= ps->current_bytes);
  ps->current_bytes -= size;

  assert (b->header.size == size);

  bytes = size + SIZE_OF_BLK;
  if (ps->edelete)
    ps->edelete (ps->emgr, b, bytes);
  else
    free (b);
}

static void *
resize (PS * ps, void *void_ptr, size_t old_size, size_t new_size)
{
  size_t old_bytes, new_bytes;
  Blk *b;

  b = PTR2BLK (void_ptr);

  assert (old_size <= ps->current_bytes);
  ps->current_bytes -= old_size;

  if ((old_bytes = old_size))
    {
      assert (old_size && b && b->header.size == old_size);
      old_bytes += SIZE_OF_BLK;
    }
  else
    assert (!b);

  if ((new_bytes = new_size))
    new_bytes += SIZE_OF_BLK;

  if (ps->eresize)
    b = ps->eresize (ps->emgr, b, old_bytes, new_bytes);
  else
    b = realloc (b, new_bytes);

  if (!new_size)
    {
      assert (!b);
      return 0;
    }

  ABORTIF (!b, "out of memory in 'resize'");
#ifndef NDEBUG
  b->header.size = new_size;
#endif

  ps->current_bytes += new_size;
  if (ps->current_bytes > ps->max_bytes)
    ps->max_bytes = ps->current_bytes;

  return b->data;
}

static unsigned
int2unsigned (int l)
{
  return (l < 0) ? 1 + 2 * -l : 2 * l;
}

static Lit *
int2lit (PS * ps, int l)
{
  return ps->lits + int2unsigned (l);
}

static Lit **
end_of_lits (Cls * c)
{
  return (Lit**)c->lits + c->size;
}

#if !defined(NDEBUG) || defined(LOGGING)

static void
dumplits (PS * ps, Lit ** l, Lit ** end)
{
  int first;
  Lit ** p;

  if (l == end)
    {
      /* empty clause */
    }
  else if (l + 1 == end)
    {
      fprintf (ps->out, "%d ", LIT2INT (l[0]));
    }
  else
    { 
      assert (l + 2 <= end);
      first = (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1])));
      fprintf (ps->out, "%d ", LIT2INT (l[first]));
      fprintf (ps->out, "%d ", LIT2INT (l[!first]));
      for (p = l + 2; p < end; p++)
	 fprintf (ps->out, "%d ", LIT2INT (*p));
    }

  fputc ('0', ps->out);
}

static void
dumpcls (PS * ps, Cls * c)
{
  Lit **end;

  if (c)
    {
      end = end_of_lits (c);
      dumplits (ps, c->lits, end);
#ifdef TRACE
      if (ps->trace)
	 fprintf (ps->out, " clause(%u)", CLS2IDX (c));
#endif
    }
  else
    fputs ("DECISION", ps->out);
}

static void
dumpclsnl (PS * ps, Cls * c)
{
  dumpcls (ps, c);
  fputc ('\n', ps->out);
}

void
dumpcnf (PS * ps)
{
  Cls **p, *c;

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;

      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif

      dumpclsnl (ps, *p);
    }
}

#endif

static void
delete_prefix (PS * ps)
{
  if (!ps->prefix)
    return;
    
  delete (ps, ps->prefix, strlen (ps->prefix) + 1);
  ps->prefix = 0;
}

static void
new_prefix (PS * ps, const char * str)
{
  delete_prefix (ps);
  assert (str);
  ps->prefix = new (ps, strlen (str) + 1);
  strcpy (ps->prefix, str);
}

static PS *
init (void * pmgr, 
      picosat_malloc pnew, picosat_realloc presize, picosat_free pdelete)
{
  PS * ps;

#if 0
  int count = 3 - !pnew - !presize - !pdelete;

  ABORTIF (count && !pnew, "API usage: missing 'picosat_set_new'");
  ABORTIF (count && !presize, "API usage: missing 'picosat_set_resize'");
  ABORTIF (count && !pdelete, "API usage: missing 'picosat_set_delete'");
#endif

  ps = pnew ? pnew (pmgr, sizeof *ps) : malloc (sizeof *ps);
  ABORTIF (!ps, "failed to allocate memory for PicoSAT manager");
  memset (ps, 0, sizeof *ps);

  ps->emgr = pmgr;
  ps->enew = pnew;
  ps->eresize = presize;
  ps->edelete = pdelete;

  ps->size_vars = 1;
  ps->state = RESET;
#ifdef TRACE
  ps->ocore = -1;
#endif
  ps->lastrheader = -2;
#ifndef NADC
  ps->adoconflictlimit = UINT_MAX;
#endif
  ps->min_flipped = UINT_MAX;

  NEWN (ps->lits, 2 * ps->size_vars);
  NEWN (ps->jwh, 2 * ps->size_vars);
  NEWN (ps->htps, 2 * ps->size_vars);
#ifndef NDSC
  NEWN (ps->dhtps, 2 * ps->size_vars);
#endif
  NEWN (ps->impls, 2 * ps->size_vars);
  NEWN (ps->vars, ps->size_vars);
  NEWN (ps->rnks, ps->size_vars);

  /* because '0' pos denotes not on heap
   */
  ENLARGE (ps->heap, ps->hhead, ps->eoh); 
  ps->hhead = ps->heap + 1;

  ps->vinc = base2flt (1, 0);		/* initial var activity */
  ps->ifvinc = ascii2flt ("1.05");	/* var score rescore factor */
#ifdef VISCORES
  ps->fvinc = ascii2flt ("0.9523809");	/*     1/f =     1/1.05 */
  ps->nvinc = ascii2flt ("0.0476191");	/* 1 - 1/f = 1 - 1/1.05 */
#endif
  ps->lscore = base2flt (1, 90);	/* var activity rescore limit */
  ps->ilvinc = base2flt (1, -90);	/* inverse of 'lscore' */

  ps->cinc = base2flt (1, 0);		/* initial clause activity */
  ps->fcinc = ascii2flt ("1.001");	/* cls activity rescore factor */
  ps->lcinc = base2flt (1, 90);		/* cls activity rescore limit */
  ps->ilcinc = base2flt (1, -90);	/* inverse of 'ilcinc' */

  ps->lreduceadjustcnt = ps->lreduceadjustinc = 100;
  ps->lpropagations = ~0ull;

#ifndef RCODE
  ps->out = stdout;
#else
  ps->out = 0;
#endif
  new_prefix (ps, "c ");
  ps->verbosity = 0;

#ifdef NO_BINARY_CLAUSES
  memset (&ps->impl, 0, sizeof (ps->impl));
  ps->impl.size = 2;

  memset (&ps->cimpl, 0, sizeof (ps->impl));
  ps->cimpl.size = 2;
#endif

#ifdef VISCORES
  ps->fviscores = popen (
    "/usr/bin/gnuplot -background black"
    " -xrm 'gnuplot*textColor:white'"
    " -xrm 'gnuplot*borderColor:white'"
    " -xrm 'gnuplot*axisColor:white'"
    , "w");
  fprintf (ps->fviscores, "unset key\n");
  // fprintf (ps->fviscores, "set log y\n");
  fflush (ps->fviscores);
  system ("rm -rf /tmp/picosat-viscores");
  system ("mkdir /tmp/picosat-viscores");
  system ("mkdir /tmp/picosat-viscores/data");
#ifdef WRITEGIF
  system ("mkdir /tmp/picosat-viscores/gif");
  fprintf (ps->fviscores,
           "set terminal gif giant animate opt size 1024,768 x000000 xffffff"
	   "\n");

  fprintf (ps->fviscores, 
           "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n");
#endif
#endif
  ps->state = READY;
  ps->last_sat_call_result = 0;

  return ps;
}

static size_t
bytes_clause (PS * ps, unsigned size, unsigned learned)
{
  size_t res;

  res = sizeof (Cls);
  res += size * sizeof (Lit *);
  res -= 2 * sizeof (Lit *);

  if (learned && size > 2)
    res += sizeof (Act);	/* add activity */

#ifdef TRACE
  if (ps->trace)
    res += sizeof (Trd);	/* add trace data */
#else
  (void) ps;
#endif

  return res;
}

static Cls *
new_clause (PS * ps, unsigned size, unsigned learned)
{
  size_t bytes;
  void * tmp;
#ifdef TRACE
  Trd *trd;
#endif
  Cls *res;

  bytes = bytes_clause (ps, size, learned);
  tmp = new (ps, bytes);

#ifdef TRACE
  if (ps->trace)
    {
      trd = tmp;

      if (learned)
	trd->idx = LIDX2IDX (ps->lhead - ps->lclauses);
      else
	trd->idx = OIDX2IDX (ps->ohead - ps->oclauses);

      res = trd->cls;
    }
  else
#endif
    res = tmp;

  res->size = size;
  res->learned = learned;

  res->collect = 0;
#ifndef NDEBUG
  res->connected = 0;
#endif
  res->locked = 0;
  res->used = 0;
#ifdef TRACE
  res->core = 0;
  res->collected = 0;
#endif

  if (learned && size > 2)
    {
      Act * p = CLS2ACT (res);
      *p = ps->cinc;
    }

  return res;
}

static void
delete_clause (PS * ps, Cls * c)
{
  size_t bytes;
#ifdef TRACE
  Trd *trd;
#endif

  bytes = bytes_clause (ps, c->size, c->learned);

#ifdef TRACE
  if (ps->trace)
    {
      trd = CLS2TRD (c);
      delete (ps, trd, bytes);
    }
  else
#endif
    delete (ps, c, bytes);
}

static void
delete_clauses (PS * ps)
{
  Cls **p;
  for (p = SOC; p != EOC; p = NXC (p))
    if (*p)
      delete_clause (ps, *p);

  DELETEN (ps->oclauses, ps->eoo - ps->oclauses);
  DELETEN (ps->lclauses, ps->EOL - ps->lclauses);

  ps->ohead = ps->eoo = ps->lhead = ps->EOL = 0;
}

#ifdef TRACE

static void
delete_zhain (PS * ps, Zhn * zhain)
{
  const Znt *p, *znt;

  assert (zhain);

  znt = zhain->znt;
  for (p = znt; *p; p++)
    ;

  delete (ps, zhain, sizeof (Zhn) + (p - znt) + 1);
}

static void
delete_zhains (PS * ps)
{
  Zhn **p, *z;
  for (p = ps->zhains; p < ps->zhead; p++)
    if ((z = *p))
      delete_zhain (ps, z);

  DELETEN (ps->zhains, ps->eoz - ps->zhains);
  ps->eoz = ps->zhead = 0;
}

#endif

#ifdef NO_BINARY_CLAUSES
static void
lrelease (PS * ps, Ltk * stk)
{
  if (stk->start)
    DELETEN (stk->start, (1 << (stk->ldsize)));
  memset (stk, 0, sizeof (*stk));
}
#endif

#ifndef NADC

static unsigned
llength (Lit ** a)
{
  Lit ** p;
  for (p = a; *p; p++)
    ;
  return p - a;
}

static void
resetadoconflict (PS * ps)
{
  assert (ps->adoconflict);
  delete_clause (ps, ps->adoconflict);
  ps->adoconflict = 0;
}

static void
reset_ados (PS * ps)
{
  Lit *** p;

  for (p = ps->ados; p < ps->hados; p++)
    DELETEN (*p, llength (*p) + 1);

  DELETEN (ps->ados, ps->eados - ps->ados);
  ps->hados = ps->eados = 0;

  DELETEN (ps->adotab, ps->szadotab);
  ps->szadotab = ps->nadotab = 0;

  if (ps->adoconflict)
    resetadoconflict (ps);

  ps->adoconflicts = 0;
  ps->adoconflictlimit = UINT_MAX;
  ps->adodisabled = 0;
}

#endif

static void
reset (PS * ps)
{
  ABORTIF (!ps || 
           ps->state == RESET, "API usage: reset without initialization");

  delete_clauses (ps);
#ifdef TRACE
  delete_zhains (ps);
#endif
#ifdef NO_BINARY_CLAUSES
  {
    unsigned i;
    for (i = 2; i <= 2 * ps->max_var + 1; i++)
      lrelease (ps, ps->impls + i);
  }
#endif
#ifndef NADC
  reset_ados (ps);
#endif
#ifndef NFL
  DELETEN (ps->saved, ps->saved_size);
#endif
  DELETEN (ps->htps, 2 * ps->size_vars);
#ifndef NDSC
  DELETEN (ps->dhtps, 2 * ps->size_vars);
#endif
  DELETEN (ps->impls, 2 * ps->size_vars);
  DELETEN (ps->lits, 2 * ps->size_vars);
  DELETEN (ps->jwh, 2 * ps->size_vars);
  DELETEN (ps->vars, ps->size_vars);
  DELETEN (ps->rnks, ps->size_vars);
  DELETEN (ps->trail, ps->eot - ps->trail);
  DELETEN (ps->heap, ps->eoh - ps->heap);
  DELETEN (ps->als, ps->eoals - ps->als);
  DELETEN (ps->CLS, ps->eocls - ps->CLS);
  DELETEN (ps->rils, ps->eorils - ps->rils);
  DELETEN (ps->cils, ps->eocils - ps->cils);
  DELETEN (ps->fals, ps->eofals - ps->fals);
  DELETEN (ps->mass, ps->szmass);
  DELETEN (ps->mssass, ps->szmssass);
  DELETEN (ps->mcsass, ps->szmcsass);
  DELETEN (ps->humus, ps->szhumus);
  DELETEN (ps->added, ps->eoa - ps->added);
  DELETEN (ps->marked, ps->eom - ps->marked);
  DELETEN (ps->dfs, ps->eod - ps->dfs);
  DELETEN (ps->resolved, ps->eor - ps->resolved);
  DELETEN (ps->levels, ps->eolevels - ps->levels);
  DELETEN (ps->dused, ps->eodused - ps->dused);
  DELETEN (ps->buffer, ps->eob - ps->buffer);
  DELETEN (ps->indices, ps->eoi - ps->indices);
  DELETEN (ps->soclauses, ps->eoso - ps->soclauses);
  delete_prefix (ps);
  delete (ps, ps->rline[0], ps->szrline);
  delete (ps, ps->rline[1], ps->szrline);
  assert (getenv ("LEAK") || !ps->current_bytes);	/* found leak if failing */
#ifdef VISCORES
  pclose (ps->fviscores);
#endif
  if (ps->edelete)
    ps->edelete (ps->emgr, ps, sizeof *ps);
  else
    free (ps);
}

inline static void
tpush (PS * ps, Lit * lit)
{
  assert (ps->lits < lit && lit <= ps->lits + 2* ps->max_var + 1);
  if (ps->thead == ps->eot)
    {
      unsigned ttail2count = ps->ttail2 - ps->trail;
      unsigned ttailcount = ps->ttail - ps->trail;
#ifndef NADC
      unsigned ttailadocount = ps->ttailado - ps->trail;
#endif
      ENLARGE (ps->trail, ps->thead, ps->eot);
      ps->ttail = ps->trail + ttailcount;
      ps->ttail2 = ps->trail + ttail2count;
#ifndef NADC
      ps->ttailado = ps->trail + ttailadocount;
#endif
    }

  *ps->thead++ = lit;
}

static void
assign_reason (PS * ps, Var * v, Cls * reason)
{
#if defined(NO_BINARY_CLAUSES) && !defined(NDEBUG)
  assert (reason != &ps->impl);
#else
  (void) ps;
#endif
  v->reason = reason;
}

static void
assign_phase (PS * ps, Lit * lit)
{
  unsigned new_phase, idx;
  Var * v = LIT2VAR (lit);

#ifndef NFL
  /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if
   * we force assignments on the top level.   The other assignments will be
   * undone and thus we can keep the old saved value of the phase.
   */
  if (!ps->LEVEL || !ps->simplifying)
#endif
    {
      new_phase = (LIT2SGN (lit) > 0);

      if (v->assigned)
	{
	  ps->sdflips -= ps->sdflips/FFLIPPED;

	  if (new_phase != v->phase)
	    {
	      assert (FFLIPPEDPREC >= FFLIPPED);
	      ps->sdflips += FFLIPPEDPREC / FFLIPPED;
	      ps->flips++;

	      idx = LIT2IDX (lit);
	      if (idx < ps->min_flipped)
		ps->min_flipped = idx;

              NOLOG (fprintf (ps->out, 
	                      "%sflipped %d\n",
			       ps->prefix, LIT2INT (lit)));
	    }
	}

      v->phase = new_phase;
      v->assigned = 1;
    }

  lit->val = TRUE;
  NOTLIT (lit)->val = FALSE;
}

inline static void
assign (PS * ps, Lit * lit, Cls * reason)
{
  Var * v = LIT2VAR (lit);
  assert (lit->val == UNDEF);
#ifdef STATS
  ps->assignments++;
#endif
  v->level = ps->LEVEL;
  assign_phase (ps, lit);
  assign_reason (ps, v, reason);
  tpush (ps, lit);
}

inline static int
cmp_added (PS * ps, Lit * k, Lit * l)
{
  Val a = k->val, b = l->val;
  Var *u, *v;
  int res;

  if (a == UNDEF && b != UNDEF)
    return -1;

  if (a != UNDEF && b == UNDEF)
    return 1;

  u = LIT2VAR (k);
  v = LIT2VAR (l);

  if (a != UNDEF)
    {
      assert (b != UNDEF);
      res = v->level - u->level;
      if (res)
	return res;		/* larger level first */
    }

  res = cmpflt (VAR2RNK (u)->score, VAR2RNK (v)->score);
  if (res)
    return res;			/* smaller activity first */

  return u - v;			/* smaller index first */
}

static void
sorttwolits (Lit ** v)
{
  Lit * a = v[0], * b = v[1];

  assert (a != b);

  if (a < b)
    return;

  v[0] = b;
  v[1] = a;
}

inline static void
sortlits (PS * ps, Lit ** v, unsigned size)
{
  if (size == 2)
    sorttwolits (v);	/* same order with and with out 'NO_BINARY_CLAUSES' */
  else
    SORT (Lit *, cmp_added, v, size);
}

#ifdef NO_BINARY_CLAUSES
static Cls *
setimpl (PS * ps, Lit * a, Lit * b)
{
  assert (!ps->implvalid);
  assert (ps->impl.size == 2);

  ps->impl.lits[0] = a;
  ps->impl.lits[1] = b;

  sorttwolits (ps->impl.lits);
  ps->implvalid = 1;

  return &ps->impl;
}

static void
resetimpl (PS * ps)
{
  ps->implvalid = 0;
}

static Cls *
setcimpl (PS * ps, Lit * a, Lit * b)
{
  assert (!ps->cimplvalid);
  assert (ps->cimpl.size == 2);

  ps->cimpl.lits[0] = a;
  ps->cimpl.lits[1] = b;

  sorttwolits (ps->cimpl.lits);
  ps->cimplvalid = 1;

  return &ps->cimpl;
}

static void
resetcimpl (PS * ps)
{
  assert (ps->cimplvalid);
  ps->cimplvalid = 0;
}

#endif

static int
cmp_ptr (PS * ps, void *l, void *k)
{
  (void) ps;
  return ((char*)l) - (char*)k;		/* arbitrarily already reverse */
}

static int
cmp_rnk (Rnk * r, Rnk * s)
{
  if (!r->moreimportant && s->moreimportant)
    return -1;

  if (r->moreimportant && !s->moreimportant)
    return 1;

  if (!r->lessimportant && s->lessimportant)
    return 1;

  if (r->lessimportant && !s->lessimportant)
    return -1;

  if (r->score < s->score)
    return -1;

  if (r->score > s->score)
    return 1;

  return -cmp_ptr (0, r, s);
}

static void
hup (PS * ps, Rnk * v)
{
  int upos, vpos;
  Rnk *u;

#ifndef NFL
  assert (!ps->simplifying);
#endif

  vpos = v->pos;

  assert (0 < vpos);
  assert (vpos < ps->hhead - ps->heap);
  assert (ps->heap[vpos] == v);

  while (vpos > 1)
    {
      upos = vpos / 2;

      u = ps->heap[upos];

      if (cmp_rnk (u, v) > 0)
	break;

      ps->heap[vpos] = u;
      u->pos = vpos;

      vpos = upos;
    }

  ps->heap[vpos] = v;
  v->pos = vpos;
}

static Cls *add_simplified_clause (PS *, int);

inline static void
add_antecedent (PS * ps, Cls * c)
{
  assert (c);

#ifdef NO_BINARY_CLAUSES
  if (ISLITREASON (c))
    return;

  if (c == &ps->impl)
    return;
#elif defined(STATS) && defined(TRACE)
  ps->antecedents++;
#endif
  if (ps->rhead == ps->eor)
    ENLARGE (ps->resolved, ps->rhead, ps->eor);

  assert (ps->rhead < ps->eor);
  *ps->rhead++ = c;
}

#ifdef TRACE

#ifdef NO_BINARY_CLAUSES
#error "can not combine TRACE and NO_BINARY_CLAUSES"
#endif

#endif /* TRACE */

static void
add_lit (PS * ps, Lit * lit)
{
  assert (lit);

  if (ps->ahead == ps->eoa)
    ENLARGE (ps->added, ps->ahead, ps->eoa);

  *ps->ahead++ = lit;
}

static void
push_var_as_marked (PS * ps, Var * v)
{
  if (ps->mhead == ps->eom)
    ENLARGE (ps->marked, ps->mhead, ps->eom);

  *ps->mhead++ = v;
}

static void
mark_var (PS * ps, Var * v)
{
  assert (!v->mark);
  v->mark = 1;
  push_var_as_marked (ps, v);
}

#ifdef NO_BINARY_CLAUSES

static Cls *
impl2reason (PS * ps, Lit * lit)
{
  Lit * other;
  Cls * res;
  other = ps->impl.lits[0];
  if (lit == other)
    other = ps->impl.lits[1];
  assert (other->val == FALSE);
  res = LIT2REASON (NOTLIT (other));
  resetimpl (ps);
  return res;
}

#endif

/* Whenever we have a top level derived unit we really should derive a unit
 * clause otherwise the resolutions in 'add_simplified_clause' become
 * incorrect.
 */
static Cls *
resolve_top_level_unit (PS * ps, Lit * lit, Cls * reason)
{
  unsigned count_resolved;
  Lit **p, **eol, *other;
  Var *u, *v;

  assert (ps->rhead == ps->resolved);
  assert (ps->ahead == ps->added);

  add_lit (ps, lit);
  add_antecedent (ps, reason);
  count_resolved = 1;
  v = LIT2VAR (lit);

  eol = end_of_lits (reason);
  for (p = reason->lits; p < eol; p++)
    {
      other = *p;
      u = LIT2VAR (other);
      if (u == v)
	continue;

      add_antecedent (ps, u->reason);
      count_resolved++;
    }

  /* Some of the literals could be assumptions.  If at least one
   * variable is not an assumption, we should resolve.
   */
  if (count_resolved >= 2)
    {
#ifdef NO_BINARY_CLAUSES
      if (reason == &ps->impl)
	resetimpl (ps);
#endif
      reason = add_simplified_clause (ps, 1);
#ifdef NO_BINARY_CLAUSES
      if (reason->size == 2)
	{
	  assert (reason == &ps->impl);
	  reason = impl2reason (ps, lit);
	}
#endif
      assign_reason (ps, v, reason);
    }
  else
    {
      ps->ahead = ps->added;
      ps->rhead = ps->resolved;
    }

  return reason;
}

static void
fixvar (PS * ps, Var * v)
{
  Rnk * r;

  assert (VAR2LIT (v) != UNDEF);
  assert (!v->level);

  ps->fixed++;

  r = VAR2RNK (v);
  r->score = INFFLT;

#ifndef NFL
  if (ps->simplifying)
    return;
#endif

  if (!r->pos)
    return;

  hup (ps, r);
}

static void
use_var (PS * ps, Var * v)
{
  if (v->used)
    return;

  v->used = 1;
  ps->vused++;
}

static void
assign_forced (PS * ps, Lit * lit, Cls * reason)
{
  Var *v;

  assert (reason);
  assert (lit->val == UNDEF);

#ifdef STATS
  ps->FORCED++;
#endif
  assign (ps, lit, reason);

#ifdef NO_BINARY_CLAUSES
  assert (reason != &ps->impl);
  if (ISLITREASON (reason)) 
    {
      reason = setimpl (ps, lit, NOTLIT (REASON2LIT (reason)));
      assert (reason);
    }
#endif
  LOG ( fprintf (ps->out,
                "%sassign %d at level %d by ",
                ps->prefix, LIT2INT (lit), ps->LEVEL);
       dumpclsnl (ps, reason));

  v = LIT2VAR (lit);
  if (!ps->LEVEL)
    use_var (ps, v);

  if (!ps->LEVEL && reason->size > 1)
    {
      reason = resolve_top_level_unit (ps, lit, reason);
      assert (reason);
    }

#ifdef NO_BINARY_CLAUSES
  if (ISLITREASON (reason) || reason == &ps->impl)
    {
      /* DO NOTHING */
    }
  else
#endif
    {
      assert (!reason->locked);
      reason->locked = 1;
      if (reason->learned && reason->size > 2)
	ps->llocked++;
    }

#ifdef NO_BINARY_CLAUSES
  if (reason == &ps->impl)
    resetimpl (ps);
#endif

  if (!ps->LEVEL)
    fixvar (ps, v);
}

#ifdef NO_BINARY_CLAUSES

static void
lpush (PS * ps, Lit * lit, Cls * c)
{
  int pos = (c->lits[0] == lit);
  Ltk * s = LIT2IMPLS (lit);
  unsigned oldsize, newsize;

  assert (c->size == 2);

  if (!s->start)
    {
      assert (!s->count);
      assert (!s->ldsize);
      NEWN (s->start, 1);
    }
  else 
    {
      oldsize = (1 << (s->ldsize));
      assert (s->count <= oldsize);
      if (s->count == oldsize)
	{
	  newsize = 2 * oldsize;
	  RESIZEN (s->start, oldsize, newsize);
	  s->ldsize++;
	}
    }

  s->start[s->count++] = c->lits[pos];
}

#endif

static void
connect_head_tail (PS * ps, Lit * lit, Cls * c)
{
  Cls ** s;
  assert (c->size >= 1);
  if (c->size == 2)
    {
#ifdef NO_BINARY_CLAUSES
      lpush (ps, lit, c);
      return;
#else
      s = LIT2IMPLS (lit);
#endif
    }
  else
    s = LIT2HTPS (lit);

  if (c->lits[0] != lit)
    {
      assert (c->size >= 2);
      assert (c->lits[1] == lit);
      c->next[1] = *s;
    }
  else
    c->next[0] = *s;

  *s = c;
}

#ifdef TRACE
static void
zpush (PS * ps, Zhn * zhain)
{
  assert (ps->trace);

  if (ps->zhead == ps->eoz)
    ENLARGE (ps->zhains, ps->zhead, ps->eoz);

  *ps->zhead++ = zhain;
}

static int
cmp_resolved (PS * ps, Cls * c, Cls * d)
{
#ifndef NDEBUG
  assert (ps->trace);
#else
  (void) ps;
#endif
  return CLS2IDX (c) - CLS2IDX (d);
}

static void
bpushc (PS * ps, unsigned char ch)
{
  if (ps->bhead == ps->eob)
    ENLARGE (ps->buffer, ps->bhead, ps->eob);

  *ps->bhead++ = ch;
}

static void
bpushu (PS * ps, unsigned u)
{
  while (u & ~0x7f)
    {
      bpushc (ps, u | 0x80);
      u >>= 7;
    }

  bpushc (ps, u);
}

static void
bpushd (PS * ps, unsigned prev, unsigned this)
{
  unsigned delta;
  assert (prev < this);
  delta = this - prev;
  bpushu (ps, delta);
}

static void
add_zhain (PS * ps)
{
  unsigned prev, this, count, rcount;
  Cls **p, *c;
  Zhn *res;

  assert (ps->trace);
  assert (ps->bhead == ps->buffer);
  assert (ps->rhead > ps->resolved);

  rcount = ps->rhead - ps->resolved;
  SORT (Cls *, cmp_resolved, ps->resolved, rcount);

  prev = 0;
  for (p = ps->resolved; p < ps->rhead; p++)
    {
      c = *p;
      this = CLS2TRD (c)->idx;
      bpushd (ps, prev, this);
      prev = this;
    }
  bpushc (ps, 0);

  count = ps->bhead - ps->buffer;

  res = new (ps, sizeof (Zhn) + count);
  res->core = 0;
  res->ref = 0;
  memcpy (res->znt, ps->buffer, count);

  ps->bhead = ps->buffer;
#ifdef STATS
  ps->znts += count - 1;
#endif
  zpush (ps, res);
}

#endif

static void
add_resolved (PS * ps, int learned)
{
#if defined(STATS) || defined(TRACE)
  Cls **p, *c;

  for (p = ps->resolved; p < ps->rhead; p++)
    {
      c = *p;
      if (c->used)
	continue;

      c->used = 1;

      if (c->size <= 2)
	continue;

#ifdef STATS
      if (c->learned)
	ps->llused++;
      else
	ps->loused++;
#endif
    }
#endif

#ifdef TRACE
  if (learned && ps->trace)
    add_zhain (ps);
#else
  (void) learned;
#endif
  ps->rhead = ps->resolved;
}

static void
incjwh (PS * ps, Cls * c)
{
  Lit **p, *lit, ** eol;
  Flt * f, inc, sum;
  unsigned size = 0;
  Var * v;
  Val val;

  eol = end_of_lits (c);

  for (p = c->lits; p < eol; p++)
    {
      lit = *p;
      val = lit->val;

      if (val && ps->LEVEL > 0)
	{
	  v = LIT2VAR (lit);
	  if (v->level > 0)
	    val = UNDEF;
	}

      if (val == TRUE)
	return;

      if (val != FALSE)
	size++;
    }

  inc = base2flt (1, -size);

  for (p = c->lits; p < eol; p++)
    {
      lit = *p;
      f = LIT2JWH (lit);
      sum = addflt (*f, inc);
      *f = sum;
    }
}

static void
write_rup_header (PS * ps, FILE * file)
{
  char line[80];
  int i;

  sprintf (line, "%%RUPD32 %u %u", ps->rupvariables, ps->rupclauses);

  fputs (line, file);
  for (i = 255 - strlen (line); i >= 0; i--)
    fputc (' ', file);

  fputc ('\n', file);
  fflush (file);
}

static Cls *
add_simplified_clause (PS * ps, int learned)
{
  unsigned num_true, num_undef, num_false, size, count_resolved;
  Lit **p, **q, *lit, ** end;
  unsigned litlevel, glue;
  Cls *res, * reason;
  int reentered;
  Val val;
  Var *v;
#if !defined(NDEBUG) && defined(TRACE)
  unsigned idx;
#endif

  reentered = 0;

REENTER:

  size = ps->ahead - ps->added;

  add_resolved (ps, learned);

  if (learned)
    {
      ps->ladded++;
      ps->llitsadded += size;
      if (size > 2)
	{
	  ps->lladded++;
	  ps->nlclauses++;
	  ps->llits += size;
	}
    }
  else
    {
      ps->oadded++;
      if (size > 2)
	{
	  ps->loadded++;
	  ps->noclauses++;
	  ps->olits += size;
	}
    }

  ps->addedclauses++;
  assert (ps->addedclauses == ps->ladded + ps->oadded);

#ifdef NO_BINARY_CLAUSES
  if (size == 2)
    res = setimpl (ps, ps->added[0], ps->added[1]);
  else
#endif
    {
      sortlits (ps, ps->added, size); 

      if (learned)
	{
	  if (ps->lhead == ps->EOL)
	    {
	      ENLARGE (ps->lclauses, ps->lhead, ps->EOL);

	      /* A very difficult to find bug, which only occurs if the
	       * learned clauses stack is immediately allocated before the
	       * original clauses stack without padding.  In this case, we
	       * have 'SOC == EOC', which terminates all loops using the
	       * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately.
	       * Unfortunately this occurred in 'fix_clause_lits' after
	       * using a recent version of the memory allocator of 'Google'
	       * perftools in the context of one large benchmark for 
	       * our SMT solver 'Boolector'.
	       */
	      if (ps->EOL == ps->oclauses)
		ENLARGE (ps->lclauses, ps->lhead, ps->EOL);
	    }

#if !defined(NDEBUG) && defined(TRACE)
	  idx = LIDX2IDX (ps->lhead - ps->lclauses);
#endif
	}
      else
	{
	  if (ps->ohead == ps->eoo)
	    {
	      ENLARGE (ps->oclauses, ps->ohead, ps->eoo);
	      if (ps->EOL == ps->oclauses)
		ENLARGE (ps->oclauses, ps->ohead, ps->eoo);	/* ditto */
	    }

#if !defined(NDEBUG) && defined(TRACE)
	  idx = OIDX2IDX (ps->ohead - ps->oclauses);
#endif
	}

      assert (ps->EOL != ps->oclauses);			/* ditto */

      res = new_clause (ps, size, learned);

      glue = 0;

      if (learned)
	{
	  assert (ps->dusedhead == ps->dused);

	  for (p = ps->added; p < ps->ahead; p++) 
	    {
	      lit = *p;
	      if (lit->val)
		{
		  litlevel = LIT2VAR (lit)->level;
		  assert (litlevel <= ps->LEVEL);
		  while (ps->levels + litlevel >= ps->levelshead)
		    {
		      if (ps->levelshead >= ps->eolevels)
			ENLARGE (ps->levels, ps->levelshead, ps->eolevels);
		      assert (ps->levelshead < ps->eolevels);
		      *ps->levelshead++ = 0;
		    }
		  if (!ps->levels[litlevel])
		    {
		      if (ps->dusedhead >= ps->eodused)
			ENLARGE (ps->dused, ps->dusedhead, ps->eodused);
		      assert (ps->dusedhead < ps->eodused);
		      *ps->dusedhead++ = litlevel;
		      ps->levels[litlevel] = 1;
		      glue++;
		    }
		}
	      else
		glue++;
	    }

	  while (ps->dusedhead > ps->dused) 
	    {
	      litlevel = *--ps->dusedhead;
	      assert (ps->levels + litlevel < ps->levelshead);
	      assert (ps->levels[litlevel]);
	      ps->levels[litlevel] = 0;
	    }
	}

      assert (glue <= MAXGLUE);
      res->glue = glue;

#if !defined(NDEBUG) && defined(TRACE)
      if (ps->trace)
	assert (CLS2IDX (res) == idx);
#endif
      if (learned)
	*ps->lhead++ = res;
      else
	*ps->ohead++ = res;

#if !defined(NDEBUG) && defined(TRACE)
      if (ps->trace && learned)
	assert (ps->zhead - ps->zhains == ps->lhead - ps->lclauses);
#endif
      assert (ps->lhead != ps->oclauses);		/* ditto */
    }

  if (learned && INCREMENTAL_RUP_FILE)
    {
      if (!ps->rupstarted)
	{
	  write_rup_header (ps, INCREMENTAL_RUP_FILE);
	  ps->rupstarted = 1;
	}
    }

  num_true = num_undef = num_false = 0;

  q = res->lits;
  for (p = ps->added; p < ps->ahead; p++)
    {
      lit = *p;
      *q++ = lit;

      if (learned && INCREMENTAL_RUP_FILE)
	fprintf (INCREMENTAL_RUP_FILE, "%d ", LIT2INT (lit));

      val = lit->val;

      num_true += (val == TRUE);
      num_undef += (val == UNDEF);
      num_false += (val == FALSE);
    }
  assert (num_false + num_true + num_undef == size);

  if (learned && INCREMENTAL_RUP_FILE)
    fputs ("0\n", INCREMENTAL_RUP_FILE);

  ps->ahead = ps->added;		/* reset */

  if (!reentered)				// TODO merge
  if (size > 0)
    {
      assert (size <= 2 || !reentered);		// TODO remove
      connect_head_tail (ps, res->lits[0], res);
      if (size > 1)
	connect_head_tail (ps, res->lits[1], res);
    }

  if (size == 0)
    {
      if (!ps->mtcls)
	ps->mtcls = res;
    }

#ifdef NO_BINARY_CLAUSES
  if (size != 2)
#endif
#ifndef NDEBUG
    res->connected = 1;
#endif

  LOG ( fprintf (ps->out, "%s%s ", ps->prefix, learned ? "learned" : "original");
        dumpclsnl (ps, res));

  /* Shrink clause by resolving it against top level assignments.
   */
  if (!ps->LEVEL && num_false > 0)
    {
      assert (ps->ahead == ps->added);
      assert (ps->rhead == ps->resolved);

      count_resolved = 1;
      add_antecedent (ps, res);

      end = end_of_lits (res);
      for (p = res->lits; p < end; p++)
	{
	  lit = *p;
	  v = LIT2VAR (lit);
	  use_var (ps, v);

	  if (lit->val == FALSE)
	    {
	      add_antecedent (ps, v->reason);
	      count_resolved++;
	    }
	  else
	    add_lit (ps, lit);
	}

      assert (count_resolved >= 2);

      learned = 1;
#ifdef NO_BINARY_CLAUSES
      if (res == &ps->impl)
	resetimpl (ps);
#endif
      reentered = 1;
      goto REENTER;		/* and return simplified clause */
    }

  if (!num_true && num_undef == 1)	/* unit clause */
    {
      lit = 0;
      for (p = res->lits; p < res->lits + size; p++)
	{
	  if ((*p)->val == UNDEF)
	    lit = *p;

	  v = LIT2VAR (*p);
	  use_var (ps, v);
	}
      assert (lit);

      reason = res;
#ifdef NO_BINARY_CLAUSES
      if (size == 2)
        {
	  Lit * other = res->lits[0];
	  if (other == lit)
	    other = res->lits[1];

	  assert (other->val == FALSE);
	  reason = LIT2REASON (NOTLIT (other));
	}
#endif
      assign_forced (ps, lit, reason);
      num_true++;
    }

  if (num_false == size && !ps->conflict)
    {
#ifdef NO_BINARY_CLAUSES
      if (res == &ps->impl)
	ps->conflict = setcimpl (ps, res->lits[0], res->lits[1]);
      else
#endif
      ps->conflict = res;
    }

  if (!learned && !num_true && num_undef)
    incjwh (ps, res);

#ifdef NO_BINARY_CLAUSES
  if (res == &ps->impl)
    resetimpl (ps);
#endif
  return res;
}

static int
trivial_clause (PS * ps)
{
  Lit **p, **q, *prev;
  Var *v;

  SORT (Lit *, cmp_ptr, ps->added,  ps->ahead - ps->added);

  prev = 0;
  q = ps->added;
  for (p = q; p < ps->ahead; p++)
    {
      Lit *this = *p;

      v = LIT2VAR (this);

      if (prev == this)		/* skip repeated literals */
	continue;

      /* Top level satisfied ? 
       */
      if (this->val == TRUE && !v->level)
	 return 1;

      if (prev == NOTLIT (this))/* found pair of dual literals */
	return 1;

      *q++ = prev = this;
    }

  ps->ahead = q;			/* shrink */

  return 0;
}

static void
simplify_and_add_original_clause (PS * ps)
{
#ifdef NO_BINARY_CLAUSES
  Cls * c;
#endif
  if (trivial_clause (ps))
    {
      ps->ahead = ps->added;

      if (ps->ohead == ps->eoo)
	ENLARGE (ps->oclauses, ps->ohead, ps->eoo);

      *ps->ohead++ = 0;

      ps->addedclauses++;
      ps->oadded++;
    }
  else
    {
      if (ps->CLS != ps->clshead)
	add_lit (ps, NOTLIT (ps->clshead[-1]));

#ifdef NO_BINARY_CLAUSES
      c = 
#endif
      add_simplified_clause (ps, 0);
#ifdef NO_BINARY_CLAUSES
      if (c == &ps->impl) assert (!ps->implvalid);
#endif
    }
}

#ifndef NADC

static void
add_ado (PS * ps)
{
  unsigned len = ps->ahead - ps->added;
  Lit ** ado, ** p, ** q, *lit;
  Var * v, * u;

#ifdef TRACE
  assert (!ps->trace);
#endif

  ABORTIF (ps->ados < ps->hados && llength (ps->ados[0]) != len,
           "internal: non matching all different constraint object lengths");

  if (ps->hados == ps->eados)
    ENLARGE (ps->ados, ps->hados, ps->eados);

  NEWN (ado, len + 1);
  *ps->hados++ = ado;

  p = ps->added;
  q = ado;
  u = 0;
  while (p < ps->ahead)
    {
      lit = *p++;
      v = LIT2VAR (lit);
      ABORTIF (v->inado, 
               "internal: variable in multiple all different objects");
      v->inado = ado;
      if (!u && !lit->val)
	u = v;
      *q++ = lit;
    }

  assert (q == ado + len);
  *q++ = 0;

  /* TODO simply do a conflict test as in propado */

  ABORTIF (!u,
    "internal: "
    "adding fully instantiated all different object not implemented yet");

  assert (u);
  assert (u->inado == ado);
  assert (!u->ado);
  u->ado = ado;

  ps->ahead = ps->added;
}

#endif

static void
hdown (PS * ps, Rnk * r)
{
  unsigned end, rpos, cpos, opos;
  Rnk *child, *other;

  assert (r->pos > 0);
  assert (ps->heap[r->pos] == r);

  end = ps->hhead - ps->heap;
  rpos = r->pos;

  for (;;)
    {
      cpos = 2 * rpos;
      if (cpos >= end)
	break;

      opos = cpos + 1;
      child = ps->heap[cpos];

      if (cmp_rnk (r, child) < 0)
	{
	  if (opos < end)
	    {
	      other = ps->heap[opos];

	      if (cmp_rnk (child, other) < 0)
		{
		  child = other;
		  cpos = opos;
		}
	    }
	}
      else if (opos < end)
	{
	  child = ps->heap[opos];

	  if (cmp_rnk (r, child) >= 0)
	    break;

	  cpos = opos;
	}
      else
	break;

      ps->heap[rpos] = child;
      child->pos = rpos;
      rpos = cpos;
    }

  r->pos = rpos;
  ps->heap[rpos] = r;
}

static Rnk *
htop (PS * ps)
{
  assert (ps->hhead > ps->heap + 1);
  return ps->heap[1];
}

static Rnk *
hpop (PS * ps)
{
  Rnk *res, *last;
  unsigned end;

  assert (ps->hhead > ps->heap + 1);

  res = ps->heap[1];
  res->pos = 0;

  end = --ps->hhead - ps->heap;
  if (end == 1)
    return res;

  last = ps->heap[end];

  ps->heap[last->pos = 1] = last;
  hdown (ps, last);

  return res;
}

inline static void
hpush (PS * ps, Rnk * r)
{
  assert (!r->pos);

  if (ps->hhead == ps->eoh)
    ENLARGE (ps->heap, ps->hhead, ps->eoh);

  r->pos = ps->hhead++ - ps->heap;
  ps->heap[r->pos] = r;
  hup (ps, r);
}

static void
fix_trail_lits (PS * ps, long delta)
{
  Lit **p;
  for (p = ps->trail; p < ps->thead; p++)
    *p += delta;
}

#ifdef NO_BINARY_CLAUSES
static void
fix_impl_lits (PS * ps, long delta)
{
  Ltk * s;
  Lit ** p;

  for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++)
    for (p = s->start; p < s->start + s->count; p++)
      *p += delta;
}
#endif

static void
fix_clause_lits (PS * ps, long delta)
{
  Cls **p, *clause;
  Lit **q, *lit, **eol;

  for (p = SOC; p != EOC; p = NXC (p))
    {
      clause = *p;
      if (!clause)
	continue;

      q = clause->lits;
      eol = end_of_lits (clause);
      while (q < eol)
	{
	  assert (q - clause->lits <= (int) clause->size);
	  lit = *q;
	  lit += delta;
	  *q++ = lit;
	}
    }
}

static void
fix_added_lits (PS * ps, long delta)
{
  Lit **p;
  for (p = ps->added; p < ps->ahead; p++)
    *p += delta;
}

static void
fix_assumed_lits (PS * ps, long delta)
{
  Lit **p;
  for (p = ps->als; p < ps->alshead; p++)
    *p += delta;
}

static void
fix_cls_lits (PS * ps, long delta)
{
  Lit **p;
  for (p = ps->CLS; p < ps->clshead; p++)
    *p += delta;
}

static void
fix_heap_rnks (PS * ps, long delta)
{
  Rnk **p;

  for (p = ps->heap + 1; p < ps->hhead; p++)
    *p += delta;
}

#ifndef NADC

static void
fix_ado (long delta, Lit ** ado)
{
  Lit ** p;
  for (p = ado; *p; p++)
    *p += delta;
}

static void
fix_ados (PS * ps, long delta)
{
  Lit *** p;

  for (p = ps->ados; p < ps->hados; p++)
    fix_ado (delta, *p);
}

#endif

static void
enlarge (PS * ps, unsigned new_size_vars)
{
  long rnks_delta, lits_delta;
  Lit *old_lits = ps->lits;
  Rnk *old_rnks = ps->rnks;

  RESIZEN (ps->lits, 2 * ps->size_vars, 2 * new_size_vars);
  RESIZEN (ps->jwh, 2 * ps->size_vars, 2 * new_size_vars);
  RESIZEN (ps->htps, 2 * ps->size_vars, 2 * new_size_vars);
#ifndef NDSC
  RESIZEN (ps->dhtps, 2 * ps->size_vars, 2 * new_size_vars);
#endif
  RESIZEN (ps->impls, 2 * ps->size_vars, 2 * new_size_vars);
  RESIZEN (ps->vars, ps->size_vars, new_size_vars);
  RESIZEN (ps->rnks, ps->size_vars, new_size_vars);

  if ((lits_delta = ps->lits - old_lits))
    {
      fix_trail_lits (ps, lits_delta);
      fix_clause_lits (ps, lits_delta);
      fix_added_lits (ps, lits_delta);
      fix_assumed_lits (ps, lits_delta);
      fix_cls_lits (ps, lits_delta);
#ifdef NO_BINARY_CLAUSES
      fix_impl_lits (ps, lits_delta);
#endif
#ifndef NADC
      fix_ados (ps, lits_delta);
#endif
    }

  if ((rnks_delta = ps->rnks - old_rnks))
    {
      fix_heap_rnks (ps, rnks_delta);
    }

  assert (ps->mhead == ps->marked);

  ps->size_vars = new_size_vars;
}

static void
unassign (PS * ps, Lit * lit)
{
  Cls *reason;
  Var *v;
  Rnk *r;

  assert (lit->val == TRUE);

  LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit)));

  v = LIT2VAR (lit);
  reason = v->reason;

#ifdef NO_BINARY_CLAUSES
  assert (reason != &ps->impl);
  if (ISLITREASON (reason))
    {
      /* DO NOTHING */
    }
  else
#endif
  if (reason)
    {
      assert (reason->locked);
      reason->locked = 0;
      if (reason->learned && reason->size > 2)
	{
	  assert (ps->llocked > 0);
	  ps->llocked--;
	}
    }

  lit->val = UNDEF;
  NOTLIT (lit)->val = UNDEF;

  r = VAR2RNK (v);
  if (!r->pos)
    hpush (ps, r);

#ifndef NDSC
  {
    Cls * p, * next, ** q;

    q = LIT2DHTPS (lit);
    p = *q;
    *q = 0;

    while (p)
      {
	Lit * other = p->lits[0];

	if (other == lit)
	  {
	    other = p->lits[1];
	    q = p->next + 1;
	  }
	else
	  {
	    assert (p->lits[1] == lit);
	    q = p->next;
	  }

	next = *q;
	*q = *LIT2HTPS (other);
	*LIT2HTPS (other) = p;
	p = next;
      }
  }
#endif

#ifndef NADC
  if (v->adotabpos)
    {
      assert (ps->nadotab);
      assert (*v->adotabpos == v->ado);

      *v->adotabpos = 0;
      v->adotabpos = 0;

      ps->nadotab--;
    }
#endif
}

static Cls *
var2reason (PS * ps, Var * var)
{
  Cls * res = var->reason;
#ifdef NO_BINARY_CLAUSES
  Lit * this, * other;
  if (ISLITREASON (res))
    {
      this = VAR2LIT (var);
      if (this->val == FALSE)
	this = NOTLIT (this);

      other = REASON2LIT (res);
      assert (other->val == TRUE);
      assert (this->val == TRUE);
      res = setimpl (ps, NOTLIT (other), this);
    }
#else
  (void) ps;
#endif
  return res;
}

static void
mark_clause_to_be_collected (Cls * c)
{
  assert (!c->collect);
  c->collect = 1;
}

static void
undo (PS * ps, unsigned new_level)
{
  Lit *lit;
  Var *v;

  while (ps->thead > ps->trail)
    {
      lit = *--ps->thead;
      v = LIT2VAR (lit);
      if (v->level == new_level)
	{
	  ps->thead++;		/* fix pre decrement */
	  break;
	}

      unassign (ps, lit);
    }

  ps->LEVEL = new_level;
  ps->ttail = ps->thead;
  ps->ttail2 = ps->thead;
#ifndef NADC
  ps->ttailado = ps->thead;
#endif

#ifdef NO_BINARY_CLAUSES
  if (ps->conflict == &ps->cimpl)
    resetcimpl (ps);
#endif
#ifndef NADC
  if (ps->conflict && ps->conflict == ps->adoconflict)
    resetadoconflict (ps);
#endif
  ps->conflict = ps->mtcls;
  if (ps->LEVEL < ps->adecidelevel)
    {
      assert (ps->als < ps->alshead);
      ps->adecidelevel = 0;
      ps->alstail = ps->als;
    }
  LOG ( fprintf (ps->out, "%sback to level %u\n", ps->prefix, ps->LEVEL));
}

#ifndef NDEBUG

static int
clause_satisfied (Cls * c)
{
  Lit **p, **eol, *lit;

  eol = end_of_lits (c);
  for (p = c->lits; p < eol; p++)
    {
      lit = *p;
      if (lit->val == TRUE)
	return 1;
    }

  return 0;
}

static void
original_clauses_satisfied (PS * ps)
{
  Cls **p, *c;

  for (p = ps->oclauses; p < ps->ohead; p++)
    {
      c = *p;

      if (!c)
	continue;

      if (c->learned)
	continue;

      assert (clause_satisfied (c));
    }
}

static void
assumptions_satisfied (PS * ps)
{
  Lit *lit, ** p;

  for (p = ps->als; p < ps->alshead; p++)
    {
      lit = *p;
      assert (lit->val == TRUE);
    }
}

#endif

static void
sflush (PS * ps)
{
  double now = picosat_time_stamp ();
  double delta = now - ps->entered;
  delta = (delta < 0) ? 0 : delta;
  ps->seconds += delta;
  ps->entered = now;
}

static double
mb (PS * ps)
{
  return ps->current_bytes / (double) (1 << 20);
}

static double
avglevel (PS * ps)
{
  return ps->decisions ? ps->levelsum / ps->decisions : 0.0;
}

static void
rheader (PS * ps)
{
  assert (ps->lastrheader <= ps->reports);

  if (ps->lastrheader == ps->reports)
    return;

  ps->lastrheader = ps->reports;

   fprintf (ps->out, "%s\n", ps->prefix);
   fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]);
   fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]);
   fprintf (ps->out, "%s\n", ps->prefix);
}

static unsigned
dynamic_flips_per_assignment_per_mille (PS * ps)
{
  assert (FFLIPPEDPREC >= 1000);
  return ps->sdflips / (FFLIPPEDPREC / 1000);
}

#ifdef NLUBY

static int
high_agility (PS * ps)
{
  return dynamic_flips_per_assignment_per_mille (ps) >= 200;
}

static int
very_high_agility (PS * ps)
{
  return dynamic_flips_per_assignment_per_mille (ps) >= 250;
}

#else

static int
medium_agility (PS * ps)
{
  return dynamic_flips_per_assignment_per_mille (ps) >= 230;
}

#endif

static void
relemdata (PS * ps)
{
  char *p;
  int x;

  if (ps->reports < 0)
    {
      /* strip trailing white space 
       */
      for (x = 0; x <= 1; x++)
	{
	  p = ps->rline[x] + strlen (ps->rline[x]);
	  while (p-- > ps->rline[x])
	    {
	      if (*p != ' ')
		break;

	      *p = 0;
	    }
	}

      rheader (ps);
    }
  else
    fputc ('\n', ps->out);

  ps->RCOUNT = 0;
}

static void
relemhead (PS * ps, const char * name, int fp, double val)
{
  int x, y, len, size;
  const char *fmt;
  unsigned tmp, e;

  if (ps->reports < 0)
    {
      x = ps->RCOUNT & 1;
      y = (ps->RCOUNT / 2) * 12 + x * 6;

      if (ps->RCOUNT == 1)
	sprintf (ps->rline[1], "%6s", "");

      len = strlen (name);
      while (ps->szrline <= len + y + 1)
	{
	  size = ps->szrline ? 2 * ps->szrline : 128;
	  ps->rline[0] = resize (ps, ps->rline[0], ps->szrline, size);
	  ps->rline[1] = resize (ps, ps->rline[1], ps->szrline, size);
	  ps->szrline = size;
	}

      fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s";
      sprintf (ps->rline[x] + y, fmt, name, "");
    }
  else if (val < 0)
    {
      assert (fp);

      if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0)
	{
	   fprintf (ps->out, "-%4.1f ", -tmp / 10.0);
	}
      else
	{
	  tmp = -val / 10.0 + 0.5;
	  e = 1;
	  while (tmp >= 100)
	    {
	      tmp /= 10;
	      e++;
	    }

	   fprintf (ps->out, "-%2ue%u ", tmp, e);
	}
    }
  else
    {
      if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000)
	{
	   fprintf (ps->out, "%5.1f ", tmp / 10.0);
	}
      else if (!fp && (tmp = val) < 100000)
	{
	   fprintf (ps->out, "%5u ", tmp);
	}
      else
	{
	  tmp = val / 10.0 + 0.5;
	  e = 1;

	  while (tmp >= 1000)
	    {
	      tmp /= 10;
	      e++;
	    }

	   fprintf (ps->out, "%3ue%u ", tmp, e);
	}
    }

  ps->RCOUNT++;
}

inline static void
relem (PS * ps, const char *name, int fp, double val)
{
  if (name)
    relemhead (ps, name, fp, val);
  else
    relemdata (ps);
}

static unsigned
reduce_limit_on_lclauses (PS * ps)
{
  unsigned res = ps->lreduce;
  res += ps->llocked;
  return res;
}

static void
report (PS * ps, int replevel, char type)
{
  int rounds;

#ifdef RCODE
  (void) type;
#endif

  if (ps->verbosity < replevel)
    return;

  sflush (ps);

  if (!ps->reports)
    ps->reports = -1;

  for (rounds = (ps->reports < 0) ? 2 : 1; rounds; rounds--)
    {
      if (ps->reports >= 0)
	 fprintf (ps->out, "%s%c ", ps->prefix, type);

      relem (ps, "seconds", 1, ps->seconds);
      relem (ps, "level", 1, avglevel (ps));
      assert (ps->fixed <=  ps->max_var);
      relem (ps, "variables", 0, ps->max_var - ps->fixed);
      relem (ps, "used", 1, PERCENT (ps->vused, ps->max_var));
      relem (ps, "original", 0, ps->noclauses);
      relem (ps, "conflicts", 0, ps->conflicts);
      // relem (ps, "decisions", 0, ps->decisions);
      // relem (ps, "conf/dec", 1, PERCENT(ps->conflicts,ps->decisions));
      // relem (ps, "limit", 0, reduce_limit_on_lclauses (ps));
      relem (ps, "learned", 0, ps->nlclauses);
      // relem (ps, "limit", 1, PERCENT (ps->nlclauses, reduce_limit_on_lclauses (ps)));
      relem (ps, "limit", 0, ps->lreduce);
#ifdef STATS
      relem (ps, "learning", 1, PERCENT (ps->llused, ps->lladded));
#endif
      relem (ps, "agility", 1, dynamic_flips_per_assignment_per_mille (ps) / 10.0);
      // relem (ps, "original", 0, ps->noclauses);
      relem (ps, "MB", 1, mb (ps));
      // relem (ps, "lladded", 0, ps->lladded);
      // relem (ps, "llused", 0, ps->llused);

      relem (ps, 0, 0, 0);

      ps->reports++;
    }

  /* Adapt this to the number of rows in your terminal.
   */
  #define ROWS 25

  if (ps->reports % (ROWS - 3) == (ROWS - 4))
    rheader (ps);

  fflush (ps->out);
}

static int
bcp_queue_is_empty (PS * ps)
{
  if (ps->ttail != ps->thead)
    return 0;

  if (ps->ttail2 != ps->thead)
    return 0;

#ifndef NADC
  if (ps->ttailado != ps->thead)
    return 0;
#endif

  return 1;
}

static int
satisfied (PS * ps)
{
  assert (!ps->mtcls);
  assert (!ps->failed_assumption);
  if (ps->alstail < ps->alshead)
    return 0;
  assert (!ps->conflict);
  assert (bcp_queue_is_empty (ps));
  return ps->thead == ps->trail + ps->max_var;	/* all assigned */
}

static void
vrescore (PS * ps)
{
  Rnk *p, *eor = ps->rnks + ps->max_var;
  for (p = ps->rnks + 1; p <= eor; p++)
    if (p->score != INFFLT)
      p->score = mulflt (p->score, ps->ilvinc);
  ps->vinc = mulflt (ps->vinc, ps->ilvinc);;
#ifdef VISCORES
  ps->nvinc = mulflt (ps->nvinc, ps->lscore);;
#endif
}

static void
inc_score (PS * ps, Var * v)
{
  Flt score;
  Rnk *r;

#ifndef NFL
  if (ps->simplifying)
    return;
#endif

  if (!v->level)
    return;

  if (v->internal)
    return;

  r = VAR2RNK (v);
  score = r->score;

  assert (score != INFFLT);

  score = addflt (score, ps->vinc);
  assert (score < INFFLT);
  r->score = score;
  if (r->pos > 0)
    hup (ps, r);

  if (score > ps->lscore)
    vrescore (ps);
}

static void
inc_activity (PS * ps, Cls * c)
{
  Act *p;

  if (!c->learned)
    return;

  if (c->size <= 2)
    return;

  p = CLS2ACT (c);
  *p = addflt (*p, ps->cinc);
}

static unsigned
hashlevel (unsigned l)
{
  return 1u << (l & 31);
}

static void
push (PS * ps, Var * v)
{
  if (ps->dhead == ps->eod)
    ENLARGE (ps->dfs, ps->dhead, ps->eod);

  *ps->dhead++ = v;
}

static Var * 
pop (PS * ps)
{
  assert (ps->dfs < ps->dhead);
  return *--ps->dhead;
}

static void
analyze (PS * ps)
{
  unsigned open, minlevel, siglevels, l, old, i, orig;
  Lit *this, *other, **p, **q, **eol;
  Var *v, *u, **m, *start, *uip;
  Cls *c;

  assert (ps->conflict);

  assert (ps->ahead == ps->added);
  assert (ps->mhead == ps->marked);
  assert (ps->rhead == ps->resolved);

  /* First, search for First UIP variable and mark all resolved variables.
   * At the same time determine the minimum decision level involved.
   * Increase activities of resolved variables.
   */
  q = ps->thead;
  open = 0;
  minlevel = ps->LEVEL;
  siglevels = 0;
  uip = 0;

  c = ps->conflict;

  for (;;)
    {
      add_antecedent (ps, c);
      inc_activity (ps, c);
      eol = end_of_lits (c);
      for (p = c->lits; p < eol; p++)
	{
	  other = *p;

	  if (other->val == TRUE)
	    continue;

	  assert (other->val == FALSE);

	  u = LIT2VAR (other);
	  if (u->mark)
	    continue;
	  
	  u->mark = 1;
	  inc_score (ps, u);
	  use_var (ps, u);

	  if (u->level == ps->LEVEL)
	    {
	      open++;
	    }
	  else 
	    {
	      push_var_as_marked (ps, u);

	      if (u->level)
		{
		  /* The statistics counter 'nonminimizedllits' sums up the
		   * number of literals that would be added if only the
		   * 'first UIP' scheme for learned clauses would be used
		   * and no clause minimization.
		   */
		  ps->nonminimizedllits++;

		  if (u->level < minlevel)
		    minlevel = u->level;

		  siglevels |= hashlevel (u->level);
		}
	      else
		{
		  assert (!u->level);
		  assert (u->reason);
		}
	    }
	}

      do
	{
	  if (q == ps->trail)
	    {
	      uip = 0;
	      goto DONE_FIRST_UIP;
	    }

	  this = *--q;
	  uip = LIT2VAR (this);
	}
      while (!uip->mark);

      uip->mark = 0;

      c = var2reason (ps, uip);
#ifdef NO_BINARY_CLAUSES
      if (c == &ps->impl)
	resetimpl (ps);
#endif
     open--;
     if ((!open && ps->LEVEL) || !c)
	break;

     assert (c);
    }

DONE_FIRST_UIP:

  if (uip)
    {
      assert (ps->LEVEL);
      this = VAR2LIT (uip);
      this += (this->val == TRUE);
      ps->nonminimizedllits++;
      ps->minimizedllits++;
      add_lit (ps, this);
#ifdef STATS
      if (uip->reason)
	ps->uips++;
#endif
    }
  else
    assert (!ps->LEVEL);

  /* Second, try to mark more intermediate variables, with the goal to
   * minimize the conflict clause.  This is a DFS from already marked
   * variables backward through the implication graph.  It tries to reach
   * other marked variables.  If the search reaches an unmarked decision
   * variable or a variable assigned below the minimum level of variables in
   * the first uip learned clause or a level on which no variable has been
   * marked, then the variable from which the DFS is started is not
   * redundant.  Otherwise the start variable is redundant and will
   * eventually be removed from the learned clause in step 4.  We initially
   * implemented BFS, but then profiling revelead that this step is a bottle
   * neck for certain incremental applications.  After switching to DFS this
   * hot spot went away.
   */
  orig = ps->mhead - ps->marked;
  for (i = 0; i < orig; i++)
    {
      start = ps->marked[i];

      assert (start->mark);
      assert (start != uip);
      assert (start->level < ps->LEVEL);

      if (!start->reason)
	continue;

      old = ps->mhead - ps->marked;
      assert (ps->dhead == ps->dfs);
      push (ps, start);

      while (ps->dhead > ps->dfs)
	{
	  u = pop (ps);
	  assert (u->mark);

	  c = var2reason (ps, u);
#ifdef NO_BINARY_CLAUSES
	  if (c == &ps->impl)
	    resetimpl (ps);
#endif
	  if (!c || 
	      ((l = u->level) && 
	       (l < minlevel || ((hashlevel (l) & ~siglevels)))))
	    {
	      while (ps->mhead > ps->marked + old)	/* reset all marked */
		(*--ps->mhead)->mark = 0;

	      ps->dhead = ps->dfs;		/* and DFS stack */
	      break;
	    }

	  eol = end_of_lits (c);
	  for (p = c->lits; p < eol; p++)
	    {
	      v = LIT2VAR (*p);
	      if (v->mark)
		continue;

	      mark_var (ps, v);
	      push (ps, v);
	    }
	}
    }

  for (m = ps->marked; m < ps->mhead; m++)
    {
      v = *m;

      assert (v->mark);
      assert (!v->resolved);

      use_var (ps, v);

      c = var2reason (ps, v);
      if (!c)
	continue;

#ifdef NO_BINARY_CLAUSES
      if (c == &ps->impl)
	resetimpl (ps);
#endif
      eol = end_of_lits (c);
      for (p = c->lits; p < eol; p++)
	{
	  other = *p;

	  u = LIT2VAR (other);
	  if (!u->level)
	    continue;

	  if (!u->mark)		/* 'MARKTEST' */
	    break;
	}

      if (p != eol)
	continue;

      add_antecedent (ps, c);
      v->resolved = 1;
    }

  for (m = ps->marked; m < ps->mhead; m++)
    {
      v = *m;

      assert (v->mark);
      v->mark = 0;

      if (v->resolved)
	{
	  v->resolved = 0;
	  continue;
	}

      this = VAR2LIT (v);
      if (this->val == TRUE)
	this++;			/* actually NOTLIT */

      add_lit (ps, this);
      ps->minimizedllits++;
    }

  assert (ps->ahead <= ps->eoa);
  assert (ps->rhead <= ps->eor);

  ps->mhead = ps->marked;
}

static void
fanalyze (PS * ps)
{
  Lit ** eol, ** p, * lit;
  Cls * c, * reason;
  Var * v, * u;
  int next;

#ifndef RCODE
  double start = picosat_time_stamp ();
#endif

  assert (ps->failed_assumption);
  assert (ps->failed_assumption->val == FALSE);

  v = LIT2VAR (ps->failed_assumption);
  reason = var2reason (ps, v);
  if (!reason) return;
#ifdef NO_BINARY_CLAUSES
  if (reason == &ps->impl)
    resetimpl (ps);
#endif

  eol = end_of_lits (reason);
  for (p = reason->lits; p != eol; p++)
    {
      lit = *p;
      u = LIT2VAR (lit);
      if (u == v) continue;
      if (u->reason) break;
    }
  if (p == eol) return;

  assert (ps->ahead == ps->added);
  assert (ps->mhead == ps->marked);
  assert (ps->rhead == ps->resolved);

  next = 0;
  mark_var (ps, v);
  add_lit (ps, NOTLIT (ps->failed_assumption));

  do
    {
      v = ps->marked[next++];
      use_var (ps, v);
      if (v->reason)
	{
	  reason = var2reason (ps, v);
#ifdef NO_BINARY_CLAUSES
	  if (reason == &ps->impl)
	    resetimpl (ps);
#endif
	  add_antecedent (ps, reason);
	  eol = end_of_lits (reason);
	  for (p = reason->lits; p != eol; p++)
	    {
	      lit = *p;
	      u = LIT2VAR (lit);
	      if (u == v) continue;
	      if (u->mark) continue;
	      mark_var (ps, u);
	    }
	}
      else
	{
	  lit = VAR2LIT (v);
	  if (lit->val == TRUE) lit = NOTLIT (lit);
	  add_lit (ps, lit);
	}
    } 
  while (ps->marked + next < ps->mhead);

  c = add_simplified_clause (ps, 1);
  v = LIT2VAR (ps->failed_assumption);
  reason = v->reason;
#ifdef NO_BINARY_CLAUSES
  if (!ISLITREASON (reason))
#endif
    {
      assert (reason->locked);
      reason->locked = 0;
      if (reason->learned && reason->size > 2)
	{
	  assert (ps->llocked > 0);
	  ps->llocked--;
	}
    }

#ifdef NO_BINARY_CLAUSES
  if (c == &ps->impl)
    {
      c = impl2reason (ps, NOTLIT (ps->failed_assumption));
    }
  else
#endif
    {
      assert (c->learned);
      assert (!c->locked);
      c->locked = 1;
      if (c->size > 2)
	{
	  ps->llocked++;
	  assert (ps->llocked > 0);
	}
    }

  v->reason = c;

  while (ps->mhead > ps->marked)
    (*--ps->mhead)->mark = 0;

  if (ps->verbosity)
     fprintf (ps->out, "%sfanalyze took %.1f seconds\n", 
	     ps->prefix, picosat_time_stamp () - start);
}

/* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in
 * which 'this' occurs.
 */
inline static void
prop2 (PS * ps, Lit * this)
{
#ifdef NO_BINARY_CLAUSES
  Lit ** l, ** start;
  Ltk * lstk;
#else
  Cls * c, ** p;
  Cls * next;
#endif
  Lit * other;
  Val tmp;

  assert (this->val == FALSE);

#ifdef NO_BINARY_CLAUSES
  lstk = LIT2IMPLS (this);
  start = lstk->start;
  l = start + lstk->count;
  while (l != start)
    {
      /* The counter 'visits' is the number of clauses that are
       * visited during propagations of assignments.
       */
      ps->visits++;
#ifdef STATS
      ps->bvisits++;
#endif
      other = *--l;
      tmp = other->val;

      if (tmp == TRUE)
	{
#ifdef STATS
	  ps->othertrue++;
	  ps->othertrue2++;
	  if (LIT2VAR (other)->level < ps->LEVEL)
	    ps->othertrue2u++;
#endif
	  continue;
	}

      if (tmp != FALSE)
	{
	  assign_forced (ps, other, LIT2REASON (NOTLIT(this)));
	  continue;
	}

      if (ps->conflict == &ps->cimpl)
	resetcimpl (ps);
      ps->conflict = setcimpl (ps, this, other);
    }
#else
  /* Traverse all binary clauses with 'this'.  Head/Tail pointers for binary
   * clauses do not have to be modified here.
   */
  p = LIT2IMPLS (this);
  for (c = *p; c; c = next)
    {
      ps->visits++;
#ifdef STATS
      ps->bvisits++;
#endif
      assert (!c->collect);
#ifdef TRACE
      assert (!c->collected);
#endif
      assert (c->size == 2);
      
      other = c->lits[0];
      if (other == this)
	{
	  next = c->next[0];
	  other = c->lits[1];
	}
      else
	next = c->next[1];

      tmp = other->val;

      if (tmp == TRUE)
	{
#ifdef STATS
	  ps->othertrue++;
	  ps->othertrue2++;
	  if (LIT2VAR (other)->level < ps->LEVEL)
	    ps->othertrue2u++;
#endif
	  continue;
	}

      if (tmp == FALSE)
	ps->conflict = c;
      else
	assign_forced (ps, other, c);	/* unit clause */
    }
#endif /* !defined(NO_BINARY_CLAUSES) */
}

#ifndef NDSC
static int
should_disconnect_head_tail (PS * ps, Lit * lit)
{
  unsigned litlevel;
  Var * v;

  assert (lit->val == TRUE);

  v = LIT2VAR (lit);
  litlevel = v->level;

  if (!litlevel)
    return 1;

#ifndef NFL
  if (ps->simplifying)
    return 0;
#endif

  return litlevel < ps->LEVEL;
}
#endif

inline static void
propl (PS * ps, Lit * this)
{
  Lit **l, *other, *prev, *new_lit, **eol;
  Cls *next, **htp_ptr, **new_htp_ptr;
  Cls *c;
#ifdef STATS
  unsigned size;
#endif

  htp_ptr = LIT2HTPS (this);
  assert (this->val == FALSE);

  /* Traverse all non binary clauses with 'this'.  Head/Tail pointers are
   * updated as well.
   */
  for (c = *htp_ptr; c; c = next)
    {
      ps->visits++;
#ifdef STATS
      size = c->size;
      assert (size >= 3);
      ps->traversals++;	/* other is dereferenced at least */

      if (size == 3)
	ps->tvisits++;
      else if (size >= 4)
	{
	  ps->lvisits++;
	  ps->ltraversals++;
	}
#endif
#ifdef TRACE
      assert (!c->collected);
#endif
      assert (c->size > 0);

      other = c->lits[0];
      if (other != this)
	{
	  assert (c->size != 1);
	  c->lits[0] = this;
	  c->lits[1] = other;
	  next = c->next[1];
	  c->next[1] = c->next[0];
	  c->next[0] = next;
	}
      else if (c->size == 1)	/* With assumptions we need to
	                         * traverse unit clauses as well.
			         */
	{
	  assert (!ps->conflict);
	  ps->conflict = c;
	  break;
	}
      else
	{
	  assert (other == this && c->size > 1);
	  other = c->lits[1];
	  next = c->next[0];
	}
      assert (other == c->lits[1]);
      assert (this == c->lits[0]);
      assert (next == c->next[0]);
      assert (!c->collect);

      if (other->val == TRUE)
	{
#ifdef STATS
	  ps->othertrue++;
	  ps->othertruel++;
#endif
#ifndef NDSC
	  if (should_disconnect_head_tail (ps, other))
	    {
	      new_htp_ptr = LIT2DHTPS (other);
	      c->next[0] = *new_htp_ptr;
	      *new_htp_ptr = c;
#ifdef STATS
	      ps->othertruelu++;
#endif
	      *htp_ptr = next;
	      continue;
	    }
#endif
	  htp_ptr = c->next;
	  continue;
	}

      l = c->lits + 1;
      eol = (Lit**) c->lits + c->size;
      prev = this;

      while (++l != eol)
	{
#ifdef STATS
	  if (size >= 3)
	    {
	      ps->traversals++;
	      if (size > 3)
		ps->ltraversals++;
	    }
#endif
	  new_lit = *l;
	  *l = prev;
	  prev = new_lit;
	  if (new_lit->val != FALSE) break;
	}

      if (l == eol)
	{
	  while (l > c->lits + 2) 
	    {
	      new_lit = *--l;
	      *l = prev;
	      prev = new_lit;
	    }
	  assert (c->lits[0] == this);

	  assert (other == c->lits[1]);
	  if (other->val == FALSE)	/* found conflict */
	    {
	      assert (!ps->conflict);
	      ps->conflict = c;
	      return;
	    }

	  assign_forced (ps, other, c);		/* unit clause */
	  htp_ptr = c->next;
	}
      else
	{
	  assert (new_lit->val == TRUE || new_lit->val == UNDEF);
	  c->lits[0] = new_lit;
	  // *l = this;
	  new_htp_ptr = LIT2HTPS (new_lit);
	  c->next[0] = *new_htp_ptr;
	  *new_htp_ptr = c;
	  *htp_ptr = next;
	}
    }
}

#ifndef NADC

static unsigned primes[] = { 996293, 330643, 753947, 500873 };

#define PRIMES ((sizeof primes)/sizeof *primes)

static unsigned
hash_ado (PS * ps, Lit ** ado, unsigned salt)
{
  unsigned i, res, tmp;
  Lit ** p, * lit;

  assert (salt < PRIMES);

  i = salt;
  res = 0;

  for (p = ado; (lit = *p); p++)
    {
      assert (lit->val);

      tmp = res >> 31;
      res <<= 1;

      if (lit->val > 0)
	res |= 1;

      assert (i < PRIMES);
      res *= primes[i++];
      if (i == PRIMES)
	i = 0;

      res += tmp;
    }

  return res & (ps->szadotab - 1);
}

static unsigned
cmp_ado (Lit ** a, Lit ** b)
{
  Lit ** p, ** q, * l, * k;
  int res;

  for (p = a, q = b; (l = *p); p++, q++)
    {
      k = *q;
      assert (k);
      if ((res = (l->val - k->val)))
	return res;
    }

  assert (!*q);

  return 0;
}

static Lit ***
find_ado (PS * ps, Lit ** ado)
{
  Lit *** res, ** other;
  unsigned pos, delta;

  pos = hash_ado (ps, ado, 0);
  assert (pos < ps->szadotab);
  res = ps->adotab + pos;

  other = *res;
  if (!other || !cmp_ado (other, ado))
    return res;

  delta = hash_ado (ps, ado, 1);
  if (!(delta & 1))
    delta++;

  assert (delta & 1);
  assert (delta < ps->szadotab);

  for (;;)
    {
      pos += delta;
      if (pos >= ps->szadotab)
	pos -= ps->szadotab;

      assert (pos < ps->szadotab);
      res = ps->adotab + pos;
      other = *res;
      if (!other || !cmp_ado (other, ado))
	return res;
    }
}

static void
enlarge_adotab (PS * ps)
{
  /* TODO make this generic */

  ABORTIF (ps->szadotab, 
           "internal: all different objects table needs larger initial size");
  assert (!ps->nadotab);
  ps->szadotab = 10000;
  NEWN (ps->adotab, ps->szadotab);
  CLRN (ps->adotab, ps->szadotab);
}

static int
propado (PS * ps, Var * v)
{
  Lit ** p, ** q, *** adotabpos, **ado, * lit;
  Var * u;

  if (ps->LEVEL && ps->adodisabled)
    return 1;

  assert (!ps->conflict);
  assert (!ps->adoconflict);
  assert (VAR2LIT (v)->val != UNDEF);
  assert (!v->adotabpos);

  if (!v->ado)
    return 1;

  assert (v->inado);

  for (p = v->ado; (lit = *p); p++)
    if (lit->val == UNDEF)
      {
	u = LIT2VAR (lit);
	assert (!u->ado);
	u->ado = v->ado;
	v->ado = 0;

	return 1;
      }

  if (4 * ps->nadotab >= 3 * ps->szadotab)	/* at least 75% filled */
    enlarge_adotab (ps);

  adotabpos = find_ado (ps, v->ado);
  ado = *adotabpos;

  if (!ado)
    {
      ps->nadotab++;
      v->adotabpos = adotabpos;
      *adotabpos = v->ado;
      return 1;
    }

  assert (ado != v->ado);

  ps->adoconflict = new_clause (ps, 2 * llength (ado), 1);
  q = ps->adoconflict->lits;

  for (p = ado; (lit = *p); p++)
    *q++ = lit->val == FALSE ? lit : NOTLIT (lit);

  for (p = v->ado; (lit = *p); p++)
    *q++ = lit->val == FALSE ? lit : NOTLIT (lit);

  assert (q == ENDOFCLS (ps->adoconflict));
  ps->conflict = ps->adoconflict;
  ps->adoconflicts++;
  return 0;
}

#endif

static void
bcp (PS * ps)
{
  int props = 0;
  assert (!ps->conflict);

  if (ps->mtcls)
    return;

  for (;;)
    {
      if (ps->ttail2 < ps->thead)	/* prioritize implications */
	{
	  props++;
	  prop2 (ps, NOTLIT (*ps->ttail2++));
	}
      else if (ps->ttail < ps->thead)	/* unit clauses or clauses with length > 2 */
	{
	  if (ps->conflict) break;
	  propl (ps, NOTLIT (*ps->ttail++));
	  if (ps->conflict) break;
	}
#ifndef NADC
      else if (ps->ttailado < ps->thead)
	{
	  if (ps->conflict) break;
	  propado (ps, LIT2VAR (*ps->ttailado++));
	  if (ps->conflict) break;
	}
#endif
      else
	break;		/* all assignments propagated, so break */
    }

  ps->propagations += props;
}

static unsigned
drive (PS * ps)
{
  unsigned res, vlevel;
  Lit **p;
  Var *v;

  res = 0;
  for (p = ps->added; p < ps->ahead; p++)
    {
      v = LIT2VAR (*p);
      vlevel = v->level;
      assert (vlevel <= ps->LEVEL);
      if (vlevel < ps->LEVEL && vlevel > res)
	res = vlevel;
    }

  return res;
}

#ifdef VISCORES

static void
viscores (PS * ps)
{
  Rnk *p, *eor = ps->rnks + ps->max_var;
  char name[100], cmd[200];
  FILE * data;
  Flt s;
  int i;

  for (p = ps->rnks + 1; p <= ps->eor; p++)
    {
      s = p->score;
      if (s == INFFLT)
	continue;
      s = mulflt (s, ps->nvinc);
      assert (flt2double (s) <= 1.0);
    }

  sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts);
  sprintf (cmd, "sort -n|nl>%s", name);

  data = popen (cmd, "w");
  for (p = ps->rnks + 1; p <= ps->eor; p++)
    {
      s = p->score;
      if (s == INFFLT)
	continue;
      s = mulflt (s, ps->nvinc);
      fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnks));
    }
  fflush (data);
  pclose (data);

  for (i = 0; i < 8; i++)
    {
      sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i);
      system (cmd);
    }

  fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts);
  fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max_var);

  for (i = 0; i < 8; i++)
    fprintf (ps->fviscores, 
             ", \"%s.%d\" using 1:2:3 with labels tc lt %d", 
	     name, i, i + 1);

  fputc ('\n', ps->fviscores);
  fflush (ps->fviscores);
#ifndef WRITEGIF
  usleep (50000);		/* refresh rate of 20 Hz */
#endif
}

#endif

static void
crescore (PS * ps)
{
  Cls **p, *c;
  Act *a;
  Flt factor;
  int l = log2flt (ps->cinc);
  assert (l > 0);
  factor = base2flt (1, -l);

  for (p = ps->lclauses; p != ps->lhead; p++)
    {
      c = *p;

      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif
      assert (c->learned);

      if (c->size <= 2)
	continue;

      a = CLS2ACT (c);
      *a = mulflt (*a, factor);
    }

  ps->cinc = mulflt (ps->cinc, factor);
}

static void
inc_vinc (PS * ps)
{
#ifdef VISCORES
  ps->nvinc = mulflt (ps->nvinc, ps->fvinc);
#endif
  ps->vinc = mulflt (ps->vinc, ps->ifvinc);
}

inline static void
inc_max_var (PS * ps)
{
  Lit *lit;
  Rnk *r;
  Var *v;

  assert (ps->max_var < ps->size_vars);

  if (ps->max_var + 1 == ps->size_vars)
    enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */

  ps->max_var++;			/* new index of variable */
  assert (ps->max_var);			/* no unsigned overflow */

  assert (ps->max_var < ps->size_vars);

  lit = ps->lits + 2 * ps->max_var;
  lit[0].val = lit[1].val = UNDEF;

  memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps);
#ifndef NDSC
  memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps);
#endif
  memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls);
  memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh);

  v = ps->vars + ps->max_var;		/* initialize variable components */
  CLR (v);

  r = ps->rnks + ps->max_var;		/* initialize rank */
  CLR (r);

  hpush (ps, r);
}

static void
force (PS * ps, Cls * c)
{
  Lit ** p, ** eol, * lit, * forced;
  Cls * reason;

  forced = 0;
  reason = c;

  eol = end_of_lits (c);
  for (p = c->lits; p < eol; p++)
    {
      lit = *p;
      if (lit->val == UNDEF)
	{
	  assert (!forced);
	  forced = lit;
#ifdef NO_BINARY_CLAUSES
	  if (c == &ps->impl)
	    reason = LIT2REASON (NOTLIT (p[p == c->lits ? 1 : -1]));
#endif
	}
      else
	assert (lit->val == FALSE);
    }

#ifdef NO_BINARY_CLAUSES
  if (c == &ps->impl)
    resetimpl (ps);
#endif
  if (!forced)
    return;

  assign_forced (ps, forced, reason);
}

static void
inc_lreduce (PS * ps)
{
#ifdef STATS
  ps->inclreduces++;
#endif
  ps->lreduce *= FREDUCE;
  ps->lreduce /= 100;
  report (ps, 1, '+');
}

static void
backtrack (PS * ps)
{
  unsigned new_level;
  Cls * c;

  ps->conflicts++;
  LOG ( fprintf (ps->out, "%sconflict ", ps->prefix); dumpclsnl (ps, ps->conflict));

  analyze (ps);
  new_level = drive (ps);
  // TODO: why not? assert (new_level != 1  || (ps->ahead - ps->added) == 2);
  c = add_simplified_clause (ps, 1);
  undo (ps, new_level);
  force (ps, c);

  if (
#ifndef NFL
      !ps->simplifying && 
#endif
      !--ps->lreduceadjustcnt)
    {
      /* With FREDUCE==110 and FREDADJ=121 we stir 'lreduce' to be
       * proportional to 'sqrt(conflicts)'.  In earlier version we actually
       * used  'FREDADJ=150', which results in 'lreduce' to approximate
       * 'conflicts^(log(1.1)/log(1.5))' which is close to the fourth root
       * of 'conflicts', since log(1.1)/log(1.5)=0.235 (as observed by
       * Donald Knuth). The square root is the same we get by a Glucose
       * style increase, which simply adds a constant at every reduction.
       * This would be way simpler to implement but for now we keep the more
       * complicated code using the adjust increments and counters.
       */
      ps->lreduceadjustinc *= FREDADJ; ps->lreduceadjustinc /= 100; ps->lreduceadjustcnt
      = ps->lreduceadjustinc;
      inc_lreduce (ps);
    }

  if (ps->verbosity >= 4 && !(ps->conflicts % 1000))
    report (ps, 4, 'C');
}

static void
inc_cinc (PS * ps)
{
  ps->cinc = mulflt (ps->cinc, ps->fcinc);
  if (ps->lcinc < ps->cinc)
    crescore (ps);
}

static void
incincs (PS * ps)
{
  inc_vinc (ps);
  inc_cinc (ps);
#ifdef VISCORES
  viscores (ps);
#endif
}

static void
disconnect_clause (PS * ps, Cls * c)
{
  assert (c->connected);

  if (c->size > 2)
    {
      if (c->learned)
	{
	  assert (ps->nlclauses > 0);
	  ps->nlclauses--;

	  assert (ps->llits >= c->size);
	  ps->llits -= c->size;
	}
      else
	{
	  assert (ps->noclauses > 0);
	  ps->noclauses--;

	  assert (ps->olits >= c->size);
	  ps->olits -= c->size;
	}
    }

#ifndef NDEBUG
  c->connected = 0;
#endif
}

static int
clause_is_toplevel_satisfied (PS * ps, Cls * c)
{
  Lit *lit, **p, **eol = end_of_lits (c);
  Var *v;

  for (p = c->lits; p < eol; p++)
    {
      lit = *p;
      if (lit->val == TRUE)
	{
	  v = LIT2VAR (lit);
	  if (!v->level)
	    return 1;
	}
    }

  return 0;
}

static int
collect_clause (PS * ps, Cls * c)
{
  assert (c->collect);
  c->collect = 0;

#ifdef TRACE
  assert (!c->collected);
  c->collected = 1;
#endif
  disconnect_clause (ps, c);

#ifdef TRACE
  if (ps->trace && (!c->learned || c->used))
    return 0;
#endif
  delete_clause (ps, c);

  return 1;
}

static size_t
collect_clauses (PS * ps)
{
  Cls *c, **p, **q, * next;
  Lit * lit, * eol;
  size_t res;
  int i;

  res = ps->current_bytes;

  eol = ps->lits + 2 * ps->max_var + 1;
  for (lit = ps->lits + 2; lit <= eol; lit++)
    {
      for (i = 0; i <= 1; i++)
	{
	  if (i)
	    {
#ifdef NO_BINARY_CLAUSES
	      Ltk * lstk = LIT2IMPLS (lit);
	      Lit ** r, ** s;
	      r = lstk->start;
	      if (lit->val != TRUE || LIT2VAR (lit)->level)
		for (s = r; s < lstk->start + lstk->count; s++)
		  {
		    Lit * other = *s;
		    Var *v = LIT2VAR (other);
		    if (v->level ||
		        other->val != TRUE)
		      *r++ = other;
		  }
	      lstk->count = r - lstk->start;
	      continue;
#else
	      p = LIT2IMPLS (lit);
#endif
	    }
	  else
	    p = LIT2HTPS (lit);

	  for (c = *p; c; c = next)
	    {
	      q = c->next;
	      if (c->lits[0] != lit)
		q++;

	      next = *q;
	      if (c->collect)
		*p = next;
	      else
		p = q;
	    }
	}
    }

#ifndef NDSC
  for (lit = ps->lits + 2; lit <= eol; lit++)
    {
      p = LIT2DHTPS (lit); 
      while ((c = *p))
	{
	  Lit * other = c->lits[0];
	  if (other == lit)
	    {
	      q = c->next + 1;
	    }
	  else
	    {
	      assert (c->lits[1] == lit);
	      q = c->next;
	    }

	  if (c->collect)
	    *p = *q;
	  else
	    p = q;
	}
    }
#endif

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;

      if (!c)
	continue;

      if (!c->collect)
	continue;

      if (collect_clause (ps, c))
	*p = 0;
    }

#ifdef TRACE
  if (!ps->trace)
#endif
    {
      q = ps->oclauses;
      for (p = q; p < ps->ohead; p++)
	if ((c = *p))
	  *q++ = c;
      ps->ohead = q;

      q = ps->lclauses;
      for (p = q; p < ps->lhead; p++)
	if ((c = *p))
	  *q++ = c;
      ps->lhead = q;
    }

  assert (ps->current_bytes <= res);
  res -= ps->current_bytes;
  ps->recycled += res;

  LOG ( fprintf (ps->out, "%scollected %ld bytes\n", ps->prefix, (long)res));

  return res;
}

static int
need_to_reduce (PS * ps)
{
  return ps->nlclauses >= reduce_limit_on_lclauses (ps);
}

#ifdef NLUBY

static void
inc_drestart (PS * ps)
{
  ps->drestart *= FRESTART;
  ps->drestart /= 100;

  if (ps->drestart >= MAXRESTART)
    ps->drestart = MAXRESTART;
}

static void
inc_ddrestart (PS * ps)
{
  ps->ddrestart *= FRESTART;
  ps->ddrestart /= 100;

  if (ps->ddrestart >= MAXRESTART)
    ps->ddrestart = MAXRESTART;
}

#else

static unsigned
luby (unsigned i)
{
  unsigned k;
  for (k = 1; k < 32; k++)
    if (i == (1u << k) - 1)
      return 1u << (k - 1);

  for (k = 1;; k++)
    if ((1u << (k - 1)) <= i && i < (1u << k) - 1)
      return luby (i - (1u << (k-1)) + 1);
}

#endif

#ifndef NLUBY
static void
inc_lrestart (PS * ps, int skip)
{
  unsigned delta;

  delta = 100 * luby (++ps->lubycnt);
  ps->lrestart = ps->conflicts + delta;

  if (ps->waslubymaxdelta)
    report (ps, 1, skip ? 'N' : 'R');
  else
    report (ps, 2, skip ? 'n' : 'r');

  if (delta > ps->lubymaxdelta)
    {
      ps->lubymaxdelta = delta;
      ps->waslubymaxdelta = 1;
    }
  else
    ps->waslubymaxdelta = 0;
}
#endif

static void
init_restart (PS * ps)
{
#ifdef NLUBY
  /* TODO: why is it better in incremental usage to have smaller initial
   * outer restart interval?
   */
  ps->ddrestart = ps->calls > 1 ? MINRESTART : 1000;
  ps->drestart = MINRESTART;
  ps->lrestart = ps->conflicts + ps->drestart;
#else
  ps->lubycnt = 0;
  ps->lubymaxdelta = 0;
  ps->waslubymaxdelta = 0;
  inc_lrestart (ps, 0);
#endif
}

static void
restart (PS * ps)
{
  int skip; 
#ifdef NLUBY
  char kind;
  int outer;
 
  inc_drestart (ps);
  outer = (ps->drestart >= ps->ddrestart);

  if (outer)
    skip = very_high_agility (ps);
  else
    skip = high_agility (ps);
#else
  skip = medium_agility (ps);
#endif

#ifdef STATS
  if (skip)
    ps->skippedrestarts++;
#endif

  assert (ps->conflicts >= ps->lrestart);

  if (!skip)
    {
      ps->restarts++;
      assert (ps->LEVEL > 1);
      LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts));
      undo (ps, 0);
    }

#ifdef NLUBY
  if (outer)
    {
      kind = skip ? 'N' : 'R';
      inc_ddrestart (ps);
      ps->drestart = MINRESTART;
    }
  else  if (skip)
    {
      kind = 'n';
    }
  else
    {
      kind = 'r';
    }

  assert (ps->drestart <= MAXRESTART);
  ps->lrestart = ps->conflicts + ps->drestart;
  assert (ps->lrestart > ps->conflicts);

  report (outer ? 1 : 2, kind);
#else
  inc_lrestart (ps, skip);
#endif
}

inline static void
assign_decision (PS * ps, Lit * lit)
{
  assert (!ps->conflict);

  ps->LEVEL++;

  LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL));
  LOG ( fprintf (ps->out,
		 "%sassign %d at level %d <= DECISION\n",
		 ps->prefix, LIT2INT (lit), ps->LEVEL));

  assign (ps, lit, 0);
}

#ifndef NFL

static int
lit_has_binary_clauses (PS * ps, Lit * lit)
{
#ifdef NO_BINARY_CLAUSES
  Ltk* lstk = LIT2IMPLS (lit);
  return lstk->count != 0;
#else
  return *LIT2IMPLS (lit) != 0;
#endif
}

static void
flbcp (PS * ps)
{
#ifdef STATS
  unsigned long long propagaions_before_bcp = ps->propagations;
#endif
  bcp (ps);
#ifdef STATS
  ps->flprops += ps->propagations - propagaions_before_bcp;
#endif
}

inline static int
cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b)
{
  (void) ps;
  return -cmp_rnk (a, b);
}

inline static Flt
rnk2jwh (PS * ps, Rnk * r)
{
  Flt res, sum, pjwh, njwh;
  Lit * plit, * nlit;

  plit = RNK2LIT (r);
  nlit = plit + 1;
  
  pjwh = *LIT2JWH (plit);
  njwh = *LIT2JWH (nlit);

  res = mulflt (pjwh, njwh);

  sum = addflt (pjwh, njwh);
  sum = mulflt (sum, base2flt (1, -10));
  res = addflt (res, sum);

  return res;
}

static int
cmp_inverse_jwh_rnk (PS * ps, Rnk * r, Rnk * s)
{
  Flt a = rnk2jwh (ps, r);
  Flt b = rnk2jwh (ps, s);
  int res = cmpflt (a, b);

  if (res)
    return -res;

  return cmp_inverse_rnk (ps, r, s);
}

static void
faillits (PS * ps)
{
  unsigned i, j, old_trail_count, common, saved_count;
  unsigned new_saved_size, oldladded = ps->ladded;
  unsigned long long limit, delta;
  Lit * lit, * other, * pivot;
  Rnk * r, ** p, ** q;
  int new_trail_count;
  double started;

  if (PLAIN)
    return;

  if (ps->heap + 1 >= ps->hhead)
    return;

  if (ps->propagations < ps->fllimit)
    return;

  sflush (ps);
  started = ps->seconds;

  ps->flcalls++;
#ifdef STATSA
  ps->flrounds++;
#endif
  delta = ps->propagations/10;
  if (delta >= 100*1000*1000) delta = 100*1000*1000;
  else if (delta <= 100*1000) delta = 100*1000;

  limit = ps->propagations + delta;
  ps->fllimit = ps->propagations;

  assert (!ps->LEVEL);
  assert (ps->simplifying);

  if (ps->flcalls <= 1)
    SORT (Rnk *, cmp_inverse_jwh_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
  else
    SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));

  i = 1;		/* NOTE: heap starts at position '1' */

  while (ps->propagations < limit)
    {
      if (ps->heap + i == ps->hhead)
	{
	  if (ps->ladded == oldladded)
	    break;

	  i = 1;
#ifdef STATS
	  ps->flrounds++;
#endif
	  oldladded = ps->ladded;
	}

      assert (ps->heap + i < ps->hhead);

      r = ps->heap[i++];
      lit = RNK2LIT (r);

      if (lit->val)
	continue;

      if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
	{
#ifdef STATS
	  ps->flskipped++;
#endif
	  continue;
	}

#ifdef STATS
      ps->fltried++;
#endif
      LOG ( fprintf (ps->out, "%strying %d as failed literal\n",
	    ps->prefix, LIT2INT (lit)));

      assign_decision (ps, lit);
      old_trail_count = ps->thead - ps->trail;
      flbcp (ps);

      if (ps->conflict)
	{
EXPLICITLY_FAILED_LITERAL:
	  LOG ( fprintf (ps->out, "%sfound explicitly failed literal %d\n",
		ps->prefix, LIT2INT (lit)));

	  ps->failedlits++;
	  ps->efailedlits++;

	  backtrack (ps);
	  flbcp (ps);

	  if (!ps->conflict)
	    continue;

CONTRADICTION:
	  assert (!ps->LEVEL);
	  backtrack (ps);
	  assert (ps->mtcls);

	  goto RETURN;
	}

      if (ps->propagations >= limit)
	{
	  undo (ps, 0);
	  break;
	}

      lit = NOTLIT (lit);

      if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
	{
#ifdef STATS
	  ps->flskipped++;
#endif
	  undo (ps, 0);
	  continue;
	}

#ifdef STATS
      ps->fltried++;
#endif
      LOG ( fprintf (ps->out, "%strying %d as failed literals\n",
	    ps->prefix, LIT2INT (lit)));

      new_trail_count = ps->thead - ps->trail;
      saved_count = new_trail_count - old_trail_count;

      if (saved_count > ps->saved_size)
	{
	  new_saved_size = ps->saved_size ? 2 * ps->saved_size : 1;
	  while (saved_count > new_saved_size)
	    new_saved_size *= 2;

	  RESIZEN (ps->saved, ps->saved_size, new_saved_size);
	  ps->saved_size = new_saved_size;
	}

      for (j = 0; j < saved_count; j++)
	ps->saved[j] = ps->trail[old_trail_count + j];

      undo (ps, 0);

      assign_decision (ps, lit);
      flbcp (ps);

      if (ps->conflict)
	goto EXPLICITLY_FAILED_LITERAL;

      pivot = (ps->thead - ps->trail <= new_trail_count) ? lit : NOTLIT (lit);

      common = 0;
      for (j = 0; j < saved_count; j++)
	if ((other = ps->saved[j])->val == TRUE)
	  ps->saved[common++] = other;

      undo (ps, 0);

      LOG (if (common)
	     fprintf (ps->out, 
		      "%sfound %d literals implied by %d and %d\n",
		      ps->prefix, common, 
		      LIT2INT (NOTLIT (lit)), LIT2INT (lit)));

#if 1 // set to zero to disable 'lifting'
      for (j = 0; 
	   j < common 
	  /* TODO: For some Velev benchmarks, extracting the common implicit
	   * failed literals took quite some time.  This needs to be fixed by
	   * a dedicated analyzer.  Up to then we bound the number of
	   * propagations in this loop as well.
	   */
	   && ps->propagations < limit + delta
	   ; j++)
	{
	  other = ps->saved[j];

	  if (other->val == TRUE)
	    continue;

	  assert (!other->val);

	  LOG ( fprintf (ps->out, 
			"%sforcing %d as forced implicitly failed literal\n",
			ps->prefix, LIT2INT (other)));

	  assert (pivot != NOTLIT (other));
	  assert (pivot != other);

	  assign_decision (ps, NOTLIT (other));
	  flbcp (ps);

	  assert (ps->LEVEL == 1);

	  if (ps->conflict)
	    {
	      backtrack (ps);
	      assert (!ps->LEVEL);
	    }
	  else
	    {
	      assign_decision (ps, pivot);
	      flbcp (ps);

	      backtrack (ps);

	      if (ps->LEVEL)
		{
		  assert (ps->LEVEL == 1);

		  flbcp (ps);

		  if (ps->conflict)
		    {
		      backtrack (ps);
		      assert (!ps->LEVEL);
		    }
		  else
		    {
		      assign_decision (ps, NOTLIT (pivot));
		      flbcp (ps);
		      backtrack (ps);

		      if (ps->LEVEL)
			{
			  assert (ps->LEVEL == 1);
			  flbcp (ps);

			  if (!ps->conflict)
			    {
#ifdef STATS
			      ps->floopsed++;
#endif
			      undo (ps, 0);
			      continue;
			    }

			  backtrack (ps);
			}

		      assert (!ps->LEVEL);
		    }

		  assert (!ps->LEVEL);
		}
	    }
	  assert (!ps->LEVEL);
	  flbcp (ps);

	  ps->failedlits++;
	  ps->ifailedlits++;

	  if (ps->conflict)
	    goto CONTRADICTION;
	}
#endif
    }

  ps->fllimit += 9 * (ps->propagations - ps->fllimit);	/* 10% for failed literals */

RETURN:

  /* First flush top level assigned literals.  Those are prohibited from
   * being pushed up the heap during 'faillits' since 'simplifying' is set.
   */
  assert (ps->heap < ps->hhead);
  for (p = q = ps->heap + 1; p < ps->hhead; p++)
    {
      r = *p;
      lit = RNK2LIT (r);
      if (lit->val)
       	r->pos = 0;
      else
	*q++ = r;
    }

  /* Then resort with respect to EVSIDS score and fix positions.
   */
  SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
  for (p = ps->heap + 1; p < ps->hhead; p++)
    (*p)->pos = p - ps->heap;

  sflush (ps);
  ps->flseconds += ps->seconds - started;
}

#endif

static void
simplify (PS * ps, int forced)
{
  Lit * lit, * notlit, ** t;
  unsigned collect, delta;
#ifdef STATS
  size_t bytes_collected;
#endif
  int * q, ilit;
  Cls **p, *c;
  Var * v;

#ifndef NDEDBUG
  (void) forced;
#endif

  assert (!ps->mtcls);
  assert (!satisfied (ps));
  assert (forced || ps->lsimplify <= ps->propagations);
  assert (forced || ps->fsimplify <= ps->fixed);

  if (ps->LEVEL)
    undo (ps, 0);
#ifndef NFL
  ps->simplifying = 1;
  faillits (ps);
  ps->simplifying = 0;

  if (ps->mtcls)
    return;
#endif

  if (ps->cils != ps->cilshead)
    {
      assert (ps->ttail == ps->thead);
      assert (ps->ttail2 == ps->thead);
      ps->ttail = ps->trail;
      for (t = ps->trail; t < ps->thead; t++)
	{
	  lit = *t;
	  v = LIT2VAR (lit);
	  if (v->internal)
	    {
	      assert (LIT2INT (lit) < 0);
	      assert (lit->val == TRUE);
	      unassign (ps, lit);
	    }
	  else
	    *ps->ttail++ = lit;
	}
      ps->ttail2 = ps->thead = ps->ttail;

      for (q = ps->cils; q != ps->cilshead; q++)
	{
	  ilit = *q;
	  assert (0 < ilit && ilit <= (int) ps->max_var);
	  v = ps->vars + ilit;
	  assert (v->internal);
	  v->level = 0;
	  v->reason = 0;
	  lit = int2lit (ps, -ilit);
	  assert (lit->val == UNDEF);
	  lit->val = TRUE;
	  notlit = NOTLIT (lit);
	  assert (notlit->val == UNDEF);
	  notlit->val = FALSE;
	}
    }

  collect = 0;
  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;
      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif

      if (c->locked)
	continue;
      
      assert (!c->collect);
      if (clause_is_toplevel_satisfied (ps, c))
	{
	  mark_clause_to_be_collected (c);
	  collect++;
	}
    }

  LOG ( fprintf (ps->out, "%scollecting %d clauses\n", ps->prefix, collect));
#ifdef STATS
  bytes_collected = 
#endif
  collect_clauses (ps);
#ifdef STATS
  ps->srecycled += bytes_collected;
#endif

  if (ps->cils != ps->cilshead)
    {
      for (q = ps->cils; q != ps->cilshead; q++)
	{
	  ilit = *q;
	  assert (0 < ilit && ilit <= (int) ps->max_var);
	  assert (ps->vars[ilit].internal);
	  if (ps->rilshead == ps->eorils)
	    ENLARGE (ps->rils, ps->rilshead, ps->eorils);
	  *ps->rilshead++ = ilit;
	  lit = int2lit (ps, -ilit);
	  assert (lit->val == TRUE);
	  lit->val = UNDEF;
	  notlit = NOTLIT (lit);
	  assert (notlit->val == FALSE);
	  notlit->val = UNDEF;
	}
      ps->cilshead = ps->cils;
    }

  delta = 10 * (ps->olits + ps->llits) + 100000;
  if (delta > 2000000)
    delta = 2000000;
  ps->lsimplify = ps->propagations + delta;
  ps->fsimplify = ps->fixed;
  ps->simps++;

  report (ps, 1, 's');
}

static void
iteration (PS * ps)
{
  assert (!ps->LEVEL);
  assert (bcp_queue_is_empty (ps));
  assert (ps->isimplify < ps->fixed);

  ps->iterations++;
  report (ps, 2, 'i');
#ifdef NLUBY
  ps->drestart = MINRESTART;
  ps->lrestart = ps->conflicts + ps->drestart;
#else
  init_restart (ps);
#endif
  ps->isimplify = ps->fixed;
}

static int
cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
{
  Act a, b, * p, * q;

  (void) ps;

  assert (c->learned);
  assert (d->learned);

  if (c->glue < d->glue)		// smaller glue preferred
    return 1;

  if (c->glue > d->glue)
    return -1;

  p = CLS2ACT (c);
  q = CLS2ACT (d);
  a = *p;
  b = *q;

  if (a < b)				// then higher activity
    return -1;

  if (b < a)
    return 1;

  if (c->size < d->size)		// then smaller size
    return 1;

  if (c->size > d->size)
    return -1;

  return 0;
}

static void
reduce (PS * ps, unsigned percentage)
{
  unsigned redcount, lcollect, collect, target;
#ifdef STATS
  size_t bytes_collected;
#endif
  Cls **p, *c;

  assert (ps->rhead == ps->resolved);

  ps->lastreduceconflicts = ps->conflicts;

  assert (percentage <= 100);
  LOG ( fprintf (ps->out, 
                "%sreducing %u%% learned clauses\n",
		ps->prefix, percentage));

  while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved))
    ENLARGE (ps->resolved, ps->rhead, ps->eor);

  collect = 0;
  lcollect = 0;

  for (p = ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p != EOC; p = NXC (p))
    {
      c = *p;
      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif

      if (c->locked)
	continue;

      assert (!c->collect);
      if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c))
	{
	  mark_clause_to_be_collected (c);
	  collect++;

	  if (c->learned && c->size > 2)
	    lcollect++;

	  continue;
	}

      if (!c->learned)
	continue;

      if (c->size <= 2)
	continue;

      assert (ps->rhead < ps->eor);
      *ps->rhead++ = c;
    }
  assert (ps->rhead <= ps->eor);

  ps->fsimplify = ps->fixed;

  redcount = ps->rhead - ps->resolved;
  SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount);

  assert (ps->nlclauses >= lcollect);
  target = ps->nlclauses - lcollect + 1;

  target = (percentage * target + 99) / 100;

  if (target >= redcount)
    target = redcount;

  ps->rhead = ps->resolved + target;
  while (ps->rhead > ps->resolved)
    {
      c = *--ps->rhead;
      mark_clause_to_be_collected (c);

      collect++;
      if (c->learned && c->size > 2)	/* just for consistency */
	lcollect++;
    }

  if (collect)
    {
      ps->reductions++;
#ifdef STATS
      bytes_collected = 
#endif
      collect_clauses (ps);
#ifdef STATS
      ps->rrecycled += bytes_collected;
#endif
      report (ps, 2, '-');
    }

  if (!lcollect)
    inc_lreduce (ps);		/* avoid dead lock */

  assert (ps->rhead == ps->resolved);
}

static void
init_reduce (PS * ps)
{
  // lreduce = loadded / 2;
  ps->lreduce = 1000;

  if (ps->lreduce < 100)
    ps->lreduce = 100;

  if (ps->verbosity)
     fprintf (ps->out, 
             "%s\n%sinitial reduction limit %u clauses\n%s\n",
	     ps->prefix, ps->prefix, ps->lreduce, ps->prefix);
}

static unsigned
rng (PS * ps)
{
  unsigned res = ps->srng;
  ps->srng *= 1664525u;
  ps->srng += 1013904223u;
  NOLOG ( fprintf (ps->out, "%srng () = %u\n", ps->prefix, res));
  return res;
}

static unsigned
rrng (PS * ps, unsigned low, unsigned high)
{
  unsigned long long tmp;
  unsigned res, elements;
  assert (low <= high);
  elements = high - low + 1;
  tmp = rng (ps);
  tmp *= elements;
  tmp >>= 32;
  tmp += low;
  res = tmp;
  NOLOG ( fprintf (ps->out, "%srrng (ps, %u, %u) = %u\n", ps->prefix, low, high, res));
  assert (low <= res);
  assert (res <= high);
  return res;
}

static Lit *
decide_phase (PS * ps, Lit * lit)
{
  Lit * not_lit = NOTLIT (lit);
  Var *v = LIT2VAR (lit);

  assert (LIT2SGN (lit) > 0);
  if (v->usedefphase)
    {
      if (v->defphase)
	{
	  /* assign to TRUE */
	}
      else
	{
	  /* assign to FALSE */
	  lit = not_lit;
	}
    }
  else if (!v->assigned)
    {
#ifdef STATS
      ps->staticphasedecisions++;
#endif
      if (GLOBAL_DEFAULT_PHASE == POSPHASE)
	{
	  /* assign to TRUE */
	}
      else if (GLOBAL_DEFAULT_PHASE == NEGPHASE)
	{
	  /* assign to FALSE */
	  lit = not_lit;
	}
      else if (GLOBAL_DEFAULT_PHASE == RNDPHASE)
	{
	  /* randomly assign default phase */
	  if (rrng (ps, 1, 2) != 2)
	    lit = not_lit;
	}
      else if (*LIT2JWH(lit) <= *LIT2JWH (not_lit))
	{
	  /* assign to FALSE (Jeroslow-Wang says there are more short
	   * clauses with negative occurence of this variable, so satisfy
	   * those, to minimize BCP) 
	   */
	  lit = not_lit;
	}
      else
	{
	  /* assign to TRUE (... but strictly more positive occurrences) */
	}
    }
  else 
    {
      /* repeat last phase: phase saving heuristic */

      if (v->phase)
	{
	  /* assign to TRUE (last phase was TRUE as well) */
	}
      else
	{
	  /* assign to FALSE (last phase was FALSE as well) */
	  lit = not_lit;
	}
    }

  return lit;
}

static unsigned
gcd (unsigned a, unsigned b)
{
  unsigned tmp;

  assert (a);
  assert (b);

  if (a < b)
    {
      tmp = a;
      a = b;
      b = tmp;
    }

  while (b)
    {
      assert (a >= b);
      tmp = b;
      b = a % b;
      a = tmp;
    }

  return a;
}

static Lit *
rdecide (PS * ps)
{
  unsigned idx, delta, spread;
  Lit * res;

  spread = RDECIDE;
  if (rrng (ps, 1, spread) != 2)
    return 0;

  assert (1 <= ps->max_var);
  idx = rrng (ps, 1, ps->max_var);
  res = int2lit (ps, idx);

  if (res->val != UNDEF)
    {
      delta = rrng (ps, 1, ps->max_var);
      while (gcd (delta, ps->max_var) != 1)
	delta--;

      assert (1 <= delta);
      assert (delta <= ps->max_var);

      do {
	idx += delta;
	if (idx > ps->max_var)
	  idx -= ps->max_var;
	res = int2lit (ps, idx);
      } while (res->val != UNDEF);
    }

#ifdef STATS
  ps->rdecisions++;
#endif
  res = decide_phase (ps, res);
  LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res)));

  return res;
}

static Lit *
sdecide (PS * ps)
{
  Lit *res;
  Rnk *r;

  for (;;)
    {
      r = htop (ps);
      res = RNK2LIT (r);
      if (res->val == UNDEF) break;
      (void) hpop (ps);
      NOLOG ( fprintf (ps->out, 
                      "%shpop %u %u %u\n",
		      ps->prefix, r - ps->rnks,
		      FLTMANTISSA(r->score),
		      FLTEXPONENT(r->score)));
    }

#ifdef STATS
  ps->sdecisions++;
#endif
  res = decide_phase (ps, res);

  LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res)));

  return res;
}

static Lit *
adecide (PS * ps)
{
  Lit *lit;
  Var * v;

  assert (ps->als < ps->alshead);
  assert (!ps->failed_assumption);

  while (ps->alstail < ps->alshead)
    {
      lit = *ps->alstail++;

      if (lit->val == FALSE)
	{
	  ps->failed_assumption = lit;
	  v = LIT2VAR (lit);

	  use_var (ps, v);

	  LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n",
			ps->prefix, LIT2INT (ps->failed_assumption)));
	  fanalyze (ps);
	  return 0;
	}

      if (lit->val == TRUE)
	{
	  v = LIT2VAR (lit);
	  if (v->level > ps->adecidelevel)
	    ps->adecidelevel = v->level;
	  continue;
	}

#ifdef STATS
      ps->assumptions++;
#endif
      LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit)));
      ps->adecidelevel = ps->LEVEL + 1;

      return lit;
    }

  return 0;
}

static void
decide (PS * ps)
{
  Lit * lit;

  assert (!satisfied (ps));
  assert (!ps->conflict);

  if (ps->alstail < ps->alshead && (lit = adecide (ps)))
    ;
  else if (ps->failed_assumption)
    return;
  else if (satisfied (ps))
    return;
  else if (!(lit = rdecide (ps)))
    lit = sdecide (ps);

  assert (lit);
  assign_decision (ps, lit);

  ps->levelsum += ps->LEVEL;
  ps->decisions++;
}

static int
sat (PS * ps, int l)
{
  int count = 0, backtracked;

  if (!ps->conflict)
    bcp (ps);

  if (ps->conflict)
    backtrack (ps);

  if (ps->mtcls)
    return PICOSAT_UNSATISFIABLE;

  if (satisfied (ps))
    goto SATISFIED;

  if (ps->lsimplify <= ps->propagations)
    simplify (ps, 0);

  if (ps->mtcls)
    return PICOSAT_UNSATISFIABLE;

  if (satisfied (ps))
    goto SATISFIED;

  init_restart (ps);

  if (!ps->lreduce)
    init_reduce (ps);

  ps->isimplify = ps->fixed;
  backtracked = 0;

  for (;;)
    {
      if (!ps->conflict)
	bcp (ps);

      if (ps->conflict)
	{
	  incincs (ps);
	  backtrack (ps);

	  if (ps->mtcls)
	    return PICOSAT_UNSATISFIABLE;
	  backtracked = 1;
	  continue;
	}

      if (satisfied (ps))
	{
SATISFIED:
#ifndef NDEBUG
	  original_clauses_satisfied (ps);
	  assumptions_satisfied (ps);
#endif
	  return PICOSAT_SATISFIABLE;
	}

      if (backtracked)
	{
	  backtracked = 0;
	  if (!ps->LEVEL && ps->isimplify < ps->fixed)
	    iteration (ps);
	}

      if (l >= 0 && count >= l)		/* decision limit reached ? */
	return PICOSAT_UNKNOWN;

      if (ps->interrupt.function &&		/* external interrupt */
	  count > 0 && !(count % INTERRUPTLIM) &&
	  ps->interrupt.function (ps->interrupt.state))
	return PICOSAT_UNKNOWN;

      if (ps->propagations >= ps->lpropagations)/* propagation limit reached ? */
	return PICOSAT_UNKNOWN;

#ifndef NADC
      if (!ps->adodisabled && ps->adoconflicts >= ps->adoconflictlimit)
	{
	  assert (bcp_queue_is_empty (ps));
	  return PICOSAT_UNKNOWN;
	}
#endif

      if (ps->fsimplify < ps->fixed && ps->lsimplify <= ps->propagations)
	{
	  simplify (ps, 0);
	  if (!bcp_queue_is_empty (ps))
	    continue;
#ifndef NFL
	  if (ps->mtcls)
	    return PICOSAT_UNSATISFIABLE;

	  if (satisfied (ps))
	    return PICOSAT_SATISFIABLE;

	  assert (!ps->LEVEL);
#endif
	}

      if (need_to_reduce (ps))
	reduce (ps, 50);

      if (ps->conflicts >= ps->lrestart && ps->LEVEL > 2)
	restart (ps);

      decide (ps);
      if (ps->failed_assumption)
	return PICOSAT_UNSATISFIABLE;
      count++;
    }
}

static void
rebias (PS * ps)
{
  Cls ** p, * c;
  Var * v;

  for (v = ps->vars + 1; v <= ps->vars + ps->max_var; v++)
    v->assigned = 0;

  memset (ps->jwh, 0, 2 * (ps->max_var + 1) * sizeof *ps->jwh);

  for (p = ps->oclauses; p < ps->ohead; p++) 
    {
      c = *p;

      if (!c) 
	continue;

      if (c->learned)
	continue;

      incjwh (ps, c);
    }
}

#ifdef TRACE

static unsigned
core (PS * ps)
{
  unsigned idx, prev, this, delta, i, lcore, vcore;
  unsigned *stack, *shead, *eos;
  Lit **q, **eol, *lit;
  Cls *c, *reason;
  Znt *p, byte;
  Zhn *zhain;
  Var *v;

  assert (ps->trace);

  assert (ps->mtcls || ps->failed_assumption);
  if (ps->ocore >= 0)
    return ps->ocore;

  lcore = ps->ocore = vcore = 0;

  stack = shead = eos = 0;
  ENLARGE (stack, shead, eos);

  if (ps->mtcls)
    {
      idx = CLS2IDX (ps->mtcls);
      *shead++ = idx;
    }
  else
    {
      assert (ps->failed_assumption);
      v = LIT2VAR (ps->failed_assumption);
      reason = v->reason;
      assert (reason);
      idx = CLS2IDX (reason);
      *shead++ = idx;
    }

  while (shead > stack)
    {
      idx = *--shead;
      zhain = IDX2ZHN (idx);

      if (zhain)
	{
	  if (zhain->core)
	    continue;

	  zhain->core = 1;
	  lcore++;

	  c = IDX2CLS (idx);
	  if (c)
	    {
	      assert (!c->core);
	      c->core = 1;
	    }

	  i = 0;
	  delta = 0;
	  prev = 0;
	  for (p = zhain->znt; (byte = *p); p++, i += 7)
	    {
	      delta |= (byte & 0x7f) << i;
	      if (byte & 0x80)
		continue;

	      this = prev + delta;
	      assert (prev < this);	/* no overflow */

	      if (shead == eos)
		ENLARGE (stack, shead, eos);
	      *shead++ = this;

	      prev = this;
	      delta = 0;
	      i = -7;
	    }
	}
      else
	{
	  c = IDX2CLS (idx);

	  assert (c);
	  assert (!c->learned);

	  if (c->core)
	    continue;

	  c->core = 1;
	  ps->ocore++;

	  eol = end_of_lits (c);
	  for (q = c->lits; q < eol; q++)
	    {
	      lit = *q;
	      v = LIT2VAR (lit);
	      if (v->core)
		continue;

	      v->core = 1;
	      vcore++;

	      if (!ps->failed_assumption) continue;
	      if (lit != ps->failed_assumption) continue;

	      reason = v->reason;
	      if (!reason) continue;
	      if (reason->core) continue;

	      idx = CLS2IDX (reason);
	      if (shead == eos)
		ENLARGE (stack, shead, eos);
	      *shead++ = idx;
	    }
	}
    }

  DELETEN (stack, eos - stack);

  if (ps->verbosity)
     fprintf (ps->out,
	     "%s%u core variables out of %u (%.1f%%)\n"
	     "%s%u core original clauses out of %u (%.1f%%)\n"
	     "%s%u core learned clauses out of %u (%.1f%%)\n",
	     ps->prefix, vcore, ps->max_var, PERCENT (vcore, ps->max_var),
	     ps->prefix, ps->ocore, ps->oadded, PERCENT (ps->ocore, ps->oadded),
	     ps->prefix, lcore, ps->ladded, PERCENT (lcore, ps->ladded));

  return ps->ocore;
}

static void
trace_lits (PS * ps, Cls * c, FILE * file)
{
  Lit **p, **eol = end_of_lits (c);

  assert (c);
  assert (c->core);

  for (p = c->lits; p < eol; p++)
    fprintf (file, "%d ", LIT2INT (*p));

  fputc ('0', file);
}

static void
write_idx (PS * ps, unsigned idx, FILE * file)
{
  fprintf (file, "%ld", EXPORTIDX (idx));
}

static void
trace_clause (PS * ps, unsigned idx, Cls * c, FILE * file, int fmt)
{
  assert (c);
  assert (c->core);
  assert (fmt == RUP_TRACE_FMT || !c->learned);
  assert (CLS2IDX (c) == idx);

  if (fmt != RUP_TRACE_FMT)
    {
      write_idx (ps, idx, file);
      fputc (' ', file);
    }

  trace_lits (ps, c, file);

  if (fmt != RUP_TRACE_FMT)
    fputs (" 0", file);

  fputc ('\n', file);
}

static void
trace_zhain (PS * ps, unsigned idx, Zhn * zhain, FILE * file, int fmt)
{
  unsigned prev, this, delta, i;
  Znt *p, byte;
  Cls * c;

  assert (zhain);
  assert (zhain->core);

  write_idx (ps, idx, file);
  fputc (' ', file);

  if (fmt == EXTENDED_TRACECHECK_TRACE_FMT)
    {
      c = IDX2CLS (idx);
      assert (c);
      trace_lits (ps, c, file);
    }
  else
    {
      assert (fmt == COMPACT_TRACECHECK_TRACE_FMT);
      putc ('*', file);
    }

  i = 0;
  delta = 0;
  prev = 0;

  for (p = zhain->znt; (byte = *p); p++, i += 7)
    {
      delta |= (byte & 0x7f) << i;
      if (byte & 0x80)
	continue;

      this = prev + delta;

      putc (' ', file);
      write_idx (ps, this, file);

      prev = this;
      delta = 0;
      i = -7;
    }

  fputs (" 0\n", file);
}

static void
write_core (PS * ps, FILE * file)
{
  Lit **q, **eol;
  Cls **p, *c;

  fprintf (file, "p cnf %u %u\n", ps->max_var, core (ps));

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;

      if (!c || c->learned || !c->core)
	continue;

      eol = end_of_lits (c);
      for (q = c->lits; q < eol; q++)
	fprintf (file, "%d ", LIT2INT (*q));

      fputs ("0\n", file);
    }
}

#endif

static void
write_trace (PS * ps, FILE * file, int fmt)
{
#ifdef TRACE
  Cls *c, ** p;
  Zhn *zhain;
  unsigned i;

  core (ps);

  if (fmt == RUP_TRACE_FMT)
    {
      ps->rupvariables = picosat_variables (ps),
      ps->rupclauses = picosat_added_original_clauses (ps);
      write_rup_header (ps, file);
    }

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;

      if (ps->oclauses <= p && p < ps->eoo)
	{
	  i = OIDX2IDX (p - ps->oclauses);
	  assert (!c || CLS2IDX (c) == i);
	}
      else
	{
          assert (ps->lclauses <= p && p < ps->EOL);
	  i = LIDX2IDX (p - ps->lclauses);
	}

      zhain = IDX2ZHN (i);

      if (zhain)
	{
	  if (zhain->core)
	    {
	      if (fmt == RUP_TRACE_FMT)
		trace_clause (ps,i, c, file, fmt);
	      else
		trace_zhain (ps, i, zhain, file, fmt);
	    }
	}
      else if (c)
	{
	  if (fmt != RUP_TRACE_FMT && c)
	    {
	      if (c->core)
		trace_clause (ps, i, c, file, fmt);
	    }
	}
    }
#else
  (void) file;
  (void) fmt;
  (void) ps;
#endif
}

static void
write_core_wrapper (PS * ps, FILE * file, int fmt)
{
  (void) fmt;
#ifdef TRACE
  write_core (ps, file);
#else
  (void) ps;
  (void) file;
#endif
}

static Lit *
import_lit (PS * ps, int lit, int nointernal)
{
  Lit * res;
  Var * v;

  ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal");
  ABORTIF (abs (lit) > (int) ps->max_var && ps->CLS != ps->clshead,
           "API usage: new variable index after 'picosat_push'");

  if (abs (lit) <= (int) ps->max_var)
    {
      res = int2lit (ps, lit);
      v = LIT2VAR (res);
      if (nointernal && v->internal)
	ABORT ("API usage: trying to import invalid literal");
      else if (!nointernal && !v->internal)
	ABORT ("API usage: trying to import invalid context");
    }
  else
    {
      while (abs (lit) > (int) ps->max_var)
	inc_max_var (ps);
      res = int2lit (ps, lit);
    }

  return res;
}

#ifdef TRACE
static void
reset_core (PS * ps)
{
  Cls ** p, * c;
  Zhn ** q, * z;
  unsigned i;

  for (i = 1; i <= ps->max_var; i++)
    ps->vars[i].core = 0;

  for (p = SOC; p != EOC; p = NXC (p))
    if ((c = *p))
      c->core = 0;

  for (q = ps->zhains; q != ps->zhead; q++)
    if ((z = *q))
      z->core = 0;

  ps->ocore = -1;
}
#endif

static void
reset_assumptions (PS * ps)
{
  Lit ** p;

  ps->failed_assumption = 0;

  if (ps->extracted_all_failed_assumptions)
    {
      for (p = ps->als; p < ps->alshead; p++)
	LIT2VAR (*p)->failed = 0;

      ps->extracted_all_failed_assumptions = 0;
    }

  ps->alstail = ps->alshead = ps->als;
  ps->adecidelevel = 0;
}

static void
check_ready (PS * ps)
{
  ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized");
}

static void
check_sat_state (PS * ps)
{
  ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state");
}

static void
check_unsat_state (PS * ps)
{
  ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state");
}

static void
check_sat_or_unsat_or_unknown_state (PS * ps)
{
  ABORTIF (ps->state != SAT && ps->state != UNSAT && ps->state != UNKNOWN,
           "API usage: expected to be in SAT, UNSAT, or UNKNOWN state");
}

static void
reset_partial (PS * ps)
{
  unsigned idx;
  if (!ps->partial)
    return;
  for (idx = 1; idx <= ps->max_var; idx++)
    ps->vars[idx].partial = 0;
  ps->partial = 0;
}

static void
reset_incremental_usage (PS * ps)
{
  unsigned num_non_false;
  Lit * lit, ** q;

  check_sat_or_unsat_or_unknown_state (ps);

  LOG ( fprintf (ps->out, "%sRESET incremental usage\n", ps->prefix));

  if (ps->LEVEL)
    undo (ps, 0);

  reset_assumptions (ps);

  if (ps->conflict)
    { 
      num_non_false = 0;
      for (q = ps->conflict->lits; q < end_of_lits (ps->conflict); q++)
	{
	  lit = *q;
	  if (lit->val != FALSE)
	    num_non_false++;
	}

      // assert (num_non_false >= 2); // TODO: why this assertion?
#ifdef NO_BINARY_CLAUSES
      if (ps->conflict == &ps->cimpl)
	resetcimpl (ps);
#endif
#ifndef NADC
      if (ps->conflict == ps->adoconflict)
	resetadoconflict (ps);
#endif
      ps->conflict = 0;
    }

#ifdef TRACE
  reset_core (ps);
#endif

  reset_partial (ps);

  ps->saved_flips = ps->flips;
  ps->min_flipped = UINT_MAX;
  ps->saved_max_var = ps->max_var;

  ps->state = READY;
}

static void
enter (PS * ps)
{
  if (ps->nentered++)
    return;

  check_ready (ps);
  ps->entered = picosat_time_stamp ();
}

static void
leave (PS * ps)
{
  assert (ps->nentered);
  if (--ps->nentered)
    return;

  sflush (ps);
}

static void
check_trace_support_and_execute (PS * ps,
                                 FILE * file, 
				 void (*f)(PS*,FILE*,int), int fmt)
{
  check_ready (ps);
  check_unsat_state (ps);
#ifdef TRACE
  ABORTIF (!ps->trace, "API usage: tracing disabled");
  enter (ps);
  f (ps, file, fmt);
  leave (ps);
#else
  (void) file;
  (void) fmt;
  (void) f;
  ABORT ("compiled without trace support");
#endif
}

static void
extract_all_failed_assumptions (PS * ps)
{
  Lit ** p, ** eol;
  Var * v, * u;
  int pos;
  Cls * c;

  assert (!ps->extracted_all_failed_assumptions);

  assert (ps->failed_assumption);
  assert (ps->mhead == ps->marked);

  if (ps->marked == ps->eom)
    ENLARGE (ps->marked, ps->mhead, ps->eom);

  v = LIT2VAR (ps->failed_assumption);
  mark_var (ps, v);
  pos = 0;

  while (pos < ps->mhead - ps->marked)
    {
      v = ps->marked[pos++];
      assert (v->mark);
      c = var2reason (ps, v);
      if (!c)
	continue;
      eol = end_of_lits (c);
      for (p = c->lits; p < eol; p++)
	{
	  u = LIT2VAR (*p);
	  if (!u->mark)
	    mark_var (ps, u);
	}
#ifdef NO_BINARY_CLAUSES
      if (c == &ps->impl)
	resetimpl (ps);
#endif
    }

  for (p = ps->als; p < ps->alshead; p++)
    {
      u = LIT2VAR (*p);
      if (!u->mark) continue;
      u->failed = 1;
      LOG ( fprintf (ps->out,
                     "%sfailed assumption %d\n",
		     ps->prefix, LIT2INT (*p)));
    }

  while (ps->mhead > ps->marked)
    (*--ps->mhead)->mark = 0;

  ps->extracted_all_failed_assumptions = 1;
}

const char *
picosat_copyright (void)
{
  return "Copyright (c) 2006 - 2014 Armin Biere JKU Linz";
}

PicoSAT *
picosat_init (void)
{
  return init (0, 0, 0, 0);
}

PicoSAT * 
picosat_minit (void * pmgr,
	       picosat_malloc pnew,
	       picosat_realloc presize,
	       picosat_free pfree)
{
  ABORTIF (!pnew, "API usage: zero 'picosat_malloc' argument");
  ABORTIF (!presize, "API usage: zero 'picosat_realloc' argument");
  ABORTIF (!pfree, "API usage: zero 'picosat_free' argument");
  return init (pmgr, pnew, presize, pfree);
}


void
picosat_adjust (PS * ps, int new_max_var)
{
  unsigned new_size_vars;

  ABORTIF (abs (new_max_var) > (int) ps->max_var && ps->CLS != ps->clshead,
           "API usage: adjusting variable index after 'picosat_push'");
  enter (ps);

  new_max_var = abs (new_max_var);
  new_size_vars = new_max_var + 1;

  if (ps->size_vars < new_size_vars)
    enlarge (ps, new_size_vars);

  while (ps->max_var < (unsigned) new_max_var)
    inc_max_var (ps);

  leave (ps);
}

int
picosat_inc_max_var (PS * ps)
{
  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  inc_max_var (ps);

  if (ps->measurealltimeinlib)
    leave (ps);

  return ps->max_var;
}

int
picosat_context (PS * ps)
{
  return ps->clshead == ps->CLS ? 0 : LIT2INT (ps->clshead[-1]);
}

int
picosat_push (PS * ps)
{
  int res;
  Lit *lit;
  Var * v;

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  if (ps->state != READY)
    reset_incremental_usage (ps);

  if (ps->rils != ps->rilshead)
    {
      res = *--ps->rilshead;
      assert (ps->vars[res].internal);
    }
  else
    {
      inc_max_var (ps);
      res = ps->max_var;
      v = ps->vars + res;
      assert (!v->internal);
      v->internal = 1;
      ps->internals++;
      LOG ( fprintf (ps->out, "%snew internal variable index %d\n", ps->prefix, res));
    }

  lit = int2lit (ps, res);

  if (ps->clshead == ps->eocls)
    ENLARGE (ps->CLS, ps->clshead, ps->eocls);
  *ps->clshead++ = lit;

  ps->contexts++;

  LOG ( fprintf (ps->out, "%snew context %d at depth %ld after push\n",
                 ps->prefix, res, (long)(ps->clshead - ps->CLS)));

  if (ps->measurealltimeinlib)
    leave (ps);

  return res;
}

int 
picosat_pop (PS * ps)
{
  Lit * lit;
  int res;
  ABORTIF (ps->CLS == ps->clshead, "API usage: too many 'picosat_pop'");
  ABORTIF (ps->added != ps->ahead, "API usage: incomplete clause");

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  if (ps->state != READY)
    reset_incremental_usage (ps);

  assert (ps->CLS < ps->clshead);
  lit = *--ps->clshead;
  LOG ( fprintf (ps->out, "%sclosing context %d at depth %ld after pop\n",
                 ps->prefix, LIT2INT (lit), (long)(ps->clshead - ps->CLS) + 1));

  if (ps->cilshead == ps->eocils)
    ENLARGE (ps->cils, ps->cilshead, ps->eocils);
  *ps->cilshead++ = LIT2INT (lit);

  if (ps->cilshead - ps->cils > MAXCILS) {
    LOG ( fprintf (ps->out,
                  "%srecycling %ld interals with forced simplification\n",
		  ps->prefix, (long)(ps->cilshead - ps->cils)));
    simplify (ps, 1);
  }

  res = picosat_context (ps);
  if (res)
    LOG ( fprintf (ps->out, "%snew context %d at depth %ld after pop\n",
		   ps->prefix, res, (long)(ps->clshead - ps->CLS)));
  else
    LOG ( fprintf (ps->out, "%souter most context reached after pop\n", ps->prefix));

  if (ps->measurealltimeinlib)
    leave (ps);
  
  return res;
}

void
picosat_set_verbosity (PS * ps, int new_verbosity_level)
{
  check_ready (ps);
  ps->verbosity = new_verbosity_level;
}

void
picosat_set_plain (PS * ps, int new_plain_value)
{
  check_ready (ps);
  PLAIN = new_plain_value;
}

int
picosat_enable_trace_generation (PS * ps)
{
  int res = 0;
  check_ready (ps);
#ifdef TRACE
  ABORTIF (ps->addedclauses, 
           "API usage: trace generation enabled after adding clauses");
  res = ps->trace = 1;
#endif
  return res;
}

void
picosat_set_incremental_rup_file (PS * ps, FILE * rup_file, int m, int n)
{
  check_ready (ps);
  assert (!ps->rupstarted);
  ps->rupvariables = m;
  ps->rupclauses = n;
}

void
picosat_set_output (PS * ps, FILE * output_file)
{
  check_ready (ps);
  ps->out = output_file;
}

void
picosat_measure_all_calls (PS * ps)
{
  check_ready (ps);
  ps->measurealltimeinlib = 1;
}

void
picosat_set_prefix (PS * ps, const char * str)
{
  check_ready (ps);
  new_prefix (ps, str);
}

void
picosat_set_seed (PS * ps, unsigned s)
{
  check_ready (ps);
  ps->srng = s;
}

void
picosat_reset (PS * ps)
{
  check_ready (ps);
  reset (ps);
}

int
picosat_add (PS * ps, int int_lit)
{
  int res = ps->oadded;
  Lit *lit;

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  ABORTIF (INCREMENTAL_RUP_FILE && ps->rupstarted && ps->oadded >= (unsigned)ps->rupclauses,
           "API usage: adding too many clauses after RUP header written");
#ifndef NADC
  ABORTIF (ps->addingtoado, 
           "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
#endif
  if (ps->state != READY)
    reset_incremental_usage (ps);

  if (ps->saveorig)
    {
      if (ps->sohead == ps->eoso)
	ENLARGE (ps->soclauses, ps->sohead, ps->eoso);

      *ps->sohead++ = int_lit;
    }

  if (int_lit)
    {
      lit = import_lit (ps, int_lit, 1);
      add_lit (ps, lit);
    }
  else
    simplify_and_add_original_clause (ps);

  if (ps->measurealltimeinlib)
    leave (ps);

  return res;
}

int
picosat_add_arg (PS * ps, ...)
{
  int lit;
  va_list ap;
  va_start (ap, ps);
  while ((lit = va_arg (ap, int)))
    (void) picosat_add (ps, lit);
  va_end (ap);
  return picosat_add (ps, 0);
}

int
picosat_add_lits (PS * ps, int * lits)
{
  const int * p;
  int lit;
  for (p = lits; (lit = *p); p++)
    (void) picosat_add (ps, lit);
  return picosat_add (ps, 0);
}

void
picosat_add_ado_lit (PS * ps, int external_lit)
{
#ifndef NADC
  Lit * internal_lit;

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  if (ps->state != READY)
    reset_incremental_usage (ps);

  ABORTIF (!ps->addingtoado && ps->ahead > ps->added,
           "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");

  if (external_lit)
    {
      ps->addingtoado = 1;
      internal_lit = import_lit (ps, external_lit, 1);
      add_lit (ps, internal_lit);
    }
  else
    {
      ps->addingtoado = 0;
      add_ado (ps);
    }
  if (ps->measurealltimeinlib)
    leave (ps);
#else
  (void) ps;
  (void) external_lit;
  ABORT ("compiled without all different constraint support");
#endif
}

static void
assume (PS * ps, Lit * lit)
{
  if (ps->alshead == ps->eoals)
    {
      assert (ps->alstail == ps->als);
      ENLARGE (ps->als, ps->alshead, ps->eoals);
      ps->alstail = ps->als;
    }

  *ps->alshead++ = lit;
  LOG ( fprintf (ps->out, "%sassumption %d\n", ps->prefix, LIT2INT (lit)));
}

static void
assume_contexts (PS * ps)
{
  Lit ** p;
  if (ps->als != ps->alshead)
    return;
  for (p = ps->CLS; p != ps->clshead; p++)
    assume (ps, *p);
}

#ifndef RCODE
static const char * enumstr (int i) {
  int last = i % 10;
  if (last == 1) return "st";
  if (last == 2) return "nd";
  if (last == 3) return "rd";
  return "th";
}
#endif

static int
tderef (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;

  assert (abs (int_lit) <= (int) ps->max_var);

  lit = int2lit (ps, int_lit);

  v = LIT2VAR (lit);
  if (v->level > 0)
    return 0;

  if (lit->val == TRUE)
    return 1;

  if (lit->val == FALSE)
    return -1;

  return 0;
}

static int
pderef (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;

  assert (abs (int_lit) <= (int) ps->max_var);

  v = ps->vars + abs (int_lit);
  if (!v->partial)
    return 0;

  lit = int2lit (ps, int_lit);

  if (lit->val == TRUE)
    return 1;

  if (lit->val == FALSE)
    return -1;

  return 0;
}

static void
minautarky (PS * ps)
{
  unsigned * occs, maxoccs, tmpoccs, npartial;
  int * p, * c, lit, best, val;
#ifdef LOGGING
  int tl;
#endif

  assert (!ps->partial);

  npartial = 0;

  NEWN (occs, 2*ps->max_var + 1);
  CLRN (occs, 2*ps->max_var + 1);
  occs += ps->max_var;
  for (p = ps->soclauses; p < ps->sohead; p++)
    occs[*p]++;
  assert (occs[0] == ps->oadded);

  for (c = ps->soclauses; c < ps->sohead; c = p + 1) 
    {
#ifdef LOGGING
      tl = 0;
#endif
      best = 0; 
      maxoccs = 0;
      for (p = c; (lit = *p); p++)
	{
	  val = tderef (ps, lit);
	  if (val < 0)
	    continue;
	  if (val > 0)
	    {
#ifdef LOGGING
	      tl = 1;
#endif
	      best = lit;
	      maxoccs = occs[lit];
	    }

	  val = pderef (ps, lit);
	  if (val > 0)
	    break;
	  if (val < 0)
	    continue;
	  val = int2lit (ps, lit)->val;
	  assert (val);
	  if (val < 0)
	    continue;
	  tmpoccs = occs[lit];
	  if (best && tmpoccs <= maxoccs)
	    continue;
	  best = lit;
	  maxoccs = tmpoccs;
	}
      if (!lit)
	{
	  assert (best);
	  LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n", 
	       ps->prefix, best, maxoccs, tl ? " (top)" : ""));
	  ps->vars[abs (best)].partial = 1;
	  npartial++;
	}
      for (p = c; (lit = *p); p++)
	{
	  assert (occs[lit] > 0);
	  occs[lit]--;
	}
    }
  occs -= ps->max_var;
  DELETEN (occs, 2*ps->max_var + 1);
  ps->partial = 1;

  if (ps->verbosity)
     fprintf (ps->out,
      "%sautarky of size %u out of %u satisfying all clauses (%.1f%%)\n",
      ps->prefix, npartial, ps->max_var, PERCENT (npartial, ps->max_var));
}

void
picosat_assume (PS * ps, int int_lit)
{
  Lit *lit;

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  if (ps->state != READY)
    reset_incremental_usage (ps);

  assume_contexts (ps);
  lit = import_lit (ps, int_lit, 1);
  assume (ps, lit);

  if (ps->measurealltimeinlib)
    leave (ps);
}

int
picosat_sat (PS * ps, int l)
{
  int res;
  char ch;

  enter (ps);

  ps->calls++;
  LOG ( fprintf (ps->out, "%sSTART call %u\n", ps->prefix, ps->calls));

  if (ps->added < ps->ahead)
    {
#ifndef NADC
      if (ps->addingtoado)
	ABORT ("API usage: incomplete all different constraint");
      else
#endif
	ABORT ("API usage: incomplete clause");
    }

  if (ps->state != READY)
    reset_incremental_usage (ps);

  assume_contexts (ps);

  res = sat (ps, l);

  assert (ps->state == READY);

  switch (res)
    {
    case PICOSAT_UNSATISFIABLE:
      ch = '0';
      ps->state = UNSAT;
      break;
    case PICOSAT_SATISFIABLE:
      ch = '1';
      ps->state = SAT;
      break;
    default:
      ch = '?';
      ps->state = UNKNOWN;
      break;
    }

  if (ps->verbosity)
    {
      report (ps, 1, ch);
      rheader (ps);
    }

  leave (ps);
  LOG ( fprintf (ps->out, "%sEND call %u result %d\n", ps->prefix, ps->calls, res));

  ps->last_sat_call_result = res;

  return res;
}

int
picosat_res (PS * ps)
{
  return ps->last_sat_call_result;
}

int
picosat_deref (PS * ps, int int_lit)
{
  Lit *lit;

  check_ready (ps);
  check_sat_state (ps);
  ABORTIF (!int_lit, "API usage: can not deref zero literal");
  ABORTIF (ps->mtcls, "API usage: deref after empty clause generated");

#ifdef STATS
  ps->derefs++;
#endif

  if (abs (int_lit) > (int) ps->max_var)
    return 0;

  lit = int2lit (ps, int_lit);

  if (lit->val == TRUE)
    return 1;

  if (lit->val == FALSE)
    return -1;

  return 0;
}

int
picosat_deref_toplevel (PS * ps, int int_lit)
{
  check_ready (ps);
  ABORTIF (!int_lit, "API usage: can not deref zero literal");

#ifdef STATS
  ps->derefs++;
#endif
  if (abs (int_lit) > (int) ps->max_var)
    return 0;

  return tderef (ps, int_lit);
}

int
picosat_inconsistent (PS * ps)
{
  check_ready (ps);
  return ps->mtcls != 0;
}

int
picosat_corelit (PS * ps, int int_lit)
{
  check_ready (ps);
  check_unsat_state (ps);
  ABORTIF (!int_lit, "API usage: zero literal can not be in core");

  assert (ps->mtcls || ps->failed_assumption);

#ifdef TRACE
  {
    int res = 0;
    ABORTIF (!ps->trace, "tracing disabled");
    if (ps->measurealltimeinlib)
      enter (ps);
    core (ps);
    if (abs (int_lit) <= (int) ps->max_var)
      res = ps->vars[abs (int_lit)].core;
    assert (!res || ps->failed_assumption || ps->vars[abs (int_lit)].used);
    if (ps->measurealltimeinlib)
      leave (ps);
    return res;
  }
#else
  ABORT ("compiled without trace support");
  return 0;
#endif
}

int
picosat_coreclause (PS * ps, int ocls)
{
  check_ready (ps);
  check_unsat_state (ps);

  ABORTIF (ocls < 0, "API usage: negative original clause index");
  ABORTIF (ocls >= (int)ps->oadded, "API usage: original clause index exceeded");

  assert (ps->mtcls || ps->failed_assumption);

#ifdef TRACE
  {
    Cls ** clsptr, * c;
    int res  = 0;

    ABORTIF (!ps->trace, "tracing disabled");
    if (ps->measurealltimeinlib)
      enter (ps);
    core (ps);
    clsptr = ps->oclauses + ocls;
    assert (clsptr < ps->ohead);
    c = *clsptr;
    if (c) 
      res = c->core;
    if (ps->measurealltimeinlib)
      leave (ps);

    return res;
  }
#else
  ABORT ("compiled without trace support");
  return 0;
#endif
}

int
picosat_failed_assumption (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;
  ABORTIF (!int_lit, "API usage: zero literal as assumption");
  check_ready (ps);
  check_unsat_state (ps);
  if (ps->mtcls)
    return 0;
  assert (ps->failed_assumption);
  if (abs (int_lit) > (int) ps->max_var)
    return 0;
  if (!ps->extracted_all_failed_assumptions)
    extract_all_failed_assumptions (ps);
  lit = import_lit (ps, int_lit, 1);
  v = LIT2VAR (lit);
  return v->failed;
}

int
picosat_failed_context (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;
  ABORTIF (!int_lit, "API usage: zero literal as context");
  ABORTIF (abs (int_lit) > (int) ps->max_var, "API usage: invalid context");
  check_ready (ps);
  check_unsat_state (ps);
  assert (ps->failed_assumption);
  if (!ps->extracted_all_failed_assumptions)
    extract_all_failed_assumptions (ps);
  lit = import_lit (ps, int_lit, 0);
  v = LIT2VAR (lit);
  return v->failed;
}

const int *
picosat_failed_assumptions (PS * ps)
{
  Lit ** p, * lit;
  Var * v;
  int ilit;

  ps->falshead = ps->fals;
  check_ready (ps);
  check_unsat_state (ps);
  if (!ps->mtcls) 
    {
      assert (ps->failed_assumption);
      if (!ps->extracted_all_failed_assumptions)
	extract_all_failed_assumptions (ps);

      for (p = ps->als; p < ps->alshead; p++)
	{
	  lit = *p;
	  v = LIT2VAR (*p);
	  if (!v->failed)
	    continue;
	  ilit = LIT2INT (lit);
	  if (ps->falshead == ps->eofals)
	    ENLARGE (ps->fals, ps->falshead, ps->eofals);
	  *ps->falshead++ = ilit;
	}
    }
  if (ps->falshead == ps->eofals)
    ENLARGE (ps->fals, ps->falshead, ps->eofals);
  *ps->falshead++ = 0;
  return ps->fals;
}

const int *
picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fix)
{
  int i, j, ilit, len, nwork, * work, res;
  signed char * redundant;
  Lit ** p, * lit;
  int failed;
  Var * v;
#ifndef NDEBUG
  int oldlen;
#endif
#ifndef RCODE
  int norig = ps->alshead - ps->als; 
#endif

  check_ready (ps);
  check_unsat_state (ps);
  len = 0;
  if (!ps->mtcls) 
    {
      assert (ps->failed_assumption);
      if (!ps->extracted_all_failed_assumptions)
	extract_all_failed_assumptions (ps);

      for (p = ps->als; p < ps->alshead; p++)
	if (LIT2VAR (*p)->failed)
	  len++;
    }

  if (ps->mass)
    DELETEN (ps->mass, ps->szmass);
  ps->szmass = len + 1;
  NEWN (ps->mass, ps->szmass);

  i = 0;
  for (p = ps->als; p < ps->alshead; p++)
    {
      lit = *p;
      v = LIT2VAR (lit);
      if (!v->failed)
	continue;
      ilit = LIT2INT (lit);
      assert (i < len);
      ps->mass[i++] = ilit;
    }
  assert (i == len);
  ps->mass[i] = 0;
  if (ps->verbosity)
     fprintf (ps->out, 
      "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n",
      ps->prefix, len, norig, PERCENT (len, norig));
  if (cb)
    cb (s, ps->mass);

  nwork = len;
  NEWN (work, nwork);
  for (i = 0; i < len; i++)
    work[i] = ps->mass[i];

  NEWN (redundant, nwork);
  CLRN (redundant, nwork);

  for (i = 0; i < nwork; i++)
    {
      if (redundant[i])
	continue;

      if (ps->verbosity > 1)
	 fprintf (ps->out,
	         "%strying to drop %d%s assumption %d\n", 
		 ps->prefix, i, enumstr (i), work[i]);
      for (j = 0; j < nwork; j++)
	{
	  if (i == j) continue;
	  if (j < i && fix) continue;
	  if (redundant[j]) continue;
	  picosat_assume (ps, work[j]);
	}

      res = picosat_sat (ps, -1);
      if (res == 10)
	{
	  if (ps->verbosity > 1)
	     fprintf (ps->out,
		     "%sfailed to drop %d%s assumption %d\n", 
		     ps->prefix, i, enumstr (i), work[i]);

	  if (fix)
	    {
	      picosat_add (ps, work[i]);
	      picosat_add (ps, 0);
	    }
	}
      else
	{
	  assert (res == 20);
	  if (ps->verbosity > 1)
	     fprintf (ps->out,
		     "%ssuceeded to drop %d%s assumption %d\n", 
		     ps->prefix, i, enumstr (i), work[i]);
	  redundant[i] = 1;
	  for (j = 0; j < nwork; j++)
	    {
	      failed = picosat_failed_assumption (ps, work[j]);
	      if (j <= i) 
		{
		  assert ((j < i && fix) || redundant[j] == !failed);
		  continue;
		}

	      if (!failed)
		{
		  redundant[j] = -1;
		  if (ps->verbosity > 1)
		     fprintf (ps->out,
			     "%salso suceeded to drop %d%s assumption %d\n", 
			     ps->prefix, j, enumstr (j), work[j]);
		}
	    }

#ifndef NDEBUG
	    oldlen = len;
#endif
	    len = 0;
	    for (j = 0; j < nwork; j++)
	      if (!redundant[j])
		ps->mass[len++] = work[j];
	    ps->mass[len] = 0;
	    assert (len < oldlen);

	    if (fix)
	      {
		picosat_add (ps, -work[i]);
		picosat_add (ps, 0);
	      }

#ifndef NDEBUG
	    for (j = 0; j <= i; j++)
	      assert (redundant[j] >= 0);
#endif
	    for (j = i + 1; j < nwork; j++) 
	      {
		if (redundant[j] >= 0)
		  continue;

		if (fix)
		  {
		    picosat_add (ps, -work[j]);
		    picosat_add (ps, 0);
		  }

		redundant[j] = 1;
	      }

	    if (ps->verbosity)
	       fprintf (ps->out, 
	"%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n",
		ps->prefix, len, norig, PERCENT (len, norig));
	    if (cb)
	      cb (s, ps->mass);
	}
    }

  DELETEN (work, nwork);
  DELETEN (redundant, nwork);

  if (ps->verbosity)
    {
       fprintf (ps->out, "%sreinitializing unsat state\n", ps->prefix);
      fflush (ps->out);
    }

  for (i = 0; i < len; i++)
    picosat_assume (ps, ps->mass[i]);

#ifndef NDEBUG
  res = 
#endif
  picosat_sat (ps, -1);
  assert (res == 20);

  if (!ps->mtcls)
    {
      assert (!ps->extracted_all_failed_assumptions);
      extract_all_failed_assumptions (ps);
    }

  return ps->mass;
}

static const int *
mss (PS * ps, int * a, int size)
{
  int i, j, k, res;

  assert (!ps->mtcls);

  if (ps->szmssass)
    DELETEN (ps->mssass, ps->szmssass);

  ps->szmssass = 0;
  ps->mssass = 0;

  ps->szmssass = size + 1;
  NEWN (ps->mssass, ps->szmssass);

  LOG ( fprintf (ps->out, "%ssearch MSS over %d assumptions\n", ps->prefix, size));

  k = 0;
  for (i = k; i < size; i++)
    {
      for (j = 0; j < k; j++)
	picosat_assume (ps, ps->mssass[j]);

      LOG ( fprintf (ps->out, 
             "%strying to add assumption %d to MSS : %d\n", 
	     ps->prefix, i, a[i])); 

      picosat_assume (ps, a[i]);

      res = picosat_sat (ps, -1);
      if (res == 10)
	{
	  LOG ( fprintf (ps->out, 
		 "%sadding assumption %d to MSS : %d\n", ps->prefix, i, a[i])); 

	  ps->mssass[k++] = a[i];

	  for (j = i + 1; j < size; j++)
	    {
	      if (picosat_deref (ps, a[j]) <= 0)
		continue;

	      LOG ( fprintf (ps->out, 
		     "%salso adding assumption %d to MSS : %d\n", 
		     ps->prefix, j, a[j])); 

	      ps->mssass[k++] = a[j];

	      if (++i != j)
		{
		  int tmp = a[i];
		  a[i] = a[j];
		  a[j] = tmp;
		}
	    }
	}
      else
	{
	  assert (res == 20);

	  LOG ( fprintf (ps->out, 
		 "%signoring assumption %d in MSS : %d\n", ps->prefix, i, a[i])); 
	}
    }
  ps->mssass[k] = 0;
  LOG ( fprintf (ps->out, "%sfound MSS of size %d\n", ps->prefix, k));

  return ps->mssass;
}

static void
reassume (PS * ps, const int * a, int size)
{
  int i;
  LOG ( fprintf (ps->out, "%sreassuming all assumptions\n", ps->prefix));
  for (i = 0; i < size; i++)
    picosat_assume (ps, a[i]);
}

const int *
picosat_maximal_satisfiable_subset_of_assumptions (PS * ps)
{
  const int * res;
  int i, *a, size;

  ABORTIF (ps->mtcls,
           "API usage: CNF inconsistent (use 'picosat_inconsistent')");

  enter (ps);

  size = ps->alshead - ps->als;
  NEWN (a, size);

  for (i = 0; i < size; i++)
    a[i] = LIT2INT (ps->als[i]);

  res = mss (ps, a, size);
  reassume (ps, a, size);

  DELETEN (a, size);

  leave (ps);

  return res;
}

static void
check_mss_flags_clean (PS * ps)
{
#ifndef NDEBUG
  unsigned i;
  for (i = 1; i <= ps->max_var; i++)
    {
      assert (!ps->vars[i].msspos);
      assert (!ps->vars[i].mssneg);
    }
#else
  (void) ps;
#endif
}

static void
push_mcsass (PS * ps, int lit)
{
  if (ps->nmcsass == ps->szmcsass)
    {
      ps->szmcsass = ps->szmcsass ? 2*ps->szmcsass : 1;
      RESIZEN (ps->mcsass, ps->nmcsass, ps->szmcsass);
    }

  ps->mcsass[ps->nmcsass++] = lit;
}

static const int *
next_mss (PS * ps, int mcs)
{
  int i, *a, size, mssize, mcsize, lit, inmss;
  const int * res, * p;
  Var * v;

  if (ps->mtcls) return 0;

  check_mss_flags_clean (ps);

  if (mcs && ps->mcsass)
    {
      DELETEN (ps->mcsass, ps->szmcsass);
      ps->nmcsass = ps->szmcsass = 0;
      ps->mcsass = 0;
    }

  size = ps->alshead - ps->als;
  NEWN (a, size);

  for (i = 0; i < size; i++)
    a[i] = LIT2INT (ps->als[i]);

  (void) picosat_sat (ps, -1);

  //TODO short cut for 'picosat_res () == 10'?

  if (ps->mtcls)
    {
      assert (picosat_res (ps) == 20);
      res = 0;
      goto DONE;
    }

  res = mss (ps, a, size);

  if (ps->mtcls)
    {
      res = 0;
      goto DONE;
    }

  for (p = res; (lit = *p); p++) 
    {
      v = ps->vars + abs (lit);
      if (lit < 0)
	{
	  assert (!v->msspos);
	  v->mssneg = 1;
	}
      else
	{
	  assert (!v->mssneg);
	  v->msspos = 1;
	}
    }

  mssize = p - res;
  mcsize = INT_MIN;

  for (i = 0; i < size; i++)
    {
      lit = a[i];
      v = ps->vars + abs (lit);
      if (lit > 0 && v->msspos)
	inmss = 1;
      else if (lit < 0 && v->mssneg)
	inmss = 1;
      else 
	inmss = 0;

      if (mssize < mcsize)
	{
	  if (inmss)
	    picosat_add (ps, -lit);
	}
      else
	{
	  if (!inmss)
	    picosat_add (ps, lit);
	}

      if (!inmss && mcs)
	push_mcsass (ps, lit);
    }
  picosat_add (ps, 0);
  if (mcs)
    push_mcsass (ps, 0);

  for (i = 0; i < size; i++)
    {
      lit = a[i];
      v = ps->vars + abs (lit);
      v->msspos = 0;
      v->mssneg = 0;
    }

DONE:

  reassume (ps, a, size);
  DELETEN (a, size);

  return res;
}

const int *
picosat_next_maximal_satisfiable_subset_of_assumptions (PS * ps)
{
  const int * res;
  enter (ps);
  res = next_mss (ps, 0);
  leave (ps);
  return  res;
}

const int *
picosat_next_minimal_correcting_subset_of_assumptions (PS * ps)
{
  const int * res, * tmp;
  enter (ps);
  tmp = next_mss (ps, 1);
  res = tmp ? ps->mcsass : 0;
  leave (ps);
  return res;
}

const int *
picosat_humus (PS * ps, 
               void (*callback)(void*state,int nmcs,int nhumus),
	       void * state)
{
  int lit, nmcs, j, nhumus;
  const int * mcs, * p;
  unsigned i;
  Var * v;
  enter (ps);
#ifndef NDEBUG
  for (i = 1; i <= ps->max_var; i++)
    {
      v = ps->vars + i;
      assert (!v->humuspos);
      assert (!v->humusneg);
    }
#endif
  nhumus = nmcs = 0;
  while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps)))
    {
      for (p = mcs; (lit = *p); p++)
	{
	  v = ps->vars + abs (lit);
	  if (lit < 0)
	    {
	      if (!v->humusneg)
		{
		  v->humusneg = 1;
		  nhumus++;
		}
	    }
	  else
	    {
	      if (!v->humuspos)
		{
		  v->humuspos = 1;
		  nhumus++;
		}
	    }
	}
      nmcs++;
      LOG ( fprintf (ps->out, 
             "%smcs %d of size %d humus %d\n",
	     ps->prefix, nmcs, (int)(p - mcs), nhumus));
      if (callback)
	callback (state, nmcs, nhumus);
    }
  assert (!ps->szhumus);
  ps->szhumus = 1;
  for (i = 1; i <= ps->max_var; i++)
    {
      v = ps->vars + i;
      if (v->humuspos)
	ps->szhumus++;
      if (v->humusneg)
	ps->szhumus++;
    }
  assert (nhumus + 1 == ps->szhumus);
  NEWN (ps->humus, ps->szhumus);
  j = 0;
  for (i = 1; i <= ps->max_var; i++)
    {
      v = ps->vars + i;
      if (v->humuspos)
	{
	  assert (j < nhumus);
	  ps->humus[j++] = (int) i;
	}
      if (v->humusneg)
	{
	  assert (j < nhumus);
	  assert (i < INT_MAX);
	  ps->humus[j++] = - (int) i;
	}
    }
  assert (j == nhumus);
  assert (j < ps->szhumus);
  ps->humus[j] = 0;
  leave (ps);
  return ps->humus;
}

int
picosat_usedlit (PS * ps, int int_lit)
{
  int res;
  check_ready (ps);
  check_sat_or_unsat_or_unknown_state (ps);
  ABORTIF (!int_lit, "API usage: zero literal can not be used");
  int_lit = abs (int_lit);
  res = (int_lit <= (int) ps->max_var) ? ps->vars[int_lit].used : 0;
  return res;
}

void
picosat_write_clausal_core (PS * ps, FILE * file)
{
  check_trace_support_and_execute (ps, file, write_core_wrapper, 0);
}

void
picosat_write_compact_trace (PS * ps, FILE * file)
{
  check_trace_support_and_execute (ps, file, write_trace,
                                   COMPACT_TRACECHECK_TRACE_FMT);
}

void
picosat_write_extended_trace (PS * ps, FILE * file)
{
  check_trace_support_and_execute (ps, file, write_trace,
                                   EXTENDED_TRACECHECK_TRACE_FMT);
}

void
picosat_write_rup_trace (PS * ps, FILE * file)
{
  check_trace_support_and_execute (ps, file, write_trace, RUP_TRACE_FMT);
}

size_t
picosat_max_bytes_allocated (PS * ps)
{
  check_ready (ps);
  return ps->max_bytes;
}

void
picosat_set_propagation_limit (PS * ps, unsigned long long l)
{
  ps->lpropagations = l;
}

unsigned long long
picosat_propagations (PS * ps)
{
  return ps->propagations;
}

unsigned long long
picosat_visits (PS * ps)
{
  return ps->visits;
}

unsigned long long
picosat_decisions (PS * ps)
{
  return ps->decisions;
}

int
picosat_variables (PS * ps)
{
  check_ready (ps);
  return (int) ps->max_var;
}

int
picosat_added_original_clauses (PS * ps)
{
  check_ready (ps);
  return (int) ps->oadded;
}

void
picosat_stats (PS * ps)
{
#ifndef RCODE
  unsigned redlits;
#endif
#ifdef STATS
  check_ready (ps);
  assert (ps->sdecisions + ps->rdecisions + ps->assumptions == ps->decisions);
#endif
  if (ps->calls > 1)
     fprintf (ps->out, "%s%u calls\n", ps->prefix, ps->calls);
  if (ps->contexts)
    {
       fprintf (ps->out, "%s%u contexts", ps->prefix, ps->contexts);
#ifdef STATS
       fprintf (ps->out, " %u internal variables", ps->internals);
#endif
       fprintf (ps->out, "\n");
    }
   fprintf (ps->out, "%s%u iterations\n", ps->prefix, ps->iterations);
   fprintf (ps->out, "%s%u restarts", ps->prefix, ps->restarts);
#ifdef STATS
   fprintf (ps->out, " (%u skipped)", ps->skippedrestarts);
#endif
  fputc ('\n', ps->out);
#ifndef NFL
   fprintf (ps->out, "%s%u failed literals", ps->prefix, ps->failedlits);
#ifdef STATS
   fprintf (ps->out,
           ", %u calls, %u rounds, %llu propagations",
           ps->flcalls, ps->flrounds, ps->flprops);
#endif
  fputc ('\n', ps->out);
#ifdef STATS
   fprintf (ps->out, 
    "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n", 
    ps->prefix, 
    ps->ifailedlits, PERCENT (ps->ifailedlits, ps->failedlits),
    ps->floopsed, ps->fltried, ps->flskipped);
#endif
#endif
   fprintf (ps->out, "%s%u conflicts", ps->prefix, ps->conflicts);
#ifdef STATS
   fprintf (ps->out, " (%u uips = %.1f%%)\n", ps->uips, PERCENT(ps->uips,ps->conflicts));
#else
  fputc ('\n', ps->out);
#endif
#ifndef NADC
   fprintf (ps->out, "%s%u adc conflicts\n", ps->prefix, ps->adoconflicts);
#endif
#ifdef STATS
   fprintf (ps->out, "%s%llu dereferenced literals\n", ps->prefix, ps->derefs);
#endif
   fprintf (ps->out, "%s%u decisions", ps->prefix, ps->decisions);
#ifdef STATS
   fprintf (ps->out, " (%u random = %.2f%%",
           ps->rdecisions, PERCENT (ps->rdecisions, ps->decisions));
   fprintf (ps->out, ", %u assumptions", ps->assumptions);
  fputc (')', ps->out);
#endif
  fputc ('\n', ps->out);
#ifdef STATS
   fprintf (ps->out,
           "%s%u static phase decisions (%.1f%% of all variables)\n",
	   ps->prefix,
	   ps->staticphasedecisions, PERCENT (ps->staticphasedecisions, ps->max_var));
#endif
   fprintf (ps->out, "%s%u fixed variables\n", ps->prefix, ps->fixed);
  assert (ps->nonminimizedllits >= ps->minimizedllits);
#ifndef RCODE
  redlits = ps->nonminimizedllits - ps->minimizedllits;
#endif
   fprintf (ps->out, "%s%u learned literals\n", ps->prefix, ps->llitsadded);
   fprintf (ps->out, "%s%.1f%% deleted literals\n",
     ps->prefix, PERCENT (redlits, ps->nonminimizedllits));

#ifdef STATS
#ifdef TRACE
   fprintf (ps->out,
	   "%s%llu antecedents (%.1f antecedents per clause",
	   ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts));
  if (ps->trace)
     fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents));
  fputs (")\n", ps->out);
#endif

   fprintf (ps->out, "%s%llu propagations (%.1f propagations per decision)\n",
           ps->prefix, ps->propagations, AVERAGE (ps->propagations, ps->decisions));
   fprintf (ps->out, "%s%llu visits (%.1f per propagation)\n",
	   ps->prefix, ps->visits, AVERAGE (ps->visits, ps->propagations));
   fprintf (ps->out, 
           "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n",
	   ps->prefix, ps->bvisits, 
	   PERCENT (ps->bvisits, ps->visits),
	   AVERAGE (ps->bvisits, ps->propagations));
   fprintf (ps->out, 
           "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n",
	   ps->prefix, ps->tvisits, 
	   PERCENT (ps->tvisits, ps->visits),
	   AVERAGE (ps->tvisits, ps->propagations));
   fprintf (ps->out, 
           "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n",
	   ps->prefix, ps->lvisits, 
	   PERCENT (ps->lvisits, ps->visits),
	   AVERAGE (ps->lvisits, ps->propagations));
   fprintf (ps->out, "%s%llu other true (%.1f%% of visited clauses)\n",
	   ps->prefix, ps->othertrue, PERCENT (ps->othertrue, ps->visits));
   fprintf (ps->out, 
           "%s%llu other true in binary clauses (%.1f%%)"
	   ", %llu upper (%.1f%%)\n",
           ps->prefix, ps->othertrue2, PERCENT (ps->othertrue2, ps->othertrue),
	   ps->othertrue2u, PERCENT (ps->othertrue2u, ps->othertrue2));
   fprintf (ps->out, 
           "%s%llu other true in large clauses (%.1f%%)"
	   ", %llu upper (%.1f%%)\n",
           ps->prefix, ps->othertruel, PERCENT (ps->othertruel, ps->othertrue),
	   ps->othertruelu, PERCENT (ps->othertruelu, ps->othertruel));
   fprintf (ps->out, "%s%llu ternary and large traversals (%.1f per visit)\n",
	   ps->prefix, ps->traversals, AVERAGE (ps->traversals, ps->visits));
   fprintf (ps->out, "%s%llu large traversals (%.1f per large visit)\n",
	   ps->prefix, ps->ltraversals, AVERAGE (ps->ltraversals, ps->lvisits));
   fprintf (ps->out, "%s%llu assignments\n", ps->prefix, ps->assignments);
#else
   fprintf (ps->out, "%s%llu propagations\n", ps->prefix, picosat_propagations (ps));
   fprintf (ps->out, "%s%llu visits\n", ps->prefix, picosat_visits (ps));
#endif
   fprintf (ps->out, "%s%.1f%% variables used\n", ps->prefix, PERCENT (ps->vused, ps->max_var));

  sflush (ps);
   fprintf (ps->out, "%s%.1f seconds in library\n", ps->prefix, ps->seconds);
   fprintf (ps->out, "%s%.1f megaprops/second\n",
	   ps->prefix, AVERAGE (ps->propagations / 1e6f, ps->seconds));
   fprintf (ps->out, "%s%.1f megavisits/second\n",
	   ps->prefix, AVERAGE (ps->visits / 1e6f, ps->seconds));
   fprintf (ps->out, "%sprobing %.1f seconds %.0f%%\n",
           ps->prefix, ps->flseconds, PERCENT (ps->flseconds, ps->seconds));
#ifdef STATS
   fprintf (ps->out,
	   "%srecycled %.1f MB in %u reductions\n",
	   ps->prefix, ps->rrecycled / (double) (1 << 20), ps->reductions);
   fprintf (ps->out,
	   "%srecycled %.1f MB in %u simplifications\n",
	   ps->prefix, ps->srecycled / (double) (1 << 20), ps->simps);
#else
   fprintf (ps->out, "%s%u simplifications\n", ps->prefix, ps->simps);
   fprintf (ps->out, "%s%u reductions\n", ps->prefix, ps->reductions);
   fprintf (ps->out, "%s%.1f MB recycled\n", ps->prefix, ps->recycled / (double) (1 << 20));
#endif
   fprintf (ps->out, "%s%.1f MB maximally allocated\n",
	    ps->prefix, picosat_max_bytes_allocated (ps) / (double) (1 << 20));
}

#ifndef NGETRUSAGE
#include <sys/time.h>
#include <sys/resource.h>
#include <sys/unistd.h>
#endif

double
picosat_time_stamp (void)
{
  double res = -1;
#ifndef NGETRUSAGE
  struct rusage u;
  res = 0;
  if (!getrusage (RUSAGE_SELF, &u))
    {
      res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec;
      res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec;
    }
#endif
  return res;
}

double
picosat_seconds (PS * ps)
{
  check_ready (ps);
  return ps->seconds;
}

void
picosat_print (PS * ps, FILE * file)
{
#ifdef NO_BINARY_CLAUSES
  Lit * lit, *other, * last;
  Ltk * stack;
#endif
  Lit **q, **eol;
  Cls **p, *c;
  unsigned n;

  if (ps->measurealltimeinlib)
    enter (ps);
  else
    check_ready (ps);

  n = 0;
  n +=  ps->alshead - ps->als;

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;

      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif
      n++;
    }

#ifdef NO_BINARY_CLAUSES
  last = int2lit (ps, -ps->max_var);
  for (lit = int2lit (ps, 1); lit <= last; lit++)
    {
      stack = LIT2IMPLS (lit);
      eol = stack->start + stack->count;
      for (q = stack->start; q < eol; q++)
	if (*q >= lit)
	  n++;
    }
#endif

  fprintf (file, "p cnf %d %u\n", ps->max_var, n);

  for (p = SOC; p != EOC; p = NXC (p))
    {
      c = *p;
      if (!c)
	continue;

#ifdef TRACE
      if (c->collected)
	continue;
#endif

      eol = end_of_lits (c);
      for (q = c->lits; q < eol; q++)
	fprintf (file, "%d ", LIT2INT (*q));

      fputs ("0\n", file);
    }

#ifdef NO_BINARY_CLAUSES
  last = int2lit (ps, -ps->max_var);
  for (lit = int2lit (ps, 1); lit <= last; lit++)
    {
      stack = LIT2IMPLS (lit);
      eol = stack->start + stack->count;
      for (q = stack->start; q < eol; q++)
	if ((other = *q) >= lit)
	  fprintf (file, "%d %d 0\n", LIT2INT (lit), LIT2INT (other));
    }
#endif

  {
    Lit **r;
    for (r = ps->als; r < ps->alshead; r++)
      fprintf (file, "%d 0\n", LIT2INT (*r));
  }

  fflush (file);

  if (ps->measurealltimeinlib)
    leave (ps);
}

void
picosat_enter (PS * ps)
{
  enter (ps);
}

void
picosat_leave (PS * ps)
{
  leave (ps);
}

void
picosat_message (PS * ps, int vlevel, const char * fmt, ...)
{
  va_list ap;

  if (vlevel > ps->verbosity)
    return;

  fputs (ps->prefix, ps->out);
  va_start (ap, fmt);
  vfprintf (ps->out, fmt, ap);
  va_end (ap);
  fputc ('\n', ps->out);
}

int
picosat_changed (PS * ps)
{
  int res;

  check_ready (ps);
  check_sat_state (ps);

  res = (ps->min_flipped <= ps->saved_max_var);
  assert (!res || ps->saved_flips != ps->flips);

  return res;
}

void
picosat_reset_phases (PS * ps)
{
  rebias (ps);
}

void
picosat_reset_scores (PS * ps)
{
  Rnk * r;
  ps->hhead = ps->heap + 1;
  for (r = ps->rnks + 1; r <= ps->rnks + ps->max_var; r++)
    {
      CLR (r);
      hpush (ps, r);
    }
}

void
picosat_remove_learned (PS * ps, unsigned percentage)
{
  enter (ps);
  reset_incremental_usage (ps);
  reduce (ps, percentage);
  leave (ps);
}

void
picosat_set_global_default_phase (PS * ps, int phase)
{
  check_ready (ps);
  ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' "
                      "with negative argument");
  ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' "
                      "with argument > 3");
  GLOBAL_DEFAULT_PHASE = phase;
}

void
picosat_set_default_phase_lit (PS * ps, int int_lit, int phase)
{
  unsigned newphase;
  Lit * lit;
  Var * v;

  check_ready (ps);

  lit = import_lit (ps, int_lit, 1);
  v = LIT2VAR (lit);

  if (phase)
    {
      newphase = (int_lit < 0) == (phase < 0);
      v->defphase = v->phase = newphase;
      v->usedefphase = v->assigned = 1;
    }
  else
    {
      v->usedefphase = v->assigned = 0;
    }
}

void
picosat_set_more_important_lit (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;
  Rnk * r;

  check_ready (ps);

  lit = import_lit (ps, int_lit, 1);
  v = LIT2VAR (lit);
  r = VAR2RNK (v);

  ABORTIF (r->lessimportant, "can not mark variable more and less important"); 

  if (r->moreimportant)
    return;

  r->moreimportant = 1;

  if (r->pos)
    hup (ps, r);
}

void
picosat_set_less_important_lit (PS * ps, int int_lit)
{
  Lit * lit;
  Var * v;
  Rnk * r;

  check_ready (ps);

  lit = import_lit (ps, int_lit, 1);
  v = LIT2VAR (lit);
  r = VAR2RNK (v);

  ABORTIF (r->moreimportant, "can not mark variable more and less important"); 

  if (r->lessimportant)
    return;

  r->lessimportant = 1;

  if (r->pos)
    hdown (ps, r);
}

#ifndef NADC

unsigned 
picosat_ado_conflicts (PS * ps)
{
  check_ready (ps);
  return ps->adoconflicts;
}

void
picosat_disable_ado (PS * ps)
{
  check_ready (ps);
  assert (!ps->adodisabled);
  ps->adodisabled = 1;
}

void
picosat_enable_ado (PS * ps)
{
  check_ready (ps);
  assert (ps->adodisabled);
  ps->adodisabled = 0;
}

void
picosat_set_ado_conflict_limit (PS * ps, unsigned newadoconflictlimit)
{
  check_ready (ps);
  ps->adoconflictlimit = newadoconflictlimit;
}

#endif

void
picosat_simplify (PS * ps)
{
  enter (ps);
  reset_incremental_usage (ps);
  simplify (ps, 1);
  leave (ps);
}

int
picosat_haveados (void)
{
#ifndef NADC
  return 1;
#else
  return 0;
#endif
}

void
picosat_save_original_clauses (PS * ps)
{
  if (ps->saveorig) return;
  ABORTIF (ps->oadded, "API usage: 'picosat_save_original_clauses' too late");
  ps->saveorig = 1;
}

void picosat_set_interrupt (PicoSAT * ps,
                            void * external_state,
			    int (*interrupted)(void * external_state)) 
{
  ps->interrupt.state = external_state;
  ps->interrupt.function = interrupted;
}

int
picosat_deref_partial (PS * ps, int int_lit) 
{
  check_ready (ps);
  check_sat_state (ps);
  ABORTIF (!int_lit, "API usage: can not partial deref zero literal");
  ABORTIF (ps->mtcls, "API usage: deref partial after empty clause generated");
  ABORTIF (!ps->saveorig, "API usage: 'picosat_save_original_clauses' missing");

#ifdef STATS
  ps->derefs++;
#endif

  if (!ps->partial)
    minautarky (ps);

  return pderef (ps, int_lit);
}