From nobody Wed Dec 17 15:33:24 2025 Received: from mail-ed1-f43.google.com (mail-ed1-f43.google.com [209.85.208.43]) (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 A21C27D08D; Wed, 10 Jul 2024 06:54:31 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.208.43 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1720594475; cv=none; b=FaRZWBEVzCdLyJ+uhxba+Q+rqrJWqz8GMQzNKsPaRHOnrqKRIQpxxzV9pdoDdp4MIT8uOWB+6w7My1UtLfV8vOxAU9snI1Sz4TXNGVkEOK8lmXJ7z1vsqzP0+I7BGyW4CcD7DdseObvDpEKWSjEboQtxj6nYSWZpDen1GxOcbIg= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1720594475; c=relaxed/simple; bh=C0i0Id+Pod2d4JSyM+yBmlGJVPSKsses0II3ACP6tuA=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=ZwCXQjkhXdrBRKlkv1Vr5/hzLeojHimQKqexmz9uvmREs/W9S/gn4HCxJvv3UBrftwFif5TR6kMngIROIudNB8Gx6NdHxabjBr8KXxfBEOpb1HtSINfhPlOExBWgIu8ozKHDMhxzkLejBc2ySO+TD1QcenoXpjGCS+wzw61AL24= 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=nEtdoQ0Q; arc=none smtp.client-ip=209.85.208.43 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="nEtdoQ0Q" Received: by mail-ed1-f43.google.com with SMTP id 4fb4d7f45d1cf-58b447c519eso7443214a12.3; Tue, 09 Jul 2024 23:54:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1720594470; x=1721199270; 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=f/t6qURsGsAE8QpAoUge5Z6l4uQMEArrGYVpLcJiBCY=; b=nEtdoQ0QTMvxtwJFdvtBnLXm0I6TeM/x876HqAjXYE4tfl7uzHOkLVRMuVNXkO2qQ3 XCGS57BK8QmWvt40jy6p2JvWKfZmnhiySxtnC9GiIEj4cCvMPC7rI1W281Z+pR6+BsLs PSoSN8DaD1ngiWG4z7lOfUJHgjL/vTcfUtJ5GiVfi1q5YiMn/+fsEz29oG5LUAJWMMVq H4pRg5IDY9vtpALC9S/QxUpG6BYW4Sa3FxSLDlK21S4DkzkF/YMWR5+djWd1uUjrO2qQ fEcBVOC8ENzFpf0v7qeI5wQ1iBIbAU4uTAO4ke1OeqjRlojSDTi1WFxd+DDlxJ24AVA+ yLTw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1720594470; x=1721199270; 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=f/t6qURsGsAE8QpAoUge5Z6l4uQMEArrGYVpLcJiBCY=; b=ILFnQpqFi0oRiWtQd2ZzXKpLjrnthFCm4p0INncsyqDr4H2RMP2mckuQIacZozO3w8 gjG5wc/RxGD42OqqSyuJmnPlxgEHp0rm1wynlJNJl6KicR72KvZ5Yl2LhLoO1+CuVD0/ U3NOsyYo9f87qYYnXrT22BLQAN9xF+qEnbKiwaYdgtWjx3yRtw73B0puAz/8r1Q4LBRs HDtCtM0suOTgCksCt8Bo/uM1YQs5dexCGLMyiYwfaP+A54h8Jp/T9W66+4O5LJ6MxSLY 5umb0Zxq1s6sNizFLrRvdTsMkD4Oy3xcDV19WFUrmjjYQjY3wbR9VhwwsKvKY162U2v8 22uA== X-Forwarded-Encrypted: i=1; AJvYcCXPeTHbhadQ69DtFKhbU+J4wboHTC75LTOrPS1dJLkt/7F2WV6gXzPBP3FyTXyIV+yBWRPtSik8Sa/42slenFM+oBDm3eMxheQ8/C+9 X-Gm-Message-State: AOJu0YzO4UrmcOZTtmh9FjtkG5AIN6dwr98rMkMyCdkSQQbIQ+EUIAZb qDZCN60rl+UjCVRCcPLXSE14k1fTbCUSDNDvYDUDhj3ONtTMIbXoeXbw9A== X-Google-Smtp-Source: AGHT+IGdV9a/atlqycXz7zdtKMAE8S0Cdd3VVAVfbxYmjeAPCgiydWzLqWo0PIALDyMOi/sPE/xBhw== X-Received: by 2002:aa7:d897:0:b0:57d:10db:488e with SMTP id 4fb4d7f45d1cf-594bb86a798mr2558411a12.30.1720594469550; Tue, 09 Jul 2024 23:54:29 -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.28 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jul 2024 23:54:29 -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 03/12] kconfig: Add picosat.c (2/3) Date: Wed, 10 Jul 2024 08:52:46 +0200 Message-Id: <20240710065255.10338-4-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" The second part of picosat.c 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(+) diff --git a/scripts/kconfig/picosat.c b/scripts/kconfig/picosat.c index 872a38b335c4..c183dffb89a3 100644 --- a/scripts/kconfig/picosat.c +++ b/scripts/kconfig/picosat.c @@ -2998,3 +2998,3003 @@ unassign (PS * ps, Lit * lit) { other =3D p->lits[1]; q =3D p->next + 1; + } + else + { + assert (p->lits[1] =3D=3D lit); + q =3D p->next; + } + + next =3D *q; + *q =3D *LIT2HTPS (other); + *LIT2HTPS (other) =3D p; + p =3D next; + } + } +#endif + +#ifndef NADC + if (v->adotabpos) + { + assert (ps->nadotab); + assert (*v->adotabpos =3D=3D v->ado); + + *v->adotabpos =3D 0; + v->adotabpos =3D 0; + + ps->nadotab--; + } +#endif +} + +static Cls * +var2reason (PS * ps, Var * var) +{ + Cls * res =3D var->reason; +#ifdef NO_BINARY_CLAUSES + Lit * this, * other; + if (ISLITREASON (res)) + { + this =3D VAR2LIT (var); + if (this->val =3D=3D FALSE) + this =3D NOTLIT (this); + + other =3D REASON2LIT (res); + assert (other->val =3D=3D TRUE); + assert (this->val =3D=3D TRUE); + res =3D setimpl (ps, NOTLIT (other), this); + } +#else + (void) ps; +#endif + return res; +} + +static void +mark_clause_to_be_collected (Cls * c) +{ + assert (!c->collect); + c->collect =3D 1; +} + +static void +undo (PS * ps, unsigned new_level) +{ + Lit *lit; + Var *v; + + while (ps->thead > ps->trail) + { + lit =3D *--ps->thead; + v =3D LIT2VAR (lit); + if (v->level =3D=3D new_level) + { + ps->thead++; /* fix pre decrement */ + break; + } + + unassign (ps, lit); + } + + ps->LEVEL =3D new_level; + ps->ttail =3D ps->thead; + ps->ttail2 =3D ps->thead; +#ifndef NADC + ps->ttailado =3D ps->thead; +#endif + +#ifdef NO_BINARY_CLAUSES + if (ps->conflict =3D=3D &ps->cimpl) + resetcimpl (ps); +#endif +#ifndef NADC + if (ps->conflict && ps->conflict =3D=3D ps->adoconflict) + resetadoconflict (ps); +#endif + ps->conflict =3D ps->mtcls; + if (ps->LEVEL < ps->adecidelevel) + { + assert (ps->als < ps->alshead); + ps->adecidelevel =3D 0; + ps->alstail =3D ps->als; + } + LOG ( fprintf (ps->out, "%sback to level %u\n", ps->prefix, ps->LEVEL)); +} + +#ifndef NDEBUG + +static int +clause_satisfied (Cls * c) +{ + Lit **p, **eol, *lit; + + eol =3D end_of_lits (c); + for (p =3D c->lits; p < eol; p++) + { + lit =3D *p; + if (lit->val =3D=3D TRUE) + return 1; + } + + return 0; +} + +static void +original_clauses_satisfied (PS * ps) +{ + Cls **p, *c; + + for (p =3D ps->oclauses; p < ps->ohead; p++) + { + c =3D *p; + + if (!c) + continue; + + if (c->learned) + continue; + + assert (clause_satisfied (c)); + } +} + +static void +assumptions_satisfied (PS * ps) +{ + Lit *lit, ** p; + + for (p =3D ps->als; p < ps->alshead; p++) + { + lit =3D *p; + assert (lit->val =3D=3D TRUE); + } +} + +#endif + +static void +sflush (PS * ps) +{ + double now =3D picosat_time_stamp (); + double delta =3D now - ps->entered; + delta =3D (delta < 0) ? 0 : delta; + ps->seconds +=3D delta; + ps->entered =3D now; +} + +static double +mb (PS * ps) +{ + return ps->current_bytes / (double) (1 << 20); +} + +static double +avglevel (PS * ps) +{ + return ps->decisions ? ps->levelsum / ps->decisions : 0.0; +} + +static void +rheader (PS * ps) +{ + assert (ps->lastrheader <=3D ps->reports); + + if (ps->lastrheader =3D=3D ps->reports) + return; + + ps->lastrheader =3D ps->reports; + + fprintf (ps->out, "%s\n", ps->prefix); + fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]); + fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]); + fprintf (ps->out, "%s\n", ps->prefix); +} + +static unsigned +dynamic_flips_per_assignment_per_mille (PS * ps) +{ + assert (FFLIPPEDPREC >=3D 1000); + return ps->sdflips / (FFLIPPEDPREC / 1000); +} + +#ifdef NLUBY + +static int +high_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >=3D 200; +} + +static int +very_high_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >=3D 250; +} + +#else + +static int +medium_agility (PS * ps) +{ + return dynamic_flips_per_assignment_per_mille (ps) >=3D 230; +} + +#endif + +static void +relemdata (PS * ps) +{ + char *p; + int x; + + if (ps->reports < 0) + { + /* strip trailing white space + */ + for (x =3D 0; x <=3D 1; x++) + { + p =3D ps->rline[x] + strlen (ps->rline[x]); + while (p-- > ps->rline[x]) + { + if (*p !=3D ' ') + break; + + *p =3D 0; + } + } + + rheader (ps); + } + else + fputc ('\n', ps->out); + + ps->RCOUNT =3D 0; +} + +static void +relemhead (PS * ps, const char * name, int fp, double val) +{ + int x, y, len, size; + const char *fmt; + unsigned tmp, e; + + if (ps->reports < 0) + { + x =3D ps->RCOUNT & 1; + y =3D (ps->RCOUNT / 2) * 12 + x * 6; + + if (ps->RCOUNT =3D=3D 1) + sprintf (ps->rline[1], "%6s", ""); + + len =3D strlen (name); + while (ps->szrline <=3D len + y + 1) + { + size =3D ps->szrline ? 2 * ps->szrline : 128; + ps->rline[0] =3D resize (ps, ps->rline[0], ps->szrline, size); + ps->rline[1] =3D resize (ps, ps->rline[1], ps->szrline, size); + ps->szrline =3D size; + } + + fmt =3D (len <=3D 6) ? "%6s%10s" : "%-10s%4s"; + sprintf (ps->rline[x] + y, fmt, name, ""); + } + else if (val < 0) + { + assert (fp); + + if (val > -100 && (tmp =3D val * 10.0 - 0.5) > -1000.0) + { + fprintf (ps->out, "-%4.1f ", -tmp / 10.0); + } + else + { + tmp =3D -val / 10.0 + 0.5; + e =3D 1; + while (tmp >=3D 100) + { + tmp /=3D 10; + e++; + } + + fprintf (ps->out, "-%2ue%u ", tmp, e); + } + } + else + { + if (fp && val < 1000 && (tmp =3D val * 10.0 + 0.5) < 10000) + { + fprintf (ps->out, "%5.1f ", tmp / 10.0); + } + else if (!fp && (tmp =3D val) < 100000) + { + fprintf (ps->out, "%5u ", tmp); + } + else + { + tmp =3D val / 10.0 + 0.5; + e =3D 1; + + while (tmp >=3D 1000) + { + tmp /=3D 10; + e++; + } + + fprintf (ps->out, "%3ue%u ", tmp, e); + } + } + + ps->RCOUNT++; +} + +inline static void +relem (PS * ps, const char *name, int fp, double val) +{ + if (name) + relemhead (ps, name, fp, val); + else + relemdata (ps); +} + +static unsigned +reduce_limit_on_lclauses (PS * ps) +{ + unsigned res =3D ps->lreduce; + res +=3D ps->llocked; + return res; +} + +static void +report (PS * ps, int replevel, char type) +{ + int rounds; + +#ifdef RCODE + (void) type; +#endif + + if (ps->verbosity < replevel) + return; + + sflush (ps); + + if (!ps->reports) + ps->reports =3D -1; + + for (rounds =3D (ps->reports < 0) ? 2 : 1; rounds; rounds--) + { + if (ps->reports >=3D 0) + fprintf (ps->out, "%s%c ", ps->prefix, type); + + relem (ps, "seconds", 1, ps->seconds); + relem (ps, "level", 1, avglevel (ps)); + assert (ps->fixed <=3D ps->max_var); + relem (ps, "variables", 0, ps->max_var - ps->fixed); + relem (ps, "used", 1, PERCENT (ps->vused, ps->max_var)); + relem (ps, "original", 0, ps->noclauses); + relem (ps, "conflicts", 0, ps->conflicts); + // relem (ps, "decisions", 0, ps->decisions); + // relem (ps, "conf/dec", 1, PERCENT(ps->conflicts,ps->decisions)); + // relem (ps, "limit", 0, reduce_limit_on_lclauses (ps)); + relem (ps, "learned", 0, ps->nlclauses); + // relem (ps, "limit", 1, PERCENT (ps->nlclauses, reduce_limit_on_lc= lauses (ps))); + relem (ps, "limit", 0, ps->lreduce); +#ifdef STATS + relem (ps, "learning", 1, PERCENT (ps->llused, ps->lladded)); +#endif + relem (ps, "agility", 1, dynamic_flips_per_assignment_per_mille (ps)= / 10.0); + // relem (ps, "original", 0, ps->noclauses); + relem (ps, "MB", 1, mb (ps)); + // relem (ps, "lladded", 0, ps->lladded); + // relem (ps, "llused", 0, ps->llused); + + relem (ps, 0, 0, 0); + + ps->reports++; + } + + /* Adapt this to the number of rows in your terminal. + */ + #define ROWS 25 + + if (ps->reports % (ROWS - 3) =3D=3D (ROWS - 4)) + rheader (ps); + + fflush (ps->out); +} + +static int +bcp_queue_is_empty (PS * ps) +{ + if (ps->ttail !=3D ps->thead) + return 0; + + if (ps->ttail2 !=3D ps->thead) + return 0; + +#ifndef NADC + if (ps->ttailado !=3D ps->thead) + return 0; +#endif + + return 1; +} + +static int +satisfied (PS * ps) +{ + assert (!ps->mtcls); + assert (!ps->failed_assumption); + if (ps->alstail < ps->alshead) + return 0; + assert (!ps->conflict); + assert (bcp_queue_is_empty (ps)); + return ps->thead =3D=3D ps->trail + ps->max_var; /* all assigned */ +} + +static void +vrescore (PS * ps) +{ + Rnk *p, *eor =3D ps->rnks + ps->max_var; + for (p =3D ps->rnks + 1; p <=3D eor; p++) + if (p->score !=3D INFFLT) + p->score =3D mulflt (p->score, ps->ilvinc); + ps->vinc =3D mulflt (ps->vinc, ps->ilvinc);; +#ifdef VISCORES + ps->nvinc =3D mulflt (ps->nvinc, ps->lscore);; +#endif +} + +static void +inc_score (PS * ps, Var * v) +{ + Flt score; + Rnk *r; + +#ifndef NFL + if (ps->simplifying) + return; +#endif + + if (!v->level) + return; + + if (v->internal) + return; + + r =3D VAR2RNK (v); + score =3D r->score; + + assert (score !=3D INFFLT); + + score =3D addflt (score, ps->vinc); + assert (score < INFFLT); + r->score =3D score; + if (r->pos > 0) + hup (ps, r); + + if (score > ps->lscore) + vrescore (ps); +} + +static void +inc_activity (PS * ps, Cls * c) +{ + Act *p; + + if (!c->learned) + return; + + if (c->size <=3D 2) + return; + + p =3D CLS2ACT (c); + *p =3D addflt (*p, ps->cinc); +} + +static unsigned +hashlevel (unsigned l) +{ + return 1u << (l & 31); +} + +static void +push (PS * ps, Var * v) +{ + if (ps->dhead =3D=3D ps->eod) + ENLARGE (ps->dfs, ps->dhead, ps->eod); + + *ps->dhead++ =3D v; +} + +static Var * +pop (PS * ps) +{ + assert (ps->dfs < ps->dhead); + return *--ps->dhead; +} + +static void +analyze (PS * ps) +{ + unsigned open, minlevel, siglevels, l, old, i, orig; + Lit *this, *other, **p, **q, **eol; + Var *v, *u, **m, *start, *uip; + Cls *c; + + assert (ps->conflict); + + assert (ps->ahead =3D=3D ps->added); + assert (ps->mhead =3D=3D ps->marked); + assert (ps->rhead =3D=3D ps->resolved); + + /* First, search for First UIP variable and mark all resolved variables. + * At the same time determine the minimum decision level involved. + * Increase activities of resolved variables. + */ + q =3D ps->thead; + open =3D 0; + minlevel =3D ps->LEVEL; + siglevels =3D 0; + uip =3D 0; + + c =3D ps->conflict; + + for (;;) + { + add_antecedent (ps, c); + inc_activity (ps, c); + eol =3D end_of_lits (c); + for (p =3D c->lits; p < eol; p++) + { + other =3D *p; + + if (other->val =3D=3D TRUE) + continue; + + assert (other->val =3D=3D FALSE); + + u =3D LIT2VAR (other); + if (u->mark) + continue; + + u->mark =3D 1; + inc_score (ps, u); + use_var (ps, u); + + if (u->level =3D=3D ps->LEVEL) + { + open++; + } + else + { + push_var_as_marked (ps, u); + + if (u->level) + { + /* The statistics counter 'nonminimizedllits' sums up the + * number of literals that would be added if only the + * 'first UIP' scheme for learned clauses would be used + * and no clause minimization. + */ + ps->nonminimizedllits++; + + if (u->level < minlevel) + minlevel =3D u->level; + + siglevels |=3D hashlevel (u->level); + } + else + { + assert (!u->level); + assert (u->reason); + } + } + } + + do + { + if (q =3D=3D ps->trail) + { + uip =3D 0; + goto DONE_FIRST_UIP; + } + + this =3D *--q; + uip =3D LIT2VAR (this); + } + while (!uip->mark); + + uip->mark =3D 0; + + c =3D var2reason (ps, uip); +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + resetimpl (ps); +#endif + open--; + if ((!open && ps->LEVEL) || !c) + break; + + assert (c); + } + +DONE_FIRST_UIP: + + if (uip) + { + assert (ps->LEVEL); + this =3D VAR2LIT (uip); + this +=3D (this->val =3D=3D TRUE); + ps->nonminimizedllits++; + ps->minimizedllits++; + add_lit (ps, this); +#ifdef STATS + if (uip->reason) + ps->uips++; +#endif + } + else + assert (!ps->LEVEL); + + /* Second, try to mark more intermediate variables, with the goal to + * minimize the conflict clause. This is a DFS from already marked + * variables backward through the implication graph. It tries to reach + * other marked variables. If the search reaches an unmarked decision + * variable or a variable assigned below the minimum level of variables = in + * the first uip learned clause or a level on which no variable has been + * marked, then the variable from which the DFS is started is not + * redundant. Otherwise the start variable is redundant and will + * eventually be removed from the learned clause in step 4. We initially + * implemented BFS, but then profiling revelead that this step is a bott= le + * neck for certain incremental applications. After switching to DFS th= is + * hot spot went away. + */ + orig =3D ps->mhead - ps->marked; + for (i =3D 0; i < orig; i++) + { + start =3D ps->marked[i]; + + assert (start->mark); + assert (start !=3D uip); + assert (start->level < ps->LEVEL); + + if (!start->reason) + continue; + + old =3D ps->mhead - ps->marked; + assert (ps->dhead =3D=3D ps->dfs); + push (ps, start); + + while (ps->dhead > ps->dfs) + { + u =3D pop (ps); + assert (u->mark); + + c =3D var2reason (ps, u); +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + resetimpl (ps); +#endif + if (!c || + ((l =3D u->level) && + (l < minlevel || ((hashlevel (l) & ~siglevels))))) + { + while (ps->mhead > ps->marked + old) /* reset all marked */ + (*--ps->mhead)->mark =3D 0; + + ps->dhead =3D ps->dfs; /* and DFS stack */ + break; + } + + eol =3D end_of_lits (c); + for (p =3D c->lits; p < eol; p++) + { + v =3D LIT2VAR (*p); + if (v->mark) + continue; + + mark_var (ps, v); + push (ps, v); + } + } + } + + for (m =3D ps->marked; m < ps->mhead; m++) + { + v =3D *m; + + assert (v->mark); + assert (!v->resolved); + + use_var (ps, v); + + c =3D var2reason (ps, v); + if (!c) + continue; + +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + resetimpl (ps); +#endif + eol =3D end_of_lits (c); + for (p =3D c->lits; p < eol; p++) + { + other =3D *p; + + u =3D LIT2VAR (other); + if (!u->level) + continue; + + if (!u->mark) /* 'MARKTEST' */ + break; + } + + if (p !=3D eol) + continue; + + add_antecedent (ps, c); + v->resolved =3D 1; + } + + for (m =3D ps->marked; m < ps->mhead; m++) + { + v =3D *m; + + assert (v->mark); + v->mark =3D 0; + + if (v->resolved) + { + v->resolved =3D 0; + continue; + } + + this =3D VAR2LIT (v); + if (this->val =3D=3D TRUE) + this++; /* actually NOTLIT */ + + add_lit (ps, this); + ps->minimizedllits++; + } + + assert (ps->ahead <=3D ps->eoa); + assert (ps->rhead <=3D ps->eor); + + ps->mhead =3D ps->marked; +} + +static void +fanalyze (PS * ps) +{ + Lit ** eol, ** p, * lit; + Cls * c, * reason; + Var * v, * u; + int next; + +#ifndef RCODE + double start =3D picosat_time_stamp (); +#endif + + assert (ps->failed_assumption); + assert (ps->failed_assumption->val =3D=3D FALSE); + + v =3D LIT2VAR (ps->failed_assumption); + reason =3D var2reason (ps, v); + if (!reason) return; +#ifdef NO_BINARY_CLAUSES + if (reason =3D=3D &ps->impl) + resetimpl (ps); +#endif + + eol =3D end_of_lits (reason); + for (p =3D reason->lits; p !=3D eol; p++) + { + lit =3D *p; + u =3D LIT2VAR (lit); + if (u =3D=3D v) continue; + if (u->reason) break; + } + if (p =3D=3D eol) return; + + assert (ps->ahead =3D=3D ps->added); + assert (ps->mhead =3D=3D ps->marked); + assert (ps->rhead =3D=3D ps->resolved); + + next =3D 0; + mark_var (ps, v); + add_lit (ps, NOTLIT (ps->failed_assumption)); + + do + { + v =3D ps->marked[next++]; + use_var (ps, v); + if (v->reason) + { + reason =3D var2reason (ps, v); +#ifdef NO_BINARY_CLAUSES + if (reason =3D=3D &ps->impl) + resetimpl (ps); +#endif + add_antecedent (ps, reason); + eol =3D end_of_lits (reason); + for (p =3D reason->lits; p !=3D eol; p++) + { + lit =3D *p; + u =3D LIT2VAR (lit); + if (u =3D=3D v) continue; + if (u->mark) continue; + mark_var (ps, u); + } + } + else + { + lit =3D VAR2LIT (v); + if (lit->val =3D=3D TRUE) lit =3D NOTLIT (lit); + add_lit (ps, lit); + } + } + while (ps->marked + next < ps->mhead); + + c =3D add_simplified_clause (ps, 1); + v =3D LIT2VAR (ps->failed_assumption); + reason =3D v->reason; +#ifdef NO_BINARY_CLAUSES + if (!ISLITREASON (reason)) +#endif + { + assert (reason->locked); + reason->locked =3D 0; + if (reason->learned && reason->size > 2) + { + assert (ps->llocked > 0); + ps->llocked--; + } + } + +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + { + c =3D impl2reason (ps, NOTLIT (ps->failed_assumption)); + } + else +#endif + { + assert (c->learned); + assert (!c->locked); + c->locked =3D 1; + if (c->size > 2) + { + ps->llocked++; + assert (ps->llocked > 0); + } + } + + v->reason =3D c; + + while (ps->mhead > ps->marked) + (*--ps->mhead)->mark =3D 0; + + if (ps->verbosity) + fprintf (ps->out, "%sfanalyze took %.1f seconds\n", + ps->prefix, picosat_time_stamp () - start); +} + +/* Propagate assignment of 'this' to 'FALSE' by visiting all binary clause= s in + * which 'this' occurs. + */ +inline static void +prop2 (PS * ps, Lit * this) +{ +#ifdef NO_BINARY_CLAUSES + Lit ** l, ** start; + Ltk * lstk; +#else + Cls * c, ** p; + Cls * next; +#endif + Lit * other; + Val tmp; + + assert (this->val =3D=3D FALSE); + +#ifdef NO_BINARY_CLAUSES + lstk =3D LIT2IMPLS (this); + start =3D lstk->start; + l =3D start + lstk->count; + while (l !=3D start) + { + /* The counter 'visits' is the number of clauses that are + * visited during propagations of assignments. + */ + ps->visits++; +#ifdef STATS + ps->bvisits++; +#endif + other =3D *--l; + tmp =3D other->val; + + if (tmp =3D=3D TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertrue2++; + if (LIT2VAR (other)->level < ps->LEVEL) + ps->othertrue2u++; +#endif + continue; + } + + if (tmp !=3D FALSE) + { + assign_forced (ps, other, LIT2REASON (NOTLIT(this))); + continue; + } + + if (ps->conflict =3D=3D &ps->cimpl) + resetcimpl (ps); + ps->conflict =3D setcimpl (ps, this, other); + } +#else + /* Traverse all binary clauses with 'this'. Head/Tail pointers for bina= ry + * clauses do not have to be modified here. + */ + p =3D LIT2IMPLS (this); + for (c =3D *p; c; c =3D next) + { + ps->visits++; +#ifdef STATS + ps->bvisits++; +#endif + assert (!c->collect); +#ifdef TRACE + assert (!c->collected); +#endif + assert (c->size =3D=3D 2); + + other =3D c->lits[0]; + if (other =3D=3D this) + { + next =3D c->next[0]; + other =3D c->lits[1]; + } + else + next =3D c->next[1]; + + tmp =3D other->val; + + if (tmp =3D=3D TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertrue2++; + if (LIT2VAR (other)->level < ps->LEVEL) + ps->othertrue2u++; +#endif + continue; + } + + if (tmp =3D=3D FALSE) + ps->conflict =3D c; + else + assign_forced (ps, other, c); /* unit clause */ + } +#endif /* !defined(NO_BINARY_CLAUSES) */ +} + +#ifndef NDSC +static int +should_disconnect_head_tail (PS * ps, Lit * lit) +{ + unsigned litlevel; + Var * v; + + assert (lit->val =3D=3D TRUE); + + v =3D LIT2VAR (lit); + litlevel =3D v->level; + + if (!litlevel) + return 1; + +#ifndef NFL + if (ps->simplifying) + return 0; +#endif + + return litlevel < ps->LEVEL; +} +#endif + +inline static void +propl (PS * ps, Lit * this) +{ + Lit **l, *other, *prev, *new_lit, **eol; + Cls *next, **htp_ptr, **new_htp_ptr; + Cls *c; +#ifdef STATS + unsigned size; +#endif + + htp_ptr =3D LIT2HTPS (this); + assert (this->val =3D=3D FALSE); + + /* Traverse all non binary clauses with 'this'. Head/Tail pointers are + * updated as well. + */ + for (c =3D *htp_ptr; c; c =3D next) + { + ps->visits++; +#ifdef STATS + size =3D c->size; + assert (size >=3D 3); + ps->traversals++; /* other is dereferenced at least */ + + if (size =3D=3D 3) + ps->tvisits++; + else if (size >=3D 4) + { + ps->lvisits++; + ps->ltraversals++; + } +#endif +#ifdef TRACE + assert (!c->collected); +#endif + assert (c->size > 0); + + other =3D c->lits[0]; + if (other !=3D this) + { + assert (c->size !=3D 1); + c->lits[0] =3D this; + c->lits[1] =3D other; + next =3D c->next[1]; + c->next[1] =3D c->next[0]; + c->next[0] =3D next; + } + else if (c->size =3D=3D 1) /* With assumptions we need to + * traverse unit clauses as well. + */ + { + assert (!ps->conflict); + ps->conflict =3D c; + break; + } + else + { + assert (other =3D=3D this && c->size > 1); + other =3D c->lits[1]; + next =3D c->next[0]; + } + assert (other =3D=3D c->lits[1]); + assert (this =3D=3D c->lits[0]); + assert (next =3D=3D c->next[0]); + assert (!c->collect); + + if (other->val =3D=3D TRUE) + { +#ifdef STATS + ps->othertrue++; + ps->othertruel++; +#endif +#ifndef NDSC + if (should_disconnect_head_tail (ps, other)) + { + new_htp_ptr =3D LIT2DHTPS (other); + c->next[0] =3D *new_htp_ptr; + *new_htp_ptr =3D c; +#ifdef STATS + ps->othertruelu++; +#endif + *htp_ptr =3D next; + continue; + } +#endif + htp_ptr =3D c->next; + continue; + } + + l =3D c->lits + 1; + eol =3D (Lit**) c->lits + c->size; + prev =3D this; + + while (++l !=3D eol) + { +#ifdef STATS + if (size >=3D 3) + { + ps->traversals++; + if (size > 3) + ps->ltraversals++; + } +#endif + new_lit =3D *l; + *l =3D prev; + prev =3D new_lit; + if (new_lit->val !=3D FALSE) break; + } + + if (l =3D=3D eol) + { + while (l > c->lits + 2) + { + new_lit =3D *--l; + *l =3D prev; + prev =3D new_lit; + } + assert (c->lits[0] =3D=3D this); + + assert (other =3D=3D c->lits[1]); + if (other->val =3D=3D FALSE) /* found conflict */ + { + assert (!ps->conflict); + ps->conflict =3D c; + return; + } + + assign_forced (ps, other, c); /* unit clause */ + htp_ptr =3D c->next; + } + else + { + assert (new_lit->val =3D=3D TRUE || new_lit->val =3D=3D UNDEF); + c->lits[0] =3D new_lit; + // *l =3D this; + new_htp_ptr =3D LIT2HTPS (new_lit); + c->next[0] =3D *new_htp_ptr; + *new_htp_ptr =3D c; + *htp_ptr =3D next; + } + } +} + +#ifndef NADC + +static unsigned primes[] =3D { 996293, 330643, 753947, 500873 }; + +#define PRIMES ((sizeof primes)/sizeof *primes) + +static unsigned +hash_ado (PS * ps, Lit ** ado, unsigned salt) +{ + unsigned i, res, tmp; + Lit ** p, * lit; + + assert (salt < PRIMES); + + i =3D salt; + res =3D 0; + + for (p =3D ado; (lit =3D *p); p++) + { + assert (lit->val); + + tmp =3D res >> 31; + res <<=3D 1; + + if (lit->val > 0) + res |=3D 1; + + assert (i < PRIMES); + res *=3D primes[i++]; + if (i =3D=3D PRIMES) + i =3D 0; + + res +=3D tmp; + } + + return res & (ps->szadotab - 1); +} + +static unsigned +cmp_ado (Lit ** a, Lit ** b) +{ + Lit ** p, ** q, * l, * k; + int res; + + for (p =3D a, q =3D b; (l =3D *p); p++, q++) + { + k =3D *q; + assert (k); + if ((res =3D (l->val - k->val))) + return res; + } + + assert (!*q); + + return 0; +} + +static Lit *** +find_ado (PS * ps, Lit ** ado) +{ + Lit *** res, ** other; + unsigned pos, delta; + + pos =3D hash_ado (ps, ado, 0); + assert (pos < ps->szadotab); + res =3D ps->adotab + pos; + + other =3D *res; + if (!other || !cmp_ado (other, ado)) + return res; + + delta =3D hash_ado (ps, ado, 1); + if (!(delta & 1)) + delta++; + + assert (delta & 1); + assert (delta < ps->szadotab); + + for (;;) + { + pos +=3D delta; + if (pos >=3D ps->szadotab) + pos -=3D ps->szadotab; + + assert (pos < ps->szadotab); + res =3D ps->adotab + pos; + other =3D *res; + if (!other || !cmp_ado (other, ado)) + return res; + } +} + +static void +enlarge_adotab (PS * ps) +{ + /* TODO make this generic */ + + ABORTIF (ps->szadotab, + "internal: all different objects table needs larger initial siz= e"); + assert (!ps->nadotab); + ps->szadotab =3D 10000; + NEWN (ps->adotab, ps->szadotab); + CLRN (ps->adotab, ps->szadotab); +} + +static int +propado (PS * ps, Var * v) +{ + Lit ** p, ** q, *** adotabpos, **ado, * lit; + Var * u; + + if (ps->LEVEL && ps->adodisabled) + return 1; + + assert (!ps->conflict); + assert (!ps->adoconflict); + assert (VAR2LIT (v)->val !=3D UNDEF); + assert (!v->adotabpos); + + if (!v->ado) + return 1; + + assert (v->inado); + + for (p =3D v->ado; (lit =3D *p); p++) + if (lit->val =3D=3D UNDEF) + { + u =3D LIT2VAR (lit); + assert (!u->ado); + u->ado =3D v->ado; + v->ado =3D 0; + + return 1; + } + + if (4 * ps->nadotab >=3D 3 * ps->szadotab) /* at least 75% filled */ + enlarge_adotab (ps); + + adotabpos =3D find_ado (ps, v->ado); + ado =3D *adotabpos; + + if (!ado) + { + ps->nadotab++; + v->adotabpos =3D adotabpos; + *adotabpos =3D v->ado; + return 1; + } + + assert (ado !=3D v->ado); + + ps->adoconflict =3D new_clause (ps, 2 * llength (ado), 1); + q =3D ps->adoconflict->lits; + + for (p =3D ado; (lit =3D *p); p++) + *q++ =3D lit->val =3D=3D FALSE ? lit : NOTLIT (lit); + + for (p =3D v->ado; (lit =3D *p); p++) + *q++ =3D lit->val =3D=3D FALSE ? lit : NOTLIT (lit); + + assert (q =3D=3D ENDOFCLS (ps->adoconflict)); + ps->conflict =3D ps->adoconflict; + ps->adoconflicts++; + return 0; +} + +#endif + +static void +bcp (PS * ps) +{ + int props =3D 0; + assert (!ps->conflict); + + if (ps->mtcls) + return; + + for (;;) + { + if (ps->ttail2 < ps->thead) /* prioritize implications */ + { + props++; + prop2 (ps, NOTLIT (*ps->ttail2++)); + } + else if (ps->ttail < ps->thead) /* unit clauses or clauses with leng= th > 2 */ + { + if (ps->conflict) break; + propl (ps, NOTLIT (*ps->ttail++)); + if (ps->conflict) break; + } +#ifndef NADC + else if (ps->ttailado < ps->thead) + { + if (ps->conflict) break; + propado (ps, LIT2VAR (*ps->ttailado++)); + if (ps->conflict) break; + } +#endif + else + break; /* all assignments propagated, so break */ + } + + ps->propagations +=3D props; +} + +static unsigned +drive (PS * ps) +{ + unsigned res, vlevel; + Lit **p; + Var *v; + + res =3D 0; + for (p =3D ps->added; p < ps->ahead; p++) + { + v =3D LIT2VAR (*p); + vlevel =3D v->level; + assert (vlevel <=3D ps->LEVEL); + if (vlevel < ps->LEVEL && vlevel > res) + res =3D vlevel; + } + + return res; +} + +#ifdef VISCORES + +static void +viscores (PS * ps) +{ + Rnk *p, *eor =3D ps->rnks + ps->max_var; + char name[100], cmd[200]; + FILE * data; + Flt s; + int i; + + for (p =3D ps->rnks + 1; p <=3D ps->eor; p++) + { + s =3D p->score; + if (s =3D=3D INFFLT) + continue; + s =3D mulflt (s, ps->nvinc); + assert (flt2double (s) <=3D 1.0); + } + + sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts); + sprintf (cmd, "sort -n|nl>%s", name); + + data =3D popen (cmd, "w"); + for (p =3D ps->rnks + 1; p <=3D ps->eor; p++) + { + s =3D p->score; + if (s =3D=3D INFFLT) + continue; + s =3D mulflt (s, ps->nvinc); + fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnk= s)); + } + fflush (data); + pclose (data); + + for (i =3D 0; i < 8; i++) + { + sprintf (cmd, "awk '$3%%8=3D=3D%d' %s>%s.%d", i, name, name, i); + system (cmd); + } + + fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts); + fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max= _var); + + for (i =3D 0; i < 8; i++) + fprintf (ps->fviscores, + ", \"%s.%d\" using 1:2:3 with labels tc lt %d", + name, i, i + 1); + + fputc ('\n', ps->fviscores); + fflush (ps->fviscores); +#ifndef WRITEGIF + usleep (50000); /* refresh rate of 20 Hz */ +#endif +} + +#endif + +static void +crescore (PS * ps) +{ + Cls **p, *c; + Act *a; + Flt factor; + int l =3D log2flt (ps->cinc); + assert (l > 0); + factor =3D base2flt (1, -l); + + for (p =3D ps->lclauses; p !=3D ps->lhead; p++) + { + c =3D *p; + + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + assert (c->learned); + + if (c->size <=3D 2) + continue; + + a =3D CLS2ACT (c); + *a =3D mulflt (*a, factor); + } + + ps->cinc =3D mulflt (ps->cinc, factor); +} + +static void +inc_vinc (PS * ps) +{ +#ifdef VISCORES + ps->nvinc =3D mulflt (ps->nvinc, ps->fvinc); +#endif + ps->vinc =3D mulflt (ps->vinc, ps->ifvinc); +} + +inline static void +inc_max_var (PS * ps) +{ + Lit *lit; + Rnk *r; + Var *v; + + assert (ps->max_var < ps->size_vars); + + if (ps->max_var + 1 =3D=3D ps->size_vars) + enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */ + + ps->max_var++; /* new index of variable */ + assert (ps->max_var); /* no unsigned overflow */ + + assert (ps->max_var < ps->size_vars); + + lit =3D ps->lits + 2 * ps->max_var; + lit[0].val =3D lit[1].val =3D UNDEF; + + memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps); +#ifndef NDSC + memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps); +#endif + memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls); + memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh); + + v =3D ps->vars + ps->max_var; /* initialize variable components */ + CLR (v); + + r =3D ps->rnks + ps->max_var; /* initialize rank */ + CLR (r); + + hpush (ps, r); +} + +static void +force (PS * ps, Cls * c) +{ + Lit ** p, ** eol, * lit, * forced; + Cls * reason; + + forced =3D 0; + reason =3D c; + + eol =3D end_of_lits (c); + for (p =3D c->lits; p < eol; p++) + { + lit =3D *p; + if (lit->val =3D=3D UNDEF) + { + assert (!forced); + forced =3D lit; +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + reason =3D LIT2REASON (NOTLIT (p[p =3D=3D c->lits ? 1 : -1])); +#endif + } + else + assert (lit->val =3D=3D FALSE); + } + +#ifdef NO_BINARY_CLAUSES + if (c =3D=3D &ps->impl) + resetimpl (ps); +#endif + if (!forced) + return; + + assign_forced (ps, forced, reason); +} + +static void +inc_lreduce (PS * ps) +{ +#ifdef STATS + ps->inclreduces++; +#endif + ps->lreduce *=3D FREDUCE; + ps->lreduce /=3D 100; + report (ps, 1, '+'); +} + +static void +backtrack (PS * ps) +{ + unsigned new_level; + Cls * c; + + ps->conflicts++; + LOG ( fprintf (ps->out, "%sconflict ", ps->prefix); dumpclsnl (ps, ps->c= onflict)); + + analyze (ps); + new_level =3D drive (ps); + // TODO: why not? assert (new_level !=3D 1 || (ps->ahead - ps->added) = =3D=3D 2); + c =3D add_simplified_clause (ps, 1); + undo (ps, new_level); + force (ps, c); + + if ( +#ifndef NFL + !ps->simplifying && +#endif + !--ps->lreduceadjustcnt) + { + /* With FREDUCE=3D=3D110 and FREDADJ=3D121 we stir 'lreduce' to be + * proportional to 'sqrt(conflicts)'. In earlier version we actually + * used 'FREDADJ=3D150', which results in 'lreduce' to approximate + * 'conflicts^(log(1.1)/log(1.5))' which is close to the fourth root + * of 'conflicts', since log(1.1)/log(1.5)=3D0.235 (as observed by + * Donald Knuth). The square root is the same we get by a Glucose + * style increase, which simply adds a constant at every reduction. + * This would be way simpler to implement but for now we keep the mo= re + * complicated code using the adjust increments and counters. + */ + ps->lreduceadjustinc *=3D FREDADJ; ps->lreduceadjustinc /=3D 100; ps= ->lreduceadjustcnt + =3D ps->lreduceadjustinc; + inc_lreduce (ps); + } + + if (ps->verbosity >=3D 4 && !(ps->conflicts % 1000)) + report (ps, 4, 'C'); +} + +static void +inc_cinc (PS * ps) +{ + ps->cinc =3D mulflt (ps->cinc, ps->fcinc); + if (ps->lcinc < ps->cinc) + crescore (ps); +} + +static void +incincs (PS * ps) +{ + inc_vinc (ps); + inc_cinc (ps); +#ifdef VISCORES + viscores (ps); +#endif +} + +static void +disconnect_clause (PS * ps, Cls * c) +{ + assert (c->connected); + + if (c->size > 2) + { + if (c->learned) + { + assert (ps->nlclauses > 0); + ps->nlclauses--; + + assert (ps->llits >=3D c->size); + ps->llits -=3D c->size; + } + else + { + assert (ps->noclauses > 0); + ps->noclauses--; + + assert (ps->olits >=3D c->size); + ps->olits -=3D c->size; + } + } + +#ifndef NDEBUG + c->connected =3D 0; +#endif +} + +static int +clause_is_toplevel_satisfied (PS * ps, Cls * c) +{ + Lit *lit, **p, **eol =3D end_of_lits (c); + Var *v; + + for (p =3D c->lits; p < eol; p++) + { + lit =3D *p; + if (lit->val =3D=3D TRUE) + { + v =3D LIT2VAR (lit); + if (!v->level) + return 1; + } + } + + return 0; +} + +static int +collect_clause (PS * ps, Cls * c) +{ + assert (c->collect); + c->collect =3D 0; + +#ifdef TRACE + assert (!c->collected); + c->collected =3D 1; +#endif + disconnect_clause (ps, c); + +#ifdef TRACE + if (ps->trace && (!c->learned || c->used)) + return 0; +#endif + delete_clause (ps, c); + + return 1; +} + +static size_t +collect_clauses (PS * ps) +{ + Cls *c, **p, **q, * next; + Lit * lit, * eol; + size_t res; + int i; + + res =3D ps->current_bytes; + + eol =3D ps->lits + 2 * ps->max_var + 1; + for (lit =3D ps->lits + 2; lit <=3D eol; lit++) + { + for (i =3D 0; i <=3D 1; i++) + { + if (i) + { +#ifdef NO_BINARY_CLAUSES + Ltk * lstk =3D LIT2IMPLS (lit); + Lit ** r, ** s; + r =3D lstk->start; + if (lit->val !=3D TRUE || LIT2VAR (lit)->level) + for (s =3D r; s < lstk->start + lstk->count; s++) + { + Lit * other =3D *s; + Var *v =3D LIT2VAR (other); + if (v->level || + other->val !=3D TRUE) + *r++ =3D other; + } + lstk->count =3D r - lstk->start; + continue; +#else + p =3D LIT2IMPLS (lit); +#endif + } + else + p =3D LIT2HTPS (lit); + + for (c =3D *p; c; c =3D next) + { + q =3D c->next; + if (c->lits[0] !=3D lit) + q++; + + next =3D *q; + if (c->collect) + *p =3D next; + else + p =3D q; + } + } + } + +#ifndef NDSC + for (lit =3D ps->lits + 2; lit <=3D eol; lit++) + { + p =3D LIT2DHTPS (lit); + while ((c =3D *p)) + { + Lit * other =3D c->lits[0]; + if (other =3D=3D lit) + { + q =3D c->next + 1; + } + else + { + assert (c->lits[1] =3D=3D lit); + q =3D c->next; + } + + if (c->collect) + *p =3D *q; + else + p =3D q; + } + } +#endif + + for (p =3D SOC; p !=3D EOC; p =3D NXC (p)) + { + c =3D *p; + + if (!c) + continue; + + if (!c->collect) + continue; + + if (collect_clause (ps, c)) + *p =3D 0; + } + +#ifdef TRACE + if (!ps->trace) +#endif + { + q =3D ps->oclauses; + for (p =3D q; p < ps->ohead; p++) + if ((c =3D *p)) + *q++ =3D c; + ps->ohead =3D q; + + q =3D ps->lclauses; + for (p =3D q; p < ps->lhead; p++) + if ((c =3D *p)) + *q++ =3D c; + ps->lhead =3D q; + } + + assert (ps->current_bytes <=3D res); + res -=3D ps->current_bytes; + ps->recycled +=3D res; + + LOG ( fprintf (ps->out, "%scollected %ld bytes\n", ps->prefix, (long)res= )); + + return res; +} + +static int +need_to_reduce (PS * ps) +{ + return ps->nlclauses >=3D reduce_limit_on_lclauses (ps); +} + +#ifdef NLUBY + +static void +inc_drestart (PS * ps) +{ + ps->drestart *=3D FRESTART; + ps->drestart /=3D 100; + + if (ps->drestart >=3D MAXRESTART) + ps->drestart =3D MAXRESTART; +} + +static void +inc_ddrestart (PS * ps) +{ + ps->ddrestart *=3D FRESTART; + ps->ddrestart /=3D 100; + + if (ps->ddrestart >=3D MAXRESTART) + ps->ddrestart =3D MAXRESTART; +} + +#else + +static unsigned +luby (unsigned i) +{ + unsigned k; + for (k =3D 1; k < 32; k++) + if (i =3D=3D (1u << k) - 1) + return 1u << (k - 1); + + for (k =3D 1;; k++) + if ((1u << (k - 1)) <=3D i && i < (1u << k) - 1) + return luby (i - (1u << (k-1)) + 1); +} + +#endif + +#ifndef NLUBY +static void +inc_lrestart (PS * ps, int skip) +{ + unsigned delta; + + delta =3D 100 * luby (++ps->lubycnt); + ps->lrestart =3D ps->conflicts + delta; + + if (ps->waslubymaxdelta) + report (ps, 1, skip ? 'N' : 'R'); + else + report (ps, 2, skip ? 'n' : 'r'); + + if (delta > ps->lubymaxdelta) + { + ps->lubymaxdelta =3D delta; + ps->waslubymaxdelta =3D 1; + } + else + ps->waslubymaxdelta =3D 0; +} +#endif + +static void +init_restart (PS * ps) +{ +#ifdef NLUBY + /* TODO: why is it better in incremental usage to have smaller initial + * outer restart interval? + */ + ps->ddrestart =3D ps->calls > 1 ? MINRESTART : 1000; + ps->drestart =3D MINRESTART; + ps->lrestart =3D ps->conflicts + ps->drestart; +#else + ps->lubycnt =3D 0; + ps->lubymaxdelta =3D 0; + ps->waslubymaxdelta =3D 0; + inc_lrestart (ps, 0); +#endif +} + +static void +restart (PS * ps) +{ + int skip; +#ifdef NLUBY + char kind; + int outer; + + inc_drestart (ps); + outer =3D (ps->drestart >=3D ps->ddrestart); + + if (outer) + skip =3D very_high_agility (ps); + else + skip =3D high_agility (ps); +#else + skip =3D medium_agility (ps); +#endif + +#ifdef STATS + if (skip) + ps->skippedrestarts++; +#endif + + assert (ps->conflicts >=3D ps->lrestart); + + if (!skip) + { + ps->restarts++; + assert (ps->LEVEL > 1); + LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts)); + undo (ps, 0); + } + +#ifdef NLUBY + if (outer) + { + kind =3D skip ? 'N' : 'R'; + inc_ddrestart (ps); + ps->drestart =3D MINRESTART; + } + else if (skip) + { + kind =3D 'n'; + } + else + { + kind =3D 'r'; + } + + assert (ps->drestart <=3D MAXRESTART); + ps->lrestart =3D ps->conflicts + ps->drestart; + assert (ps->lrestart > ps->conflicts); + + report (outer ? 1 : 2, kind); +#else + inc_lrestart (ps, skip); +#endif +} + +inline static void +assign_decision (PS * ps, Lit * lit) +{ + assert (!ps->conflict); + + ps->LEVEL++; + + LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL)); + LOG ( fprintf (ps->out, + "%sassign %d at level %d <=3D DECISION\n", + ps->prefix, LIT2INT (lit), ps->LEVEL)); + + assign (ps, lit, 0); +} + +#ifndef NFL + +static int +lit_has_binary_clauses (PS * ps, Lit * lit) +{ +#ifdef NO_BINARY_CLAUSES + Ltk* lstk =3D LIT2IMPLS (lit); + return lstk->count !=3D 0; +#else + return *LIT2IMPLS (lit) !=3D 0; +#endif +} + +static void +flbcp (PS * ps) +{ +#ifdef STATS + unsigned long long propagaions_before_bcp =3D ps->propagations; +#endif + bcp (ps); +#ifdef STATS + ps->flprops +=3D ps->propagations - propagaions_before_bcp; +#endif +} + +inline static int +cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b) +{ + (void) ps; + return -cmp_rnk (a, b); +} + +inline static Flt +rnk2jwh (PS * ps, Rnk * r) +{ + Flt res, sum, pjwh, njwh; + Lit * plit, * nlit; + + plit =3D RNK2LIT (r); + nlit =3D plit + 1; + + pjwh =3D *LIT2JWH (plit); + njwh =3D *LIT2JWH (nlit); + + res =3D mulflt (pjwh, njwh); + + sum =3D addflt (pjwh, njwh); + sum =3D mulflt (sum, base2flt (1, -10)); + res =3D addflt (res, sum); + + return res; +} + +static int +cmp_inverse_jwh_rnk (PS * ps, Rnk * r, Rnk * s) +{ + Flt a =3D rnk2jwh (ps, r); + Flt b =3D rnk2jwh (ps, s); + int res =3D cmpflt (a, b); + + if (res) + return -res; + + return cmp_inverse_rnk (ps, r, s); +} + +static void +faillits (PS * ps) +{ + unsigned i, j, old_trail_count, common, saved_count; + unsigned new_saved_size, oldladded =3D ps->ladded; + unsigned long long limit, delta; + Lit * lit, * other, * pivot; + Rnk * r, ** p, ** q; + int new_trail_count; + double started; + + if (ps->plain) + return; + + if (ps->heap + 1 >=3D ps->hhead) + return; + + if (ps->propagations < ps->fllimit) + return; + + sflush (ps); + started =3D ps->seconds; + + ps->flcalls++; +#ifdef STATSA + ps->flrounds++; +#endif + delta =3D ps->propagations/10; + if (delta >=3D 100*1000*1000) delta =3D 100*1000*1000; + else if (delta <=3D 100*1000) delta =3D 100*1000; + + limit =3D ps->propagations + delta; + ps->fllimit =3D ps->propagations; + + assert (!ps->LEVEL); + assert (ps->simplifying); + + if (ps->flcalls <=3D 1) + SORT (Rnk *, cmp_inverse_jwh_rnk, ps->heap + 1, ps->hhead - (ps->heap = + 1)); + else + SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1)= ); + + i =3D 1; /* NOTE: heap starts at position '1' */ + + while (ps->propagations < limit) + { + if (ps->heap + i =3D=3D ps->hhead) + { + if (ps->ladded =3D=3D oldladded) + break; + + i =3D 1; +#ifdef STATS + ps->flrounds++; +#endif + oldladded =3D ps->ladded; + } + + assert (ps->heap + i < ps->hhead); + + r =3D ps->heap[i++]; + lit =3D RNK2LIT (r); + + if (lit->val) + continue; + + if (!lit_has_binary_clauses (ps, NOTLIT (lit))) + { +#ifdef STATS + ps->flskipped++; +#endif + continue; + } + +#ifdef STATS + ps->fltried++; +#endif + LOG ( fprintf (ps->out, "%strying %d as failed literal\n", + ps->prefix, LIT2INT (lit))); + + assign_decision (ps, lit); + old_trail_count =3D ps->thead - ps->trail; + flbcp (ps); + + if (ps->conflict) + { +EXPLICITLY_FAILED_LITERAL: + LOG ( fprintf (ps->out, "%sfound explicitly failed literal %d\n", + ps->prefix, LIT2INT (lit))); + + ps->failedlits++; + ps->efailedlits++; + + backtrack (ps); + flbcp (ps); + + if (!ps->conflict) + continue; + +CONTRADICTION: + assert (!ps->LEVEL); + backtrack (ps); + assert (ps->mtcls); + + goto RETURN; + } + + if (ps->propagations >=3D limit) + { + undo (ps, 0); + break; + } + + lit =3D NOTLIT (lit); + + if (!lit_has_binary_clauses (ps, NOTLIT (lit))) + { +#ifdef STATS + ps->flskipped++; +#endif + undo (ps, 0); + continue; + } + +#ifdef STATS + ps->fltried++; +#endif + LOG ( fprintf (ps->out, "%strying %d as failed literals\n", + ps->prefix, LIT2INT (lit))); + + new_trail_count =3D ps->thead - ps->trail; + saved_count =3D new_trail_count - old_trail_count; + + if (saved_count > ps->saved_size) + { + new_saved_size =3D ps->saved_size ? 2 * ps->saved_size : 1; + while (saved_count > new_saved_size) + new_saved_size *=3D 2; + + RESIZEN (ps->saved, ps->saved_size, new_saved_size); + ps->saved_size =3D new_saved_size; + } + + for (j =3D 0; j < saved_count; j++) + ps->saved[j] =3D ps->trail[old_trail_count + j]; + + undo (ps, 0); + + assign_decision (ps, lit); + flbcp (ps); + + if (ps->conflict) + goto EXPLICITLY_FAILED_LITERAL; + + pivot =3D (ps->thead - ps->trail <=3D new_trail_count) ? lit : NOTLI= T (lit); + + common =3D 0; + for (j =3D 0; j < saved_count; j++) + if ((other =3D ps->saved[j])->val =3D=3D TRUE) + ps->saved[common++] =3D other; + + undo (ps, 0); + + LOG (if (common) + fprintf (ps->out, + "%sfound %d literals implied by %d and %d\n", + ps->prefix, common, + LIT2INT (NOTLIT (lit)), LIT2INT (lit))); + +#if 1 // set to zero to disable 'lifting' + for (j =3D 0; + j < common + /* TODO: For some Velev benchmarks, extracting the common implicit + * failed literals took quite some time. This needs to be fixed by + * a dedicated analyzer. Up to then we bound the number of + * propagations in this loop as well. + */ + && ps->propagations < limit + delta + ; j++) + { + other =3D ps->saved[j]; + + if (other->val =3D=3D TRUE) + continue; + + assert (!other->val); + + LOG ( fprintf (ps->out, + "%sforcing %d as forced implicitly failed literal\n", + ps->prefix, LIT2INT (other))); + + assert (pivot !=3D NOTLIT (other)); + assert (pivot !=3D other); + + assign_decision (ps, NOTLIT (other)); + flbcp (ps); + + assert (ps->LEVEL =3D=3D 1); + + if (ps->conflict) + { + backtrack (ps); + assert (!ps->LEVEL); + } + else + { + assign_decision (ps, pivot); + flbcp (ps); + + backtrack (ps); + + if (ps->LEVEL) + { + assert (ps->LEVEL =3D=3D 1); + + flbcp (ps); + + if (ps->conflict) + { + backtrack (ps); + assert (!ps->LEVEL); + } + else + { + assign_decision (ps, NOTLIT (pivot)); + flbcp (ps); + backtrack (ps); + + if (ps->LEVEL) + { + assert (ps->LEVEL =3D=3D 1); + flbcp (ps); + + if (!ps->conflict) + { +#ifdef STATS + ps->floopsed++; +#endif + undo (ps, 0); + continue; + } + + backtrack (ps); + } + + assert (!ps->LEVEL); + } + + assert (!ps->LEVEL); + } + } + assert (!ps->LEVEL); + flbcp (ps); + + ps->failedlits++; + ps->ifailedlits++; + + if (ps->conflict) + goto CONTRADICTION; + } +#endif + } + + ps->fllimit +=3D 9 * (ps->propagations - ps->fllimit); /* 10% for failed= literals */ + +RETURN: + + /* First flush top level assigned literals. Those are prohibited from + * being pushed up the heap during 'faillits' since 'simplifying' is set. + */ + assert (ps->heap < ps->hhead); + for (p =3D q =3D ps->heap + 1; p < ps->hhead; p++) + { + r =3D *p; + lit =3D RNK2LIT (r); + if (lit->val) + r->pos =3D 0; + else + *q++ =3D r; + } + + /* Then resort with respect to EVSIDS score and fix positions. + */ + SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1)); + for (p =3D ps->heap + 1; p < ps->hhead; p++) + (*p)->pos =3D p - ps->heap; + + sflush (ps); + ps->flseconds +=3D ps->seconds - started; +} + +#endif + +static void +simplify (PS * ps, int forced) +{ + Lit * lit, * notlit, ** t; + unsigned collect, delta; +#ifdef STATS + size_t bytes_collected; +#endif + int * q, ilit; + Cls **p, *c; + Var * v; + +#ifndef NDEDBUG + (void) forced; +#endif + + assert (!ps->mtcls); + assert (!satisfied (ps)); + assert (forced || ps->lsimplify <=3D ps->propagations); + assert (forced || ps->fsimplify <=3D ps->fixed); + + if (ps->LEVEL) + undo (ps, 0); +#ifndef NFL + ps->simplifying =3D 1; + faillits (ps); + ps->simplifying =3D 0; + + if (ps->mtcls) + return; +#endif + + if (ps->cils !=3D ps->cilshead) + { + assert (ps->ttail =3D=3D ps->thead); + assert (ps->ttail2 =3D=3D ps->thead); + ps->ttail =3D ps->trail; + for (t =3D ps->trail; t < ps->thead; t++) + { + lit =3D *t; + v =3D LIT2VAR (lit); + if (v->internal) + { + assert (LIT2INT (lit) < 0); + assert (lit->val =3D=3D TRUE); + unassign (ps, lit); + } + else + *ps->ttail++ =3D lit; + } + ps->ttail2 =3D ps->thead =3D ps->ttail; + + for (q =3D ps->cils; q !=3D ps->cilshead; q++) + { + ilit =3D *q; + assert (0 < ilit && ilit <=3D (int) ps->max_var); + v =3D ps->vars + ilit; + assert (v->internal); + v->level =3D 0; + v->reason =3D 0; + lit =3D int2lit (ps, -ilit); + assert (lit->val =3D=3D UNDEF); + lit->val =3D TRUE; + notlit =3D NOTLIT (lit); + assert (notlit->val =3D=3D UNDEF); + notlit->val =3D FALSE; + } + } + + collect =3D 0; + for (p =3D SOC; p !=3D EOC; p =3D NXC (p)) + { + c =3D *p; + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + + if (c->locked) + continue; + + assert (!c->collect); + if (clause_is_toplevel_satisfied (ps, c)) + { + mark_clause_to_be_collected (c); + collect++; + } + } + + LOG ( fprintf (ps->out, "%scollecting %d clauses\n", ps->prefix, collect= )); +#ifdef STATS + bytes_collected =3D +#endif + collect_clauses (ps); +#ifdef STATS + ps->srecycled +=3D bytes_collected; +#endif + + if (ps->cils !=3D ps->cilshead) + { + for (q =3D ps->cils; q !=3D ps->cilshead; q++) + { + ilit =3D *q; + assert (0 < ilit && ilit <=3D (int) ps->max_var); + assert (ps->vars[ilit].internal); + if (ps->rilshead =3D=3D ps->eorils) + ENLARGE (ps->rils, ps->rilshead, ps->eorils); + *ps->rilshead++ =3D ilit; + lit =3D int2lit (ps, -ilit); + assert (lit->val =3D=3D TRUE); + lit->val =3D UNDEF; + notlit =3D NOTLIT (lit); + assert (notlit->val =3D=3D FALSE); + notlit->val =3D UNDEF; + } + ps->cilshead =3D ps->cils; + } + + delta =3D 10 * (ps->olits + ps->llits) + 100000; + if (delta > 2000000) + delta =3D 2000000; + ps->lsimplify =3D ps->propagations + delta; + ps->fsimplify =3D ps->fixed; + ps->simps++; + + report (ps, 1, 's'); +} + +static void +iteration (PS * ps) +{ + assert (!ps->LEVEL); + assert (bcp_queue_is_empty (ps)); + assert (ps->isimplify < ps->fixed); + + ps->iterations++; + report (ps, 2, 'i'); +#ifdef NLUBY + ps->drestart =3D MINRESTART; + ps->lrestart =3D ps->conflicts + ps->drestart; +#else + init_restart (ps); +#endif + ps->isimplify =3D ps->fixed; +} + +static int +cmp_glue_activity_size (PS * ps, Cls * c, Cls * d) +{ + Act a, b, * p, * q; + + (void) ps; + + assert (c->learned); + assert (d->learned); + + if (c->glue < d->glue) // smaller glue preferred + return 1; + + if (c->glue > d->glue) + return -1; + + p =3D CLS2ACT (c); + q =3D CLS2ACT (d); + a =3D *p; + b =3D *q; + + if (a < b) // then higher activity + return -1; + + if (b < a) + return 1; + + if (c->size < d->size) // then smaller size + return 1; + + if (c->size > d->size) + return -1; + + return 0; +} + +static void +reduce (PS * ps, unsigned percentage) +{ + unsigned redcount, lcollect, collect, target; +#ifdef STATS + size_t bytes_collected; +#endif + Cls **p, *c; + + assert (ps->rhead =3D=3D ps->resolved); + + ps->lastreduceconflicts =3D ps->conflicts; + + assert (percentage <=3D 100); + LOG ( fprintf (ps->out, + "%sreducing %u%% learned clauses\n", + ps->prefix, percentage)); + + while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved)) + ENLARGE (ps->resolved, ps->rhead, ps->eor); + + collect =3D 0; + lcollect =3D 0; + + for (p =3D ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p !=3D EO= C; p =3D NXC (p)) + { + c =3D *p; + if (!c) + continue; + +#ifdef TRACE + if (c->collected) + continue; +#endif + + if (c->locked) + continue; + + assert (!c->collect); + if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c= )) + { + mark_clause_to_be_collected (c); + collect++; + + if (c->learned && c->size > 2) + lcollect++; + + continue; + } + + if (!c->learned) + continue; + + if (c->size <=3D 2) + continue; + + assert (ps->rhead < ps->eor); + *ps->rhead++ =3D c; + } + assert (ps->rhead <=3D ps->eor); + + ps->fsimplify =3D ps->fixed; + + redcount =3D ps->rhead - ps->resolved; + SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount); + + assert (ps->nlclauses >=3D lcollect); + target =3D ps->nlclauses - lcollect + 1; + + target =3D (percentage * target + 99) / 100; + + if (target >=3D redcount) + target =3D redcount; + + ps->rhead =3D ps->resolved + target; + while (ps->rhead > ps->resolved) + { + c =3D *--ps->rhead; + mark_clause_to_be_collected (c); + + collect++; + if (c->learned && c->size > 2) /* just for consistency */ + lcollect++; + } + + if (collect) + { + ps->reductions++; +#ifdef STATS + bytes_collected =3D +#endif + collect_clauses (ps); +#ifdef STATS + ps->rrecycled +=3D bytes_collected; +#endif + report (ps, 2, '-'); + } + + if (!lcollect) + inc_lreduce (ps); /* avoid dead lock */ + + assert (ps->rhead =3D=3D ps->resolved); +} + +static void +init_reduce (PS * ps) +{ + // lreduce =3D loadded / 2; + ps->lreduce =3D 1000; + + if (ps->lreduce < 100) + ps->lreduce =3D 100; + + if (ps->verbosity) + fprintf (ps->out, + "%s\n%sinitial reduction limit %u clauses\n%s\n", + ps->prefix, ps->prefix, ps->lreduce, ps->prefix); +} + +static unsigned +rng (PS * ps) +{ + unsigned res =3D ps->srng; + ps->srng *=3D 1664525u; + ps->srng +=3D 1013904223u; + NOLOG ( fprintf (ps->out, "%srng () =3D %u\n", ps->prefix, res)); + return res; +} + +static unsigned +rrng (PS * ps, unsigned low, unsigned high) +{ + unsigned long long tmp; + unsigned res, elements; + assert (low <=3D high); + elements =3D high - low + 1; + tmp =3D rng (ps); + tmp *=3D elements; + tmp >>=3D 32; + tmp +=3D low; + res =3D tmp; + NOLOG ( fprintf (ps->out, "%srrng (ps, %u, %u) =3D %u\n", ps->prefix, lo= w, high, res)); + assert (low <=3D res); + assert (res <=3D high); + return res; +} + +static Lit * +decide_phase (PS * ps, Lit * lit) +{ + Lit * not_lit =3D NOTLIT (lit); + Var *v =3D LIT2VAR (lit); + + assert (LIT2SGN (lit) > 0); + if (v->usedefphase) + { + if (v->defphase) + { + /* assign to TRUE */ + } + else + { + /* assign to FALSE */ + lit =3D not_lit; + } + } + else if (!v->assigned) + { +#ifdef STATS + ps->staticphasedecisions++; +#endif + if (ps->defaultphase =3D=3D POSPHASE) + { + /* assign to TRUE */ + } + else if (ps->defaultphase =3D=3D NEGPHASE) + { + /* assign to FALSE */ + lit =3D not_lit; + } + else if (ps->defaultphase =3D=3D RNDPHASE) + { + /* randomly assign default phase */ + if (rrng (ps, 1, 2) !=3D 2) + lit =3D not_lit; + } + else if (*LIT2JWH(lit) <=3D *LIT2JWH (not_lit)) + { + /* assign to FALSE (Jeroslow-Wang says there are more short + * clauses with negative occurence of this variable, so satisfy + * those, to minimize BCP) + */ + lit =3D not_lit; + } + else + { + /* assign to TRUE (... but strictly more positive occurrences) */ + } + } + else + { + /* repeat last phase: phase saving heuristic */ + + if (v->phase) + { + /* assign to TRUE (last phase was TRUE as well) */ + } + else + { + /* assign to FALSE (last phase was FALSE as well) */ + lit =3D not_lit; + } + } + + return lit; +} + +static unsigned +gcd (unsigned a, unsigned b) +{ + unsigned tmp; + + assert (a); + assert (b); + + if (a < b) + { + tmp =3D a; + a =3D b; + b =3D tmp; + } + + while (b) + { + assert (a >=3D b); + tmp =3D b; + b =3D a % b; + a =3D tmp; + } + + return a; +} + +static Lit * +rdecide (PS * ps) +{ + unsigned idx, delta, spread; + Lit * res; + + spread =3D RDECIDE; + if (rrng (ps, 1, spread) !=3D 2) + return 0; + + assert (1 <=3D ps->max_var); + idx =3D rrng (ps, 1, ps->max_var); + res =3D int2lit (ps, idx); + + if (res->val !=3D UNDEF) + { + delta =3D rrng (ps, 1, ps->max_var); + while (gcd (delta, ps->max_var) !=3D 1) + delta--; + + assert (1 <=3D delta); + assert (delta <=3D ps->max_var); + + do { + idx +=3D delta; + if (idx > ps->max_var) + idx -=3D ps->max_var; + res =3D int2lit (ps, idx); + } while (res->val !=3D UNDEF); + } + +#ifdef STATS + ps->rdecisions++; +#endif + res =3D decide_phase (ps, res); + LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res))); + + return res; +} + +static Lit * +sdecide (PS * ps) +{ + Lit *res; + Rnk *r; + + for (;;) + { + r =3D htop (ps); + res =3D RNK2LIT (r); + if (res->val =3D=3D UNDEF) break; + (void) hpop (ps); + NOLOG ( fprintf (ps->out, + "%shpop %u %u %u\n", + ps->prefix, r - ps->rnks, + FLTMANTISSA(r->score), + FLTEXPONENT(r->score))); + } + +#ifdef STATS + ps->sdecisions++; +#endif + res =3D decide_phase (ps, res); + + LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res))); + + return res; +} + +static Lit * +adecide (PS * ps) +{ + Lit *lit; + Var * v; + + assert (ps->als < ps->alshead); + assert (!ps->failed_assumption); + + while (ps->alstail < ps->alshead) + { + lit =3D *ps->alstail++; + + if (lit->val =3D=3D FALSE) + { + ps->failed_assumption =3D lit; + v =3D LIT2VAR (lit); + + use_var (ps, v); + + LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n", + ps->prefix, LIT2INT (ps->failed_assumption))); + fanalyze (ps); + return 0; + } + + if (lit->val =3D=3D TRUE) + { + v =3D LIT2VAR (lit); + if (v->level > ps->adecidelevel) + ps->adecidelevel =3D v->level; + continue; + } + +#ifdef STATS + ps->assumptions++; +#endif + LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit))= ); + ps->adecidelevel =3D ps->LEVEL + 1; + + return lit; + } + + return 0; +} + +static void +decide (PS * ps) +{ + Lit * lit; + + assert (!satisfied (ps)); + assert (!ps->conflict); + + if (ps->alstail < ps->alshead && (lit =3D adecide (ps))) + ; + else if (ps->failed_assumption) + return; + else if (satisfied (ps)) + return; + else if (!(lit =3D rdecide (ps))) + lit =3D sdecide (ps); + + assert (lit); + assign_decision (ps, lit); + + ps->levelsum +=3D ps->LEVEL; + ps->decisions++; +} + +static int +sat (PS * ps, int l) +{ + int count =3D 0, backtracked; + + if (!ps->conflict) + bcp (ps); + + if (ps->conflict) + backtrack (ps); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + goto SATISFIED; + + if (ps->lsimplify <=3D ps->propagations) + simplify (ps, 0); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + goto SATISFIED; + + init_restart (ps); + + if (!ps->lreduce) + init_reduce (ps); + + ps->isimplify =3D ps->fixed; + backtracked =3D 0; + + for (;;) + { + if (!ps->conflict) + bcp (ps); + + if (ps->conflict) + { + incincs (ps); + backtrack (ps); + + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + backtracked =3D 1; + continue; + } + + if (satisfied (ps)) + { +SATISFIED: +#ifndef NDEBUG + original_clauses_satisfied (ps); + assumptions_satisfied (ps); +#endif + return PICOSAT_SATISFIABLE; + } + + if (backtracked) + { + backtracked =3D 0; + if (!ps->LEVEL && ps->isimplify < ps->fixed) + iteration (ps); + } + + if (l >=3D 0 && count >=3D l) /* decision limit reached ? */ + return PICOSAT_UNKNOWN; + + if (ps->interrupt.function && /* external interrupt */ + count > 0 && !(count % INTERRUPTLIM) && + ps->interrupt.function (ps->interrupt.state)) + return PICOSAT_UNKNOWN; + + if (ps->propagations >=3D ps->lpropagations)/* propagation limit rea= ched ? */ + return PICOSAT_UNKNOWN; + +#ifndef NADC + if (!ps->adodisabled && ps->adoconflicts >=3D ps->adoconflictlimit) + { + assert (bcp_queue_is_empty (ps)); + return PICOSAT_UNKNOWN; + } +#endif + + if (ps->fsimplify < ps->fixed && ps->lsimplify <=3D ps->propagations) + { + simplify (ps, 0); + if (!bcp_queue_is_empty (ps)) + continue; +#ifndef NFL + if (ps->mtcls) + return PICOSAT_UNSATISFIABLE; + + if (satisfied (ps)) + return PICOSAT_SATISFIABLE; + + assert (!ps->LEVEL); +#endif + } + + if (need_to_reduce (ps)) + reduce (ps, 50); --=20 2.39.2