2 #include "solver_interface.h"
7 #include <sys/resource.h>
9 #include "utils/System.h"
10 #include "utils/ParseUtils.h"
11 #include "utils/Options.h"
12 #include "core/Dimacs.h"
13 #include "simp/SimpSolver.h"
15 using namespace Glucose;
18 static const char* _certified = "CORE -- CERTIFIED UNSAT";
20 void printStats(Solver& solver)
22 double cpu_time = cpuTime();
23 double mem_used = 0;//memUsedPeak();
24 printf("c restarts : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
25 printf("c blocked restarts : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
26 printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
27 printf("c nb ReduceDB : %" PRIu64"\n", solver.nbReduceDB);
28 printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses);
29 printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2);
30 printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin);
31 printf("c nb learnts size 1 : %" PRIu64"\n", solver.nbUn);
33 printf("c conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
34 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);
35 printf("c propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
36 printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
37 printf("c nb reduced Clauses : %" PRIu64"\n",solver.nbReducedClauses);
39 if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
40 printf("c CPU time : %g s\n", cpu_time);
45 static Solver* solver;
46 // Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
47 // for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
48 static void SIGINT_interrupt(int signum) { solver->interrupt(); }
50 // Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
51 // destructors and may cause deadlocks if a malloc/free function happens to be running (these
52 // functions are guarded by locks for multithreaded use).
53 static void SIGINT_exit(int signum) {
54 printf("\n"); printf("*** INTERRUPTED ***\n");
55 if (solver->verbosity > 0){
57 printf("\n"); printf("*** INTERRUPTED ***\n"); }
71 ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
72 if (ptr == -1 || ptr == 0)
75 ssize_t bytestoread=(4-(ptr & 3)) & 3;
76 while(bytestoread != 0) {
77 ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
78 if (p == -1 || p == 0)
87 return buffer[offset++];
91 ssize_t bytestowrite=sizeof(int)*outoffset;
92 ssize_t byteswritten=0;
94 ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
96 fprintf(stderr, "Write failure\n");
101 } while(bytestowrite != 0);
105 void putInt(int value) {
106 if (outoffset>=IS_BUFFERSIZE) {
109 outbuffer[outoffset++]=value;
112 void readClauses(Solver *solver) {
114 int numvars = solver->nVars();
115 bool haveClause = false;
116 fprintf(stderr,"Let's read clauses ...\n");
120 // fprintf(stderr,"%d ", lit);
121 int var = abs(lit) - 1;
122 while (var >= numvars) {
126 clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
129 // fprintf(stderr, "\n");
131 solver->addClause_(clause);
135 // fprintf(stderr, "****************************************************************\n");
143 void processCommands(SimpSolver *solver) {
145 int command=getInt();
149 // fprintf(stderr, "Freezing %d\n", var);
150 solver->setFrozen(var, true);
155 // SimpSolver* solver2 = (SimpSolver*)solver->clone();
156 double time1 = cpuTime();
157 lbool ret = solver->solveLimited(dummy);
158 // double time2 = cpuTime();
160 // lbool ret2 = solver2->solveLimited(dummy2);
161 // double time3 = cpuTime();
162 // fprintf( stderr, "First execution time: %f\t second execution time: %f\n", time2 - time1, time3-time2);
165 putInt(solver->nVars());
166 for(int i=0;i<solver->nVars();i++) {
167 putInt(solver->model[i]==l_True);
169 } else if (ret == l_False) {
171 putInt(solver->assumptionsSize());
172 fprintf(stderr, "assumption size = %d\nConflict Array: ",solver->assumptionsSize());
173 for(int i=0;i<solver->conflict.size();i++) {
174 fprintf(stderr, "%d = %d, ", i, sign(solver->conflict[i])==true);
176 fprintf(stderr, "\n***********************\n");
177 for(int i=0;i<solver->assumptionsSize();i++) {
178 putInt(sign(solver->conflict[i])==true);
187 fprintf(stderr, "Unreconized command\n");
193 void processSAT(SimpSolver *solver) {
194 buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
197 outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
201 double initial_time = cpuTime();
203 double parse_time = cpuTime();
204 processCommands(solver);
205 double finish_time = cpuTime();
206 printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
212 //=================================================================================================
215 int main(int argc, char** argv) {
217 printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
220 setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
223 #if defined(__linux__)
224 fpu_control_t oldcw, newcw;
225 _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
226 //printf("c WARNING: for repeatability, setting FPU to use double precision\n");
230 IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 0, IntRange(0, 2));
231 BoolOption mod ("MAIN", "model", "show model.", false);
232 IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
233 BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true);
234 StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
235 IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
236 IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
238 BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false);
239 StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL");
241 parseOptions(argc, argv, true);
246 S.verbEveryConflicts = vv;
249 // Use signal handlers that forcibly quit until the solver will be
250 // able to respond to interrupts:
251 signal(SIGINT, SIGINT_exit);
252 signal(SIGXCPU,SIGINT_exit);
255 // Set limit on CPU-time:
256 if (cpu_lim != INT32_MAX){
258 getrlimit(RLIMIT_CPU, &rl);
259 if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
260 rl.rlim_cur = cpu_lim;
261 if (setrlimit(RLIMIT_CPU, &rl) == -1)
262 printf("c WARNING! Could not set resource limit: CPU-time.\n");
265 // Set limit on virtual memory:
266 if (mem_lim != INT32_MAX){
267 rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
269 getrlimit(RLIMIT_AS, &rl);
270 if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
271 rl.rlim_cur = new_mem_lim;
272 if (setrlimit(RLIMIT_AS, &rl) == -1)
273 printf("c WARNING! Could not set resource limit: Virtual memory.\n");
276 //do solver stuff here
279 printf("c | Number of variables: %12d |\n", S.nVars());
280 printf("c | Number of clauses: %12d |\n", S.nClauses());
283 // Change to signal-handlers that will only notify the solver and allow it to terminate
285 signal(SIGINT, SIGINT_interrupt);
286 signal(SIGXCPU,SIGINT_interrupt);
295 } catch (OutOfMemoryException&){
296 printf("c =========================================================================================================\n");
297 printf("INDETERMINATE\n");