text: #include "internal.hpp"
  
  namespace CaDiCaL {
  
  /*------------------------------------------------------------------------*/
  
  Tracer::Tracer (Internal * i, File * f, bool b) :
    internal (i),
    file (f), binary (b),
    added (0), deleted (0)
  {
    (void) internal;
    LOG ("TRACER new");
  }
  
  Tracer::~Tracer () {
    LOG ("TRACER delete");
    delete file;
  }
  
  /*------------------------------------------------------------------------*/
  
  // Support for binary DRAT format.
  
  inline void Tracer::put_binary_zero () {
    assert (binary);
    assert (file);
    file->put ((unsigned char) 0);
  }
  
  inline void Tracer::put_binary_lit (int lit) {
    assert (binary);
    assert (file);
    assert (lit != INT_MIN);
    unsigned x = 2*abs (lit) + (lit < 0);
    unsigned char ch;
    while (x & ~0x7f) {
      ch = (x & 0x7f) | 0x80;
      file->put (ch);
      x >>= 7;
    }
    ch = x;
    file->put (ch);
  }
  
  /*------------------------------------------------------------------------*/
  
  void Tracer::add_derived_clause (const vector<int> & clause) {
    if (file->closed ()) return;
    LOG ("TRACER tracing addition of derived clause");
    if (binary) file->put ('a');
    for (const auto & external_lit : clause)
      if (binary) put_binary_lit (external_lit);
      else file->put (external_lit), file->put (' ');
    if (binary) put_binary_zero ();
    else file->put ("0\n");
    added++;
  }
  
  void Tracer::delete_clause (const vector<int> & clause) {
    if (file->closed ()) return;
    LOG ("TRACER tracing deletion of clause");
    if (binary) file->put ('d');
    else file->put ("d ");
    for (const auto & external_lit : clause)
      if (binary) put_binary_lit (external_lit);
      else file->put (external_lit), file->put (' ');
    if (binary) put_binary_zero ();
    else file->put ("0\n");
    deleted++;
  }
  
  /*------------------------------------------------------------------------*/
  
  bool Tracer::closed () { return file->closed (); }
  
  void Tracer::close () { assert (!closed ()); file->close (); }
  
  void Tracer::flush () {
    assert (!closed ());
    file->flush ();
    MSG ("traced %" PRId64 " added and %" PRId64 " deleted clauses",
      added, deleted);
  }
  
  }
  