6c73a7bebb7ff6148755a4364c773d59effda064
[satlib.git] / lingeling / code / lglincremental.c
1 /*-------------------------------------------------------------------------*/
2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
3 /*-------------------------------------------------------------------------*/
4
5 #include "lglib.h"
6
7 #include <assert.h>
8 #include <ctype.h>
9 #include <limits.h>
10 #include <signal.h>
11 #include <stdarg.h>
12 #include <stdio.h>
13 #include <stdlib.h>
14 #include <string.h>
15 #include <unistd.h>
16 #include "solver_interface.h"
17
18 static LGL * lgl4sigh;
19 static int catchedsig, verbose, ignmissingheader, ignaddcls;
20
21 static void (*sig_int_handler)(int);
22 static void (*sig_segv_handler)(int);
23 static void (*sig_abrt_handler)(int);
24 static void (*sig_term_handler)(int);
25 static void (*sig_bus_handler)(int);
26 static void (*sig_alrm_handler)(int);
27
28 static void resetsighandlers (void) {
29   (void) signal (SIGINT, sig_int_handler);
30   (void) signal (SIGSEGV, sig_segv_handler);
31   (void) signal (SIGABRT, sig_abrt_handler);
32   (void) signal (SIGTERM, sig_term_handler);
33   (void) signal (SIGBUS, sig_bus_handler);
34 }
35
36 static void caughtsigmsg (int sig) {
37   if (verbose < 0) return;
38   printf ("c\nc CAUGHT SIGNAL %d", sig);
39   switch (sig) {
40     case SIGINT: printf (" SIGINT"); break;
41     case SIGSEGV: printf (" SIGSEGV"); break;
42     case SIGABRT: printf (" SIGABRT"); break;
43     case SIGTERM: printf (" SIGTERM"); break;
44     case SIGBUS: printf (" SIGBUS"); break;
45     case SIGALRM: printf (" SIGALRM"); break;
46     default: break;
47   }
48   printf ("\nc\n");
49   fflush (stdout);
50 }
51
52 static void catchsig (int sig) {
53   if (!catchedsig) {
54     catchedsig = 1;
55     caughtsigmsg (sig);
56     fputs ("c s UNKNOWN\n", stdout);
57     fflush (stdout);
58     if (verbose >= 0) {
59       lglflushtimers (lgl4sigh);
60       lglstats (lgl4sigh);
61       caughtsigmsg (sig);
62     }
63   }
64   resetsighandlers ();
65   if (!getenv ("LGLNABORT")) raise (sig); else exit (1);
66 }
67
68 static void setsighandlers (void) {
69   sig_int_handler = signal (SIGINT, catchsig);
70   sig_segv_handler = signal (SIGSEGV, catchsig);
71   sig_abrt_handler = signal (SIGABRT, catchsig);
72   sig_term_handler = signal (SIGTERM, catchsig);
73   sig_bus_handler = signal (SIGBUS, catchsig);
74 }
75
76 static int timelimit = -1, caughtalarm = 0;
77
78 static void catchalrm (int sig) {
79   assert (sig == SIGALRM);
80   if (!caughtalarm) {
81     caughtalarm = 1;
82     caughtsigmsg (sig);
83     if (timelimit >= 0) {
84       printf ("c time limit of %d reached after %.1f seconds\nc\n",
85               timelimit, lglsec (lgl4sigh));
86       fflush (stdout);
87     }
88   }
89 }
90
91 static int checkalarm (void * ptr) {
92   assert (ptr == (void*) &caughtalarm);
93   return caughtalarm;
94 }
95
96 static int primes[] = {
97   200000033, 200000039, 200000051, 200000069, 200000081,
98 };
99
100 static int nprimes = sizeof primes / sizeof *primes;
101
102
103
104 int *buffer;
105 int length;
106 int offset;
107
108 int *outbuffer;
109 int outoffset;
110
111 int getInt() {
112   if (offset>=length) {
113     ssize_t ptr;
114     offset = 0;
115     do {
116       ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
117       if (ptr == -1)
118         exit(-1);
119     } while(ptr==0);
120     ssize_t bytestoread=(4-(ptr & 3)) & 3;
121     while(bytestoread != 0) {
122       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
123       if (p == -1)
124         exit(-1);
125       bytestoread -= p;
126       ptr += p;
127     }
128     length = ptr / 4;
129     offset = 0;
130   }
131   
132   return buffer[offset++];
133 }
134
135 void flushInts() {
136   ssize_t bytestowrite=sizeof(int)*outoffset;
137   ssize_t byteswritten=0;
138   do {
139     ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
140     if (n == -1) {
141       fprintf(stderr, "Write failure\n");
142       exit(-1);
143     }
144     bytestowrite -= n;
145     byteswritten += n;
146   } while(bytestowrite != 0);
147   outoffset = 0;
148 }
149
150 void putInt(int value) {
151   if (outoffset>=IS_BUFFERSIZE) {
152     flushInts();
153   }
154   outbuffer[outoffset++]=value;
155 }
156
157 void readClauses(LGL *solver) {
158   bool haveClause = false;
159   while(true) {
160     int lit=getInt();
161     if (lit!=0) {
162       haveClause = true;
163       lgladd(solver, lit);
164     } else {
165       if (haveClause) {
166         lgladd(solver, 0);
167         haveClause = false;
168       } else {
169         //done with clauses
170         return;
171       }
172     }
173   }
174 }
175
176 void processCommands(LGL *solver) {
177   while(true) {
178     int command=getInt();
179     switch(command) {
180     case IS_FREEZE: {
181       int var=getInt();
182       lglfreeze(solver, var);
183       break;
184     }
185     case IS_RUNSOLVER: {
186       int ret = lglsat(solver);
187       if (ret == 10) {
188         putInt(IS_SAT);
189         int numvars=lglmaxvar(solver);
190         putInt(numvars);
191         for(int i=1;i<=numvars;i++) {
192           putInt(lglderef(solver, i) > 0);
193         }
194       } else if (ret == 20) {
195         putInt(IS_UNSAT);
196       } else {
197         putInt(IS_INDETER);
198       }
199       flushInts();
200       return;
201     }
202     default:
203       fprintf(stderr, "Unreconized command\n");
204       exit(-1);
205     }
206   }
207 }
208   
209 void processSAT(LGL *solver) {
210   buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
211   offset=0;
212   length=0;
213   outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
214   outoffset=0;
215   
216   while(true) {
217     double initial_time = cpuTime();    
218     readClauses(solver);
219     double parse_time = cpuTime();
220     processCommands(solver);
221     double finish_time = cpuTime();    
222     printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
223   }
224 }
225
226
227
228 int main (int argc, char ** argv) {
229   int res, i, j, val, len, lineno, simponly, count;
230   const char * pname, * match, * p, * err, * thanks;
231   int maxvar, lit, nopts, simplevel;
232   FILE * pfile;
233   char * tmp;
234   LGL * lgl;
235   lineno = 1;
236   res = simponly = simplevel = 0;
237   pname = thanks = 0;
238   lgl4sigh = lgl = lglinit ();
239   setsighandlers ();
240   for (i = 1; i < argc; i++) {
241     if (!strcmp (argv[i], "-h") || !strcmp (argv[i], "--help")) {
242       printf ("usage: lingeling [<option> ...][<file>[.gz]]\n");
243       printf ("\n");
244       printf ("where <option> is one of the following:\n");
245       printf ("\n");
246       printf ("-q               be quiet (same as '--verbose=-1')\n");
247       printf ("-s               only simplify and print to output file\n");
248       printf ("-O<L>            set simplification level to <L>\n");
249       printf ("-p <options>     read options from file\n");
250       printf ("\n");
251       printf ("-t <seconds>     set time limit\n");
252       printf ("\n");
253       printf ("\n");
254       printf ("-h|--help        print command line option summary\n");
255       printf ("-f|--force       force reading even without header\n");
256       printf ("-i|--ignore      ignore additional clauses\n");
257       printf ("-r|--ranges      print value ranges of options\n");
258       printf ("-d|--defaults    print default values of options\n");
259       printf ("-P|--pcs         print (full) PCS file\n");
260       printf ("--pcs-mixed      print mixed PCS file\n");
261       printf ("--pcs-reduced    print reduced PCS file\n");
262       printf ("-e|--embedded    ditto but in an embedded format print\n");
263       printf ("-n|--no-witness   do not print solution (see '--witness')\n");
264       printf ("\n");
265       printf ("--thanks=<whom>  alternative way of specifying the seed\n");
266       printf ("                 (inspired by Vampire)\n");
267       printf ("\n");
268       printf (
269 "The following options can also be used in the form '--<name>=<int>',\n"
270 "just '--<name>' for increment and '--no-<name>' for zero.  They\n"
271 "can be embedded into the CNF file, set through the API or capitalized\n"
272 "with prefix 'LGL' instead of '--' through environment variables.\n"
273 "Their default values are displayed in square brackets.\n");
274       printf ("\n");
275       lglusage (lgl);
276       goto DONE;
277     } else if (!strcmp (argv[i], "-s")) simponly = 1;
278     else if (argv[i][0] == '-' && argv[i][1] == 'O') {
279       if (simplevel > 0) {
280         fprintf (stderr, "*** lingeling error: multiple '-O..' options\n");
281         res = 1;
282         goto DONE;
283       }
284       if ((simplevel = atoi (argv[i] + 2)) <= 0) {
285         fprintf (stderr,
286            "*** lingeling error: invalid '%s' option\n", argv[i]);
287         res = 1;
288         goto DONE;
289       }
290     } else if (!strcmp (argv[i], "-q")) lglsetopt (lgl, "verbose", -1);
291     else if (!strcmp (argv[i], "-p")) {
292       if (++i == argc) {
293         fprintf (stderr, "*** lingeling error: argument to '-p' missing\n");
294         res = 1;
295         goto DONE;
296       } 
297       if (pname) {
298         fprintf (stderr, 
299                  "*** lingeling error: "
300                  "multiple option files '%s' and '%s'\n",
301                  pname, argv[i]);
302         res = 1;
303         goto DONE;
304       }
305       pname = argv[i];
306     } else if (!strcmp (argv[i], "-t")) {
307       if (++i == argc) {
308         fprintf (stderr, "*** lingeling error: argument to '-t' missing\n");
309         res = 1;
310         goto DONE;
311       }
312       if (timelimit >= 0) {
313         fprintf (stderr, "*** lingeling error: timit limit set twice\n");
314         res = 1;
315         goto DONE;
316       }
317       for (p = argv[i]; *p && isdigit (*p); p++) 
318         ;
319       if (p == argv[i] || *p || (timelimit = atoi (argv[i])) < 0) {
320         fprintf (stderr, 
321           "*** lingeling error: invalid time limit '-t %s'\n", argv[i]);
322         res = 1;
323         goto DONE;
324       }
325     } else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--defaults")) {
326       lglopts (lgl, "", 0);
327       goto DONE;
328     } else if (!strcmp (argv[i], "-e") || !strcmp (argv[i], "--embedded")) {
329       lglopts (lgl, "c ", 1);
330       goto DONE;
331     } else if (!strcmp (argv[i], "-r") || !strcmp (argv[i], "--ranges")) {
332       lglrgopts (lgl);
333       goto DONE;
334     } else if (!strcmp (argv[i], "-P") || !strcmp (argv[i], "--pcs")) {
335       printf ("# generated by 'lingeling --pcs'\n");
336       printf ("# version %s\n", lglversion ());
337       lglpcs (lgl, 0);
338       goto DONE;
339     } else if (!strcmp (argv[i], "--pcs-mixed")) {
340       printf ("# generated by 'lingeling --pcs-mixed'\n");
341       printf ("# version %s\n", lglversion ());
342       lglpcs (lgl, 1);
343       goto DONE;
344     } else if (!strcmp (argv[i], "--pcs-reduced")) {
345       printf ("# generated by 'lingeling --pcs-reduced'\n");
346       printf ("# version %s\n", lglversion ());
347       lglpcs (lgl, -1);
348       goto DONE;
349     } else if (!strcmp (argv[i], "-f") || !strcmp (argv[i], "--force")) {
350       ignmissingheader = 1;
351     } else if (!strcmp (argv[i], "-i") || !strcmp (argv[i], "--ignore")) {
352       ignaddcls = 1;
353     } else if (!strcmp (argv[i], "-n") || !strcmp (argv[i], "no-witness")) {
354       lglsetopt (lgl, "witness", 0);
355     } else if (argv[i][0] == '-') {
356       if (argv[i][1] == '-') {
357         match = strchr (argv[i] + 2, '=');
358         if (match) {
359           p = match + 1;
360           if (*p == '-') p++;   // TODO for what is this useful again?
361           len = p - argv[i];
362           if (!strncmp (argv[i], "--write-api-trace=", len)) {
363             // TODO not handled yet ...
364             continue;
365           } else if (!strncmp (argv[i], "--thanks=", len)) {
366             thanks = match + 1;
367             continue;
368           } else if (!isdigit (*p)) {
369 ERR:
370             fprintf (stderr,
371               "*** lingeling error: invalid command line option '%s'\n",
372               argv[i]);
373             res = 1;
374             goto DONE;
375           }
376           while (*++p) if (!isdigit (*p)) goto ERR;
377           len = match - argv[i] - 2;
378           tmp = malloc (len + 1);
379           j = 0;
380           for (p = argv[i] + 2; *p != '='; p++) tmp[j++] = *p;
381           tmp[j] = 0;
382           val = atoi (match + 1);
383         } else if (!strncmp (argv[i], "--no-", 5)) {
384           tmp = strdup (argv[i] + 5);
385           val = 0;
386         } else {
387           tmp = strdup (argv[i] + 2);
388           val = lglgetopt (lgl, tmp) + 1;
389         }
390         if (!lglhasopt (lgl, tmp)) { free (tmp); goto ERR; }
391         lglsetopt (lgl, tmp, val);
392         free (tmp);
393       } else {
394         if (argv[i][2]) goto ERR;
395         if (!lglhasopt (lgl, argv[i] + 1)) goto ERR;
396         val = lglgetopt (lgl, argv[i] + 1) + 1;
397         lglsetopt (lgl, argv[i] + 1, val);
398       }
399     }
400   }
401   verbose = lglgetopt (lgl, "verbose");
402   if (verbose >= 0) {
403     lglbnr ("Lingeling SAT Solver", "c ", stdout);
404     if (simponly) printf ("c simplifying only\n");
405     if (simponly) fflush (stdout);
406     lglsetopt (lgl, "trep", 1);
407   }
408   if (thanks) {
409     unsigned seed = 0, i = 0, ch;
410     int iseed;
411     for (p = thanks; (ch = *p); p++) {
412       seed += primes[i++] * ch;
413       if (i == nprimes) i = 0;
414     }
415     if (seed >= (unsigned) INT_MAX) seed >>= 1;
416     assert (seed <= (unsigned) INT_MAX);
417     iseed = (int) seed;
418     assert (iseed >= 0);
419     if (verbose)
420       printf ("c will have to thank %s (--seed=%d)\nc\n",
421         thanks, iseed);
422     lglsetopt (lgl, "seed", iseed);
423   }
424   if (verbose >= 2) {
425    printf ("c\nc options after command line parsing:\nc\n");
426    lglopts (lgl, "c ", 0);
427    printf ("c\n");
428    lglsizes (lgl);
429    printf ("c\n");
430   }
431
432   if (pname) {
433     pfile = fopen (pname, "r");
434     if (!pfile) {
435       fprintf (stderr,
436         "*** lingeling error: can not read option file %s\n", pname);
437       res = 1;
438       goto DONE;
439     }
440     if (verbose >= 0) {
441       printf ("c reading options file %s\n", pname);
442       fflush (stdout);
443     }
444     nopts = lglreadopts (lgl, pfile);
445     if (verbose >= 0) 
446       printf ("c read and set %d options\nc\n", nopts), fflush (stdout);
447     fclose (pfile);
448   }
449
450   fflush (stdout);
451
452   if (verbose >= 1) {
453     printf ("c\n");
454     if (verbose >= 2) printf ("c final options:\nc\n");
455     lglopts (lgl, "c ", 0);
456   }
457   if (timelimit >= 0) {
458     if (verbose >= 0) {
459       printf ("c\nc setting time limit of %d seconds\n", timelimit);
460       fflush (stdout);
461     }
462     lglseterm (lgl, checkalarm, &caughtalarm);
463     sig_alrm_handler = signal (SIGALRM, catchalrm);
464     alarm (timelimit);
465   }
466
467   processSAT(lgl);
468   
469   if (timelimit >= 0) {
470     caughtalarm = 0;
471     (void) signal (SIGALRM, sig_alrm_handler);
472   }
473   if (verbose >= 0) fputs ("c\n", stdout), lglstats (lgl);
474 DONE:
475   resetsighandlers ();
476   lgl4sigh = 0;
477   lglrelease (lgl);
478   return 0;
479 }