text: #ifndef _internal_hpp_INCLUDED
  #define _internal_hpp_INCLUDED
  
  /*------------------------------------------------------------------------*/
  
  // Wrapped build specific headers which should go first.
  
  #include "inttypes.hpp"
  
  /*------------------------------------------------------------------------*/
  
  // Common 'C' headers.
  
  #include <cassert>
  #include <climits>
  #include <cmath>
  #include <cstdio>
  #include <cstdlib>
  #include <cstring>
  #include <cctype>
  #include <csignal>
  
  // Less common 'C' header.
  
  extern "C" {
  #include <unistd.h>
  }
  
  /*------------------------------------------------------------------------*/
  
  // Common 'C++' headers.
  
  #include <algorithm>
  #include <queue>
  #include <string>
  #include <vector>
  
  /*------------------------------------------------------------------------*/
  
  // All internal headers are included here.  This gives a nice overview on
  // what is needed altogether. The 'Internal' class needs almost all the
  // headers anyhow (since the idea is to avoid pointer references as much as
  // possible).  Most implementation files need to see the definition of the
  // 'Internal' too.  Thus there is no real advantage in trying to reduce the
  // number of header files included here.  The other benefit of having all
  // header files here is that '.cpp' files then only need to include this.
  
  #include "arena.hpp"
  #include "averages.hpp"
  #include "bins.hpp"
  #include "block.hpp"
  #include "cadical.hpp"
  #include "checker.hpp"
  #include "clause.hpp"
  #include "config.hpp"
  #include "contract.hpp"
  #include "cover.hpp"
  #include "elim.hpp"
  #include "ema.hpp"
  #include "external.hpp"
  #include "file.hpp"
  #include "flags.hpp"
  #include "format.hpp"
  #include "heap.hpp"
  #include "instantiate.hpp"
  #include "internal.hpp"
  #include "level.hpp"
  #include "limit.hpp"
  #include "logging.hpp"
  #include "message.hpp"
  #include "observer.hpp"
  #include "occs.hpp"
  #include "options.hpp"
  #include "parse.hpp"
  #include "phases.hpp"
  #include "profile.hpp"
  #include "proof.hpp"
  #include "queue.hpp"
  #include "radix.hpp"
  #include "random.hpp"
  #include "range.hpp"
  #include "reap.hpp"
  #include "reluctant.hpp"
  #include "resources.hpp"
  #include "score.hpp"
  #include "stats.hpp"
  #include "terminal.hpp"
  #include "tracer.hpp"
  #include "util.hpp"
  #include "var.hpp"
  #include "version.hpp"
  #include "vivify.hpp"
  #include "watch.hpp"
  
  /*------------------------------------------------------------------------*/
  
  namespace CaDiCaL {
  
  using namespace std;
  
  struct Coveror;
  struct External;
  struct Walker;
  
  struct CubesWithStatus {
    int status;
    std::vector<std::vector<int>> cubes;
  };
  
  /*------------------------------------------------------------------------*/
  
  struct Internal {
  
    /*----------------------------------------------------------------------*/
  
    // The actual internal state of the solver is set and maintained in this
    // section.  This is currently only used for debugging and testing.
  
    enum Mode {
      BLOCK    = (1<<0),
      CONDITION= (1<<1),
      COVER    = (1<<2),
      DECOMP   = (1<<3),
      DEDUP    = (1<<4),
      ELIM     = (1<<5),
      LUCKY    = (1<<6),
      PROBE    = (1<<7),
      SEARCH   = (1<<8),
      SIMPLIFY = (1<<9),
      SUBSUME  = (1<<10),
      TERNARY  = (1<<11),
      TRANSRED = (1<<12),
      VIVIFY   = (1<<13),
      WALK     = (1<<14),
    };
  
    bool in_mode (Mode m) const { return (mode & m) != 0; }
    void set_mode (Mode m) { assert (!(mode & m)); mode |= m; }
    void reset_mode (Mode m) { assert (mode & m); mode &= ~m; }
    void require_mode (Mode m) const { assert (mode & m), (void) m; }
  
    /*----------------------------------------------------------------------*/
  
    int mode;                     // current internal state
    bool unsat;                   // empty clause found or learned
    bool iterating;               // report learned unit ('i' line)
    bool localsearching;          // true during local search
    bool lookingahead;            // true during look ahead
    bool preprocessing;           // true during preprocessing
    bool protected_reasons;       // referenced reasons are protected
    bool force_saved_phase;       // force saved phase in decision
    bool searching_lucky_phases;  // during 'lucky_phases'
    bool stable;                  // true during stabilization phase
    bool reported;                // reported in this solving call
    char rephased;                // last type of resetting phases
    Reluctant reluctant;          // restart counter in stable mode
    size_t vsize;                 // actually allocated variable data size
    int max_var;                  // internal maximum variable index
    int level;                    // decision level ('control.size () - 1')
    Phases phases;                // saved, target and best phases
    signed char * vals;           // assignment [-max_var,max_var]
    vector<signed char> marks;    // signed marks [1,max_var]
    vector<unsigned> frozentab;   // frozen counters [1,max_var]
    vector<int> i2e;              // maps internal 'idx' to external 'lit'
    Queue queue;                  // variable move to front decision queue
    Links links;                  // table of links for decision queue
    double score_inc;             // current score increment
    ScoreSchedule scores;         // score based decision priority queue
    vector<double> stab;          // table of variable scores [1,max_var]
    vector<Var> vtab;             // variable table [1,max_var]
    vector<int> parents;          // parent literals during probing
    vector<Flags> ftab;           // variable and literal flags
    vector<int64_t> btab;         // enqueue time stamps for queue
    vector<int64_t> gtab;         // time stamp table to recompute glue
    vector<Occs> otab;            // table of occurrences for all literals
    vector<int> ptab;             // table for caching probing attempts
    vector<int64_t> ntab;         // number of one-sided occurrences table
    vector<Bins> big;             // binary implication graph
    vector<Watches> wtab;         // table of watches for all literals
    Clause * conflict;            // set in 'propagation', reset in 'analyze'
    Clause * ignore;              // ignored during 'vivify_propagate'
    size_t propagated;            // next trail position to propagate
    size_t propagated2;           // next binary trail position to propagate
    size_t best_assigned;         // best maximum assigned ever
    size_t target_assigned;       // maximum assigned without conflict
    size_t no_conflict_until;     // largest trail prefix without conflict
    vector<int> trail;            // currently assigned literals
    vector<int> clause;           // simplified in parsing & learning
    vector<int> assumptions;      // assumed literals
    vector<int> constraint;       // literals of the constraint
    bool unsat_constraint;        // constraint used for unsatisfiability?
    bool marked_failed;           // are the failed assumptions marked?
    vector<int> original;         // original added literals
    vector<int> levels;           // decision levels in learned clause
    vector<int> analyzed;         // analyzed literals in 'analyze'
    vector<int> minimized;        // removable or poison in 'minimize'
    vector<int> shrinkable;       // removable or poison in 'shrink'
    Reap reap;                    // radix heap for shrink
  
    vector<int> probes;           // remaining scheduled probes
    vector<Level> control;        // 'level + 1 == control.size ()'
    vector<Clause*> clauses;      // ordered collection of all clauses
    Averages averages;            // glue, size, jump moving averages
    Limit lim;                    // limits for various phases
    Last last;                    // statistics at last occurrence
    Inc inc;                      // increments on limits
    Proof * proof;                // clausal proof observers if non zero
    Checker * checker;            // online proof checker observing proof
    Tracer * tracer;              // proof to file tracer observing proof
    Options opts;                 // run-time options
    Stats stats;                  // statistics
  #ifndef QUIET
    Profiles profiles;            // time profiles for various functions
    bool force_phase_messages;    // force 'phase (...)' messages
  #endif
    Arena arena;                  // memory arena for moving garbage collector
    Format error_message;         // provide persistent error message
    string prefix;                // verbose messages prefix
    int NUM_AUX_DECISIONS;
    Internal * internal;          // proxy to 'this' in macros
    External * external;          // proxy to 'external' buddy in 'Solver'
  
    /*----------------------------------------------------------------------*/
  
    // Asynchronous termination flag written by 'terminate' and read by
    // 'terminated_asynchronously' (the latter at the end of this header).
    //
    volatile bool termination_forced;
  
    /*----------------------------------------------------------------------*/
  
    const Range vars;             // Provides safe variable iteration.
    const Sange lits;             // Provides safe literal iteration.
  
    /*----------------------------------------------------------------------*/
  
    Internal ();
    ~Internal ();
  
    /*----------------------------------------------------------------------*/
  
    // Internal delegates and helpers for corresponding functions in
    // 'External' and 'Solver'.  The 'init_vars' function initializes
    // variables up to and including the requested variable index.
    //
    void init_vars (int new_max_var);
  
    void init_enqueue (int idx);
    void init_queue (int old_max_var, int new_max_var);
  
    void init_scores (int old_max_var, int new_max_var);
  
    void add_original_lit (int lit);
  
    // Enlarge tables.
    //
    void enlarge_vals (size_t new_vsize);
    void enlarge (int new_max_var);
  
    // A variable is 'active' if it is not eliminated nor fixed.
    //
    bool active (int lit) { return flags(lit).active (); }
  
    int active () const {
      int res = stats.active;
  #ifndef NDEBUG
      int tmp = max_var;
      tmp -= stats.unused;
      tmp -= stats.now.fixed;
      tmp -= stats.now.eliminated;
      tmp -= stats.now.substituted;
      tmp -= stats.now.pure;
      assert (tmp >= 0);
      assert (tmp == res);
  #endif
      return res;
    }
  
    void reactivate (int lit);    // During 'restore'.
  
    // Currently remaining active redundant and irredundant clauses.
  
    int64_t redundant () const { return stats.current.redundant; }
  
    int64_t irredundant () const { return stats.current.irredundant; }
  
    double clause_variable_ratio () const {
      return relative (irredundant (), active ());
    }
  
    // Scale values relative to clause variable ratio.
    //
    double scale (double v) const;
  
    // Unsigned literals (abs) with checks.
    //
    int vidx (int lit) const {
      int idx;
      assert (lit);
      assert (lit != INT_MIN);
      idx = abs (lit);
      assert (idx <= max_var);
      return idx;
    }
  
    // Unsigned version with LSB denoting sign.  This is used in indexing arrays
    // by literals.  The idea is to keep the elements in such an array for both
    // the positive and negated version of a literal close together.
    //
    unsigned vlit (int lit) { return (lit < 0) + 2u * (unsigned) vidx (lit); }
  
    int u2i (unsigned u) {
      assert (u > 1);
      int res = u/2;
      assert (res <= max_var);
      if (u & 1) res = -res;
      return res;
    }
  
    // Helper functions to access variable and literal data.
    //
    Var & var (int lit)        { return vtab[vidx (lit)]; }
    Link & link (int lit)      { return links[vidx (lit)]; }
    Flags & flags (int lit)    { return ftab[vidx (lit)]; }
    int64_t & bumped (int lit) { return btab[vidx (lit)]; }
    int & propfixed (int lit)  { return ptab[vlit (lit)]; }
    double & score (int lit)   { return stab[vidx (lit)]; }
  
    const Flags &
    flags (int lit) const       { return ftab[vidx (lit)]; }
  
    bool occurring () const     { return !otab.empty (); }
    bool watching () const      { return !wtab.empty (); }
  
    Bins & bins (int lit)       { return big[vlit (lit)]; }
    Occs & occs (int lit)       { return otab[vlit (lit)]; }
    int64_t & noccs (int lit)   { return ntab[vlit (lit)]; }
    Watches & watches (int lit) { return wtab[vlit (lit)]; }
  
    // Variable bumping through exponential VSIDS (EVSIDS) as in MiniSAT.
    //
    bool use_scores () const { return opts.score && stable; }
    void bump_variable_score (int lit);
    void bump_variable_score_inc ();
    void rescale_variable_scores ();
  
    // Marking variables with a sign (positive or negative).
    //
    signed char marked (int lit) const {
      signed char res = marks [ vidx (lit) ];
      if (lit < 0) res = -res;
      return res;
    }
    void mark (int lit) {
      assert (!marked (lit));
      marks[vidx (lit)] = sign (lit);
      assert (marked (lit) > 0);
      assert (marked (-lit) < 0);
    }
    void unmark (int lit) {
      marks [ vidx (lit) ] = 0;
      assert (!marked (lit));
    }
  
    // Use only bits 6 and 7 to store the sign or zero.  The remaining
    // bits can be use as additional flags.
    //
    signed char marked67 (int lit) const {
      signed char res = marks [ vidx (lit) ] >> 6;
      if (lit < 0) res = -res;
      return res;
    }
    void mark67 (int lit) {
      signed char & m = marks[vidx (lit)];
      const signed char mask = 0x3f;
  #ifndef NDEBUG
      const signed char bits = m & mask;
  #endif
      m = (m & mask) | (sign (lit) << 6);
      assert (marked (lit) > 0);
      assert (marked (-lit) < 0);
      assert ((m & mask) == bits);
      assert (marked67 (lit) > 0);
      assert (marked67 (-lit) < 0);
    }
    void unmark67 (int lit) {
      signed char & m = marks[vidx (lit)];
      const signed char mask = 0x3f;
  #ifndef NDEBUG
      const signed bits = m & mask;
  #endif
      m &= mask;
      assert ((m & mask) == bits);
    }
  
    void unmark (vector<int> & lits) {
      for (const auto & lit : lits)
        unmark (lit);
    }
  
    // The other 6 bits of the 'marks' bytes can be used as additional
    // (unsigned) marking bits.  Currently we only use the least significant
    // bit in 'condition' to mark variables in the conditional part.
    //
    bool getbit (int lit, int bit) const {
      assert (0 <= bit), assert (bit < 6);
      return marks[vidx (lit)] & (1<<bit);
    }
    void setbit (int lit, int bit) {
      assert (0 <= bit), assert (bit < 6);
      assert (!getbit (lit, bit));
      marks[vidx (lit)] |= (1<<bit);
      assert (getbit (lit, bit));
    }
    void unsetbit (int lit, int bit) {
      assert (0 <= bit), assert (bit < 6);
      assert (getbit (lit, bit));
      marks[vidx (lit)] &= ~(1<<bit);
      assert (!getbit (lit, bit));
    }
  
    // Marking individual literals.
    //
    bool marked2 (int lit) const {
      unsigned res = marks [ vidx (lit) ];
      assert (res <= 3);
      unsigned bit = bign (lit);
      return (res & bit) != 0;
    }
    void mark2 (int lit) {
      marks[vidx (lit)] |= bign (lit);
      assert (marked2 (lit));
    }
  
    // Marking and unmarking of all literals in a clause.
    //
    void mark_clause ();          // mark 'this->clause'
    void mark (Clause *);
    void mark2 (Clause *);
    void unmark_clause ();        // unmark 'this->clause'
    void unmark (Clause *);
  
    // Watch literal 'lit' in clause with blocking literal 'blit'.
    // Inlined here, since it occurs in the tight inner loop of 'propagate'.
    //
    inline void watch_literal (int lit, int blit, Clause * c) {
      assert (lit != blit);
      Watches & ws = watches (lit);
      ws.push_back (Watch (blit, c));
      LOG (c, "watch %d blit %d in", lit, blit);
    }
  
    // Add two watches to a clause.  This is used initially during allocation
    // of a clause and during connecting back all watches after preprocessing.
    //
    inline void watch_clause (Clause * c) {
      const int l0 = c->literals[0];
      const int l1 = c->literals[1];
      watch_literal (l0, l1, c);
      watch_literal (l1, l0, c);
    }
  
    inline void unwatch_clause (Clause * c) {
      const int l0 = c->literals[0];
      const int l1 = c->literals[1];
      remove_watch (watches (l0), c);
      remove_watch (watches (l1), c);
    }
  
    // Update queue to point to last potentially still unassigned variable.
    // All variables after 'queue.unassigned' in bump order are assumed to be
    // assigned.  Then update the 'queue.bumped' field and log it.  This is
    // inlined here since it occurs in several inner loops.
    //
    inline void update_queue_unassigned (int idx) {
      assert (0 < idx);
      assert (idx <= max_var);
      queue.unassigned = idx;
      queue.bumped = btab[idx];
      LOG ("queue unassigned now %d bumped %" PRId64 "", idx, btab[idx]);
    }
  
    void bump_queue (int idx);
  
    // Mark (active) variables as eliminated, substituted, pure or fixed,
    // which turns them into inactive variables.
    //
    void mark_eliminated (int);
    void mark_substituted (int);
    void mark_active (int);
    void mark_fixed (int);
    void mark_pure (int);
  
    // Managing clauses in 'clause.cpp'.  Without explicit 'Clause' argument
    // these functions work on the global temporary 'clause'.
    //
    Clause * new_clause (bool red, int glue = 0);
    void promote_clause (Clause *, int new_glue);
    size_t shrink_clause (Clause *, int new_size);
    void minimize_sort_clause();
    void shrink_and_minimize_clause ();
    void reset_shrinkable();
    void mark_shrinkable_as_removable(int, std::vector<int>::size_type);
    int shrink_literal(int, int, unsigned);
    unsigned shrunken_block_uip(int, int, std::vector<int>::reverse_iterator &,
                                std::vector<int>::reverse_iterator &,
                                std::vector<int>::size_type, const int);
    void shrunken_block_no_uip(const std::vector<int>::reverse_iterator&, const std::vector<int>::reverse_iterator&, unsigned&, const int);
    void push_literals_of_block(const std::vector<int>::reverse_iterator&, const std::vector<int>::reverse_iterator&, int, unsigned);
    unsigned shrink_next(unsigned&, unsigned&);
    std::vector<int>::reverse_iterator minimize_and_shrink_block(std::vector<int>::reverse_iterator&, unsigned int&, unsigned int&, const int);
    unsigned shrink_block(std::vector<int>::reverse_iterator&, std::vector<int>::reverse_iterator&, int, unsigned&, unsigned&, const int, unsigned);
    unsigned shrink_along_reason(int, int, bool, bool&, unsigned);
  
    void deallocate_clause(Clause *);
    void delete_clause (Clause *);
    void mark_garbage (Clause *);
    void assign_original_unit (int);
    void add_new_original_clause ();
    Clause * new_learned_redundant_clause (int glue);
    Clause * new_hyper_binary_resolved_clause (bool red, int glue);
    Clause * new_clause_as (const Clause * orig);
    Clause * new_resolved_irredundant_clause ();
  
    // Forward reasoning through propagation in 'propagate.cpp'.
    //
    int assignment_level (int lit, Clause*);
    void search_assign (int lit, Clause *);
    void search_assign_driving (int lit, Clause * reason);
    void search_assume_decision (int decision);
    void assign_unit (int lit);
    bool propagate ();
  
    // Undo and restart in 'backtrack.cpp'.
    //
    void unassign (int lit);
    void update_target_and_best ();
    void backtrack (int target_level = 0);
  
    // Minimized learned clauses in 'minimize.cpp'.
    //
    bool minimize_literal (int lit, int depth = 0);
    void minimize_clause ();
  
    // Learning from conflicts in 'analyze.cc'.
    //
    void learn_empty_clause ();
    void learn_unit_clause (int lit);
    void bump_variable (int lit);
    void bump_variables ();
    int recompute_glue (Clause *);
    void bump_clause (Clause *);
    void clear_analyzed_literals ();
    void clear_analyzed_levels ();
    void clear_minimized_literals ();
    bool bump_also_reason_literal (int lit);
    void bump_also_reason_literals (int lit, int limit);
    void bump_also_all_reason_literals ();
    void analyze_literal (int lit, int & open);
    void analyze_reason (int lit, Clause *, int & open);
    Clause * new_driving_clause (const int glue, int & jump);
    int find_conflict_level (int & forced);
    int determine_actual_backtrack_level (int jump);
    void analyze ();
    void iterate ();       // report learned unit clause
  
    // Use last learned clause to subsume some more.
    //
    void eagerly_subsume_recently_learned_clauses (Clause *);
  
    // Restarting policy in 'restart.cc'.
    //
    bool stabilizing ();
    bool restarting ();
    int reuse_trail ();
    void restart ();
  
    // Functions to set and reset certain 'phases'.
    //
    void clear_phases (vector<signed char> &);  // reset argument to zero
    void copy_phases (vector<signed char> &);   // copy 'saved' to argument
  
    // Resetting the saved phased in 'rephase.cpp'.
    //
    bool rephasing ();
    char rephase_best ();
    char rephase_flipping ();
    char rephase_inverted ();
    char rephase_original ();
    char rephase_random ();
    char rephase_walk ();
    void shuffle_scores ();
    void shuffle_queue ();
    void rephase ();
  
    // Lucky feasible case checking.
    //
    int unlucky (int res);
    int trivially_false_satisfiable ();
    int trivially_true_satisfiable ();
    int forward_false_satisfiable ();
    int forward_true_satisfiable ();
    int backward_false_satisfiable ();
    int backward_true_satisfiable ();
    int positive_horn_satisfiable ();
    int negative_horn_satisfiable ();
  
    // Asynchronous terminating check.
    //
    bool terminated_asynchronously (int factor = 1);
  
    bool search_limits_hit ();
  
    void terminate () {
      LOG ("forcing asynchronous termination");
      termination_forced = true;
    }
  
    // Reducing means determining useless clauses with 'reduce' in
    // 'reduce.cpp' as well as root level satisfied clause and then removing
    // those which are not used as reason anymore with garbage collection.
    //
    bool flushing ();
    bool reducing ();
    void protect_reasons ();
    void mark_clauses_to_be_flushed ();
    void mark_useless_redundant_clauses_as_garbage ();
    bool propagate_out_of_order_units ();
    void unprotect_reasons ();
    void reduce ();
  
    // Garbage collection in 'collect.cpp' called from 'reduce' and during
    // inprocessing and preprocessing.
    //
    int clause_contains_fixed_literal (Clause *);
    void remove_falsified_literals (Clause *);
    void mark_satisfied_clauses_as_garbage ();
    void copy_clause (Clause *);
    void flush_watches (int lit, Watches &);
    size_t flush_occs (int lit);
    void flush_all_occs_and_watches ();
    void update_reason_references ();
    void copy_non_garbage_clauses ();
    void delete_garbage_clauses ();
    void check_clause_stats ();
    void check_var_stats ();
    bool arenaing ();
    void garbage_collection ();
  
    // Set-up occurrence list counters and containers.
    //
    void init_occs ();
    void init_bins ();
    void init_noccs ();
    void reset_occs ();
    void reset_bins ();
    void reset_noccs ();
  
    // Operators on watches.
    //
    void init_watches ();
    void connect_watches (bool irredundant_only = false);
    void sort_watches ();
    void clear_watches ();
    void reset_watches ();
  
    // Regular forward subsumption checking in 'subsume.cpp'.
    //
    bool subsuming ();
    void strengthen_clause (Clause *, int);
    void subsume_clause (Clause * subsuming, Clause * subsumed);
    int subsume_check (Clause * subsuming, Clause * subsumed);
    int try_to_subsume_clause (Clause *, vector<Clause*> & shrunken);
    void reset_subsume_bits ();
    bool subsume_round ();
    void subsume (bool update_limits = true);
  
    // Covered clause elimination of large clauses.
    //
    void covered_literal_addition (int lit, Coveror &);
    void asymmetric_literal_addition (int lit, Coveror &);
    void cover_push_extension (int lit, Coveror &);
    bool cover_propagate_asymmetric (int lit, Clause * ignore, Coveror &);
    bool cover_propagate_covered (int lit, Coveror &);
    bool cover_clause (Clause * c, Coveror &);
    int64_t cover_round ();
    bool cover ();
  
    // Strengthening through vivification in 'vivify.cpp'.
    //
    void flush_vivification_schedule (Vivifier &);
    bool consider_to_vivify_clause (Clause * candidate, bool redundant_mode);
    void vivify_analyze_redundant (Vivifier &, Clause * start, bool &);
    bool vivify_all_decisions (Clause * candidate, int subsume);
    void vivify_post_process_analysis (Clause * candidate, int subsume);
    void vivify_strengthen (Clause * candidate);
    void vivify_assign (int lit, Clause *);
    void vivify_assume (int lit);
    bool vivify_propagate ();
    void vivify_clause (Vivifier &, Clause * candidate);
    void vivify_round (bool redundant_mode, int64_t delta);
    void vivify ();
  
    // Compacting (shrinking internal variable tables) in 'compact.cpp'
    //
    bool compacting ();
    void compact ();
  
    // Transitive reduction of binary implication graph in 'transred.cpp'
    //
    void transred ();
  
    // We monitor the maximum size and glue of clauses during 'reduce' and
    // thus can predict if a redundant extended clause is likely to be kept in
    // the next 'reduce' phase.  These clauses are target of subsumption and
    // vivification checks, in addition to irredundant clauses.  Their
    // variables are also marked as being 'added'.
    //
    bool likely_to_be_kept_clause (Clause * c) {
      if (!c->redundant) return true;
      if (c->keep) return true;
      if (c->glue > lim.keptglue) return false;
      if (c->size > lim.keptsize) return false;
      return true;
    }
  
    // We mark variables in added or shrunken clauses as 'subsume' candidates
    // if the clause is likely to be kept in the next 'reduce' phase (see last
    // function above).  This gives a persistent (across consecutive
    // interleaved search and inprocessing phases) set of variables which have
    // to be reconsidered in subsumption checks, i.e., only clauses with
    // 'subsume' marked variables are checked to be forward subsumed.
    // A similar technique is used to reduce the effort in hyper ternary
    // resolution to focus on variables in new ternary clauses.
    //
    void mark_subsume (int lit) {
      Flags & f = flags (lit);
      if (f.subsume) return;
      LOG ("marking %d as subsuming literal candidate", abs (lit));
      stats.mark.subsume++;
      f.subsume = true;
    }
    void mark_ternary (int lit) {
      Flags & f = flags (lit);
      if (f.ternary) return;
      LOG ("marking %d as ternary resolution literal candidate", abs (lit));
      stats.mark.ternary++;
      f.ternary = true;
    }
    void mark_added (int lit, int size, bool redundant);
    void mark_added (Clause *);
  
    bool marked_subsume(int lit) const { return flags(lit).subsume; }
  
      // If irredundant clauses are removed or literals in clauses are removed,
      // then variables in such clauses should be reconsidered to be eliminated
      // through bounded variable elimination.  In contrast to 'subsume' the
      // 'elim' flag is restricted to 'irredundant' clauses only. For blocked
      // clause elimination it is better to have a more precise signed version,
      // which allows to independently mark positive and negative literals.
      //
      void mark_elim(int lit) {
        Flags &f = flags(lit);
        if (f.elim)
          return;
        LOG("marking %d as elimination literal candidate", lit);
        stats.mark.elim++;
        f.elim = true;
      }
      void mark_block(int lit) {
        Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        if (f.block & bit)
          return;
        LOG("marking %d as blocking literal candidate", lit);
        stats.mark.block++;
        f.block |= bit;
      }
      void mark_removed(int lit) {
        mark_elim(lit);
        mark_block(-lit);
      }
      void mark_removed(Clause *, int except = 0);
  
      // The following two functions are only used for testing & debugging.
  
      bool marked_block(int lit) const {
        const Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        return (f.block & bit) != 0;
      }
      void unmark_block(int lit) {
        Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        f.block &= ~bit;
      }
  
      // During scheduling literals for blocked clause elimination we skip those
      // literals which occur negated in a too large clause.
      //
      void mark_skip(int lit) {
        Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        if (f.skip & bit)
          return;
        LOG("marking %d to be skipped as blocking literal", lit);
        f.skip |= bit;
      }
      bool marked_skip(int lit) {
        const Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        return (f.skip & bit) != 0;
      }
  
      // Blocked Clause elimination in 'block.cpp'.
      //
      bool is_blocked_clause(Clause * c, int pivot);
      void block_schedule(Blocker &);
      size_t block_candidates(Blocker &, int lit);
      Clause *block_impossible(Blocker &, int lit);
      void block_literal_with_at_least_two_negative_occs(Blocker &, int lit);
      void block_literal_with_one_negative_occ(Blocker &, int lit);
      void block_pure_literal(Blocker &, int lit);
      void block_reschedule_clause(Blocker &, int lit, Clause *);
      void block_reschedule(Blocker &, int lit);
      void block_literal(Blocker &, int lit);
      bool block();
  
      // Find gates in 'gates.cpp' for bounded variable substitution.
      //
      int second_literal_in_binary_clause(Eliminator &, Clause *, int first);
      void mark_binary_literals(Eliminator &, int pivot);
      void find_and_gate(Eliminator &, int pivot);
      void find_equivalence(Eliminator &, int pivot);
  
      bool get_ternary_clause(Clause *, int &, int &, int &);
      bool match_ternary_clause(Clause *, int, int, int);
      Clause *find_ternary_clause(int, int, int);
  
      bool get_clause(Clause *, vector<int> &);
      bool is_clause(Clause *, const vector<int> &);
      Clause *find_clause(const vector<int> &);
      void find_xor_gate(Eliminator &, int pivot);
  
      void find_if_then_else(Eliminator &, int pivot);
  
      void find_gate_clauses(Eliminator &, int pivot);
      void unmark_gate_clauses(Eliminator &);
  
      // Bounded variable elimination in 'elim.cpp'.
      //
      bool eliminating();
      double compute_elim_score(unsigned lit);
      void mark_redundant_clauses_with_eliminated_variables_as_garbage();
      void unmark_binary_literals(Eliminator &);
      bool resolve_clauses(Eliminator &, Clause *, int pivot, Clause *, bool);
      void mark_eliminated_clauses_as_garbage(Eliminator &, int pivot);
      bool elim_resolvents_are_bounded(Eliminator &, int pivot);
      void elim_update_removed_lit(Eliminator &, int lit);
      void elim_update_removed_clause(Eliminator &, Clause *, int except = 0);
      void elim_update_added_clause(Eliminator &, Clause *);
      void elim_add_resolvents(Eliminator &, int pivot);
      void elim_backward_clause(Eliminator &, Clause *);
      void elim_backward_clauses(Eliminator &);
      void elim_propagate(Eliminator &, int unit);
      void elim_on_the_fly_self_subsumption(Eliminator &, Clause *, int);
      void try_to_eliminate_variable(Eliminator &, int pivot);
      void increase_elimination_bound();
      int elim_round(bool &completed);
      void elim(bool update_limits = true);
  
      void inst_assign(int lit);
      bool inst_propagate();
      void collect_instantiation_candidates(Instantiator &);
      bool instantiate_candidate(int lit, Clause *);
      void instantiate(Instantiator &);
  
      // Hyper ternary resolution.
      //
      bool ternary_find_binary_clause(int, int);
      bool ternary_find_ternary_clause(int, int, int);
      Clause *new_hyper_ternary_resolved_clause(bool red);
      bool hyper_ternary_resolve(Clause *, int, Clause *);
      void ternary_lit(int pivot, int64_t &steps, int64_t &htrs);
      void ternary_idx(int idx, int64_t &steps, int64_t &htrs);
      bool ternary_round(int64_t & steps, int64_t & htrs);
      bool ternary();
  
      // Probing in 'probe.cpp'.
      //
      bool probing();
      void failed_literal(int lit);
      void probe_assign_unit(int lit);
      void probe_assign_decision(int lit);
      void probe_assign(int lit, int parent);
      void mark_duplicated_binary_clauses_as_garbage();
      int get_parent_reason_literal(int lit);
      void set_parent_reason_literal(int lit, int reason);
      int probe_dominator(int a, int b);
      int hyper_binary_resolve(Clause *);
      void probe_propagate2();
      bool probe_propagate();
      bool is_binary_clause(Clause * c, int &, int &);
      void generate_probes();
      void flush_probes();
      int next_probe();
      bool probe_round();
      void probe(bool update_limits = true);
  
      // ProbSAT/WalkSAT implementation called initially or from 'rephase'.
      //
      void walk_save_minimum(Walker &);
      Clause *walk_pick_clause(Walker &);
      unsigned walk_break_value(int lit);
      int walk_pick_lit(Walker &, Clause *);
      void walk_flip_lit(Walker &, int lit);
      int walk_round(int64_t limit, bool prev);
      void walk();
  
      // Detect strongly connected components in the binary implication graph
      // (BIG) and equivalent literal substitution (ELS) in 'decompose.cpp'.
      //
      bool decompose_round();
      void decompose();
  
      void reset_limits();      // Reset after 'solve' call.
  
      // Assumption handling.
      //
      void assume(int);         // New assumption literal.
      bool failed(int lit);     // Literal failed assumption?
      void reset_assumptions(); // Reset after 'solve' call.
      void failing();           // Prepare failed assumptions.
  
      bool assumed(int lit) {   // Marked as assumption.
        Flags &f = flags(lit);
        const unsigned bit = bign(lit);
        return (f.assumed & bit) != 0;
      }
  
      // Add temporary clause as constraint.
      //
      void constrain(int);      // Add literal to constraint.
      bool failed_constraint(); // Was constraint used to proof unsatisfiablity?
      void reset_constraint();  // Reset after 'solve' call.
  
      // Forcing decision variables to a certain phase.
      //
      void phase(int lit);
      void unphase(int lit);
  
      // Globally blocked clause elimination.
      //
      bool is_autarky_literal(int lit) const;
      bool is_conditional_literal(int lit) const;
      void mark_as_conditional_literal(int lit);
      void unmark_as_conditional_literal(int lit);
      //
      bool is_in_candidate_clause(int lit) const;
      void mark_in_candidate_clause(int lit);
      void unmark_in_candidate_clause(int lit);
      //
      void condition_assign(int lit);
      void condition_unassign(int lit);
      //
      bool conditioning();
      long condition_round(long unassigned_literal_propagation_limit);
      void condition(bool update_limits = true);
  
      // Part on picking the next decision in 'decide.cpp'.
      //
      bool satisfied();
      int next_decision_variable_on_queue();
      int next_decision_variable_with_best_score();
      int next_decision_variable();
      int decide_phase(int idx, bool target);
      int likely_phase(int idx);
      int decide(); // 0=decision, 20=failed
  
      // Internal functions to enable explicit search limits.
      //
      void limit_terminate(int);
      void limit_decisions(int);     // Force decision limit.
      void limit_conflicts(int);     // Force conflict limit.
      void limit_preprocessing(int); // Enable 'n' preprocessing rounds.
      void limit_local_search(int);  // Enable 'n' local search rounds.
  
      // External versions can access limits by 'name'.
      //
      static bool is_valid_limit(const char *name);
      bool limit(const char *name, int); // 'true' if 'name' valid
  
      // Set all the CDCL search limits and increments for scheduling
      // inprocessing, restarts, clause database reductions, etc.
      //
      void init_report_limits();
      void init_preprocessing_limits();
      void init_search_limits();
  
      // The computed averages are local to the 'stable' and 'unstable' phase.
      // Their main use is to be reported in 'report', except for the 'glue'
      // averages, which are used to schedule (prohibit actually) restarts
      // during 'unstable' phases ('stable' phases use reluctant doubling).
      //
      void init_averages();
      void swap_averages();
  
      int try_to_satisfy_formula_by_saved_phases();
      void produce_failed_assumptions();
  
      // Main solve & search functions in 'internal.cpp'.
      //
      // We have three pre-solving techniques.  These consist of preprocessing,
      // local search and searching for lucky phases, which in full solving
      // mode except for the last are usually optional and then followed by
      // the main CDCL search loop with inprocessing.  If only preprocessing
      // is requested from 'External::simplifiy' only preprocessing is called
      // though. This is all orchestrated by the 'solve' function.
      //
      int already_solved();
      int restore_clauses();
      bool preprocess_round(int round);
      int preprocess();
      int local_search_round(int round);
      int local_search();
      int lucky_phases();
      int cdcl_loop_with_inprocessing();
      void reset_solving();
      int solve(bool preprocess_only = false);
  
      //
      int lookahead();
      CubesWithStatus generate_cubes(int, int);
      int most_occurring_literal();
      int lookahead_probing();
      int lookahead_next_probe();
      void lookahead_flush_probes();
      void lookahead_generate_probes();
      std::vector<int> lookahead_populate_locc();
      int lookahead_locc(const std::vector<int> &);
  
      bool terminating_asked();
  
  #ifndef QUIET
    // Built in profiling in 'profile.cpp' (see also 'profile.hpp').
    //
    void start_profiling (Profile & p, double);
    void stop_profiling (Profile & p, double);
  
    double update_profiles ();    // Returns 'time ()'.
    void print_profile ();
  #endif
  
    // Get the value of an internal literal: -1=false, 0=unassigned, 1=true.
    // We use a redundant table for both negative and positive literals.  This
    // allows a branch-less check for the value of literal and is considered
    // substantially faster than negating the result if the argument is
    // negative.  We also avoid taking the absolute value.
    //
    signed char val (int lit) const {
      assert (-max_var <= lit);
      assert (lit);
      assert (lit <= max_var);
      return vals[lit];
    }
  
    // As 'val' but restricted to the root-level value of a literal.
    // It is not that time critical and also needs to check the decision level
    // of the variable anyhow.
    //
    int fixed (int lit) {
      assert (-max_var <= lit);
      assert (lit);
      assert (lit <= max_var);
      const int idx = vidx (lit);
      int res = vals[idx];
      if (res && vtab[idx].level) res = 0;
      if (lit < 0) res = -res;
      return res;
    }
  
    // Map back an internal literal to an external.
    //
    int externalize (int lit) {
      assert (lit != INT_MIN);
      const int idx = abs (lit);
      assert (idx);
      assert (idx <= max_var);
      int res = i2e[idx];
      if (lit < 0) res = -res;
      return res;
    }
  
    // Explicit freezing and melting of variables.
    //
    void freeze (int lit) {
      int idx = vidx (lit);
      unsigned & ref = frozentab[idx];
      if (ref < UINT_MAX) {
        ref++;
        LOG ("variable %d frozen %u times", idx, ref);
      } else LOG ("variable %d remains frozen forever", idx);
    }
    void melt (int lit) {
      int idx = vidx (lit);
      unsigned & ref = frozentab[idx];
      if (ref < UINT_MAX) {
        if (!--ref) {
          LOG ("variable %d completely molten", idx);
        } else
          LOG ("variable %d melted once but remains frozen %u times",
            lit, ref);
      } else LOG ("variable %d remains frozen forever", idx);
    }
    bool frozen (int lit) { return frozentab[vidx (lit)] > 0; }
  
    // Parsing functions in 'parse.cpp'.
    //
    const char * parse_dimacs (FILE *);
    const char * parse_dimacs (const char *);
    const char * parse_solution (const char *);
  
    // Enable and disable proof logging and checking.
    //
    void new_proof_on_demand ();
    void close_trace ();          // Stop proof tracing.
    void flush_trace ();          // Flush proof trace file.
    void trace (File *);          // Start write proof file.
    void check ();                // Enable online proof checking.
  
    // Dump to '<stdout>' as DIMACS for debugging.
    //
    void dump (Clause *);
    void dump ();
  
    // Export and traverse all irredundant (non-unit) clauses.
    //
    bool traverse_clauses (ClauseIterator &);
  
    /*----------------------------------------------------------------------*/
  
    double solve_time ();         // accumulated time spent in 'solve ()'
  
    double process_time ();       // since solver was initialized
    double real_time ();          // since solver was initialized
  
    double time () {
      return opts.realtime ? real_time () : process_time ();
    }
  
    // Regularly reports what is going on in 'report.cpp'.
    //
    void report (char type, int verbose_level = 0);
    void report_solving(int);
  
    void print_statistics ();
    void print_resource_usage ();
  
    /*----------------------------------------------------------------------*/
  
  #ifndef QUIET
  
    void print_prefix ();
  
    // Non-verbose messages and warnings, i.e., always printed unless 'quiet'
    // is set, which disables messages at run-time, or even 'QUIET' is defined
    // through the configuration option './configure --quiet', which disables
    // such messages completely at compile-time.
    //
    void vmessage (const char *, va_list &);
    void message (const char *, ...)
                  CADICAL_ATTRIBUTE_FORMAT (2, 3);
    void message ();                              // empty line
  
    // Verbose messages with explicit verbose 'level' controlled by
    // 'opts.verbose' (verbose level '0' gives the same as 'message').
    //
    void vverbose (int level, const char * fmt, va_list &);
    void verbose (int level, const char * fmt, ...)
                  CADICAL_ATTRIBUTE_FORMAT (3, 4);
    void verbose (int level);
  
    // This is for printing section headers in the form
    //
    //  c ---- [ <title> ] ---------------------
    //
    // nicely aligned (and of course is ignored if 'quiet' is set).
    //
    void section (const char * title);
  
    // Print verbose message about phases if 'opts.verbose > 1' (but not if
    // 'quiet' is set).  Note that setting 'log' or '-l' forces all verbose
    // output (and also ignores 'quiet' set to true').  The 'phase' argument
    // is used to print a 'phase' prefix for the message as follows:
    //
    //  c [<phase>] ...
    //
    void phase (const char * phase, const char *, ...)
                CADICAL_ATTRIBUTE_FORMAT (3, 4);
  
    // Same as the last 'phase' above except that the prefix gets a count:
    //
    //  c [<phase>-<count>] ...
    //
    void phase (const char * phase, int64_t count, const char *, ...)
                CADICAL_ATTRIBUTE_FORMAT (4, 5);
  #endif
  
    // Print error messages which are really always printed (even if 'quiet'
    // is set).  This leads to exit the current process with exit status '1'.
    //
    // TODO add possibility to use a call back instead of calling exit.
    //
    void error_message_end ();
    void verror (const char *, va_list &);
    void error (const char *, ...)
                CADICAL_ATTRIBUTE_FORMAT (2, 3);
    void error_message_start ();
  
    // Warning messages.
    //
    void warning (const char *, ...)
                  CADICAL_ATTRIBUTE_FORMAT (2, 3);
    };
  
  // Fatal internal error which leads to abort.
  //
  void fatal_message_start ();
  void fatal_message_end ();
  void fatal (const char *, ...)
              CADICAL_ATTRIBUTE_FORMAT (1, 2);
  
  /*------------------------------------------------------------------------*/
  
  // Has to be put here, i.e., not into 'score.hpp', since we need the
  // definition of 'Internal::score' above (after '#include "score.hpp"').
  
  inline bool score_smaller::operator () (unsigned a, unsigned b) {
  
    // Avoid computing twice 'abs' in 'score ()'.
    //
    assert (1 <= a);
    assert (a <= (unsigned) internal->max_var);
    assert (1 <= b);
    assert (b <= (unsigned) internal->max_var);
    double s = internal->stab[a];
    double t = internal->stab[b];
  
    if (s < t) return true;
    if (s > t) return false;
  
    return a > b;
  }
  
  /*------------------------------------------------------------------------*/
  
  // Implemented here for keeping it all inline (requires Internal::fixed).
  
  inline int External::fixed (int elit) const {
    assert (elit);
    assert (elit != INT_MIN);
    int eidx = abs (elit);
    if (eidx > max_var) return 0;
    int ilit = e2i [eidx];
    if (!ilit) return 0;
    if (elit < 0) ilit = -ilit;
    return internal->fixed (ilit);
  }
  
  /*------------------------------------------------------------------------*/
  
  // We want to have termination checks inlined, particularly the first
  // function which appears in preprocessor loops.  Even though this first
  // 'termination_forced' is set asynchronously, this should not lead to a
  // data race issue (it also has been declared 'volatile').
  
  inline bool Internal::terminated_asynchronously (int factor)
  {
    // First way of asynchronous termination is through 'terminate' which sets
    // the 'termination_forced' flag directly.  The second way is through a
    // call back to a 'terminator' if it is non-zero, which however is costly.
    //
    if (termination_forced)
    {
      LOG ("termination asynchronously forced");
      return true;
    }
  
    // This is only for testing and debugging asynchronous termination calls.
    // In production code this could be removed but then should not be costly
    // and keeping it will allow to test correctness of asynchronous
    // termination on the production platform too.  After this triggers we
    // have to set the 'termination_forced' flag, such that subsequent calls
    // to this function do not check this again.
    //
    if (lim.terminate.forced) {
      assert (lim.terminate.forced > 0);
      if (lim.terminate.forced-- == 1) {
        LOG ("internally forcing termination");
        termination_forced = true;
        return true;
      }
      LOG ("decremented internal forced termination limit to %d",
        lim.terminate.forced);
    }
  
    // The second way of asynchronous termination is through registering and
    // calling an external 'Terminator' object.  This is of course more costly
    // than just checking a (volatile though) boolean flag, particularly in
    // tight loops.  To avoid this cost we only call the terminator in
    // intervals of 'opts.terminateint', which in addition can be scaled up by
    // the argument 'factor'.  If the terminator returns 'true' we set the
    // 'termination_forced' flag to 'true' in order to remember the
    // termination status and to avoid the terminator again.  Setting this
    // flag leads to the first test above to succeed in subsequent calls.
    //
    if (external->terminator && !lim.terminate.check--) {
      assert (factor > 0);
      assert (INT_MAX/factor > opts.terminateint);
      lim.terminate.check = factor * opts.terminateint;
      if (external->terminator->terminate ()) {
        termination_forced = true;                        // Cache it.
        LOG ("connected terminator forces termination");
        return true;
      }
    }
  
    return false;
  }
  
  /*------------------------------------------------------------------------*/
  
  inline bool Internal::search_limits_hit ()
  {
    assert (!preprocessing);
    assert (!localsearching);
  
    if (lim.conflicts >= 0 &&
        stats.conflicts >= lim.conflicts) {
      LOG ("conflict limit %" PRId64 " reached", lim.conflicts);
      return true;
    }
  
    if (lim.decisions >= 0 &&
        stats.decisions >= lim.decisions) {
      LOG ("decision limit %" PRId64 " reached", lim.decisions);
      return true;
    }
  
    return false;
  }
  
  /*------------------------------------------------------------------------*/
  
  }
  
  #endif
  