From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 21FC0C433EF for ; Fri, 22 Oct 2021 13:36:43 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id ED9856112F for ; Fri, 22 Oct 2021 13:36:42 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231537AbhJVNi7 (ORCPT ); Fri, 22 Oct 2021 09:38:59 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:42338 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231516AbhJVNi7 (ORCPT ); Fri, 22 Oct 2021 09:38:59 -0400 Received: from out2.mail.ruhr-uni-bochum.de (out2.mail.ruhr-uni-bochum.de [IPv6:2a05:3e00:c:1001::8693:2ae5]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 159BAC061764 for ; Fri, 22 Oct 2021 06:36:41 -0700 (PDT) Received: from mx2.mail.ruhr-uni-bochum.de (localhost [127.0.0.1]) by out2.mail.ruhr-uni-bochum.de (Postfix mo-ext) with ESMTP id 4HbQP35b3Rz8SJF; Fri, 22 Oct 2021 15:36:39 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=rub.de; s=mail-2017; t=1634909799; bh=4WVP6DWGBdUweprIk6AQzPgvlgA8hBdwcvOa8w3e1IQ=; h=Date:Subject:From:To:Cc:References:In-Reply-To:From; b=Dnt8IZOo5hQq7fdnNnVkGzUSf0NZPLT4QGDwM92cgqMylhI4sU6AtxZ5FdSxfDIrg RRptjwffKTVZNFLPD9Eg1vlbadgplMpEkSdsn+L2oZTVRVBnUXtMcFg6YO2jp9h3mF AaYbh8D0zJaRGFoCVUP7nmASjE7WZCY49JoLLTXQ= Received: from out2.mail.ruhr-uni-bochum.de (localhost [127.0.0.1]) by mx2.mail.ruhr-uni-bochum.de (Postfix idis) with ESMTP id 4HbQP34kkMz8SJ6; Fri, 22 Oct 2021 15:36:39 +0200 (CEST) X-RUB-Notes: Internal origin=IPv6:2a05:3e00:c:1001::8693:2aec X-Envelope-Sender: Received: from mail2.mail.ruhr-uni-bochum.de (mail2.mail.ruhr-uni-bochum.de [IPv6:2a05:3e00:c:1001::8693:2aec]) by out2.mail.ruhr-uni-bochum.de (Postfix mi-int) with ESMTP id 4HbQP33LLhz8SF3; Fri, 22 Oct 2021 15:36:39 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.1 at mx2.mail.ruhr-uni-bochum.de Received: from [10.150.66.4] (nb02.ig09.ruhr-uni-bochum.de [10.150.66.4]) by mail2.mail.ruhr-uni-bochum.de (Postfix) with ESMTPSA id 4HbQP31ZxHzDgyY; Fri, 22 Oct 2021 15:36:39 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.0 at mail2.mail.ruhr-uni-bochum.de Message-ID: Date: Fri, 22 Oct 2021 15:36:37 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.2.0 Subject: [RFC v3 02/12] Add picosat.c (1/3) Content-Language: en-US From: Thorsten Berger To: linux-kbuild@vger.kernel.org Cc: deltaone@debian.org, phayax@gmail.com, Eugene Groshev , Sarah Nadi , Mel Gorman , "Luis R. Rodriguez" References: <7706ed5e-4771-770a-5cf2-d3c8346fa1dc@rub.de> In-Reply-To: <7706ed5e-4771-770a-5cf2-d3c8346fa1dc@rub.de> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Precedence: bulk List-ID: X-Mailing-List: linux-kbuild@vger.kernel.org Subject: [RFC v3 02/12] Add picosat.c (1/3) PicoSAT is the SAT solver used in this project. picosat.c is the actual SAT solver. Since the file is too big for a single patch, it needs to be split up. This patch contains the first part of the file. ---  scripts/kconfig/picosat.c | 3000 +++++++++++++++++++++++++++++++++++++  1 file changed, 3000 insertions(+)  create mode 100644 scripts/kconfig/picosat.c diff --git a/scripts/kconfig/picosat.c b/scripts/kconfig/picosat.c new file mode 100644 index 000000000000..653bf0f0b99f --- /dev/null +++ b/scripts/kconfig/picosat.c @@ -0,0 +1,3000 @@ +/**************************************************************************** +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 +#include +#include +#include +#include +#include +#include +#include + +#include "picosat.h" + +/* By default code for 'all different constraints' is disabled, since 'NADC' + * is defined. + */ +#define NADC + +/* By default we enable failed literals, since 'NFL' is undefined. + * +#define NFL + */ + +/* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined. + * +#define NDSC + */ + +/* Do not use luby restart schedule instead of inner/outer. + * +#define NLUBY + */ + +/* Enabling this define, will use gnuplot to visualize how the scores evolve. + * +#define VISCORES + */ +#ifdef VISCORES +// #define WRITEGIF        /* ... to generate a video */ +#endif + +#ifdef VISCORES +#ifndef WRITEGIF +#include         /* for 'usleep' */ +#endif +#endif + +#ifdef RCODE +#include +#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<= FLTCARRY) +    { +      if (e >= FLTMAXEXPONENT) +        return INFFLT; + +      e++; +      m >>= 1; +    } +    } + +  m &= ~FLTMSB; +  return packflt (m, e); +} + +static Flt +addflt (Flt a, Flt b) +{ +  unsigned ma, mb, delta; +  int ea, eb; + +  CMPSWAPFLT (a, b); +  if (!b) +    return a; + +  UNPACKFLT (a, ma, ea); +  UNPACKFLT (b, mb, eb); + +  assert (ea >= eb); +  delta = ea - eb; +  if (delta < 32) mb >>= delta; else mb = 0; +  if (!mb) +    return a; + +  ma += mb; +  if (ma & FLTCARRY) +    { +      if (ea == FLTMAXEXPONENT) +    return INFFLT; + +      ea++; +      ma >>= 1; +    } + +  assert (ma < FLTCARRY); +  ma &= FLTMAXMANTISSA; + +  return packflt (ma, ea); +} + +static Flt +mulflt (Flt a, Flt b) +{ +  unsigned ma, mb; +  unsigned long long accu; +  int ea, eb; + +  CMPSWAPFLT (a, b); +  if (!b) +    return ZEROFLT; + +  UNPACKFLT (a, ma, ea); +  UNPACKFLT (b, mb, eb); + +  ea += eb; +  ea += 24; +  if (ea > FLTMAXEXPONENT) +    return INFFLT; + +  if (ea < FLTMINEXPONENT) +    return EPSFLT; + +  accu = ma; +  accu *= mb; +  accu >>= 24; + +  if (accu >= FLTCARRY) +    { +      if (ea == FLTMAXEXPONENT) +    return INFFLT; + +      ea++; +      accu >>= 1; + +      if (accu >= FLTCARRY) +    return INFFLT; +    } + +  assert (accu < FLTCARRY); +  assert (accu & FLTMSB); + +  ma = accu; +  ma &= ~FLTMSB; + +  return packflt (ma, ea); +} + +static Flt +ascii2flt (const char *str) +{ +  Flt ten = base2flt (10, 0); +  Flt onetenth = base2flt (26843546, -28); +  Flt res = ZEROFLT, tmp, base; +  const char *p = str; +  int ch; + +  ch = *p++; + +  if (ch != '.') +    { +      if (!isdigit (ch)) +    return INFFLT;    /* better abort ? */ + +      res = base2flt (ch - '0', 0); + +      while ((ch = *p++)) +    { +      if (ch == '.') +        break; + +      if (!isdigit (ch)) +        return INFFLT;    /* better abort? */ + +      res = mulflt (res, ten); +      tmp = base2flt (ch - '0', 0); +      res = addflt (res, tmp); +    } +    } + +  if (ch == '.') +    { +      ch = *p++; +      if (!isdigit (ch)) +    return INFFLT;    /* better abort ? */ + +      base = onetenth; +      tmp = mulflt (base2flt (ch - '0', 0), base); +      res = addflt (res, tmp); + +      while ((ch = *p++)) +    { +      if (!isdigit (ch)) +        return INFFLT;    /* better abort? */ + +      base = mulflt (base, onetenth); +      tmp = mulflt (base2flt (ch - '0', 0), base); +      res = addflt (res, tmp); +    } +    } + +  return res; +} + +#if defined(VISCORES) + +static double +flt2double (Flt f) +{ +  double res; +  unsigned m; +  int e, i; + +  UNPACKFLT (f, m, e); +  res = m; + +  if (e < 0) +    { +      for (i = e; i < 0; i++) +    res *= 0.5; +    } +  else +    { +      for (i = 0; i < e; i++) +    res *= 2.0; +    } + +  return res; +} + +#endif + +static int +log2flt (Flt a) +{ +  return FLTEXPONENT (a) + 24; +} + +static int +cmpflt (Flt a, Flt b) +{ +  if (a < b) +    return -1; + +  if (a > b) +    return 1; + +  return 0; +} + +static void * +new (PS * ps, size_t size) +{ +  size_t bytes; +  Blk *b; +   +  if (!size) +    return 0; + +  bytes = size + SIZE_OF_BLK; + +  if (ps->enew) +    b = ps->enew (ps->emgr, bytes); +  else +    b = malloc (bytes); + +  ABORTIF (!b, "out of memory in 'new'"); +#ifndef NDEBUG +  b->header.size = size; +#endif +  ps->current_bytes += size; +  if (ps->current_bytes > ps->max_bytes) +    ps->max_bytes = ps->current_bytes; +  return b->data; +} + +static void +delete (PS * ps, void *void_ptr, size_t size) +{ +  size_t bytes; +  Blk *b; + +  if (!void_ptr) +    { +      assert (!size); +      return; +    } + +  assert (size); +  b = PTR2BLK (void_ptr); + +  assert (size <= ps->current_bytes); +  ps->current_bytes -= size; + +  assert (b->header.size == size); + +  bytes = size + SIZE_OF_BLK; +  if (ps->edelete) +    ps->edelete (ps->emgr, b, bytes); +  else +    free (b); +} + +static void * +resize (PS * ps, void *void_ptr, size_t old_size, size_t new_size) +{ +  size_t old_bytes, new_bytes; +  Blk *b; + +  b = PTR2BLK (void_ptr); + +  assert (old_size <= ps->current_bytes); +  ps->current_bytes -= old_size; + +  if ((old_bytes = old_size)) +    { +      assert (old_size && b && b->header.size == old_size); +      old_bytes += SIZE_OF_BLK; +    } +  else +    assert (!b); + +  if ((new_bytes = new_size)) +    new_bytes += SIZE_OF_BLK; + +  if (ps->eresize) +    b = ps->eresize (ps->emgr, b, old_bytes, new_bytes); +  else +    b = realloc (b, new_bytes); + +  if (!new_size) +    { +      assert (!b); +      return 0; +    } + +  ABORTIF (!b, "out of memory in 'resize'"); +#ifndef NDEBUG +  b->header.size = new_size; +#endif + +  ps->current_bytes += new_size; +  if (ps->current_bytes > ps->max_bytes) +    ps->max_bytes = ps->current_bytes; + +  return b->data; +} + +static unsigned +int2unsigned (int l) +{ +  return (l < 0) ? 1 + 2 * -l : 2 * l; +} + +static Lit * +int2lit (PS * ps, int l) +{ +  return ps->lits + int2unsigned (l); +} + +static Lit ** +end_of_lits (Cls * c) +{ +  return (Lit**)c->lits + c->size; +} + +#if !defined(NDEBUG) || defined(LOGGING) + +static void +dumplits (PS * ps, Lit ** l, Lit ** end) +{ +  int first; +  Lit ** p; + +  if (l == end) +    { +      /* empty clause */ +    } +  else if (l + 1 == end) +    { +      fprintf (ps->out, "%d ", LIT2INT (l[0])); +    } +  else +    { +      assert (l + 2 <= end); +      first = (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1]))); +      fprintf (ps->out, "%d ", LIT2INT (l[first])); +      fprintf (ps->out, "%d ", LIT2INT (l[!first])); +      for (p = l + 2; p < end; p++) +     fprintf (ps->out, "%d ", LIT2INT (*p)); +    } + +  fputc ('0', ps->out); +} + +static void +dumpcls (PS * ps, Cls * c) +{ +  Lit **end; + +  if (c) +    { +      end = end_of_lits (c); +      dumplits (ps, c->lits, end); +#ifdef TRACE +      if (ps->trace) +     fprintf (ps->out, " clause(%u)", CLS2IDX (c)); +#endif +    } +  else +    fputs ("DECISION", ps->out); +} + +static void +dumpclsnl (PS * ps, Cls * c) +{ +  dumpcls (ps, c); +  fputc ('\n', ps->out); +} + +void +dumpcnf (PS * ps) +{ +  Cls **p, *c; + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; + +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif + +      dumpclsnl (ps, *p); +    } +} + +#endif + +static void +delete_prefix (PS * ps) +{ +  if (!ps->prefix) +    return; +     +  delete (ps, ps->prefix, strlen (ps->prefix) + 1); +  ps->prefix = 0; +} + +static void +new_prefix (PS * ps, const char * str) +{ +  delete_prefix (ps); +  assert (str); +  ps->prefix = new (ps, strlen (str) + 1); +  strcpy (ps->prefix, str); +} + +static PS * +init (void * pmgr, +      picosat_malloc pnew, picosat_realloc presize, picosat_free pdelete) +{ +  PS * ps; + +#if 0 +  int count = 3 - !pnew - !presize - !pdelete; + +  ABORTIF (count && !pnew, "API usage: missing 'picosat_set_new'"); +  ABORTIF (count && !presize, "API usage: missing 'picosat_set_resize'"); +  ABORTIF (count && !pdelete, "API usage: missing 'picosat_set_delete'"); +#endif + +  ps = pnew ? pnew (pmgr, sizeof *ps) : malloc (sizeof *ps); +  ABORTIF (!ps, "failed to allocate memory for PicoSAT manager"); +  memset (ps, 0, sizeof *ps); + +  ps->emgr = pmgr; +  ps->enew = pnew; +  ps->eresize = presize; +  ps->edelete = pdelete; + +  ps->size_vars = 1; +  ps->state = RESET; +  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 unsigned +llength (Lit ** a) +{ +  Lit ** p; +  for (p = a; *p; p++) +    ; +  return p - a; +} + +static void +resetadoconflict (PS * ps) +{ +  assert (ps->adoconflict); +  delete_clause (ps, ps->adoconflict); +  ps->adoconflict = 0; +} + +static void +reset_ados (PS * ps) +{ +  Lit *** p; + +  for (p = ps->ados; p < ps->hados; p++) +    DELETEN (*p, llength (*p) + 1); + +  DELETEN (ps->ados, ps->eados - ps->ados); +  ps->hados = ps->eados = 0; + +  DELETEN (ps->adotab, ps->szadotab); +  ps->szadotab = ps->nadotab = 0; + +  if (ps->adoconflict) +    resetadoconflict (ps); + +  ps->adoconflicts = 0; +  ps->adoconflictlimit = UINT_MAX; +  ps->adodisabled = 0; +} + +#endif + +static void +reset (PS * ps) +{ +  ABORTIF (!ps || +           ps->state == RESET, "API usage: reset without initialization"); + +  delete_clauses (ps); +#ifdef TRACE +  delete_zhains (ps); +#endif +#ifdef NO_BINARY_CLAUSES +  { +    unsigned i; +    for (i = 2; i <= 2 * ps->max_var + 1; i++) +      lrelease (ps, ps->impls + i); +  } +#endif +#ifndef NADC +  reset_ados (ps); +#endif +#ifndef NFL +  DELETEN (ps->saved, ps->saved_size); +#endif +  DELETEN (ps->htps, 2 * ps->size_vars); +#ifndef NDSC +  DELETEN (ps->dhtps, 2 * ps->size_vars); +#endif +  DELETEN (ps->impls, 2 * ps->size_vars); +  DELETEN (ps->lits, 2 * ps->size_vars); +  DELETEN (ps->jwh, 2 * ps->size_vars); +  DELETEN (ps->vars, ps->size_vars); +  DELETEN (ps->rnks, ps->size_vars); +  DELETEN (ps->trail, ps->eot - ps->trail); +  DELETEN (ps->heap, ps->eoh - ps->heap); +  DELETEN (ps->als, ps->eoals - ps->als); +  DELETEN (ps->CLS, ps->eocls - ps->CLS); +  DELETEN (ps->rils, ps->eorils - ps->rils); +  DELETEN (ps->cils, ps->eocils - ps->cils); +  DELETEN (ps->fals, ps->eofals - ps->fals); +  DELETEN (ps->mass, ps->szmass); +  DELETEN (ps->mssass, ps->szmssass); +  DELETEN (ps->mcsass, ps->szmcsass); +  DELETEN (ps->humus, ps->szhumus); +  DELETEN (ps->added, ps->eoa - ps->added); +  DELETEN (ps->marked, ps->eom - ps->marked); +  DELETEN (ps->dfs, ps->eod - ps->dfs); +  DELETEN (ps->resolved, ps->eor - ps->resolved); +  DELETEN (ps->levels, ps->eolevels - ps->levels); +  DELETEN (ps->dused, ps->eodused - ps->dused); +  DELETEN (ps->buffer, ps->eob - ps->buffer); +  DELETEN (ps->indices, ps->eoi - ps->indices); +  DELETEN (ps->soclauses, ps->eoso - ps->soclauses); +  delete_prefix (ps); +  delete (ps, ps->rline[0], ps->szrline); +  delete (ps, ps->rline[1], ps->szrline); +  assert (getenv ("LEAK") || !ps->current_bytes);    /* found leak if failing */ +#ifdef VISCORES +  pclose (ps->fviscores); +#endif +  if (ps->edelete) +    ps->edelete (ps->emgr, ps, sizeof *ps); +  else +    free (ps); +} + +inline static void +tpush (PS * ps, Lit * lit) +{ +  assert (ps->lits < lit && lit <= ps->lits + 2* ps->max_var + 1); +  if (ps->thead == ps->eot) +    { +      unsigned ttail2count = ps->ttail2 - ps->trail; +      unsigned ttailcount = ps->ttail - ps->trail; +#ifndef NADC +      unsigned ttailadocount = ps->ttailado - ps->trail; +#endif +      ENLARGE (ps->trail, ps->thead, ps->eot); +      ps->ttail = ps->trail + ttailcount; +      ps->ttail2 = ps->trail + ttail2count; +#ifndef NADC +      ps->ttailado = ps->trail + ttailadocount; +#endif +    } + +  *ps->thead++ = lit; +} + +static void +assign_reason (PS * ps, Var * v, Cls * reason) +{ +#if defined(NO_BINARY_CLAUSES) && !defined(NDEBUG) +  assert (reason != &ps->impl); +#else +  (void) ps; +#endif +  v->reason = reason; +} + +static void +assign_phase (PS * ps, Lit * lit) +{ +  unsigned new_phase, idx; +  Var * v = LIT2VAR (lit); + +#ifndef NFL +  /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if +   * we force assignments on the top level.   The other assignments will be +   * undone and thus we can keep the old saved value of the phase. +   */ +  if (!ps->LEVEL || !ps->simplifying) +#endif +    { +      new_phase = (LIT2SGN (lit) > 0); + +      if (v->assigned) +    { +      ps->sdflips -= ps->sdflips/FFLIPPED; + +      if (new_phase != v->phase) +        { +          assert (FFLIPPEDPREC >= FFLIPPED); +          ps->sdflips += FFLIPPEDPREC / FFLIPPED; +          ps->flips++; + +          idx = LIT2IDX (lit); +          if (idx < ps->min_flipped) +        ps->min_flipped = idx; + +              NOLOG (fprintf (ps->out, +                          "%sflipped %d\n", +                   ps->prefix, LIT2INT (lit))); +        } +    } + +      v->phase = new_phase; +      v->assigned = 1; +    } + +  lit->val = TRUE; +  NOTLIT (lit)->val = FALSE; +} + +inline static void +assign (PS * ps, Lit * lit, Cls * reason) +{ +  Var * v = LIT2VAR (lit); +  assert (lit->val == UNDEF); +#ifdef STATS +  ps->assignments++; +#endif +  v->level = ps->LEVEL; +  assign_phase (ps, lit); +  assign_reason (ps, v, reason); +  tpush (ps, lit); +} + +inline static int +cmp_added (PS * ps, Lit * k, Lit * l) +{ +  Val a = k->val, b = l->val; +  Var *u, *v; +  int res; + +  if (a == UNDEF && b != UNDEF) +    return -1; + +  if (a != UNDEF && b == UNDEF) +    return 1; + +  u = LIT2VAR (k); +  v = LIT2VAR (l); + +  if (a != UNDEF) +    { +      assert (b != UNDEF); +      res = v->level - u->level; +      if (res) +    return res;        /* larger level first */ +    } + +  res = cmpflt (VAR2RNK (u)->score, VAR2RNK (v)->score); +  if (res) +    return res;            /* smaller activity first */ + +  return u - v;            /* smaller index first */ +} + +static void +sorttwolits (Lit ** v) +{ +  Lit * a = v[0], * b = v[1]; + +  assert (a != b); + +  if (a < b) +    return; + +  v[0] = b; +  v[1] = a; +} + +inline static void +sortlits (PS * ps, Lit ** v, unsigned size) +{ +  if (size == 2) +    sorttwolits (v);    /* same order with and with out 'NO_BINARY_CLAUSES' */ +  else +    SORT (Lit *, cmp_added, v, size); +} + +#ifdef NO_BINARY_CLAUSES +static Cls * +setimpl (PS * ps, Lit * a, Lit * b) +{ +  assert (!ps->implvalid); +  assert (ps->impl.size == 2); + +  ps->impl.lits[0] = a; +  ps->impl.lits[1] = b; + +  sorttwolits (ps->impl.lits); +  ps->implvalid = 1; + +  return &ps->impl; +} + +static void +resetimpl (PS * ps) +{ +  ps->implvalid = 0; +} + +static Cls * +setcimpl (PS * ps, Lit * a, Lit * b) +{ +  assert (!ps->cimplvalid); +  assert (ps->cimpl.size == 2); + +  ps->cimpl.lits[0] = a; +  ps->cimpl.lits[1] = b; + +  sorttwolits (ps->cimpl.lits); +  ps->cimplvalid = 1; + +  return &ps->cimpl; +} + +static void +resetcimpl (PS * ps) +{ +  assert (ps->cimplvalid); +  ps->cimplvalid = 0; +} + +#endif + +static int +cmp_ptr (PS * ps, void *l, void *k) +{ +  (void) ps; +  return ((char*)l) - (char*)k;        /* arbitrarily already reverse */ +} + +static int +cmp_rnk (Rnk * r, Rnk * s) +{ +  if (!r->moreimportant && s->moreimportant) +    return -1; + +  if (r->moreimportant && !s->moreimportant) +    return 1; + +  if (!r->lessimportant && s->lessimportant) +    return 1; + +  if (r->lessimportant && !s->lessimportant) +    return -1; + +  if (r->score < s->score) +    return -1; + +  if (r->score > s->score) +    return 1; + +  return -cmp_ptr (0, r, s); +} + +static void +hup (PS * ps, Rnk * v) +{ +  int upos, vpos; +  Rnk *u; + +#ifndef NFL +  assert (!ps->simplifying); +#endif + +  vpos = v->pos; + +  assert (0 < vpos); +  assert (vpos < ps->hhead - ps->heap); +  assert (ps->heap[vpos] == v); + +  while (vpos > 1) +    { +      upos = vpos / 2; + +      u = ps->heap[upos]; + +      if (cmp_rnk (u, v) > 0) +    break; + +      ps->heap[vpos] = u; +      u->pos = vpos; + +      vpos = upos; +    } + +  ps->heap[vpos] = v; +  v->pos = vpos; +} + +static Cls *add_simplified_clause (PS *, int); + +inline static void +add_antecedent (PS * ps, Cls * c) +{ +  assert (c); + +#ifdef NO_BINARY_CLAUSES +  if (ISLITREASON (c)) +    return; + +  if (c == &ps->impl) +    return; +#elif defined(STATS) && defined(TRACE) +  ps->antecedents++; +#endif +  if (ps->rhead == ps->eor) +    ENLARGE (ps->resolved, ps->rhead, ps->eor); + +  assert (ps->rhead < ps->eor); +  *ps->rhead++ = c; +} + +#ifdef TRACE + +#ifdef NO_BINARY_CLAUSES +#error "can not combine TRACE and NO_BINARY_CLAUSES" +#endif + +#endif /* TRACE */ + +static void +add_lit (PS * ps, Lit * lit) +{ +  assert (lit); + +  if (ps->ahead == ps->eoa) +    ENLARGE (ps->added, ps->ahead, ps->eoa); + +  *ps->ahead++ = lit; +} + +static void +push_var_as_marked (PS * ps, Var * v) +{ +  if (ps->mhead == ps->eom) +    ENLARGE (ps->marked, ps->mhead, ps->eom); + +  *ps->mhead++ = v; +} + +static void +mark_var (PS * ps, Var * v) +{ +  assert (!v->mark); +  v->mark = 1; +  push_var_as_marked (ps, v); +} + +#ifdef NO_BINARY_CLAUSES + +static Cls * +impl2reason (PS * ps, Lit * lit) +{ +  Lit * other; +  Cls * res; +  other = ps->impl.lits[0]; +  if (lit == other) +    other = ps->impl.lits[1]; +  assert (other->val == FALSE); +  res = LIT2REASON (NOTLIT (other)); +  resetimpl (ps); +  return res; +} + +#endif + +/* Whenever we have a top level derived unit we really should derive a unit + * clause otherwise the resolutions in 'add_simplified_clause' become + * incorrect. + */ +static Cls * +resolve_top_level_unit (PS * ps, Lit * lit, Cls * reason) +{ +  unsigned count_resolved; +  Lit **p, **eol, *other; +  Var *u, *v; + +  assert (ps->rhead == ps->resolved); +  assert (ps->ahead == ps->added); + +  add_lit (ps, lit); +  add_antecedent (ps, reason); +  count_resolved = 1; +  v = LIT2VAR (lit); + +  eol = end_of_lits (reason); +  for (p = reason->lits; p < eol; p++) +    { +      other = *p; +      u = LIT2VAR (other); +      if (u == v) +    continue; + +      add_antecedent (ps, u->reason); +      count_resolved++; +    } + +  /* Some of the literals could be assumptions.  If at least one +   * variable is not an assumption, we should resolve. +   */ +  if (count_resolved >= 2) +    { +#ifdef NO_BINARY_CLAUSES +      if (reason == &ps->impl) +    resetimpl (ps); +#endif +      reason = add_simplified_clause (ps, 1); +#ifdef NO_BINARY_CLAUSES +      if (reason->size == 2) +    { +      assert (reason == &ps->impl); +      reason = impl2reason (ps, lit); +    } +#endif +      assign_reason (ps, v, reason); +    } +  else +    { +      ps->ahead = ps->added; +      ps->rhead = ps->resolved; +    } + +  return reason; +} + +static void +fixvar (PS * ps, Var * v) +{ +  Rnk * r; + +  assert (VAR2LIT (v) != UNDEF); +  assert (!v->level); + +  ps->fixed++; + +  r = VAR2RNK (v); +  r->score = INFFLT; + +#ifndef NFL +  if (ps->simplifying) +    return; +#endif + +  if (!r->pos) +    return; + +  hup (ps, r); +} + +static void +use_var (PS * ps, Var * v) +{ +  if (v->used) +    return; + +  v->used = 1; +  ps->vused++; +} + +static void +assign_forced (PS * ps, Lit * lit, Cls * reason) +{ +  Var *v; + +  assert (reason); +  assert (lit->val == UNDEF); + +#ifdef STATS +  ps->FORCED++; +#endif +  assign (ps, lit, reason); + +#ifdef NO_BINARY_CLAUSES +  assert (reason != &ps->impl); +  if (ISLITREASON (reason)) +    { +      reason = setimpl (ps, lit, NOTLIT (REASON2LIT (reason))); +      assert (reason); +    } +#endif +  LOG ( fprintf (ps->out, +                "%sassign %d at level %d by ", +                ps->prefix, LIT2INT (lit), ps->LEVEL); +       dumpclsnl (ps, reason)); + +  v = LIT2VAR (lit); +  if (!ps->LEVEL) +    use_var (ps, v); + +  if (!ps->LEVEL && reason->size > 1) +    { +      reason = resolve_top_level_unit (ps, lit, reason); +      assert (reason); +    } + +#ifdef NO_BINARY_CLAUSES +  if (ISLITREASON (reason) || reason == &ps->impl) +    { +      /* DO NOTHING */ +    } +  else +#endif +    { +      assert (!reason->locked); +      reason->locked = 1; +      if (reason->learned && reason->size > 2) +    ps->llocked++; +    } + +#ifdef NO_BINARY_CLAUSES +  if (reason == &ps->impl) +    resetimpl (ps); +#endif + +  if (!ps->LEVEL) +    fixvar (ps, v); +} + +#ifdef NO_BINARY_CLAUSES + +static void +lpush (PS * ps, Lit * lit, Cls * c) +{ +  int pos = (c->lits[0] == lit); +  Ltk * s = LIT2IMPLS (lit); +  unsigned oldsize, newsize; + +  assert (c->size == 2); + +  if (!s->start) +    { +      assert (!s->count); +      assert (!s->ldsize); +      NEWN (s->start, 1); +    } +  else +    { +      oldsize = (1 << (s->ldsize)); +      assert (s->count <= oldsize); +      if (s->count == oldsize) +    { +      newsize = 2 * oldsize; +      RESIZEN (s->start, oldsize, newsize); +      s->ldsize++; +    } +    } + +  s->start[s->count++] = c->lits[pos]; +} + +#endif + +static void +connect_head_tail (PS * ps, Lit * lit, Cls * c) +{ +  Cls ** s; +  assert (c->size >= 1); +  if (c->size == 2) +    { +#ifdef NO_BINARY_CLAUSES +      lpush (ps, lit, c); +      return; +#else +      s = LIT2IMPLS (lit); +#endif +    } +  else +    s = LIT2HTPS (lit); + +  if (c->lits[0] != lit) +    { +      assert (c->size >= 2); +      assert (c->lits[1] == lit); +      c->next[1] = *s; +    } +  else +    c->next[0] = *s; + +  *s = c; +} + +#ifdef TRACE +static void +zpush (PS * ps, Zhn * zhain) +{ +  assert (ps->trace); + +  if (ps->zhead == ps->eoz) +    ENLARGE (ps->zhains, ps->zhead, ps->eoz); + +  *ps->zhead++ = zhain; +} + +static int +cmp_resolved (PS * ps, Cls * c, Cls * d) +{ +#ifndef NDEBUG +  assert (ps->trace); +#else +  (void) ps; +#endif +  return CLS2IDX (c) - CLS2IDX (d); +} + +static void +bpushc (PS * ps, unsigned char ch) +{ +  if (ps->bhead == ps->eob) +    ENLARGE (ps->buffer, ps->bhead, ps->eob); + +  *ps->bhead++ = ch; +} + +static void +bpushu (PS * ps, unsigned u) +{ +  while (u & ~0x7f) +    { +      bpushc (ps, u | 0x80); +      u >>= 7; +    } + +  bpushc (ps, u); +} + +static void +bpushd (PS * ps, unsigned prev, unsigned this) +{ +  unsigned delta; +  assert (prev < this); +  delta = this - prev; +  bpushu (ps, delta); +} + +static void +add_zhain (PS * ps) +{ +  unsigned prev, this, count, rcount; +  Cls **p, *c; +  Zhn *res; + +  assert (ps->trace); +  assert (ps->bhead == ps->buffer); +  assert (ps->rhead > ps->resolved); + +  rcount = ps->rhead - ps->resolved; +  SORT (Cls *, cmp_resolved, ps->resolved, rcount); + +  prev = 0; +  for (p = ps->resolved; p < ps->rhead; p++) +    { +      c = *p; +      this = CLS2TRD (c)->idx; +      bpushd (ps, prev, this); +      prev = this; +    } +  bpushc (ps, 0); + +  count = ps->bhead - ps->buffer; + +  res = new (ps, sizeof (Zhn) + count); +  res->core = 0; +  res->ref = 0; +  memcpy (res->znt, ps->buffer, count); + +  ps->bhead = ps->buffer; +#ifdef STATS +  ps->znts += count - 1; +#endif +  zpush (ps, res); +} + +#endif + +static void +add_resolved (PS * ps, int learned) +{ +#if defined(STATS) || defined(TRACE) +  Cls **p, *c; + +  for (p = ps->resolved; p < ps->rhead; p++) +    { +      c = *p; +      if (c->used) +    continue; + +      c->used = 1; + +      if (c->size <= 2) +    continue; + +#ifdef STATS +      if (c->learned) +    ps->llused++; +      else +    ps->loused++; +#endif +    } +#endif + +#ifdef TRACE +  if (learned && ps->trace) +    add_zhain (ps); +#else +  (void) learned; +#endif +  ps->rhead = ps->resolved; +} + +static void +incjwh (PS * ps, Cls * c) +{ +  Lit **p, *lit, ** eol; +  Flt * f, inc, sum; +  unsigned size = 0; +  Var * v; +  Val val; + +  eol = end_of_lits (c); + +  for (p = c->lits; p < eol; p++) +    { +      lit = *p; +      val = lit->val; + +      if (val && ps->LEVEL > 0) +    { +      v = LIT2VAR (lit); +      if (v->level > 0) +        val = UNDEF; +    } + +      if (val == TRUE) +    return; + +      if (val != FALSE) +    size++; +    } + +  inc = base2flt (1, -size); + +  for (p = c->lits; p < eol; p++) +    { +      lit = *p; +      f = LIT2JWH (lit); +      sum = addflt (*f, inc); +      *f = sum; +    } +} + +static void +write_rup_header (PS * ps, FILE * file) +{ +  char line[80]; +  int i; + +  sprintf (line, "%%RUPD32 %u %u", ps->rupvariables, ps->rupclauses); + +  fputs (line, file); +  for (i = 255 - strlen (line); i >= 0; i--) +    fputc (' ', file); + +  fputc ('\n', file); +  fflush (file); +} + +static Cls * +add_simplified_clause (PS * ps, int learned) +{ +  unsigned num_true, num_undef, num_false, size, count_resolved; +  Lit **p, **q, *lit, ** end; +  unsigned litlevel, glue; +  Cls *res, * reason; +  int reentered; +  Val val; +  Var *v; +#if !defined(NDEBUG) && defined(TRACE) +  unsigned idx; +#endif + +  reentered = 0; + +REENTER: + +  size = ps->ahead - ps->added; + +  add_resolved (ps, learned); + +  if (learned) +    { +      ps->ladded++; +      ps->llitsadded += size; +      if (size > 2) +    { +      ps->lladded++; +      ps->nlclauses++; +      ps->llits += size; +    } +    } +  else +    { +      ps->oadded++; +      if (size > 2) +    { +      ps->loadded++; +      ps->noclauses++; +      ps->olits += size; +    } +    } + +  ps->addedclauses++; +  assert (ps->addedclauses == ps->ladded + ps->oadded); + +#ifdef NO_BINARY_CLAUSES +  if (size == 2) +    res = setimpl (ps, ps->added[0], ps->added[1]); +  else +#endif +    { +      sortlits (ps, ps->added, size); + +      if (learned) +    { +      if (ps->lhead == ps->EOL) +        { +          ENLARGE (ps->lclauses, ps->lhead, ps->EOL); + +          /* A very difficult to find bug, which only occurs if the +           * learned clauses stack is immediately allocated before the +           * original clauses stack without padding.  In this case, we +           * have 'SOC == EOC', which terminates all loops using the +           * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately. +           * Unfortunately this occurred in 'fix_clause_lits' after +           * using a recent version of the memory allocator of 'Google' +           * perftools in the context of one large benchmark for +           * our SMT solver 'Boolector'. +           */ +          if (ps->EOL == ps->oclauses) +        ENLARGE (ps->lclauses, ps->lhead, ps->EOL); +        } + +#if !defined(NDEBUG) && defined(TRACE) +      idx = LIDX2IDX (ps->lhead - ps->lclauses); +#endif +    } +      else +    { +      if (ps->ohead == ps->eoo) +        { +          ENLARGE (ps->oclauses, ps->ohead, ps->eoo); +          if (ps->EOL == ps->oclauses) +        ENLARGE (ps->oclauses, ps->ohead, ps->eoo);    /* ditto */ +        } + +#if !defined(NDEBUG) && defined(TRACE) +      idx = OIDX2IDX (ps->ohead - ps->oclauses); +#endif +    } + +      assert (ps->EOL != ps->oclauses);            /* ditto */ + +      res = new_clause (ps, size, learned); + +      glue = 0; + +      if (learned) +    { +      assert (ps->dusedhead == ps->dused); + +      for (p = ps->added; p < ps->ahead; p++) +        { +          lit = *p; +          if (lit->val) +        { +          litlevel = LIT2VAR (lit)->level; +          assert (litlevel <= ps->LEVEL); +          while (ps->levels + litlevel >= ps->levelshead) +            { +              if (ps->levelshead >= ps->eolevels) +            ENLARGE (ps->levels, ps->levelshead, ps->eolevels); +              assert (ps->levelshead < ps->eolevels); +              *ps->levelshead++ = 0; +            } +          if (!ps->levels[litlevel]) +            { +              if (ps->dusedhead >= ps->eodused) +            ENLARGE (ps->dused, ps->dusedhead, ps->eodused); +              assert (ps->dusedhead < ps->eodused); +              *ps->dusedhead++ = litlevel; +              ps->levels[litlevel] = 1; +              glue++; +            } +        } +          else +        glue++; +        } + +      while (ps->dusedhead > ps->dused) +        { +          litlevel = *--ps->dusedhead; +          assert (ps->levels + litlevel < ps->levelshead); +          assert (ps->levels[litlevel]); +          ps->levels[litlevel] = 0; +        } +    } + +      assert (glue <= MAXGLUE); +      res->glue = glue; + +#if !defined(NDEBUG) && defined(TRACE) +      if (ps->trace) +    assert (CLS2IDX (res) == idx); +#endif +      if (learned) +    *ps->lhead++ = res; +      else +    *ps->ohead++ = res; + +#if !defined(NDEBUG) && defined(TRACE) +      if (ps->trace && learned) +    assert (ps->zhead - ps->zhains == ps->lhead - ps->lclauses); +#endif +      assert (ps->lhead != ps->oclauses);        /* ditto */ +    } + +  if (learned && 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 void +fix_trail_lits (PS * ps, long delta) +{ +  Lit **p; +  for (p = ps->trail; p < ps->thead; p++) +    *p += delta; +} + +#ifdef NO_BINARY_CLAUSES +static void +fix_impl_lits (PS * ps, long delta) +{ +  Ltk * s; +  Lit ** p; + +  for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++) +    for (p = s->start; p < s->start + s->count; p++) +      *p += delta; +} +#endif + +static void +fix_clause_lits (PS * ps, long delta) +{ +  Cls **p, *clause; +  Lit **q, *lit, **eol; + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      clause = *p; +      if (!clause) +    continue; + +      q = clause->lits; +      eol = end_of_lits (clause); +      while (q < eol) +    { +      assert (q - clause->lits <= (int) clause->size); +      lit = *q; +      lit += delta; +      *q++ = lit; +    } +    } +} + +static void +fix_added_lits (PS * ps, long delta) +{ +  Lit **p; +  for (p = ps->added; p < ps->ahead; p++) +    *p += delta; +} + +static void +fix_assumed_lits (PS * ps, long delta) +{ +  Lit **p; +  for (p = ps->als; p < ps->alshead; p++) +    *p += delta; +} + +static void +fix_cls_lits (PS * ps, long delta) +{ +  Lit **p; +  for (p = ps->CLS; p < ps->clshead; p++) +    *p += delta; +} + +static void +fix_heap_rnks (PS * ps, long delta) +{ +  Rnk **p; + +  for (p = ps->heap + 1; p < ps->hhead; p++) +    *p += delta; +} + +#ifndef NADC + +static void +fix_ado (long delta, Lit ** ado) +{ +  Lit ** p; +  for (p = ado; *p; p++) +    *p += delta; +} + +static void +fix_ados (PS * ps, long delta) +{ +  Lit *** p; + +  for (p = ps->ados; p < ps->hados; p++) +    fix_ado (delta, *p); +} + +#endif + +static void +enlarge (PS * ps, unsigned new_size_vars) +{ +  long rnks_delta, lits_delta; +  Lit *old_lits = ps->lits; +  Rnk *old_rnks = ps->rnks; + +  RESIZEN (ps->lits, 2 * ps->size_vars, 2 * new_size_vars); +  RESIZEN (ps->jwh, 2 * ps->size_vars, 2 * new_size_vars); +  RESIZEN (ps->htps, 2 * ps->size_vars, 2 * new_size_vars); +#ifndef NDSC +  RESIZEN (ps->dhtps, 2 * ps->size_vars, 2 * new_size_vars); +#endif +  RESIZEN (ps->impls, 2 * ps->size_vars, 2 * new_size_vars); +  RESIZEN (ps->vars, ps->size_vars, new_size_vars); +  RESIZEN (ps->rnks, ps->size_vars, new_size_vars); + +  if ((lits_delta = ps->lits - old_lits)) +    { +      fix_trail_lits (ps, lits_delta); +      fix_clause_lits (ps, lits_delta); +      fix_added_lits (ps, lits_delta); +      fix_assumed_lits (ps, lits_delta); +      fix_cls_lits (ps, lits_delta); +#ifdef NO_BINARY_CLAUSES +      fix_impl_lits (ps, lits_delta); +#endif +#ifndef NADC +      fix_ados (ps, lits_delta); +#endif +    } + +  if ((rnks_delta = ps->rnks - old_rnks)) +    { +      fix_heap_rnks (ps, rnks_delta); +    } + +  assert (ps->mhead == ps->marked); + +  ps->size_vars = new_size_vars; +} + +static void +unassign (PS * ps, Lit * lit) +{ +  Cls *reason; +  Var *v; +  Rnk *r; + +  assert (lit->val == TRUE); + +  LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit))); + +  v = LIT2VAR (lit); +  reason = v->reason; + +#ifdef NO_BINARY_CLAUSES +  assert (reason != &ps->impl); +  if (ISLITREASON (reason)) +    { +      /* DO NOTHING */ +    } +  else +#endif +  if (reason) +    { +      assert (reason->locked); +      reason->locked = 0; +      if (reason->learned && reason->size > 2) +    { +      assert (ps->llocked > 0); +      ps->llocked--; +    } +    } + +  lit->val = UNDEF; +  NOTLIT (lit)->val = UNDEF; + +  r = VAR2RNK (v); +  if (!r->pos) +    hpush (ps, r); + +#ifndef NDSC +  { +    Cls * p, * next, ** q; + +    q = LIT2DHTPS (lit); +    p = *q; +    *q = 0; + +    while (p) +      { +    Lit * other = p->lits[0]; + +    if (other == lit) +      { +        other = p->lits[1]; +        q = p->next + 1; -- 2.33.0