From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 136BFC433F5 for ; Fri, 22 Oct 2021 13:38:13 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id E05806112F for ; Fri, 22 Oct 2021 13:38:12 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231564AbhJVNk3 (ORCPT ); Fri, 22 Oct 2021 09:40:29 -0400 Received: from out1.mail.ruhr-uni-bochum.de ([134.147.53.149]:31709 "EHLO out1.mail.ruhr-uni-bochum.de" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231516AbhJVNk3 (ORCPT ); Fri, 22 Oct 2021 09:40:29 -0400 Received: from mx1.mail.ruhr-uni-bochum.de (localhost [127.0.0.1]) by out1.mail.ruhr-uni-bochum.de (Postfix mo-ext) with ESMTP id 4HbQQp1zhSz8S6M; Fri, 22 Oct 2021 15:38:10 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=rub.de; s=mail-2017; t=1634909890; bh=UBsJF4KlTyaH7h2QJbPkvJf5CvluVqiE/KqIiSqdQpA=; h=Date:Subject:From:To:Cc:References:In-Reply-To:From; b=GdjeyWi6uqHr+xgEgwC/UIGmdu0hQsWM0des83h14Vzk+scunXIogCh+VaIu38dKK CCRbP4xaVztOL01hxzw8KcyIqh3wlfHXfUmM8ZPu2/kN+5XZ8Uch/oJAPYPip2vcRt Sh0aOakgjh9g5glMHVE1L+DokRcogIaGDm1Y56hA= Received: from out1.mail.ruhr-uni-bochum.de (localhost [127.0.0.1]) by mx1.mail.ruhr-uni-bochum.de (Postfix idis) with ESMTP id 4HbQQp16X1z8S6L; Fri, 22 Oct 2021 15:38:10 +0200 (CEST) X-Envelope-Sender: X-RUB-Notes: Internal origin=134.147.42.236 Received: from mail2.mail.ruhr-uni-bochum.de (mail2.mail.ruhr-uni-bochum.de [134.147.42.236]) by out1.mail.ruhr-uni-bochum.de (Postfix mi-int) with ESMTP id 4HbQQn6jb1z8S6K; Fri, 22 Oct 2021 15:38:09 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.1 at mx1.mail.ruhr-uni-bochum.de Received: from [10.150.66.4] (nb02.ig09.ruhr-uni-bochum.de [10.150.66.4]) by mail2.mail.ruhr-uni-bochum.de (Postfix) with ESMTPSA id 4HbQQn4dP4zDgys; Fri, 22 Oct 2021 15:38:09 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.0 at mail2.mail.ruhr-uni-bochum.de Message-ID: <61051172-6078-4920-a335-3ad1c8ab0d1c@rub.de> Date: Fri, 22 Oct 2021 15:38:07 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.2.0 Subject: [RFC v3 03/12] Add picosat.c (2/3) Content-Language: en-US From: Thorsten Berger To: linux-kbuild@vger.kernel.org Cc: deltaone@debian.org, phayax@gmail.com, Eugene Groshev , Sarah Nadi , Mel Gorman , "Luis R. Rodriguez" References: <7706ed5e-4771-770a-5cf2-d3c8346fa1dc@rub.de> In-Reply-To: <7706ed5e-4771-770a-5cf2-d3c8346fa1dc@rub.de> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Precedence: bulk List-ID: X-Mailing-List: linux-kbuild@vger.kernel.org The second part of picosat.c ---  scripts/kconfig/picosat.c | 3000 +++++++++++++++++++++++++++++++++++++  1 file changed, 3000 insertions(+) diff --git a/scripts/kconfig/picosat.c b/scripts/kconfig/picosat.c index 653bf0f0b99f..0a6eb3d5a45d 100644 --- a/scripts/kconfig/picosat.c +++ b/scripts/kconfig/picosat.c @@ -2998,3 +2998,3003 @@ unassign (PS * ps, Lit * lit)        {          other = p->lits[1];          q = p->next + 1; +      } +    else +      { +        assert (p->lits[1] == lit); +        q = p->next; +      } + +    next = *q; +    *q = *LIT2HTPS (other); +    *LIT2HTPS (other) = p; +    p = next; +      } +  } +#endif + +#ifndef NADC +  if (v->adotabpos) +    { +      assert (ps->nadotab); +      assert (*v->adotabpos == v->ado); + +      *v->adotabpos = 0; +      v->adotabpos = 0; + +      ps->nadotab--; +    } +#endif +} + +static Cls * +var2reason (PS * ps, Var * var) +{ +  Cls * res = var->reason; +#ifdef NO_BINARY_CLAUSES +  Lit * this, * other; +  if (ISLITREASON (res)) +    { +      this = VAR2LIT (var); +      if (this->val == FALSE) +    this = NOTLIT (this); + +      other = REASON2LIT (res); +      assert (other->val == TRUE); +      assert (this->val == TRUE); +      res = setimpl (ps, NOTLIT (other), this); +    } +#else +  (void) ps; +#endif +  return res; +} + +static void +mark_clause_to_be_collected (Cls * c) +{ +  assert (!c->collect); +  c->collect = 1; +} + +static void +undo (PS * ps, unsigned new_level) +{ +  Lit *lit; +  Var *v; + +  while (ps->thead > ps->trail) +    { +      lit = *--ps->thead; +      v = LIT2VAR (lit); +      if (v->level == new_level) +    { +      ps->thead++;        /* fix pre decrement */ +      break; +    } + +      unassign (ps, lit); +    } + +  ps->LEVEL = new_level; +  ps->ttail = ps->thead; +  ps->ttail2 = ps->thead; +#ifndef NADC +  ps->ttailado = ps->thead; +#endif + +#ifdef NO_BINARY_CLAUSES +  if (ps->conflict == &ps->cimpl) +    resetcimpl (ps); +#endif +#ifndef NADC +  if (ps->conflict && ps->conflict == ps->adoconflict) +    resetadoconflict (ps); +#endif +  ps->conflict = ps->mtcls; +  if (ps->LEVEL < ps->adecidelevel) +    { +      assert (ps->als < ps->alshead); +      ps->adecidelevel = 0; +      ps->alstail = ps->als; +    } +  LOG ( fprintf (ps->out, "%sback to level %u\n", ps->prefix, ps->LEVEL)); +} + +#ifndef NDEBUG + +static int +clause_satisfied (Cls * c) +{ +  Lit **p, **eol, *lit; + +  eol = end_of_lits (c); +  for (p = c->lits; p < eol; p++) +    { +      lit = *p; +      if (lit->val == TRUE) +    return 1; +    } + +  return 0; +} + +static void +original_clauses_satisfied (PS * ps) +{ +  Cls **p, *c; + +  for (p = ps->oclauses; p < ps->ohead; p++) +    { +      c = *p; + +      if (!c) +    continue; + +      if (c->learned) +    continue; + +      assert (clause_satisfied (c)); +    } +} + +static void +assumptions_satisfied (PS * ps) +{ +  Lit *lit, ** p; + +  for (p = ps->als; p < ps->alshead; p++) +    { +      lit = *p; +      assert (lit->val == TRUE); +    } +} + +#endif + +static void +sflush (PS * ps) +{ +  double now = picosat_time_stamp (); +  double delta = now - ps->entered; +  delta = (delta < 0) ? 0 : delta; +  ps->seconds += delta; +  ps->entered = now; +} + +static double +mb (PS * ps) +{ +  return ps->current_bytes / (double) (1 << 20); +} + +static double +avglevel (PS * ps) +{ +  return ps->decisions ? ps->levelsum / ps->decisions : 0.0; +} + +static void +rheader (PS * ps) +{ +  assert (ps->lastrheader <= ps->reports); + +  if (ps->lastrheader == ps->reports) +    return; + +  ps->lastrheader = ps->reports; + +   fprintf (ps->out, "%s\n", ps->prefix); +   fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]); +   fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]); +   fprintf (ps->out, "%s\n", ps->prefix); +} + +static unsigned +dynamic_flips_per_assignment_per_mille (PS * ps) +{ +  assert (FFLIPPEDPREC >= 1000); +  return ps->sdflips / (FFLIPPEDPREC / 1000); +} + +#ifdef NLUBY + +static int +high_agility (PS * ps) +{ +  return dynamic_flips_per_assignment_per_mille (ps) >= 200; +} + +static int +very_high_agility (PS * ps) +{ +  return dynamic_flips_per_assignment_per_mille (ps) >= 250; +} + +#else + +static int +medium_agility (PS * ps) +{ +  return dynamic_flips_per_assignment_per_mille (ps) >= 230; +} + +#endif + +static void +relemdata (PS * ps) +{ +  char *p; +  int x; + +  if (ps->reports < 0) +    { +      /* strip trailing white space +       */ +      for (x = 0; x <= 1; x++) +    { +      p = ps->rline[x] + strlen (ps->rline[x]); +      while (p-- > ps->rline[x]) +        { +          if (*p != ' ') +        break; + +          *p = 0; +        } +    } + +      rheader (ps); +    } +  else +    fputc ('\n', ps->out); + +  ps->RCOUNT = 0; +} + +static void +relemhead (PS * ps, const char * name, int fp, double val) +{ +  int x, y, len, size; +  const char *fmt; +  unsigned tmp, e; + +  if (ps->reports < 0) +    { +      x = ps->RCOUNT & 1; +      y = (ps->RCOUNT / 2) * 12 + x * 6; + +      if (ps->RCOUNT == 1) +    sprintf (ps->rline[1], "%6s", ""); + +      len = strlen (name); +      while (ps->szrline <= len + y + 1) +    { +      size = ps->szrline ? 2 * ps->szrline : 128; +      ps->rline[0] = resize (ps, ps->rline[0], ps->szrline, size); +      ps->rline[1] = resize (ps, ps->rline[1], ps->szrline, size); +      ps->szrline = size; +    } + +      fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s"; +      sprintf (ps->rline[x] + y, fmt, name, ""); +    } +  else if (val < 0) +    { +      assert (fp); + +      if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0) +    { +       fprintf (ps->out, "-%4.1f ", -tmp / 10.0); +    } +      else +    { +      tmp = -val / 10.0 + 0.5; +      e = 1; +      while (tmp >= 100) +        { +          tmp /= 10; +          e++; +        } + +       fprintf (ps->out, "-%2ue%u ", tmp, e); +    } +    } +  else +    { +      if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000) +    { +       fprintf (ps->out, "%5.1f ", tmp / 10.0); +    } +      else if (!fp && (tmp = val) < 100000) +    { +       fprintf (ps->out, "%5u ", tmp); +    } +      else +    { +      tmp = val / 10.0 + 0.5; +      e = 1; + +      while (tmp >= 1000) +        { +          tmp /= 10; +          e++; +        } + +       fprintf (ps->out, "%3ue%u ", tmp, e); +    } +    } + +  ps->RCOUNT++; +} + +inline static void +relem (PS * ps, const char *name, int fp, double val) +{ +  if (name) +    relemhead (ps, name, fp, val); +  else +    relemdata (ps); +} + +static unsigned +reduce_limit_on_lclauses (PS * ps) +{ +  unsigned res = ps->lreduce; +  res += ps->llocked; +  return res; +} + +static void +report (PS * ps, int replevel, char type) +{ +  int rounds; + +#ifdef RCODE +  (void) type; +#endif + +  if (ps->verbosity < replevel) +    return; + +  sflush (ps); + +  if (!ps->reports) +    ps->reports = -1; + +  for (rounds = (ps->reports < 0) ? 2 : 1; rounds; rounds--) +    { +      if (ps->reports >= 0) +     fprintf (ps->out, "%s%c ", ps->prefix, type); + +      relem (ps, "seconds", 1, ps->seconds); +      relem (ps, "level", 1, avglevel (ps)); +      assert (ps->fixed <=  ps->max_var); +      relem (ps, "variables", 0, ps->max_var - ps->fixed); +      relem (ps, "used", 1, PERCENT (ps->vused, ps->max_var)); +      relem (ps, "original", 0, ps->noclauses); +      relem (ps, "conflicts", 0, ps->conflicts); +      // relem (ps, "decisions", 0, ps->decisions); +      // relem (ps, "conf/dec", 1, PERCENT(ps->conflicts,ps->decisions)); +      // relem (ps, "limit", 0, reduce_limit_on_lclauses (ps)); +      relem (ps, "learned", 0, ps->nlclauses); +      // relem (ps, "limit", 1, PERCENT (ps->nlclauses, reduce_limit_on_lclauses (ps))); +      relem (ps, "limit", 0, ps->lreduce); +#ifdef STATS +      relem (ps, "learning", 1, PERCENT (ps->llused, ps->lladded)); +#endif +      relem (ps, "agility", 1, dynamic_flips_per_assignment_per_mille (ps) / 10.0); +      // relem (ps, "original", 0, ps->noclauses); +      relem (ps, "MB", 1, mb (ps)); +      // relem (ps, "lladded", 0, ps->lladded); +      // relem (ps, "llused", 0, ps->llused); + +      relem (ps, 0, 0, 0); + +      ps->reports++; +    } + +  /* Adapt this to the number of rows in your terminal. +   */ +  #define ROWS 25 + +  if (ps->reports % (ROWS - 3) == (ROWS - 4)) +    rheader (ps); + +  fflush (ps->out); +} + +static int +bcp_queue_is_empty (PS * ps) +{ +  if (ps->ttail != ps->thead) +    return 0; + +  if (ps->ttail2 != ps->thead) +    return 0; + +#ifndef NADC +  if (ps->ttailado != ps->thead) +    return 0; +#endif + +  return 1; +} + +static int +satisfied (PS * ps) +{ +  assert (!ps->mtcls); +  assert (!ps->failed_assumption); +  if (ps->alstail < ps->alshead) +    return 0; +  assert (!ps->conflict); +  assert (bcp_queue_is_empty (ps)); +  return ps->thead == ps->trail + ps->max_var;    /* all assigned */ +} + +static void +vrescore (PS * ps) +{ +  Rnk *p, *eor = ps->rnks + ps->max_var; +  for (p = ps->rnks + 1; p <= eor; p++) +    if (p->score != INFFLT) +      p->score = mulflt (p->score, ps->ilvinc); +  ps->vinc = mulflt (ps->vinc, ps->ilvinc);; +#ifdef VISCORES +  ps->nvinc = mulflt (ps->nvinc, ps->lscore);; +#endif +} + +static void +inc_score (PS * ps, Var * v) +{ +  Flt score; +  Rnk *r; + +#ifndef NFL +  if (ps->simplifying) +    return; +#endif + +  if (!v->level) +    return; + +  if (v->internal) +    return; + +  r = VAR2RNK (v); +  score = r->score; + +  assert (score != INFFLT); + +  score = addflt (score, ps->vinc); +  assert (score < INFFLT); +  r->score = score; +  if (r->pos > 0) +    hup (ps, r); + +  if (score > ps->lscore) +    vrescore (ps); +} + +static void +inc_activity (PS * ps, Cls * c) +{ +  Act *p; + +  if (!c->learned) +    return; + +  if (c->size <= 2) +    return; + +  p = CLS2ACT (c); +  *p = addflt (*p, ps->cinc); +} + +static unsigned +hashlevel (unsigned l) +{ +  return 1u << (l & 31); +} + +static void +push (PS * ps, Var * v) +{ +  if (ps->dhead == ps->eod) +    ENLARGE (ps->dfs, ps->dhead, ps->eod); + +  *ps->dhead++ = v; +} + +static Var * +pop (PS * ps) +{ +  assert (ps->dfs < ps->dhead); +  return *--ps->dhead; +} + +static void +analyze (PS * ps) +{ +  unsigned open, minlevel, siglevels, l, old, i, orig; +  Lit *this, *other, **p, **q, **eol; +  Var *v, *u, **m, *start, *uip; +  Cls *c; + +  assert (ps->conflict); + +  assert (ps->ahead == ps->added); +  assert (ps->mhead == ps->marked); +  assert (ps->rhead == ps->resolved); + +  /* First, search for First UIP variable and mark all resolved variables. +   * At the same time determine the minimum decision level involved. +   * Increase activities of resolved variables. +   */ +  q = ps->thead; +  open = 0; +  minlevel = ps->LEVEL; +  siglevels = 0; +  uip = 0; + +  c = ps->conflict; + +  for (;;) +    { +      add_antecedent (ps, c); +      inc_activity (ps, c); +      eol = end_of_lits (c); +      for (p = c->lits; p < eol; p++) +    { +      other = *p; + +      if (other->val == TRUE) +        continue; + +      assert (other->val == FALSE); + +      u = LIT2VAR (other); +      if (u->mark) +        continue; +      +      u->mark = 1; +      inc_score (ps, u); +      use_var (ps, u); + +      if (u->level == ps->LEVEL) +        { +          open++; +        } +      else +        { +          push_var_as_marked (ps, u); + +          if (u->level) +        { +          /* The statistics counter 'nonminimizedllits' sums up the +           * number of literals that would be added if only the +           * 'first UIP' scheme for learned clauses would be used +           * and no clause minimization. +           */ +          ps->nonminimizedllits++; + +          if (u->level < minlevel) +            minlevel = u->level; + +          siglevels |= hashlevel (u->level); +        } +          else +        { +          assert (!u->level); +          assert (u->reason); +        } +        } +    } + +      do +    { +      if (q == ps->trail) +        { +          uip = 0; +          goto DONE_FIRST_UIP; +        } + +      this = *--q; +      uip = LIT2VAR (this); +    } +      while (!uip->mark); + +      uip->mark = 0; + +      c = var2reason (ps, uip); +#ifdef NO_BINARY_CLAUSES +      if (c == &ps->impl) +    resetimpl (ps); +#endif +     open--; +     if ((!open && ps->LEVEL) || !c) +    break; + +     assert (c); +    } + +DONE_FIRST_UIP: + +  if (uip) +    { +      assert (ps->LEVEL); +      this = VAR2LIT (uip); +      this += (this->val == TRUE); +      ps->nonminimizedllits++; +      ps->minimizedllits++; +      add_lit (ps, this); +#ifdef STATS +      if (uip->reason) +    ps->uips++; +#endif +    } +  else +    assert (!ps->LEVEL); + +  /* Second, try to mark more intermediate variables, with the goal to +   * minimize the conflict clause.  This is a DFS from already marked +   * variables backward through the implication graph.  It tries to reach +   * other marked variables.  If the search reaches an unmarked decision +   * variable or a variable assigned below the minimum level of variables in +   * the first uip learned clause or a level on which no variable has been +   * marked, then the variable from which the DFS is started is not +   * redundant.  Otherwise the start variable is redundant and will +   * eventually be removed from the learned clause in step 4.  We initially +   * implemented BFS, but then profiling revelead that this step is a bottle +   * neck for certain incremental applications.  After switching to DFS this +   * hot spot went away. +   */ +  orig = ps->mhead - ps->marked; +  for (i = 0; i < orig; i++) +    { +      start = ps->marked[i]; + +      assert (start->mark); +      assert (start != uip); +      assert (start->level < ps->LEVEL); + +      if (!start->reason) +    continue; + +      old = ps->mhead - ps->marked; +      assert (ps->dhead == ps->dfs); +      push (ps, start); + +      while (ps->dhead > ps->dfs) +    { +      u = pop (ps); +      assert (u->mark); + +      c = var2reason (ps, u); +#ifdef NO_BINARY_CLAUSES +      if (c == &ps->impl) +        resetimpl (ps); +#endif +      if (!c || +          ((l = u->level) && +           (l < minlevel || ((hashlevel (l) & ~siglevels))))) +        { +          while (ps->mhead > ps->marked + old)    /* reset all marked */ +        (*--ps->mhead)->mark = 0; + +          ps->dhead = ps->dfs;        /* and DFS stack */ +          break; +        } + +      eol = end_of_lits (c); +      for (p = c->lits; p < eol; p++) +        { +          v = LIT2VAR (*p); +          if (v->mark) +        continue; + +          mark_var (ps, v); +          push (ps, v); +        } +    } +    } + +  for (m = ps->marked; m < ps->mhead; m++) +    { +      v = *m; + +      assert (v->mark); +      assert (!v->resolved); + +      use_var (ps, v); + +      c = var2reason (ps, v); +      if (!c) +    continue; + +#ifdef NO_BINARY_CLAUSES +      if (c == &ps->impl) +    resetimpl (ps); +#endif +      eol = end_of_lits (c); +      for (p = c->lits; p < eol; p++) +    { +      other = *p; + +      u = LIT2VAR (other); +      if (!u->level) +        continue; + +      if (!u->mark)        /* 'MARKTEST' */ +        break; +    } + +      if (p != eol) +    continue; + +      add_antecedent (ps, c); +      v->resolved = 1; +    } + +  for (m = ps->marked; m < ps->mhead; m++) +    { +      v = *m; + +      assert (v->mark); +      v->mark = 0; + +      if (v->resolved) +    { +      v->resolved = 0; +      continue; +    } + +      this = VAR2LIT (v); +      if (this->val == TRUE) +    this++;            /* actually NOTLIT */ + +      add_lit (ps, this); +      ps->minimizedllits++; +    } + +  assert (ps->ahead <= ps->eoa); +  assert (ps->rhead <= ps->eor); + +  ps->mhead = ps->marked; +} + +static void +fanalyze (PS * ps) +{ +  Lit ** eol, ** p, * lit; +  Cls * c, * reason; +  Var * v, * u; +  int next; + +#ifndef RCODE +  double start = picosat_time_stamp (); +#endif + +  assert (ps->failed_assumption); +  assert (ps->failed_assumption->val == FALSE); + +  v = LIT2VAR (ps->failed_assumption); +  reason = var2reason (ps, v); +  if (!reason) return; +#ifdef NO_BINARY_CLAUSES +  if (reason == &ps->impl) +    resetimpl (ps); +#endif + +  eol = end_of_lits (reason); +  for (p = reason->lits; p != eol; p++) +    { +      lit = *p; +      u = LIT2VAR (lit); +      if (u == v) continue; +      if (u->reason) break; +    } +  if (p == eol) return; + +  assert (ps->ahead == ps->added); +  assert (ps->mhead == ps->marked); +  assert (ps->rhead == ps->resolved); + +  next = 0; +  mark_var (ps, v); +  add_lit (ps, NOTLIT (ps->failed_assumption)); + +  do +    { +      v = ps->marked[next++]; +      use_var (ps, v); +      if (v->reason) +    { +      reason = var2reason (ps, v); +#ifdef NO_BINARY_CLAUSES +      if (reason == &ps->impl) +        resetimpl (ps); +#endif +      add_antecedent (ps, reason); +      eol = end_of_lits (reason); +      for (p = reason->lits; p != eol; p++) +        { +          lit = *p; +          u = LIT2VAR (lit); +          if (u == v) continue; +          if (u->mark) continue; +          mark_var (ps, u); +        } +    } +      else +    { +      lit = VAR2LIT (v); +      if (lit->val == TRUE) lit = NOTLIT (lit); +      add_lit (ps, lit); +    } +    } +  while (ps->marked + next < ps->mhead); + +  c = add_simplified_clause (ps, 1); +  v = LIT2VAR (ps->failed_assumption); +  reason = v->reason; +#ifdef NO_BINARY_CLAUSES +  if (!ISLITREASON (reason)) +#endif +    { +      assert (reason->locked); +      reason->locked = 0; +      if (reason->learned && reason->size > 2) +    { +      assert (ps->llocked > 0); +      ps->llocked--; +    } +    } + +#ifdef NO_BINARY_CLAUSES +  if (c == &ps->impl) +    { +      c = impl2reason (ps, NOTLIT (ps->failed_assumption)); +    } +  else +#endif +    { +      assert (c->learned); +      assert (!c->locked); +      c->locked = 1; +      if (c->size > 2) +    { +      ps->llocked++; +      assert (ps->llocked > 0); +    } +    } + +  v->reason = c; + +  while (ps->mhead > ps->marked) +    (*--ps->mhead)->mark = 0; + +  if (ps->verbosity) +     fprintf (ps->out, "%sfanalyze took %.1f seconds\n", +         ps->prefix, picosat_time_stamp () - start); +} + +/* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in + * which 'this' occurs. + */ +inline static void +prop2 (PS * ps, Lit * this) +{ +#ifdef NO_BINARY_CLAUSES +  Lit ** l, ** start; +  Ltk * lstk; +#else +  Cls * c, ** p; +  Cls * next; +#endif +  Lit * other; +  Val tmp; + +  assert (this->val == FALSE); + +#ifdef NO_BINARY_CLAUSES +  lstk = LIT2IMPLS (this); +  start = lstk->start; +  l = start + lstk->count; +  while (l != start) +    { +      /* The counter 'visits' is the number of clauses that are +       * visited during propagations of assignments. +       */ +      ps->visits++; +#ifdef STATS +      ps->bvisits++; +#endif +      other = *--l; +      tmp = other->val; + +      if (tmp == TRUE) +    { +#ifdef STATS +      ps->othertrue++; +      ps->othertrue2++; +      if (LIT2VAR (other)->level < ps->LEVEL) +        ps->othertrue2u++; +#endif +      continue; +    } + +      if (tmp != FALSE) +    { +      assign_forced (ps, other, LIT2REASON (NOTLIT(this))); +      continue; +    } + +      if (ps->conflict == &ps->cimpl) +    resetcimpl (ps); +      ps->conflict = setcimpl (ps, this, other); +    } +#else +  /* Traverse all binary clauses with 'this'.  Head/Tail pointers for binary +   * clauses do not have to be modified here. +   */ +  p = LIT2IMPLS (this); +  for (c = *p; c; c = next) +    { +      ps->visits++; +#ifdef STATS +      ps->bvisits++; +#endif +      assert (!c->collect); +#ifdef TRACE +      assert (!c->collected); +#endif +      assert (c->size == 2); +       +      other = c->lits[0]; +      if (other == this) +    { +      next = c->next[0]; +      other = c->lits[1]; +    } +      else +    next = c->next[1]; + +      tmp = other->val; + +      if (tmp == TRUE) +    { +#ifdef STATS +      ps->othertrue++; +      ps->othertrue2++; +      if (LIT2VAR (other)->level < ps->LEVEL) +        ps->othertrue2u++; +#endif +      continue; +    } + +      if (tmp == FALSE) +    ps->conflict = c; +      else +    assign_forced (ps, other, c);    /* unit clause */ +    } +#endif /* !defined(NO_BINARY_CLAUSES) */ +} + +#ifndef NDSC +static int +should_disconnect_head_tail (PS * ps, Lit * lit) +{ +  unsigned litlevel; +  Var * v; + +  assert (lit->val == TRUE); + +  v = LIT2VAR (lit); +  litlevel = v->level; + +  if (!litlevel) +    return 1; + +#ifndef NFL +  if (ps->simplifying) +    return 0; +#endif + +  return litlevel < ps->LEVEL; +} +#endif + +inline static void +propl (PS * ps, Lit * this) +{ +  Lit **l, *other, *prev, *new_lit, **eol; +  Cls *next, **htp_ptr, **new_htp_ptr; +  Cls *c; +#ifdef STATS +  unsigned size; +#endif + +  htp_ptr = LIT2HTPS (this); +  assert (this->val == FALSE); + +  /* Traverse all non binary clauses with 'this'.  Head/Tail pointers are +   * updated as well. +   */ +  for (c = *htp_ptr; c; c = next) +    { +      ps->visits++; +#ifdef STATS +      size = c->size; +      assert (size >= 3); +      ps->traversals++;    /* other is dereferenced at least */ + +      if (size == 3) +    ps->tvisits++; +      else if (size >= 4) +    { +      ps->lvisits++; +      ps->ltraversals++; +    } +#endif +#ifdef TRACE +      assert (!c->collected); +#endif +      assert (c->size > 0); + +      other = c->lits[0]; +      if (other != this) +    { +      assert (c->size != 1); +      c->lits[0] = this; +      c->lits[1] = other; +      next = c->next[1]; +      c->next[1] = c->next[0]; +      c->next[0] = next; +    } +      else if (c->size == 1)    /* With assumptions we need to +                             * traverse unit clauses as well. +                     */ +    { +      assert (!ps->conflict); +      ps->conflict = c; +      break; +    } +      else +    { +      assert (other == this && c->size > 1); +      other = c->lits[1]; +      next = c->next[0]; +    } +      assert (other == c->lits[1]); +      assert (this == c->lits[0]); +      assert (next == c->next[0]); +      assert (!c->collect); + +      if (other->val == TRUE) +    { +#ifdef STATS +      ps->othertrue++; +      ps->othertruel++; +#endif +#ifndef NDSC +      if (should_disconnect_head_tail (ps, other)) +        { +          new_htp_ptr = LIT2DHTPS (other); +          c->next[0] = *new_htp_ptr; +          *new_htp_ptr = c; +#ifdef STATS +          ps->othertruelu++; +#endif +          *htp_ptr = next; +          continue; +        } +#endif +      htp_ptr = c->next; +      continue; +    } + +      l = c->lits + 1; +      eol = (Lit**) c->lits + c->size; +      prev = this; + +      while (++l != eol) +    { +#ifdef STATS +      if (size >= 3) +        { +          ps->traversals++; +          if (size > 3) +        ps->ltraversals++; +        } +#endif +      new_lit = *l; +      *l = prev; +      prev = new_lit; +      if (new_lit->val != FALSE) break; +    } + +      if (l == eol) +    { +      while (l > c->lits + 2) +        { +          new_lit = *--l; +          *l = prev; +          prev = new_lit; +        } +      assert (c->lits[0] == this); + +      assert (other == c->lits[1]); +      if (other->val == FALSE)    /* found conflict */ +        { +          assert (!ps->conflict); +          ps->conflict = c; +          return; +        } + +      assign_forced (ps, other, c);        /* unit clause */ +      htp_ptr = c->next; +    } +      else +    { +      assert (new_lit->val == TRUE || new_lit->val == UNDEF); +      c->lits[0] = new_lit; +      // *l = this; +      new_htp_ptr = LIT2HTPS (new_lit); +      c->next[0] = *new_htp_ptr; +      *new_htp_ptr = c; +      *htp_ptr = next; +    } +    } +} + +#ifndef NADC + +static unsigned primes[] = { 996293, 330643, 753947, 500873 }; + +#define PRIMES ((sizeof primes)/sizeof *primes) + +static unsigned +hash_ado (PS * ps, Lit ** ado, unsigned salt) +{ +  unsigned i, res, tmp; +  Lit ** p, * lit; + +  assert (salt < PRIMES); + +  i = salt; +  res = 0; + +  for (p = ado; (lit = *p); p++) +    { +      assert (lit->val); + +      tmp = res >> 31; +      res <<= 1; + +      if (lit->val > 0) +    res |= 1; + +      assert (i < PRIMES); +      res *= primes[i++]; +      if (i == PRIMES) +    i = 0; + +      res += tmp; +    } + +  return res & (ps->szadotab - 1); +} + +static unsigned +cmp_ado (Lit ** a, Lit ** b) +{ +  Lit ** p, ** q, * l, * k; +  int res; + +  for (p = a, q = b; (l = *p); p++, q++) +    { +      k = *q; +      assert (k); +      if ((res = (l->val - k->val))) +    return res; +    } + +  assert (!*q); + +  return 0; +} + +static Lit *** +find_ado (PS * ps, Lit ** ado) +{ +  Lit *** res, ** other; +  unsigned pos, delta; + +  pos = hash_ado (ps, ado, 0); +  assert (pos < ps->szadotab); +  res = ps->adotab + pos; + +  other = *res; +  if (!other || !cmp_ado (other, ado)) +    return res; + +  delta = hash_ado (ps, ado, 1); +  if (!(delta & 1)) +    delta++; + +  assert (delta & 1); +  assert (delta < ps->szadotab); + +  for (;;) +    { +      pos += delta; +      if (pos >= ps->szadotab) +    pos -= ps->szadotab; + +      assert (pos < ps->szadotab); +      res = ps->adotab + pos; +      other = *res; +      if (!other || !cmp_ado (other, ado)) +    return res; +    } +} + +static void +enlarge_adotab (PS * ps) +{ +  /* TODO make this generic */ + +  ABORTIF (ps->szadotab, +           "internal: all different objects table needs larger initial size"); +  assert (!ps->nadotab); +  ps->szadotab = 10000; +  NEWN (ps->adotab, ps->szadotab); +  CLRN (ps->adotab, ps->szadotab); +} + +static int +propado (PS * ps, Var * v) +{ +  Lit ** p, ** q, *** adotabpos, **ado, * lit; +  Var * u; + +  if (ps->LEVEL && ps->adodisabled) +    return 1; + +  assert (!ps->conflict); +  assert (!ps->adoconflict); +  assert (VAR2LIT (v)->val != UNDEF); +  assert (!v->adotabpos); + +  if (!v->ado) +    return 1; + +  assert (v->inado); + +  for (p = v->ado; (lit = *p); p++) +    if (lit->val == UNDEF) +      { +    u = LIT2VAR (lit); +    assert (!u->ado); +    u->ado = v->ado; +    v->ado = 0; + +    return 1; +      } + +  if (4 * ps->nadotab >= 3 * ps->szadotab)    /* at least 75% filled */ +    enlarge_adotab (ps); + +  adotabpos = find_ado (ps, v->ado); +  ado = *adotabpos; + +  if (!ado) +    { +      ps->nadotab++; +      v->adotabpos = adotabpos; +      *adotabpos = v->ado; +      return 1; +    } + +  assert (ado != v->ado); + +  ps->adoconflict = new_clause (ps, 2 * llength (ado), 1); +  q = ps->adoconflict->lits; + +  for (p = ado; (lit = *p); p++) +    *q++ = lit->val == FALSE ? lit : NOTLIT (lit); + +  for (p = v->ado; (lit = *p); p++) +    *q++ = lit->val == FALSE ? lit : NOTLIT (lit); + +  assert (q == ENDOFCLS (ps->adoconflict)); +  ps->conflict = ps->adoconflict; +  ps->adoconflicts++; +  return 0; +} + +#endif + +static void +bcp (PS * ps) +{ +  int props = 0; +  assert (!ps->conflict); + +  if (ps->mtcls) +    return; + +  for (;;) +    { +      if (ps->ttail2 < ps->thead)    /* prioritize implications */ +    { +      props++; +      prop2 (ps, NOTLIT (*ps->ttail2++)); +    } +      else if (ps->ttail < ps->thead)    /* unit clauses or clauses with length > 2 */ +    { +      if (ps->conflict) break; +      propl (ps, NOTLIT (*ps->ttail++)); +      if (ps->conflict) break; +    } +#ifndef NADC +      else if (ps->ttailado < ps->thead) +    { +      if (ps->conflict) break; +      propado (ps, LIT2VAR (*ps->ttailado++)); +      if (ps->conflict) break; +    } +#endif +      else +    break;        /* all assignments propagated, so break */ +    } + +  ps->propagations += props; +} + +static unsigned +drive (PS * ps) +{ +  unsigned res, vlevel; +  Lit **p; +  Var *v; + +  res = 0; +  for (p = ps->added; p < ps->ahead; p++) +    { +      v = LIT2VAR (*p); +      vlevel = v->level; +      assert (vlevel <= ps->LEVEL); +      if (vlevel < ps->LEVEL && vlevel > res) +    res = vlevel; +    } + +  return res; +} + +#ifdef VISCORES + +static void +viscores (PS * ps) +{ +  Rnk *p, *eor = ps->rnks + ps->max_var; +  char name[100], cmd[200]; +  FILE * data; +  Flt s; +  int i; + +  for (p = ps->rnks + 1; p <= ps->eor; p++) +    { +      s = p->score; +      if (s == INFFLT) +    continue; +      s = mulflt (s, ps->nvinc); +      assert (flt2double (s) <= 1.0); +    } + +  sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts); +  sprintf (cmd, "sort -n|nl>%s", name); + +  data = popen (cmd, "w"); +  for (p = ps->rnks + 1; p <= ps->eor; p++) +    { +      s = p->score; +      if (s == INFFLT) +    continue; +      s = mulflt (s, ps->nvinc); +      fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnks)); +    } +  fflush (data); +  pclose (data); + +  for (i = 0; i < 8; i++) +    { +      sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i); +      system (cmd); +    } + +  fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts); +  fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max_var); + +  for (i = 0; i < 8; i++) +    fprintf (ps->fviscores, +             ", \"%s.%d\" using 1:2:3 with labels tc lt %d", +         name, i, i + 1); + +  fputc ('\n', ps->fviscores); +  fflush (ps->fviscores); +#ifndef WRITEGIF +  usleep (50000);        /* refresh rate of 20 Hz */ +#endif +} + +#endif + +static void +crescore (PS * ps) +{ +  Cls **p, *c; +  Act *a; +  Flt factor; +  int l = log2flt (ps->cinc); +  assert (l > 0); +  factor = base2flt (1, -l); + +  for (p = ps->lclauses; p != ps->lhead; p++) +    { +      c = *p; + +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif +      assert (c->learned); + +      if (c->size <= 2) +    continue; + +      a = CLS2ACT (c); +      *a = mulflt (*a, factor); +    } + +  ps->cinc = mulflt (ps->cinc, factor); +} + +static void +inc_vinc (PS * ps) +{ +#ifdef VISCORES +  ps->nvinc = mulflt (ps->nvinc, ps->fvinc); +#endif +  ps->vinc = mulflt (ps->vinc, ps->ifvinc); +} + +inline static void +inc_max_var (PS * ps) +{ +  Lit *lit; +  Rnk *r; +  Var *v; + +  assert (ps->max_var < ps->size_vars); + +  if (ps->max_var + 1 == ps->size_vars) +    enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */ + +  ps->max_var++;            /* new index of variable */ +  assert (ps->max_var);            /* no unsigned overflow */ + +  assert (ps->max_var < ps->size_vars); + +  lit = ps->lits + 2 * ps->max_var; +  lit[0].val = lit[1].val = UNDEF; + +  memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps); +#ifndef NDSC +  memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps); +#endif +  memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls); +  memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh); + +  v = ps->vars + ps->max_var;        /* initialize variable components */ +  CLR (v); + +  r = ps->rnks + ps->max_var;        /* initialize rank */ +  CLR (r); + +  hpush (ps, r); +} + +static void +force (PS * ps, Cls * c) +{ +  Lit ** p, ** eol, * lit, * forced; +  Cls * reason; + +  forced = 0; +  reason = c; + +  eol = end_of_lits (c); +  for (p = c->lits; p < eol; p++) +    { +      lit = *p; +      if (lit->val == UNDEF) +    { +      assert (!forced); +      forced = lit; +#ifdef NO_BINARY_CLAUSES +      if (c == &ps->impl) +        reason = LIT2REASON (NOTLIT (p[p == c->lits ? 1 : -1])); +#endif +    } +      else +    assert (lit->val == FALSE); +    } + +#ifdef NO_BINARY_CLAUSES +  if (c == &ps->impl) +    resetimpl (ps); +#endif +  if (!forced) +    return; + +  assign_forced (ps, forced, reason); +} + +static void +inc_lreduce (PS * ps) +{ +#ifdef STATS +  ps->inclreduces++; +#endif +  ps->lreduce *= FREDUCE; +  ps->lreduce /= 100; +  report (ps, 1, '+'); +} + +static void +backtrack (PS * ps) +{ +  unsigned new_level; +  Cls * c; + +  ps->conflicts++; +  LOG ( fprintf (ps->out, "%sconflict ", ps->prefix); dumpclsnl (ps, ps->conflict)); + +  analyze (ps); +  new_level = drive (ps); +  // TODO: why not? assert (new_level != 1  || (ps->ahead - ps->added) == 2); +  c = add_simplified_clause (ps, 1); +  undo (ps, new_level); +  force (ps, c); + +  if ( +#ifndef NFL +      !ps->simplifying && +#endif +      !--ps->lreduceadjustcnt) +    { +      /* With FREDUCE==110 and FREDADJ=121 we stir 'lreduce' to be +       * proportional to 'sqrt(conflicts)'.  In earlier version we actually +       * used  'FREDADJ=150', which results in 'lreduce' to approximate +       * 'conflicts^(log(1.1)/log(1.5))' which is close to the fourth root +       * of 'conflicts', since log(1.1)/log(1.5)=0.235 (as observed by +       * Donald Knuth). The square root is the same we get by a Glucose +       * style increase, which simply adds a constant at every reduction. +       * This would be way simpler to implement but for now we keep the more +       * complicated code using the adjust increments and counters. +       */ +      ps->lreduceadjustinc *= FREDADJ; ps->lreduceadjustinc /= 100; ps->lreduceadjustcnt +      = ps->lreduceadjustinc; +      inc_lreduce (ps); +    } + +  if (ps->verbosity >= 4 && !(ps->conflicts % 1000)) +    report (ps, 4, 'C'); +} + +static void +inc_cinc (PS * ps) +{ +  ps->cinc = mulflt (ps->cinc, ps->fcinc); +  if (ps->lcinc < ps->cinc) +    crescore (ps); +} + +static void +incincs (PS * ps) +{ +  inc_vinc (ps); +  inc_cinc (ps); +#ifdef VISCORES +  viscores (ps); +#endif +} + +static void +disconnect_clause (PS * ps, Cls * c) +{ +  assert (c->connected); + +  if (c->size > 2) +    { +      if (c->learned) +    { +      assert (ps->nlclauses > 0); +      ps->nlclauses--; + +      assert (ps->llits >= c->size); +      ps->llits -= c->size; +    } +      else +    { +      assert (ps->noclauses > 0); +      ps->noclauses--; + +      assert (ps->olits >= c->size); +      ps->olits -= c->size; +    } +    } + +#ifndef NDEBUG +  c->connected = 0; +#endif +} + +static int +clause_is_toplevel_satisfied (PS * ps, Cls * c) +{ +  Lit *lit, **p, **eol = end_of_lits (c); +  Var *v; + +  for (p = c->lits; p < eol; p++) +    { +      lit = *p; +      if (lit->val == TRUE) +    { +      v = LIT2VAR (lit); +      if (!v->level) +        return 1; +    } +    } + +  return 0; +} + +static int +collect_clause (PS * ps, Cls * c) +{ +  assert (c->collect); +  c->collect = 0; + +#ifdef TRACE +  assert (!c->collected); +  c->collected = 1; +#endif +  disconnect_clause (ps, c); + +#ifdef TRACE +  if (ps->trace && (!c->learned || c->used)) +    return 0; +#endif +  delete_clause (ps, c); + +  return 1; +} + +static size_t +collect_clauses (PS * ps) +{ +  Cls *c, **p, **q, * next; +  Lit * lit, * eol; +  size_t res; +  int i; + +  res = ps->current_bytes; + +  eol = ps->lits + 2 * ps->max_var + 1; +  for (lit = ps->lits + 2; lit <= eol; lit++) +    { +      for (i = 0; i <= 1; i++) +    { +      if (i) +        { +#ifdef NO_BINARY_CLAUSES +          Ltk * lstk = LIT2IMPLS (lit); +          Lit ** r, ** s; +          r = lstk->start; +          if (lit->val != TRUE || LIT2VAR (lit)->level) +        for (s = r; s < lstk->start + lstk->count; s++) +          { +            Lit * other = *s; +            Var *v = LIT2VAR (other); +            if (v->level || +                other->val != TRUE) +              *r++ = other; +          } +          lstk->count = r - lstk->start; +          continue; +#else +          p = LIT2IMPLS (lit); +#endif +        } +      else +        p = LIT2HTPS (lit); + +      for (c = *p; c; c = next) +        { +          q = c->next; +          if (c->lits[0] != lit) +        q++; + +          next = *q; +          if (c->collect) +        *p = next; +          else +        p = q; +        } +    } +    } + +#ifndef NDSC +  for (lit = ps->lits + 2; lit <= eol; lit++) +    { +      p = LIT2DHTPS (lit); +      while ((c = *p)) +    { +      Lit * other = c->lits[0]; +      if (other == lit) +        { +          q = c->next + 1; +        } +      else +        { +          assert (c->lits[1] == lit); +          q = c->next; +        } + +      if (c->collect) +        *p = *q; +      else +        p = q; +    } +    } +#endif + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; + +      if (!c) +    continue; + +      if (!c->collect) +    continue; + +      if (collect_clause (ps, c)) +    *p = 0; +    } + +#ifdef TRACE +  if (!ps->trace) +#endif +    { +      q = ps->oclauses; +      for (p = q; p < ps->ohead; p++) +    if ((c = *p)) +      *q++ = c; +      ps->ohead = q; + +      q = ps->lclauses; +      for (p = q; p < ps->lhead; p++) +    if ((c = *p)) +      *q++ = c; +      ps->lhead = q; +    } + +  assert (ps->current_bytes <= res); +  res -= ps->current_bytes; +  ps->recycled += res; + +  LOG ( fprintf (ps->out, "%scollected %ld bytes\n", ps->prefix, (long)res)); + +  return res; +} + +static int +need_to_reduce (PS * ps) +{ +  return ps->nlclauses >= reduce_limit_on_lclauses (ps); +} + +#ifdef NLUBY + +static void +inc_drestart (PS * ps) +{ +  ps->drestart *= FRESTART; +  ps->drestart /= 100; + +  if (ps->drestart >= MAXRESTART) +    ps->drestart = MAXRESTART; +} + +static void +inc_ddrestart (PS * ps) +{ +  ps->ddrestart *= FRESTART; +  ps->ddrestart /= 100; + +  if (ps->ddrestart >= MAXRESTART) +    ps->ddrestart = MAXRESTART; +} + +#else + +static unsigned +luby (unsigned i) +{ +  unsigned k; +  for (k = 1; k < 32; k++) +    if (i == (1u << k) - 1) +      return 1u << (k - 1); + +  for (k = 1;; k++) +    if ((1u << (k - 1)) <= i && i < (1u << k) - 1) +      return luby (i - (1u << (k-1)) + 1); +} + +#endif + +#ifndef NLUBY +static void +inc_lrestart (PS * ps, int skip) +{ +  unsigned delta; + +  delta = 100 * luby (++ps->lubycnt); +  ps->lrestart = ps->conflicts + delta; + +  if (ps->waslubymaxdelta) +    report (ps, 1, skip ? 'N' : 'R'); +  else +    report (ps, 2, skip ? 'n' : 'r'); + +  if (delta > ps->lubymaxdelta) +    { +      ps->lubymaxdelta = delta; +      ps->waslubymaxdelta = 1; +    } +  else +    ps->waslubymaxdelta = 0; +} +#endif + +static void +init_restart (PS * ps) +{ +#ifdef NLUBY +  /* TODO: why is it better in incremental usage to have smaller initial +   * outer restart interval? +   */ +  ps->ddrestart = ps->calls > 1 ? MINRESTART : 1000; +  ps->drestart = MINRESTART; +  ps->lrestart = ps->conflicts + ps->drestart; +#else +  ps->lubycnt = 0; +  ps->lubymaxdelta = 0; +  ps->waslubymaxdelta = 0; +  inc_lrestart (ps, 0); +#endif +} + +static void +restart (PS * ps) +{ +  int skip; +#ifdef NLUBY +  char kind; +  int outer; + +  inc_drestart (ps); +  outer = (ps->drestart >= ps->ddrestart); + +  if (outer) +    skip = very_high_agility (ps); +  else +    skip = high_agility (ps); +#else +  skip = medium_agility (ps); +#endif + +#ifdef STATS +  if (skip) +    ps->skippedrestarts++; +#endif + +  assert (ps->conflicts >= ps->lrestart); + +  if (!skip) +    { +      ps->restarts++; +      assert (ps->LEVEL > 1); +      LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts)); +      undo (ps, 0); +    } + +#ifdef NLUBY +  if (outer) +    { +      kind = skip ? 'N' : 'R'; +      inc_ddrestart (ps); +      ps->drestart = MINRESTART; +    } +  else  if (skip) +    { +      kind = 'n'; +    } +  else +    { +      kind = 'r'; +    } + +  assert (ps->drestart <= MAXRESTART); +  ps->lrestart = ps->conflicts + ps->drestart; +  assert (ps->lrestart > ps->conflicts); + +  report (outer ? 1 : 2, kind); +#else +  inc_lrestart (ps, skip); +#endif +} + +inline static void +assign_decision (PS * ps, Lit * lit) +{ +  assert (!ps->conflict); + +  ps->LEVEL++; + +  LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL)); +  LOG ( fprintf (ps->out, +         "%sassign %d at level %d <= DECISION\n", +         ps->prefix, LIT2INT (lit), ps->LEVEL)); + +  assign (ps, lit, 0); +} + +#ifndef NFL + +static int +lit_has_binary_clauses (PS * ps, Lit * lit) +{ +#ifdef NO_BINARY_CLAUSES +  Ltk* lstk = LIT2IMPLS (lit); +  return lstk->count != 0; +#else +  return *LIT2IMPLS (lit) != 0; +#endif +} + +static void +flbcp (PS * ps) +{ +#ifdef STATS +  unsigned long long propagaions_before_bcp = ps->propagations; +#endif +  bcp (ps); +#ifdef STATS +  ps->flprops += ps->propagations - propagaions_before_bcp; +#endif +} + +inline static int +cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b) +{ +  (void) ps; +  return -cmp_rnk (a, b); +} + +inline static Flt +rnk2jwh (PS * ps, Rnk * r) +{ +  Flt res, sum, pjwh, njwh; +  Lit * plit, * nlit; + +  plit = RNK2LIT (r); +  nlit = plit + 1; +   +  pjwh = *LIT2JWH (plit); +  njwh = *LIT2JWH (nlit); + +  res = mulflt (pjwh, njwh); + +  sum = addflt (pjwh, njwh); +  sum = mulflt (sum, base2flt (1, -10)); +  res = addflt (res, sum); + +  return res; +} + +static int +cmp_inverse_jwh_rnk (PS * ps, Rnk * r, Rnk * s) +{ +  Flt a = rnk2jwh (ps, r); +  Flt b = rnk2jwh (ps, s); +  int res = cmpflt (a, b); + +  if (res) +    return -res; + +  return cmp_inverse_rnk (ps, r, s); +} + +static void +faillits (PS * ps) +{ +  unsigned i, j, old_trail_count, common, saved_count; +  unsigned new_saved_size, oldladded = ps->ladded; +  unsigned long long limit, delta; +  Lit * lit, * other, * pivot; +  Rnk * r, ** p, ** q; +  int new_trail_count; +  double started; + +  if (ps->plain) +    return; + +  if (ps->heap + 1 >= ps->hhead) +    return; + +  if (ps->propagations < ps->fllimit) +    return; + +  sflush (ps); +  started = ps->seconds; + +  ps->flcalls++; +#ifdef STATSA +  ps->flrounds++; +#endif +  delta = ps->propagations/10; +  if (delta >= 100*1000*1000) delta = 100*1000*1000; +  else if (delta <= 100*1000) delta = 100*1000; + +  limit = ps->propagations + delta; +  ps->fllimit = ps->propagations; + +  assert (!ps->LEVEL); +  assert (ps->simplifying); + +  if (ps->flcalls <= 1) +    SORT (Rnk *, cmp_inverse_jwh_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1)); +  else +    SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1)); + +  i = 1;        /* NOTE: heap starts at position '1' */ + +  while (ps->propagations < limit) +    { +      if (ps->heap + i == ps->hhead) +    { +      if (ps->ladded == oldladded) +        break; + +      i = 1; +#ifdef STATS +      ps->flrounds++; +#endif +      oldladded = ps->ladded; +    } + +      assert (ps->heap + i < ps->hhead); + +      r = ps->heap[i++]; +      lit = RNK2LIT (r); + +      if (lit->val) +    continue; + +      if (!lit_has_binary_clauses (ps, NOTLIT (lit))) +    { +#ifdef STATS +      ps->flskipped++; +#endif +      continue; +    } + +#ifdef STATS +      ps->fltried++; +#endif +      LOG ( fprintf (ps->out, "%strying %d as failed literal\n", +        ps->prefix, LIT2INT (lit))); + +      assign_decision (ps, lit); +      old_trail_count = ps->thead - ps->trail; +      flbcp (ps); + +      if (ps->conflict) +    { +EXPLICITLY_FAILED_LITERAL: +      LOG ( fprintf (ps->out, "%sfound explicitly failed literal %d\n", +        ps->prefix, LIT2INT (lit))); + +      ps->failedlits++; +      ps->efailedlits++; + +      backtrack (ps); +      flbcp (ps); + +      if (!ps->conflict) +        continue; + +CONTRADICTION: +      assert (!ps->LEVEL); +      backtrack (ps); +      assert (ps->mtcls); + +      goto RETURN; +    } + +      if (ps->propagations >= limit) +    { +      undo (ps, 0); +      break; +    } + +      lit = NOTLIT (lit); + +      if (!lit_has_binary_clauses (ps, NOTLIT (lit))) +    { +#ifdef STATS +      ps->flskipped++; +#endif +      undo (ps, 0); +      continue; +    } + +#ifdef STATS +      ps->fltried++; +#endif +      LOG ( fprintf (ps->out, "%strying %d as failed literals\n", +        ps->prefix, LIT2INT (lit))); + +      new_trail_count = ps->thead - ps->trail; +      saved_count = new_trail_count - old_trail_count; + +      if (saved_count > ps->saved_size) +    { +      new_saved_size = ps->saved_size ? 2 * ps->saved_size : 1; +      while (saved_count > new_saved_size) +        new_saved_size *= 2; + +      RESIZEN (ps->saved, ps->saved_size, new_saved_size); +      ps->saved_size = new_saved_size; +    } + +      for (j = 0; j < saved_count; j++) +    ps->saved[j] = ps->trail[old_trail_count + j]; + +      undo (ps, 0); + +      assign_decision (ps, lit); +      flbcp (ps); + +      if (ps->conflict) +    goto EXPLICITLY_FAILED_LITERAL; + +      pivot = (ps->thead - ps->trail <= new_trail_count) ? lit : NOTLIT (lit); + +      common = 0; +      for (j = 0; j < saved_count; j++) +    if ((other = ps->saved[j])->val == TRUE) +      ps->saved[common++] = other; + +      undo (ps, 0); + +      LOG (if (common) +         fprintf (ps->out, +              "%sfound %d literals implied by %d and %d\n", +              ps->prefix, common, +              LIT2INT (NOTLIT (lit)), LIT2INT (lit))); + +#if 1 // set to zero to disable 'lifting' +      for (j = 0; +       j < common +      /* TODO: For some Velev benchmarks, extracting the common implicit +       * failed literals took quite some time.  This needs to be fixed by +       * a dedicated analyzer.  Up to then we bound the number of +       * propagations in this loop as well. +       */ +       && ps->propagations < limit + delta +       ; j++) +    { +      other = ps->saved[j]; + +      if (other->val == TRUE) +        continue; + +      assert (!other->val); + +      LOG ( fprintf (ps->out, +            "%sforcing %d as forced implicitly failed literal\n", +            ps->prefix, LIT2INT (other))); + +      assert (pivot != NOTLIT (other)); +      assert (pivot != other); + +      assign_decision (ps, NOTLIT (other)); +      flbcp (ps); + +      assert (ps->LEVEL == 1); + +      if (ps->conflict) +        { +          backtrack (ps); +          assert (!ps->LEVEL); +        } +      else +        { +          assign_decision (ps, pivot); +          flbcp (ps); + +          backtrack (ps); + +          if (ps->LEVEL) +        { +          assert (ps->LEVEL == 1); + +          flbcp (ps); + +          if (ps->conflict) +            { +              backtrack (ps); +              assert (!ps->LEVEL); +            } +          else +            { +              assign_decision (ps, NOTLIT (pivot)); +              flbcp (ps); +              backtrack (ps); + +              if (ps->LEVEL) +            { +              assert (ps->LEVEL == 1); +              flbcp (ps); + +              if (!ps->conflict) +                { +#ifdef STATS +                  ps->floopsed++; +#endif +                  undo (ps, 0); +                  continue; +                } + +              backtrack (ps); +            } + +              assert (!ps->LEVEL); +            } + +          assert (!ps->LEVEL); +        } +        } +      assert (!ps->LEVEL); +      flbcp (ps); + +      ps->failedlits++; +      ps->ifailedlits++; + +      if (ps->conflict) +        goto CONTRADICTION; +    } +#endif +    } + +  ps->fllimit += 9 * (ps->propagations - ps->fllimit);    /* 10% for failed literals */ + +RETURN: + +  /* First flush top level assigned literals.  Those are prohibited from +   * being pushed up the heap during 'faillits' since 'simplifying' is set. +   */ +  assert (ps->heap < ps->hhead); +  for (p = q = ps->heap + 1; p < ps->hhead; p++) +    { +      r = *p; +      lit = RNK2LIT (r); +      if (lit->val) +           r->pos = 0; +      else +    *q++ = r; +    } + +  /* Then resort with respect to EVSIDS score and fix positions. +   */ +  SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1)); +  for (p = ps->heap + 1; p < ps->hhead; p++) +    (*p)->pos = p - ps->heap; + +  sflush (ps); +  ps->flseconds += ps->seconds - started; +} + +#endif + +static void +simplify (PS * ps, int forced) +{ +  Lit * lit, * notlit, ** t; +  unsigned collect, delta; +#ifdef STATS +  size_t bytes_collected; +#endif +  int * q, ilit; +  Cls **p, *c; +  Var * v; + +#ifndef NDEDBUG +  (void) forced; +#endif + +  assert (!ps->mtcls); +  assert (!satisfied (ps)); +  assert (forced || ps->lsimplify <= ps->propagations); +  assert (forced || ps->fsimplify <= ps->fixed); + +  if (ps->LEVEL) +    undo (ps, 0); +#ifndef NFL +  ps->simplifying = 1; +  faillits (ps); +  ps->simplifying = 0; + +  if (ps->mtcls) +    return; +#endif + +  if (ps->cils != ps->cilshead) +    { +      assert (ps->ttail == ps->thead); +      assert (ps->ttail2 == ps->thead); +      ps->ttail = ps->trail; +      for (t = ps->trail; t < ps->thead; t++) +    { +      lit = *t; +      v = LIT2VAR (lit); +      if (v->internal) +        { +          assert (LIT2INT (lit) < 0); +          assert (lit->val == TRUE); +          unassign (ps, lit); +        } +      else +        *ps->ttail++ = lit; +    } +      ps->ttail2 = ps->thead = ps->ttail; + +      for (q = ps->cils; q != ps->cilshead; q++) +    { +      ilit = *q; +      assert (0 < ilit && ilit <= (int) ps->max_var); +      v = ps->vars + ilit; +      assert (v->internal); +      v->level = 0; +      v->reason = 0; +      lit = int2lit (ps, -ilit); +      assert (lit->val == UNDEF); +      lit->val = TRUE; +      notlit = NOTLIT (lit); +      assert (notlit->val == UNDEF); +      notlit->val = FALSE; +    } +    } + +  collect = 0; +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif + +      if (c->locked) +    continue; +       +      assert (!c->collect); +      if (clause_is_toplevel_satisfied (ps, c)) +    { +      mark_clause_to_be_collected (c); +      collect++; +    } +    } + +  LOG ( fprintf (ps->out, "%scollecting %d clauses\n", ps->prefix, collect)); +#ifdef STATS +  bytes_collected = +#endif +  collect_clauses (ps); +#ifdef STATS +  ps->srecycled += bytes_collected; +#endif + +  if (ps->cils != ps->cilshead) +    { +      for (q = ps->cils; q != ps->cilshead; q++) +    { +      ilit = *q; +      assert (0 < ilit && ilit <= (int) ps->max_var); +      assert (ps->vars[ilit].internal); +      if (ps->rilshead == ps->eorils) +        ENLARGE (ps->rils, ps->rilshead, ps->eorils); +      *ps->rilshead++ = ilit; +      lit = int2lit (ps, -ilit); +      assert (lit->val == TRUE); +      lit->val = UNDEF; +      notlit = NOTLIT (lit); +      assert (notlit->val == FALSE); +      notlit->val = UNDEF; +    } +      ps->cilshead = ps->cils; +    } + +  delta = 10 * (ps->olits + ps->llits) + 100000; +  if (delta > 2000000) +    delta = 2000000; +  ps->lsimplify = ps->propagations + delta; +  ps->fsimplify = ps->fixed; +  ps->simps++; + +  report (ps, 1, 's'); +} + +static void +iteration (PS * ps) +{ +  assert (!ps->LEVEL); +  assert (bcp_queue_is_empty (ps)); +  assert (ps->isimplify < ps->fixed); + +  ps->iterations++; +  report (ps, 2, 'i'); +#ifdef NLUBY +  ps->drestart = MINRESTART; +  ps->lrestart = ps->conflicts + ps->drestart; +#else +  init_restart (ps); +#endif +  ps->isimplify = ps->fixed; +} + +static int +cmp_glue_activity_size (PS * ps, Cls * c, Cls * d) +{ +  Act a, b, * p, * q; + +  (void) ps; + +  assert (c->learned); +  assert (d->learned); + +  if (c->glue < d->glue)        // smaller glue preferred +    return 1; + +  if (c->glue > d->glue) +    return -1; + +  p = CLS2ACT (c); +  q = CLS2ACT (d); +  a = *p; +  b = *q; + +  if (a < b)                // then higher activity +    return -1; + +  if (b < a) +    return 1; + +  if (c->size < d->size)        // then smaller size +    return 1; + +  if (c->size > d->size) +    return -1; + +  return 0; +} + +static void +reduce (PS * ps, unsigned percentage) +{ +  unsigned redcount, lcollect, collect, target; +#ifdef STATS +  size_t bytes_collected; +#endif +  Cls **p, *c; + +  assert (ps->rhead == ps->resolved); + +  ps->lastreduceconflicts = ps->conflicts; + +  assert (percentage <= 100); +  LOG ( fprintf (ps->out, +                "%sreducing %u%% learned clauses\n", +        ps->prefix, percentage)); + +  while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved)) +    ENLARGE (ps->resolved, ps->rhead, ps->eor); + +  collect = 0; +  lcollect = 0; + +  for (p = ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p != EOC; p = NXC (p)) +    { +      c = *p; +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif + +      if (c->locked) +    continue; + +      assert (!c->collect); +      if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c)) +    { +      mark_clause_to_be_collected (c); +      collect++; + +      if (c->learned && c->size > 2) +        lcollect++; + +      continue; +    } + +      if (!c->learned) +    continue; + +      if (c->size <= 2) +    continue; + +      assert (ps->rhead < ps->eor); +      *ps->rhead++ = c; +    } +  assert (ps->rhead <= ps->eor); + +  ps->fsimplify = ps->fixed; + +  redcount = ps->rhead - ps->resolved; +  SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount); + +  assert (ps->nlclauses >= lcollect); +  target = ps->nlclauses - lcollect + 1; + +  target = (percentage * target + 99) / 100; + +  if (target >= redcount) +    target = redcount; + +  ps->rhead = ps->resolved + target; +  while (ps->rhead > ps->resolved) +    { +      c = *--ps->rhead; +      mark_clause_to_be_collected (c); + +      collect++; +      if (c->learned && c->size > 2)    /* just for consistency */ +    lcollect++; +    } + +  if (collect) +    { +      ps->reductions++; +#ifdef STATS +      bytes_collected = +#endif +      collect_clauses (ps); +#ifdef STATS +      ps->rrecycled += bytes_collected; +#endif +      report (ps, 2, '-'); +    } + +  if (!lcollect) +    inc_lreduce (ps);        /* avoid dead lock */ + +  assert (ps->rhead == ps->resolved); +} + +static void +init_reduce (PS * ps) +{ +  // lreduce = loadded / 2; +  ps->lreduce = 1000; + +  if (ps->lreduce < 100) +    ps->lreduce = 100; + +  if (ps->verbosity) +     fprintf (ps->out, +             "%s\n%sinitial reduction limit %u clauses\n%s\n", +         ps->prefix, ps->prefix, ps->lreduce, ps->prefix); +} + +static unsigned +rng (PS * ps) +{ +  unsigned res = ps->srng; +  ps->srng *= 1664525u; +  ps->srng += 1013904223u; +  NOLOG ( fprintf (ps->out, "%srng () = %u\n", ps->prefix, res)); +  return res; +} + +static unsigned +rrng (PS * ps, unsigned low, unsigned high) +{ +  unsigned long long tmp; +  unsigned res, elements; +  assert (low <= high); +  elements = high - low + 1; +  tmp = rng (ps); +  tmp *= elements; +  tmp >>= 32; +  tmp += low; +  res = tmp; +  NOLOG ( fprintf (ps->out, "%srrng (ps, %u, %u) = %u\n", ps->prefix, low, high, res)); +  assert (low <= res); +  assert (res <= high); +  return res; +} + +static Lit * +decide_phase (PS * ps, Lit * lit) +{ +  Lit * not_lit = NOTLIT (lit); +  Var *v = LIT2VAR (lit); + +  assert (LIT2SGN (lit) > 0); +  if (v->usedefphase) +    { +      if (v->defphase) +    { +      /* assign to TRUE */ +    } +      else +    { +      /* assign to FALSE */ +      lit = not_lit; +    } +    } +  else if (!v->assigned) +    { +#ifdef STATS +      ps->staticphasedecisions++; +#endif +      if (ps->defaultphase == POSPHASE) +    { +      /* assign to TRUE */ +    } +      else if (ps->defaultphase == NEGPHASE) +    { +      /* assign to FALSE */ +      lit = not_lit; +    } +      else if (ps->defaultphase == RNDPHASE) +    { +      /* randomly assign default phase */ +      if (rrng (ps, 1, 2) != 2) +        lit = not_lit; +    } +      else if (*LIT2JWH(lit) <= *LIT2JWH (not_lit)) +    { +      /* assign to FALSE (Jeroslow-Wang says there are more short +       * clauses with negative occurence of this variable, so satisfy +       * those, to minimize BCP) +       */ +      lit = not_lit; +    } +      else +    { +      /* assign to TRUE (... but strictly more positive occurrences) */ +    } +    } +  else +    { +      /* repeat last phase: phase saving heuristic */ + +      if (v->phase) +    { +      /* assign to TRUE (last phase was TRUE as well) */ +    } +      else +    { +      /* assign to FALSE (last phase was FALSE as well) */ +      lit = not_lit; +    } +    } + +  return lit; +} + +static unsigned +gcd (unsigned a, unsigned b) +{ +  unsigned tmp; + +  assert (a); +  assert (b); + +  if (a < b) +    { +      tmp = a; +      a = b; +      b = tmp; +    } + +  while (b) +    { +      assert (a >= b); +      tmp = b; +      b = a % b; +      a = tmp; +    } + +  return a; +} + +static Lit * +rdecide (PS * ps) +{ +  unsigned idx, delta, spread; +  Lit * res; + +  spread = RDECIDE; +  if (rrng (ps, 1, spread) != 2) +    return 0; + +  assert (1 <= ps->max_var); +  idx = rrng (ps, 1, ps->max_var); +  res = int2lit (ps, idx); + +  if (res->val != UNDEF) +    { +      delta = rrng (ps, 1, ps->max_var); +      while (gcd (delta, ps->max_var) != 1) +    delta--; + +      assert (1 <= delta); +      assert (delta <= ps->max_var); + +      do { +    idx += delta; +    if (idx > ps->max_var) +      idx -= ps->max_var; +    res = int2lit (ps, idx); +      } while (res->val != UNDEF); +    } + +#ifdef STATS +  ps->rdecisions++; +#endif +  res = decide_phase (ps, res); +  LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res))); + +  return res; +} + +static Lit * +sdecide (PS * ps) +{ +  Lit *res; +  Rnk *r; + +  for (;;) +    { +      r = htop (ps); +      res = RNK2LIT (r); +      if (res->val == UNDEF) break; +      (void) hpop (ps); +      NOLOG ( fprintf (ps->out, +                      "%shpop %u %u %u\n", +              ps->prefix, r - ps->rnks, +              FLTMANTISSA(r->score), +              FLTEXPONENT(r->score))); +    } + +#ifdef STATS +  ps->sdecisions++; +#endif +  res = decide_phase (ps, res); + +  LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res))); + +  return res; +} + +static Lit * +adecide (PS * ps) +{ +  Lit *lit; +  Var * v; + +  assert (ps->als < ps->alshead); +  assert (!ps->failed_assumption); + +  while (ps->alstail < ps->alshead) +    { +      lit = *ps->alstail++; + +      if (lit->val == FALSE) +    { +      ps->failed_assumption = lit; +      v = LIT2VAR (lit); + +      use_var (ps, v); + +      LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n", +            ps->prefix, LIT2INT (ps->failed_assumption))); +      fanalyze (ps); +      return 0; +    } + +      if (lit->val == TRUE) +    { +      v = LIT2VAR (lit); +      if (v->level > ps->adecidelevel) +        ps->adecidelevel = v->level; +      continue; +    } + +#ifdef STATS +      ps->assumptions++; +#endif +      LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit))); +      ps->adecidelevel = ps->LEVEL + 1; + +      return lit; +    } + +  return 0; +} + +static void +decide (PS * ps) +{ +  Lit * lit; + +  assert (!satisfied (ps)); +  assert (!ps->conflict); + +  if (ps->alstail < ps->alshead && (lit = adecide (ps))) +    ; +  else if (ps->failed_assumption) +    return; +  else if (satisfied (ps)) +    return; +  else if (!(lit = rdecide (ps))) +    lit = sdecide (ps); + +  assert (lit); +  assign_decision (ps, lit); + +  ps->levelsum += ps->LEVEL; +  ps->decisions++; +} + +static int +sat (PS * ps, int l) +{ +  int count = 0, backtracked; + +  if (!ps->conflict) +    bcp (ps); + +  if (ps->conflict) +    backtrack (ps); + +  if (ps->mtcls) +    return PICOSAT_UNSATISFIABLE; + +  if (satisfied (ps)) +    goto SATISFIED; + +  if (ps->lsimplify <= ps->propagations) +    simplify (ps, 0); + +  if (ps->mtcls) +    return PICOSAT_UNSATISFIABLE; + +  if (satisfied (ps)) +    goto SATISFIED; + +  init_restart (ps); + +  if (!ps->lreduce) +    init_reduce (ps); + +  ps->isimplify = ps->fixed; +  backtracked = 0; + +  for (;;) +    { +      if (!ps->conflict) +    bcp (ps); + +      if (ps->conflict) +    { +      incincs (ps); +      backtrack (ps); + +      if (ps->mtcls) +        return PICOSAT_UNSATISFIABLE; +      backtracked = 1; +      continue; +    } + +      if (satisfied (ps)) +    { +SATISFIED: +#ifndef NDEBUG +      original_clauses_satisfied (ps); +      assumptions_satisfied (ps); +#endif +      return PICOSAT_SATISFIABLE; +    } + +      if (backtracked) +    { +      backtracked = 0; +      if (!ps->LEVEL && ps->isimplify < ps->fixed) +        iteration (ps); +    } + +      if (l >= 0 && count >= l)        /* decision limit reached ? */ +    return PICOSAT_UNKNOWN; + +      if (ps->interrupt.function &&        /* external interrupt */ +      count > 0 && !(count % INTERRUPTLIM) && +      ps->interrupt.function (ps->interrupt.state)) +    return PICOSAT_UNKNOWN; + +      if (ps->propagations >= ps->lpropagations)/* propagation limit reached ? */ +    return PICOSAT_UNKNOWN; + +#ifndef NADC +      if (!ps->adodisabled && ps->adoconflicts >= ps->adoconflictlimit) +    { +      assert (bcp_queue_is_empty (ps)); +      return PICOSAT_UNKNOWN; +    } +#endif + +      if (ps->fsimplify < ps->fixed && ps->lsimplify <= ps->propagations) +    { +      simplify (ps, 0); +      if (!bcp_queue_is_empty (ps)) +        continue; +#ifndef NFL +      if (ps->mtcls) +        return PICOSAT_UNSATISFIABLE; + +      if (satisfied (ps)) +        return PICOSAT_SATISFIABLE; + +      assert (!ps->LEVEL); +#endif +    } + +      if (need_to_reduce (ps)) +    reduce (ps, 50); -- 2.33.0