diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
commit | 1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (patch) | |
tree | 210ffc156c83f04fb0c61a40b4f9037d7ba8a7e1 /test/monniaux/picosat-965/picosat.c | |
parent | 222c9047d61961db9c6b19fed5ca49829223fd33 (diff) | |
parent | 12be46d59a2483a10d77fa8ee67f7e0ca1bd702f (diff) | |
download | compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.tar.gz compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.zip |
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'test/monniaux/picosat-965/picosat.c')
-rw-r--r-- | test/monniaux/picosat-965/picosat.c | 8508 |
1 files changed, 8508 insertions, 0 deletions
diff --git a/test/monniaux/picosat-965/picosat.c b/test/monniaux/picosat-965/picosat.c new file mode 100644 index 00000000..21442f44 --- /dev/null +++ b/test/monniaux/picosat-965/picosat.c @@ -0,0 +1,8508 @@ +/**************************************************************************** +Copyright (c) 2006 - 2015, Armin Biere, Johannes Kepler University. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to +deal in the Software without restriction, including without limitation the +rights to use, copy, modify, merge, publish, distribute, sublicense, and/or +sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS +IN THE SOFTWARE. +****************************************************************************/ + +#include <stdlib.h> +#include <stdio.h> +#include <string.h> +#include <assert.h> +#include <limits.h> +#include <ctype.h> +#include <stdarg.h> +#include <stdint.h> + +#include "picosat.h" + +#define INLINE inline + +/* By default code for 'all different constraints' is disabled, since 'NADC' + * is defined. + */ +#define NADC + +/* By default we enable failed literals, since 'NFL' is undefined. + * +#define NFL + */ + +/* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined. + * +#define NDSC + */ + +/* Do not use luby restart schedule instead of inner/outer. + * +#define NLUBY + */ + +/* Enabling this define, will use gnuplot to visualize how the scores evolve. + * +#define VISCORES + */ + +#ifdef VISCORES +// #define WRITEGIF /* ... to generate a video */ +#endif + +#ifdef VISCORES +#ifndef WRITEGIF +#include <unistd.h> /* for 'usleep' */ +#endif +#endif + +#ifdef RCODE +#include <R.h> +#endif + +#define MINRESTART 100 /* minimum restart interval */ +#define MAXRESTART 1000000 /* maximum restart interval */ +#define RDECIDE 1000 /* interval of random decisions */ +#define FRESTART 110 /* restart increase factor in percent */ +#define FREDUCE 110 /* reduce increase factor in percent */ +#define FREDADJ 121 /* reduce increase adjustment factor */ +#define MAXCILS 10 /* maximal number of unrecycled internals */ +#define FFLIPPED 10000 /* flipped reduce factor */ +#define FFLIPPEDPREC 10000000/* flipped reduce factor precision */ +#define INTERRUPTLIM 1024 /* check interrupt after that many decisions */ + +#ifndef TRACE +#define NO_BINARY_CLAUSES /* store binary clauses more compactly */ +#endif + +/* For debugging purposes you may want to define 'LOGGING', which actually + * can be enforced by using './configure.sh --log'. + */ +#ifdef LOGGING +#define LOG(code) do { code; } while (0) +#else +#define LOG(code) do { } while (0) +#endif +#define NOLOG(code) do { } while (0) /* log exception */ +#define ONLYLOG(code) do { code; } while (0) /* force logging */ + +#define FALSE ((Val)-1) +#define UNDEF ((Val)0) +#define TRUE ((Val)1) + +#define COMPACT_TRACECHECK_TRACE_FMT 0 +#define EXTENDED_TRACECHECK_TRACE_FMT 1 +#define RUP_TRACE_FMT 2 + +#define NEWN(p,n) do { (p) = new (ps, sizeof (*(p)) * (n)); } while (0) +#define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0) +#define CLR(p) CLRN(p,1) +#define DELETEN(p,n) \ + do { delete (ps, p, sizeof (*(p)) * (n)); (p) = 0; } while (0) + +#define RESIZEN(p,old_num,new_num) \ + do { \ + size_t old_size = sizeof (*(p)) * (old_num); \ + size_t new_size = sizeof (*(p)) * (new_num); \ + (p) = resize (ps, (p), old_size, new_size) ; \ + } while (0) + +#define ENLARGE(start,head,end) \ + do { \ + unsigned old_num = (ptrdiff_t)((end) - (start)); \ + size_t new_num = old_num ? (2 * old_num) : 1; \ + unsigned count = (head) - (start); \ + assert ((start) <= (end)); \ + RESIZEN((start),old_num,new_num); \ + (head) = (start) + count; \ + (end) = (start) + new_num; \ + } while (0) + +#define NOTLIT(l) (ps->lits + (1 ^ ((l) - ps->lits))) + +#define LIT2IDX(l) ((ptrdiff_t)((l) - ps->lits) / 2) +#define LIT2IMPLS(l) (ps->impls + (ptrdiff_t)((l) - ps->lits)) +#define LIT2INT(l) ((int)(LIT2SGN(l) * LIT2IDX(l))) +#define LIT2SGN(l) (((ptrdiff_t)((l) - ps->lits) & 1) ? -1 : 1) +#define LIT2VAR(l) (ps->vars + LIT2IDX(l)) +#define LIT2HTPS(l) (ps->htps + (ptrdiff_t)((l) - ps->lits)) +#define LIT2JWH(l) (ps->jwh + ((l) - ps->lits)) + +#ifndef NDSC +#define LIT2DHTPS(l) (ps->dhtps + (ptrdiff_t)((l) - ps->lits)) +#endif + +#ifdef NO_BINARY_CLAUSES +typedef uintptr_t Wrd; +#define ISLITREASON(C) (1&(Wrd)C) +#define LIT2REASON(L) \ + (assert (L->val==TRUE), ((Cls*)(1 + (2*(L - ps->lits))))) +#define REASON2LIT(C) ((Lit*)(ps->lits + ((Wrd)C)/2)) +#endif + +#define ENDOFCLS(c) ((void*)((Lit**)(c)->lits + (c)->size)) + +#define SOC ((ps->oclauses == ps->ohead) ? ps->lclauses : ps->oclauses) +#define EOC (ps->lhead) +#define NXC(p) (((p) + 1 == ps->ohead) ? ps->lclauses : (p) + 1) + +#define OIDX2IDX(idx) (2 * ((idx) + 1)) +#define LIDX2IDX(idx) (2 * (idx) + 1) + +#define ISLIDX(idx) ((idx)&1) + +#define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1) +#define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2) + +#define EXPORTIDX(idx) \ + ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ps->ohead - ps->oclauses)) : IDX2OIDX(idx)) + 1) + +#define IDX2CLS(i) \ + (assert(i), (ISLIDX(i) ? ps->lclauses : ps->oclauses)[(i)/2 - !ISLIDX(i)]) + +#define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? ps->zhains[(i)/2] : 0)) + +#define CLS2TRD(c) (((Trd*)(c)) - 1) +#define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx) + +#define CLS2ACT(c) \ + ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c))) + +#define VAR2LIT(v) (ps->lits + 2 * ((v) - ps->vars)) +#define VAR2RNK(v) (ps->rnks + ((v) - ps->vars)) + +#define RNK2LIT(r) (ps->lits + 2 * ((r) - ps->rnks)) +#define RNK2VAR(r) (ps->vars + ((r) - ps->rnks)) + +#define BLK_FILL_BYTES 8 +#define SIZE_OF_BLK (sizeof (Blk) - BLK_FILL_BYTES) + +#define PTR2BLK(void_ptr) \ + ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - SIZE_OF_BLK) : 0) + +#define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0) +#define PERCENT(a,b) (100.0 * AVERAGE(a,b)) + +#ifndef RCODE +#define ABORT(msg) \ + do { \ + fputs ("*** picosat: " msg "\n", stderr); \ + abort (); \ + } while (0) +#else +#define ABORT(msg) \ + do { \ + Rf_error (msg); \ + } while (0) +#endif + +#define ABORTIF(cond,msg) \ + do { \ + if (!(cond)) break; \ + ABORT (msg); \ + } while (0) + +#define ZEROFLT (0x00000000u) +#define EPSFLT (0x00000001u) +#define INFFLT (0xffffffffu) + +#define FLTCARRY (1u << 25) +#define FLTMSB (1u << 24) +#define FLTMAXMANTISSA (FLTMSB - 1) + +#define FLTMANTISSA(d) ((d) & FLTMAXMANTISSA) +#define FLTEXPONENT(d) ((int)((d) >> 24) - 128) + +#define FLTMINEXPONENT (-128) +#define FLTMAXEXPONENT (127) + +#define CMPSWAPFLT(a,b) \ + do { \ + Flt tmp; \ + if (((a) < (b))) \ + { \ + tmp = (a); \ + (a) = (b); \ + (b) = tmp; \ + } \ + } while (0) + +#define UNPACKFLT(u,m,e) \ + do { \ + (m) = FLTMANTISSA(u); \ + (e) = FLTEXPONENT(u); \ + (m) |= FLTMSB; \ + } while (0) + +#define INSERTION_SORT_LIMIT 10 + +#define SORTING_SWAP(T,p,q) \ +do { \ + T tmp = *(q); \ + *(q) = *(p); \ + *(p) = tmp; \ +} while (0) + +#define SORTING_CMP_SWAP(T,cmp,p,q) \ +do { \ + if ((cmp) (ps, *(p), *(q)) > 0) \ + SORTING_SWAP (T, p, q); \ +} while(0) + +#define QUICKSORT_PARTITION(T,cmp,a,l,r) \ +do { \ + T pivot; \ + int j; \ + i = (l) - 1; /* result in 'i' */ \ + j = (r); \ + pivot = (a)[j]; \ + for (;;) \ + { \ + while ((cmp) (ps, (a)[++i], pivot) < 0) \ + ; \ + while ((cmp) (ps, pivot, (a)[--j]) < 0) \ + if (j == (l)) \ + break; \ + if (i >= j) \ + break; \ + SORTING_SWAP (T, (a) + i, (a) + j); \ + } \ + SORTING_SWAP (T, (a) + i, (a) + (r)); \ +} while(0) + +#define QUICKSORT(T,cmp,a,n) \ +do { \ + int l = 0, r = (n) - 1, m, ll, rr, i; \ + assert (ps->ihead == ps->indices); \ + if (r - l <= INSERTION_SORT_LIMIT) \ + break; \ + for (;;) \ + { \ + m = (l + r) / 2; \ + SORTING_SWAP (T, (a) + m, (a) + r - 1); \ + SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r - 1); \ + SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r); \ + SORTING_CMP_SWAP (T, cmp, (a) + r - 1, (a) + r); \ + QUICKSORT_PARTITION (T, cmp, (a), l + 1, r - 1); \ + if (i - l < r - i) \ + { \ + ll = i + 1; \ + rr = r; \ + r = i - 1; \ + } \ + else \ + { \ + ll = l; \ + rr = i - 1; \ + l = i + 1; \ + } \ + if (r - l > INSERTION_SORT_LIMIT) \ + { \ + assert (rr - ll > INSERTION_SORT_LIMIT); \ + if (ps->ihead == ps->eoi) \ + ENLARGE (ps->indices, ps->ihead, ps->eoi); \ + *ps->ihead++ = ll; \ + if (ps->ihead == ps->eoi) \ + ENLARGE (ps->indices, ps->ihead, ps->eoi); \ + *ps->ihead++ = rr; \ + } \ + else if (rr - ll > INSERTION_SORT_LIMIT) \ + { \ + l = ll; \ + r = rr; \ + } \ + else if (ps->ihead > ps->indices) \ + { \ + r = *--ps->ihead; \ + l = *--ps->ihead; \ + } \ + else \ + break; \ + } \ +} while (0) + +#define INSERTION_SORT(T,cmp,a,n) \ +do { \ + T pivot; \ + int l = 0, r = (n) - 1, i, j; \ + for (i = r; i > l; i--) \ + SORTING_CMP_SWAP (T, cmp, (a) + i - 1, (a) + i); \ + for (i = l + 2; i <= r; i++) \ + { \ + j = i; \ + pivot = (a)[i]; \ + while ((cmp) (ps, pivot, (a)[j - 1]) < 0) \ + { \ + (a)[j] = (a)[j - 1]; \ + j--; \ + } \ + (a)[j] = pivot; \ + } \ +} while (0) + +#ifdef NDEBUG +#define CHECK_SORTED(cmp,a,n) do { } while(0) +#else +#define CHECK_SORTED(cmp,a,n) \ +do { \ + int i; \ + for (i = 0; i < (n) - 1; i++) \ + assert ((cmp) (ps, (a)[i], (a)[i + 1]) <= 0); \ +} while(0) +#endif + +#define SORT(T,cmp,a,n) \ +do { \ + T * aa = (a); \ + int nn = (n); \ + QUICKSORT (T, cmp, aa, nn); \ + INSERTION_SORT (T, cmp, aa, nn); \ + assert (ps->ihead == ps->indices); \ + CHECK_SORTED (cmp, aa, nn); \ +} while (0) + +#define WRDSZ (sizeof (long) * 8) + +#ifdef RCODE +#define fprintf(...) do { } while (0) +#define vfprintf(...) do { } while (0) +#define fputs(...) do { } while (0) +#define fputc(...) do { } while (0) +#endif + +typedef unsigned Flt; /* 32 bit deterministic soft float */ +typedef Flt Act; /* clause and variable activity */ +typedef struct Blk Blk; /* allocated memory block */ +typedef struct Cls Cls; /* clause */ +typedef struct Lit Lit; /* literal */ +typedef struct Rnk Rnk; /* variable to score mapping */ +typedef signed char Val; /* TRUE, UNDEF, FALSE */ +typedef struct Var Var; /* variable */ +#ifdef TRACE +typedef struct Trd Trd; /* trace data for clauses */ +typedef struct Zhn Zhn; /* compressed chain (=zain) data */ +typedef unsigned char Znt; /* compressed antecedent data */ +#endif + +#ifdef NO_BINARY_CLAUSES +typedef struct Ltk Ltk; + +struct Ltk +{ + Lit ** start; + unsigned count : WRDSZ == 32 ? 27 : 32; + unsigned ldsize : WRDSZ == 32 ? 5 : 32; +}; +#endif + +struct Lit +{ + Val val; +}; + +struct Var +{ + unsigned mark : 1; /*bit 1*/ + unsigned resolved : 1; /*bit 2*/ + unsigned phase : 1; /*bit 3*/ + unsigned assigned : 1; /*bit 4*/ + unsigned used : 1; /*bit 5*/ + unsigned failed : 1; /*bit 6*/ + unsigned internal : 1; /*bit 7*/ + unsigned usedefphase : 1; /*bit 8*/ + unsigned defphase : 1; /*bit 9*/ + unsigned msspos : 1; /*bit 10*/ + unsigned mssneg : 1; /*bit 11*/ + unsigned humuspos : 1; /*bit 12*/ + unsigned humusneg : 1; /*bit 13*/ + unsigned partial : 1; /*bit 14*/ +#ifdef TRACE + unsigned core : 1; /*bit 15*/ +#endif + unsigned level; + Cls *reason; +#ifndef NADC + Lit ** inado; + Lit ** ado; + Lit *** adotabpos; +#endif +}; + +struct Rnk +{ + Act score; + unsigned pos : 30; /* 0 iff not on heap */ + unsigned moreimportant : 1; + unsigned lessimportant : 1; +}; + +struct Cls +{ + unsigned size; + + unsigned collect:1; /* bit 1 */ + unsigned learned:1; /* bit 2 */ + unsigned locked:1; /* bit 3 */ + unsigned used:1; /* bit 4 */ +#ifndef NDEBUG + unsigned connected:1; /* bit 5 */ +#endif +#ifdef TRACE + unsigned collected:1; /* bit 6 */ + unsigned core:1; /* bit 7 */ +#endif + +#define LDMAXGLUE 25 /* 32 - 7 */ +#define MAXGLUE ((1<<LDMAXGLUE)-1) + + unsigned glue:LDMAXGLUE; + + Cls *next[2]; + Lit *lits[2]; +}; + +#ifdef TRACE +struct Zhn +{ + unsigned ref:31; + unsigned core:1; + Znt * liz; + Znt znt[0]; +}; + +struct Trd +{ + unsigned idx; + Cls cls[0]; +}; +#endif + +struct Blk +{ +#ifndef NDEBUG + union + { + size_t size; /* this is what we really use */ + void *as_two_ptrs[2]; /* 2 * sizeof (void*) alignment of data */ + } + header; +#endif + char data[BLK_FILL_BYTES]; +}; + +enum State +{ + RESET = 0, + READY = 1, + SAT = 2, + UNSAT = 3, + UNKNOWN = 4, +}; + +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; + + struct { + void * state; + int (*function) (void *); + } interrupt; + +#ifdef VISCORES + FILE * fviscores; +#endif +}; + +typedef PicoSAT PS; + +static INLINE Flt +packflt (unsigned m, int e) +{ + Flt res; + assert (m < FLTMSB); + assert (FLTMINEXPONENT <= e); + assert (e <= FLTMAXEXPONENT); + res = m | ((unsigned)(e + 128) << 24); + return res; +} + +static Flt +base2flt (unsigned m, int e) +{ + if (!m) + return ZEROFLT; + + if (m < FLTMSB) + { + do + { + if (e <= FLTMINEXPONENT) + return EPSFLT; + + e--; + m <<= 1; + + } + while (m < FLTMSB); + } + else + { + while (m >= FLTCARRY) + { + if (e >= FLTMAXEXPONENT) + return INFFLT; + + e++; + m >>= 1; + } + } + + m &= ~FLTMSB; + return packflt (m, e); +} + +static Flt +addflt (Flt a, Flt b) +{ + unsigned ma, mb, delta; + int ea, eb; + + CMPSWAPFLT (a, b); + if (!b) + return a; + + UNPACKFLT (a, ma, ea); + UNPACKFLT (b, mb, eb); + + assert (ea >= eb); + delta = ea - eb; + if (delta < 32) mb >>= delta; else mb = 0; + if (!mb) + return a; + + ma += mb; + if (ma & FLTCARRY) + { + if (ea == FLTMAXEXPONENT) + return INFFLT; + + ea++; + ma >>= 1; + } + + assert (ma < FLTCARRY); + ma &= FLTMAXMANTISSA; + + return packflt (ma, ea); +} + +static Flt +mulflt (Flt a, Flt b) +{ + unsigned ma, mb; + unsigned long long accu; + int ea, eb; + + CMPSWAPFLT (a, b); + if (!b) + return ZEROFLT; + + UNPACKFLT (a, ma, ea); + UNPACKFLT (b, mb, eb); + + ea += eb; + ea += 24; + if (ea > FLTMAXEXPONENT) + return INFFLT; + + if (ea < FLTMINEXPONENT) + return EPSFLT; + + accu = ma; + accu *= mb; + accu >>= 24; + + if (accu >= FLTCARRY) + { + if (ea == FLTMAXEXPONENT) + return INFFLT; + + ea++; + accu >>= 1; + + if (accu >= FLTCARRY) + return INFFLT; + } + + assert (accu < FLTCARRY); + assert (accu & FLTMSB); + + ma = accu; + ma &= ~FLTMSB; + + return packflt (ma, ea); +} + +static Flt +ascii2flt (const char *str) +{ + Flt ten = base2flt (10, 0); + Flt onetenth = base2flt (26843546, -28); + Flt res = ZEROFLT, tmp, base; + const char *p = str; + int ch; + + ch = *p++; + + if (ch != '.') + { + if (!isdigit (ch)) + return INFFLT; /* better abort ? */ + + res = base2flt (ch - '0', 0); + + while ((ch = *p++)) + { + if (ch == '.') + break; + + if (!isdigit (ch)) + return INFFLT; /* better abort? */ + + res = mulflt (res, ten); + tmp = base2flt (ch - '0', 0); + res = addflt (res, tmp); + } + } + + if (ch == '.') + { + ch = *p++; + if (!isdigit (ch)) + return INFFLT; /* better abort ? */ + + base = onetenth; + tmp = mulflt (base2flt (ch - '0', 0), base); + res = addflt (res, tmp); + + while ((ch = *p++)) + { + if (!isdigit (ch)) + return INFFLT; /* better abort? */ + + base = mulflt (base, onetenth); + tmp = mulflt (base2flt (ch - '0', 0), base); + res = addflt (res, tmp); + } + } + + return res; +} + +#if defined(VISCORES) + +static double +flt2double (Flt f) +{ + double res; + unsigned m; + int e, i; + + UNPACKFLT (f, m, e); + res = m; + + if (e < 0) + { + for (i = e; i < 0; i++) + res *= 0.5; + } + else + { + for (i = 0; i < e; i++) + res *= 2.0; + } + + return res; +} + +#endif + +static INLINE int +log2flt (Flt a) +{ + return FLTEXPONENT (a) + 24; +} + +static INLINE 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 INLINE unsigned +int2unsigned (int l) +{ + return (l < 0) ? 1 + 2 * -l : 2 * l; +} + +static INLINE Lit * +int2lit (PS * ps, int l) +{ + return ps->lits + int2unsigned (l); +} + +static INLINE Lit ** +end_of_lits (Cls * c) +{ + return (Lit**)c->lits + c->size; +} + +#if !defined(NDEBUG) || defined(LOGGING) + +static void +dumplits (PS * ps, Lit ** l, Lit ** end) +{ + int first; + Lit ** p; + + if (l == end) + { + /* empty clause */ + } + else if (l + 1 == end) + { + fprintf (ps->out, "%d ", LIT2INT (l[0])); + } + else + { + assert (l + 2 <= end); + first = (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1]))); + fprintf (ps->out, "%d ", LIT2INT (l[first])); + fprintf (ps->out, "%d ", LIT2INT (l[!first])); + for (p = l + 2; p < end; p++) + fprintf (ps->out, "%d ", LIT2INT (*p)); + } + + fputc ('0', ps->out); +} + +static void +dumpcls (PS * ps, Cls * c) +{ + Lit **end; + + if (c) + { + end = end_of_lits (c); + dumplits (ps, c->lits, end); +#ifdef TRACE + if (ps->trace) + fprintf (ps->out, " clause(%u)", CLS2IDX (c)); +#endif + } + else + fputs ("DECISION", ps->out); +} + +static void +dumpclsnl (PS * ps, Cls * c) +{ + dumpcls (ps, c); + fputc ('\n', ps->out); +} + +void +dumpcnf (PS * ps) +{ + Cls **p, *c; + + for (p = SOC; p != EOC; p = NXC (p)) + { + c = *p; + + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + + dumpclsnl (ps, *p); + } +} + +#endif + +static INLINE 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; + +#ifndef RCODE + ps->out = stdout; +#else + ps->out = 0; +#endif + 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) + { + Act * p = CLS2ACT (res); + *p = ps->cinc; + } + + return res; +} + +static void +delete_clause (PS * ps, Cls * c) +{ + size_t bytes; +#ifdef TRACE + Trd *trd; +#endif + + bytes = bytes_clause (ps, c->size, c->learned); + +#ifdef TRACE + if (ps->trace) + { + trd = CLS2TRD (c); + delete (ps, trd, bytes); + } + else +#endif + delete (ps, c, bytes); +} + +static void +delete_clauses (PS * ps) +{ + Cls **p; + for (p = SOC; p != EOC; p = NXC (p)) + if (*p) + delete_clause (ps, *p); + + DELETEN (ps->oclauses, ps->eoo - ps->oclauses); + DELETEN (ps->lclauses, ps->EOL - ps->lclauses); + + ps->ohead = ps->eoo = ps->lhead = ps->EOL = 0; +} + +#ifdef TRACE + +static void +delete_zhain (PS * ps, Zhn * zhain) +{ + const Znt *p, *znt; + + assert (zhain); + + znt = zhain->znt; + for (p = znt; *p; p++) + ; + + delete (ps, zhain, sizeof (Zhn) + (p - znt) + 1); +} + +static void +delete_zhains (PS * ps) +{ + Zhn **p, *z; + for (p = ps->zhains; p < ps->zhead; p++) + if ((z = *p)) + delete_zhain (ps, z); + + DELETEN (ps->zhains, ps->eoz - ps->zhains); + ps->eoz = ps->zhead = 0; +} + +#endif + +#ifdef NO_BINARY_CLAUSES +static void +lrelease (PS * ps, Ltk * stk) +{ + if (stk->start) + DELETEN (stk->start, (1 << (stk->ldsize))); + memset (stk, 0, sizeof (*stk)); +} +#endif + +#ifndef NADC + +static INLINE unsigned +llength (Lit ** a) +{ + Lit ** p; + for (p = a; *p; p++) + ; + return p - a; +} + +static INLINE void +resetadoconflict (PS * ps) +{ + assert (ps->adoconflict); + delete_clause (ps, ps->adoconflict); + ps->adoconflict = 0; +} + +static INLINE void +reset_ados (PS * ps) +{ + Lit *** p; + + for (p = ps->ados; p < ps->hados; p++) + DELETEN (*p, llength (*p) + 1); + + DELETEN (ps->ados, ps->eados - ps->ados); + ps->hados = ps->eados = 0; + + DELETEN (ps->adotab, ps->szadotab); + ps->szadotab = ps->nadotab = 0; + + if (ps->adoconflict) + resetadoconflict (ps); + + ps->adoconflicts = 0; + ps->adoconflictlimit = UINT_MAX; + ps->adodisabled = 0; +} + +#endif + +static void +reset (PS * ps) +{ + ABORTIF (!ps || + ps->state == RESET, "API usage: reset without initialization"); + + delete_clauses (ps); +#ifdef TRACE + delete_zhains (ps); +#endif +#ifdef NO_BINARY_CLAUSES + { + unsigned i; + for (i = 2; i <= 2 * ps->max_var + 1; i++) + lrelease (ps, ps->impls + i); + } +#endif +#ifndef NADC + reset_ados (ps); +#endif +#ifndef NFL + DELETEN (ps->saved, ps->saved_size); +#endif + DELETEN (ps->htps, 2 * ps->size_vars); +#ifndef NDSC + DELETEN (ps->dhtps, 2 * ps->size_vars); +#endif + DELETEN (ps->impls, 2 * ps->size_vars); + DELETEN (ps->lits, 2 * ps->size_vars); + DELETEN (ps->jwh, 2 * ps->size_vars); + DELETEN (ps->vars, ps->size_vars); + DELETEN (ps->rnks, ps->size_vars); + DELETEN (ps->trail, ps->eot - ps->trail); + DELETEN (ps->heap, ps->eoh - ps->heap); + DELETEN (ps->als, ps->eoals - ps->als); + DELETEN (ps->CLS, ps->eocls - ps->CLS); + DELETEN (ps->rils, ps->eorils - ps->rils); + DELETEN (ps->cils, ps->eocils - ps->cils); + DELETEN (ps->fals, ps->eofals - ps->fals); + DELETEN (ps->mass, ps->szmass); + DELETEN (ps->mssass, ps->szmssass); + DELETEN (ps->mcsass, ps->szmcsass); + DELETEN (ps->humus, ps->szhumus); + DELETEN (ps->added, ps->eoa - ps->added); + DELETEN (ps->marked, ps->eom - ps->marked); + DELETEN (ps->dfs, ps->eod - ps->dfs); + DELETEN (ps->resolved, ps->eor - ps->resolved); + DELETEN (ps->levels, ps->eolevels - ps->levels); + DELETEN (ps->dused, ps->eodused - ps->dused); + DELETEN (ps->buffer, ps->eob - ps->buffer); + DELETEN (ps->indices, ps->eoi - ps->indices); + DELETEN (ps->soclauses, ps->eoso - ps->soclauses); + delete_prefix (ps); + delete (ps, ps->rline[0], ps->szrline); + delete (ps, ps->rline[1], ps->szrline); + assert (getenv ("LEAK") || !ps->current_bytes); /* found leak if failing */ +#ifdef VISCORES + pclose (ps->fviscores); +#endif + if (ps->edelete) + ps->edelete (ps->emgr, ps, sizeof *ps); + else + free (ps); +} + +inline static void +tpush (PS * ps, Lit * lit) +{ + assert (ps->lits < lit && lit <= ps->lits + 2* ps->max_var + 1); + if (ps->thead == ps->eot) + { + unsigned ttail2count = ps->ttail2 - ps->trail; + unsigned ttailcount = ps->ttail - ps->trail; +#ifndef NADC + unsigned ttailadocount = ps->ttailado - ps->trail; +#endif + ENLARGE (ps->trail, ps->thead, ps->eot); + ps->ttail = ps->trail + ttailcount; + ps->ttail2 = ps->trail + ttail2count; +#ifndef NADC + ps->ttailado = ps->trail + ttailadocount; +#endif + } + + *ps->thead++ = lit; +} + +static INLINE 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 INLINE 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 INLINE 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 INLINE 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 INLINE void +resetcimpl (PS * ps) +{ + assert (ps->cimplvalid); + ps->cimplvalid = 0; +} + +#endif + +static INLINE int +cmp_ptr (PS * ps, void *l, void *k) +{ + (void) ps; + return ((char*)l) - (char*)k; /* arbitrarily already reverse */ +} + +static int +cmp_rnk (Rnk * r, Rnk * s) +{ + if (!r->moreimportant && s->moreimportant) + return -1; + + if (r->moreimportant && !s->moreimportant) + return 1; + + if (!r->lessimportant && s->lessimportant) + return 1; + + if (r->lessimportant && !s->lessimportant) + return -1; + + if (r->score < s->score) + return -1; + + if (r->score > s->score) + return 1; + + return -cmp_ptr (0, r, s); +} + +static void +hup (PS * ps, Rnk * v) +{ + int upos, vpos; + Rnk *u; + +#ifndef NFL + assert (!ps->simplifying); +#endif + + vpos = v->pos; + + assert (0 < vpos); + assert (vpos < ps->hhead - ps->heap); + assert (ps->heap[vpos] == v); + + while (vpos > 1) + { + upos = vpos / 2; + + u = ps->heap[upos]; + + if (cmp_rnk (u, v) > 0) + break; + + ps->heap[vpos] = u; + u->pos = vpos; + + vpos = upos; + } + + ps->heap[vpos] = v; + v->pos = vpos; +} + +static Cls *add_simplified_clause (PS *, int); + +inline static void +add_antecedent (PS * ps, Cls * c) +{ + assert (c); + +#ifdef NO_BINARY_CLAUSES + if (ISLITREASON (c)) + return; + + if (c == &ps->impl) + return; +#elif defined(STATS) && defined(TRACE) + ps->antecedents++; +#endif + if (ps->rhead == ps->eor) + ENLARGE (ps->resolved, ps->rhead, ps->eor); + + assert (ps->rhead < ps->eor); + *ps->rhead++ = c; +} + +#ifdef TRACE + +#ifdef NO_BINARY_CLAUSES +#error "can not combine TRACE and NO_BINARY_CLAUSES" +#endif + +#endif /* TRACE */ + +static INLINE 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 INLINE 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 INLINE 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 INLINE 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 INLINE int +cmp_resolved (PS * ps, Cls * c, Cls * d) +{ +#ifndef NDEBUG + assert (ps->trace); +#else + (void) ps; +#endif + return CLS2IDX (c) - CLS2IDX (d); +} + +static INLINE void +bpushc (PS * ps, unsigned char ch) +{ + if (ps->bhead == ps->eob) + ENLARGE (ps->buffer, ps->bhead, ps->eob); + + *ps->bhead++ = ch; +} + +static INLINE void +bpushu (PS * ps, unsigned u) +{ + while (u & ~0x7f) + { + bpushc (ps, u | 0x80); + u >>= 7; + } + + bpushc (ps, u); +} + +static INLINE 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); + *ps->hados++ = ado; + + p = ps->added; + q = ado; + u = 0; + while (p < ps->ahead) + { + lit = *p++; + v = LIT2VAR (lit); + ABORTIF (v->inado, + "internal: variable in multiple all different objects"); + v->inado = ado; + if (!u && !lit->val) + u = v; + *q++ = lit; + } + + assert (q == ado + len); + *q++ = 0; + + /* TODO simply do a conflict test as in propado */ + + ABORTIF (!u, + "internal: " + "adding fully instantiated all different object not implemented yet"); + + assert (u); + assert (u->inado == ado); + assert (!u->ado); + u->ado = ado; + + ps->ahead = ps->added; +} + +#endif + +static void +hdown (PS * ps, Rnk * r) +{ + unsigned end, rpos, cpos, opos; + Rnk *child, *other; + + assert (r->pos > 0); + assert (ps->heap[r->pos] == r); + + end = ps->hhead - ps->heap; + rpos = r->pos; + + for (;;) + { + cpos = 2 * rpos; + if (cpos >= end) + break; + + opos = cpos + 1; + child = ps->heap[cpos]; + + if (cmp_rnk (r, child) < 0) + { + if (opos < end) + { + other = ps->heap[opos]; + + if (cmp_rnk (child, other) < 0) + { + child = other; + cpos = opos; + } + } + } + else if (opos < end) + { + child = ps->heap[opos]; + + if (cmp_rnk (r, child) >= 0) + break; + + cpos = opos; + } + else + break; + + ps->heap[rpos] = child; + child->pos = rpos; + rpos = cpos; + } + + r->pos = rpos; + ps->heap[rpos] = r; +} + +static Rnk * +htop (PS * ps) +{ + assert (ps->hhead > ps->heap + 1); + return ps->heap[1]; +} + +static Rnk * +hpop (PS * ps) +{ + Rnk *res, *last; + unsigned end; + + assert (ps->hhead > ps->heap + 1); + + res = ps->heap[1]; + res->pos = 0; + + end = --ps->hhead - ps->heap; + if (end == 1) + return res; + + last = ps->heap[end]; + + ps->heap[last->pos = 1] = last; + hdown (ps, last); + + return res; +} + +inline static void +hpush (PS * ps, Rnk * r) +{ + assert (!r->pos); + + if (ps->hhead == ps->eoh) + ENLARGE (ps->heap, ps->hhead, ps->eoh); + + r->pos = ps->hhead++ - ps->heap; + ps->heap[r->pos] = r; + hup (ps, r); +} + +static INLINE void +fix_trail_lits (PS * ps, long delta) +{ + Lit **p; + for (p = ps->trail; p < ps->thead; p++) + *p += delta; +} + +#ifdef NO_BINARY_CLAUSES +static void +fix_impl_lits (PS * ps, long delta) +{ + Ltk * s; + Lit ** p; + + for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++) + for (p = s->start; p < s->start + s->count; p++) + *p += delta; +} +#endif + +static void +fix_clause_lits (PS * ps, long delta) +{ + Cls **p, *clause; + Lit **q, *lit, **eol; + + for (p = SOC; p != EOC; p = NXC (p)) + { + clause = *p; + if (!clause) + continue; + + q = clause->lits; + eol = end_of_lits (clause); + while (q < eol) + { + assert (q - clause->lits <= (int) clause->size); + lit = *q; + lit += delta; + *q++ = lit; + } + } +} + +static INLINE void +fix_added_lits (PS * ps, long delta) +{ + Lit **p; + for (p = ps->added; p < ps->ahead; p++) + *p += delta; +} + +static INLINE void +fix_assumed_lits (PS * ps, long delta) +{ + Lit **p; + for (p = ps->als; p < ps->alshead; p++) + *p += delta; +} + +static INLINE void +fix_cls_lits (PS * ps, long delta) +{ + Lit **p; + for (p = ps->CLS; p < ps->clshead; p++) + *p += delta; +} + +static INLINE void +fix_heap_rnks (PS * ps, long delta) +{ + Rnk **p; + + for (p = ps->heap + 1; p < ps->hhead; p++) + *p += delta; +} + +#ifndef NADC + +static INLINE void +fix_ado (long delta, Lit ** ado) +{ + Lit ** p; + for (p = ado; *p; p++) + *p += delta; +} + +static INLINE void +fix_ados (PS * ps, long delta) +{ + Lit *** p; + + for (p = ps->ados; p < ps->hados; p++) + fix_ado (delta, *p); +} + +#endif + +static void +enlarge (PS * ps, unsigned new_size_vars) +{ + long rnks_delta, lits_delta; + Lit *old_lits = ps->lits; + Rnk *old_rnks = ps->rnks; + + RESIZEN (ps->lits, 2 * ps->size_vars, 2 * new_size_vars); + RESIZEN (ps->jwh, 2 * ps->size_vars, 2 * new_size_vars); + RESIZEN (ps->htps, 2 * ps->size_vars, 2 * new_size_vars); +#ifndef NDSC + RESIZEN (ps->dhtps, 2 * ps->size_vars, 2 * new_size_vars); +#endif + RESIZEN (ps->impls, 2 * ps->size_vars, 2 * new_size_vars); + RESIZEN (ps->vars, ps->size_vars, new_size_vars); + RESIZEN (ps->rnks, ps->size_vars, new_size_vars); + + if ((lits_delta = ps->lits - old_lits)) + { + fix_trail_lits (ps, lits_delta); + fix_clause_lits (ps, lits_delta); + fix_added_lits (ps, lits_delta); + fix_assumed_lits (ps, lits_delta); + fix_cls_lits (ps, lits_delta); +#ifdef NO_BINARY_CLAUSES + fix_impl_lits (ps, lits_delta); +#endif +#ifndef NADC + fix_ados (ps, lits_delta); +#endif + } + + if ((rnks_delta = ps->rnks - old_rnks)) + { + fix_heap_rnks (ps, rnks_delta); + } + + assert (ps->mhead == ps->marked); + + ps->size_vars = new_size_vars; +} + +static void +unassign (PS * ps, Lit * lit) +{ + Cls *reason; + Var *v; + Rnk *r; + + assert (lit->val == TRUE); + + LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit))); + + v = LIT2VAR (lit); + reason = v->reason; + +#ifdef NO_BINARY_CLAUSES + assert (reason != &ps->impl); + if (ISLITREASON (reason)) + { + /* DO NOTHING */ + } + else +#endif + if (reason) + { + assert (reason->locked); + reason->locked = 0; + if (reason->learned && reason->size > 2) + { + assert (ps->llocked > 0); + ps->llocked--; + } + } + + lit->val = UNDEF; + NOTLIT (lit)->val = UNDEF; + + r = VAR2RNK (v); + if (!r->pos) + hpush (ps, r); + +#ifndef NDSC + { + Cls * p, * next, ** q; + + q = LIT2DHTPS (lit); + p = *q; + *q = 0; + + while (p) + { + Lit * other = p->lits[0]; + + if (other == lit) + { + other = p->lits[1]; + q = p->next + 1; + } + else + { + assert (p->lits[1] == lit); + q = p->next; + } + + next = *q; + *q = *LIT2HTPS (other); + *LIT2HTPS (other) = p; + p = next; + } + } +#endif + +#ifndef NADC + if (v->adotabpos) + { + assert (ps->nadotab); + assert (*v->adotabpos == v->ado); + + *v->adotabpos = 0; + v->adotabpos = 0; + + ps->nadotab--; + } +#endif +} + +static Cls * +var2reason (PS * ps, Var * var) +{ + Cls * res = var->reason; +#ifdef NO_BINARY_CLAUSES + Lit * this, * other; + if (ISLITREASON (res)) + { + this = VAR2LIT (var); + if (this->val == FALSE) + this = NOTLIT (this); + + other = REASON2LIT (res); + assert (other->val == TRUE); + assert (this->val == TRUE); + res = setimpl (ps, NOTLIT (other), this); + } +#else + (void) ps; +#endif + return res; +} + +static INLINE 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) +{ +#ifdef HAS_FLOAT + double now = picosat_time_stamp (); + double delta = now - ps->entered; + delta = (delta < 0) ? 0 : delta; + ps->seconds += delta; + ps->entered = now; +#endif +} + +static double +mb (PS * ps) +{ + return ps->current_bytes / (double) (1 << 20); +} + +static INLINE double +avglevel (PS * ps) +{ + return ps->decisions ? ps->levelsum / ps->decisions : 0.0; +} + +static void +rheader (PS * ps) +{ + assert (ps->lastrheader <= ps->reports); + + if (ps->lastrheader == ps->reports) + return; + + ps->lastrheader = ps->reports; + + fprintf (ps->out, "%s\n", ps->prefix); + fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]); + fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]); + fprintf (ps->out, "%s\n", ps->prefix); +} + +static unsigned +dynamic_flips_per_assignment_per_mille (PS * ps) +{ + assert (FFLIPPEDPREC >= 1000); + return ps->sdflips / (FFLIPPEDPREC / 1000); +} + +#ifdef NLUBY + +static int +high_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >= 200; +} + +static int +very_high_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >= 250; +} + +#else + +static int +medium_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >= 230; +} + +#endif + +static void +relemdata (PS * ps) +{ + char *p; + int x; + + if (ps->reports < 0) + { + /* strip trailing white space + */ + for (x = 0; x <= 1; x++) + { + p = ps->rline[x] + strlen (ps->rline[x]); + while (p-- > ps->rline[x]) + { + if (*p != ' ') + break; + + *p = 0; + } + } + + rheader (ps); + } + else + fputc ('\n', ps->out); + + ps->RCOUNT = 0; +} + +static void +relemhead (PS * ps, const char * name, int fp, double val) +{ + int x, y, len, size; + const char *fmt; + unsigned tmp, e; + + if (ps->reports < 0) + { + x = ps->RCOUNT & 1; + y = (ps->RCOUNT / 2) * 12 + x * 6; + + if (ps->RCOUNT == 1) + sprintf (ps->rline[1], "%6s", ""); + + len = strlen (name); + while (ps->szrline <= len + y + 1) + { + size = ps->szrline ? 2 * ps->szrline : 128; + ps->rline[0] = resize (ps, ps->rline[0], ps->szrline, size); + ps->rline[1] = resize (ps, ps->rline[1], ps->szrline, size); + ps->szrline = size; + } + + fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s"; + sprintf (ps->rline[x] + y, fmt, name, ""); + } + else if (val < 0) + { + assert (fp); + + if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0) + { + fprintf (ps->out, "-%4.1f ", -tmp / 10.0); + } + else + { + tmp = -val / 10.0 + 0.5; + e = 1; + while (tmp >= 100) + { + tmp /= 10; + e++; + } + + fprintf (ps->out, "-%2ue%u ", tmp, e); + } + } + else + { + if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000) + { + fprintf (ps->out, "%5.1f ", tmp / 10.0); + } + else if (!fp && (tmp = val) < 100000) + { + fprintf (ps->out, "%5u ", tmp); + } + else + { + tmp = val / 10.0 + 0.5; + e = 1; + + while (tmp >= 1000) + { + tmp /= 10; + e++; + } + + fprintf (ps->out, "%3ue%u ", tmp, e); + } + } + + ps->RCOUNT++; +} + +inline static void +relem (PS * ps, const char *name, int fp, double val) +{ + if (name) + relemhead (ps, name, fp, val); + else + relemdata (ps); +} + +static unsigned +reduce_limit_on_lclauses (PS * ps) +{ + unsigned res = ps->lreduce; + res += ps->llocked; + return res; +} + +static void +report (PS * ps, int replevel, char type) +{ + int rounds; + +#ifdef RCODE + (void) type; +#endif + + if (ps->verbosity < replevel) + return; + + sflush (ps); + + if (!ps->reports) + ps->reports = -1; + + for (rounds = (ps->reports < 0) ? 2 : 1; rounds; rounds--) + { + if (ps->reports >= 0) + fprintf (ps->out, "%s%c ", ps->prefix, type); +#ifdef DMONNIAUX_DISABLE + + 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); +#endif + + ps->reports++; + } + + /* Adapt this to the number of rows in your terminal. + */ + #define ROWS 25 + + if (INT_MOD(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 INLINE unsigned +hashlevel (unsigned l) +{ + return 1u << (l & 31); +} + +static INLINE void +push (PS * ps, Var * v) +{ + if (ps->dhead == ps->eod) + ENLARGE (ps->dfs, ps->dhead, ps->eod); + + *ps->dhead++ = v; +} + +static INLINE Var * +pop (PS * ps) +{ + assert (ps->dfs < ps->dhead); + return *--ps->dhead; +} + +static void +analyze (PS * ps) +{ + unsigned open, minlevel, siglevels, l, old, i, orig; + Lit *this, *other, **p, **q, **eol; + Var *v, *u, **m, *start, *uip; + Cls *c; + + assert (ps->conflict); + + assert (ps->ahead == ps->added); + assert (ps->mhead == ps->marked); + assert (ps->rhead == ps->resolved); + + /* First, search for First UIP variable and mark all resolved variables. + * At the same time determine the minimum decision level involved. + * Increase activities of resolved variables. + */ + q = ps->thead; + open = 0; + minlevel = ps->LEVEL; + siglevels = 0; + uip = 0; + + c = ps->conflict; + + for (;;) + { + add_antecedent (ps, c); + inc_activity (ps, c); + eol = end_of_lits (c); + for (p = c->lits; p < eol; p++) + { + other = *p; + + if (other->val == TRUE) + continue; + + assert (other->val == FALSE); + + u = LIT2VAR (other); + if (u->mark) + continue; + + u->mark = 1; + inc_score (ps, u); + use_var (ps, u); + + if (u->level == ps->LEVEL) + { + open++; + } + else + { + push_var_as_marked (ps, u); + + if (u->level) + { + /* The statistics counter 'nonminimizedllits' sums up the + * number of literals that would be added if only the + * 'first UIP' scheme for learned clauses would be used + * and no clause minimization. + */ + ps->nonminimizedllits++; + + if (u->level < minlevel) + minlevel = u->level; + + siglevels |= hashlevel (u->level); + } + else + { + assert (!u->level); + assert (u->reason); + } + } + } + + do + { + if (q == ps->trail) + { + uip = 0; + goto DONE_FIRST_UIP; + } + + this = *--q; + uip = LIT2VAR (this); + } + while (!uip->mark); + + uip->mark = 0; + + c = var2reason (ps, uip); +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + resetimpl (ps); +#endif + open--; + if ((!open && ps->LEVEL) || !c) + break; + + assert (c); + } + +DONE_FIRST_UIP: + + if (uip) + { + assert (ps->LEVEL); + this = VAR2LIT (uip); + this += (this->val == TRUE); + ps->nonminimizedllits++; + ps->minimizedllits++; + add_lit (ps, this); +#ifdef STATS + if (uip->reason) + ps->uips++; +#endif + } + else + assert (!ps->LEVEL); + + /* Second, try to mark more intermediate variables, with the goal to + * minimize the conflict clause. This is a DFS from already marked + * variables backward through the implication graph. It tries to reach + * other marked variables. If the search reaches an unmarked decision + * variable or a variable assigned below the minimum level of variables in + * the first uip learned clause or a level on which no variable has been + * marked, then the variable from which the DFS is started is not + * redundant. Otherwise the start variable is redundant and will + * eventually be removed from the learned clause in step 4. We initially + * implemented BFS, but then profiling revelead that this step is a bottle + * neck for certain incremental applications. After switching to DFS this + * hot spot went away. + */ + orig = ps->mhead - ps->marked; + for (i = 0; i < orig; i++) + { + start = ps->marked[i]; + + assert (start->mark); + assert (start != uip); + assert (start->level < ps->LEVEL); + + if (!start->reason) + continue; + + old = ps->mhead - ps->marked; + assert (ps->dhead == ps->dfs); + push (ps, start); + + while (ps->dhead > ps->dfs) + { + u = pop (ps); + assert (u->mark); + + c = var2reason (ps, u); +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + resetimpl (ps); +#endif + if (!c || + ((l = u->level) && + (l < minlevel || ((hashlevel (l) & ~siglevels))))) + { + while (ps->mhead > ps->marked + old) /* reset all marked */ + (*--ps->mhead)->mark = 0; + + ps->dhead = ps->dfs; /* and DFS stack */ + break; + } + + eol = end_of_lits (c); + for (p = c->lits; p < eol; p++) + { + v = LIT2VAR (*p); + if (v->mark) + continue; + + mark_var (ps, v); + push (ps, v); + } + } + } + + for (m = ps->marked; m < ps->mhead; m++) + { + v = *m; + + assert (v->mark); + assert (!v->resolved); + + use_var (ps, v); + + c = var2reason (ps, v); + if (!c) + continue; + +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + resetimpl (ps); +#endif + eol = end_of_lits (c); + for (p = c->lits; p < eol; p++) + { + other = *p; + + u = LIT2VAR (other); + if (!u->level) + continue; + + if (!u->mark) /* 'MARKTEST' */ + break; + } + + if (p != eol) + continue; + + add_antecedent (ps, c); + v->resolved = 1; + } + + for (m = ps->marked; m < ps->mhead; m++) + { + v = *m; + + assert (v->mark); + v->mark = 0; + + if (v->resolved) + { + v->resolved = 0; + continue; + } + + this = VAR2LIT (v); + if (this->val == TRUE) + this++; /* actually NOTLIT */ + + add_lit (ps, this); + ps->minimizedllits++; + } + + assert (ps->ahead <= ps->eoa); + assert (ps->rhead <= ps->eor); + + ps->mhead = ps->marked; +} + +static void +fanalyze (PS * ps) +{ + Lit ** eol, ** p, * lit; + Cls * c, * reason; + Var * v, * u; + int next; + +#ifndef RCODE + double start = picosat_time_stamp (); +#endif + + assert (ps->failed_assumption); + assert (ps->failed_assumption->val == FALSE); + + v = LIT2VAR (ps->failed_assumption); + reason = var2reason (ps, v); + if (!reason) return; +#ifdef NO_BINARY_CLAUSES + if (reason == &ps->impl) + resetimpl (ps); +#endif + + eol = end_of_lits (reason); + for (p = reason->lits; p != eol; p++) + { + lit = *p; + u = LIT2VAR (lit); + if (u == v) continue; + if (u->reason) break; + } + if (p == eol) return; + + assert (ps->ahead == ps->added); + assert (ps->mhead == ps->marked); + assert (ps->rhead == ps->resolved); + + next = 0; + mark_var (ps, v); + add_lit (ps, NOTLIT (ps->failed_assumption)); + + do + { + v = ps->marked[next++]; + use_var (ps, v); + if (v->reason) + { + reason = var2reason (ps, v); +#ifdef NO_BINARY_CLAUSES + if (reason == &ps->impl) + resetimpl (ps); +#endif + add_antecedent (ps, reason); + eol = end_of_lits (reason); + for (p = reason->lits; p != eol; p++) + { + lit = *p; + u = LIT2VAR (lit); + if (u == v) continue; + if (u->mark) continue; + mark_var (ps, u); + } + } + else + { + lit = VAR2LIT (v); + if (lit->val == TRUE) lit = NOTLIT (lit); + add_lit (ps, lit); + } + } + while (ps->marked + next < ps->mhead); + + c = add_simplified_clause (ps, 1); + v = LIT2VAR (ps->failed_assumption); + reason = v->reason; +#ifdef NO_BINARY_CLAUSES + if (!ISLITREASON (reason)) +#endif + { + assert (reason->locked); + reason->locked = 0; + if (reason->learned && reason->size > 2) + { + assert (ps->llocked > 0); + ps->llocked--; + } + } + +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + { + c = impl2reason (ps, NOTLIT (ps->failed_assumption)); + } + else +#endif + { + assert (c->learned); + assert (!c->locked); + c->locked = 1; + if (c->size > 2) + { + ps->llocked++; + assert (ps->llocked > 0); + } + } + + v->reason = c; + + while (ps->mhead > ps->marked) + (*--ps->mhead)->mark = 0; + + if (ps->verbosity) + fprintf (ps->out, "%sfanalyze took %.1f seconds\n", + ps->prefix, picosat_time_stamp () - start); +} + +/* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in + * which 'this' occurs. + */ +inline static void +prop2 (PS * ps, Lit * this) +{ +#ifdef NO_BINARY_CLAUSES + Lit ** l, ** start; + Ltk * lstk; +#else + Cls * c, ** p; + Cls * next; +#endif + Lit * other; + Val tmp; + + assert (this->val == FALSE); + +#ifdef NO_BINARY_CLAUSES + lstk = LIT2IMPLS (this); + start = lstk->start; + l = start + lstk->count; + while (l != start) + { + /* The counter 'visits' is the number of clauses that are + * visited during propagations of assignments. + */ + ps->visits++; +#ifdef STATS + ps->bvisits++; +#endif + other = *--l; + tmp = other->val; + + if (tmp == TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertrue2++; + if (LIT2VAR (other)->level < ps->LEVEL) + ps->othertrue2u++; +#endif + continue; + } + + if (tmp != FALSE) + { + assign_forced (ps, other, LIT2REASON (NOTLIT(this))); + continue; + } + + if (ps->conflict == &ps->cimpl) + resetcimpl (ps); + ps->conflict = setcimpl (ps, this, other); + } +#else + /* Traverse all binary clauses with 'this'. Head/Tail pointers for binary + * clauses do not have to be modified here. + */ + p = LIT2IMPLS (this); + for (c = *p; c; c = next) + { + ps->visits++; +#ifdef STATS + ps->bvisits++; +#endif + assert (!c->collect); +#ifdef TRACE + assert (!c->collected); +#endif + assert (c->size == 2); + + other = c->lits[0]; + if (other == this) + { + next = c->next[0]; + other = c->lits[1]; + } + else + next = c->next[1]; + + tmp = other->val; + + if (tmp == TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertrue2++; + if (LIT2VAR (other)->level < ps->LEVEL) + ps->othertrue2u++; +#endif + continue; + } + + if (tmp == FALSE) + ps->conflict = c; + else + assign_forced (ps, other, c); /* unit clause */ + } +#endif /* !defined(NO_BINARY_CLAUSES) */ +} + +#ifndef NDSC +static int +should_disconnect_head_tail (PS * ps, Lit * lit) +{ + unsigned litlevel; + Var * v; + + assert (lit->val == TRUE); + + v = LIT2VAR (lit); + litlevel = v->level; + + if (!litlevel) + return 1; + +#ifndef NFL + if (ps->simplifying) + return 0; +#endif + + return litlevel < ps->LEVEL; +} +#endif + +inline static void +propl (PS * ps, Lit * this) +{ + Lit **l, *other, *prev, *new_lit, **eol; + Cls *next, **htp_ptr, **new_htp_ptr; + Cls *c; +#ifdef STATS + unsigned size; +#endif + + htp_ptr = LIT2HTPS (this); + assert (this->val == FALSE); + + /* Traverse all non binary clauses with 'this'. Head/Tail pointers are + * updated as well. + */ + for (c = *htp_ptr; c; c = next) + { + ps->visits++; +#ifdef STATS + size = c->size; + assert (size >= 3); + ps->traversals++; /* other is dereferenced at least */ + + if (size == 3) + ps->tvisits++; + else if (size >= 4) + { + ps->lvisits++; + ps->ltraversals++; + } +#endif +#ifdef TRACE + assert (!c->collected); +#endif + assert (c->size > 0); + + other = c->lits[0]; + if (other != this) + { + assert (c->size != 1); + c->lits[0] = this; + c->lits[1] = other; + next = c->next[1]; + c->next[1] = c->next[0]; + c->next[0] = next; + } + else if (c->size == 1) /* With assumptions we need to + * traverse unit clauses as well. + */ + { + assert (!ps->conflict); + ps->conflict = c; + break; + } + else + { + assert (other == this && c->size > 1); + other = c->lits[1]; + next = c->next[0]; + } + assert (other == c->lits[1]); + assert (this == c->lits[0]); + assert (next == c->next[0]); + assert (!c->collect); + + if (other->val == TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertruel++; +#endif +#ifndef NDSC + if (should_disconnect_head_tail (ps, other)) + { + new_htp_ptr = LIT2DHTPS (other); + c->next[0] = *new_htp_ptr; + *new_htp_ptr = c; +#ifdef STATS + ps->othertruelu++; +#endif + *htp_ptr = next; + continue; + } +#endif + htp_ptr = c->next; + continue; + } + + l = c->lits + 1; + eol = (Lit**) c->lits + c->size; + prev = this; + + while (++l != eol) + { +#ifdef STATS + if (size >= 3) + { + ps->traversals++; + if (size > 3) + ps->ltraversals++; + } +#endif + new_lit = *l; + *l = prev; + prev = new_lit; + if (new_lit->val != FALSE) break; + } + + if (l == eol) + { + while (l > c->lits + 2) + { + new_lit = *--l; + *l = prev; + prev = new_lit; + } + assert (c->lits[0] == this); + + assert (other == c->lits[1]); + if (other->val == FALSE) /* found conflict */ + { + assert (!ps->conflict); + ps->conflict = c; + return; + } + + assign_forced (ps, other, c); /* unit clause */ + htp_ptr = c->next; + } + else + { + assert (new_lit->val == TRUE || new_lit->val == UNDEF); + c->lits[0] = new_lit; + // *l = this; + new_htp_ptr = LIT2HTPS (new_lit); + c->next[0] = *new_htp_ptr; + *new_htp_ptr = c; + *htp_ptr = next; + } + } +} + +#ifndef NADC + +static unsigned primes[] = { 996293, 330643, 753947, 500873 }; + +#define PRIMES ((sizeof primes)/sizeof *primes) + +static unsigned +hash_ado (PS * ps, Lit ** ado, unsigned salt) +{ + unsigned i, res, tmp; + Lit ** p, * lit; + + assert (salt < PRIMES); + + i = salt; + res = 0; + + for (p = ado; (lit = *p); p++) + { + assert (lit->val); + + tmp = res >> 31; + res <<= 1; + + if (lit->val > 0) + res |= 1; + + assert (i < PRIMES); + res *= primes[i++]; + if (i == PRIMES) + i = 0; + + res += tmp; + } + + return res & (ps->szadotab - 1); +} + +static unsigned +cmp_ado (Lit ** a, Lit ** b) +{ + Lit ** p, ** q, * l, * k; + int res; + + for (p = a, q = b; (l = *p); p++, q++) + { + k = *q; + assert (k); + if ((res = (l->val - k->val))) + return res; + } + + assert (!*q); + + return 0; +} + +static Lit *** +find_ado (PS * ps, Lit ** ado) +{ + Lit *** res, ** other; + unsigned pos, delta; + + pos = hash_ado (ps, ado, 0); + assert (pos < ps->szadotab); + res = ps->adotab + pos; + + other = *res; + if (!other || !cmp_ado (other, ado)) + return res; + + delta = hash_ado (ps, ado, 1); + if (!(delta & 1)) + delta++; + + assert (delta & 1); + assert (delta < ps->szadotab); + + for (;;) + { + pos += delta; + if (pos >= ps->szadotab) + pos -= ps->szadotab; + + assert (pos < ps->szadotab); + res = ps->adotab + pos; + other = *res; + if (!other || !cmp_ado (other, ado)) + return res; + } +} + +static void +enlarge_adotab (PS * ps) +{ + /* TODO make this generic */ + + ABORTIF (ps->szadotab, + "internal: all different objects table needs larger initial size"); + assert (!ps->nadotab); + ps->szadotab = 10000; + NEWN (ps->adotab, ps->szadotab); + CLRN (ps->adotab, ps->szadotab); +} + +static int +propado (PS * ps, Var * v) +{ + Lit ** p, ** q, *** adotabpos, **ado, * lit; + Var * u; + + if (ps->LEVEL && ps->adodisabled) + return 1; + + assert (!ps->conflict); + assert (!ps->adoconflict); + assert (VAR2LIT (v)->val != UNDEF); + assert (!v->adotabpos); + + if (!v->ado) + return 1; + + assert (v->inado); + + for (p = v->ado; (lit = *p); p++) + if (lit->val == UNDEF) + { + u = LIT2VAR (lit); + assert (!u->ado); + u->ado = v->ado; + v->ado = 0; + + return 1; + } + + if (4 * ps->nadotab >= 3 * ps->szadotab) /* at least 75% filled */ + enlarge_adotab (ps); + + adotabpos = find_ado (ps, v->ado); + ado = *adotabpos; + + if (!ado) + { + ps->nadotab++; + v->adotabpos = adotabpos; + *adotabpos = v->ado; + return 1; + } + + assert (ado != v->ado); + + ps->adoconflict = new_clause (ps, 2 * llength (ado), 1); + q = ps->adoconflict->lits; + + for (p = ado; (lit = *p); p++) + *q++ = lit->val == FALSE ? lit : NOTLIT (lit); + + for (p = v->ado; (lit = *p); p++) + *q++ = lit->val == FALSE ? lit : NOTLIT (lit); + + assert (q == ENDOFCLS (ps->adoconflict)); + ps->conflict = ps->adoconflict; + ps->adoconflicts++; + return 0; +} + +#endif + +static void +bcp (PS * ps) +{ + int props = 0; + assert (!ps->conflict); + + if (ps->mtcls) + return; + + for (;;) + { + if (ps->ttail2 < ps->thead) /* prioritize implications */ + { + props++; + prop2 (ps, NOTLIT (*ps->ttail2++)); + } + else if (ps->ttail < ps->thead) /* unit clauses or clauses with length > 2 */ + { + if (ps->conflict) break; + propl (ps, NOTLIT (*ps->ttail++)); + if (ps->conflict) break; + } +#ifndef NADC + else if (ps->ttailado < ps->thead) + { + if (ps->conflict) break; + propado (ps, LIT2VAR (*ps->ttailado++)); + if (ps->conflict) break; + } +#endif + else + break; /* all assignments propagated, so break */ + } + + ps->propagations += props; +} + +static unsigned +drive (PS * ps) +{ + unsigned res, vlevel; + Lit **p; + Var *v; + + res = 0; + for (p = ps->added; p < ps->ahead; p++) + { + v = LIT2VAR (*p); + vlevel = v->level; + assert (vlevel <= ps->LEVEL); + if (vlevel < ps->LEVEL && vlevel > res) + res = vlevel; + } + + return res; +} + +#ifdef VISCORES + +static void +viscores (PS * ps) +{ + Rnk *p, *eor = ps->rnks + ps->max_var; + char name[100], cmd[200]; + FILE * data; + Flt s; + int i; + + for (p = ps->rnks + 1; p <= ps->eor; p++) + { + s = p->score; + if (s == INFFLT) + continue; + s = mulflt (s, ps->nvinc); + assert (flt2double (s) <= 1.0); + } + + sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts); + sprintf (cmd, "sort -n|nl>%s", name); + + data = popen (cmd, "w"); + for (p = ps->rnks + 1; p <= ps->eor; p++) + { + s = p->score; + if (s == INFFLT) + continue; + s = mulflt (s, ps->nvinc); + fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnks)); + } + fflush (data); + pclose (data); + + for (i = 0; i < 8; i++) + { + sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i); + system (cmd); + } + + fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts); + fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max_var); + + for (i = 0; i < 8; i++) + fprintf (ps->fviscores, + ", \"%s.%d\" using 1:2:3 with labels tc lt %d", + name, i, i + 1); + + fputc ('\n', ps->fviscores); + fflush (ps->fviscores); +#ifndef WRITEGIF + usleep (50000); /* refresh rate of 20 Hz */ +#endif +} + +#endif + +static void +crescore (PS * ps) +{ + Cls **p, *c; + Act *a; + Flt factor; + int l = log2flt (ps->cinc); + assert (l > 0); + factor = base2flt (1, -l); + + for (p = ps->lclauses; p != ps->lhead; p++) + { + c = *p; + + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + assert (c->learned); + + if (c->size <= 2) + continue; + + a = CLS2ACT (c); + *a = mulflt (*a, factor); + } + + ps->cinc = mulflt (ps->cinc, factor); +} + +static void +inc_vinc (PS * ps) +{ +#ifdef VISCORES + ps->nvinc = mulflt (ps->nvinc, ps->fvinc); +#endif + ps->vinc = mulflt (ps->vinc, ps->ifvinc); +} + +inline static void +inc_max_var (PS * ps) +{ + Lit *lit; + Rnk *r; + Var *v; + + assert (ps->max_var < ps->size_vars); + + if (ps->max_var + 1 == ps->size_vars) + enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */ + + ps->max_var++; /* new index of variable */ + assert (ps->max_var); /* no unsigned overflow */ + + assert (ps->max_var < ps->size_vars); + + lit = ps->lits + 2 * ps->max_var; + lit[0].val = lit[1].val = UNDEF; + + memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps); +#ifndef NDSC + memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps); +#endif + memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls); + memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh); + + v = ps->vars + ps->max_var; /* initialize variable components */ + CLR (v); + + r = ps->rnks + ps->max_var; /* initialize rank */ + CLR (r); + + hpush (ps, r); +} + +static void +force (PS * ps, Cls * c) +{ + Lit ** p, ** eol, * lit, * forced; + Cls * reason; + + forced = 0; + reason = c; + + eol = end_of_lits (c); + for (p = c->lits; p < eol; p++) + { + lit = *p; + if (lit->val == UNDEF) + { + assert (!forced); + forced = lit; +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + reason = LIT2REASON (NOTLIT (p[p == c->lits ? 1 : -1])); +#endif + } + else + assert (lit->val == FALSE); + } + +#ifdef NO_BINARY_CLAUSES + if (c == &ps->impl) + resetimpl (ps); +#endif + if (!forced) + return; + + assign_forced (ps, forced, reason); +} + +static INLINE 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 && !(INT_MOD(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 INLINE int +need_to_reduce (PS * ps) +{ + return ps->nlclauses >= reduce_limit_on_lclauses (ps); +} + +#ifdef NLUBY + +static void +inc_drestart (PS * ps) +{ + ps->drestart *= FRESTART; + ps->drestart /= 100; + + if (ps->drestart >= MAXRESTART) + ps->drestart = MAXRESTART; +} + +static void +inc_ddrestart (PS * ps) +{ + ps->ddrestart *= FRESTART; + ps->ddrestart /= 100; + + if (ps->ddrestart >= MAXRESTART) + ps->ddrestart = MAXRESTART; +} + +#else + +static unsigned +luby (unsigned i) +{ + unsigned k; + for (k = 1; k < 32; k++) + if (i == (1u << k) - 1) + return 1u << (k - 1); + + for (k = 1;; k++) + if ((1u << (k - 1)) <= i && i < (1u << k) - 1) + return luby (i - (1u << (k-1)) + 1); +} + +#endif + +#ifndef NLUBY +static void +inc_lrestart (PS * ps, int skip) +{ + unsigned delta; + + delta = 100 * luby (++ps->lubycnt); + ps->lrestart = ps->conflicts + delta; + + if (ps->waslubymaxdelta) + report (ps, 1, skip ? 'N' : 'R'); + else + report (ps, 2, skip ? 'n' : 'r'); + + if (delta > ps->lubymaxdelta) + { + ps->lubymaxdelta = delta; + ps->waslubymaxdelta = 1; + } + else + ps->waslubymaxdelta = 0; +} +#endif + +static void +init_restart (PS * ps) +{ +#ifdef NLUBY + /* TODO: why is it better in incremental usage to have smaller initial + * outer restart interval? + */ + ps->ddrestart = ps->calls > 1 ? MINRESTART : 1000; + ps->drestart = MINRESTART; + ps->lrestart = ps->conflicts + ps->drestart; +#else + ps->lubycnt = 0; + ps->lubymaxdelta = 0; + ps->waslubymaxdelta = 0; + inc_lrestart (ps, 0); +#endif +} + +static void +restart (PS * ps) +{ + int skip; +#ifdef NLUBY + char kind; + int outer; + + inc_drestart (ps); + outer = (ps->drestart >= ps->ddrestart); + + if (outer) + skip = very_high_agility (ps); + else + skip = high_agility (ps); +#else + skip = medium_agility (ps); +#endif + +#ifdef STATS + if (skip) + ps->skippedrestarts++; +#endif + + assert (ps->conflicts >= ps->lrestart); + + if (!skip) + { + ps->restarts++; + assert (ps->LEVEL > 1); + LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts)); + undo (ps, 0); + } + +#ifdef NLUBY + if (outer) + { + kind = skip ? 'N' : 'R'; + inc_ddrestart (ps); + ps->drestart = MINRESTART; + } + else if (skip) + { + kind = 'n'; + } + else + { + kind = 'r'; + } + + assert (ps->drestart <= MAXRESTART); + ps->lrestart = ps->conflicts + ps->drestart; + assert (ps->lrestart > ps->conflicts); + + report (outer ? 1 : 2, kind); +#else + inc_lrestart (ps, skip); +#endif +} + +inline static void +assign_decision (PS * ps, Lit * lit) +{ + assert (!ps->conflict); + + ps->LEVEL++; + + LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL)); + LOG ( fprintf (ps->out, + "%sassign %d at level %d <= DECISION\n", + ps->prefix, LIT2INT (lit), ps->LEVEL)); + + assign (ps, lit, 0); +} + +#ifndef NFL + +static INLINE 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 INLINE 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, b, * p, * q; + + (void) ps; + + assert (c->learned); + assert (d->learned); + + if (c->glue < d->glue) // smaller glue preferred + return 1; + + if (c->glue > d->glue) + return -1; + + p = CLS2ACT (c); + q = CLS2ACT (d); + a = *p; + b = *q; + + if (a < b) // then higher activity + return -1; + + if (b < a) + return 1; + + if (c->size < d->size) // then smaller size + return 1; + + if (c->size > d->size) + return -1; + + return 0; +} + +static void +reduce (PS * ps, unsigned percentage) +{ + unsigned redcount, lcollect, collect, target; +#ifdef STATS + size_t bytes_collected; +#endif + Cls **p, *c; + + assert (ps->rhead == ps->resolved); + + ps->lastreduceconflicts = ps->conflicts; + + assert (percentage <= 100); + LOG ( fprintf (ps->out, + "%sreducing %u%% learned clauses\n", + ps->prefix, percentage)); + + while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved)) + ENLARGE (ps->resolved, ps->rhead, ps->eor); + + collect = 0; + lcollect = 0; + + for (p = ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p != EOC; p = NXC (p)) + { + c = *p; + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + + if (c->locked) + continue; + + assert (!c->collect); + if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c)) + { + mark_clause_to_be_collected (c); + collect++; + + if (c->learned && c->size > 2) + lcollect++; + + continue; + } + + if (!c->learned) + continue; + + if (c->size <= 2) + continue; + + assert (ps->rhead < ps->eor); + *ps->rhead++ = c; + } + assert (ps->rhead <= ps->eor); + + ps->fsimplify = ps->fixed; + + redcount = ps->rhead - ps->resolved; + SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount); + + assert (ps->nlclauses >= lcollect); + target = ps->nlclauses - lcollect + 1; + + target = (percentage * target + 99) / 100; + + if (target >= redcount) + target = redcount; + + ps->rhead = ps->resolved + target; + while (ps->rhead > ps->resolved) + { + c = *--ps->rhead; + mark_clause_to_be_collected (c); + + collect++; + if (c->learned && c->size > 2) /* just for consistency */ + lcollect++; + } + + if (collect) + { + ps->reductions++; +#ifdef STATS + bytes_collected = +#endif + collect_clauses (ps); +#ifdef STATS + ps->rrecycled += bytes_collected; +#endif + report (ps, 2, '-'); + } + + if (!lcollect) + inc_lreduce (ps); /* avoid dead lock */ + + assert (ps->rhead == ps->resolved); +} + +static void +init_reduce (PS * ps) +{ + // lreduce = loadded / 2; + ps->lreduce = 1000; + + if (ps->lreduce < 100) + ps->lreduce = 100; + + if (ps->verbosity) + fprintf (ps->out, + "%s\n%sinitial reduction limit %u clauses\n%s\n", + ps->prefix, ps->prefix, ps->lreduce, ps->prefix); +} + +static INLINE 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 = INT_MOD(a, b); + a = tmp; + } + + return a; +} + +static Lit * +rdecide (PS * ps) +{ + unsigned idx, delta, spread; + Lit * res; + + spread = RDECIDE; + if (rrng (ps, 1, spread) != 2) + return 0; + + assert (1 <= ps->max_var); + idx = rrng (ps, 1, ps->max_var); + res = int2lit (ps, idx); + + if (res->val != UNDEF) + { + delta = rrng (ps, 1, ps->max_var); + while (gcd (delta, ps->max_var) != 1) + delta--; + + assert (1 <= delta); + assert (delta <= ps->max_var); + + do { + idx += delta; + if (idx > ps->max_var) + idx -= ps->max_var; + res = int2lit (ps, idx); + } while (res->val != UNDEF); + } + +#ifdef STATS + ps->rdecisions++; +#endif + res = decide_phase (ps, res); + LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res))); + + return res; +} + +static Lit * +sdecide (PS * ps) +{ + Lit *res; + Rnk *r; + + for (;;) + { + r = htop (ps); + res = RNK2LIT (r); + if (res->val == UNDEF) break; + (void) hpop (ps); + NOLOG ( fprintf (ps->out, + "%shpop %u %u %u\n", + ps->prefix, r - ps->rnks, + FLTMANTISSA(r->score), + FLTEXPONENT(r->score))); + } + +#ifdef STATS + ps->sdecisions++; +#endif + res = decide_phase (ps, res); + + LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res))); + + return res; +} + +static Lit * +adecide (PS * ps) +{ + Lit *lit; + Var * v; + + assert (ps->als < ps->alshead); + assert (!ps->failed_assumption); + + while (ps->alstail < ps->alshead) + { + lit = *ps->alstail++; + + if (lit->val == FALSE) + { + ps->failed_assumption = lit; + v = LIT2VAR (lit); + + use_var (ps, v); + + LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n", + ps->prefix, LIT2INT (ps->failed_assumption))); + fanalyze (ps); + return 0; + } + + if (lit->val == TRUE) + { + v = LIT2VAR (lit); + if (v->level > ps->adecidelevel) + ps->adecidelevel = v->level; + continue; + } + +#ifdef STATS + ps->assumptions++; +#endif + LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit))); + ps->adecidelevel = ps->LEVEL + 1; + + return lit; + } + + return 0; +} + +static void +decide (PS * ps) +{ + Lit * lit; + + assert (!satisfied (ps)); + assert (!ps->conflict); + + if (ps->alstail < ps->alshead && (lit = adecide (ps))) + ; + else if (ps->failed_assumption) + return; + else if (satisfied (ps)) + return; + else if (!(lit = rdecide (ps))) + lit = sdecide (ps); + + assert (lit); + assign_decision (ps, lit); + + ps->levelsum += ps->LEVEL; + ps->decisions++; +} + +static int +sat (PS * ps, int l) +{ + int count = 0, backtracked; + + if (!ps->conflict) + bcp (ps); + + if (ps->conflict) + backtrack (ps); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + goto SATISFIED; + + if (ps->lsimplify <= ps->propagations) + simplify (ps, 0); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + goto SATISFIED; + + init_restart (ps); + + if (!ps->lreduce) + init_reduce (ps); + + ps->isimplify = ps->fixed; + backtracked = 0; + + for (;;) + { + if (!ps->conflict) + bcp (ps); + + if (ps->conflict) + { + incincs (ps); + backtrack (ps); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + backtracked = 1; + continue; + } + + if (satisfied (ps)) + { +SATISFIED: +#ifndef NDEBUG + original_clauses_satisfied (ps); + assumptions_satisfied (ps); +#endif + return PICOSAT_SATISFIABLE; + } + + if (backtracked) + { + backtracked = 0; + if (!ps->LEVEL && ps->isimplify < ps->fixed) + iteration (ps); + } + + if (l >= 0 && count >= l) /* decision limit reached ? */ + return PICOSAT_UNKNOWN; + + if (ps->interrupt.function && /* external interrupt */ + count > 0 && !(INT_MOD(count, INTERRUPTLIM)) && + ps->interrupt.function (ps->interrupt.state)) + return PICOSAT_UNKNOWN; + + if (ps->propagations >= ps->lpropagations)/* propagation limit reached ? */ + return PICOSAT_UNKNOWN; + +#ifndef NADC + if (!ps->adodisabled && ps->adoconflicts >= ps->adoconflictlimit) + { + assert (bcp_queue_is_empty (ps)); + return PICOSAT_UNKNOWN; + } +#endif + + if (ps->fsimplify < ps->fixed && ps->lsimplify <= ps->propagations) + { + simplify (ps, 0); + if (!bcp_queue_is_empty (ps)) + continue; +#ifndef NFL + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + return PICOSAT_SATISFIABLE; + + assert (!ps->LEVEL); +#endif + } + + if (need_to_reduce (ps)) + reduce (ps, 50); + + if (ps->conflicts >= ps->lrestart && ps->LEVEL > 2) + restart (ps); + + decide (ps); + if (ps->failed_assumption) + return PICOSAT_UNSATISFIABLE; + count++; + } +} + +static void +rebias (PS * ps) +{ + Cls ** p, * c; + Var * v; + + for (v = ps->vars + 1; v <= ps->vars + ps->max_var; v++) + v->assigned = 0; + + memset (ps->jwh, 0, 2 * (ps->max_var + 1) * sizeof *ps->jwh); + + for (p = ps->oclauses; p < ps->ohead; p++) + { + c = *p; + + if (!c) + continue; + + if (c->learned) + continue; + + incjwh (ps, c); + } +} + +#ifdef TRACE + +static unsigned +core (PS * ps) +{ + unsigned idx, prev, this, delta, i, lcore, vcore; + unsigned *stack, *shead, *eos; + Lit **q, **eol, *lit; + Cls *c, *reason; + Znt *p, byte; + Zhn *zhain; + Var *v; + + assert (ps->trace); + + assert (ps->mtcls || ps->failed_assumption); + if (ps->ocore >= 0) + return ps->ocore; + + lcore = ps->ocore = vcore = 0; + + stack = shead = eos = 0; + ENLARGE (stack, shead, eos); + + if (ps->mtcls) + { + idx = CLS2IDX (ps->mtcls); + *shead++ = idx; + } + else + { + assert (ps->failed_assumption); + v = LIT2VAR (ps->failed_assumption); + reason = v->reason; + assert (reason); + idx = CLS2IDX (reason); + *shead++ = idx; + } + + while (shead > stack) + { + idx = *--shead; + zhain = IDX2ZHN (idx); + + if (zhain) + { + if (zhain->core) + continue; + + zhain->core = 1; + lcore++; + + c = IDX2CLS (idx); + if (c) + { + assert (!c->core); + c->core = 1; + } + + i = 0; + delta = 0; + prev = 0; + for (p = zhain->znt; (byte = *p); p++, i += 7) + { + delta |= (byte & 0x7f) << i; + if (byte & 0x80) + continue; + + this = prev + delta; + assert (prev < this); /* no overflow */ + + if (shead == eos) + ENLARGE (stack, shead, eos); + *shead++ = this; + + prev = this; + delta = 0; + i = -7; + } + } + else + { + c = IDX2CLS (idx); + + assert (c); + assert (!c->learned); + + if (c->core) + continue; + + c->core = 1; + ps->ocore++; + + eol = end_of_lits (c); + for (q = c->lits; q < eol; q++) + { + lit = *q; + v = LIT2VAR (lit); + if (v->core) + continue; + + v->core = 1; + vcore++; + + if (!ps->failed_assumption) continue; + if (lit != ps->failed_assumption) continue; + + reason = v->reason; + if (!reason) continue; + if (reason->core) continue; + + idx = CLS2IDX (reason); + if (shead == eos) + ENLARGE (stack, shead, eos); + *shead++ = idx; + } + } + } + + DELETEN (stack, eos - stack); + + if (ps->verbosity) + fprintf (ps->out, + "%s%u core variables out of %u (%.1f%%)\n" + "%s%u core original clauses out of %u (%.1f%%)\n" + "%s%u core learned clauses out of %u (%.1f%%)\n", + ps->prefix, vcore, ps->max_var, PERCENT (vcore, ps->max_var), + ps->prefix, ps->ocore, ps->oadded, PERCENT (ps->ocore, ps->oadded), + ps->prefix, lcore, ps->ladded, PERCENT (lcore, ps->ladded)); + + return ps->ocore; +} + +static void +trace_lits (PS * ps, Cls * c, FILE * file) +{ + Lit **p, **eol = end_of_lits (c); + + assert (c); + assert (c->core); + + for (p = c->lits; p < eol; p++) + fprintf (file, "%d ", LIT2INT (*p)); + + fputc ('0', file); +} + +static void +write_idx (PS * ps, unsigned idx, FILE * file) +{ + fprintf (file, "%ld", EXPORTIDX (idx)); +} + +static void +trace_clause (PS * ps, unsigned idx, Cls * c, FILE * file, int fmt) +{ + assert (c); + assert (c->core); + assert (fmt == RUP_TRACE_FMT || !c->learned); + assert (CLS2IDX (c) == idx); + + if (fmt != RUP_TRACE_FMT) + { + write_idx (ps, idx, file); + fputc (' ', file); + } + + trace_lits (ps, c, file); + + if (fmt != RUP_TRACE_FMT) + fputs (" 0", file); + + fputc ('\n', file); +} + +static void +trace_zhain (PS * ps, unsigned idx, Zhn * zhain, FILE * file, int fmt) +{ + unsigned prev, this, delta, i; + Znt *p, byte; + Cls * c; + + assert (zhain); + assert (zhain->core); + + write_idx (ps, idx, file); + fputc (' ', file); + + if (fmt == EXTENDED_TRACECHECK_TRACE_FMT) + { + c = IDX2CLS (idx); + assert (c); + trace_lits (ps, c, file); + } + else + { + assert (fmt == COMPACT_TRACECHECK_TRACE_FMT); + putc ('*', file); + } + + i = 0; + delta = 0; + prev = 0; + + for (p = zhain->znt; (byte = *p); p++, i += 7) + { + delta |= (byte & 0x7f) << i; + if (byte & 0x80) + continue; + + this = prev + delta; + + putc (' ', file); + write_idx (ps, this, file); + + prev = this; + delta = 0; + i = -7; + } + + fputs (" 0\n", file); +} + +static void +write_core (PS * ps, FILE * file) +{ + Lit **q, **eol; + Cls **p, *c; + + fprintf (file, "p cnf %u %u\n", ps->max_var, core (ps)); + + for (p = SOC; p != EOC; p = NXC (p)) + { + c = *p; + + if (!c || c->learned || !c->core) + continue; + + eol = end_of_lits (c); + for (q = c->lits; q < eol; q++) + fprintf (file, "%d ", LIT2INT (*q)); + + fputs ("0\n", file); + } +} + +#endif + +static void +write_trace (PS * ps, FILE * file, int fmt) +{ +#ifdef TRACE + Cls *c, ** p; + Zhn *zhain; + unsigned i; + + core (ps); + + if (fmt == RUP_TRACE_FMT) + { + ps->rupvariables = picosat_variables (ps), + ps->rupclauses = picosat_added_original_clauses (ps); + write_rup_header (ps, file); + } + + for (p = SOC; p != EOC; p = NXC (p)) + { + c = *p; + + if (ps->oclauses <= p && p < ps->eoo) + { + i = OIDX2IDX (p - ps->oclauses); + assert (!c || CLS2IDX (c) == i); + } + else + { + assert (ps->lclauses <= p && p < ps->EOL); + i = LIDX2IDX (p - ps->lclauses); + } + + zhain = IDX2ZHN (i); + + if (zhain) + { + if (zhain->core) + { + if (fmt == RUP_TRACE_FMT) + trace_clause (ps,i, c, file, fmt); + else + trace_zhain (ps, i, zhain, file, fmt); + } + } + else if (c) + { + if (fmt != RUP_TRACE_FMT && c) + { + if (c->core) + trace_clause (ps, i, c, file, fmt); + } + } + } +#else + (void) file; + (void) fmt; + (void) ps; +#endif +} + +static void +write_core_wrapper (PS * ps, FILE * file, int fmt) +{ + (void) fmt; +#ifdef TRACE + write_core (ps, file); +#else + (void) ps; + (void) file; +#endif +} + +static Lit * +import_lit (PS * ps, int lit, int nointernal) +{ + Lit * res; + Var * v; + + ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal"); + ABORTIF (abs (lit) > (int) ps->max_var && ps->CLS != ps->clshead, + "API usage: new variable index after 'picosat_push'"); + + if (abs (lit) <= (int) ps->max_var) + { + res = int2lit (ps, lit); + v = LIT2VAR (res); + if (nointernal && v->internal) + ABORT ("API usage: trying to import invalid literal"); + else if (!nointernal && !v->internal) + ABORT ("API usage: trying to import invalid context"); + } + else + { + while (abs (lit) > (int) ps->max_var) + inc_max_var (ps); + res = int2lit (ps, lit); + } + + return res; +} + +#ifdef TRACE +static void +reset_core (PS * ps) +{ + Cls ** p, * c; + Zhn ** q, * z; + unsigned i; + + for (i = 1; i <= ps->max_var; i++) + ps->vars[i].core = 0; + + for (p = SOC; p != EOC; p = NXC (p)) + if ((c = *p)) + c->core = 0; + + for (q = ps->zhains; q != ps->zhead; q++) + if ((z = *q)) + z->core = 0; + + ps->ocore = -1; +} +#endif + +static void +reset_assumptions (PS * ps) +{ + Lit ** p; + + ps->failed_assumption = 0; + + if (ps->extracted_all_failed_assumptions) + { + for (p = ps->als; p < ps->alshead; p++) + LIT2VAR (*p)->failed = 0; + + ps->extracted_all_failed_assumptions = 0; + } + + ps->alstail = ps->alshead = ps->als; + ps->adecidelevel = 0; +} + +static INLINE void +check_ready (PS * ps) +{ + ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized"); +} + +static INLINE void +check_sat_state (PS * ps) +{ + ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state"); +} + +static INLINE void +check_unsat_state (PS * ps) +{ + ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state"); +} + +static INLINE 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 INLINE 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 (ps, external_lit, 1); + add_lit (ps, internal_lit); + } + else + { + ps->addingtoado = 0; + add_ado (ps); + } + if (ps->measurealltimeinlib) + leave (ps); +#else + (void) ps; + (void) external_lit; + ABORT ("compiled without all different constraint support"); +#endif +} + +static void +assume (PS * ps, Lit * lit) +{ + if (ps->alshead == ps->eoals) + { + assert (ps->alstail == ps->als); + ENLARGE (ps->als, ps->alshead, ps->eoals); + ps->alstail = ps->als; + } + + *ps->alshead++ = lit; + LOG ( fprintf (ps->out, "%sassumption %d\n", ps->prefix, LIT2INT (lit))); +} + +static void +assume_contexts (PS * ps) +{ + Lit ** p; + if (ps->als != ps->alshead) + return; + for (p = ps->CLS; p != ps->clshead; p++) + assume (ps, *p); +} + +#ifndef RCODE +static const char * enumstr (int i) { + int last = INT_MOD(i, 10); + if (last == 1) return "st"; + if (last == 2) return "nd"; + if (last == 3) return "rd"; + return "th"; +} +#endif + +static int +tderef (PS * ps, int int_lit) +{ + Lit * lit; + Var * v; + + assert (abs (int_lit) <= (int) ps->max_var); + + lit = int2lit (ps, int_lit); + + v = LIT2VAR (lit); + if (v->level > 0) + return 0; + + if (lit->val == TRUE) + return 1; + + if (lit->val == FALSE) + return -1; + + return 0; +} + +static int +pderef (PS * ps, int int_lit) +{ + Lit * lit; + Var * v; + + assert (abs (int_lit) <= (int) ps->max_var); + + v = ps->vars + abs (int_lit); + if (!v->partial) + return 0; + + lit = int2lit (ps, int_lit); + + if (lit->val == TRUE) + return 1; + + if (lit->val == FALSE) + return -1; + + return 0; +} + +static void +minautarky (PS * ps) +{ + unsigned * occs, maxoccs, tmpoccs, npartial; + int * p, * c, lit, best, val; +#ifdef LOGGING + int tl; +#endif + + assert (!ps->partial); + + npartial = 0; + + NEWN (occs, 2*ps->max_var + 1); + CLRN (occs, 2*ps->max_var + 1); + occs += ps->max_var; + for (p = ps->soclauses; p < ps->sohead; p++) + occs[*p]++; + assert (occs[0] == ps->oadded); + + for (c = ps->soclauses; c < ps->sohead; c = p + 1) + { +#ifdef LOGGING + tl = 0; +#endif + best = 0; + maxoccs = 0; + for (p = c; (lit = *p); p++) + { + val = tderef (ps, lit); + if (val < 0) + continue; + if (val > 0) + { +#ifdef LOGGING + tl = 1; +#endif + best = lit; + maxoccs = occs[lit]; + } + + val = pderef (ps, lit); + if (val > 0) + break; + if (val < 0) + continue; + val = int2lit (ps, lit)->val; + assert (val); + if (val < 0) + continue; + tmpoccs = occs[lit]; + if (best && tmpoccs <= maxoccs) + continue; + best = lit; + maxoccs = tmpoccs; + } + if (!lit) + { + assert (best); + LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n", + ps->prefix, best, maxoccs, tl ? " (top)" : "")); + ps->vars[abs (best)].partial = 1; + npartial++; + } + for (p = c; (lit = *p); p++) + { + assert (occs[lit] > 0); + occs[lit]--; + } + } + occs -= ps->max_var; + DELETEN (occs, 2*ps->max_var + 1); + ps->partial = 1; + + if (ps->verbosity) + fprintf (ps->out, + "%sautarky of size %u out of %u satisfying all clauses (%.1f%%)\n", + ps->prefix, npartial, ps->max_var, PERCENT (npartial, ps->max_var)); +} + +void +picosat_assume (PS * ps, int int_lit) +{ + Lit *lit; + + if (ps->measurealltimeinlib) + enter (ps); + else + check_ready (ps); + + if (ps->state != READY) + reset_incremental_usage (ps); + + assume_contexts (ps); + lit = import_lit (ps, int_lit, 1); + assume (ps, lit); + + if (ps->measurealltimeinlib) + leave (ps); +} + +int +picosat_sat (PS * ps, int l) +{ + int res; + char ch; + + enter (ps); + + ps->calls++; + LOG ( fprintf (ps->out, "%sSTART call %u\n", ps->prefix, ps->calls)); + + if (ps->added < ps->ahead) + { +#ifndef NADC + if (ps->addingtoado) + ABORT ("API usage: incomplete all different constraint"); + else +#endif + ABORT ("API usage: incomplete clause"); + } + + if (ps->state != READY) + reset_incremental_usage (ps); + + assume_contexts (ps); + + res = sat (ps, l); + + assert (ps->state == READY); + + switch (res) + { + case PICOSAT_UNSATISFIABLE: + ch = '0'; + ps->state = UNSAT; + break; + case PICOSAT_SATISFIABLE: + ch = '1'; + ps->state = SAT; + break; + default: + ch = '?'; + ps->state = UNKNOWN; + break; + } + + if (ps->verbosity) + { + report (ps, 1, ch); + rheader (ps); + } + + leave (ps); + LOG ( fprintf (ps->out, "%sEND call %u result %d\n", ps->prefix, ps->calls, res)); + + ps->last_sat_call_result = res; + + return res; +} + +int +picosat_res (PS * ps) +{ + return ps->last_sat_call_result; +} + +int +picosat_deref (PS * ps, int int_lit) +{ + Lit *lit; + + check_ready (ps); + check_sat_state (ps); + ABORTIF (!int_lit, "API usage: can not deref zero literal"); + ABORTIF (ps->mtcls, "API usage: deref after empty clause generated"); + +#ifdef STATS + ps->derefs++; +#endif + + if (abs (int_lit) > (int) ps->max_var) + return 0; + + lit = int2lit (ps, int_lit); + + if (lit->val == TRUE) + return 1; + + if (lit->val == FALSE) + return -1; + + return 0; +} + +int +picosat_deref_toplevel (PS * ps, int int_lit) +{ + check_ready (ps); + ABORTIF (!int_lit, "API usage: can not deref zero literal"); + +#ifdef STATS + ps->derefs++; +#endif + if (abs (int_lit) > (int) ps->max_var) + return 0; + + return tderef (ps, int_lit); +} + +int +picosat_inconsistent (PS * ps) +{ + check_ready (ps); + return ps->mtcls != 0; +} + +int +picosat_corelit (PS * ps, int int_lit) +{ + check_ready (ps); + check_unsat_state (ps); + ABORTIF (!int_lit, "API usage: zero literal can not be in core"); + + assert (ps->mtcls || ps->failed_assumption); + +#ifdef TRACE + { + int res = 0; + ABORTIF (!ps->trace, "tracing disabled"); + if (ps->measurealltimeinlib) + enter (ps); + core (ps); + if (abs (int_lit) <= (int) ps->max_var) + res = ps->vars[abs (int_lit)].core; + assert (!res || ps->failed_assumption || ps->vars[abs (int_lit)].used); + if (ps->measurealltimeinlib) + leave (ps); + return res; + } +#else + ABORT ("compiled without trace support"); + return 0; +#endif +} + +int +picosat_coreclause (PS * ps, int ocls) +{ + check_ready (ps); + check_unsat_state (ps); + + ABORTIF (ocls < 0, "API usage: negative original clause index"); + ABORTIF (ocls >= (int)ps->oadded, "API usage: original clause index exceeded"); + + assert (ps->mtcls || ps->failed_assumption); + +#ifdef TRACE + { + Cls ** clsptr, * c; + int res = 0; + + ABORTIF (!ps->trace, "tracing disabled"); + if (ps->measurealltimeinlib) + enter (ps); + core (ps); + clsptr = ps->oclauses + ocls; + assert (clsptr < ps->ohead); + c = *clsptr; + if (c) + res = c->core; + if (ps->measurealltimeinlib) + leave (ps); + + return res; + } +#else + ABORT ("compiled without trace support"); + return 0; +#endif +} + +int +picosat_failed_assumption (PS * ps, int int_lit) +{ + Lit * lit; + Var * v; + ABORTIF (!int_lit, "API usage: zero literal as assumption"); + check_ready (ps); + check_unsat_state (ps); + if (ps->mtcls) + return 0; + assert (ps->failed_assumption); + if (abs (int_lit) > (int) ps->max_var) + return 0; + if (!ps->extracted_all_failed_assumptions) + extract_all_failed_assumptions (ps); + lit = import_lit (ps, int_lit, 1); + v = LIT2VAR (lit); + return v->failed; +} + +int +picosat_failed_context (PS * ps, int int_lit) +{ + Lit * lit; + Var * v; + ABORTIF (!int_lit, "API usage: zero literal as context"); + ABORTIF (abs (int_lit) > (int) ps->max_var, "API usage: invalid context"); + check_ready (ps); + check_unsat_state (ps); + assert (ps->failed_assumption); + if (!ps->extracted_all_failed_assumptions) + extract_all_failed_assumptions (ps); + lit = import_lit (ps, int_lit, 0); + v = LIT2VAR (lit); + return v->failed; +} + +const int * +picosat_failed_assumptions (PS * ps) +{ + Lit ** p, * lit; + Var * v; + int ilit; + + ps->falshead = ps->fals; + check_ready (ps); + check_unsat_state (ps); + if (!ps->mtcls) + { + assert (ps->failed_assumption); + if (!ps->extracted_all_failed_assumptions) + extract_all_failed_assumptions (ps); + + for (p = ps->als; p < ps->alshead; p++) + { + lit = *p; + v = LIT2VAR (*p); + if (!v->failed) + continue; + ilit = LIT2INT (lit); + if (ps->falshead == ps->eofals) + ENLARGE (ps->fals, ps->falshead, ps->eofals); + *ps->falshead++ = ilit; + } + } + if (ps->falshead == ps->eofals) + ENLARGE (ps->fals, ps->falshead, ps->eofals); + *ps->falshead++ = 0; + return ps->fals; +} + +const int * +picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fix) +{ + int i, j, ilit, len, nwork, * work, res; + signed char * redundant; + Lit ** p, * lit; + int failed; + Var * v; +#ifndef NDEBUG + int oldlen; +#endif +#ifndef RCODE + int norig = ps->alshead - ps->als; +#endif + + check_ready (ps); + check_unsat_state (ps); + len = 0; + if (!ps->mtcls) + { + assert (ps->failed_assumption); + if (!ps->extracted_all_failed_assumptions) + extract_all_failed_assumptions (ps); + + for (p = ps->als; p < ps->alshead; p++) + if (LIT2VAR (*p)->failed) + len++; + } + + if (ps->mass) + DELETEN (ps->mass, ps->szmass); + ps->szmass = len + 1; + NEWN (ps->mass, ps->szmass); + + i = 0; + for (p = ps->als; p < ps->alshead; p++) + { + lit = *p; + v = LIT2VAR (lit); + if (!v->failed) + continue; + ilit = LIT2INT (lit); + assert (i < len); + ps->mass[i++] = ilit; + } + assert (i == len); + ps->mass[i] = 0; + if (ps->verbosity) + fprintf (ps->out, + "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n", + ps->prefix, len, norig, PERCENT (len, norig)); + if (cb) + cb (s, ps->mass); + + nwork = len; + NEWN (work, nwork); + for (i = 0; i < len; i++) + work[i] = ps->mass[i]; + + NEWN (redundant, nwork); + CLRN (redundant, nwork); + + for (i = 0; i < nwork; i++) + { + if (redundant[i]) + continue; + + if (ps->verbosity > 1) + fprintf (ps->out, + "%strying to drop %d%s assumption %d\n", + ps->prefix, i, enumstr (i), work[i]); + for (j = 0; j < nwork; j++) + { + if (i == j) continue; + if (j < i && fix) continue; + if (redundant[j]) continue; + picosat_assume (ps, work[j]); + } + + res = picosat_sat (ps, -1); + if (res == 10) + { + if (ps->verbosity > 1) + fprintf (ps->out, + "%sfailed to drop %d%s assumption %d\n", + ps->prefix, i, enumstr (i), work[i]); + + if (fix) + { + picosat_add (ps, work[i]); + picosat_add (ps, 0); + } + } + else + { + assert (res == 20); + if (ps->verbosity > 1) + fprintf (ps->out, + "%ssuceeded to drop %d%s assumption %d\n", + ps->prefix, i, enumstr (i), work[i]); + redundant[i] = 1; + for (j = 0; j < nwork; j++) + { + failed = picosat_failed_assumption (ps, work[j]); + if (j <= i) + { + assert ((j < i && fix) || redundant[j] == !failed); + continue; + } + + if (!failed) + { + redundant[j] = -1; + if (ps->verbosity > 1) + fprintf (ps->out, + "%salso suceeded to drop %d%s assumption %d\n", + ps->prefix, j, enumstr (j), work[j]); + } + } + +#ifndef NDEBUG + oldlen = len; +#endif + len = 0; + for (j = 0; j < nwork; j++) + if (!redundant[j]) + ps->mass[len++] = work[j]; + ps->mass[len] = 0; + assert (len < oldlen); + + if (fix) + { + picosat_add (ps, -work[i]); + picosat_add (ps, 0); + } + +#ifndef NDEBUG + for (j = 0; j <= i; j++) + assert (redundant[j] >= 0); +#endif + for (j = i + 1; j < nwork; j++) + { + if (redundant[j] >= 0) + continue; + + if (fix) + { + picosat_add (ps, -work[j]); + picosat_add (ps, 0); + } + + redundant[j] = 1; + } + + if (ps->verbosity) + fprintf (ps->out, + "%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n", + ps->prefix, len, norig, PERCENT (len, norig)); + if (cb) + cb (s, ps->mass); + } + } + + DELETEN (work, nwork); + DELETEN (redundant, nwork); + + if (ps->verbosity) + { + fprintf (ps->out, "%sreinitializing unsat state\n", ps->prefix); + fflush (ps->out); + } + + for (i = 0; i < len; i++) + picosat_assume (ps, ps->mass[i]); + +#ifndef NDEBUG + res = +#endif + picosat_sat (ps, -1); + assert (res == 20); + + if (!ps->mtcls) + { + assert (!ps->extracted_all_failed_assumptions); + extract_all_failed_assumptions (ps); + } + + return ps->mass; +} + +static const int * +mss (PS * ps, int * a, int size) +{ + int i, j, k, res; + + assert (!ps->mtcls); + + if (ps->szmssass) + DELETEN (ps->mssass, ps->szmssass); + + ps->szmssass = 0; + ps->mssass = 0; + + ps->szmssass = size + 1; + NEWN (ps->mssass, ps->szmssass); + + LOG ( fprintf (ps->out, "%ssearch MSS over %d assumptions\n", ps->prefix, size)); + + k = 0; + for (i = k; i < size; i++) + { + for (j = 0; j < k; j++) + picosat_assume (ps, ps->mssass[j]); + + LOG ( fprintf (ps->out, + "%strying to add assumption %d to MSS : %d\n", + ps->prefix, i, a[i])); + + picosat_assume (ps, a[i]); + + res = picosat_sat (ps, -1); + if (res == 10) + { + LOG ( fprintf (ps->out, + "%sadding assumption %d to MSS : %d\n", ps->prefix, i, a[i])); + + ps->mssass[k++] = a[i]; + + for (j = i + 1; j < size; j++) + { + if (picosat_deref (ps, a[j]) <= 0) + continue; + + LOG ( fprintf (ps->out, + "%salso adding assumption %d to MSS : %d\n", + ps->prefix, j, a[j])); + + ps->mssass[k++] = a[j]; + + if (++i != j) + { + int tmp = a[i]; + a[i] = a[j]; + a[j] = tmp; + } + } + } + else + { + assert (res == 20); + + LOG ( fprintf (ps->out, + "%signoring assumption %d in MSS : %d\n", ps->prefix, i, a[i])); + } + } + ps->mssass[k] = 0; + LOG ( fprintf (ps->out, "%sfound MSS of size %d\n", ps->prefix, k)); + + return ps->mssass; +} + +static void +reassume (PS * ps, const int * a, int size) +{ + int i; + LOG ( fprintf (ps->out, "%sreassuming all assumptions\n", ps->prefix)); + for (i = 0; i < size; i++) + picosat_assume (ps, a[i]); +} + +const int * +picosat_maximal_satisfiable_subset_of_assumptions (PS * ps) +{ + const int * res; + int i, *a, size; + + ABORTIF (ps->mtcls, + "API usage: CNF inconsistent (use 'picosat_inconsistent')"); + + enter (ps); + + size = ps->alshead - ps->als; + NEWN (a, size); + + for (i = 0; i < size; i++) + a[i] = LIT2INT (ps->als[i]); + + res = mss (ps, a, size); + reassume (ps, a, size); + + DELETEN (a, size); + + leave (ps); + + return res; +} + +static void +check_mss_flags_clean (PS * ps) +{ +#ifndef NDEBUG + unsigned i; + for (i = 1; i <= ps->max_var; i++) + { + assert (!ps->vars[i].msspos); + assert (!ps->vars[i].mssneg); + } +#else + (void) ps; +#endif +} + +static void +push_mcsass (PS * ps, int lit) +{ + if (ps->nmcsass == ps->szmcsass) + { + ps->szmcsass = ps->szmcsass ? 2*ps->szmcsass : 1; + RESIZEN (ps->mcsass, ps->nmcsass, ps->szmcsass); + } + + ps->mcsass[ps->nmcsass++] = lit; +} + +static const int * +next_mss (PS * ps, int mcs) +{ + int i, *a, size, mssize, mcsize, lit, inmss; + const int * res, * p; + Var * v; + + if (ps->mtcls) return 0; + + check_mss_flags_clean (ps); + + if (mcs && ps->mcsass) + { + DELETEN (ps->mcsass, ps->szmcsass); + ps->nmcsass = ps->szmcsass = 0; + ps->mcsass = 0; + } + + size = ps->alshead - ps->als; + NEWN (a, size); + + for (i = 0; i < size; i++) + a[i] = LIT2INT (ps->als[i]); + + (void) picosat_sat (ps, -1); + + //TODO short cut for 'picosat_res () == 10'? + + if (ps->mtcls) + { + assert (picosat_res (ps) == 20); + res = 0; + goto DONE; + } + + res = mss (ps, a, size); + + if (ps->mtcls) + { + res = 0; + goto DONE; + } + + for (p = res; (lit = *p); p++) + { + v = ps->vars + abs (lit); + if (lit < 0) + { + assert (!v->msspos); + v->mssneg = 1; + } + else + { + assert (!v->mssneg); + v->msspos = 1; + } + } + + mssize = p - res; + mcsize = INT_MIN; + + for (i = 0; i < size; i++) + { + lit = a[i]; + v = ps->vars + abs (lit); + if (lit > 0 && v->msspos) + inmss = 1; + else if (lit < 0 && v->mssneg) + inmss = 1; + else + inmss = 0; + + if (mssize < mcsize) + { + if (inmss) + picosat_add (ps, -lit); + } + else + { + if (!inmss) + picosat_add (ps, lit); + } + + if (!inmss && mcs) + push_mcsass (ps, lit); + } + picosat_add (ps, 0); + if (mcs) + push_mcsass (ps, 0); + + for (i = 0; i < size; i++) + { + lit = a[i]; + v = ps->vars + abs (lit); + v->msspos = 0; + v->mssneg = 0; + } + +DONE: + + reassume (ps, a, size); + DELETEN (a, size); + + return res; +} + +const int * +picosat_next_maximal_satisfiable_subset_of_assumptions (PS * ps) +{ + const int * res; + enter (ps); + res = next_mss (ps, 0); + leave (ps); + return res; +} + +const int * +picosat_next_minimal_correcting_subset_of_assumptions (PS * ps) +{ + const int * res, * tmp; + enter (ps); + tmp = next_mss (ps, 1); + res = tmp ? ps->mcsass : 0; + leave (ps); + return res; +} + +const int * +picosat_humus (PS * ps, + void (*callback)(void*state,int nmcs,int nhumus), + void * state) +{ + int lit, nmcs, j, nhumus; + const int * mcs, * p; + unsigned i; + Var * v; + enter (ps); +#ifndef NDEBUG + for (i = 1; i <= ps->max_var; i++) + { + v = ps->vars + i; + assert (!v->humuspos); + assert (!v->humusneg); + } +#endif + nhumus = nmcs = 0; + while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps))) + { + for (p = mcs; (lit = *p); p++) + { + v = ps->vars + abs (lit); + if (lit < 0) + { + if (!v->humusneg) + { + v->humusneg = 1; + nhumus++; + } + } + else + { + if (!v->humuspos) + { + v->humuspos = 1; + nhumus++; + } + } + } + nmcs++; + LOG ( fprintf (ps->out, + "%smcs %d of size %d humus %d\n", + ps->prefix, nmcs, (int)(p - mcs), nhumus)); + if (callback) + callback (state, nmcs, nhumus); + } + assert (!ps->szhumus); + ps->szhumus = 1; + for (i = 1; i <= ps->max_var; i++) + { + v = ps->vars + i; + if (v->humuspos) + ps->szhumus++; + if (v->humusneg) + ps->szhumus++; + } + assert (nhumus + 1 == ps->szhumus); + NEWN (ps->humus, ps->szhumus); + j = 0; + for (i = 1; i <= ps->max_var; i++) + { + v = ps->vars + i; + if (v->humuspos) + { + assert (j < nhumus); + ps->humus[j++] = (int) i; + } + if (v->humusneg) + { + assert (j < nhumus); + assert (i < INT_MAX); + ps->humus[j++] = - (int) i; + } + } + assert (j == nhumus); + assert (j < ps->szhumus); + ps->humus[j] = 0; + leave (ps); + return ps->humus; +} + +int +picosat_usedlit (PS * ps, int int_lit) +{ + int res; + check_ready (ps); + check_sat_or_unsat_or_unknown_state (ps); + ABORTIF (!int_lit, "API usage: zero literal can not be used"); + int_lit = abs (int_lit); + res = (int_lit <= (int) ps->max_var) ? ps->vars[int_lit].used : 0; + return res; +} + +void +picosat_write_clausal_core (PS * ps, FILE * file) +{ + check_trace_support_and_execute (ps, file, write_core_wrapper, 0); +} + +void +picosat_write_compact_trace (PS * ps, FILE * file) +{ + check_trace_support_and_execute (ps, file, write_trace, + COMPACT_TRACECHECK_TRACE_FMT); +} + +void +picosat_write_extended_trace (PS * ps, FILE * file) +{ + check_trace_support_and_execute (ps, file, write_trace, + EXTENDED_TRACECHECK_TRACE_FMT); +} + +void +picosat_write_rup_trace (PS * ps, FILE * file) +{ + check_trace_support_and_execute (ps, file, write_trace, RUP_TRACE_FMT); +} + +size_t +picosat_max_bytes_allocated (PS * ps) +{ + check_ready (ps); + return ps->max_bytes; +} + +void +picosat_set_propagation_limit (PS * ps, unsigned long long l) +{ + ps->lpropagations = l; +} + +unsigned long long +picosat_propagations (PS * ps) +{ + return ps->propagations; +} + +unsigned long long +picosat_visits (PS * ps) +{ + return ps->visits; +} + +unsigned long long +picosat_decisions (PS * ps) +{ + return ps->decisions; +} + +int +picosat_variables (PS * ps) +{ + check_ready (ps); + return (int) ps->max_var; +} + +int +picosat_added_original_clauses (PS * ps) +{ + check_ready (ps); + return (int) ps->oadded; +} + +void +picosat_stats (PS * ps) +{ +#ifndef RCODE + unsigned redlits; +#endif +#ifdef STATS + check_ready (ps); + assert (ps->sdecisions + ps->rdecisions + ps->assumptions == ps->decisions); +#endif + if (ps->calls > 1) + fprintf (ps->out, "%s%u calls\n", ps->prefix, ps->calls); + if (ps->contexts) + { + fprintf (ps->out, "%s%u contexts", ps->prefix, ps->contexts); +#ifdef STATS + fprintf (ps->out, " %u internal variables", ps->internals); +#endif + fprintf (ps->out, "\n"); + } + fprintf (ps->out, "%s%u iterations\n", ps->prefix, ps->iterations); + fprintf (ps->out, "%s%u restarts", ps->prefix, ps->restarts); +#ifdef STATS + fprintf (ps->out, " (%u skipped)", ps->skippedrestarts); +#endif + fputc ('\n', ps->out); +#ifndef NFL + fprintf (ps->out, "%s%u failed literals", ps->prefix, ps->failedlits); +#ifdef STATS + fprintf (ps->out, + ", %u calls, %u rounds, %llu propagations", + ps->flcalls, ps->flrounds, ps->flprops); +#endif + fputc ('\n', ps->out); +#ifdef STATS + fprintf (ps->out, + "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n", + ps->prefix, + ps->ifailedlits, PERCENT (ps->ifailedlits, ps->failedlits), + ps->floopsed, ps->fltried, ps->flskipped); +#endif +#endif + fprintf (ps->out, "%s%u conflicts", ps->prefix, ps->conflicts); +#ifdef STATS + fprintf (ps->out, " (%u uips = %.1f%%)\n", ps->uips, PERCENT(ps->uips,ps->conflicts)); +#else + fputc ('\n', ps->out); +#endif +#ifndef NADC + fprintf (ps->out, "%s%u adc conflicts\n", ps->prefix, ps->adoconflicts); +#endif +#ifdef STATS + fprintf (ps->out, "%s%llu dereferenced literals\n", ps->prefix, ps->derefs); +#endif + fprintf (ps->out, "%s%u decisions", ps->prefix, ps->decisions); +#ifdef STATS + fprintf (ps->out, " (%u random = %.2f%%", + ps->rdecisions, PERCENT (ps->rdecisions, ps->decisions)); + fprintf (ps->out, ", %u assumptions", ps->assumptions); + fputc (')', ps->out); +#endif + fputc ('\n', ps->out); +#ifdef STATS + fprintf (ps->out, + "%s%u static phase decisions (%.1f%% of all variables)\n", + ps->prefix, + ps->staticphasedecisions, PERCENT (ps->staticphasedecisions, ps->max_var)); +#endif + fprintf (ps->out, "%s%u fixed variables\n", ps->prefix, ps->fixed); + assert (ps->nonminimizedllits >= ps->minimizedllits); +#ifndef RCODE + redlits = ps->nonminimizedllits - ps->minimizedllits; +#endif + fprintf (ps->out, "%s%u learned literals\n", ps->prefix, ps->llitsadded); + fprintf (ps->out, "%s%.1f%% deleted literals\n", + ps->prefix, PERCENT (redlits, ps->nonminimizedllits)); + +#ifdef STATS +#ifdef TRACE + fprintf (ps->out, + "%s%llu antecedents (%.1f antecedents per clause", + ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts)); + if (ps->trace) + fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents)); + fputs (")\n", ps->out); +#endif + + fprintf (ps->out, "%s%llu propagations (%.1f propagations per decision)\n", + ps->prefix, ps->propagations, AVERAGE (ps->propagations, ps->decisions)); + fprintf (ps->out, "%s%llu visits (%.1f per propagation)\n", + ps->prefix, ps->visits, AVERAGE (ps->visits, ps->propagations)); + fprintf (ps->out, + "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n", + ps->prefix, ps->bvisits, + PERCENT (ps->bvisits, ps->visits), + AVERAGE (ps->bvisits, ps->propagations)); + fprintf (ps->out, + "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n", + ps->prefix, ps->tvisits, + PERCENT (ps->tvisits, ps->visits), + AVERAGE (ps->tvisits, ps->propagations)); + fprintf (ps->out, + "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n", + ps->prefix, ps->lvisits, + PERCENT (ps->lvisits, ps->visits), + AVERAGE (ps->lvisits, ps->propagations)); + fprintf (ps->out, "%s%llu other true (%.1f%% of visited clauses)\n", + ps->prefix, ps->othertrue, PERCENT (ps->othertrue, ps->visits)); + fprintf (ps->out, + "%s%llu other true in binary clauses (%.1f%%)" + ", %llu upper (%.1f%%)\n", + ps->prefix, ps->othertrue2, PERCENT (ps->othertrue2, ps->othertrue), + ps->othertrue2u, PERCENT (ps->othertrue2u, ps->othertrue2)); + fprintf (ps->out, + "%s%llu other true in large clauses (%.1f%%)" + ", %llu upper (%.1f%%)\n", + ps->prefix, ps->othertruel, PERCENT (ps->othertruel, ps->othertrue), + ps->othertruelu, PERCENT (ps->othertruelu, ps->othertruel)); + fprintf (ps->out, "%s%llu ternary and large traversals (%.1f per visit)\n", + ps->prefix, ps->traversals, AVERAGE (ps->traversals, ps->visits)); + fprintf (ps->out, "%s%llu large traversals (%.1f per large visit)\n", + ps->prefix, ps->ltraversals, AVERAGE (ps->ltraversals, ps->lvisits)); + fprintf (ps->out, "%s%llu assignments\n", ps->prefix, ps->assignments); +#else + fprintf (ps->out, "%s%llu propagations\n", ps->prefix, picosat_propagations (ps)); + fprintf (ps->out, "%s%llu visits\n", ps->prefix, picosat_visits (ps)); +#endif + fprintf (ps->out, "%s%.1f%% variables used\n", ps->prefix, PERCENT (ps->vused, ps->max_var)); + + sflush (ps); + fprintf (ps->out, "%s%.1f seconds in library\n", ps->prefix, ps->seconds); + fprintf (ps->out, "%s%.1f megaprops/second\n", + ps->prefix, AVERAGE (ps->propagations / 1e6f, ps->seconds)); + fprintf (ps->out, "%s%.1f megavisits/second\n", + ps->prefix, AVERAGE (ps->visits / 1e6f, ps->seconds)); + fprintf (ps->out, "%sprobing %.1f seconds %.0f%%\n", + ps->prefix, ps->flseconds, PERCENT (ps->flseconds, ps->seconds)); +#ifdef STATS + fprintf (ps->out, + "%srecycled %.1f MB in %u reductions\n", + ps->prefix, ps->rrecycled / (double) (1 << 20), ps->reductions); + fprintf (ps->out, + "%srecycled %.1f MB in %u simplifications\n", + ps->prefix, ps->srecycled / (double) (1 << 20), ps->simps); +#else + fprintf (ps->out, "%s%u simplifications\n", ps->prefix, ps->simps); + fprintf (ps->out, "%s%u reductions\n", ps->prefix, ps->reductions); + fprintf (ps->out, "%s%.1f MB recycled\n", ps->prefix, ps->recycled / (double) (1 << 20)); +#endif + fprintf (ps->out, "%s%.1f MB maximally allocated\n", + ps->prefix, picosat_max_bytes_allocated (ps) / (double) (1 << 20)); +} + +#ifndef NGETRUSAGE +#include <sys/time.h> +#include <sys/resource.h> +#include <sys/unistd.h> +#endif + +double +picosat_time_stamp (void) +{ + double res = -1; +#ifndef NGETRUSAGE + struct rusage u; + res = 0; + if (!getrusage (RUSAGE_SELF, &u)) + { + res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec; + res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec; + } +#endif + return res; +} + +double +picosat_seconds (PS * ps) +{ + check_ready (ps); + return ps->seconds; +} + +void +picosat_print (PS * ps, FILE * file) +{ +#ifdef NO_BINARY_CLAUSES + Lit * lit, *other, * last; + Ltk * stack; +#endif + Lit **q, **eol; + Cls **p, *c; + unsigned n; + + if (ps->measurealltimeinlib) + enter (ps); + else + check_ready (ps); + + n = 0; + n += ps->alshead - ps->als; + + for (p = SOC; p != EOC; p = NXC (p)) + { + c = *p; + + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + n++; + } + +#ifdef NO_BINARY_CLAUSES + last = int2lit (ps, -ps->max_var); + for (lit = int2lit (ps, 1); lit <= last; lit++) + { + stack = LIT2IMPLS (lit); + eol = stack->start + stack->count; + for (q = stack->start; q < eol; q++) + if (*q >= lit) + n++; + } +#endif + + fprintf (file, "p cnf %d %u\n", ps->max_var, n); + + for (p = SOC; p != EOC; p = NXC (p)) + { + c = *p; + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + + eol = end_of_lits (c); + for (q = c->lits; q < eol; q++) + fprintf (file, "%d ", LIT2INT (*q)); + + fputs ("0\n", file); + } + +#ifdef NO_BINARY_CLAUSES + last = int2lit (ps, -ps->max_var); + for (lit = int2lit (ps, 1); lit <= last; lit++) + { + stack = LIT2IMPLS (lit); + eol = stack->start + stack->count; + for (q = stack->start; q < eol; q++) + if ((other = *q) >= lit) + fprintf (file, "%d %d 0\n", LIT2INT (lit), LIT2INT (other)); + } +#endif + + { + Lit **r; + for (r = ps->als; r < ps->alshead; r++) + fprintf (file, "%d 0\n", LIT2INT (*r)); + } + + fflush (file); + + if (ps->measurealltimeinlib) + leave (ps); +} + +void +picosat_enter (PS * ps) +{ + enter (ps); +} + +void +picosat_leave (PS * ps) +{ + leave (ps); +} + +void +picosat_message (PS * ps, int vlevel, const char * fmt, ...) +{ + va_list ap; + + if (vlevel > ps->verbosity) + return; + + fputs (ps->prefix, ps->out); + va_start (ap, fmt); + vfprintf (ps->out, fmt, ap); + va_end (ap); + fputc ('\n', ps->out); +} + +int +picosat_changed (PS * ps) +{ + int res; + + check_ready (ps); + check_sat_state (ps); + + res = (ps->min_flipped <= ps->saved_max_var); + assert (!res || ps->saved_flips != ps->flips); + + return res; +} + +void +picosat_reset_phases (PS * ps) +{ + rebias (ps); +} + +void +picosat_reset_scores (PS * ps) +{ + Rnk * r; + ps->hhead = ps->heap + 1; + for (r = ps->rnks + 1; r <= ps->rnks + ps->max_var; r++) + { + CLR (r); + hpush (ps, r); + } +} + +void +picosat_remove_learned (PS * ps, unsigned percentage) +{ + enter (ps); + reset_incremental_usage (ps); + reduce (ps, percentage); + leave (ps); +} + +void +picosat_set_global_default_phase (PS * ps, int phase) +{ + check_ready (ps); + ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' " + "with negative argument"); + ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' " + "with argument > 3"); + 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 (PS * ps, unsigned newadoconflictlimit) +{ + check_ready (ps); + ps->adoconflictlimit = newadoconflictlimit; +} + +#endif + +void +picosat_simplify (PS * ps) +{ + enter (ps); + reset_incremental_usage (ps); + simplify (ps, 1); + leave (ps); +} + +int +picosat_haveados (void) +{ +#ifndef NADC + return 1; +#else + return 0; +#endif +} + +void +picosat_save_original_clauses (PS * ps) +{ + if (ps->saveorig) return; + ABORTIF (ps->oadded, "API usage: 'picosat_save_original_clauses' too late"); + ps->saveorig = 1; +} + +void picosat_set_interrupt (PicoSAT * ps, + void * external_state, + int (*interrupted)(void * external_state)) +{ + ps->interrupt.state = external_state; + ps->interrupt.function = interrupted; +} + +int +picosat_deref_partial (PS * ps, int int_lit) +{ + check_ready (ps); + check_sat_state (ps); + ABORTIF (!int_lit, "API usage: can not partial deref zero literal"); + ABORTIF (ps->mtcls, "API usage: deref partial after empty clause generated"); + ABORTIF (!ps->saveorig, "API usage: 'picosat_save_original_clauses' missing"); + +#ifdef STATS + ps->derefs++; +#endif + + if (!ps->partial) + minautarky (ps); + + return pderef (ps, int_lit); +} |