#include "solver_interface.h"
#include <errno.h>

#include <signal.h>
#include <zlib.h>
#include <sys/resource.h>

#include "utils/System.h"
#include "utils/ParseUtils.h"
#include "utils/Options.h"
#include "core/Dimacs.h"
#include "simp/SimpSolver.h"

using namespace Glucose;


static const char* _certified = "CORE -- CERTIFIED UNSAT";

void printStats(Solver& solver)
{
    double cpu_time = cpuTime();
    double mem_used = 0;//memUsedPeak();
    printf("c restarts              : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
    printf("c blocked restarts      : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
    printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
    printf("c nb ReduceDB           : %" PRIu64"\n", solver.nbReduceDB);
    printf("c nb removed Clauses    : %" PRIu64"\n",solver.nbRemovedClauses);
    printf("c nb learnts DL2        : %" PRIu64"\n", solver.nbDL2);
    printf("c nb learnts size 2     : %" PRIu64"\n", solver.nbBin);
    printf("c nb learnts size 1     : %" PRIu64"\n", solver.nbUn);

    printf("c conflicts             : %-12" PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
    printf("c decisions             : %-12" PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
    printf("c propagations          : %-12" PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
    printf("c conflict literals     : %-12" PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
    printf("c nb reduced Clauses    : %" PRIu64"\n",solver.nbReducedClauses);
    
    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
    printf("c CPU time              : %g s\n", cpu_time);
}



static Solver* solver;
// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
static void SIGINT_interrupt(int signum) { solver->interrupt(); }

// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
// destructors and may cause deadlocks if a malloc/free function happens to be running (these
// functions are guarded by locks for multithreaded use).
static void SIGINT_exit(int signum) {
    printf("\n"); printf("*** INTERRUPTED ***\n");
    if (solver->verbosity > 0){
        printStats(*solver);
        printf("\n"); printf("*** INTERRUPTED ***\n"); }
    _exit(1); }


int *buffer;
int length;
int offset;

int getInt() {
  if (offset>=length) {
    ssize_t ptr;
    offset = 0;
    do {
      ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
      if (ptr == -1)
        exit(-1);
    } while(ptr==0);
    ssize bytestoread=(4-(ptr & 3)) & 3;
    while(bytestoread != 0) {
      ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
      if (p == -1)
        exit(-1);
      bytestoread -= p;
      ptr += p;
    }
    length = ptr / 4;
    offset = 0;
  }
  
  return buffer[offset++];
}

void putInt(int value) {
}

void readClauses(Solver *solver) {
  vec<Lit> clause;
  int numvars = solver->nVars();
  bool haveClause = false;
  while(true) {
    int lit=getInt();
    if (lit!=0) {
      int var = abs(lit) - 1;
      while (var >= numvars) {
        numvars++;
        solver->newVar();
      }
      clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
      haveClause = true;
    } else {
      if (haveClause) {
        solver->addClause_(clause);
        haveClause = false;
        clause.clear();
      } else {
        //done with clauses
        return;
      }
    }
  }
}

void processCommands(Solver *solver) {
  while(true) {
    int command=getInt();
    switch(command) {
    case IS_FREEZE:
      int var=getInt();
      solver->setFrozen(var, true);
      break;
    case IS_RUNSOLVER: {
      vec<Lit> dummy;
      lbool ret = solver->solveLimited(dummy);
      if (ret == l_True) {
        putInt(IS_SAT);
        putInt(solver->nVars());
        for(int i=0;i<solver->nVars();i++) {
          putInt(solver->model[i]==l_True);
        }
      } else if (ret == l_False) {
        putInt(IS_UNSAT);
      } else {
        putInt(IS_INDETER);
      }
      flushInts();
      return;
    }
    default:
      fprintf(stderr, "Unreconized command\n");
      exit(-1);
    }
  }
}
  
void processSAT(Solver *solver) {
  buffer=(int *) malloc(sizeof(int)*BUFFERSIZE);
  offset=0;
  length=0;
  
  while(true) {
    double initial_time = cpuTime();    
    readClauses(solver);
    double parse_time = cpuTime();
    processCommands(solver);
    double finish_time = cpuTime();    
    
  }
}



//=================================================================================================
// Main:

int main(int argc, char** argv) {
  try {
    printf("c\nc This is glucose 4.0 --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
    
    
    setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
    
    
#if defined(__linux__)
    fpu_control_t oldcw, newcw;
    _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
    //printf("c WARNING: for repeatability, setting FPU to use double precision\n");
#endif
    // Extra options:
    //
    IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
    BoolOption   mod   ("MAIN", "model",   "show model.", false);
    IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
    BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);
    StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
    IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
    IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
    
    BoolOption    opt_certified      (_certified, "certified",    "Certified UNSAT using DRUP format", false);
    StringOption  opt_certified_file      (_certified, "certified-output",    "Certified UNSAT output file", "NULL");
         
    parseOptions(argc, argv, true);
    
    SimpSolver  S;
    S.parsing = 1;
    S.verbosity = verb;
    S.verbEveryConflicts = vv;
    S.showModel = mod;
    solver = &S;
    // Use signal handlers that forcibly quit until the solver will be
    // able to respond to interrupts:
    signal(SIGINT, SIGINT_exit);
    signal(SIGXCPU,SIGINT_exit);


    // Set limit on CPU-time:
    if (cpu_lim != INT32_MAX){
      rlimit rl;
      getrlimit(RLIMIT_CPU, &rl);
      if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
        rl.rlim_cur = cpu_lim;
        if (setrlimit(RLIMIT_CPU, &rl) == -1)
          printf("c WARNING! Could not set resource limit: CPU-time.\n");
      } }
    
    // Set limit on virtual memory:
    if (mem_lim != INT32_MAX){
      rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
      rlimit rl;
      getrlimit(RLIMIT_AS, &rl);
      if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
        rl.rlim_cur = new_mem_lim;
        if (setrlimit(RLIMIT_AS, &rl) == -1)
          printf("c WARNING! Could not set resource limit: Virtual memory.\n");
      } }
    
    //do solver stuff here
    processSAT(&S);
    
    printf("c |  Number of variables:  %12d                                                                   |\n", S.nVars());
    printf("c |  Number of clauses:    %12d                                                                   |\n", S.nClauses());
    
    double parsed_time = cpuTime();
    if (S.verbosity > 0){
      printf("c |  Parse time:           %12.2f s                                                                 |\n", parsed_time - initial_time);
      printf("c |                                                                                                       |\n"); }
    
    // Change to signal-handlers that will only notify the solver and allow it to terminate
    // voluntarily:
    signal(SIGINT, SIGINT_interrupt);
    signal(SIGXCPU,SIGINT_interrupt);
    
    S.parsing = 0;

#ifdef NDEBUG
    exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
#else
    return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
#endif
  } catch (OutOfMemoryException&){
    printf("c =========================================================================================================\n");
    printf("INDETERMINATE\n");
    exit(0);
  }
}