#include "cadical.hpp"

#include <cstdlib>
#include <cstring>

namespace CaDiCaL {

struct Wrapper : Learner, Terminator {

  Solver *solver;
  struct {
    void *state;
    int (*function) (void *);
  } terminator;

  struct {
    void *state;
    int max_length;
    int *begin_clause, *end_clause, *capacity_clause;
    void (*function) (void *, int *);
  } learner;

  bool terminate () {
    if (!terminator.function)
      return false;
    return terminator.function (terminator.state);
  }

  bool learning (int size) {
    if (!learner.function)
      return false;
    return size <= learner.max_length;
  }

  void learn (int lit) {
    if (learner.end_clause == learner.capacity_clause) {
      size_t count = learner.end_clause - learner.begin_clause;
      size_t size = count ? 2 * count : 1;
      learner.begin_clause =
          (int *) realloc (learner.begin_clause, size * sizeof (int));
      learner.end_clause = learner.begin_clause + count;
      learner.capacity_clause = learner.begin_clause + size;
    }
    *learner.end_clause++ = lit;
    if (lit)
      return;
    learner.function (learner.state, learner.begin_clause);
    learner.end_clause = learner.begin_clause;
  }

  Wrapper () : solver (new Solver ()) {
    memset (&terminator, 0, sizeof terminator);
    memset (&learner, 0, sizeof learner);
  }

  ~Wrapper () {
    terminator.function = 0;
    if (learner.begin_clause)
      free (learner.begin_clause);
    delete solver;
  }
};

} // namespace CaDiCaL

using namespace CaDiCaL;

extern "C" {

#include "ccadical.h"

const char *ccadical_signature (void) { return Solver::signature (); }

CCaDiCaL *ccadical_init (void) { return (CCaDiCaL *) new Wrapper (); }

void ccadical_release (CCaDiCaL *wrapper) { delete (Wrapper *) wrapper; }

void ccadical_constrain (CCaDiCaL *wrapper, int lit) {
  ((Wrapper *) wrapper)->solver->constrain (lit);
}

int ccadical_constraint_failed (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->constraint_failed ();
}

void ccadical_set_option (CCaDiCaL *wrapper, const char *name, int val) {
  ((Wrapper *) wrapper)->solver->set (name, val);
}

void ccadical_limit (CCaDiCaL *wrapper, const char *name, int val) {
  ((Wrapper *) wrapper)->solver->limit (name, val);
}

int ccadical_get_option (CCaDiCaL *wrapper, const char *name) {
  return ((Wrapper *) wrapper)->solver->get (name);
}

void ccadical_add (CCaDiCaL *wrapper, int lit) {
  ((Wrapper *) wrapper)->solver->add (lit);
}

void ccadical_assume (CCaDiCaL *wrapper, int lit) {
  ((Wrapper *) wrapper)->solver->assume (lit);
}

int ccadical_solve (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->solve ();
}

int ccadical_simplify (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->simplify ();
}

int ccadical_val (CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *) wrapper)->solver->val (lit);
}

int ccadical_failed (CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *) wrapper)->solver->failed (lit);
}

void ccadical_print_statistics (CCaDiCaL *wrapper) {
  ((Wrapper *) wrapper)->solver->statistics ();
}

void ccadical_terminate (CCaDiCaL *wrapper) {
  ((Wrapper *) wrapper)->solver->terminate ();
}

int64_t ccadical_active (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->active ();
}

int64_t ccadical_irredundant (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->irredundant ();
}

int ccadical_fixed (CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *) wrapper)->solver->fixed (lit);
}

void ccadical_set_terminate (CCaDiCaL *ptr, void *state,
                             int (*terminate) (void *)) {
  Wrapper *wrapper = (Wrapper *) ptr;
  wrapper->terminator.state = state;
  wrapper->terminator.function = terminate;
  if (terminate)
    wrapper->solver->connect_terminator (wrapper);
  else
    wrapper->solver->disconnect_terminator ();
}

void ccadical_set_learn (CCaDiCaL *ptr, void *state, int max_length,
                         void (*learn) (void *state, int *clause)) {
  Wrapper *wrapper = (Wrapper *) ptr;
  wrapper->learner.state = state;
  wrapper->learner.max_length = max_length;
  wrapper->learner.function = learn;
  if (learn)
    wrapper->solver->connect_learner (wrapper);
  else
    wrapper->solver->disconnect_learner ();
}

void ccadical_freeze (CCaDiCaL *ptr, int lit) {
  ((Wrapper *) ptr)->solver->freeze (lit);
}

void ccadical_melt (CCaDiCaL *ptr, int lit) {
  ((Wrapper *) ptr)->solver->melt (lit);
}

int ccadical_frozen (CCaDiCaL *ptr, int lit) {
  return ((Wrapper *) ptr)->solver->frozen (lit);
}

int ccadical_trace_proof (CCaDiCaL *ptr, FILE *file, const char *path) {
  return ((Wrapper *) ptr)->solver->trace_proof (file, path);
}

int ccadical_trace_proof_callback (
  CCaDiCaL *ptr, void* state,
  const void (*process) (void* state, uint64_t id,
                         const int*, unsigned long long,
                         const uint64_t*, unsigned long long)
) {
  ((Wrapper *) ptr)->solver->set("lrat", 1);
  auto cb = [process, state](uint64_t id, const std::vector<int>& clause, const std::vector<uint64_t> dependencies) {
    process(state, id, clause.data(), clause.size(), dependencies.data(), dependencies.size());
  };
  return ((Wrapper *) ptr)->solver->trace_proof (cb);
}

void ccadical_close_proof (CCaDiCaL *ptr) {
  ((Wrapper *) ptr)->solver->close_proof_trace ();
}

void ccadical_conclude (CCaDiCaL *ptr) {
  ((Wrapper *) ptr)->solver->conclude ();
}

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

// Extending C API (Christoph Jabs)

int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
  try {
    ((Wrapper*) wrapper)->solver->add (lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
  try {
    ((Wrapper*) wrapper)->solver->assume (lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
  try {
    ((Wrapper*) wrapper)->solver->constrain (lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_solve_mem (CCaDiCaL * wrapper) {
  try {
    return ((Wrapper*) wrapper)->solver->solve ();
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
  return ((Wrapper *) ptr)->solver->configure (name);
}

void ccadical_phase (CCaDiCaL *ptr, int lit) {
  ((Wrapper *) ptr)->solver->phase (lit);
}

void ccadical_unphase (CCaDiCaL *ptr, int lit) {
  ((Wrapper *) ptr)->solver->unphase (lit);
}

int ccadical_vars (CCaDiCaL *ptr) {
  return ((Wrapper *) ptr)->solver->vars ();
}

bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
                              int val) {
  return ((Wrapper *) wrapper)->solver->set (name, val);
}

bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
  return ((Wrapper *) wrapper)->solver->limit (name, val);
}

int64_t ccadical_redundant (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->redundant ();
}

int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
  return ((Wrapper *) wrapper)->solver->simplify (rounds);
}

int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
  try {
    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int64_t ccadical_propagations (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->propagations ();
}

int64_t ccadical_decisions (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->decisions ();
}

int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
  return ((Wrapper *) wrapper)->solver->conflicts ();
}

bool ccadical_flip (CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *) wrapper)->solver->flip (lit);
}

bool ccadical_flippable (CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *) wrapper)->solver->flippable (lit);
}

/*------------------------------------------------------------------------*/
}
