<commit_before>#include "clause.hpp"
#include "internal.hpp"
#include "iterator.hpp"
#include "macros.hpp"
#include "message.hpp"
#include "proof.hpp"

#include <algorithm>

namespace CaDiCaL {

// Code for conflict analysis, e.g., to generate the first UIP clause.  The
// main function is 'analyze' below.  It further uses 'minimize' to minimize
// the first UIP clause, which is in 'minimize.cpp'.  An important side
// effect of conflict analysis is to update the decision queue by bumping
// variables.  Similarly resolved clauses are bumped to mark them as active.

/*------------------------------------------------------------------------*/

void Internal::learn_empty_clause () {
  assert (!unsat);
  LOG ("learned empty clause");
  if (proof) proof->trace_empty_clause ();
  unsat = true;
}

void Internal::learn_unit_clause (int lit) {
  LOG ("learned unit clause %d", lit);
  if (proof) proof->trace_unit_clause (lit);
  iterating = true;
  stats.fixed++;
}

/*------------------------------------------------------------------------*/

// Important variables recently used in conflict analysis are 'bumped',
// which means to move them to the front of the VMTF decision queue.  The
// 'bumped' time stamp is updated accordingly.  It is used to determine
// whether the 'queue.assigned' pointer has to be moved in 'unassign'.

void Internal::bump_variable (int lit) {
  const int idx = vidx (lit);
  Link * l = ltab + idx;
  if (!l->next) return;
  queue.dequeue (ltab, l);
  queue.enqueue (ltab, l);
  btab[idx] = ++stats.bumped;
  LOG ("moved to front %d and bumped %ld", idx, btab[idx]);
  if (!vals[idx]) update_queue_unassigned (idx);
}

// Initially we proposed to bump the variable in the current 'bumped' stamp
// order only.  This maintains the current order between bumped variables.
// On few benchmarks this however lead to a large number of propagations per
// seconds, which can be reduced by an order of magnitude by focusing
// somewhat on recently assigned variables more, particularly in this
// situation.  This can easily be achieved by using the sum of the 'bumped'
// time stamp and trail height 'trail' for comparison.  Note that 'bumped'
// is always increasing and gets really large, while 'trail' can never be
// larger than the number of variables, so there is likely a potential for
// further optimization.

struct bump_earlier {
  Internal * internal;
  bump_earlier (Internal * s) : internal (s) { }
  bool operator () (int a, int b) {
    long s = internal->bumped (a) + internal->var (a).trail;
    long t = internal->bumped (b) + internal->var (b).trail;
    return s < t;
  }
};

void Internal::bump_variables () {
  START (bump);
  reverse (analyzed.begin (), analyzed.end ());
  stable_sort (analyzed.begin (), analyzed.end (), bump_earlier (this));
  for (const_int_iterator i = analyzed.begin (); i != analyzed.end (); i++)
    bump_variable (*i);
  STOP (bump);
}

/*------------------------------------------------------------------------*/

// Clause activity is replaced by a move-to-front scheme as well with
// 'resolved' as time stamp.  Only long and high glue clauses are stamped
// since small or low glue clauses are kept anyhow (and do not actually have
// a 'resolved' field).  We keep the relative order of bumped clauses by
// sorting them first.

void Internal::bump_resolved_clauses () {
  START (bump);
  sort (resolved.begin (), resolved.end (), resolved_earlier ());
  for (const_clause_iterator i = resolved.begin (); i != resolved.end (); i++)
    (*i)->resolved () = ++stats.resolved;
  STOP (bump);
  resolved.clear ();
}

void Internal::resolve_clause (Clause * c) {
  if (!c->redundant) return;
  if (c->size <= opts.keepsize) return;
  if (c->glue <= opts.keepglue) return;
  assert (c->extended);
  resolved.push_back (c);
}

/*------------------------------------------------------------------------*/

// During conflict analysis literals not seen yet either become part of the
// first UIP clause (if on lower decision level), are dropped (if fixed),
// or are resolved away (if on the current decision level and different from
// the first UIP).  At the same time we update the number of seen literals on
// a decision level and the smallest trail position of a seen literal for
// each decision level.  This both helps conflict clause minimization.  The
// number of seen levels is the glucose level (also called glue, or LBD).

inline void Internal::analyze_literal (int lit, int & open) {
  assert (lit);<commit_msg>inline<commit_after>#include "clause.hpp"
#include "internal.hpp"
#include "iterator.hpp"
#include "macros.hpp"
#include "message.hpp"
#include "proof.hpp"

#include <algorithm>

namespace CaDiCaL {

// Code for conflict analysis, e.g., to generate the first UIP clause.  The
// main function is 'analyze' below.  It further uses 'minimize' to minimize
// the first UIP clause, which is in 'minimize.cpp'.  An important side
// effect of conflict analysis is to update the decision queue by bumping
// variables.  Similarly resolved clauses are bumped to mark them as active.

/*------------------------------------------------------------------------*/

void Internal::learn_empty_clause () {
  assert (!unsat);
  LOG ("learned empty clause");
  if (proof) proof->trace_empty_clause ();
  unsat = true;
}

void Internal::learn_unit_clause (int lit) {
  LOG ("learned unit clause %d", lit);
  if (proof) proof->trace_unit_clause (lit);
  iterating = true;
  stats.fixed++;
}

/*------------------------------------------------------------------------*/

// Important variables recently used in conflict analysis are 'bumped',
// which means to move them to the front of the VMTF decision queue.  The
// 'bumped' time stamp is updated accordingly.  It is used to determine
// whether the 'queue.assigned' pointer has to be moved in 'unassign'.

void Internal::bump_variable (int lit) {
  const int idx = vidx (lit);
  Link * l = ltab + idx;
  if (!l->next) return;
  queue.dequeue (ltab, l);
  queue.enqueue (ltab, l);
  btab[idx] = ++stats.bumped;
  LOG ("moved to front %d and bumped %ld", idx, btab[idx]);
  if (!vals[idx]) update_queue_unassigned (idx);
}

// Initially we proposed to bump the variable in the current 'bumped' stamp
// order only.  This maintains the current order between bumped variables.
// On few benchmarks this however lead to a large number of propagations per
// seconds, which can be reduced by an order of magnitude by focusing
// somewhat on recently assigned variables more, particularly in this
// situation.  This can easily be achieved by using the sum of the 'bumped'
// time stamp and trail height 'trail' for comparison.  Note that 'bumped'
// is always increasing and gets really large, while 'trail' can never be
// larger than the number of variables, so there is likely a potential for
// further optimization.

struct bump_earlier {
  Internal * internal;
  bump_earlier (Internal * s) : internal (s) { }
  bool operator () (int a, int b) {
    long s = internal->bumped (a) + internal->var (a).trail;
    long t = internal->bumped (b) + internal->var (b).trail;
    return s < t;
  }
};

void Internal::bump_variables () {
  START (bump);
  reverse (analyzed.begin (), analyzed.end ());
  stable_sort (analyzed.begin (), analyzed.end (), bump_earlier (this));
  for (const_int_iterator i = analyzed.begin (); i != analyzed.end (); i++)
    bump_variable (*i);
  STOP (bump);
}

/*------------------------------------------------------------------------*/

// Clause activity is replaced by a move-to-front scheme as well with
// 'resolved' as time stamp.  Only long and high glue clauses are stamped
// since small or low glue clauses are kept anyhow (and do not actually have
// a 'resolved' field).  We keep the relative order of bumped clauses by
// sorting them first.

void Internal::bump_resolved_clauses () {
  START (bump);
  sort (resolved.begin (), resolved.end (), resolved_earlier ());
  for (const_clause_iterator i = resolved.begin (); i != resolved.end (); i++)
    (*i)->resolved () = ++stats.resolved;
  STOP (bump);
  resolved.clear ();
}

inline void Internal::resolve_clause (Clause * c) {
  if (!c->redundant) return;
  if (c->size <= opts.keepsize) return;
  if (c->glue <= opts.keepglue) return;
  assert (c->extended);
  resolved.push_back (c);
}

/*------------------------------------------------------------------------*/

// During conflict analysis literals not seen yet either become part of the
// first UIP clause (if on lower decision level), are dropped (if fixed),
// or are resolved away (if on the current decision level and different from
// the first UIP).  At the same time we update the number of seen literals on
// a decision level and the smallest trail position of a seen literal for
// each decision level.  This both helps conflict clause minimization.  The
// number of seen levels is the glucose level (also called glue, or LBD).

inline void Internal::analyze_literal (int lit, int & open) {
  assert (lit);
{'fraction_non_alphanumeric': 0.1737391690735392, 'fraction_numerical': 0.0, 'mean_word_length': 2.821307300509338, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5347020', 'n_tokens_mistral': 2570, 'n_tokens_neox': 2509, 'n_words': 1066}