text: #include "internal.hpp"
  
  /*------------------------------------------------------------------------*/
  
  namespace CaDiCaL {
  
  /*------------------------------------------------------------------------*/
  
  // See corresponding header file 'cadical.hpp' (!) for more information.
  //
  // Again, to avoid confusion, note that, 'cadical.hpp' is the header file of
  // this file 'solver.cpp', since we want to call the application and main
  // file 'cadical.cpp', while at the same time using 'cadical.hpp' as the
  // main header file of the library (and not 'solver.hpp').
  
  /*------------------------------------------------------------------------*/
  #ifdef LOGGING
  
  // Needs to be kept in sync with the color schemes used in 'logging.cpp'.
  //
  #define api_code blue_code              // API call color
  #define log_code magenta_code           // standard/default logging color
  #define emph_code bright_magenta_code   // emphasized logging color
  
  #endif
  /*------------------------------------------------------------------------*/
  
  // Log state transitions.
  
  #define STATE(S) \
  do { \
    assert (is_power_of_two (S)); \
    if (_state == S) break; \
    _state = S; \
    LOG ("API enters state %s" #S "%s", \
      tout.emph_code (), tout.normal_code ()); \
  } while (0)
  
  void Solver::transition_to_unknown_state () {
    if (state () == CONFIGURING) {
      LOG ("API leaves state %sCONFIGURING%s",
        tout.emph_code (), tout.normal_code ());
      if (internal->opts.check &&
          internal->opts.checkproof) {
        internal->check ();
      }
    } else if (state () == SATISFIED) {
      LOG ("API leaves state %sSATISFIED%s",
        tout.emph_code (), tout.normal_code ());
      external->reset_assumptions ();
      external->reset_constraint ();
    } else if (state () == UNSATISFIED) {
      LOG ("API leaves state %sUNSATISFIED%s",
        tout.emph_code (), tout.normal_code ());
      external->reset_assumptions ();
      external->reset_constraint ();
    }
    if (state () != UNKNOWN) STATE (UNKNOWN);
  }
  
  /*------------------------------------------------------------------------*/
  #ifdef LOGGING
  /*------------------------------------------------------------------------*/
  
  // The following logging code is useful for debugging mostly (or trying to
  // understand what the solver is actually doing).  It needs to be enabled
  // during configuration using the '-l' option for './configure', which
  // forces 'LOGGING' to be defined during compilation.  This includes all the
  // logging code, which then still needs to enabled during run-time with the
  // '-l' or 'log' option.
  
  static void
  log_api_call (Internal * internal,
    const char * name, const char * suffix) {
    Logger::log (internal, "API call %s'%s ()'%s %s",
      tout.api_code (), name, tout.log_code (), suffix);
  }
  
  static void
  log_api_call (Internal * internal,
    const char * name, int arg, const char * suffix) {
    Logger::log (internal, "API call %s'%s (%d)'%s %s",
      tout.api_code (), name, arg, tout.log_code (), suffix);
  }
  
  static void
  log_api_call (Internal * internal,
    const char * name, const char * arg, const char * suffix) {
    Logger::log (internal, "API call %s'%s (\"%s\")'%s %s",
      tout.api_code (), name, arg, tout.log_code (), suffix);
  }
  
  static void
  log_api_call (Internal * internal,
    const char * name, const char * a1, int a2, const char * s) {
    Logger::log (internal, "API call %s'%s (\"%s\", %d)'%s %s",
      tout.api_code (), name, a1, a2, tout.log_code (), s);
  }
  
  /*------------------------------------------------------------------------*/
  
  // We factored out API call begin/end logging and use overloaded functions.
  
  static void
  log_api_call_begin (Internal * internal, const char * name) {
    Logger::log_empty_line (internal);
    log_api_call (internal, name, "started");
  }
  
  static void
  log_api_call_begin (Internal * internal, const char * name, int arg) {
    Logger::log_empty_line (internal);
    log_api_call (internal, name, arg, "started");
  }
  
  static void
  log_api_call_begin (Internal * internal,
                      const char * name, const char * arg) {
    Logger::log_empty_line (internal);
    log_api_call (internal, name, arg, "started");
  }
  
  static void
  log_api_call_begin (Internal * internal, const char * name,
                      const char * arg1, int arg2) {
    Logger::log_empty_line (internal);
    log_api_call (internal, name, arg1, arg2, "started");
  }
  
  /*------------------------------------------------------------------------*/
  
  static void
  log_api_call_end (Internal * internal, const char * name)
  {
    log_api_call (internal, name, "succeeded");
  }
  
  static void
  log_api_call_end (Internal * internal, const char * name, int lit) {
    log_api_call (internal, name, lit, "succeeded");
  }
  
  static void
  log_api_call_end (Internal * internal,
                      const char * name, const char * arg) {
    Logger::log_empty_line (internal);
    log_api_call (internal, name, arg, "succeeded");
  }
  
  static void
  log_api_call_end (Internal * internal, const char * name,
                    const char * arg,
                    bool res)
  {
    log_api_call (internal, name, arg, res ? "succeeded" : "failed");
  }
  
  static void
  log_api_call_end (Internal * internal, const char * name,
                    const char * arg, int val,
                    bool res)
  {
    log_api_call (internal, name, arg, val, res ? "succeeded" : "failed");
  }
  
  static void
  log_api_call_returns (Internal * internal, const char * name, bool res) {
    log_api_call (internal, name,
      res ? "returns 'true'" : "returns 'false'");
  }
  
  static void
  log_api_call_returns (Internal * internal, const char * name, int res) {
    char fmt[32];
    sprintf (fmt, "returns '%d'", res);
    log_api_call (internal, name, fmt);
  }
  
  static void
  log_api_call_returns (Internal * internal, const char * name, int64_t res) {
    char fmt[32];
    sprintf (fmt, "returns '%" PRId64 "'", res);
    log_api_call (internal, name, fmt);
  }
  
  static void
  log_api_call_returns (Internal * internal,
                        const char * name, int lit, int res) {
    char fmt[32];
    sprintf (fmt, "returns '%d'", res);
    log_api_call (internal, name, lit, fmt);
  }
  
  static void
  log_api_call_returns (Internal * internal,
                        const char * name, const char * arg, bool res) {
    log_api_call (internal, name, arg,
      res ? "returns 'true'" : "returns 'false'");
  }
  
  static void
  log_api_call_returns (Internal * internal,
                        const char * name, int lit, bool res) {
    log_api_call (internal, name, lit,
      res ? "returns 'true'" : "returns 'false'");
  }
  
  static void
  log_api_call_returns (Internal * internal,
    const char * name, const char * arg, const char * res) {
    Logger::log (internal, "API call %s'%s (\"%s\")'%s returns '%s'",
      tout.api_code (), name, arg, tout.log_code (), res ? res : "<null>");
  }
  
  static void
  log_api_call_returns (Internal * internal,
    const char * name, const char * arg1, int arg2, const char * res) {
    Logger::log (internal, "API call %s'%s (\"%s\", %d)'%s returns '%s'",
      tout.api_code (), name, arg1, arg2, tout.log_code (),
      res ? res : "<null>");
  }
  
  /*------------------------------------------------------------------------*/
  
  #define LOG_API_CALL_BEGIN(...) \
  do { \
    if (!internal->opts.log) break; \
    log_api_call_begin (internal, __VA_ARGS__); \
  } while (0)
  
  #define LOG_API_CALL_END(...) \
  do { \
    if (!internal->opts.log) break; \
    log_api_call_end (internal, __VA_ARGS__); \
  } while (0)
  
  #define LOG_API_CALL_RETURNS(...) \
  do { \
    if (!internal->opts.log) break; \
    log_api_call_returns (internal, __VA_ARGS__); \
  } while (0)
  
  /*------------------------------------------------------------------------*/
  #else   // end of 'then' part of 'ifdef LOGGING'
  /*------------------------------------------------------------------------*/
  
  #define LOG_API_CALL_BEGIN(...) do { } while (0)
  #define LOG_API_CALL_END(...) do { } while (0)
  #define LOG_API_CALL_RETURNS(...) do { } while (0)
  
  /*------------------------------------------------------------------------*/
  #endif  // end of 'else' part of 'ifdef LOGGING'
  /*------------------------------------------------------------------------*/
  
  /*------------------------------------------------------------------------*/
  #ifndef NTRACING
  /*------------------------------------------------------------------------*/
  
  #define TRACE(...) \
  do { \
    if ((this == 0)) break; \
    if ((internal == 0)) break; \
    LOG_API_CALL_BEGIN (__VA_ARGS__); \
    if (!trace_api_file) break; \
    trace_api_call (__VA_ARGS__); \
  } while (0)
  
  void Solver::trace_api_call (const char * s0) const {
    assert (trace_api_file);
    LOG ("TRACE %s", s0);
    fprintf (trace_api_file, "%s\n", s0);
    fflush (trace_api_file);
  }
  
  void Solver::trace_api_call (const char * s0, int i1) const {
    assert (trace_api_file);
    LOG ("TRACE %s %d", s0, i1);
    fprintf (trace_api_file, "%s %d\n", s0, i1);
    fflush (trace_api_file);
  }
  
  void
  Solver::trace_api_call (const char * s0, const char * s1, int i2) const {
    assert (trace_api_file);
    LOG ("TRACE %s %s %d", s0, s1, i2);
    fprintf (trace_api_file, "%s %s %d\n", s0, s1, i2);
    fflush (trace_api_file);
  }
  
  /*------------------------------------------------------------------------*/
  
  // The global 'tracing_api_calls_through_environment_variable_method' flag
  // is used to ensure that only one solver traces to a file.  Otherwise the
  // method to use an environment variable to point to the trace file is
  // bogus, since those different solver instances would all write to the same
  // file producing garbage.  A more sophisticated solution would use a
  // different mechanism to tell the solver to which file to trace to, but in
  // our experience it is quite convenient to get traces out of applications
  // which use the solver as library by just setting an environment variable
  // without requiring to change any application code.
  //
  static bool tracing_api_calls_through_environment_variable_method;
  
  /*------------------------------------------------------------------------*/
  #else // NTRACING
  /*------------------------------------------------------------------------*/
  
  #define TRACE(...) do { } while (0)
  
  /*------------------------------------------------------------------------*/
  #endif
  /*------------------------------------------------------------------------*/
  
  Solver::Solver () {
  
  #ifndef NTRACING
    const char * path = getenv ("CADICAL_API_TRACE");
    if (!path) path = getenv ("CADICALAPITRACE");
    if (path) {
      if (tracing_api_calls_through_environment_variable_method)
        FATAL ("can not trace API calls of two solver instances "
          "using environment variable 'CADICAL_API_TRACE'");
      if (!(trace_api_file = fopen (path, "w")))
        FATAL ("failed to open file '%s' to trace API calls "
          "using environment variable 'CADICAL_API_TRACE'", path);
      close_trace_api_file = true;
      tracing_api_calls_through_environment_variable_method = true;
    } else {
      tracing_api_calls_through_environment_variable_method = false;
      close_trace_api_file = false;
      trace_api_file = 0;
    }
  #endif
  
    adding_clause     = false;
    adding_constraint = false;
    _state = INITIALIZING;
    internal = new Internal ();
    TRACE ("init");
    external = new External (internal);
    STATE (CONFIGURING);
  #ifndef NTRACING
    if (tracing_api_calls_through_environment_variable_method)
      message ("tracing API calls to '%s'", path);
  #endif
  }
  
  Solver::~Solver () {
  
    TRACE ("reset");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    STATE (DELETING);
  
  #ifdef LOGGING
    //
    // After deleting 'internal' logging does not work anymore.
    //
    bool logging = internal->opts.log;
    int level = internal->level;
    string prefix = internal->prefix;
  #endif
  
    delete internal;
    delete external;
  
  #ifndef NTRACING
    if (close_trace_api_file) {
      close_trace_api_file = false;
      assert (trace_api_file);
      assert (tracing_api_calls_through_environment_variable_method);
      fclose (trace_api_file);
      tracing_api_calls_through_environment_variable_method = false;
    }
  #endif
  
  #ifdef LOGGING
    //
    // Need to log success of this API call manually.
    //
    if (logging) {
      printf ("%s%sLOG %s%d%s API call %s'reset ()'%s succeeded%s\n",
        prefix.c_str (),
        tout.log_code (),
        tout.emph_code (),
        level,
        tout.log_code (),
        tout.api_code (),
        tout.log_code (),
        tout.normal_code ());
      fflush (stdout);
    }
  #endif
  }
  
  /*------------------------------------------------------------------------*/
  
  int Solver::vars () {
    TRACE ("vars");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    int res = external->max_var;
    LOG_API_CALL_RETURNS ("vars", res);
    return res;
  }
  
  void Solver::reserve (int min_max_var) {
    TRACE ("reserve", min_max_var);
    REQUIRE_VALID_STATE ();
    transition_to_unknown_state ();
    external->reset_extended ();
    external->init (min_max_var);
    LOG_API_CALL_END ("reserve", min_max_var);
  }
  
  /*------------------------------------------------------------------------*/
  #ifndef NTRACING
  
  void Solver::trace_api_calls (FILE * file) {
    LOG_API_CALL_BEGIN ("trace_api_calls");
    REQUIRE_VALID_STATE ();
    REQUIRE (file != 0, "invalid zero file argument");
    REQUIRE (!tracing_api_calls_through_environment_variable_method,
      "already tracing API calls "
      "using environment variable 'CADICAL_API_TRACE'");
    REQUIRE (!trace_api_file, "called twice");
    trace_api_file = file;
    LOG_API_CALL_END ("trace_api_calls");
    trace_api_call ("init");
  }
  
  #endif
  /*------------------------------------------------------------------------*/
  
  bool Solver::is_valid_option (const char * name) {
    return Options::has (name);
  }
  
  bool Solver::is_preprocessing_option (const char * name) {
    return Options::is_preprocessing_option (name);
  }
  
  bool Solver::is_valid_long_option (const char * arg) {
    string name;
    int tmp;
    return Options::parse_long_option (arg, name, tmp);
  }
  
  int Solver::get (const char * arg) {
    REQUIRE_VALID_OR_SOLVING_STATE ();
    return internal->opts.get (arg);
  }
  
  bool Solver::set (const char * arg, int val) {
    TRACE ("set", arg, val);
    REQUIRE_VALID_STATE ();
    if (strcmp (arg, "log") &&
        strcmp (arg, "quiet") &&
        strcmp (arg, "report") &&
        strcmp (arg, "verbose")) {
      REQUIRE (state () == CONFIGURING,
        "can only set option 'set (\"%s\", %d)' right after initialization",
        arg, val);
    }
    bool res = internal->opts.set (arg, val);
    LOG_API_CALL_END ("set", arg, val, res);
    return res;
  }
  
  bool Solver::set_long_option (const char * arg) {
    LOG_API_CALL_BEGIN ("set", arg);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only set option '%s' right after initialization", arg);
    bool res;
    if (arg[0] != '-' || arg[1] != '-') res = false;
    else {
      int val;
      string name;
      res = Options::parse_long_option (arg, name, val);
      if (res) set (name.c_str (), val);
    }
    LOG_API_CALL_END ("set", arg, res);
    return res;
  }
  
  void Solver::optimize (int arg) {
    LOG_API_CALL_BEGIN ("optimize", arg);
    REQUIRE_VALID_STATE ();
    internal->opts.optimize (arg);
    LOG_API_CALL_END ("optimize", arg);
  }
  
  bool Solver::limit (const char * arg, int val) {
    TRACE ("limit", arg, val);
    REQUIRE_VALID_STATE ();
    bool res = internal->limit (arg, val);
    LOG_API_CALL_END ("limit", arg, val, res);
    return res;
  }
  
  bool Solver::is_valid_limit (const char * arg) {
    return Internal::is_valid_limit (arg);
  }
  
  void Solver::prefix (const char * str) {
    LOG_API_CALL_BEGIN ("prefix", str);
    REQUIRE_VALID_OR_SOLVING_STATE ();
    internal->prefix = str;
    LOG_API_CALL_END ("prefix", str);
  }
  
  bool Solver::is_valid_configuration (const char * name) {
    return Config::has (name);
  }
  
  bool Solver::configure (const char * name) {
    LOG_API_CALL_BEGIN ("configure", name);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only set configuration '%s' right after initialization", name);
    bool res = Config::set (internal->opts, name);
    LOG_API_CALL_END ("configure", name, res);
    return res;
  }
  
  /*===== IPASIR BEGIN =====================================================*/
  
  void Solver::add (int lit) {
    TRACE ("add", lit);
    REQUIRE_VALID_STATE ();
    if (lit) REQUIRE_VALID_LIT (lit);
    transition_to_unknown_state ();
    external->add (lit);
    adding_clause = lit;
    if (adding_clause) STATE (ADDING);
    else if (!adding_constraint) STATE (UNKNOWN);
    LOG_API_CALL_END ("add", lit);
  }
  
  void Solver::constrain (int lit) {
    TRACE ("constrain", lit);
    REQUIRE_VALID_STATE ();
    if (lit) REQUIRE_VALID_LIT (lit);
    transition_to_unknown_state ();
    external->constrain (lit);
    adding_constraint = lit;
    if (adding_constraint) STATE (ADDING);
    else if (!adding_clause) STATE (UNKNOWN);
    LOG_API_CALL_END ("constrain", lit);
  }
  
  void Solver::assume (int lit) {
    TRACE ("assume", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    transition_to_unknown_state ();
    external->assume (lit);
    LOG_API_CALL_END ("assume", lit);
  }
  
  int Solver::lookahead () {
    TRACE ("lookahead");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    int lit = external->lookahead ();
    TRACE ("lookahead");
    return lit;
  }
  
  Solver::CubesWithStatus Solver::generate_cubes (int depth, int min_depth) {
    TRACE ("lookahead_cubes");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    auto cubes = external->generate_cubes (depth, min_depth);
    TRACE ("lookahead_cubes");
  
    CubesWithStatus cubes2;
    cubes2.status = cubes.status;
    cubes2.cubes = cubes.cubes;
    return cubes2;
  }
  
  void Solver::reset_assumptions () {
    TRACE ("reset_assumptions");
    REQUIRE_VALID_STATE ();
    transition_to_unknown_state ();
    external->reset_assumptions ();
    LOG_API_CALL_END ("reset_assumptions");
  }
  
  void Solver::reset_constraint () {
    TRACE ("reset_constraint");
    REQUIRE_VALID_STATE ();
    transition_to_unknown_state ();
    external->reset_constraint ();
    LOG_API_CALL_END ("reset_constraint");
  }
  
  /*------------------------------------------------------------------------*/
  
  int Solver::call_external_solve_and_check_results (bool preprocess_only) {
    transition_to_unknown_state ();
    assert (state () & READY);
    STATE (SOLVING);
    const int res = external->solve (preprocess_only);
         if (res == 10) STATE (SATISFIED);
    else if (res == 20) STATE (UNSATISFIED);
    else                STATE (UNKNOWN);
  #if 0 // EXPENSIVE ALTERNATIVE ASSUMPTION CHECKING
    // This checks that the set of failed assumptions form a core using the
    // external 'copy (...)' function to copy the solver, which can be trusted
    // less, since it involves copying the extension stack too.  The
    // 'External::check_assumptions_failing' is a better alternative and can
    // be enabled by options too.  We keep this code though to have an
    // alternative failed assumption checking available for debugging.
    //
    if (res == 20 && !external->assumptions.empty ()) {
      Solver checker;
      checker.prefix ("checker ");
      copy (checker);
      for (const auto & lit : external->assumptions)
        if (failed (lit))
          checker.add (lit), checker.add (0);
      if (checker.solve () != 20)
        FATAL ("copying assumption checker failed");
    }
  #endif
    if (!res) external->reset_assumptions ();
    return res;
  }
  
  int Solver::solve () {
    TRACE ("solve");
    REQUIRE_READY_STATE ();
    const int res = call_external_solve_and_check_results (false);
    LOG_API_CALL_RETURNS ("solve", res);
    return res;
  }
  
  int Solver::simplify (int rounds) {
    TRACE ("simplify", rounds);
    REQUIRE_READY_STATE ();
    REQUIRE (rounds >= 0,
      "negative number of simplification rounds '%d'", rounds);
    internal->limit ("preprocessing", rounds);
    const int res = call_external_solve_and_check_results (true);
    LOG_API_CALL_RETURNS ("simplify", rounds, res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  int Solver::val (int lit) {
    TRACE ("val", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    REQUIRE (state () == SATISFIED,
      "can only get value in satisfied state");
    if (!external->extended) external->extend ();
    int res = external->ival (lit);
    LOG_API_CALL_RETURNS ("val", lit, res);
    return res;
  }
  
  bool Solver::failed (int lit) {
    TRACE ("failed", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    REQUIRE (state () == UNSATISFIED,
      "can only get failed assumptions in unsatisfied state");
    bool res = external->failed (lit);
    LOG_API_CALL_RETURNS ("failed", lit, res);
    return res;
  }
  
  bool Solver::constraint_failed () {
    TRACE ("constraint_failed");
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == UNSATISFIED,
      "can only determine if constraint failed in unsatisfied state");
    bool res = external->failed_constraint ();
    LOG_API_CALL_RETURNS ("constraint_failed", res);
    return res;
  }
  
  int Solver::fixed (int lit) const {
    TRACE ("fixed", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    int res = external->fixed (lit);
    LOG_API_CALL_RETURNS ("fixed", lit, res);
    return res;
  }
  
  void Solver::phase (int lit) {
    TRACE ("phase", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    external->phase (lit);
    LOG_API_CALL_END ("phase", lit);
  }
  
  void Solver::unphase (int lit) {
    TRACE ("unphase", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    external->unphase (lit);
    LOG_API_CALL_END ("unphase", lit);
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::terminate () {
    LOG_API_CALL_BEGIN ("terminate");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    external->terminate ();
    LOG_API_CALL_END ("terminate");
  }
  
  void Solver::connect_terminator (Terminator * terminator) {
    LOG_API_CALL_BEGIN ("connect_terminator");
    REQUIRE_VALID_STATE ();
    REQUIRE (terminator, "can not connect zero terminator");
  #ifdef LOGGING
    if (external->terminator)
      LOG ("connecting new terminator (disconnecting previous one)");
    else
      LOG ("connecting new terminator (no previous one)");
  #endif
    external->terminator = terminator;
    LOG_API_CALL_END ("connect_terminator");
  }
  
  void Solver::disconnect_terminator () {
    LOG_API_CALL_BEGIN ("disconnect_terminator");
    REQUIRE_VALID_STATE ();
  #ifdef LOGGING
      if (external->terminator)
        LOG ("disconnecting previous terminator");
      else
        LOG ("ignoring to disconnect terminator (no previous one)");
  #endif
    external->terminator = 0;
    LOG_API_CALL_END ("disconnect_terminator");
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::connect_learner (Learner * learner) {
    LOG_API_CALL_BEGIN ("connect_learner");
    REQUIRE_VALID_STATE ();
    REQUIRE (learner, "can not connect zero learner");
  #ifdef LOGGING
    if (external->learner)
      LOG ("connecting new learner (disconnecting previous one)");
    else
      LOG ("connecting new learner (no previous one)");
  #endif
    external->learner = learner;
    LOG_API_CALL_END ("connect_learner");
  }
  
  void Solver::disconnect_learner () {
    LOG_API_CALL_BEGIN ("disconnect_learner");
    REQUIRE_VALID_STATE ();
  #ifdef LOGGING
      if (external->learner)
        LOG ("disconnecting previous learner");
      else
        LOG ("ignoring to disconnect learner (no previous one)");
  #endif
    external->learner = 0;
    LOG_API_CALL_END ("disconnect_learner");
  }
  
  /*===== IPASIR END =======================================================*/
  
  int Solver::active () const {
    TRACE ("active");
    REQUIRE_VALID_STATE ();
    int res = internal->active ();
    LOG_API_CALL_RETURNS ("active", res);
    return res;
  }
  
  int64_t Solver::redundant () const {
    TRACE ("redundant");
    REQUIRE_VALID_STATE ();
    int64_t res = internal->redundant ();
    LOG_API_CALL_RETURNS ("redundant", res);
    return res;
  }
  
  int64_t Solver::irredundant () const {
    TRACE ("irredundant");
    REQUIRE_VALID_STATE ();
    int64_t res = internal->irredundant ();
    LOG_API_CALL_RETURNS ("irredundant", res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::freeze (int lit) {
    TRACE ("freeze", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    external->freeze (lit);
    LOG_API_CALL_END ("freeze", lit);
  }
  
  void Solver::melt (int lit) {
    TRACE ("melt", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    REQUIRE (external->frozen (lit),
      "can not melt completely melted literal '%d'", lit);
    external->melt (lit);
    LOG_API_CALL_END ("melt", lit);
  }
  
  bool Solver::frozen (int lit) const {
    TRACE ("frozen", lit);
    REQUIRE_VALID_STATE ();
    REQUIRE_VALID_LIT (lit);
    bool res = external->frozen (lit);
    LOG_API_CALL_RETURNS ("frozen", lit, res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  bool Solver::trace_proof (FILE * external_file, const char * name) {
    LOG_API_CALL_BEGIN ("trace_proof", name);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only start proof tracing to '%s' right after initialization",
      name);
    REQUIRE (!internal->tracer, "already tracing proof");
    File * internal_file = File::write (internal, external_file, name);
    assert (internal_file);
    internal->trace (internal_file);
    LOG_API_CALL_RETURNS ("trace_proof", name, true);
    return true;
  }
  
  bool Solver::trace_proof (const char * path) {
    LOG_API_CALL_BEGIN ("trace_proof", path);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only start proof tracing to '%s' right after initialization",
      path);
    REQUIRE (!internal->tracer, "already tracing proof");
    File * internal_file = File::write (internal, path);
    bool res = (internal_file != 0);
    internal->trace (internal_file);
    LOG_API_CALL_RETURNS ("trace_proof", path, res);
    return res;
  }
  
  void Solver::flush_proof_trace () {
    LOG_API_CALL_BEGIN ("flush_proof_trace");
    REQUIRE_VALID_STATE ();
    REQUIRE (internal->tracer, "proof is not traced");
    REQUIRE (!internal->tracer->closed (), "proof trace already closed");
    internal->flush_trace ();
    LOG_API_CALL_END ("flush_proof_trace");
  }
  
  void Solver::close_proof_trace () {
    LOG_API_CALL_BEGIN ("close_proof_trace");
    REQUIRE_VALID_STATE ();
    REQUIRE (internal->tracer, "proof is not traced");
    REQUIRE (!internal->tracer->closed (), "proof trace already closed");
    internal->close_trace ();
    LOG_API_CALL_END ("close_proof_trace");
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::build (FILE * file, const char * prefix) {
  
    assert (file == stdout || file == stderr);
  
    Terminal * terminal;
  
    if (file == stdout) terminal = &tout;
    else if (file == stderr) terminal = &terr;
    else terminal = 0;
  
    const char * v = CaDiCaL::version ();
    const char * i = identifier ();
    const char * c = compiler ();
    const char * b = date ();
    const char * f = flags ();
  
    assert (v);
  
    fputs (prefix, file);
    if (terminal) terminal->magenta ();
    fputs ("Version ", file);
    if (terminal) terminal->normal ();
    fputs (v, file);
    if (i) {
      if (terminal) terminal->magenta ();
      fputc (' ', file);
      fputs (i, file);
      if (terminal) terminal->normal ();
    }
    fputc ('\n', file);
  
    if (c) {
      fputs (prefix, file);
      if (terminal) terminal->magenta ();
      fputs (c, file);
      if (f) {
        fputc (' ', file);
        fputs (f, file);
      }
      if (terminal) terminal->normal ();
      fputc ('\n', file);
    }
  
    if (b) {
      fputs (prefix, file);
      if (terminal) terminal->magenta ();
      fputs (b, file);
      if (terminal) terminal->normal ();
      fputc ('\n', file);
    }
  
    fflush (file);
  }
  
  const char * Solver::version () { return CaDiCaL::version (); }
  
  const char * Solver::signature () { return CaDiCaL::signature (); }
  
  void Solver::options () {
    REQUIRE_VALID_STATE ();
    internal->opts.print ();
  }
  
  void Solver::usage () { Options::usage (); }
  
  void Solver::configurations () { Config::usage (); }
  
  void Solver::statistics () {
    if (state () == DELETING) return;
    TRACE ("stats");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    internal->print_statistics ();
    LOG_API_CALL_END ("stats");
  }
  
  void Solver::resources () {
    if (state () == DELETING) return;
    TRACE ("resources");
    REQUIRE_VALID_OR_SOLVING_STATE ();
    internal->print_resource_usage ();
    LOG_API_CALL_END ("resources");
  }
  
  /*------------------------------------------------------------------------*/
  
  const char * Solver::read_aux(File* file)
  {
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    std::vector<int, std::allocator<int> > cubes;
    bool incremental = false;
    Parser * parser = new Parser (this, file, &incremental, &cubes);
    const char * err = parser->parse_aux ();
    delete parser;
    return err;
  }
  
  const char * Solver::read_aux(FILE * external_file, const char* name)
  {
    LOG_API_CALL_BEGIN ("read_aux", name);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read auxiliary variable file right after initialization");
    File * file = File::read (internal, external_file, name);
    assert (file);
    const char * err =
      read_aux (file);
    delete file;
    LOG_API_CALL_RETURNS ("read_aux", name, err);
    return err;
  }
  
  const char * Solver::read_aux(const char* path)
  {
    LOG_API_CALL_BEGIN ("read_aux", path);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read auxiliary file right after initialization");
    File * file = File::read (internal, path);
    if (!file)
      return internal->error_message.init (
               "failed to read auxiliary file '%s'", path);
    const char * err = read_aux (file);
    delete file;
    LOG_API_CALL_RETURNS ("read_aux", path, err);
    return err;
  }
  
  /*------------------------------------------------------------------------*/
  
  const char * Solver::read_dimacs (File * file, int & vars, int strict,
                                    bool * incremental, vector<int> * cubes)
  {
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    Parser * parser = new Parser (this, file, incremental, cubes);
    const char * err = parser->parse_dimacs (vars, strict);
    delete parser;
    return err;
  }
  
  const char *
  Solver::read_dimacs (FILE * external_file,
                       const char * name, int & vars, int strict) {
    LOG_API_CALL_BEGIN ("read_dimacs", name);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    File * file = File::read (internal, external_file, name);
    assert (file);
    const char * err = read_dimacs (file, vars, strict);
    delete file;
    LOG_API_CALL_RETURNS ("read_dimacs", name, err);
    return err;
  }
  
  const char *
  Solver::read_dimacs (const char * path, int & vars, int strict) {
    LOG_API_CALL_BEGIN ("read_dimacs", path);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    File * file = File::read (internal, path);
    if (!file)
      return internal->error_message.init (
               "failed to read DIMACS file '%s'", path);
    const char * err = read_dimacs (file, vars, strict);
    delete file;
    LOG_API_CALL_RETURNS ("read_dimacs", path, err);
    return err;
  }
  
  const char *
  Solver::read_dimacs (FILE * external_file,
                       const char * name, int & vars, int strict,
                       bool & incremental, vector<int> & cubes) {
    LOG_API_CALL_BEGIN ("read_dimacs", name);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    File * file = File::read (internal, external_file, name);
    assert (file);
    const char * err =
      read_dimacs (file, vars, strict, &incremental, &cubes);
    delete file;
    LOG_API_CALL_RETURNS ("read_dimacs", name, err);
    return err;
  }
  
  const char *
  Solver::read_dimacs (const char * path, int & vars, int strict,
                       bool & incremental, vector<int> & cubes) {
    LOG_API_CALL_BEGIN ("read_dimacs", path);
    REQUIRE_VALID_STATE ();
    REQUIRE (state () == CONFIGURING,
      "can only read DIMACS file right after initialization");
    File * file = File::read (internal, path);
    if (!file)
      return internal->error_message.init (
               "failed to read DIMACS file '%s'", path);
    const char * err =
      read_dimacs (file, vars, strict, &incremental, &cubes);
    delete file;
    LOG_API_CALL_RETURNS ("read_dimacs", path, err);
    return err;
  }
  
  const char * Solver::read_solution (const char * path) {
    LOG_API_CALL_BEGIN ("solution", path);
    REQUIRE_VALID_STATE ();
    File * file = File::read (internal, path);
    if (!file) return internal->error_message.init (
                        "failed to read solution file '%s'", path);
    Parser * parser = new Parser (this, file, 0, 0);
    const char * err = parser->parse_solution ();
    delete parser;
    delete file;
    if (!err) external->check_assignment (&External::sol);
    LOG_API_CALL_RETURNS ("read_solution", path, err);
    return err;
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::dump_cnf () {
    TRACE ("dump");
    REQUIRE_INITIALIZED ();
    internal->dump ();
    LOG_API_CALL_END ("dump");
  }
  
  /*------------------------------------------------------------------------*/
  
  bool Solver::traverse_clauses (ClauseIterator & it) const {
    LOG_API_CALL_BEGIN ("traverse_clauses");
    REQUIRE_VALID_STATE ();
    bool res = external->traverse_all_frozen_units_as_clauses (it) &&
               internal->traverse_clauses (it);
    LOG_API_CALL_RETURNS ("traverse_clauses", res);
    return res;
  }
  
  bool Solver::traverse_witnesses_backward (WitnessIterator & it) const {
    LOG_API_CALL_BEGIN ("traverse_witnesses_backward");
    REQUIRE_VALID_STATE ();
    bool res = external->traverse_all_non_frozen_units_as_witnesses (it) &&
               external->traverse_witnesses_backward (it);
    LOG_API_CALL_RETURNS ("traverse_witnesses_backward", res);
    return res;
  }
  
  bool Solver::traverse_witnesses_forward (WitnessIterator & it) const {
    LOG_API_CALL_BEGIN ("traverse_witnesses_forward");
    REQUIRE_VALID_STATE ();
    bool res = external->traverse_witnesses_forward (it) &&
               external->traverse_all_non_frozen_units_as_witnesses (it);
    LOG_API_CALL_RETURNS ("traverse_witnesses_forward", res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  class ClauseCounter : public ClauseIterator {
  public:
    int vars;
    int64_t clauses;
    ClauseCounter () : vars (0), clauses (0) { }
    bool clause (const vector<int> & c) {
      for (const auto & lit : c) {
        assert (lit != INT_MIN);
        int idx = abs (lit);
        if (idx > vars) vars = idx;
      }
      clauses++;
      return true;
    }
  };
  
  class ClauseWriter : public ClauseIterator {
    File * file;
  public:
    ClauseWriter (File * f) : file (f) { }
    bool clause (const vector<int> & c) {
      for (const auto & lit : c) {
        if (!file->put (lit)) return false;
        if (!file->put (' ')) return false;
      }
      return file->put ("0\n");
    }
  };
  
  const char * Solver::write_dimacs (const char * path, int min_max_var) {
    LOG_API_CALL_BEGIN ("write_dimacs", path, min_max_var);
    REQUIRE_VALID_STATE ();
  #ifndef QUIET
    const double start = internal->time ();
  #endif
    internal->restore_clauses ();
    ClauseCounter counter;
    (void) traverse_clauses (counter);
    LOG ("found maximal variable %d and %" PRId64 " clauses",
      counter.vars, counter.clauses);
    File * file = File::write (internal, path);
    const char * res = 0;
    if (file) {
      int actual_max_vars = max (min_max_var, counter.vars);
      MSG ("writing %s'p cnf %d %" PRId64 "'%s header",
        tout.green_code (), actual_max_vars, counter.clauses,
        tout.normal_code ());
      file->put ("p cnf ");
      file->put (actual_max_vars);
      file->put (' ');
      file->put (counter.clauses);
      file->put ('\n');
      ClauseWriter writer (file);
      if (!traverse_clauses (writer))
        res = internal->error_message.init (
                "writing to DIMACS file '%s' failed", path);
      delete file;
    } else res = internal->error_message.init (
                   "failed to open DIMACS file '%s' for writing", path);
  #ifndef QUIET
    if (!res) {
      const double end = internal->time ();
      MSG ("wrote %" PRId64 " clauses in %.2f seconds %s time",
        counter.clauses, end - start,
        internal->opts.realtime ? "real" : "process");
    }
  #endif
    LOG_API_CALL_RETURNS ("write_dimacs", path, min_max_var, res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  struct WitnessWriter : public WitnessIterator {
    File * file;
    int64_t witnesses;
    WitnessWriter (File * f) : file (f), witnesses (0) { }
    bool write (const vector<int> & a) {
      for (const auto & lit : a) {
        if (!file->put (lit)) return false;
        if (!file->put (' ')) return false;
      }
      return file->put ('0');
    }
    bool witness (const vector<int> & c, const vector<int> & w) {
      if (!write (c)) return false;
      if (!file->put (' ')) return false;
      if (!write (w)) return false;
      if (!file->put ('\n')) return false;
      witnesses++;
      return true;
    }
  };
  
  const char * Solver::write_extension (const char * path) {
    LOG_API_CALL_BEGIN ("write_extension", path);
    REQUIRE_VALID_STATE ();
    const char * res = 0;
  #ifndef QUIET
    const double start = internal->time ();
  #endif
    File * file = File::write (internal, path);
    WitnessWriter writer (file);
    if (file) {
      if (!traverse_witnesses_backward (writer))
        res = internal->error_message.init (
                "writing to DIMACS file '%s' failed", path);
      delete file;
    } else res = internal->error_message.init (
                   "failed to open extension file '%s' for writing", path);
  #ifndef QUIET
    if (!res) {
      const double end = internal->time ();
      MSG ("wrote %" PRId64 " witnesses in %.2f seconds %s time",
        writer.witnesses, end - start,
        internal->opts.realtime ? "real" : "process");
    }
  #endif
    LOG_API_CALL_RETURNS ("write_extension", path, res);
    return res;
  }
  
  /*------------------------------------------------------------------------*/
  
  struct ClauseCopier : public ClauseIterator {
    Solver & dst;
  public:
    ClauseCopier (Solver & d) : dst (d) { }
    bool clause (const vector<int> & c) {
      for (const auto & lit : c)
        dst.add (lit);
      dst.add (0);
      return true;
    }
  };
  
  struct WitnessCopier : public WitnessIterator {
    External * dst;
  public:
    WitnessCopier (External * d) : dst (d) { }
    bool witness (const vector<int> & c, const vector<int> & w) {
      dst->push_external_clause_and_witness_on_extension_stack (c, w);
      return true;
    }
  };
  
  void Solver::copy (Solver & other) const {
    REQUIRE_READY_STATE ();
    REQUIRE (other.state () & CONFIGURING,
      "target solver already modified");
    internal->opts.copy (other.internal->opts);
    ClauseCopier clause_copier (other);
    traverse_clauses (clause_copier);
    WitnessCopier witness_copier (other.external);
    traverse_witnesses_forward (witness_copier);
    external->copy_flags (*other.external);
  }
  
  /*------------------------------------------------------------------------*/
  
  void Solver::section (const char * title) {
    if (state () == DELETING) return;
  #ifdef QUIET
    (void) title;
  #endif
    REQUIRE_INITIALIZED ();
    SECTION (title);
  }
  
  void Solver::message (const char * fmt, ...) {
    if (state () == DELETING) return;
  #ifdef QUIET
    (void) fmt;
  #else
    REQUIRE_INITIALIZED ();
    va_list ap;
    va_start (ap, fmt);
    internal->vmessage (fmt, ap);
    va_end (ap);
  #endif
  }
  
  void Solver::message () {
    if (state () == DELETING) return;
    REQUIRE_INITIALIZED ();
  #ifndef QUIET
    internal->message ();
  #endif
  }
  
  void Solver::verbose (int level, const char * fmt, ...) {
    if (state () == DELETING) return;
    REQUIRE_VALID_OR_SOLVING_STATE ();
  #ifdef QUIET
    (void) level;
    (void) fmt;
  #else
    va_list ap;
    va_start (ap, fmt);
    internal->vverbose (level, fmt, ap);
    va_end (ap);
  #endif
  }
  
  void Solver::error (const char * fmt, ...) {
    if (state () == DELETING) return;
    REQUIRE_INITIALIZED ();
    va_list ap;
    va_start (ap, fmt);
    internal->verror (fmt, ap);
    va_end (ap);
  }
  
  }
  