-
-#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);
- }
-}
projects / satlib.git / commitdiff