Radish alpha
H
rad:z3QDZAW2FAfuLvihrhiyDC9fAD8G9
HardenedBSD Package Manager
Radicle
Git
Add picosat code.
Vsevolod Stakhov committed 11 years ago
commit 47b7b439286b5b884d73369358ccf710d0d6b9d8
parent 6a53935
6 files changed +9287 -0
modified external/Makefile.am
@@ -58,6 +58,7 @@ noinst_HEADERS= expat/amiga/expat_68k.h \
		libyaml/include/yaml.h \
		libyaml/src/yaml_private.h \
		libyaml/win32/config.h \
+
		picosat/picosat.h \
		sqlite/sqlite3.h \
		uthash/utarray.h \
		uthash/uthash.h \
@@ -71,6 +72,7 @@ noinst_LTLIBRARIES= libucl.la libucl_static.la \
			libyaml.la libyaml_static.la \
			libexpat.la libexpat_static.la \
			libsbuf.la libsbuf_static.la \
+
			libpicosat.la libpicosat_static.la \
			@LIBELF_BUNDLED@

libelf_la_SOURCES=	libelf/elf.c \
@@ -182,6 +184,16 @@ libyaml_static_la_SOURCES= $(libyaml_la_SOURCES)
libyaml_static_la_CFLAGS= $(yaml_common_cflags) -static
libyaml_static_la_LDFLAGS=	-all-static

+
picosat_common_cflags=	-I$(top_srcdir)/external/picosat \
+
			-Wno-strict-aliasing \
+
			-Wno-unused		
+
libpicosat_la_SOURCES=	picosat/picosat.c \
+
			picosat/version.c
+
libpicosat_la_CFLAGS=	$(picosat_common_cflags) -shared
+
libpicosat_static_la_SOURCES=	$(libpicosat_la_SOURCES)
+
libpicosat_static_la_CFLAGS= $(picosat_common_cflags) -static
+
libpicosat_static_la_LDFLAGS=	-all-static
+

sqlite_common_cflags=	-DHAVE_SQLITE_CONFIG_H \
			-Wno-unused-variable \
			-Wno-unused-function \
added external/picosat/LICENSE
@@ -0,0 +1,20 @@
+
Copyright (c) 2006 - 2013, 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.
+

added external/picosat/picosat.c
@@ -0,0 +1,8589 @@
+
/****************************************************************************
+
Copyright (c) 2006 - 2014, 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 "picosat.h"
+

+
/* 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
+

+
#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 */
+

+
#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 the '--log' option for the configure script.
+
 */
+
#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 = (unsigned)((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) ((unsigned)((l) - ps->lits) / 2)
+
#define LIT2IMPLS(l) (ps->impls + (unsigned)((l) - ps->lits))
+
#define LIT2INT(l) ((int)(LIT2SGN(l) * LIT2IDX(l)))
+
#define LIT2SGN(l) (((unsigned)((l) - ps->lits) & 1) ? -1 : 1)
+
#define LIT2VAR(l) (ps->vars + LIT2IDX(l))
+
#define LIT2HTPS(l) (ps->htps + (unsigned)((l) - ps->lits))
+
#define LIT2JWH(l) (ps->jwh + ((l) - ps->lits))
+

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

+
#ifdef NO_BINARY_CLAUSES
+
typedef unsigned long 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*)((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))
+

+
#define ABORT(msg) \
+
  do { \
+
    fputs ("*** picosat: " msg "\n", stderr); \
+
    abort (); \
+
  } while (0)
+

+
#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)
+

+
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,
+
};
+

+
enum Phase
+
{
+
  POSPHASE,
+
  NEGPHASE,
+
  JWLPHASE,
+
  RNDPHASE,
+
};
+

+
struct PicoSAT 
+
{
+
  enum State state;
+
  enum Phase defaultphase;
+
  int last_sat_call_result;
+

+
  FILE *out;
+
  char * prefix;
+
  int verbosity;
+
  int plain;
+
  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
+
  FILE * rup;
+
  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;
+

+
#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 | ((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;
+
  mb >>= delta;
+
  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;
+
  char 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 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;
+
  ps->defaultphase = JWLPHASE;
+
#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;
+

+
  ps->out = stdout;
+
  new_prefix (ps, "c ");
+
  ps->verbosity = 0;
+
  ps->plain = 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->defaultphase = JWLPHASE;
+
  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)
+
    *CLS2ACT (res) = 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->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
+
  ps->implvalid = 0;
+
  ps->cimplvalid = 0;
+
  {
+
    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);
+
  ps->saved_size = 0;
+
#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);
+
  ps->trail = ps->ttail = ps->ttail2 = ps->thead = ps->eot = 0;
+
#ifndef NADC
+
  ps->ttailado = 0;
+
#endif
+

+
  DELETEN (ps->heap, ps->eoh - ps->heap);
+
  ps->heap = ps->hhead = ps->eoh = 0;
+

+
  DELETEN (ps->als, ps->eoals - ps->als);
+
  ps->als = ps->eoals = ps->alshead = ps->alstail = 0;
+
  ps->extracted_all_failed_assumptions = 0;
+
  ps->failed_assumption = 0;
+
  ps->adecidelevel = 0;
+
  DELETEN (ps->CLS, ps->eocls - ps->CLS);
+
  ps->CLS = ps->eocls = ps->clshead = 0;
+
  DELETEN (ps->rils, ps->eorils - ps->rils);
+
  ps->rils = ps->eorils = ps->rilshead = 0;
+
  DELETEN (ps->cils, ps->eocils - ps->cils);
+
  ps->cils = ps->eocils = ps->cilshead = 0;
+
  DELETEN (ps->fals, ps->eofals - ps->fals);
+
  ps->fals = ps->eofals = ps->falshead = 0;
+
  DELETEN (ps->mass, ps->szmass);
+
  ps->szmass = 0;
+
  ps->mass = 0;
+
  DELETEN (ps->mssass, ps->szmssass);
+
  ps->szmssass = 0;
+
  ps->mssass = 0;
+
  DELETEN (ps->mcsass, ps->szmcsass);
+
  ps->nmcsass = ps->szmcsass = 0;
+
  ps->mcsass = 0;
+
  DELETEN (ps->humus, ps->szhumus);
+
  ps->szhumus = 0;
+
  ps->humus = 0;
+

+
  ps->size_vars = 0;
+
  ps->max_var = 0;
+

+
  ps->mtcls = 0;
+
#ifdef TRACE
+
  ps->ocore = -1;
+
#endif
+
  ps->conflict = 0;
+

+
  DELETEN (ps->added, ps->eoa - ps->added);
+
  ps->eoa = ps->ahead = 0;
+

+
  DELETEN (ps->marked, ps->eom - ps->marked);
+
  ps->eom = ps->mhead = 0;
+

+
  DELETEN (ps->dfs, ps->eod - ps->dfs);
+
  ps->eod = ps->dhead = 0;
+

+
  DELETEN (ps->resolved, ps->eor - ps->resolved);
+
  ps->eor = ps->rhead = 0;
+

+
  DELETEN (ps->levels, ps->eolevels - ps->levels);
+
  ps->eolevels = ps->levelshead = 0;
+

+
  DELETEN (ps->dused, ps->eodused - ps->dused);
+
  ps->eodused = ps->dusedhead = 0;
+

+
  DELETEN (ps->buffer, ps->eob - ps->buffer);
+
  ps->eob = ps->bhead = 0;
+

+
  DELETEN (ps->indices, ps->eoi - ps->indices);
+
  ps->eoi = ps->ihead = 0;
+

+
  DELETEN (ps->soclauses, ps->eoso - ps->soclauses);
+
  ps->soclauses = ps->eoso = ps->sohead = 0;
+
  ps->saveorig = ps->partial = 0;
+

+
  delete_prefix (ps);
+

+
  delete (ps, ps->rline[0], ps->szrline);
+
  delete (ps, ps->rline[1], ps->szrline);
+
  ps->rline[0] = ps->rline[1] = 0;
+
  ps->szrline = ps->RCOUNT = 0;
+
  assert (getenv ("LEAK") || !ps->current_bytes);	/* found leak if failing */
+
  ps->max_bytes = 0;
+
  ps->recycled = 0;
+
  ps->current_bytes = 0;
+

+
  ps->lrestart = 0;
+
  ps->lreduce = 0;
+
  ps->lastreduceconflicts = 0;
+
  ps->llocked = 0;
+
  ps->lsimplify = 0;
+
  ps->fsimplify = 0;
+

+
  ps->seconds = 0;
+
  ps->flseconds = 0;
+
  ps->entered = 0;
+
  ps->nentered = 0;
+
  ps->measurealltimeinlib = 0;
+

+
  ps->levelsum = 0.0;
+
  ps->calls = 0;
+
  ps->decisions = 0;
+
  ps->restarts = 0;
+
  ps->simps = 0;
+
  ps->iterations = 0;
+
  ps->reports = 0;
+
  ps->lastrheader = -2;
+
  ps->fixed = 0;
+
#ifndef NFL
+
  ps->failedlits = 0;
+
  ps->simplifying = 0;
+
  ps->fllimit = 0;
+
#ifdef STATS
+
  ps->efailedlits = ps->ifailedlits = 0;
+
  ps->fltried = ps->flskipped = ps->floopsed = 0;
+
  ps->flcalls = ps->flrounds = 0;
+
  ps->flprops = 0;
+
#endif
+
#endif
+
  ps->propagations = 0;
+
  ps->contexts = 0;
+
  ps->internals = 0;
+
  ps->conflicts = 0;
+
  ps->noclauses = 0;
+
  ps->oadded = 0;
+
  ps->lladded = 0;
+
  ps->loadded = 0;
+
  ps->olits = 0;
+
  ps->nlclauses = 0;
+
  ps->ladded = 0;
+
  ps->addedclauses = 0;
+
  ps->llits = 0;
+
  ps->out = 0;
+
#ifdef TRACE
+
  ps->trace = 0;
+
#endif
+
  ps->rup = 0;
+
  ps->rupstarted = 0;
+
  ps->rupclauses = 0;
+
  ps->rupvariables = 0;
+
  ps->LEVEL = 0;
+

+
  ps->reductions = 0;
+

+
  ps->vused = 0;
+
  ps->llitsadded = 0;
+
  ps->visits = 0;
+
#ifdef STATS
+
  ps->loused = 0;
+
  ps->llused = 0;
+
  ps->bvisits = 0;
+
  ps->tvisits = 0;
+
  ps->lvisits = 0;
+
  ps->othertrue = 0;
+
  ps->othertrue2 = 0;
+
  ps->othertruel = 0;
+
  ps->othertrue2u = 0;
+
  ps->othertruelu = 0;
+
  ps->ltraversals = 0;
+
  ps->traversals = 0;
+
#ifndef NO_BINARY_CLAUSES
+
  ps->antecedents = 0;
+
#endif
+
  ps->znts = 0;
+
  ps->uips = 0;
+
  ps->assumptions = 0;
+
  ps->rdecisions = 0;
+
  ps->sdecisions = 0;
+
  ps->srecycled = 0;
+
  ps->rrecycled = 0;
+
#endif
+
  ps->minimizedllits = 0;
+
  ps->nonminimizedllits = 0;
+
  ps->state = RESET;
+
  ps->srng = 0;
+

+
  ps->saved_flips = 0;
+
  ps->saved_max_var = 0;
+
  ps->min_flipped = UINT_MAX;
+

+
  ps->flips = 0;
+
#ifdef STATS
+
  ps->FORCED = 0;
+
  ps->assignments = 0;
+
#endif
+

+
  ps->sdflips = 0;
+
  ps->defaultphase = JWLPHASE;
+

+
#ifdef STATS
+
  ps->staticphasedecisions = 0;
+
  ps->inclreduces = 0;
+
  ps->skippedrestarts = 0;
+
#endif
+

+
#ifdef VISCORES
+
  pclose (ps->fviscores);
+
  ps->fviscores = 0;
+
#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;
+
#else
+
#ifdef STATS
+
  ps->antecedents++;
+
#endif
+
#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 && ps->rup)
+
    {
+
      if (!ps->rupstarted)
+
	{
+
	  write_rup_header (ps, ps->rup);
+
	  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 && ps->rup)
+
	fprintf (ps->rup, "%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 && ps->rup)
+
    fputs ("0\n", ps->rup);
+

+
  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);
+
  *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; 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);
+

+
  lits_delta = ps->lits - old_lits;
+
  rnks_delta = ps->rnks - old_rnks;
+

+
  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
+
  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;
+

+
  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;
+

+
  double start = picosat_time_stamp ();
+

+
  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 = 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 (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 (Lit ** ado)
+
{
+
  Lit *** res, ** other;
+
  unsigned pos, delta;
+

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

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

+
  delta = hash_ado (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 (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 (v->ado);
+
  ado = *adotabpos;
+

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

+
  assert (ado != v->ado);
+

+
  ps->adoconflict = new_clause (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);
+

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

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

+
  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 int
+
luby (int i)
+
{
+
  int k;
+
  for (k = 1; k < 32; k++)
+
    if (i == (1 << k) - 1)
+
      return 1 << (k - 1);
+

+
  for (k = 1;; k++)
+
    if ((1 << (k - 1)) <= i && i < (1 << k) - 1)
+
      return luby (i - (1 << (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 (ps->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;
+
  Act b;
+

+
  (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;
+

+
  a = *CLS2ACT (c);
+
  b = *CLS2ACT (d);
+

+
  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 (ps->defaultphase == POSPHASE)
+
	{
+
	  /* assign to TRUE */
+
	}
+
      else if (ps->defaultphase == NEGPHASE)
+
	{
+
	  /* assign to FALSE */
+
	  lit = not_lit;
+
	}
+
      else if (ps->defaultphase == 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->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);
+
  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->rup = rup_file;
+
  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 (ps->rup && 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 (external_lit, 1);
+
      add_lit (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);
+
}
+

+
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";
+
}
+

+
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;
+

+
  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) 
+
    {
+
      best = 0; 
+
      maxoccs = 0;
+
      for (p = c; (lit = *p); p++)
+
	{
+
	  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\n", 
+
	       ps->prefix, best, maxoccs));
+
	  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)
+
{
+
  Lit *lit;
+
  Var * v;
+

+
  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;
+

+
  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;
+
}
+

+
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, norig = ps->alshead - ps->als, nwork, * work, res;
+
  signed char * redundant;
+
  Lit ** p, * lit;
+
  int failed;
+
  Var * v;
+
#ifndef NDEBUG
+
  int oldlen;
+
#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)
+
{
+
  unsigned redlits;
+
#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);
+
  redlits = ps->nonminimizedllits - ps->minimizedllits;
+
   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
+
#ifndef NO_BINARY_CLAUSES
+
   fprintf (ps->out,
+
	   "%s%llu antecedents (%.1f antecedents per clause",
+
	   ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts));
+
#endif
+
#ifdef TRACE
+
  if (ps->trace)
+
     fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents));
+
#endif
+
#if !defined(NO_BINARY_CLAUSES) || defined(TRACE)
+
  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");
+
  ps->defaultphase = 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 (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;
+
}
+

+
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);
+
}
added external/picosat/picosat.h
@@ -0,0 +1,649 @@
+
/****************************************************************************
+
Copyright (c) 2006 - 2014, 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.
+
****************************************************************************/
+

+
#ifndef picosat_h_INCLUDED
+
#define picosat_h_INCLUDED
+

+
/*------------------------------------------------------------------------*/
+

+
#include <stdlib.h>
+
#include <stdio.h>
+

+
/*------------------------------------------------------------------------*/
+
/* The following macros allows for users to distiguish between different
+
 * versions of the API.  The first 'PICOSAT_REENTRANT_API' is defined for
+
 * the new reentrant API which allows to generate multiple instances of
+
 * PicoSAT in one process.  The second 'PICOSAT_API_VERSION' defines the
+
 * (smallest) version of PicoSAT to which this API conforms.
+
 */
+
#define PICOSAT_REENTRANT_API
+
#define PICOSAT_API_VERSION 953		/* API version */
+

+
/*------------------------------------------------------------------------*/
+
/* These are the return values for 'picosat_sat' as for instance
+
 * standardized by the output format of the SAT competition.
+
 */
+
#define PICOSAT_UNKNOWN         0
+
#define PICOSAT_SATISFIABLE     10
+
#define PICOSAT_UNSATISFIABLE   20
+

+
/*------------------------------------------------------------------------*/
+

+
typedef struct PicoSAT PicoSAT;
+

+
/*------------------------------------------------------------------------*/
+

+
const char *picosat_version (void);
+
const char *picosat_config (void);
+
const char *picosat_copyright (void);
+

+
/*------------------------------------------------------------------------*/
+
/* You can make PicoSAT use an external memory manager instead of the one
+
 * provided by LIBC. But then you need to call these three function before
+
 * 'picosat_init'.  The memory manager functions here all have an additional
+
 * first argument which is a pointer to the memory manager, but otherwise
+
 * are supposed to work as their LIBC counter parts 'malloc', 'realloc' and
+
 * 'free'.  As exception the 'resize' and 'delete' function have as third
+
 * argument the number of bytes of the block given as second argument.
+
 */
+

+
typedef void * (*picosat_malloc)(void *, size_t);
+
typedef void * (*picosat_realloc)(void*, void *, size_t, size_t);
+
typedef void (*picosat_free)(void*, void*, size_t);
+

+
/*------------------------------------------------------------------------*/
+

+
PicoSAT * picosat_init (void);          /* constructor */
+

+
PicoSAT * picosat_minit (void * state,
+
			 picosat_malloc,
+
			 picosat_realloc,
+
			 picosat_free);
+

+
void picosat_reset (PicoSAT *);         /* destructor */
+

+
/*------------------------------------------------------------------------*/
+
/* The following five functions are essentially parameters to 'init', and
+
 * thus should be called right after 'picosat_init' before doing anything
+
 * else.  You should not call any of them after adding a literal.
+
 */
+

+
/* Set output file, default is 'stdout'.
+
 */
+
void picosat_set_output (PicoSAT *, FILE *);
+

+
/* Measure all time spent in all calls in the solver.  By default only the
+
 * time spent in 'picosat_sat' is measured.  Enabling this function might
+
 * for instance triple the time needed to add large CNFs, since every call
+
 * to 'picosat_add' will trigger a call to 'getrusage'.
+
 */
+
void picosat_measure_all_calls (PicoSAT *);
+

+
/* Set the prefix used for printing verbose messages and statistics.
+
 * Default is "c ".
+
 */
+
void picosat_set_prefix (PicoSAT *, const char *);
+

+
/* Set verbosity level.  A verbosity level of 1 and above prints more and
+
 * more detailed progress reports on the output file, set by
+
 * 'picosat_set_output'.  Verbose messages are prefixed with the string set
+
 * by 'picosat_set_prefix'.
+
 */
+
void picosat_set_verbosity (PicoSAT *, int new_verbosity_level);
+

+
/* Disable/Enable all pre-processing, currently only failed literal probing.
+
 *
+
 *  new_plain_value != 0    only 'plain' solving, so no preprocessing
+
 *  new_plain_value == 0    allow preprocessing
+
 */
+
void picosat_set_plain (PicoSAT *, int new_plain_value);
+

+
/* Set default initial phase: 
+
 *
+
 *   0 = false
+
 *   1 = true
+
 *   2 = Jeroslow-Wang (default)
+
 *   3 = random initial phase
+
 *
+
 * After a variable has been assigned the first time, it will always
+
 * be assigned the previous value if it is picked as decision variable.
+
 * The initial assignment can be chosen with this function.
+
 */
+
void picosat_set_global_default_phase (PicoSAT *, int);
+

+
/* Set next/initial phase of a particular variable if picked as decision
+
 * variable.  Second argument 'phase' has the following meaning:
+
 *
+
 *   negative = next value if picked as decision variable is false
+
 *
+
 *   positive = next value if picked as decision variable is true
+
 *
+
 *   0        = use global default phase as next value and
+
 *              assume 'lit' was never assigned
+
 *
+
 * Again if 'lit' is assigned afterwards through a forced assignment,
+
 * then this forced assignment is the next phase if this variable is
+
 * used as decision variable.
+
 */
+
void picosat_set_default_phase_lit (PicoSAT *, int lit, int phase);
+

+
/* You can reset all phases by the following function.
+
 */
+
void picosat_reset_phases (PicoSAT *);
+

+
/* Scores can be erased as well.  Note, however, that even after erasing 
+
 * scores and phases, learned clauses are kept.  In addition head tail
+
 * pointers for literals are not moved either.  So expect a difference
+
 * between calling the solver in incremental mode or with a fresh copy of
+
 * the CNF.
+
 */
+
void picosat_reset_scores (PicoSAT *);
+

+
/* Reset assignment if in SAT state and then remove the given percentage of
+
 * less active (large) learned clauses.  If you specify 100% all large
+
 * learned clauses are removed.
+
 */
+
void picosat_remove_learned (PicoSAT *, unsigned percentage);
+

+
/* Set some variables to be more important than others.  These variables are
+
 * always used as decisions before other variables are used.  Dually there
+
 * is a set of variables that is used last.  The default is
+
 * to mark all variables as being indifferent only.
+
 */
+
void picosat_set_more_important_lit (PicoSAT *, int lit);
+
void picosat_set_less_important_lit (PicoSAT *, int lit);
+

+
/* Allows to print to internal 'out' file from client.
+
 */
+
void picosat_message (PicoSAT *, int verbosity_level, const char * fmt, ...);
+

+
/* Set a seed for the random number generator.  The random number generator
+
 * is currently just used for generating random decisions.  In our
+
 * experiments having random decisions did not really help on industrial
+
 * examples, but was rather helpful to randomize the solver in order to
+
 * do proper benchmarking of different internal parameter sets.
+
 */
+
void picosat_set_seed (PicoSAT *, unsigned random_number_generator_seed);
+

+
/* If you ever want to extract cores or proof traces with the current
+
 * instance of PicoSAT initialized with 'picosat_init', then make sure to
+
 * call 'picosat_enable_trace_generation' right after 'picosat_init'.   This
+
 * is not necessary if you only use 'picosat_set_incremental_rup_file'.
+
 *
+
 * NOTE, trace generation code is not necessarily included, e.g. if you
+
 * configure PicoSAT with full optimzation as './configure -O' or with
+
 
+
 * you do not get any results by trying to generate traces.
+
 *
+
 * The return value is non-zero if code for generating traces is included
+
 * and it is zero if traces can not be generated.
+
 */
+
int picosat_enable_trace_generation (PicoSAT *);
+

+
/* You can dump proof traces in RUP format incrementally even without
+
 * keeping the proof trace in memory.  The advantage is a reduction of
+
 * memory usage, but the dumped clauses do not necessarily belong to the
+
 * clausal core.  Beside the file the additional parameters denotes the
+
 * maximal number of variables and the number of original clauses.
+
 */
+
void picosat_set_incremental_rup_file (PicoSAT *, FILE * file, int m, int n);
+

+
/* Save original clauses for 'picosat_deref_partial'.  See comments to that
+
 * function further down.
+
 */
+
void picosat_save_original_clauses (PicoSAT *);
+

+
/*------------------------------------------------------------------------*/
+
/* This function returns the next available unused variable index and
+
 * allocates a variable for it even though this variable does not occur as
+
 * assumption, nor in a clause or any other constraints.  In future calls to
+
 * 'picosat_sat', 'picosat_deref' and particularly for 'picosat_changed',
+
 * this variable is treated as if it had been used.
+
 */
+
int picosat_inc_max_var (PicoSAT *);
+

+
/*------------------------------------------------------------------------*/
+
/* Push and pop semantics for PicoSAT.   'picosat_push' opens up a new
+
 * context.  All clauses added in this context are attached to it and
+
 * discarded when the context is closed with 'picosat_pop'.  It is also
+
 * possible to nest contexts.
+
 *
+
 * The current implementation uses a new internal variable for each context.
+
 * However, the indices for these internal variables are shared with
+
 * ordinary external variables.  This means that after any call to
+
 * 'picosat_push', new variable indices should be obtained with
+
 * 'picosat_inc_max_var' and not just by incrementing the largest variable
+
 * index used so far.
+
 *
+
 * The return value is the index of the literal that assumes this context.
+
 * This literal can only be used for 'picosat_failed_context' otherwise
+
 * it will lead to an API usage error.
+
 */
+
int picosat_push (PicoSAT *);
+

+
/* This is as 'picosat_failed_assumption', but only for internal variables
+
 * generated by 'picosat_push'.
+
 */
+
int picosat_failed_context (PicoSAT *, int lit);
+

+
/* Returns the literal that assumes the current context or zero if the
+
 * outer context has been reached.
+
 */
+
int picosat_context (PicoSAT *);	
+

+
/* Closes the current context and recycles the literal generated for
+
 * assuming this context.  The return value is the literal for the new
+
 * outer context or zero if the outer most context has been reached.
+
 */
+
int picosat_pop (PicoSAT *);
+

+
/* Force immmediate removal of all satisfied clauses and clauses that are
+
 * added or generated in closed contexts.  This function is called
+
 * internally if enough units are learned or after a certain number of
+
 * contexts have been closed.  This number is fixed at compile time
+
 * and defined as MAXCILS in 'picosat.c'.
+
 *
+
 * Note that learned clauses which only involve outer contexts are kept.
+
 */
+
void picosat_simplify (PicoSAT *);
+

+
/*------------------------------------------------------------------------*/
+
/* If you know a good estimate on how many variables you are going to use
+
 * then calling this function before adding literals will result in less
+
 * resizing of the variable table.  But this is just a minor optimization.
+
 * Beside exactly allocating enough variables it has the same effect as
+
 * calling 'picosat_inc_max_var'.
+
 */
+
void picosat_adjust (PicoSAT *, int max_idx);
+

+
/*------------------------------------------------------------------------*/
+
/* Statistics.
+
 */
+
int picosat_variables (PicoSAT *);                      /* p cnf <m> n */
+
int picosat_added_original_clauses (PicoSAT *);         /* p cnf m <n> */
+
size_t picosat_max_bytes_allocated (PicoSAT *);
+
double picosat_time_stamp (void);                       /* ... in process */
+
void picosat_stats (PicoSAT *);                         /* > output file */
+
unsigned long long picosat_propagations (PicoSAT *);	/* #propagations */
+
unsigned long long picosat_decisions (PicoSAT *);	/* #decisions */
+
unsigned long long picosat_visits (PicoSAT *);		/* #visits */
+

+
/* The time spent in calls to the library or in 'picosat_sat' respectively.
+
 * The former is returned if, right after initialization
+
 * 'picosat_measure_all_calls' is called.
+
 */
+
double picosat_seconds (PicoSAT *);
+

+
/*------------------------------------------------------------------------*/
+
/* Add a literal of the next clause.  A zero terminates the clause.  The
+
 * solver is incremental.  Adding a new literal will reset the previous
+
 * assignment.   The return value is the original clause index to which
+
 * this literal respectively the trailing zero belong starting at 0.
+
 */
+
int picosat_add (PicoSAT *, int lit);
+

+
/* As the previous function, but allows to add a full clause at once with an
+
 * at compiled time known size.  The list of argument literals has to be
+
 * terminated with a zero literal.  Literals beyond the first zero literal
+
 * are discarded.
+
 */
+
int picosat_add_arg (PicoSAT *, ...);
+

+
/* As the previous function but with an at compile time unknown size.
+
 */
+
int picosat_add_lits (PicoSAT *, int * lits);
+

+
/* Print the CNF to the given file in DIMACS format.
+
 */
+
void picosat_print (PicoSAT *, FILE *);
+

+
/* You can add arbitrary many assumptions before the next 'picosat_sat'
+
 * call.  This is similar to the using assumptions in MiniSAT, except that
+
 * for PicoSAT you do not have to collect all your assumptions in a vector
+
 * yourself.  In PicoSAT you can add one after the other, to be used in the 
+
 * next call to 'picosat_sat'.
+
 *
+
 * These assumptions can be interpreted as adding unit clauses with those
+
 * assumptions as literals.  However these assumption clauses are only valid
+
 * for exactly the next call to 'picosat_sat', and will be removed
+
 * afterwards, e.g. in following future calls to 'picosat_sat' after the
+
 * next 'picosat_sat' call, unless they are assumed again trough
+
 * 'picosat_assume'.
+
 *
+
 * More precisely, assumptions actually remain valid even after the next
+
 * call to 'picosat_sat' has returned.  Valid means they remain 'assumed'
+
 * internally until a call to 'picosat_add', 'picosat_assume', or a second
+
 * 'picosat_sat', following the first 'picosat_sat'.  The reason for keeping
+
 * them valid is to allow 'picosat_failed_assumption' to return correct
+
 * values.  
+
 *
+
 * Example:
+
 *
+
 *   picosat_assume (1);        // assume unit clause '1 0'
+
 *   picosat_assume (-2);       // additionally assume clause '-2 0'
+
 *   res = picosat_sat (1000);  // assumes 1 and -2 to hold
+
 *                              // 1000 decisions max.
+
 *
+
 *   if (res == PICOSAT_UNSATISFIABLE) 
+
 *     {
+
 *       if (picosat_failed_assumption (1))
+
 *         // unit clause '1 0' was necessary to derive UNSAT
+
 *
+
 *       if (picosat_failed_assumption (-2))
+
 *         // unit clause '-2 0' was necessary to derive UNSAT
+
 *
+
 *       // at least one but also both could be necessary
+
 *
+
 *       picosat_assume (17);  // previous assumptions are removed
+
 *                             // now assume unit clause '17 0' for
+
 *                             // the next call to 'picosat_sat'
+
 *
+
 *       // adding a new clause, actually the first literal of
+
 *       // a clause would also make the assumptions used in the previous
+
 *       // call to 'picosat_sat' invalid.
+
 *
+
 *       // The first two assumptions above are not assumed anymore.  Only
+
 *       // the assumptions, since the last call to 'picosat_sat' returned
+
 *       // are assumed, e.g. the unit clause '17 0'.
+
 *
+
 *       res = picosat_sat (-1);
+
 *     }
+
 *   else if (res == PICOSAT_SATISFIABLE)
+
 *     {
+
 *       // now the assignment is valid and we can call 'picosat_deref'
+
 *
+
 *       assert (picosat_deref (1) == 1));
+
 *       assert (picosat_deref (-2) == 1));
+
 *
+
 *       val = picosat_deref (15);
+
 *
+
 *       // previous two assumptions are still valid
+
 *
+
 *       // would become invalid if 'picosat_add' or 'picosat_assume' is
+
 *       // called here, but we immediately call 'picosat_sat'.  Now when
+
 *       // entering 'picosat_sat' the solver knows that the previous call
+
 *       // returned SAT and it can safely reset the previous assumptions
+
 *
+
 *       res = picosat_sat (-1);
+
 *     }
+
 *   else
+
 *     {
+
 *       assert (res == PICOSAT_UNKNOWN);
+
 *
+
 *       // assumptions valid, but assignment invalid
+
 *       // except for top level assigned literals which
+
 *       // necessarily need to have this value if the formula is SAT
+
 *
+
 *       // as above the solver nows that the previous call returned UNKWOWN
+
 *       // and will before doing anything else reset assumptions
+
 *
+
 *       picosat_sat (-1);
+
 *     }
+
 */
+
void picosat_assume (PicoSAT *, int lit);
+

+
/*------------------------------------------------------------------------*/
+
/* This is an experimental feature for handling 'all different constraints'
+
 * (ADC).  Currently only one global ADC can be handled.  The bit-width of
+
 * all the bit-vectors entered in this ADC (stored in 'all different
+
 * objects' or ADOs) has to be identical.
+
 *
+
 * TODO: also handle top level assigned literals here.
+
 */
+
void picosat_add_ado_lit (PicoSAT *, int);
+

+
/*------------------------------------------------------------------------*/
+
/* Call the main SAT routine.  A negative decision limit sets no limit on
+
 * the number of decisions.  The return values are as above, e.g.
+
 * 'PICOSAT_UNSATISFIABLE', 'PICOSAT_SATISFIABLE', or 'PICOSAT_UNKNOWN'.
+
 */
+
int picosat_sat (PicoSAT *, int decision_limit);
+

+
/* As alternative to a decision limit you can use the number of propagations
+
 * as limit.  This is more linearly related to execution time. This has to
+
 * be called after 'picosat_init' and before 'picosat_sat'.
+
 */
+
void picosat_set_propagation_limit (PicoSAT *, unsigned long long limit);
+

+
/* Return last result of calling 'picosat_sat' or '0' if not called.
+
 */
+
int picosat_res (PicoSAT *);
+

+
/* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then
+
 * the satisfying assignment can be obtained by 'dereferencing' literals.
+
 * The value of the literal is return as '1' for 'true',  '-1' for 'false'
+
 * and '0' for an unknown value.
+
 */
+
int picosat_deref (PicoSAT *, int lit);
+

+
/* Same as before but just returns true resp. false if the literals is
+
 * forced to this assignment at the top level.  This function does not
+
 * require that 'picosat_sat' was called and also does not internally reset
+
 * incremental usage.
+
 */
+
int picosat_deref_toplevel (PicoSAT *, int lit);
+

+
/* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE' a
+
 * partial satisfying assignment can be obtained as well.  It satisfies all
+
 * original clauses.  The value of the literal is return as '1' for 'true',
+
 * '-1' for 'false' and '0' for an unknown value.  In order to make this
+
 * work all original clauses have to be saved internally, which has to be
+
 * enabled by 'picosat_save_original_clauses' right after initialization.
+
 */
+
int picosat_deref_partial (PicoSAT *, int lit);
+

+
/* Returns non zero if the CNF is unsatisfiable because an empty clause was
+
 * added or derived.
+
 */
+
int picosat_inconsistent  (PicoSAT *);
+

+
/* Returns non zero if the literal is a failed assumption, which is defined
+
 * as an assumption used to derive unsatisfiability.  This is as accurate as
+
 * generating core literals, but still of course is an overapproximation of
+
 * the set of assumptions really necessary.  The technique does not need
+
 * clausal core generation nor tracing to be enabled and thus can be much
+
 * more effective.  The function can only be called as long the current
+
 * assumptions are valid.  See 'picosat_assume' for more details.
+
 */
+
int picosat_failed_assumption (PicoSAT *, int lit);
+

+
/* Returns a zero terminated list of failed assumption in the last call to
+
 * 'picosat_sat'.  The pointer is valid until the next call to
+
 * 'picosat_sat' or 'picosat_failed_assumptions'.  It only makes sense if the
+
 * last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'.
+
 */
+
const int * picosat_failed_assumptions (PicoSAT *);
+

+
/* Returns a zero terminated minimized list of failed assumption for the last
+
 * call to 'picosat_sat'.  The pointer is valid until the next call to this
+
 * function or 'picosat_sat' or 'picosat_mus_assumptions'.  It only makes sense
+
 * if the last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'.
+
 *
+
 * The call back function is called for all successful simplification
+
 * attempts.  The first argument of the call back function is the state
+
 * given as first argument to 'picosat_mus_assumptions'.  The second
+
 * argument to the call back function is the new reduced list of failed
+
 * assumptions.
+
 *
+
 * This function will call 'picosat_assume' and 'picosat_sat' internally but
+
 * before returning reestablish a proper UNSAT state, e.g.
+
 * 'picosat_failed_assumption' will work afterwards as expected.
+
 *
+
 * The last argument if non zero fixes assumptions.  In particular, if an
+
 * assumption can not be removed it is permanently assigned true, otherwise
+
 * if it turns out to be redundant it is permanently assumed to be false.
+
 */
+
const int * picosat_mus_assumptions (PicoSAT *, void *,
+
                                     void(*)(void*,const int*),int);
+

+
/* Compute one maximal subset of satisfiable assumptions.  You need to set
+
 * the assumptions, call 'picosat_sat' and check for 'picosat_inconsistent',
+
 * before calling this function.  The result is a zero terminated array of
+
 * assumptions that consistently can be asserted at the same time.  Before
+
 * returing the library 'reassumes' all assumptions.
+
 *
+
 * It could be beneficial to set the default phase of assumptions
+
 * to true (positive).  This can speed up the computation.
+
 */
+
const int * picosat_maximal_satisfiable_subset_of_assumptions (PicoSAT *);
+

+
/* This function assumes that you have set up all assumptions with
+
 * 'picosat_assume'.  Then it calls 'picosat_sat' internally unless the
+
 * formula is already inconsistent without assumptions, i.e.  it contains
+
 * the empty clause.  After that it extracts a maximal satisfiable subset of
+
 * assumptions.
+
 *
+
 * The result is a zero terminated maximal subset of consistent assumptions
+
 * or a zero pointer if the formula contains the empty clause and thus no
+
 * more maximal consistent subsets of assumptions can be extracted.  In the
+
 * first case, before returning, a blocking clause is added, that rules out
+
 * the result for the next call.
+
 *
+
 * NOTE: adding the blocking clause changes the CNF.
+
 *
+
 * So the following idiom
+
 *
+
 * const int * mss;
+
 * picosat_assume (a1);
+
 * picosat_assume (a2);
+
 * picosat_assume (a3);
+
 * picosat_assume (a4);
+
 * while ((mss = picosat_next_maximal_satisfiable_subset_of_assumptions ()))
+
 *   process_mss (mss);
+
 *
+
 * can be used to iterate over all maximal consistent subsets of
+
 * the set of assumptions {a1,a2,a3,a4}.
+
 *
+
 * It could be beneficial to set the default phase of assumptions
+
 * to true (positive).  This might speed up the computation.
+
 */
+
const int * 
+
picosat_next_maximal_satisfiable_subset_of_assumptions (PicoSAT *);
+

+
/* Similarly we can iterate over all minimal correcting assumption sets.
+
 * See the CAMUS literature [M. Liffiton, K. Sakallah JAR 2008].
+
 *
+
 * The result contains each assumed literal only once, even if it
+
 * was assumed multiple times (in contrast to the maximal consistent
+
 * subset functions above).
+
 *
+
 * It could be beneficial to set the default phase of assumptions
+
 * to true (positive).  This might speed up the computation.
+
 */
+
const int *
+
picosat_next_minimal_correcting_subset_of_assumptions (PicoSAT *);
+

+
/* Compute the union of all minmal correcting sets, which is called
+
 * the 'high level union of all minimal unsatisfiable subset sets'
+
 * or 'HUMUS' in our papers.
+
 *
+
 * It uses 'picosat_next_minimal_correcting_subset_of_assumptions' and
+
 * the same notes and advices apply.  In particular, this implies that
+
 * after calling the function once, the current CNF becomes inconsistent,
+
 * and PicoSAT has to be reset.  So even this function internally uses
+
 * PicoSAT incrementally, it can not be used incrementally itself at this
+
 * point.
+
 *
+
 * The 'callback' can be used for progress logging and is called after
+
 * each extracted minimal correcting set if non zero.  The 'nhumus'
+
 * parameter of 'callback' denotes the number of assumptions found to be
+
 * part of the HUMUS sofar.
+
 */
+
const int *
+
picosat_humus (PicoSAT *,
+
               void (*callback)(void * state, int nmcs, int nhumus),
+
	       void * state);
+

+
/*------------------------------------------------------------------------*/
+
/* Assume that a previous call to 'picosat_sat' in incremental usage,
+
 * returned 'SATISFIABLE'.  Then a couple of clauses and optionally new
+
 * variables were added (a new variable is a variable that has an index
+
 * larger then the maximum variable added so far).  The next call to
+
 * 'picosat_sat' also returns 'SATISFIABLE'. If this function
+
 * 'picosat_changed' returns '0', then the assignment to the old variables
+
 * is guaranteed to not have changed.  Otherwise it might have changed.
+
 * 
+
 * The return value to this function is only valid until new clauses are
+
 * added through 'picosat_add', an assumption is made through
+
 * 'picosat_assume', or again 'picosat_sat' is called.  This is the same
+
 * assumption as for 'picosat_deref'.
+
 *
+
 * TODO currently this function might also return a non zero value even if
+
 * the old assignment did not change, because it only checks whether the
+
 * assignment of at least one old variable was flipped at least once during
+
 * the search.  In principle it should be possible to be exact in the other
+
 * direction as well by using a counter of variables that have an odd number
+
 * of flips.  But this is not implemented yet.
+
 */
+
int picosat_changed (PicoSAT *);
+

+
/*------------------------------------------------------------------------*/
+
/* The following six functions internally extract the variable and clausal
+
 * core and thus require trace generation to be enabled with
+
 * 'picosat_enable_trace_generation' right after calling 'picosat_init'.
+
 *
+
 * TODO: using these functions in incremental mode with failed assumptions
+
 * has only been tested for 'picosat_corelit' thoroughly.  The others
+
 * probably only work in non-incremental mode or without using
+
 * 'picosat_assume'.
+
 */
+

+
/* This function determines whether the i'th added original clause is in the
+
 * core.  The 'i' is the return value of 'picosat_add', which starts at zero
+
 * and is incremented by one after a original clause is added (that is after
+
 * 'picosat_add (0)').  For the index 'i' the following has to hold: 
+
 *
+
 *   0 <= i < picosat_added_original_clauses ()
+
 */
+
int picosat_coreclause (PicoSAT *, int i);
+

+
/* This function gives access to the variable core, which is made up of the
+
 * variables that were resolved in deriving the empty clause.
+
 */
+
int picosat_corelit (PicoSAT *, int lit);
+

+
/* Write the clauses that were used in deriving the empty clause to a file
+
 * in DIMACS format.
+
 */
+
void picosat_write_clausal_core (PicoSAT *, FILE * core_file);
+

+
/* Write a proof trace in TraceCheck format to a file.
+
 */
+
void picosat_write_compact_trace (PicoSAT *, FILE * trace_file);
+
void picosat_write_extended_trace (PicoSAT *, FILE * trace_file);
+

+
/* Write a RUP trace to a file.  This trace file contains only the learned
+
 * core clauses while this is not necessarily the case for the RUP file
+
 * obtained with 'picosat_set_incremental_rup_file'.
+
 */
+
void picosat_write_rup_trace (PicoSAT *, FILE * trace_file);
+

+
/*------------------------------------------------------------------------*/
+
/* Keeping the proof trace around is not necessary if an over-approximation
+
 * of the core is enough.  A literal is 'used' if it was involved in a
+
 * resolution to derive a learned clause.  The core literals are necessarily
+
 * a subset of the 'used' literals.
+
 */
+

+
int picosat_usedlit (PicoSAT *, int lit);
+
/*------------------------------------------------------------------------*/
+
#endif
added external/picosat/version.c
@@ -0,0 +1,14 @@
+
#include "config.h"
+

+
const char *
+
picosat_version (void)
+
{
+
  return PICOSAT_VERSION;
+
}
+

+
const char *
+
picosat_config (void)
+
{
+
  return PICOSAT_CC " " PICOSAT_CFLAGS;
+
}
+

modified libpkg/Makefile.am
@@ -6,6 +6,7 @@ pkg_common_cflags= -I$(top_srcdir)/libpkg \
			-I$(top_srcdir)/external/libsbuf \
			-I$(top_srcdir)/external/expat/lib \
			-I$(top_srcdir)/external/libucl/include \
+
			-I$(top_srcdir)/external/picosat \
			-I$(top_srcdir)/external/uthash \
			-I$(top_srcdir)/external/sqlite \
			-I$(top_srcdir)/external/libyaml/include \
@@ -57,6 +58,7 @@ libpkg_la_LIBADD= $(top_builddir)/external/libucl.la \
			$(top_builddir)/external/libyaml.la \
			$(top_builddir)/external/libexpat.la \
			$(top_builddir)/external/libsbuf.la \
+
			$(top_builddir)/external/libpicosat.la \
			@REPOS_LDADD@ \
			@LIBELF_LIB@ \
			@LIBEXECINFO_LIB@ \
@@ -78,6 +80,7 @@ libpkg_static_la_CFLAGS= $(pkg_common_cflags) -static
libpkg_static_la_LIBADD=	$(top_builddir)/external/libucl_static.la \
			$(top_builddir)/external/libsqlite_static.la \
			$(top_builddir)/external/libexpat_static.la \
+
			$(top_builddir)/external/libpicosat_static.la \
			$(top_builddir)/external/libyaml_static.la \
			$(top_builddir)/external/libsbuf_static.la \
			@REPOS_LDADD_STATIC@