From patchwork Wed Oct 20 09:38:49 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Thorsten Berger X-Patchwork-Id: 12571907 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 82439C433F5 for ; Wed, 20 Oct 2021 09:38:56 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 5F80C6135E for ; Wed, 20 Oct 2021 09:38:56 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229881AbhJTJlJ (ORCPT ); Wed, 20 Oct 2021 05:41:09 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:40920 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229555AbhJTJlI (ORCPT ); Wed, 20 Oct 2021 05:41:08 -0400 Received: from out1.mail.ruhr-uni-bochum.de (out1.mail.ruhr-uni-bochum.de [IPv6:2a05:3e00:8:1001::8693:3595]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id E4B01C06161C for ; Wed, 20 Oct 2021 02:38:53 -0700 (PDT) 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 4HZ5Cc10SWz8S5T; Wed, 20 Oct 2021 11:38:52 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=rub.de; s=mail-2017; t=1634722732; bh=0Hy5/5JvT7i3Zud40JHckKtpwttjzl0l18d3t6ddIHk=; h=Date:Subject:From:To:Cc:References:In-Reply-To:From; b=EFr3tPf4X0sXncocrqAr2RNy4K1mOS0zsKiNJ/xciPe5yvK74XplAHfzfF/tRkwpI bjioHz+lN55xZqP/oM0f+AIU04+i7TdePXZ7hR3fDKkVA/vaYsAoQtWAnLFzh4nv7R eOYsjMhYDxn68BJHInfCD7Tqal22R2JPkwkHJ6Hk= 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 4HZ5Cb6w17z8S5g; Wed, 20 Oct 2021 11:38:51 +0200 (CEST) X-RUB-Notes: Internal origin=IPv6:2a05:3e00:c:1001::8693:2aec X-Envelope-Sender: Received: from mail2.mail.ruhr-uni-bochum.de (mail2.mail.ruhr-uni-bochum.de [IPv6:2a05:3e00:c:1001::8693:2aec]) by out1.mail.ruhr-uni-bochum.de (Postfix mi-int) with ESMTP id 4HZ5Cb4PzBz8S5Q; Wed, 20 Oct 2021 11:38:51 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.1 at mx1.mail.ruhr-uni-bochum.de Received: from [192.168.188.22] (unknown [5.63.49.65]) by mail2.mail.ruhr-uni-bochum.de (Postfix) with ESMTPSA id 4HZ5Cb0hmhzDgyl; Wed, 20 Oct 2021 11:38:51 +0200 (CEST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.0 at mail2.mail.ruhr-uni-bochum.de Message-ID: Date: Wed, 20 Oct 2021 11:38:49 +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 04/12] Add picosat.c (3/3) Content-Language: en-US From: Thorsten Berger To: linux-kbuild@vger.kernel.org Cc: "Luis R. Rodriguez" , deltaone@debian.org, phayax@gmail.com, Eugene Groshev , Sarah Nadi , Mel Gorman , "Luis R. Rodriguez" References: In-Reply-To: Precedence: bulk List-ID: X-Mailing-List: linux-kbuild@vger.kernel.org Co-developed-by: Patrick Franz Signed-off-by: Patrick Franz Co-developed-by: Ibrahim Fayaz Signed-off-by: Ibrahim Fayaz Reviewed-by: Luis Chamberlain Tested-by: Evgeny Groshev Suggested-by: Sarah Nadi Suggested-by: Thorsten Berger Signed-off-by: Thorsten Berger ---  scripts/kconfig/picosat.c | 2502 +++++++++++++++++++++++++++++++++++++  1 file changed, 2502 insertions(+) diff --git a/scripts/kconfig/picosat.c b/scripts/kconfig/picosat.c index 0a6eb3d5a45d..76db7ae0028a 100644 --- a/scripts/kconfig/picosat.c +++ b/scripts/kconfig/picosat.c @@ -5998,3 +5998,2505 @@ sat (PS * ps, int l)          if (need_to_reduce (ps))      reduce (ps, 50); + +      if (ps->conflicts >= ps->lrestart && ps->LEVEL > 2) +    restart (ps); + +      decide (ps); +      if (ps->failed_assumption) +    return PICOSAT_UNSATISFIABLE; +      count++; +    } +} + +static void +rebias (PS * ps) +{ +  Cls ** p, * c; +  Var * v; + +  for (v = ps->vars + 1; v <= ps->vars + ps->max_var; v++) +    v->assigned = 0; + +  memset (ps->jwh, 0, 2 * (ps->max_var + 1) * sizeof *ps->jwh); + +  for (p = ps->oclauses; p < ps->ohead; p++) +    { +      c = *p; + +      if (!c) +    continue; + +      if (c->learned) +    continue; + +      incjwh (ps, c); +    } +} + +#ifdef TRACE + +static unsigned +core (PS * ps) +{ +  unsigned idx, prev, this, delta, i, lcore, vcore; +  unsigned *stack, *shead, *eos; +  Lit **q, **eol, *lit; +  Cls *c, *reason; +  Znt *p, byte; +  Zhn *zhain; +  Var *v; + +  assert (ps->trace); + +  assert (ps->mtcls || ps->failed_assumption); +  if (ps->ocore >= 0) +    return ps->ocore; + +  lcore = ps->ocore = vcore = 0; + +  stack = shead = eos = 0; +  ENLARGE (stack, shead, eos); + +  if (ps->mtcls) +    { +      idx = CLS2IDX (ps->mtcls); +      *shead++ = idx; +    } +  else +    { +      assert (ps->failed_assumption); +      v = LIT2VAR (ps->failed_assumption); +      reason = v->reason; +      assert (reason); +      idx = CLS2IDX (reason); +      *shead++ = idx; +    } + +  while (shead > stack) +    { +      idx = *--shead; +      zhain = IDX2ZHN (idx); + +      if (zhain) +    { +      if (zhain->core) +        continue; + +      zhain->core = 1; +      lcore++; + +      c = IDX2CLS (idx); +      if (c) +        { +          assert (!c->core); +          c->core = 1; +        } + +      i = 0; +      delta = 0; +      prev = 0; +      for (p = zhain->znt; (byte = *p); p++, i += 7) +        { +          delta |= (byte & 0x7f) << i; +          if (byte & 0x80) +        continue; + +          this = prev + delta; +          assert (prev < this);    /* no overflow */ + +          if (shead == eos) +        ENLARGE (stack, shead, eos); +          *shead++ = this; + +          prev = this; +          delta = 0; +          i = -7; +        } +    } +      else +    { +      c = IDX2CLS (idx); + +      assert (c); +      assert (!c->learned); + +      if (c->core) +        continue; + +      c->core = 1; +      ps->ocore++; + +      eol = end_of_lits (c); +      for (q = c->lits; q < eol; q++) +        { +          lit = *q; +          v = LIT2VAR (lit); +          if (v->core) +        continue; + +          v->core = 1; +          vcore++; + +          if (!ps->failed_assumption) continue; +          if (lit != ps->failed_assumption) continue; + +          reason = v->reason; +          if (!reason) continue; +          if (reason->core) continue; + +          idx = CLS2IDX (reason); +          if (shead == eos) +        ENLARGE (stack, shead, eos); +          *shead++ = idx; +        } +    } +    } + +  DELETEN (stack, eos - stack); + +  if (ps->verbosity) +     fprintf (ps->out, +         "%s%u core variables out of %u (%.1f%%)\n" +         "%s%u core original clauses out of %u (%.1f%%)\n" +         "%s%u core learned clauses out of %u (%.1f%%)\n", +         ps->prefix, vcore, ps->max_var, PERCENT (vcore, ps->max_var), +         ps->prefix, ps->ocore, ps->oadded, PERCENT (ps->ocore, ps->oadded), +         ps->prefix, lcore, ps->ladded, PERCENT (lcore, ps->ladded)); + +  return ps->ocore; +} + +static void +trace_lits (PS * ps, Cls * c, FILE * file) +{ +  Lit **p, **eol = end_of_lits (c); + +  assert (c); +  assert (c->core); + +  for (p = c->lits; p < eol; p++) +    fprintf (file, "%d ", LIT2INT (*p)); + +  fputc ('0', file); +} + +static void +write_idx (PS * ps, unsigned idx, FILE * file) +{ +  fprintf (file, "%ld", EXPORTIDX (idx)); +} + +static void +trace_clause (PS * ps, unsigned idx, Cls * c, FILE * file, int fmt) +{ +  assert (c); +  assert (c->core); +  assert (fmt == RUP_TRACE_FMT || !c->learned); +  assert (CLS2IDX (c) == idx); + +  if (fmt != RUP_TRACE_FMT) +    { +      write_idx (ps, idx, file); +      fputc (' ', file); +    } + +  trace_lits (ps, c, file); + +  if (fmt != RUP_TRACE_FMT) +    fputs (" 0", file); + +  fputc ('\n', file); +} + +static void +trace_zhain (PS * ps, unsigned idx, Zhn * zhain, FILE * file, int fmt) +{ +  unsigned prev, this, delta, i; +  Znt *p, byte; +  Cls * c; + +  assert (zhain); +  assert (zhain->core); + +  write_idx (ps, idx, file); +  fputc (' ', file); + +  if (fmt == EXTENDED_TRACECHECK_TRACE_FMT) +    { +      c = IDX2CLS (idx); +      assert (c); +      trace_lits (ps, c, file); +    } +  else +    { +      assert (fmt == COMPACT_TRACECHECK_TRACE_FMT); +      putc ('*', file); +    } + +  i = 0; +  delta = 0; +  prev = 0; + +  for (p = zhain->znt; (byte = *p); p++, i += 7) +    { +      delta |= (byte & 0x7f) << i; +      if (byte & 0x80) +    continue; + +      this = prev + delta; + +      putc (' ', file); +      write_idx (ps, this, file); + +      prev = this; +      delta = 0; +      i = -7; +    } + +  fputs (" 0\n", file); +} + +static void +write_core (PS * ps, FILE * file) +{ +  Lit **q, **eol; +  Cls **p, *c; + +  fprintf (file, "p cnf %u %u\n", ps->max_var, core (ps)); + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; + +      if (!c || c->learned || !c->core) +    continue; + +      eol = end_of_lits (c); +      for (q = c->lits; q < eol; q++) +    fprintf (file, "%d ", LIT2INT (*q)); + +      fputs ("0\n", file); +    } +} + +#endif + +static void +write_trace (PS * ps, FILE * file, int fmt) +{ +#ifdef TRACE +  Cls *c, ** p; +  Zhn *zhain; +  unsigned i; + +  core (ps); + +  if (fmt == RUP_TRACE_FMT) +    { +      ps->rupvariables = picosat_variables (ps), +      ps->rupclauses = picosat_added_original_clauses (ps); +      write_rup_header (ps, file); +    } + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; + +      if (ps->oclauses <= p && p < ps->eoo) +    { +      i = OIDX2IDX (p - ps->oclauses); +      assert (!c || CLS2IDX (c) == i); +    } +      else +    { +          assert (ps->lclauses <= p && p < ps->EOL); +      i = LIDX2IDX (p - ps->lclauses); +    } + +      zhain = IDX2ZHN (i); + +      if (zhain) +    { +      if (zhain->core) +        { +          if (fmt == RUP_TRACE_FMT) +        trace_clause (ps,i, c, file, fmt); +          else +        trace_zhain (ps, i, zhain, file, fmt); +        } +    } +      else if (c) +    { +      if (fmt != RUP_TRACE_FMT && c) +        { +          if (c->core) +        trace_clause (ps, i, c, file, fmt); +        } +    } +    } +#else +  (void) file; +  (void) fmt; +  (void) ps; +#endif +} + +static void +write_core_wrapper (PS * ps, FILE * file, int fmt) +{ +  (void) fmt; +#ifdef TRACE +  write_core (ps, file); +#else +  (void) ps; +  (void) file; +#endif +} + +static Lit * +import_lit (PS * ps, int lit, int nointernal) +{ +  Lit * res; +  Var * v; + +  ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal"); +  ABORTIF (abs (lit) > (int) ps->max_var && ps->CLS != ps->clshead, +           "API usage: new variable index after 'picosat_push'"); + +  if (abs (lit) <= (int) ps->max_var) +    { +      res = int2lit (ps, lit); +      v = LIT2VAR (res); +      if (nointernal && v->internal) +    ABORT ("API usage: trying to import invalid literal"); +      else if (!nointernal && !v->internal) +    ABORT ("API usage: trying to import invalid context"); +    } +  else +    { +      while (abs (lit) > (int) ps->max_var) +    inc_max_var (ps); +      res = int2lit (ps, lit); +    } + +  return res; +} + +#ifdef TRACE +static void +reset_core (PS * ps) +{ +  Cls ** p, * c; +  Zhn ** q, * z; +  unsigned i; + +  for (i = 1; i <= ps->max_var; i++) +    ps->vars[i].core = 0; + +  for (p = SOC; p != EOC; p = NXC (p)) +    if ((c = *p)) +      c->core = 0; + +  for (q = ps->zhains; q != ps->zhead; q++) +    if ((z = *q)) +      z->core = 0; + +  ps->ocore = -1; +} +#endif + +static void +reset_assumptions (PS * ps) +{ +  Lit ** p; + +  ps->failed_assumption = 0; + +  if (ps->extracted_all_failed_assumptions) +    { +      for (p = ps->als; p < ps->alshead; p++) +    LIT2VAR (*p)->failed = 0; + +      ps->extracted_all_failed_assumptions = 0; +    } + +  ps->alstail = ps->alshead = ps->als; +  ps->adecidelevel = 0; +} + +static void +check_ready (PS * ps) +{ +  ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized"); +} + +static void +check_sat_state (PS * ps) +{ +  ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state"); +} + +static void +check_unsat_state (PS * ps) +{ +  ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state"); +} + +static void +check_sat_or_unsat_or_unknown_state (PS * ps) +{ +  ABORTIF (ps->state != SAT && ps->state != UNSAT && ps->state != UNKNOWN, +           "API usage: expected to be in SAT, UNSAT, or UNKNOWN state"); +} + +static void +reset_partial (PS * ps) +{ +  unsigned idx; +  if (!ps->partial) +    return; +  for (idx = 1; idx <= ps->max_var; idx++) +    ps->vars[idx].partial = 0; +  ps->partial = 0; +} + +static void +reset_incremental_usage (PS * ps) +{ +  unsigned num_non_false; +  Lit * lit, ** q; + +  check_sat_or_unsat_or_unknown_state (ps); + +  LOG ( fprintf (ps->out, "%sRESET incremental usage\n", ps->prefix)); + +  if (ps->LEVEL) +    undo (ps, 0); + +  reset_assumptions (ps); + +  if (ps->conflict) +    { +      num_non_false = 0; +      for (q = ps->conflict->lits; q < end_of_lits (ps->conflict); q++) +    { +      lit = *q; +      if (lit->val != FALSE) +        num_non_false++; +    } + +      // assert (num_non_false >= 2); // TODO: why this assertion? +#ifdef NO_BINARY_CLAUSES +      if (ps->conflict == &ps->cimpl) +    resetcimpl (ps); +#endif +#ifndef NADC +      if (ps->conflict == ps->adoconflict) +    resetadoconflict (ps); +#endif +      ps->conflict = 0; +    } + +#ifdef TRACE +  reset_core (ps); +#endif + +  reset_partial (ps); + +  ps->saved_flips = ps->flips; +  ps->min_flipped = UINT_MAX; +  ps->saved_max_var = ps->max_var; + +  ps->state = READY; +} + +static void +enter (PS * ps) +{ +  if (ps->nentered++) +    return; + +  check_ready (ps); +  ps->entered = picosat_time_stamp (); +} + +static void +leave (PS * ps) +{ +  assert (ps->nentered); +  if (--ps->nentered) +    return; + +  sflush (ps); +} + +static void +check_trace_support_and_execute (PS * ps, +                                 FILE * file, +                 void (*f)(PS*,FILE*,int), int fmt) +{ +  check_ready (ps); +  check_unsat_state (ps); +#ifdef TRACE +  ABORTIF (!ps->trace, "API usage: tracing disabled"); +  enter (ps); +  f (ps, file, fmt); +  leave (ps); +#else +  (void) file; +  (void) fmt; +  (void) f; +  ABORT ("compiled without trace support"); +#endif +} + +static void +extract_all_failed_assumptions (PS * ps) +{ +  Lit ** p, ** eol; +  Var * v, * u; +  int pos; +  Cls * c; + +  assert (!ps->extracted_all_failed_assumptions); + +  assert (ps->failed_assumption); +  assert (ps->mhead == ps->marked); + +  if (ps->marked == ps->eom) +    ENLARGE (ps->marked, ps->mhead, ps->eom); + +  v = LIT2VAR (ps->failed_assumption); +  mark_var (ps, v); +  pos = 0; + +  while (pos < ps->mhead - ps->marked) +    { +      v = ps->marked[pos++]; +      assert (v->mark); +      c = var2reason (ps, v); +      if (!c) +    continue; +      eol = end_of_lits (c); +      for (p = c->lits; p < eol; p++) +    { +      u = LIT2VAR (*p); +      if (!u->mark) +        mark_var (ps, u); +    } +#ifdef NO_BINARY_CLAUSES +      if (c == &ps->impl) +    resetimpl (ps); +#endif +    } + +  for (p = ps->als; p < ps->alshead; p++) +    { +      u = LIT2VAR (*p); +      if (!u->mark) continue; +      u->failed = 1; +      LOG ( fprintf (ps->out, +                     "%sfailed assumption %d\n", +             ps->prefix, LIT2INT (*p))); +    } + +  while (ps->mhead > ps->marked) +    (*--ps->mhead)->mark = 0; + +  ps->extracted_all_failed_assumptions = 1; +} + +const char * +picosat_copyright (void) +{ +  return "Copyright (c) 2006 - 2014 Armin Biere JKU Linz"; +} + +PicoSAT * +picosat_init (void) +{ +  return init (0, 0, 0, 0); +} + +PicoSAT * +picosat_minit (void * pmgr, +           picosat_malloc pnew, +           picosat_realloc presize, +           picosat_free pfree) +{ +  ABORTIF (!pnew, "API usage: zero 'picosat_malloc' argument"); +  ABORTIF (!presize, "API usage: zero 'picosat_realloc' argument"); +  ABORTIF (!pfree, "API usage: zero 'picosat_free' argument"); +  return init (pmgr, pnew, presize, pfree); +} + + +void +picosat_adjust (PS * ps, int new_max_var) +{ +  unsigned new_size_vars; + +  ABORTIF (abs (new_max_var) > (int) ps->max_var && ps->CLS != ps->clshead, +           "API usage: adjusting variable index after 'picosat_push'"); +  enter (ps); + +  new_max_var = abs (new_max_var); +  new_size_vars = new_max_var + 1; + +  if (ps->size_vars < new_size_vars) +    enlarge (ps, new_size_vars); + +  while (ps->max_var < (unsigned) new_max_var) +    inc_max_var (ps); + +  leave (ps); +} + +int +picosat_inc_max_var (PS * ps) +{ +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  inc_max_var (ps); + +  if (ps->measurealltimeinlib) +    leave (ps); + +  return ps->max_var; +} + +int +picosat_context (PS * ps) +{ +  return ps->clshead == ps->CLS ? 0 : LIT2INT (ps->clshead[-1]); +} + +int +picosat_push (PS * ps) +{ +  int res; +  Lit *lit; +  Var * v; + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  if (ps->rils != ps->rilshead) +    { +      res = *--ps->rilshead; +      assert (ps->vars[res].internal); +    } +  else +    { +      inc_max_var (ps); +      res = ps->max_var; +      v = ps->vars + res; +      assert (!v->internal); +      v->internal = 1; +      ps->internals++; +      LOG ( fprintf (ps->out, "%snew internal variable index %d\n", ps->prefix, res)); +    } + +  lit = int2lit (ps, res); + +  if (ps->clshead == ps->eocls) +    ENLARGE (ps->CLS, ps->clshead, ps->eocls); +  *ps->clshead++ = lit; + +  ps->contexts++; + +  LOG ( fprintf (ps->out, "%snew context %d at depth %ld after push\n", +                 ps->prefix, res, (long)(ps->clshead - ps->CLS))); + +  if (ps->measurealltimeinlib) +    leave (ps); + +  return res; +} + +int +picosat_pop (PS * ps) +{ +  Lit * lit; +  int res; +  ABORTIF (ps->CLS == ps->clshead, "API usage: too many 'picosat_pop'"); +  ABORTIF (ps->added != ps->ahead, "API usage: incomplete clause"); + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  assert (ps->CLS < ps->clshead); +  lit = *--ps->clshead; +  LOG ( fprintf (ps->out, "%sclosing context %d at depth %ld after pop\n", +                 ps->prefix, LIT2INT (lit), (long)(ps->clshead - ps->CLS) + 1)); + +  if (ps->cilshead == ps->eocils) +    ENLARGE (ps->cils, ps->cilshead, ps->eocils); +  *ps->cilshead++ = LIT2INT (lit); + +  if (ps->cilshead - ps->cils > MAXCILS) { +    LOG ( fprintf (ps->out, +                  "%srecycling %ld interals with forced simplification\n", +          ps->prefix, (long)(ps->cilshead - ps->cils))); +    simplify (ps, 1); +  } + +  res = picosat_context (ps); +  if (res) +    LOG ( fprintf (ps->out, "%snew context %d at depth %ld after pop\n", +           ps->prefix, res, (long)(ps->clshead - ps->CLS))); +  else +    LOG ( fprintf (ps->out, "%souter most context reached after pop\n", ps->prefix)); + +  if (ps->measurealltimeinlib) +    leave (ps); +   +  return res; +} + +void +picosat_set_verbosity (PS * ps, int new_verbosity_level) +{ +  check_ready (ps); +  ps->verbosity = new_verbosity_level; +} + +void +picosat_set_plain (PS * ps, int new_plain_value) +{ +  check_ready (ps); +  ps->plain = new_plain_value; +} + +int +picosat_enable_trace_generation (PS * ps) +{ +  int res = 0; +  check_ready (ps); +#ifdef TRACE +  ABORTIF (ps->addedclauses, +           "API usage: trace generation enabled after adding clauses"); +  res = ps->trace = 1; +#endif +  return res; +} + +void +picosat_set_incremental_rup_file (PS * ps, FILE * rup_file, int m, int n) +{ +  check_ready (ps); +  assert (!ps->rupstarted); +  ps->rup = rup_file; +  ps->rupvariables = m; +  ps->rupclauses = n; +} + +void +picosat_set_output (PS * ps, FILE * output_file) +{ +  check_ready (ps); +  ps->out = output_file; +} + +void +picosat_measure_all_calls (PS * ps) +{ +  check_ready (ps); +  ps->measurealltimeinlib = 1; +} + +void +picosat_set_prefix (PS * ps, const char * str) +{ +  check_ready (ps); +  new_prefix (ps, str); +} + +void +picosat_set_seed (PS * ps, unsigned s) +{ +  check_ready (ps); +  ps->srng = s; +} + +void +picosat_reset (PS * ps) +{ +  check_ready (ps); +  reset (ps); +} + +int +picosat_add (PS * ps, int int_lit) +{ +  int res = ps->oadded; +  Lit *lit; + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  ABORTIF (ps->rup && ps->rupstarted && ps->oadded >= (unsigned)ps->rupclauses, +           "API usage: adding too many clauses after RUP header written"); +#ifndef NADC +  ABORTIF (ps->addingtoado, +           "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed"); +#endif +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  if (ps->saveorig) +    { +      if (ps->sohead == ps->eoso) +    ENLARGE (ps->soclauses, ps->sohead, ps->eoso); + +      *ps->sohead++ = int_lit; +    } + +  if (int_lit) +    { +      lit = import_lit (ps, int_lit, 1); +      add_lit (ps, lit); +    } +  else +    simplify_and_add_original_clause (ps); + +  if (ps->measurealltimeinlib) +    leave (ps); + +  return res; +} + +int +picosat_add_arg (PS * ps, ...) +{ +  int lit; +  va_list ap; +  va_start (ap, ps); +  while ((lit = va_arg (ap, int))) +    (void) picosat_add (ps, lit); +  va_end (ap); +  return picosat_add (ps, 0); +} + +int +picosat_add_lits (PS * ps, int * lits) +{ +  const int * p; +  int lit; +  for (p = lits; (lit = *p); p++) +    (void) picosat_add (ps, lit); +  return picosat_add (ps, 0); +} + +void +picosat_add_ado_lit (PS * ps, int external_lit) +{ +#ifndef NADC +  Lit * internal_lit; + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  ABORTIF (!ps->addingtoado && ps->ahead > ps->added, +           "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed"); + +  if (external_lit) +    { +      ps->addingtoado = 1; +      internal_lit = import_lit (ps, external_lit, 1); +      add_lit (ps, internal_lit); +    } +  else +    { +      ps->addingtoado = 0; +      add_ado (ps); +    } +  if (ps->measurealltimeinlib) +    leave (ps); +#else +  (void) ps; +  (void) external_lit; +  ABORT ("compiled without all different constraint support"); +#endif +} + +static void +assume (PS * ps, Lit * lit) +{ +  if (ps->alshead == ps->eoals) +    { +      assert (ps->alstail == ps->als); +      ENLARGE (ps->als, ps->alshead, ps->eoals); +      ps->alstail = ps->als; +    } + +  *ps->alshead++ = lit; +  LOG ( fprintf (ps->out, "%sassumption %d\n", ps->prefix, LIT2INT (lit))); +} + +static void +assume_contexts (PS * ps) +{ +  Lit ** p; +  if (ps->als != ps->alshead) +    return; +  for (p = ps->CLS; p != ps->clshead; p++) +    assume (ps, *p); +} + +#ifndef RCODE +static const char * enumstr (int i) { +  int last = i % 10; +  if (last == 1) return "st"; +  if (last == 2) return "nd"; +  if (last == 3) return "rd"; +  return "th"; +} +#endif + +static int +tderef (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; + +  assert (abs (int_lit) <= (int) ps->max_var); + +  lit = int2lit (ps, int_lit); + +  v = LIT2VAR (lit); +  if (v->level > 0) +    return 0; + +  if (lit->val == TRUE) +    return 1; + +  if (lit->val == FALSE) +    return -1; + +  return 0; +} + +static int +pderef (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; + +  assert (abs (int_lit) <= (int) ps->max_var); + +  v = ps->vars + abs (int_lit); +  if (!v->partial) +    return 0; + +  lit = int2lit (ps, int_lit); + +  if (lit->val == TRUE) +    return 1; + +  if (lit->val == FALSE) +    return -1; + +  return 0; +} + +static void +minautarky (PS * ps) +{ +  unsigned * occs, maxoccs, tmpoccs, npartial; +  int * p, * c, lit, best, val; +#ifdef LOGGING +  int tl; +#endif + +  assert (!ps->partial); + +  npartial = 0; + +  NEWN (occs, 2*ps->max_var + 1); +  CLRN (occs, 2*ps->max_var + 1); +  occs += ps->max_var; +  for (p = ps->soclauses; p < ps->sohead; p++) +    occs[*p]++; +  assert (occs[0] == ps->oadded); + +  for (c = ps->soclauses; c < ps->sohead; c = p + 1) +    { +#ifdef LOGGING +      tl = 0; +#endif +      best = 0; +      maxoccs = 0; +      for (p = c; (lit = *p); p++) +    { +      val = tderef (ps, lit); +      if (val < 0) +        continue; +      if (val > 0) +        { +#ifdef LOGGING +          tl = 1; +#endif +          best = lit; +          maxoccs = occs[lit]; +        } + +      val = pderef (ps, lit); +      if (val > 0) +        break; +      if (val < 0) +        continue; +      val = int2lit (ps, lit)->val; +      assert (val); +      if (val < 0) +        continue; +      tmpoccs = occs[lit]; +      if (best && tmpoccs <= maxoccs) +        continue; +      best = lit; +      maxoccs = tmpoccs; +    } +      if (!lit) +    { +      assert (best); +      LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n", +           ps->prefix, best, maxoccs, tl ? " (top)" : "")); +      ps->vars[abs (best)].partial = 1; +      npartial++; +    } +      for (p = c; (lit = *p); p++) +    { +      assert (occs[lit] > 0); +      occs[lit]--; +    } +    } +  occs -= ps->max_var; +  DELETEN (occs, 2*ps->max_var + 1); +  ps->partial = 1; + +  if (ps->verbosity) +     fprintf (ps->out, +      "%sautarky of size %u out of %u satisfying all clauses (%.1f%%)\n", +      ps->prefix, npartial, ps->max_var, PERCENT (npartial, ps->max_var)); +} + +void +picosat_assume (PS * ps, int int_lit) +{ +  Lit *lit; + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  assume_contexts (ps); +  lit = import_lit (ps, int_lit, 1); +  assume (ps, lit); + +  if (ps->measurealltimeinlib) +    leave (ps); +} + +int +picosat_sat (PS * ps, int l) +{ +  int res; +  char ch; + +  enter (ps); + +  ps->calls++; +  LOG ( fprintf (ps->out, "%sSTART call %u\n", ps->prefix, ps->calls)); + +  if (ps->added < ps->ahead) +    { +#ifndef NADC +      if (ps->addingtoado) +    ABORT ("API usage: incomplete all different constraint"); +      else +#endif +    ABORT ("API usage: incomplete clause"); +    } + +  if (ps->state != READY) +    reset_incremental_usage (ps); + +  assume_contexts (ps); + +  res = sat (ps, l); + +  assert (ps->state == READY); + +  switch (res) +    { +    case PICOSAT_UNSATISFIABLE: +      ch = '0'; +      ps->state = UNSAT; +      break; +    case PICOSAT_SATISFIABLE: +      ch = '1'; +      ps->state = SAT; +      break; +    default: +      ch = '?'; +      ps->state = UNKNOWN; +      break; +    } + +  if (ps->verbosity) +    { +      report (ps, 1, ch); +      rheader (ps); +    } + +  leave (ps); +  LOG ( fprintf (ps->out, "%sEND call %u result %d\n", ps->prefix, ps->calls, res)); + +  ps->last_sat_call_result = res; + +  return res; +} + +int +picosat_res (PS * ps) +{ +  return ps->last_sat_call_result; +} + +int +picosat_deref (PS * ps, int int_lit) +{ +  Lit *lit; + +  check_ready (ps); +  check_sat_state (ps); +  ABORTIF (!int_lit, "API usage: can not deref zero literal"); +  ABORTIF (ps->mtcls, "API usage: deref after empty clause generated"); + +#ifdef STATS +  ps->derefs++; +#endif + +  if (abs (int_lit) > (int) ps->max_var) +    return 0; + +  lit = int2lit (ps, int_lit); + +  if (lit->val == TRUE) +    return 1; + +  if (lit->val == FALSE) +    return -1; + +  return 0; +} + +int +picosat_deref_toplevel (PS * ps, int int_lit) +{ +  check_ready (ps); +  ABORTIF (!int_lit, "API usage: can not deref zero literal"); + +#ifdef STATS +  ps->derefs++; +#endif +  if (abs (int_lit) > (int) ps->max_var) +    return 0; + +  return tderef (ps, int_lit); +} + +int +picosat_inconsistent (PS * ps) +{ +  check_ready (ps); +  return ps->mtcls != 0; +} + +int +picosat_corelit (PS * ps, int int_lit) +{ +  check_ready (ps); +  check_unsat_state (ps); +  ABORTIF (!int_lit, "API usage: zero literal can not be in core"); + +  assert (ps->mtcls || ps->failed_assumption); + +#ifdef TRACE +  { +    int res = 0; +    ABORTIF (!ps->trace, "tracing disabled"); +    if (ps->measurealltimeinlib) +      enter (ps); +    core (ps); +    if (abs (int_lit) <= (int) ps->max_var) +      res = ps->vars[abs (int_lit)].core; +    assert (!res || ps->failed_assumption || ps->vars[abs (int_lit)].used); +    if (ps->measurealltimeinlib) +      leave (ps); +    return res; +  } +#else +  ABORT ("compiled without trace support"); +  return 0; +#endif +} + +int +picosat_coreclause (PS * ps, int ocls) +{ +  check_ready (ps); +  check_unsat_state (ps); + +  ABORTIF (ocls < 0, "API usage: negative original clause index"); +  ABORTIF (ocls >= (int)ps->oadded, "API usage: original clause index exceeded"); + +  assert (ps->mtcls || ps->failed_assumption); + +#ifdef TRACE +  { +    Cls ** clsptr, * c; +    int res  = 0; + +    ABORTIF (!ps->trace, "tracing disabled"); +    if (ps->measurealltimeinlib) +      enter (ps); +    core (ps); +    clsptr = ps->oclauses + ocls; +    assert (clsptr < ps->ohead); +    c = *clsptr; +    if (c) +      res = c->core; +    if (ps->measurealltimeinlib) +      leave (ps); + +    return res; +  } +#else +  ABORT ("compiled without trace support"); +  return 0; +#endif +} + +int +picosat_failed_assumption (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; +  ABORTIF (!int_lit, "API usage: zero literal as assumption"); +  check_ready (ps); +  check_unsat_state (ps); +  if (ps->mtcls) +    return 0; +  assert (ps->failed_assumption); +  if (abs (int_lit) > (int) ps->max_var) +    return 0; +  if (!ps->extracted_all_failed_assumptions) +    extract_all_failed_assumptions (ps); +  lit = import_lit (ps, int_lit, 1); +  v = LIT2VAR (lit); +  return v->failed; +} + +int +picosat_failed_context (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; +  ABORTIF (!int_lit, "API usage: zero literal as context"); +  ABORTIF (abs (int_lit) > (int) ps->max_var, "API usage: invalid context"); +  check_ready (ps); +  check_unsat_state (ps); +  assert (ps->failed_assumption); +  if (!ps->extracted_all_failed_assumptions) +    extract_all_failed_assumptions (ps); +  lit = import_lit (ps, int_lit, 0); +  v = LIT2VAR (lit); +  return v->failed; +} + +const int * +picosat_failed_assumptions (PS * ps) +{ +  Lit ** p, * lit; +  Var * v; +  int ilit; + +  ps->falshead = ps->fals; +  check_ready (ps); +  check_unsat_state (ps); +  if (!ps->mtcls) +    { +      assert (ps->failed_assumption); +      if (!ps->extracted_all_failed_assumptions) +    extract_all_failed_assumptions (ps); + +      for (p = ps->als; p < ps->alshead; p++) +    { +      lit = *p; +      v = LIT2VAR (*p); +      if (!v->failed) +        continue; +      ilit = LIT2INT (lit); +      if (ps->falshead == ps->eofals) +        ENLARGE (ps->fals, ps->falshead, ps->eofals); +      *ps->falshead++ = ilit; +    } +    } +  if (ps->falshead == ps->eofals) +    ENLARGE (ps->fals, ps->falshead, ps->eofals); +  *ps->falshead++ = 0; +  return ps->fals; +} + +const int * +picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fix) +{ +  int i, j, ilit, len, nwork, * work, res; +  signed char * redundant; +  Lit ** p, * lit; +  int failed; +  Var * v; +#ifndef NDEBUG +  int oldlen; +#endif +#ifndef RCODE +  int norig = ps->alshead - ps->als; +#endif + +  check_ready (ps); +  check_unsat_state (ps); +  len = 0; +  if (!ps->mtcls) +    { +      assert (ps->failed_assumption); +      if (!ps->extracted_all_failed_assumptions) +    extract_all_failed_assumptions (ps); + +      for (p = ps->als; p < ps->alshead; p++) +    if (LIT2VAR (*p)->failed) +      len++; +    } + +  if (ps->mass) +    DELETEN (ps->mass, ps->szmass); +  ps->szmass = len + 1; +  NEWN (ps->mass, ps->szmass); + +  i = 0; +  for (p = ps->als; p < ps->alshead; p++) +    { +      lit = *p; +      v = LIT2VAR (lit); +      if (!v->failed) +    continue; +      ilit = LIT2INT (lit); +      assert (i < len); +      ps->mass[i++] = ilit; +    } +  assert (i == len); +  ps->mass[i] = 0; +  if (ps->verbosity) +     fprintf (ps->out, +      "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n", +      ps->prefix, len, norig, PERCENT (len, norig)); +  if (cb) +    cb (s, ps->mass); + +  nwork = len; +  NEWN (work, nwork); +  for (i = 0; i < len; i++) +    work[i] = ps->mass[i]; + +  NEWN (redundant, nwork); +  CLRN (redundant, nwork); + +  for (i = 0; i < nwork; i++) +    { +      if (redundant[i]) +    continue; + +      if (ps->verbosity > 1) +     fprintf (ps->out, +             "%strying to drop %d%s assumption %d\n", +         ps->prefix, i, enumstr (i), work[i]); +      for (j = 0; j < nwork; j++) +    { +      if (i == j) continue; +      if (j < i && fix) continue; +      if (redundant[j]) continue; +      picosat_assume (ps, work[j]); +    } + +      res = picosat_sat (ps, -1); +      if (res == 10) +    { +      if (ps->verbosity > 1) +         fprintf (ps->out, +             "%sfailed to drop %d%s assumption %d\n", +             ps->prefix, i, enumstr (i), work[i]); + +      if (fix) +        { +          picosat_add (ps, work[i]); +          picosat_add (ps, 0); +        } +    } +      else +    { +      assert (res == 20); +      if (ps->verbosity > 1) +         fprintf (ps->out, +             "%ssuceeded to drop %d%s assumption %d\n", +             ps->prefix, i, enumstr (i), work[i]); +      redundant[i] = 1; +      for (j = 0; j < nwork; j++) +        { +          failed = picosat_failed_assumption (ps, work[j]); +          if (j <= i) +        { +          assert ((j < i && fix) || redundant[j] == !failed); +          continue; +        } + +          if (!failed) +        { +          redundant[j] = -1; +          if (ps->verbosity > 1) +             fprintf (ps->out, +                 "%salso suceeded to drop %d%s assumption %d\n", +                 ps->prefix, j, enumstr (j), work[j]); +        } +        } + +#ifndef NDEBUG +        oldlen = len; +#endif +        len = 0; +        for (j = 0; j < nwork; j++) +          if (!redundant[j]) +        ps->mass[len++] = work[j]; +        ps->mass[len] = 0; +        assert (len < oldlen); + +        if (fix) +          { +        picosat_add (ps, -work[i]); +        picosat_add (ps, 0); +          } + +#ifndef NDEBUG +        for (j = 0; j <= i; j++) +          assert (redundant[j] >= 0); +#endif +        for (j = i + 1; j < nwork; j++) +          { +        if (redundant[j] >= 0) +          continue; + +        if (fix) +          { +            picosat_add (ps, -work[j]); +            picosat_add (ps, 0); +          } + +        redundant[j] = 1; +          } + +        if (ps->verbosity) +           fprintf (ps->out, +    "%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n", +        ps->prefix, len, norig, PERCENT (len, norig)); +        if (cb) +          cb (s, ps->mass); +    } +    } + +  DELETEN (work, nwork); +  DELETEN (redundant, nwork); + +  if (ps->verbosity) +    { +       fprintf (ps->out, "%sreinitializing unsat state\n", ps->prefix); +      fflush (ps->out); +    } + +  for (i = 0; i < len; i++) +    picosat_assume (ps, ps->mass[i]); + +#ifndef NDEBUG +  res = +#endif +  picosat_sat (ps, -1); +  assert (res == 20); + +  if (!ps->mtcls) +    { +      assert (!ps->extracted_all_failed_assumptions); +      extract_all_failed_assumptions (ps); +    } + +  return ps->mass; +} + +static const int * +mss (PS * ps, int * a, int size) +{ +  int i, j, k, res; + +  assert (!ps->mtcls); + +  if (ps->szmssass) +    DELETEN (ps->mssass, ps->szmssass); + +  ps->szmssass = 0; +  ps->mssass = 0; + +  ps->szmssass = size + 1; +  NEWN (ps->mssass, ps->szmssass); + +  LOG ( fprintf (ps->out, "%ssearch MSS over %d assumptions\n", ps->prefix, size)); + +  k = 0; +  for (i = k; i < size; i++) +    { +      for (j = 0; j < k; j++) +    picosat_assume (ps, ps->mssass[j]); + +      LOG ( fprintf (ps->out, +             "%strying to add assumption %d to MSS : %d\n", +         ps->prefix, i, a[i])); + +      picosat_assume (ps, a[i]); + +      res = picosat_sat (ps, -1); +      if (res == 10) +    { +      LOG ( fprintf (ps->out, +         "%sadding assumption %d to MSS : %d\n", ps->prefix, i, a[i])); + +      ps->mssass[k++] = a[i]; + +      for (j = i + 1; j < size; j++) +        { +          if (picosat_deref (ps, a[j]) <= 0) +        continue; + +          LOG ( fprintf (ps->out, +             "%salso adding assumption %d to MSS : %d\n", +             ps->prefix, j, a[j])); + +          ps->mssass[k++] = a[j]; + +          if (++i != j) +        { +          int tmp = a[i]; +          a[i] = a[j]; +          a[j] = tmp; +        } +        } +    } +      else +    { +      assert (res == 20); + +      LOG ( fprintf (ps->out, +         "%signoring assumption %d in MSS : %d\n", ps->prefix, i, a[i])); +    } +    } +  ps->mssass[k] = 0; +  LOG ( fprintf (ps->out, "%sfound MSS of size %d\n", ps->prefix, k)); + +  return ps->mssass; +} + +static void +reassume (PS * ps, const int * a, int size) +{ +  int i; +  LOG ( fprintf (ps->out, "%sreassuming all assumptions\n", ps->prefix)); +  for (i = 0; i < size; i++) +    picosat_assume (ps, a[i]); +} + +const int * +picosat_maximal_satisfiable_subset_of_assumptions (PS * ps) +{ +  const int * res; +  int i, *a, size; + +  ABORTIF (ps->mtcls, +           "API usage: CNF inconsistent (use 'picosat_inconsistent')"); + +  enter (ps); + +  size = ps->alshead - ps->als; +  NEWN (a, size); + +  for (i = 0; i < size; i++) +    a[i] = LIT2INT (ps->als[i]); + +  res = mss (ps, a, size); +  reassume (ps, a, size); + +  DELETEN (a, size); + +  leave (ps); + +  return res; +} + +static void +check_mss_flags_clean (PS * ps) +{ +#ifndef NDEBUG +  unsigned i; +  for (i = 1; i <= ps->max_var; i++) +    { +      assert (!ps->vars[i].msspos); +      assert (!ps->vars[i].mssneg); +    } +#else +  (void) ps; +#endif +} + +static void +push_mcsass (PS * ps, int lit) +{ +  if (ps->nmcsass == ps->szmcsass) +    { +      ps->szmcsass = ps->szmcsass ? 2*ps->szmcsass : 1; +      RESIZEN (ps->mcsass, ps->nmcsass, ps->szmcsass); +    } + +  ps->mcsass[ps->nmcsass++] = lit; +} + +static const int * +next_mss (PS * ps, int mcs) +{ +  int i, *a, size, mssize, mcsize, lit, inmss; +  const int * res, * p; +  Var * v; + +  if (ps->mtcls) return 0; + +  check_mss_flags_clean (ps); + +  if (mcs && ps->mcsass) +    { +      DELETEN (ps->mcsass, ps->szmcsass); +      ps->nmcsass = ps->szmcsass = 0; +      ps->mcsass = 0; +    } + +  size = ps->alshead - ps->als; +  NEWN (a, size); + +  for (i = 0; i < size; i++) +    a[i] = LIT2INT (ps->als[i]); + +  (void) picosat_sat (ps, -1); + +  //TODO short cut for 'picosat_res () == 10'? + +  if (ps->mtcls) +    { +      assert (picosat_res (ps) == 20); +      res = 0; +      goto DONE; +    } + +  res = mss (ps, a, size); + +  if (ps->mtcls) +    { +      res = 0; +      goto DONE; +    } + +  for (p = res; (lit = *p); p++) +    { +      v = ps->vars + abs (lit); +      if (lit < 0) +    { +      assert (!v->msspos); +      v->mssneg = 1; +    } +      else +    { +      assert (!v->mssneg); +      v->msspos = 1; +    } +    } + +  mssize = p - res; +  mcsize = INT_MIN; + +  for (i = 0; i < size; i++) +    { +      lit = a[i]; +      v = ps->vars + abs (lit); +      if (lit > 0 && v->msspos) +    inmss = 1; +      else if (lit < 0 && v->mssneg) +    inmss = 1; +      else +    inmss = 0; + +      if (mssize < mcsize) +    { +      if (inmss) +        picosat_add (ps, -lit); +    } +      else +    { +      if (!inmss) +        picosat_add (ps, lit); +    } + +      if (!inmss && mcs) +    push_mcsass (ps, lit); +    } +  picosat_add (ps, 0); +  if (mcs) +    push_mcsass (ps, 0); + +  for (i = 0; i < size; i++) +    { +      lit = a[i]; +      v = ps->vars + abs (lit); +      v->msspos = 0; +      v->mssneg = 0; +    } + +DONE: + +  reassume (ps, a, size); +  DELETEN (a, size); + +  return res; +} + +const int * +picosat_next_maximal_satisfiable_subset_of_assumptions (PS * ps) +{ +  const int * res; +  enter (ps); +  res = next_mss (ps, 0); +  leave (ps); +  return  res; +} + +const int * +picosat_next_minimal_correcting_subset_of_assumptions (PS * ps) +{ +  const int * res, * tmp; +  enter (ps); +  tmp = next_mss (ps, 1); +  res = tmp ? ps->mcsass : 0; +  leave (ps); +  return res; +} + +const int * +picosat_humus (PS * ps, +               void (*callback)(void*state,int nmcs,int nhumus), +           void * state) +{ +  int lit, nmcs, j, nhumus; +  const int * mcs, * p; +  unsigned i; +  Var * v; +  enter (ps); +#ifndef NDEBUG +  for (i = 1; i <= ps->max_var; i++) +    { +      v = ps->vars + i; +      assert (!v->humuspos); +      assert (!v->humusneg); +    } +#endif +  nhumus = nmcs = 0; +  while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps))) +    { +      for (p = mcs; (lit = *p); p++) +    { +      v = ps->vars + abs (lit); +      if (lit < 0) +        { +          if (!v->humusneg) +        { +          v->humusneg = 1; +          nhumus++; +        } +        } +      else +        { +          if (!v->humuspos) +        { +          v->humuspos = 1; +          nhumus++; +        } +        } +    } +      nmcs++; +      LOG ( fprintf (ps->out, +             "%smcs %d of size %d humus %d\n", +         ps->prefix, nmcs, (int)(p - mcs), nhumus)); +      if (callback) +    callback (state, nmcs, nhumus); +    } +  assert (!ps->szhumus); +  ps->szhumus = 1; +  for (i = 1; i <= ps->max_var; i++) +    { +      v = ps->vars + i; +      if (v->humuspos) +    ps->szhumus++; +      if (v->humusneg) +    ps->szhumus++; +    } +  assert (nhumus + 1 == ps->szhumus); +  NEWN (ps->humus, ps->szhumus); +  j = 0; +  for (i = 1; i <= ps->max_var; i++) +    { +      v = ps->vars + i; +      if (v->humuspos) +    { +      assert (j < nhumus); +      ps->humus[j++] = (int) i; +    } +      if (v->humusneg) +    { +      assert (j < nhumus); +      assert (i < INT_MAX); +      ps->humus[j++] = - (int) i; +    } +    } +  assert (j == nhumus); +  assert (j < ps->szhumus); +  ps->humus[j] = 0; +  leave (ps); +  return ps->humus; +} + +int +picosat_usedlit (PS * ps, int int_lit) +{ +  int res; +  check_ready (ps); +  check_sat_or_unsat_or_unknown_state (ps); +  ABORTIF (!int_lit, "API usage: zero literal can not be used"); +  int_lit = abs (int_lit); +  res = (int_lit <= (int) ps->max_var) ? ps->vars[int_lit].used : 0; +  return res; +} + +void +picosat_write_clausal_core (PS * ps, FILE * file) +{ +  check_trace_support_and_execute (ps, file, write_core_wrapper, 0); +} + +void +picosat_write_compact_trace (PS * ps, FILE * file) +{ +  check_trace_support_and_execute (ps, file, write_trace, +                                   COMPACT_TRACECHECK_TRACE_FMT); +} + +void +picosat_write_extended_trace (PS * ps, FILE * file) +{ +  check_trace_support_and_execute (ps, file, write_trace, +                                   EXTENDED_TRACECHECK_TRACE_FMT); +} + +void +picosat_write_rup_trace (PS * ps, FILE * file) +{ +  check_trace_support_and_execute (ps, file, write_trace, RUP_TRACE_FMT); +} + +size_t +picosat_max_bytes_allocated (PS * ps) +{ +  check_ready (ps); +  return ps->max_bytes; +} + +void +picosat_set_propagation_limit (PS * ps, unsigned long long l) +{ +  ps->lpropagations = l; +} + +unsigned long long +picosat_propagations (PS * ps) +{ +  return ps->propagations; +} + +unsigned long long +picosat_visits (PS * ps) +{ +  return ps->visits; +} + +unsigned long long +picosat_decisions (PS * ps) +{ +  return ps->decisions; +} + +int +picosat_variables (PS * ps) +{ +  check_ready (ps); +  return (int) ps->max_var; +} + +int +picosat_added_original_clauses (PS * ps) +{ +  check_ready (ps); +  return (int) ps->oadded; +} + +void +picosat_stats (PS * ps) +{ +#ifndef RCODE +  unsigned redlits; +#endif +#ifdef STATS +  check_ready (ps); +  assert (ps->sdecisions + ps->rdecisions + ps->assumptions == ps->decisions); +#endif +  if (ps->calls > 1) +     fprintf (ps->out, "%s%u calls\n", ps->prefix, ps->calls); +  if (ps->contexts) +    { +       fprintf (ps->out, "%s%u contexts", ps->prefix, ps->contexts); +#ifdef STATS +       fprintf (ps->out, " %u internal variables", ps->internals); +#endif +       fprintf (ps->out, "\n"); +    } +   fprintf (ps->out, "%s%u iterations\n", ps->prefix, ps->iterations); +   fprintf (ps->out, "%s%u restarts", ps->prefix, ps->restarts); +#ifdef STATS +   fprintf (ps->out, " (%u skipped)", ps->skippedrestarts); +#endif +  fputc ('\n', ps->out); +#ifndef NFL +   fprintf (ps->out, "%s%u failed literals", ps->prefix, ps->failedlits); +#ifdef STATS +   fprintf (ps->out, +           ", %u calls, %u rounds, %llu propagations", +           ps->flcalls, ps->flrounds, ps->flprops); +#endif +  fputc ('\n', ps->out); +#ifdef STATS +   fprintf (ps->out, +    "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n", +    ps->prefix, +    ps->ifailedlits, PERCENT (ps->ifailedlits, ps->failedlits), +    ps->floopsed, ps->fltried, ps->flskipped); +#endif +#endif +   fprintf (ps->out, "%s%u conflicts", ps->prefix, ps->conflicts); +#ifdef STATS +   fprintf (ps->out, " (%u uips = %.1f%%)\n", ps->uips, PERCENT(ps->uips,ps->conflicts)); +#else +  fputc ('\n', ps->out); +#endif +#ifndef NADC +   fprintf (ps->out, "%s%u adc conflicts\n", ps->prefix, ps->adoconflicts); +#endif +#ifdef STATS +   fprintf (ps->out, "%s%llu dereferenced literals\n", ps->prefix, ps->derefs); +#endif +   fprintf (ps->out, "%s%u decisions", ps->prefix, ps->decisions); +#ifdef STATS +   fprintf (ps->out, " (%u random = %.2f%%", +           ps->rdecisions, PERCENT (ps->rdecisions, ps->decisions)); +   fprintf (ps->out, ", %u assumptions", ps->assumptions); +  fputc (')', ps->out); +#endif +  fputc ('\n', ps->out); +#ifdef STATS +   fprintf (ps->out, +           "%s%u static phase decisions (%.1f%% of all variables)\n", +       ps->prefix, +       ps->staticphasedecisions, PERCENT (ps->staticphasedecisions, ps->max_var)); +#endif +   fprintf (ps->out, "%s%u fixed variables\n", ps->prefix, ps->fixed); +  assert (ps->nonminimizedllits >= ps->minimizedllits); +#ifndef RCODE +  redlits = ps->nonminimizedllits - ps->minimizedllits; +#endif +   fprintf (ps->out, "%s%u learned literals\n", ps->prefix, ps->llitsadded); +   fprintf (ps->out, "%s%.1f%% deleted literals\n", +     ps->prefix, PERCENT (redlits, ps->nonminimizedllits)); + +#ifdef STATS +#ifdef TRACE +   fprintf (ps->out, +       "%s%llu antecedents (%.1f antecedents per clause", +       ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts)); +  if (ps->trace) +     fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents)); +  fputs (")\n", ps->out); +#endif + +   fprintf (ps->out, "%s%llu propagations (%.1f propagations per decision)\n", +           ps->prefix, ps->propagations, AVERAGE (ps->propagations, ps->decisions)); +   fprintf (ps->out, "%s%llu visits (%.1f per propagation)\n", +       ps->prefix, ps->visits, AVERAGE (ps->visits, ps->propagations)); +   fprintf (ps->out, +           "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n", +       ps->prefix, ps->bvisits, +       PERCENT (ps->bvisits, ps->visits), +       AVERAGE (ps->bvisits, ps->propagations)); +   fprintf (ps->out, +           "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n", +       ps->prefix, ps->tvisits, +       PERCENT (ps->tvisits, ps->visits), +       AVERAGE (ps->tvisits, ps->propagations)); +   fprintf (ps->out, +           "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n", +       ps->prefix, ps->lvisits, +       PERCENT (ps->lvisits, ps->visits), +       AVERAGE (ps->lvisits, ps->propagations)); +   fprintf (ps->out, "%s%llu other true (%.1f%% of visited clauses)\n", +       ps->prefix, ps->othertrue, PERCENT (ps->othertrue, ps->visits)); +   fprintf (ps->out, +           "%s%llu other true in binary clauses (%.1f%%)" +       ", %llu upper (%.1f%%)\n", +           ps->prefix, ps->othertrue2, PERCENT (ps->othertrue2, ps->othertrue), +       ps->othertrue2u, PERCENT (ps->othertrue2u, ps->othertrue2)); +   fprintf (ps->out, +           "%s%llu other true in large clauses (%.1f%%)" +       ", %llu upper (%.1f%%)\n", +           ps->prefix, ps->othertruel, PERCENT (ps->othertruel, ps->othertrue), +       ps->othertruelu, PERCENT (ps->othertruelu, ps->othertruel)); +   fprintf (ps->out, "%s%llu ternary and large traversals (%.1f per visit)\n", +       ps->prefix, ps->traversals, AVERAGE (ps->traversals, ps->visits)); +   fprintf (ps->out, "%s%llu large traversals (%.1f per large visit)\n", +       ps->prefix, ps->ltraversals, AVERAGE (ps->ltraversals, ps->lvisits)); +   fprintf (ps->out, "%s%llu assignments\n", ps->prefix, ps->assignments); +#else +   fprintf (ps->out, "%s%llu propagations\n", ps->prefix, picosat_propagations (ps)); +   fprintf (ps->out, "%s%llu visits\n", ps->prefix, picosat_visits (ps)); +#endif +   fprintf (ps->out, "%s%.1f%% variables used\n", ps->prefix, PERCENT (ps->vused, ps->max_var)); + +  sflush (ps); +   fprintf (ps->out, "%s%.1f seconds in library\n", ps->prefix, ps->seconds); +   fprintf (ps->out, "%s%.1f megaprops/second\n", +       ps->prefix, AVERAGE (ps->propagations / 1e6f, ps->seconds)); +   fprintf (ps->out, "%s%.1f megavisits/second\n", +       ps->prefix, AVERAGE (ps->visits / 1e6f, ps->seconds)); +   fprintf (ps->out, "%sprobing %.1f seconds %.0f%%\n", +           ps->prefix, ps->flseconds, PERCENT (ps->flseconds, ps->seconds)); +#ifdef STATS +   fprintf (ps->out, +       "%srecycled %.1f MB in %u reductions\n", +       ps->prefix, ps->rrecycled / (double) (1 << 20), ps->reductions); +   fprintf (ps->out, +       "%srecycled %.1f MB in %u simplifications\n", +       ps->prefix, ps->srecycled / (double) (1 << 20), ps->simps); +#else +   fprintf (ps->out, "%s%u simplifications\n", ps->prefix, ps->simps); +   fprintf (ps->out, "%s%u reductions\n", ps->prefix, ps->reductions); +   fprintf (ps->out, "%s%.1f MB recycled\n", ps->prefix, ps->recycled / (double) (1 << 20)); +#endif +   fprintf (ps->out, "%s%.1f MB maximally allocated\n", +        ps->prefix, picosat_max_bytes_allocated (ps) / (double) (1 << 20)); +} + +#ifndef NGETRUSAGE +#include +#include +#include +#endif + +double +picosat_time_stamp (void) +{ +  double res = -1; +#ifndef NGETRUSAGE +  struct rusage u; +  res = 0; +  if (!getrusage (RUSAGE_SELF, &u)) +    { +      res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec; +      res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec; +    } +#endif +  return res; +} + +double +picosat_seconds (PS * ps) +{ +  check_ready (ps); +  return ps->seconds; +} + +void +picosat_print (PS * ps, FILE * file) +{ +#ifdef NO_BINARY_CLAUSES +  Lit * lit, *other, * last; +  Ltk * stack; +#endif +  Lit **q, **eol; +  Cls **p, *c; +  unsigned n; + +  if (ps->measurealltimeinlib) +    enter (ps); +  else +    check_ready (ps); + +  n = 0; +  n +=  ps->alshead - ps->als; + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; + +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif +      n++; +    } + +#ifdef NO_BINARY_CLAUSES +  last = int2lit (ps, -ps->max_var); +  for (lit = int2lit (ps, 1); lit <= last; lit++) +    { +      stack = LIT2IMPLS (lit); +      eol = stack->start + stack->count; +      for (q = stack->start; q < eol; q++) +    if (*q >= lit) +      n++; +    } +#endif + +  fprintf (file, "p cnf %d %u\n", ps->max_var, n); + +  for (p = SOC; p != EOC; p = NXC (p)) +    { +      c = *p; +      if (!c) +    continue; + +#ifdef TRACE +      if (c->collected) +    continue; +#endif + +      eol = end_of_lits (c); +      for (q = c->lits; q < eol; q++) +    fprintf (file, "%d ", LIT2INT (*q)); + +      fputs ("0\n", file); +    } + +#ifdef NO_BINARY_CLAUSES +  last = int2lit (ps, -ps->max_var); +  for (lit = int2lit (ps, 1); lit <= last; lit++) +    { +      stack = LIT2IMPLS (lit); +      eol = stack->start + stack->count; +      for (q = stack->start; q < eol; q++) +    if ((other = *q) >= lit) +      fprintf (file, "%d %d 0\n", LIT2INT (lit), LIT2INT (other)); +    } +#endif + +  { +    Lit **r; +    for (r = ps->als; r < ps->alshead; r++) +      fprintf (file, "%d 0\n", LIT2INT (*r)); +  } + +  fflush (file); + +  if (ps->measurealltimeinlib) +    leave (ps); +} + +void +picosat_enter (PS * ps) +{ +  enter (ps); +} + +void +picosat_leave (PS * ps) +{ +  leave (ps); +} + +void +picosat_message (PS * ps, int vlevel, const char * fmt, ...) +{ +  va_list ap; + +  if (vlevel > ps->verbosity) +    return; + +  fputs (ps->prefix, ps->out); +  va_start (ap, fmt); +  vfprintf (ps->out, fmt, ap); +  va_end (ap); +  fputc ('\n', ps->out); +} + +int +picosat_changed (PS * ps) +{ +  int res; + +  check_ready (ps); +  check_sat_state (ps); + +  res = (ps->min_flipped <= ps->saved_max_var); +  assert (!res || ps->saved_flips != ps->flips); + +  return res; +} + +void +picosat_reset_phases (PS * ps) +{ +  rebias (ps); +} + +void +picosat_reset_scores (PS * ps) +{ +  Rnk * r; +  ps->hhead = ps->heap + 1; +  for (r = ps->rnks + 1; r <= ps->rnks + ps->max_var; r++) +    { +      CLR (r); +      hpush (ps, r); +    } +} + +void +picosat_remove_learned (PS * ps, unsigned percentage) +{ +  enter (ps); +  reset_incremental_usage (ps); +  reduce (ps, percentage); +  leave (ps); +} + +void +picosat_set_global_default_phase (PS * ps, int phase) +{ +  check_ready (ps); +  ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' " +                      "with negative argument"); +  ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' " +                      "with argument > 3"); +  ps->defaultphase = phase; +} + +void +picosat_set_default_phase_lit (PS * ps, int int_lit, int phase) +{ +  unsigned newphase; +  Lit * lit; +  Var * v; + +  check_ready (ps); + +  lit = import_lit (ps, int_lit, 1); +  v = LIT2VAR (lit); + +  if (phase) +    { +      newphase = (int_lit < 0) == (phase < 0); +      v->defphase = v->phase = newphase; +      v->usedefphase = v->assigned = 1; +    } +  else +    { +      v->usedefphase = v->assigned = 0; +    } +} + +void +picosat_set_more_important_lit (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; +  Rnk * r; + +  check_ready (ps); + +  lit = import_lit (ps, int_lit, 1); +  v = LIT2VAR (lit); +  r = VAR2RNK (v); + +  ABORTIF (r->lessimportant, "can not mark variable more and less important"); + +  if (r->moreimportant) +    return; + +  r->moreimportant = 1; + +  if (r->pos) +    hup (ps, r); +} + +void +picosat_set_less_important_lit (PS * ps, int int_lit) +{ +  Lit * lit; +  Var * v; +  Rnk * r; + +  check_ready (ps); + +  lit = import_lit (ps, int_lit, 1); +  v = LIT2VAR (lit); +  r = VAR2RNK (v); + +  ABORTIF (r->moreimportant, "can not mark variable more and less important"); + +  if (r->lessimportant) +    return; + +  r->lessimportant = 1; + +  if (r->pos) +    hdown (ps, r); +} + +#ifndef NADC + +unsigned +picosat_ado_conflicts (PS * ps) +{ +  check_ready (ps); +  return ps->adoconflicts; +} + +void +picosat_disable_ado (PS * ps) +{ +  check_ready (ps); +  assert (!ps->adodisabled); +  ps->adodisabled = 1; +} + +void +picosat_enable_ado (PS * ps) +{ +  check_ready (ps); +  assert (ps->adodisabled); +  ps->adodisabled = 0; +} + +void +picosat_set_ado_conflict_limit (PS * ps, unsigned newadoconflictlimit) +{ +  check_ready (ps); +  ps->adoconflictlimit = newadoconflictlimit; +} + +#endif + +void +picosat_simplify (PS * ps) +{ +  enter (ps); +  reset_incremental_usage (ps); +  simplify (ps, 1); +  leave (ps); +} + +int +picosat_haveados (void) +{ +#ifndef NADC +  return 1; +#else +  return 0; +#endif +} + +void +picosat_save_original_clauses (PS * ps) +{ +  if (ps->saveorig) return; +  ABORTIF (ps->oadded, "API usage: 'picosat_save_original_clauses' too late"); +  ps->saveorig = 1; +} + +void picosat_set_interrupt (PicoSAT * ps, +                            void * external_state, +                int (*interrupted)(void * external_state)) +{ +  ps->interrupt.state = external_state; +  ps->interrupt.function = interrupted; +} + +int +picosat_deref_partial (PS * ps, int int_lit) +{ +  check_ready (ps); +  check_sat_state (ps); +  ABORTIF (!int_lit, "API usage: can not partial deref zero literal"); +  ABORTIF (ps->mtcls, "API usage: deref partial after empty clause generated"); +  ABORTIF (!ps->saveorig, "API usage: 'picosat_save_original_clauses' missing"); + +#ifdef STATS +  ps->derefs++; +#endif + +  if (!ps->partial) +    minautarky (ps); + +  return pderef (ps, int_lit); +}