From nobody Wed Dec 17 15:33:24 2025 Received: from mail-lj1-f181.google.com (mail-lj1-f181.google.com [209.85.208.181]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id F024D7BB06; Wed, 10 Jul 2024 06:54:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.208.181 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1720594474; cv=none; b=anhs+eVSymwFSHdIZjqewUWWz9RvW1i7JTY4B+h1c3WU661PyXbgLjO3hXpPXi20O9Y/xdcuikkuqL/hYmt7Se93MjQF5LlokGuHm7GTa11A4TQkbSrTUj9ci8U8U7wqtwIkHJX5SoivkLRKvInixd0PtqNGi1y22W8z3AP5By0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1720594474; c=relaxed/simple; bh=RqawAEV+fmtmwlfKkxY79Y8QX5x7zi3iFGYhOs5QYW0=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=eIe6TeAMD5zdYxEv2ViYznTGnm64WPAsjzfbbQ6W/boto3jX+puE1QPUSgWaVvfyHhTmYpd8FMnv+bklN/dkuO1z+ghWfFlMIiU4uIks7KU7BQhp9L1zV+xdj7Qn85R94ReyQ5CKpcpzwaoUU7BLjBEvQb0qG50EdEPsygHUwcE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=UAymWaH2; arc=none smtp.client-ip=209.85.208.181 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="UAymWaH2" Received: by mail-lj1-f181.google.com with SMTP id 38308e7fff4ca-2ec61eeed8eso71203901fa.0; Tue, 09 Jul 2024 23:54:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1720594468; x=1721199268; darn=vger.kernel.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=9OiR6XqTxrPzfPOqCzsX9poP6s4vUBvThBfmkaA77SI=; b=UAymWaH2jDZCsxOD8lsrmdOQCdn2KYg67s/mLavZb4tT17IJJ3tCYPcMVkCSljnl1t NCksOke3Z1AB06rw8VzTayuw+cL30kAGM7w88f79fVgFWQ3QlwXfVebWgpWd/T9sps41 4jdPzkpy/69DcBbGw8+aaFbDk8lRat0I4yavwOg9GkzzsLophKxNQMBdu2qx7ZOs3EPG k1N6BUSMywDMWHq/bzCPfbkLi0XpnYJhDdJ6xb7FXew4Lrp5RjaZJOAX+aBNWtz1Ikl2 iKMkzw0ZM+KE5asX5t3KMYxn4ChKK4+gad+HKJpnR4o2NtRU8txblQDPLzRZYItAue/u fxMg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1720594468; x=1721199268; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=9OiR6XqTxrPzfPOqCzsX9poP6s4vUBvThBfmkaA77SI=; b=JKymh7zOwxQeuGY/JvhVujQaDpMYrmRwNRkZOB6SfmzKkS9DXVi7ufQSC9JZ1DXThF oGkXOIZw15B+eavTL8Kg1LaxqtyWjXKuu58WqnxinRKn72XwI3xr4WjsOKX2Bv9UfrMn KieWGFctVmcyWw3f+pA96k97JmJkoJ/aHjYft1ZiR5ffTMWLx6W1yMA0ePMid6/xuQnx BZWUIpnITg+vzxQz0+mZ+cu2u4wYyUK9sdLGNOlb4XRikY4r7mAiMTwwf7c2xHOpKwnB BBi1o44Tc2sRqOKHGYJgZWlPQPlkIA7UTH2j+WPAVHI/hh+oi50yVjf8jBfQ/MkKXRqD ye7Q== X-Forwarded-Encrypted: i=1; AJvYcCU5BHVwuUoXVCq5TTmfNCWqnrmyD5AagFQ8fBpFxiw1uv60assNczFvuSMa9++Xj41H6sn0vv6VWJMAAkV0x9EyjlE5AlVGIIZCxMwi X-Gm-Message-State: AOJu0YwtQUv6xu4Yg/kOytuC0kHuYbjflGl7PXNGWMZyNR9qgj1cCm40 CrV7LzW6TTe+ymGIsgQuPW2hy0iUAKGiwaI7uN3lXT4yFRFaskqR0utvFg== X-Google-Smtp-Source: AGHT+IHDyyGtiX42HJdETXWil2T7ot/rKZCraJ/MYgYj76JD+D0z0kdm++YpEoqyDR+eOnyt6HNz/Q== X-Received: by 2002:a2e:6e0e:0:b0:2ee:7b7d:66ee with SMTP id 38308e7fff4ca-2eeb318a2f2mr27094331fa.41.1720594467356; Tue, 09 Jul 2024 23:54:27 -0700 (PDT) Received: from localhost.localdomain ([2a02:908:e842:bf20::c7d2]) by smtp.gmail.com with ESMTPSA id 4fb4d7f45d1cf-594bc7c8a39sm1894590a12.55.2024.07.09.23.54.24 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jul 2024 23:54:26 -0700 (PDT) From: Ole Schuerks To: linux-kbuild@vger.kernel.org Cc: ole0811sch@gmail.com, jude.gyimah@rub.de, thorsten.berger@rub.de, deltaone@debian.org, jan.sollmann@rub.de, mcgrof@kernel.org, masahiroy@kernel.org, linux-kernel@vger.kernel.org Subject: [PATCH v4 02/12] kconfig: Add picosat.c (1/3) Date: Wed, 10 Jul 2024 08:52:45 +0200 Message-Id: <20240710065255.10338-3-ole0811sch@gmail.com> X-Mailer: git-send-email 2.39.2 In-Reply-To: <20240710065255.10338-1-ole0811sch@gmail.com> References: <20240710065255.10338-1-ole0811sch@gmail.com> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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. Signed-off-by: Patrick Franz Signed-off-by: Ibrahim Fayaz Signed-off-by: Thorsten Berger Signed-off-by: Ole Schuerks --- 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..872a38b335c4 --- /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 co= py +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 DEALIN= GS +IN THE SOFTWARE. +**************************************************************************= **/ + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "picosat.h" + +/* By default code for 'all different constraints' is disabled, since 'NAD= C' + * 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 evol= ve. + * +#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) =3D 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) =3D 0; } while (0) + +#define RESIZEN(p,old_num,new_num) \ + do { \ + size_t old_size =3D sizeof (*(p)) * (old_num); \ + size_t new_size =3D sizeof (*(p)) * (new_num); \ + (p) =3D resize (ps, (p), old_size, new_size) ; \ + } while (0) + +#define ENLARGE(start,head,end) \ + do { \ + unsigned old_num =3D (ptrdiff_t)((end) - (start)); \ + size_t new_num =3D old_num ? (2 * old_num) : 1; \ + unsigned count =3D (head) - (start); \ + assert ((start) <=3D (end)); \ + RESIZEN((start),old_num,new_num); \ + (head) =3D (start) + count; \ + (end) =3D (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=3D=3DTRUE), ((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 =3D=3D ps->ohead) ? ps->lclauses : ps->oclauses) +#define EOC (ps->lhead) +#define NXC(p) (((p) + 1 =3D=3D 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 =3D (a); \ + (a) =3D (b); \ + (b) =3D tmp; \ + } \ + } while (0) + +#define UNPACKFLT(u,m,e) \ + do { \ + (m) =3D FLTMANTISSA(u); \ + (e) =3D FLTEXPONENT(u); \ + (m) |=3D FLTMSB; \ + } while (0) + +#define INSERTION_SORT_LIMIT 10 + +#define SORTING_SWAP(T,p,q) \ +do { \ + T tmp =3D *(q); \ + *(q) =3D *(p); \ + *(p) =3D 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 =3D (l) - 1; /* result in 'i' */ \ + j =3D (r); \ + pivot =3D (a)[j]; \ + for (;;) \ + { \ + while ((cmp) (ps, (a)[++i], pivot) < 0) \ + ; \ + while ((cmp) (ps, pivot, (a)[--j]) < 0) \ + if (j =3D=3D (l)) \ + break; \ + if (i >=3D 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 =3D 0, r =3D (n) - 1, m, ll, rr, i; \ + assert (ps->ihead =3D=3D ps->indices); \ + if (r - l <=3D INSERTION_SORT_LIMIT) \ + break; \ + for (;;) \ + { \ + m =3D (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 =3D i + 1; \ + rr =3D r; \ + r =3D i - 1; \ + } \ + else \ + { \ + ll =3D l; \ + rr =3D i - 1; \ + l =3D i + 1; \ + } \ + if (r - l > INSERTION_SORT_LIMIT) \ + { \ + assert (rr - ll > INSERTION_SORT_LIMIT); \ + if (ps->ihead =3D=3D ps->eoi) \ + ENLARGE (ps->indices, ps->ihead, ps->eoi); \ + *ps->ihead++ =3D ll; \ + if (ps->ihead =3D=3D ps->eoi) \ + ENLARGE (ps->indices, ps->ihead, ps->eoi); \ + *ps->ihead++ =3D rr; \ + } \ + else if (rr - ll > INSERTION_SORT_LIMIT) \ + { \ + l =3D ll; \ + r =3D rr; \ + } \ + else if (ps->ihead > ps->indices) \ + { \ + r =3D *--ps->ihead; \ + l =3D *--ps->ihead; \ + } \ + else \ + break; \ + } \ +} while (0) + +#define INSERTION_SORT(T,cmp,a,n) \ +do { \ + T pivot; \ + int l =3D 0, r =3D (n) - 1, i, j; \ + for (i =3D r; i > l; i--) \ + SORTING_CMP_SWAP (T, cmp, (a) + i - 1, (a) + i); \ + for (i =3D l + 2; i <=3D r; i++) \ + { \ + j =3D i; \ + pivot =3D (a)[i]; \ + while ((cmp) (ps, pivot, (a)[j - 1]) < 0) \ + { \ + (a)[j] =3D (a)[j - 1]; \ + j--; \ + } \ + (a)[j] =3D 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 =3D 0; i < (n) - 1; i++) \ + assert ((cmp) (ps, (a)[i], (a)[i + 1]) <=3D 0); \ +} while(0) +#endif + +#define SORT(T,cmp,a,n) \ +do { \ + T * aa =3D (a); \ + int nn =3D (n); \ + QUICKSORT (T, cmp, aa, nn); \ + INSERTION_SORT (T, cmp, aa, nn); \ + assert (ps->ihead =3D=3D 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 (=3Dzain) data */ +typedef unsigned char Znt; /* compressed antecedent data */ +#endif + +#ifdef NO_BINARY_CLAUSES +typedef struct Ltk Ltk; + +struct Ltk +{ + Lit ** start; + unsigned count : WRDSZ =3D=3D 32 ? 27 : 32; + unsigned ldsize : WRDSZ =3D=3D 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<=3D FLTCARRY) + { + if (e >=3D FLTMAXEXPONENT) + return INFFLT; + + e++; + m >>=3D 1; + } + } + + m &=3D ~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 >=3D eb); + delta =3D ea - eb; + if (delta < 32) mb >>=3D delta; else mb =3D 0; + if (!mb) + return a; + + ma +=3D mb; + if (ma & FLTCARRY) + { + if (ea =3D=3D FLTMAXEXPONENT) + return INFFLT; + + ea++; + ma >>=3D 1; + } + + assert (ma < FLTCARRY); + ma &=3D 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 +=3D eb; + ea +=3D 24; + if (ea > FLTMAXEXPONENT) + return INFFLT; + + if (ea < FLTMINEXPONENT) + return EPSFLT; + + accu =3D ma; + accu *=3D mb; + accu >>=3D 24; + + if (accu >=3D FLTCARRY) + { + if (ea =3D=3D FLTMAXEXPONENT) + return INFFLT; + + ea++; + accu >>=3D 1; + + if (accu >=3D FLTCARRY) + return INFFLT; + } + + assert (accu < FLTCARRY); + assert (accu & FLTMSB); + + ma =3D accu; + ma &=3D ~FLTMSB; + + return packflt (ma, ea); +} + +static Flt +ascii2flt (const char *str) +{ + Flt ten =3D base2flt (10, 0); + Flt onetenth =3D base2flt (26843546, -28); + Flt res =3D ZEROFLT, tmp, base; + const char *p =3D str; + int ch; + + ch =3D *p++; + + if (ch !=3D '.') + { + if (!isdigit (ch)) + return INFFLT; /* better abort ? */ + + res =3D base2flt (ch - '0', 0); + + while ((ch =3D *p++)) + { + if (ch =3D=3D '.') + break; + + if (!isdigit (ch)) + return INFFLT; /* better abort? */ + + res =3D mulflt (res, ten); + tmp =3D base2flt (ch - '0', 0); + res =3D addflt (res, tmp); + } + } + + if (ch =3D=3D '.') + { + ch =3D *p++; + if (!isdigit (ch)) + return INFFLT; /* better abort ? */ + + base =3D onetenth; + tmp =3D mulflt (base2flt (ch - '0', 0), base); + res =3D addflt (res, tmp); + + while ((ch =3D *p++)) + { + if (!isdigit (ch)) + return INFFLT; /* better abort? */ + + base =3D mulflt (base, onetenth); + tmp =3D mulflt (base2flt (ch - '0', 0), base); + res =3D 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 =3D m; + + if (e < 0) + { + for (i =3D e; i < 0; i++) + res *=3D 0.5; + } + else + { + for (i =3D 0; i < e; i++) + res *=3D 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 =3D size + SIZE_OF_BLK; + + if (ps->enew) + b =3D ps->enew (ps->emgr, bytes); + else + b =3D malloc (bytes); + + ABORTIF (!b, "out of memory in 'new'"); +#ifndef NDEBUG + b->header.size =3D size; +#endif + ps->current_bytes +=3D size; + if (ps->current_bytes > ps->max_bytes) + ps->max_bytes =3D 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 =3D PTR2BLK (void_ptr); + + assert (size <=3D ps->current_bytes); + ps->current_bytes -=3D size; + + assert (b->header.size =3D=3D size); + + bytes =3D 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 =3D PTR2BLK (void_ptr); + + assert (old_size <=3D ps->current_bytes); + ps->current_bytes -=3D old_size; + + if ((old_bytes =3D old_size)) + { + assert (old_size && b && b->header.size =3D=3D old_size); + old_bytes +=3D SIZE_OF_BLK; + } + else + assert (!b); + + if ((new_bytes =3D new_size)) + new_bytes +=3D SIZE_OF_BLK; + + if (ps->eresize) + b =3D ps->eresize (ps->emgr, b, old_bytes, new_bytes); + else + b =3D realloc (b, new_bytes); + + if (!new_size) + { + assert (!b); + return 0; + } + + ABORTIF (!b, "out of memory in 'resize'"); +#ifndef NDEBUG + b->header.size =3D new_size; +#endif + + ps->current_bytes +=3D new_size; + if (ps->current_bytes > ps->max_bytes) + ps->max_bytes =3D 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 =3D=3D end) + { + /* empty clause */ + } + else if (l + 1 =3D=3D end) + { + fprintf (ps->out, "%d ", LIT2INT (l[0])); + } + else + { + assert (l + 2 <=3D end); + first =3D (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1]))); + fprintf (ps->out, "%d ", LIT2INT (l[first])); + fprintf (ps->out, "%d ", LIT2INT (l[!first])); + for (p =3D 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 =3D 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 =3D SOC; p !=3D EOC; p =3D NXC (p)) + { + c =3D *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 =3D 0; +} + +static void +new_prefix (PS * ps, const char * str) +{ + delete_prefix (ps); + assert (str); + ps->prefix =3D 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 =3D 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 =3D pnew ? pnew (pmgr, sizeof *ps) : malloc (sizeof *ps); + ABORTIF (!ps, "failed to allocate memory for PicoSAT manager"); + memset (ps, 0, sizeof *ps); + + ps->emgr =3D pmgr; + ps->enew =3D pnew; + ps->eresize =3D presize; + ps->edelete =3D pdelete; + + ps->size_vars =3D 1; + ps->state =3D RESET; + ps->defaultphase =3D JWLPHASE; +#ifdef TRACE + ps->ocore =3D -1; +#endif + ps->lastrheader =3D -2; +#ifndef NADC + ps->adoconflictlimit =3D UINT_MAX; +#endif + ps->min_flipped =3D 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 =3D ps->heap + 1; + + ps->vinc =3D base2flt (1, 0); /* initial var activity */ + ps->ifvinc =3D ascii2flt ("1.05"); /* var score rescore factor */ +#ifdef VISCORES + ps->fvinc =3D ascii2flt ("0.9523809"); /* 1/f =3D 1/1.05 */ + ps->nvinc =3D ascii2flt ("0.0476191"); /* 1 - 1/f =3D 1 - 1/1.05 */ +#endif + ps->lscore =3D base2flt (1, 90); /* var activity rescore limit */ + ps->ilvinc =3D base2flt (1, -90); /* inverse of 'lscore' */ + + ps->cinc =3D base2flt (1, 0); /* initial clause activity */ + ps->fcinc =3D ascii2flt ("1.001"); /* cls activity rescore factor */ + ps->lcinc =3D base2flt (1, 90); /* cls activity rescore limit */ + ps->ilcinc =3D base2flt (1, -90); /* inverse of 'ilcinc' */ + + ps->lreduceadjustcnt =3D ps->lreduceadjustinc =3D 100; + ps->lpropagations =3D ~0ull; + +#ifndef RCODE + ps->out =3D stdout; +#else + ps->out =3D 0; +#endif + new_prefix (ps, "c "); + ps->verbosity =3D 0; + ps->plain =3D 0; + +#ifdef NO_BINARY_CLAUSES + memset (&ps->impl, 0, sizeof (ps->impl)); + ps->impl.size =3D 2; + + memset (&ps->cimpl, 0, sizeof (ps->impl)); + ps->cimpl.size =3D 2; +#endif + +#ifdef VISCORES + ps->fviscores =3D 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 xffff= ff" + "\n"); + + fprintf (ps->fviscores, + "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n"); +#endif +#endif + ps->defaultphase =3D JWLPHASE; + ps->state =3D READY; + ps->last_sat_call_result =3D 0; + + return ps; +} + +static size_t +bytes_clause (PS * ps, unsigned size, unsigned learned) +{ + size_t res; + + res =3D sizeof (Cls); + res +=3D size * sizeof (Lit *); + res -=3D 2 * sizeof (Lit *); + + if (learned && size > 2) + res +=3D sizeof (Act); /* add activity */ + +#ifdef TRACE + if (ps->trace) + res +=3D 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 =3D bytes_clause (ps, size, learned); + tmp =3D new (ps, bytes); + +#ifdef TRACE + if (ps->trace) + { + trd =3D tmp; + + if (learned) + trd->idx =3D LIDX2IDX (ps->lhead - ps->lclauses); + else + trd->idx =3D OIDX2IDX (ps->ohead - ps->oclauses); + + res =3D trd->cls; + } + else +#endif + res =3D tmp; + + res->size =3D size; + res->learned =3D learned; + + res->collect =3D 0; +#ifndef NDEBUG + res->connected =3D 0; +#endif + res->locked =3D 0; + res->used =3D 0; +#ifdef TRACE + res->core =3D 0; + res->collected =3D 0; +#endif + + if (learned && size > 2) + { + Act * p =3D CLS2ACT (res); + *p =3D ps->cinc; + } + + return res; +} + +static void +delete_clause (PS * ps, Cls * c) +{ + size_t bytes; +#ifdef TRACE + Trd *trd; +#endif + + bytes =3D bytes_clause (ps, c->size, c->learned); + +#ifdef TRACE + if (ps->trace) + { + trd =3D CLS2TRD (c); + delete (ps, trd, bytes); + } + else +#endif + delete (ps, c, bytes); +} + +static void +delete_clauses (PS * ps) +{ + Cls **p; + for (p =3D SOC; p !=3D EOC; p =3D NXC (p)) + if (*p) + delete_clause (ps, *p); + + DELETEN (ps->oclauses, ps->eoo - ps->oclauses); + DELETEN (ps->lclauses, ps->EOL - ps->lclauses); + + ps->ohead =3D ps->eoo =3D ps->lhead =3D ps->EOL =3D 0; +} + +#ifdef TRACE + +static void +delete_zhain (PS * ps, Zhn * zhain) +{ + const Znt *p, *znt; + + assert (zhain); + + znt =3D zhain->znt; + for (p =3D znt; *p; p++) + ; + + delete (ps, zhain, sizeof (Zhn) + (p - znt) + 1); +} + +static void +delete_zhains (PS * ps) +{ + Zhn **p, *z; + for (p =3D ps->zhains; p < ps->zhead; p++) + if ((z =3D *p)) + delete_zhain (ps, z); + + DELETEN (ps->zhains, ps->eoz - ps->zhains); + ps->eoz =3D ps->zhead =3D 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 =3D a; *p; p++) + ; + return p - a; +} + +static void +resetadoconflict (PS * ps) +{ + assert (ps->adoconflict); + delete_clause (ps, ps->adoconflict); + ps->adoconflict =3D 0; +} + +static void +reset_ados (PS * ps) +{ + Lit *** p; + + for (p =3D ps->ados; p < ps->hados; p++) + DELETEN (*p, llength (*p) + 1); + + DELETEN (ps->ados, ps->eados - ps->ados); + ps->hados =3D ps->eados =3D 0; + + DELETEN (ps->adotab, ps->szadotab); + ps->szadotab =3D ps->nadotab =3D 0; + + if (ps->adoconflict) + resetadoconflict (ps); + + ps->adoconflicts =3D 0; + ps->adoconflictlimit =3D UINT_MAX; + ps->adodisabled =3D 0; +} + +#endif + +static void +reset (PS * ps) +{ + ABORTIF (!ps || + ps->state =3D=3D RESET, "API usage: reset without initializatio= n"); + + delete_clauses (ps); +#ifdef TRACE + delete_zhains (ps); +#endif +#ifdef NO_BINARY_CLAUSES + { + unsigned i; + for (i =3D 2; i <=3D 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 <=3D ps->lits + 2* ps->max_var + 1); + if (ps->thead =3D=3D ps->eot) + { + unsigned ttail2count =3D ps->ttail2 - ps->trail; + unsigned ttailcount =3D ps->ttail - ps->trail; +#ifndef NADC + unsigned ttailadocount =3D ps->ttailado - ps->trail; +#endif + ENLARGE (ps->trail, ps->thead, ps->eot); + ps->ttail =3D ps->trail + ttailcount; + ps->ttail2 =3D ps->trail + ttail2count; +#ifndef NADC + ps->ttailado =3D ps->trail + ttailadocount; +#endif + } + + *ps->thead++ =3D lit; +} + +static void +assign_reason (PS * ps, Var * v, Cls * reason) +{ +#if defined(NO_BINARY_CLAUSES) && !defined(NDEBUG) + assert (reason !=3D &ps->impl); +#else + (void) ps; +#endif + v->reason =3D reason; +} + +static void +assign_phase (PS * ps, Lit * lit) +{ + unsigned new_phase, idx; + Var * v =3D 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 =3D (LIT2SGN (lit) > 0); + + if (v->assigned) + { + ps->sdflips -=3D ps->sdflips/FFLIPPED; + + if (new_phase !=3D v->phase) + { + assert (FFLIPPEDPREC >=3D FFLIPPED); + ps->sdflips +=3D FFLIPPEDPREC / FFLIPPED; + ps->flips++; + + idx =3D LIT2IDX (lit); + if (idx < ps->min_flipped) + ps->min_flipped =3D idx; + + NOLOG (fprintf (ps->out, + "%sflipped %d\n", + ps->prefix, LIT2INT (lit))); + } + } + + v->phase =3D new_phase; + v->assigned =3D 1; + } + + lit->val =3D TRUE; + NOTLIT (lit)->val =3D FALSE; +} + +inline static void +assign (PS * ps, Lit * lit, Cls * reason) +{ + Var * v =3D LIT2VAR (lit); + assert (lit->val =3D=3D UNDEF); +#ifdef STATS + ps->assignments++; +#endif + v->level =3D 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 =3D k->val, b =3D l->val; + Var *u, *v; + int res; + + if (a =3D=3D UNDEF && b !=3D UNDEF) + return -1; + + if (a !=3D UNDEF && b =3D=3D UNDEF) + return 1; + + u =3D LIT2VAR (k); + v =3D LIT2VAR (l); + + if (a !=3D UNDEF) + { + assert (b !=3D UNDEF); + res =3D v->level - u->level; + if (res) + return res; /* larger level first */ + } + + res =3D 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 =3D v[0], * b =3D v[1]; + + assert (a !=3D b); + + if (a < b) + return; + + v[0] =3D b; + v[1] =3D a; +} + +inline static void +sortlits (PS * ps, Lit ** v, unsigned size) +{ + if (size =3D=3D 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 =3D=3D 2); + + ps->impl.lits[0] =3D a; + ps->impl.lits[1] =3D b; + + sorttwolits (ps->impl.lits); + ps->implvalid =3D 1; + + return &ps->impl; +} + +static void +resetimpl (PS * ps) +{ + ps->implvalid =3D 0; +} + +static Cls * +setcimpl (PS * ps, Lit * a, Lit * b) +{ + assert (!ps->cimplvalid); + assert (ps->cimpl.size =3D=3D 2); + + ps->cimpl.lits[0] =3D a; + ps->cimpl.lits[1] =3D b; + + sorttwolits (ps->cimpl.lits); + ps->cimplvalid =3D 1; + + return &ps->cimpl; +} + +static void +resetcimpl (PS * ps) +{ + assert (ps->cimplvalid); + ps->cimplvalid =3D 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 =3D v->pos; + + assert (0 < vpos); + assert (vpos < ps->hhead - ps->heap); + assert (ps->heap[vpos] =3D=3D v); + + while (vpos > 1) + { + upos =3D vpos / 2; + + u =3D ps->heap[upos]; + + if (cmp_rnk (u, v) > 0) + break; + + ps->heap[vpos] =3D u; + u->pos =3D vpos; + + vpos =3D upos; + } + + ps->heap[vpos] =3D v; + v->pos =3D 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 =3D=3D &ps->impl) + return; +#elif defined(STATS) && defined(TRACE) + ps->antecedents++; +#endif + if (ps->rhead =3D=3D ps->eor) + ENLARGE (ps->resolved, ps->rhead, ps->eor); + + assert (ps->rhead < ps->eor); + *ps->rhead++ =3D 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 =3D=3D ps->eoa) + ENLARGE (ps->added, ps->ahead, ps->eoa); + + *ps->ahead++ =3D lit; +} + +static void +push_var_as_marked (PS * ps, Var * v) +{ + if (ps->mhead =3D=3D ps->eom) + ENLARGE (ps->marked, ps->mhead, ps->eom); + + *ps->mhead++ =3D v; +} + +static void +mark_var (PS * ps, Var * v) +{ + assert (!v->mark); + v->mark =3D 1; + push_var_as_marked (ps, v); +} + +#ifdef NO_BINARY_CLAUSES + +static Cls * +impl2reason (PS * ps, Lit * lit) +{ + Lit * other; + Cls * res; + other =3D ps->impl.lits[0]; + if (lit =3D=3D other) + other =3D ps->impl.lits[1]; + assert (other->val =3D=3D FALSE); + res =3D 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 =3D=3D ps->resolved); + assert (ps->ahead =3D=3D ps->added); + + add_lit (ps, lit); + add_antecedent (ps, reason); + count_resolved =3D 1; + v =3D LIT2VAR (lit); + + eol =3D end_of_lits (reason); + for (p =3D reason->lits; p < eol; p++) + { + other =3D *p; + u =3D LIT2VAR (other); + if (u =3D=3D 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 >=3D 2) + { +#ifdef NO_BINARY_CLAUSES + if (reason =3D=3D &ps->impl) + resetimpl (ps); +#endif + reason =3D add_simplified_clause (ps, 1); +#ifdef NO_BINARY_CLAUSES + if (reason->size =3D=3D 2) + { + assert (reason =3D=3D &ps->impl); + reason =3D impl2reason (ps, lit); + } +#endif + assign_reason (ps, v, reason); + } + else + { + ps->ahead =3D ps->added; + ps->rhead =3D ps->resolved; + } + + return reason; +} + +static void +fixvar (PS * ps, Var * v) +{ + Rnk * r; + + assert (VAR2LIT (v) !=3D UNDEF); + assert (!v->level); + + ps->fixed++; + + r =3D VAR2RNK (v); + r->score =3D 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 =3D 1; + ps->vused++; +} + +static void +assign_forced (PS * ps, Lit * lit, Cls * reason) +{ + Var *v; + + assert (reason); + assert (lit->val =3D=3D UNDEF); + +#ifdef STATS + ps->FORCED++; +#endif + assign (ps, lit, reason); + +#ifdef NO_BINARY_CLAUSES + assert (reason !=3D &ps->impl); + if (ISLITREASON (reason)) + { + reason =3D 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 =3D LIT2VAR (lit); + if (!ps->LEVEL) + use_var (ps, v); + + if (!ps->LEVEL && reason->size > 1) + { + reason =3D resolve_top_level_unit (ps, lit, reason); + assert (reason); + } + +#ifdef NO_BINARY_CLAUSES + if (ISLITREASON (reason) || reason =3D=3D &ps->impl) + { + /* DO NOTHING */ + } + else +#endif + { + assert (!reason->locked); + reason->locked =3D 1; + if (reason->learned && reason->size > 2) + ps->llocked++; + } + +#ifdef NO_BINARY_CLAUSES + if (reason =3D=3D &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 =3D (c->lits[0] =3D=3D lit); + Ltk * s =3D LIT2IMPLS (lit); + unsigned oldsize, newsize; + + assert (c->size =3D=3D 2); + + if (!s->start) + { + assert (!s->count); + assert (!s->ldsize); + NEWN (s->start, 1); + } + else + { + oldsize =3D (1 << (s->ldsize)); + assert (s->count <=3D oldsize); + if (s->count =3D=3D oldsize) + { + newsize =3D 2 * oldsize; + RESIZEN (s->start, oldsize, newsize); + s->ldsize++; + } + } + + s->start[s->count++] =3D c->lits[pos]; +} + +#endif + +static void +connect_head_tail (PS * ps, Lit * lit, Cls * c) +{ + Cls ** s; + assert (c->size >=3D 1); + if (c->size =3D=3D 2) + { +#ifdef NO_BINARY_CLAUSES + lpush (ps, lit, c); + return; +#else + s =3D LIT2IMPLS (lit); +#endif + } + else + s =3D LIT2HTPS (lit); + + if (c->lits[0] !=3D lit) + { + assert (c->size >=3D 2); + assert (c->lits[1] =3D=3D lit); + c->next[1] =3D *s; + } + else + c->next[0] =3D *s; + + *s =3D c; +} + +#ifdef TRACE +static void +zpush (PS * ps, Zhn * zhain) +{ + assert (ps->trace); + + if (ps->zhead =3D=3D ps->eoz) + ENLARGE (ps->zhains, ps->zhead, ps->eoz); + + *ps->zhead++ =3D 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 =3D=3D ps->eob) + ENLARGE (ps->buffer, ps->bhead, ps->eob); + + *ps->bhead++ =3D ch; +} + +static void +bpushu (PS * ps, unsigned u) +{ + while (u & ~0x7f) + { + bpushc (ps, u | 0x80); + u >>=3D 7; + } + + bpushc (ps, u); +} + +static void +bpushd (PS * ps, unsigned prev, unsigned this) +{ + unsigned delta; + assert (prev < this); + delta =3D 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 =3D=3D ps->buffer); + assert (ps->rhead > ps->resolved); + + rcount =3D ps->rhead - ps->resolved; + SORT (Cls *, cmp_resolved, ps->resolved, rcount); + + prev =3D 0; + for (p =3D ps->resolved; p < ps->rhead; p++) + { + c =3D *p; + this =3D CLS2TRD (c)->idx; + bpushd (ps, prev, this); + prev =3D this; + } + bpushc (ps, 0); + + count =3D ps->bhead - ps->buffer; + + res =3D new (ps, sizeof (Zhn) + count); + res->core =3D 0; + res->ref =3D 0; + memcpy (res->znt, ps->buffer, count); + + ps->bhead =3D ps->buffer; +#ifdef STATS + ps->znts +=3D 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 =3D ps->resolved; p < ps->rhead; p++) + { + c =3D *p; + if (c->used) + continue; + + c->used =3D 1; + + if (c->size <=3D 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 =3D ps->resolved; +} + +static void +incjwh (PS * ps, Cls * c) +{ + Lit **p, *lit, ** eol; + Flt * f, inc, sum; + unsigned size =3D 0; + Var * v; + Val val; + + eol =3D end_of_lits (c); + + for (p =3D c->lits; p < eol; p++) + { + lit =3D *p; + val =3D lit->val; + + if (val && ps->LEVEL > 0) + { + v =3D LIT2VAR (lit); + if (v->level > 0) + val =3D UNDEF; + } + + if (val =3D=3D TRUE) + return; + + if (val !=3D FALSE) + size++; + } + + inc =3D base2flt (1, -size); + + for (p =3D c->lits; p < eol; p++) + { + lit =3D *p; + f =3D LIT2JWH (lit); + sum =3D addflt (*f, inc); + *f =3D 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 =3D 255 - strlen (line); i >=3D 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 =3D 0; + +REENTER: + + size =3D ps->ahead - ps->added; + + add_resolved (ps, learned); + + if (learned) + { + ps->ladded++; + ps->llitsadded +=3D size; + if (size > 2) + { + ps->lladded++; + ps->nlclauses++; + ps->llits +=3D size; + } + } + else + { + ps->oadded++; + if (size > 2) + { + ps->loadded++; + ps->noclauses++; + ps->olits +=3D size; + } + } + + ps->addedclauses++; + assert (ps->addedclauses =3D=3D ps->ladded + ps->oadded); + +#ifdef NO_BINARY_CLAUSES + if (size =3D=3D 2) + res =3D setimpl (ps, ps->added[0], ps->added[1]); + else +#endif + { + sortlits (ps, ps->added, size); + + if (learned) + { + if (ps->lhead =3D=3D 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 =3D=3D EOC', which terminates all loops using the + * idiom 'for (p =3D SOC; p !=3D EOC; p =3D 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 =3D=3D ps->oclauses) + ENLARGE (ps->lclauses, ps->lhead, ps->EOL); + } + +#if !defined(NDEBUG) && defined(TRACE) + idx =3D LIDX2IDX (ps->lhead - ps->lclauses); +#endif + } + else + { + if (ps->ohead =3D=3D ps->eoo) + { + ENLARGE (ps->oclauses, ps->ohead, ps->eoo); + if (ps->EOL =3D=3D ps->oclauses) + ENLARGE (ps->oclauses, ps->ohead, ps->eoo); /* ditto */ + } + +#if !defined(NDEBUG) && defined(TRACE) + idx =3D OIDX2IDX (ps->ohead - ps->oclauses); +#endif + } + + assert (ps->EOL !=3D ps->oclauses); /* ditto */ + + res =3D new_clause (ps, size, learned); + + glue =3D 0; + + if (learned) + { + assert (ps->dusedhead =3D=3D ps->dused); + + for (p =3D ps->added; p < ps->ahead; p++) + { + lit =3D *p; + if (lit->val) + { + litlevel =3D LIT2VAR (lit)->level; + assert (litlevel <=3D ps->LEVEL); + while (ps->levels + litlevel >=3D ps->levelshead) + { + if (ps->levelshead >=3D ps->eolevels) + ENLARGE (ps->levels, ps->levelshead, ps->eolevels); + assert (ps->levelshead < ps->eolevels); + *ps->levelshead++ =3D 0; + } + if (!ps->levels[litlevel]) + { + if (ps->dusedhead >=3D ps->eodused) + ENLARGE (ps->dused, ps->dusedhead, ps->eodused); + assert (ps->dusedhead < ps->eodused); + *ps->dusedhead++ =3D litlevel; + ps->levels[litlevel] =3D 1; + glue++; + } + } + else + glue++; + } + + while (ps->dusedhead > ps->dused) + { + litlevel =3D *--ps->dusedhead; + assert (ps->levels + litlevel < ps->levelshead); + assert (ps->levels[litlevel]); + ps->levels[litlevel] =3D 0; + } + } + + assert (glue <=3D MAXGLUE); + res->glue =3D glue; + +#if !defined(NDEBUG) && defined(TRACE) + if (ps->trace) + assert (CLS2IDX (res) =3D=3D idx); +#endif + if (learned) + *ps->lhead++ =3D res; + else + *ps->ohead++ =3D res; + +#if !defined(NDEBUG) && defined(TRACE) + if (ps->trace && learned) + assert (ps->zhead - ps->zhains =3D=3D ps->lhead - ps->lclauses); +#endif + assert (ps->lhead !=3D ps->oclauses); /* ditto */ + } + + if (learned && ps->rup) + { + if (!ps->rupstarted) + { + write_rup_header (ps, ps->rup); + ps->rupstarted =3D 1; + } + } + + num_true =3D num_undef =3D num_false =3D 0; + + q =3D res->lits; + for (p =3D ps->added; p < ps->ahead; p++) + { + lit =3D *p; + *q++ =3D lit; + + if (learned && ps->rup) + fprintf (ps->rup, "%d ", LIT2INT (lit)); + + val =3D lit->val; + + num_true +=3D (val =3D=3D TRUE); + num_undef +=3D (val =3D=3D UNDEF); + num_false +=3D (val =3D=3D FALSE); + } + assert (num_false + num_true + num_undef =3D=3D size); + + if (learned && ps->rup) + fputs ("0\n", ps->rup); + + ps->ahead =3D ps->added; /* reset */ + + if (!reentered) // TODO merge + if (size > 0) + { + assert (size <=3D 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 =3D=3D 0) + { + if (!ps->mtcls) + ps->mtcls =3D res; + } + +#ifdef NO_BINARY_CLAUSES + if (size !=3D 2) +#endif +#ifndef NDEBUG + res->connected =3D 1; +#endif + + LOG ( fprintf (ps->out, "%s%s ", ps->prefix, learned ? "learned" : "orig= inal"); + dumpclsnl (ps, res)); + + /* Shrink clause by resolving it against top level assignments. + */ + if (!ps->LEVEL && num_false > 0) + { + assert (ps->ahead =3D=3D ps->added); + assert (ps->rhead =3D=3D ps->resolved); + + count_resolved =3D 1; + add_antecedent (ps, res); + + end =3D end_of_lits (res); + for (p =3D res->lits; p < end; p++) + { + lit =3D *p; + v =3D LIT2VAR (lit); + use_var (ps, v); + + if (lit->val =3D=3D FALSE) + { + add_antecedent (ps, v->reason); + count_resolved++; + } + else + add_lit (ps, lit); + } + + assert (count_resolved >=3D 2); + + learned =3D 1; +#ifdef NO_BINARY_CLAUSES + if (res =3D=3D &ps->impl) + resetimpl (ps); +#endif + reentered =3D 1; + goto REENTER; /* and return simplified clause */ + } + + if (!num_true && num_undef =3D=3D 1) /* unit clause */ + { + lit =3D 0; + for (p =3D res->lits; p < res->lits + size; p++) + { + if ((*p)->val =3D=3D UNDEF) + lit =3D *p; + + v =3D LIT2VAR (*p); + use_var (ps, v); + } + assert (lit); + + reason =3D res; +#ifdef NO_BINARY_CLAUSES + if (size =3D=3D 2) + { + Lit * other =3D res->lits[0]; + if (other =3D=3D lit) + other =3D res->lits[1]; + + assert (other->val =3D=3D FALSE); + reason =3D LIT2REASON (NOTLIT (other)); + } +#endif + assign_forced (ps, lit, reason); + num_true++; + } + + if (num_false =3D=3D size && !ps->conflict) + { +#ifdef NO_BINARY_CLAUSES + if (res =3D=3D &ps->impl) + ps->conflict =3D setcimpl (ps, res->lits[0], res->lits[1]); + else +#endif + ps->conflict =3D res; + } + + if (!learned && !num_true && num_undef) + incjwh (ps, res); + +#ifdef NO_BINARY_CLAUSES + if (res =3D=3D &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 =3D 0; + q =3D ps->added; + for (p =3D q; p < ps->ahead; p++) + { + Lit *this =3D *p; + + v =3D LIT2VAR (this); + + if (prev =3D=3D this) /* skip repeated literals */ + continue; + + /* Top level satisfied ? + */ + if (this->val =3D=3D TRUE && !v->level) + return 1; + + if (prev =3D=3D NOTLIT (this))/* found pair of dual literals */ + return 1; + + *q++ =3D prev =3D this; + } + + ps->ahead =3D 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 =3D ps->added; + + if (ps->ohead =3D=3D ps->eoo) + ENLARGE (ps->oclauses, ps->ohead, ps->eoo); + + *ps->ohead++ =3D 0; + + ps->addedclauses++; + ps->oadded++; + } + else + { + if (ps->CLS !=3D ps->clshead) + add_lit (ps, NOTLIT (ps->clshead[-1])); + +#ifdef NO_BINARY_CLAUSES + c =3D +#endif + add_simplified_clause (ps, 0); +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) assert (!ps->implvalid); +#endif + } +} + +#ifndef NADC + +static void +add_ado (PS * ps) +{ + unsigned len =3D 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]) !=3D len, + "internal: non matching all different constraint object lengths= "); + + if (ps->hados =3D=3D ps->eados) + ENLARGE (ps->ados, ps->hados, ps->eados); + + NEWN (ado, len + 1); + *ps->hados++ =3D ado; + + p =3D ps->added; + q =3D ado; + u =3D 0; + while (p < ps->ahead) + { + lit =3D *p++; + v =3D LIT2VAR (lit); + ABORTIF (v->inado, + "internal: variable in multiple all different objects"); + v->inado =3D ado; + if (!u && !lit->val) + u =3D v; + *q++ =3D lit; + } + + assert (q =3D=3D ado + len); + *q++ =3D 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 =3D=3D ado); + assert (!u->ado); + u->ado =3D ado; + + ps->ahead =3D 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] =3D=3D r); + + end =3D ps->hhead - ps->heap; + rpos =3D r->pos; + + for (;;) + { + cpos =3D 2 * rpos; + if (cpos >=3D end) + break; + + opos =3D cpos + 1; + child =3D ps->heap[cpos]; + + if (cmp_rnk (r, child) < 0) + { + if (opos < end) + { + other =3D ps->heap[opos]; + + if (cmp_rnk (child, other) < 0) + { + child =3D other; + cpos =3D opos; + } + } + } + else if (opos < end) + { + child =3D ps->heap[opos]; + + if (cmp_rnk (r, child) >=3D 0) + break; + + cpos =3D opos; + } + else + break; + + ps->heap[rpos] =3D child; + child->pos =3D rpos; + rpos =3D cpos; + } + + r->pos =3D rpos; + ps->heap[rpos] =3D 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 =3D ps->heap[1]; + res->pos =3D 0; + + end =3D --ps->hhead - ps->heap; + if (end =3D=3D 1) + return res; + + last =3D ps->heap[end]; + + ps->heap[last->pos =3D 1] =3D last; + hdown (ps, last); + + return res; +} + +inline static void +hpush (PS * ps, Rnk * r) +{ + assert (!r->pos); + + if (ps->hhead =3D=3D ps->eoh) + ENLARGE (ps->heap, ps->hhead, ps->eoh); + + r->pos =3D ps->hhead++ - ps->heap; + ps->heap[r->pos] =3D r; + hup (ps, r); +} + +static void +fix_trail_lits (PS * ps, long delta) +{ + Lit **p; + for (p =3D ps->trail; p < ps->thead; p++) + *p +=3D delta; +} + +#ifdef NO_BINARY_CLAUSES +static void +fix_impl_lits (PS * ps, long delta) +{ + Ltk * s; + Lit ** p; + + for (s =3D ps->impls + 2; s <=3D ps->impls + 2 * ps->max_var + 1; s++) + for (p =3D s->start; p < s->start + s->count; p++) + *p +=3D delta; +} +#endif + +static void +fix_clause_lits (PS * ps, long delta) +{ + Cls **p, *clause; + Lit **q, *lit, **eol; + + for (p =3D SOC; p !=3D EOC; p =3D NXC (p)) + { + clause =3D *p; + if (!clause) + continue; + + q =3D clause->lits; + eol =3D end_of_lits (clause); + while (q < eol) + { + assert (q - clause->lits <=3D (int) clause->size); + lit =3D *q; + lit +=3D delta; + *q++ =3D lit; + } + } +} + +static void +fix_added_lits (PS * ps, long delta) +{ + Lit **p; + for (p =3D ps->added; p < ps->ahead; p++) + *p +=3D delta; +} + +static void +fix_assumed_lits (PS * ps, long delta) +{ + Lit **p; + for (p =3D ps->als; p < ps->alshead; p++) + *p +=3D delta; +} + +static void +fix_cls_lits (PS * ps, long delta) +{ + Lit **p; + for (p =3D ps->CLS; p < ps->clshead; p++) + *p +=3D delta; +} + +static void +fix_heap_rnks (PS * ps, long delta) +{ + Rnk **p; + + for (p =3D ps->heap + 1; p < ps->hhead; p++) + *p +=3D delta; +} + +#ifndef NADC + +static void +fix_ado (long delta, Lit ** ado) +{ + Lit ** p; + for (p =3D ado; *p; p++) + *p +=3D delta; +} + +static void +fix_ados (PS * ps, long delta) +{ + Lit *** p; + + for (p =3D 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 =3D ps->lits; + Rnk *old_rnks =3D 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 =3D 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 =3D ps->rnks - old_rnks)) + { + fix_heap_rnks (ps, rnks_delta); + } + + assert (ps->mhead =3D=3D ps->marked); + + ps->size_vars =3D new_size_vars; +} + +static void +unassign (PS * ps, Lit * lit) +{ + Cls *reason; + Var *v; + Rnk *r; + + assert (lit->val =3D=3D TRUE); + + LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit))); + + v =3D LIT2VAR (lit); + reason =3D v->reason; + +#ifdef NO_BINARY_CLAUSES + assert (reason !=3D &ps->impl); + if (ISLITREASON (reason)) + { + /* DO NOTHING */ + } + else +#endif + if (reason) + { + assert (reason->locked); + reason->locked =3D 0; + if (reason->learned && reason->size > 2) + { + assert (ps->llocked > 0); + ps->llocked--; + } + } + + lit->val =3D UNDEF; + NOTLIT (lit)->val =3D UNDEF; + + r =3D VAR2RNK (v); + if (!r->pos) + hpush (ps, r); + +#ifndef NDSC + { + Cls * p, * next, ** q; + + q =3D LIT2DHTPS (lit); + p =3D *q; + *q =3D 0; + + while (p) + { + Lit * other =3D p->lits[0]; + + if (other =3D=3D lit) + { + other =3D p->lits[1]; + q =3D p->next + 1; --=20 2.39.2