1 /*-------------------------------------------------------------------------*/
2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
3 /*-------------------------------------------------------------------------*/
16 #include "solver_interface.h"
18 static LGL * lgl4sigh;
19 static int catchedsig, verbose, ignmissingheader, ignaddcls;
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);
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);
36 static void caughtsigmsg (int sig) {
37 if (verbose < 0) return;
38 printf ("c\nc CAUGHT SIGNAL %d", 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;
52 static void catchsig (int sig) {
56 fputs ("c s UNKNOWN\n", stdout);
59 lglflushtimers (lgl4sigh);
65 if (!getenv ("LGLNABORT")) raise (sig); else exit (1);
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);
76 static int timelimit = -1, caughtalarm = 0;
78 static void catchalrm (int sig) {
79 assert (sig == SIGALRM);
84 printf ("c time limit of %d reached after %.1f seconds\nc\n",
85 timelimit, lglsec (lgl4sigh));
91 static int checkalarm (void * ptr) {
92 assert (ptr == (void*) &caughtalarm);
96 static int primes[] = {
97 200000033, 200000039, 200000051, 200000069, 200000081,
100 static int nprimes = sizeof primes / sizeof *primes;
112 if (offset>=length) {
116 ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
120 ssize_t bytestoread=(4-(ptr & 3)) & 3;
121 while(bytestoread != 0) {
122 ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
132 return buffer[offset++];
136 ssize_t bytestowrite=sizeof(int)*outoffset;
137 ssize_t byteswritten=0;
139 ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
141 fprintf(stderr, "Write failure\n");
146 } while(bytestowrite != 0);
150 void putInt(int value) {
151 if (outoffset>=IS_BUFFERSIZE) {
154 outbuffer[outoffset++]=value;
157 void readClauses(LGL *solver) {
158 bool haveClause = false;
176 void processCommands(LGL *solver) {
178 int command=getInt();
182 lglfreeze(solver, var);
186 int ret = lglsat(solver);
189 int numvars=lglmaxvar(solver);
191 for(int i=1;i<=numvars;i++) {
192 putInt(lglderef(solver, i) > 0);
194 } else if (ret == 20) {
203 fprintf(stderr, "Unreconized command\n");
209 void processSAT(LGL *solver) {
210 buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
213 outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
217 double initial_time = cpuTime();
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);
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;
236 res = simponly = simplevel = 0;
238 lgl4sigh = lgl = lglinit ();
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");
244 printf ("where <option> is one of the following:\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");
251 printf ("-t <seconds> set time limit\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");
265 printf ("--thanks=<whom> alternative way of specifying the seed\n");
266 printf (" (inspired by Vampire)\n");
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");
277 } else if (!strcmp (argv[i], "-s")) simponly = 1;
278 else if (argv[i][0] == '-' && argv[i][1] == 'O') {
280 fprintf (stderr, "*** lingeling error: multiple '-O..' options\n");
284 if ((simplevel = atoi (argv[i] + 2)) <= 0) {
286 "*** lingeling error: invalid '%s' option\n", argv[i]);
290 } else if (!strcmp (argv[i], "-q")) lglsetopt (lgl, "verbose", -1);
291 else if (!strcmp (argv[i], "-p")) {
293 fprintf (stderr, "*** lingeling error: argument to '-p' missing\n");
299 "*** lingeling error: "
300 "multiple option files '%s' and '%s'\n",
306 } else if (!strcmp (argv[i], "-t")) {
308 fprintf (stderr, "*** lingeling error: argument to '-t' missing\n");
312 if (timelimit >= 0) {
313 fprintf (stderr, "*** lingeling error: timit limit set twice\n");
317 for (p = argv[i]; *p && isdigit (*p); p++)
319 if (p == argv[i] || *p || (timelimit = atoi (argv[i])) < 0) {
321 "*** lingeling error: invalid time limit '-t %s'\n", argv[i]);
325 } else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--defaults")) {
326 lglopts (lgl, "", 0);
328 } else if (!strcmp (argv[i], "-e") || !strcmp (argv[i], "--embedded")) {
329 lglopts (lgl, "c ", 1);
331 } else if (!strcmp (argv[i], "-r") || !strcmp (argv[i], "--ranges")) {
334 } else if (!strcmp (argv[i], "-P") || !strcmp (argv[i], "--pcs")) {
335 printf ("# generated by 'lingeling --pcs'\n");
336 printf ("# version %s\n", lglversion ());
339 } else if (!strcmp (argv[i], "--pcs-mixed")) {
340 printf ("# generated by 'lingeling --pcs-mixed'\n");
341 printf ("# version %s\n", lglversion ());
344 } else if (!strcmp (argv[i], "--pcs-reduced")) {
345 printf ("# generated by 'lingeling --pcs-reduced'\n");
346 printf ("# version %s\n", lglversion ());
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")) {
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, '=');
360 if (*p == '-') p++; // TODO for what is this useful again?
362 if (!strncmp (argv[i], "--write-api-trace=", len)) {
363 // TODO not handled yet ...
365 } else if (!strncmp (argv[i], "--thanks=", len)) {
368 } else if (!isdigit (*p)) {
371 "*** lingeling error: invalid command line option '%s'\n",
376 while (*++p) if (!isdigit (*p)) goto ERR;
377 len = match - argv[i] - 2;
378 tmp = malloc (len + 1);
380 for (p = argv[i] + 2; *p != '='; p++) tmp[j++] = *p;
382 val = atoi (match + 1);
383 } else if (!strncmp (argv[i], "--no-", 5)) {
384 tmp = strdup (argv[i] + 5);
387 tmp = strdup (argv[i] + 2);
388 val = lglgetopt (lgl, tmp) + 1;
390 if (!lglhasopt (lgl, tmp)) { free (tmp); goto ERR; }
391 lglsetopt (lgl, tmp, val);
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);
401 verbose = lglgetopt (lgl, "verbose");
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);
409 unsigned seed = 0, i = 0, ch;
411 for (p = thanks; (ch = *p); p++) {
412 seed += primes[i++] * ch;
413 if (i == nprimes) i = 0;
415 if (seed >= (unsigned) INT_MAX) seed >>= 1;
416 assert (seed <= (unsigned) INT_MAX);
420 printf ("c will have to thank %s (--seed=%d)\nc\n",
422 lglsetopt (lgl, "seed", iseed);
425 printf ("c\nc options after command line parsing:\nc\n");
426 lglopts (lgl, "c ", 0);
433 pfile = fopen (pname, "r");
436 "*** lingeling error: can not read option file %s\n", pname);
441 printf ("c reading options file %s\n", pname);
444 nopts = lglreadopts (lgl, pfile);
446 printf ("c read and set %d options\nc\n", nopts), fflush (stdout);
454 if (verbose >= 2) printf ("c final options:\nc\n");
455 lglopts (lgl, "c ", 0);
457 if (timelimit >= 0) {
459 printf ("c\nc setting time limit of %d seconds\n", timelimit);
462 lglseterm (lgl, checkalarm, &caughtalarm);
463 sig_alrm_handler = signal (SIGALRM, catchalrm);
469 if (timelimit >= 0) {
471 (void) signal (SIGALRM, sig_alrm_handler);
473 if (verbose >= 0) fputs ("c\n", stdout), lglstats (lgl);