#include "lglib.h"
#include <assert.h>
#include <ctype.h>
#include <pthread.h>
#include <signal.h>
#include <stdarg.h>
#include <stdlib.h>
#include <string.h>
#include <sys/time.h>
#include <math.h>
#include <limits.h>
#include <unistd.h>
#define CLONELIMIT 20000
#define INC(BYTES) \
do { \
allocated += (BYTES); \
if (allocated > maxallocated) maxallocated = allocated; \
} while (0)
#define DEC(BYTES) \
do { \
assert (allocated >= (BYTES)); \
allocated -= (BYTES); \
} while (0)
#define NEW(PTR,N) \
do { \
size_t BYTES = (N) * sizeof *(PTR); \
(PTR) = malloc (BYTES); \
if(!(PTR)) { die ("out of memory"); exit (1); } \
memset ((PTR), 0, BYTES); \
INC (BYTES); \
} while (0)
#define DEL(PTR,N) \
do { \
size_t BYTES = (N) * sizeof *(PTR); \
DEC (BYTES); \
free (PTR); \
(PTR) = 0; \
} while (0);
#define RSZ(PTR,O,N) \
do { \
size_t OBYTES = (O) * sizeof *(PTR); \
size_t NBYTES = (N) * sizeof *(PTR); \
DEC (OBYTES); \
(PTR) = realloc ((PTR), NBYTES); \
if (!(PTR)) die ("out of memory"); \
INC (NBYTES); \
} while (0)
#define ENLARGE(STACK) \
do { \
size_t oldbytes, newbytes; \
oldbytes = sz ## STACK * sizeof *STACK; \
DEC (oldbytes); \
sz ## STACK = sz ## STACK ? 2*sz ## STACK : 1; \
newbytes = sz ## STACK * sizeof *STACK; \
STACK = realloc (STACK, newbytes); \
if (!(STACK)) die ("out of memory"); \
INC (newbytes); \
} while (0)
#define PUSH(STACK,ELEM) \
do { \
if (n ## STACK >= sz ## STACK) ENLARGE (STACK); \
STACK[n ## STACK++] = ELEM; \
} while (0)
#define WID(W) \
(assert (workers <= (W) && (W) < workers + nworkers), (int)((W) - workers))
typedef struct Worker {
LGL * lgl;
struct {
LGL * lgl;
int count, bcount;
int64_t decs, confs, props;
pthread_mutex_t lock;
} cloned;
int last, res;
pthread_t thread;
FILE * proof, * post;
int * failed, nfailed;
} Worker;
static double startime;
static size_t allocated, maxallocated;
static FILE * statsfile, * histfile;
static Worker * workers;
static int nworkers;
static int nassumptions, queue, szassumptions;
static int maxassumptionsize, sumassumptions, redassumptions;
static double * times, sumtimes;
static int ** assumptions;
static int nvars, szvars, nclauses, nused, * used;
static signed char * vals;
static int nlits, szlits;
static int * lits;
static int verbose, bar, nowitness, plain, doclone, deterministic;
static int noreverse, addassumptions = 1, noflush, reduce, nomelt;
static const char * druptraceprefix;
static int lineno = 1;
static char * inputname;
static FILE * inputfile;
static int done;
static pthread_mutex_t msgmutex = PTHREAD_MUTEX_INITIALIZER;
static pthread_mutex_t donemutex = PTHREAD_MUTEX_INITIALIZER;
static pthread_mutex_t queuemutex = PTHREAD_MUTEX_INITIALIZER;
static pthread_mutex_t finishedmutex = PTHREAD_MUTEX_INITIALIZER;
static int finished;
static void msglock (void * voidptr) {
(void) voidptr;
pthread_mutex_lock (&msgmutex);
}
static void msgunlock (void * voidptr) {
(void) voidptr;
pthread_mutex_unlock (&msgmutex);
}
static void msg (Worker * w, int level, const char * fmt, ...) {
va_list ap;
if (verbose < level) return;
msglock (0);
if (w) printf ("c %d ", WID (w)); else printf ("c - ");
va_start (ap, fmt);
vprintf (fmt, ap);
va_end (ap);
fputc ('\n', stdout);
fflush (stdout);
msgunlock (0);
}
static void die (const char * fmt, ...) {
va_list ap;
fputs ("*** [ilingeling] ", stderr);
va_start (ap, fmt);
vfprintf (stderr, fmt, ap);
va_end (ap);
fputc ('\n', stderr);
fflush (stderr);
exit (1);
}
static void warn (const char * fmt, ...) {
va_list ap;
fputs ("*** [ilingeling] warning: ", stderr);
va_start (ap, fmt);
vfprintf (stderr, fmt, ap);
va_end (ap);
fputc ('\n', stderr);
fflush (stderr);
}
static double currentime (void) {
double res = 0;
struct timeval tv;
if (!gettimeofday (&tv, 0)) res = 1e-6 * tv.tv_usec, res += tv.tv_sec;
return res;
}
static double getime () { return currentime () - startime; }
static int isnum (const char * str) {
const char * p = str;
if (!isdigit ((int)*p++)) return 0;
while (*p && isdigit ((int)*p)) p++;
return !*p;
}
static int term (void * voidptr) {
Worker * w = voidptr;
int res;
msg (w, 3, "checking early termination");
if (pthread_mutex_lock (&donemutex))
warn ("failed to lock 'done' mutex in termination check");
res = done;
if (pthread_mutex_unlock (&donemutex))
warn ("failed to unlock 'done' mutex in termination check");
msg (w, 3, "early termination check %s", res ? "succeeded" : "failed");
return res;
}
static void progress (int pmille, int total, int max, double avg, int nl) {
int ch, i, lim, eta;
char fmt[16];
double rem;
msglock (0);
if (isatty (1)) fputc ('\r', stdout);
lim = 10;
for (i = 1; lim < max && i < 11; i++) lim *= 10;
sprintf (fmt, "c %%0%dd", i);
printf (fmt, total);
printf (" / %d |", max);
for (i = 0; i < pmille/50; i++) fputc ('=', stdout);
if (total == max) ch = '=';
else switch (pmille % 4) {
case 1 : ch = '\\'; break;
case 2 : ch = '|'; break;
case 3 : ch = '/'; break;
default: ch = '-'; break;
}
if (i++ < 20) fputc (ch, stdout);
while (i++ < 20) fputc ('-', stdout);
printf ("| %3d%%", pmille/10);
printf (" %.4f sec/cube", avg);
if (max <= total) eta = 0;
else {
rem = (max - total) * avg;
if (rem >= 100*3600) eta = INT_MAX;
else { eta = rem; assert (eta < INT_MAX); }
}
if (eta < INT_MAX) {
if (eta > 3600) printf (" %02d:", eta / 3600), eta %= 3600;
else printf (" ");
printf ("%02d:%02d ETS", eta/60, eta%60);
} else printf (" --:-- ETS");
if (nl || !isatty (1)) fputc ('\n', stdout);
fflush (stdout);
msgunlock (0);
}
static void initlgl (LGL * lgl, Worker * w, int opts) {
lglsetid (lgl, WID (w), nworkers);
lglsetime (lgl, getime);
lglseterm (lgl, term, w);
lglsetmsglock (lgl, msglock, msgunlock, w);
if (!opts) return;
if (verbose) lglsetopt (lgl, "verbose", verbose-1);
if (plain) lglsetopt (lgl, "plain", 1);
lglsetopt (lgl, "reduceinc", 1000);
lglsetopt (lgl, "reduceinit", 1000);
lglsetopt (lgl, "reusetrail", 1);
lglsetopt (lgl, "gluekeep", 3);
lglsetopt (lgl, "scincinc", 50);
lglsetopt (lgl, "scincincmode", 0);
if (druptraceprefix) {
char * name = malloc (strlen (druptraceprefix) + 30);
sprintf (name, "%s%d.proof", druptraceprefix, WID (w));
if (!(w->proof = fopen (name, "w")))
die ("worker %d can not write DRUP proof to '%s'", WID (w), name);
lglsetout (lgl, w->proof);
sprintf (name, "%s%d.cnf", druptraceprefix, WID (w));
if (!(w->post = fopen (name, "w")))
die ("worker %d can not write post CNF cubes to '%s'", WID (w), name);
free (name);
lglsetopt (lgl, "druplig", 1);
lglsetopt (lgl, "drupligtrace", 1);
} else w->post = w->proof = 0;
}
static int justreturn (Worker * w) {
int res;
if (pthread_mutex_lock (&donemutex))
warn ("worker %d failed to lock 'done' mutex", WID (w));
res = done;
if (pthread_mutex_unlock (&donemutex))
warn ("worker %d failed to unlock 'done' mutex", WID (w));
return res;
}
static int sat (Worker * w) {
#ifndef NDEBUG
int oldres;
#endif
int res;
char name[100];
LGL * cloned;
if (!druptraceprefix && doclone) lglsetopt (w->lgl, "clim", CLONELIMIT);
else lglsetopt (w->lgl, "clim", -1),
lglsetopt (w->lgl, "plim", -1),
lglsetopt (w->lgl, "dlim", -1);
if (!noflush) lglflushcache (w->lgl);
res = lglsat (w->lgl);
assert (!druptraceprefix || !doclone || res);
if (!res && !justreturn (w)) {
msg (w, 1, "cloning after %d conflicts", CLONELIMIT);
cloned = lglclone (w->lgl);
lglfixate (cloned);
lglmeltall (cloned);
initlgl (cloned, w, 0);
lglsetopt (cloned, "clim", -1);
sprintf (name, "c F%d ", w->cloned.count++);
lglsetprefix (cloned, name);
if (pthread_mutex_lock (&w->cloned.lock))
warn ("worker %d failed to lock 'cloned' mutex", WID (w));
assert (!w->cloned.lgl);
w->cloned.lgl = cloned;
if (pthread_mutex_unlock (&w->cloned.lock))
warn ("worker %d failed to unlock 'cloned' mutex", WID (w));
res = lglsat (cloned);
if (pthread_mutex_lock (&w->cloned.lock))
warn ("worker %d failed to lock 'cloned' mutex", WID (w));
assert (cloned == w->cloned.lgl);
w->cloned.lgl = 0;
w->cloned.decs += lglgetdecs (cloned);
w->cloned.confs += lglgetconfs (cloned);
w->cloned.props += lglgetprops (cloned);
w->cloned.decs -= lglgetdecs (w->lgl);
w->cloned.confs -= lglgetconfs (w->lgl);
w->cloned.props -= lglgetprops (w->lgl);
if (pthread_mutex_unlock (&w->cloned.lock))
warn ("worker %d failed to unlock 'cloned' mutex", WID (w));
if (verbose >=2 && statsfile) {
lglsetout (cloned, statsfile);
lglstats (cloned);
lglsetout (cloned, stdout);
}
msg (w, 1, "joining cloned solver");
#ifndef NDEBUG
oldres =
#else
(void)
#endif
lglunclone (w->lgl, cloned);
assert (!oldres || res == oldres);
assert (res);
}
return res;
}
static void * work (void * voidptr) {
int i, last, pm, lm, count, lit, idx, *a, * p, size, red, fin;
double start, end, delta, avg;
Worker * w = voidptr;
msg (w, 1, "running");
for (;;) {
if (pthread_mutex_lock (&queuemutex))
die ("worker %d failed to lock 'queue' mutex", WID (w));
assert (queue <= nassumptions);
if (deterministic && (queue % nworkers) != WID (w)) {
if (pthread_mutex_unlock (&queuemutex))
die ("worker %d failed to unlock 'queue' mutex", WID (w));
usleep (1000);
continue;
}
if ((last = queue) < nassumptions) queue++;
if (pthread_mutex_unlock (&queuemutex))
die ("worker %d failed to unlock 'queue' mutex", WID (w));
if (last == nassumptions) {
DONE:
if (!bar) msg (w, 1, "done");
return 0;
}
msg (w, 2, "got job %d", last);
count = 0;
for(i = w->last + 1; i <= last; i++) {
a = assumptions[i];
if (addassumptions > 1 && i < last) {
for (p = a; (lit = *p); p++) lgladd (w->lgl, -lit);
lgladd (w->lgl, 0);
}
if (!nomelt)
for (p = a; (lit = *p); p++)
if (used [idx = abs (lit)] == i)
lglmelt (w->lgl, idx), count++;
}
msg (w, 2, "melted %d variables", count);
a = assumptions[w->last = last];
if (noreverse) {
for (p = a; (lit = *p); p++)
lglassume (w->lgl, lit);
} else {
for (i = 0; a[i]; i++)
;
for (p = a + i - 1; p >= a; p--)
lglassume (w->lgl, *p);
}
start = getime ();
w->res = sat (w);
end = getime ();
delta = end - start;
delta = (delta <= 0) ? 0 : delta;
times[last] = delta;
if (bar) {
(void) pthread_mutex_lock (&finishedmutex);
fin = ++finished;
sumtimes += delta;
avg = sumtimes / fin;
(void) pthread_mutex_unlock (&finishedmutex);
pm = (1000*(fin-1))/nassumptions;
lm = (1000*fin)/nassumptions;
if (pm < lm) progress (lm, fin, nassumptions, avg, 0);
}
if (w->res == 10) {
if (!bar) msg (w, 1, "job %d SATISFIABLE", last);
if (pthread_mutex_lock (&donemutex))
warn ("worker %d failed to lock 'done' mutex", WID (w));
done = 1;
if (pthread_mutex_unlock (&donemutex))
warn ("worker %d failed to unlock 'done' mutex", WID (w));
goto DONE;
} else if (w->res == 20) {
w->nfailed = 0;
if (!w->failed) NEW (w->failed, maxassumptionsize);
for (p = a; (lit = *p); p++)
if (lglfailed (w->lgl, lit)) {
assert (w->nfailed < maxassumptionsize);
w->failed[w->nfailed++] = lit;
}
if (druptraceprefix) {
assert (w->proof);
for (i = 0; i < w->nfailed; i++)
fprintf (w->proof, "%d ", -w->failed[i]);
fputs ("0\n", w->proof);
for (i = 0; i < w->nfailed; i++)
fprintf (w->proof, "%d ", -w->failed[i]);
fputs ("0\n", w->proof);
}
if (addassumptions) {
for (i = 0; i < w->nfailed; i++)
lgladd (w->lgl, -w->failed[i]);
lgladd (w->lgl, 0);
}
if (druptraceprefix) {
assert (w->post);
for (i = 0; i < w->nfailed; i++)
fprintf (w->post, "%d ", -w->failed[i]);
fputs ("0\n", w->post);
}
red = w->nfailed;
sumassumptions += (size = p - a);
redassumptions += red;
if (!bar)
msg (w, 1, "job %d UNSATISFIABLE (%d failed / %d) in %.3f seconds",
last, red, size, delta);
if (!red && !deterministic) {
if (!bar) msg (w, 1, "job %d ACTUALLY FOUND EMPTY CLAUSE", last);
if (pthread_mutex_lock (&donemutex))
warn ("worker %d failed to lock 'done' mutex", WID (w));
done = 1;
if (pthread_mutex_unlock (&donemutex))
warn ("worker %d failed to unlock 'done' mutex", WID (w));
goto DONE;
}
if (reduce) lglreducecache (w->lgl);
} else {
if (!bar) msg (w, 1, "job %d UNKNOWN", last);
goto DONE;
}
}
}
static void init (void) {
Worker * w;
assert (nworkers > 0);
NEW (workers, nworkers);
for (w = workers; w < workers + nworkers; w++) {
w->last = -1;
w->lgl = lglinit ();
pthread_mutex_init (&w->cloned.lock, 0);
initlgl (w->lgl, w, 1);
}
msg (0, 1, "allocated %d workers", nworkers);
}
static void reset (void) {
int i, * p, * a;
if (vals) DEL (vals, nvars);
for (i = 0; i < nworkers; i++) {
Worker * w = workers + i;
lglrelease (w->lgl);
if (w->proof) {
assert (druptraceprefix);
assert (w->proof);
w->proof = 0;
assert (w->post);
fclose (w->post);
w->post = 0;
} else assert (!w->post);
if (w->failed) DEL (w->failed, maxassumptionsize);
}
DEL (workers, nworkers);
for (i = 0; i < nassumptions; i++) {
for (p = (a = assumptions[i]); *p; p++)
;
DEL (a, (p - a) + 1);
}
DEL (assumptions, szassumptions);
DEL (times, nassumptions);
DEL (lits, szlits);
DEL (used, szvars);
if (allocated)
warn ("internal memory leak of %lld bytes", (long long) allocated);
}
static void perr (const char * fmt, ...) {
va_list ap;
fprintf (stderr, "%s:%d: ", inputname, lineno);
va_start (ap, fmt);
vfprintf (stderr, fmt, ap);
fputc ('\n', stderr);
fflush (stderr);
exit (1);
}
static int next (void) {
int res;
res = getc (inputfile);
if (res == '\n') lineno++;
return res;
}
static void add (int lit) {
int i;
for (i = 0; i < nworkers; i++) lgladd (workers[i].lgl, lit);
}
static void parse (void) {
int ch, lit, sign, * assumption, i;
HEADER:
ch = next ();
if (ch == EOF) perr ("unexpected end-of-file in header");
if (ch == 'c') {
while ((ch = next ()) != '\n')
if (ch == EOF)
perr ("unexpected end-of-file in header comment");
goto HEADER;
}
if (ch != 'p' ||
next () != ' ' ||
next () != 'i' ||
next () != 'n' ||
next () != 'c' ||
next () != 'c' ||
next () != 'n' ||
next () != 'f') perr ("invalid header (expected 'p inccnf')");
ch = next ();
CLAUSES:
if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n') {
ch = next (); goto CLAUSES;
}
if (ch == 'c') {
while ((ch = next ()) != '\n')
if (ch == EOF)
perr ("unexpected end-of-file in body comment");
goto CLAUSES;
}
if (ch == EOF && nlits) perr ("unexpected end-of-file in clause");
if (ch == 'a' && nlits) perr ("unexpected 'a' in clause");
if (ch == 'a') goto ASSUMPTIONS;
if (ch == EOF) goto DONE;
if (ch == 'a') goto ASSUMPTIONS;
if (ch == '-') {
sign = -1;
ch = next ();
if (!isdigit (ch)) perr ("expected digit after '-'");
} else sign = 1;
if (!isdigit (ch)) perr ("expected literal");
lit = ch - '0';
while (isdigit (ch = next ())) lit = 10*lit + ch - '0';
if (lit > nvars) {
if (lit >= szvars) {
int oldszvars = szvars;
szvars = szvars ? 2*szvars : 1;
while (szvars <= lit) szvars *= 2;
RSZ (used, oldszvars, szvars);
for (i = oldszvars; i < szvars; i++) used[i] = -1;
}
assert (lit < szvars);
nvars = lit;
}
lit *= sign;
if (lit) nlits++; else nlits = 0, nclauses++;
add (lit);
goto CLAUSES;
ASSUMPTIONS:
assert (!nlits);
assert (ch == 'a');
ch = next ();
if (ch != ' ') perr ("expected space after 'a'");
LITS:
ch = next ();
if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n') goto LITS;
if (ch == EOF && nlits) perr ("unexpected end-of-file in assumptions");
if (ch == '-') {
sign = -1;
ch = next ();
if (!isdigit (ch)) perr ("expected digit after '-'");
} else sign = 1;
if (!isdigit (ch)) perr ("expected literal");
lit = ch - '0';
while (isdigit (ch = next ())) lit = 10*lit + ch - '0';
if (lit > nvars)
perr ("assumption %d exceeds maximum variables %d", lit, nvars);
assert (0 <= lit && lit < szvars);
if (used[lit] < 0) nused++;
used[lit] = nassumptions;
lit *= sign;
if (ch != ' ' && ch != '\t' && ch != '\r' && ch != '\n')
perr ("expected white space after '%l'", lit);
if (lit) { PUSH (lits, lit); goto LITS; }
NEW (assumption, nlits + 1);
for (i = 0; i < nlits; i++) assumption[i] = lits[i];
assert (!assumption[nlits]);
PUSH (assumptions, assumption);
if (nlits > maxassumptionsize) maxassumptionsize = nlits;
nlits = 0;
NEXT:
ch = next ();
if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n') goto NEXT;
if (ch == EOF) goto DONE;
if (ch == '-' || isdigit (ch))
#if 1
goto CLAUSES;
if (ch != 'a') perr ("expected literal, 'a' or end-of-file");
#else#endif
goto ASSUMPTIONS;
DONE:
msg (0, 1, "maximum variable %d in %d clauses", nvars, nclauses);
msg (0, 1, "parsed %d assumptions", nassumptions);
nvars++;
NEW (times, nassumptions);
for (i = 0; i < nassumptions; i++) times[i] = -1;
}
static void freeze (void) {
int idx, i;
for (idx = 1; idx < nvars; idx++)
if (used[idx] >= 0)
for (i = 0; i < nworkers; i++)
lglfreeze (workers[i].lgl, idx);
}
static void start (void) {
Worker * w;
for (w = workers; w < workers + nworkers; w++) {
if (pthread_create (&w->thread, 0, work, w))
die ("failed to create worker thread %d", WID (w));
}
}
static void stop (void) {
Worker * w;
double avg;
for (w = workers; w < workers + nworkers; w++)
if (pthread_join (w->thread, 0))
die ("failed to join worker %d", WID (w));
if (bar) {
avg = finished ? sumtimes / finished : 0.0;
progress ((1000*finished)/nassumptions, finished, nassumptions, avg, 1);
}
msg (0, 1, "joined all %d workers", nworkers);
}
static void statsps (FILE * file,
const char * name, long long stats, double time) {
const char * scale;
if (stats > 10000000) scale = " million", stats /= 1000000;
else if (stats > 10000) scale = " thousand", stats /= 1000;
else scale = "";
fprintf (file,
"c %lld%s %s, %.1f%s per second\n",
stats, scale, name, (time > 0 ? stats/time : 0.0), scale);
}
static int cmpdblptr (const void * p, const void * q) {
double a = *(double*)p;
double b = *(double*)q;
if (a < b) return -1;
if (a > b) return 1;
return 0;
}
static void stats (void) {
int64_t decs = 0, confs = 0, props = 0;;
double mb = maxallocated / (double)(1<<20);
double wct = getime (), prt = lglprocesstime ();
FILE * file = statsfile ? statsfile : stdout;
double sum, t, min, max, avg, std;
int i, n, cloned = 0;
for (i = 0; i < nworkers; i++) lglflushtimers (workers[i].lgl);
for (i = 0; i < nworkers; i++) {
lglflushtimers (workers[i].lgl);
fprintf (file, "c\n");
fprintf (file, "c ---------[worker %d stats]------------------\n", i);
fprintf (file, "c\n");
lglsetout (workers[i].lgl, file);
lglstats (workers[i].lgl);
lglsetout (workers[i].lgl, stdout);
mb += lglmb (workers[i].lgl);
decs += lglgetdecs (workers[i].lgl);
confs += lglgetconfs (workers[i].lgl);
props += lglgetprops (workers[i].lgl);
if (pthread_mutex_lock (&workers[i].cloned.lock))
warn ("worker failed to lock 'cloned' mutex");
if (workers[i].cloned.lgl) {
fprintf (file, "c ---------[cloned worker %d dstats]----------\n", i);
fprintf (file, "c\n");
lglsetout (workers[i].cloned.lgl, file);
lglstats (workers[i].cloned.lgl);
lglsetout (workers[i].cloned.lgl, stdout);
mb += lglmb (workers[i].cloned.lgl);
decs += lglgetdecs (workers[i].cloned.lgl);
confs += lglgetconfs (workers[i].cloned.lgl);
props += lglgetprops (workers[i].cloned.lgl);
mb -= lglmb (workers[i].lgl);
decs -= lglgetdecs (workers[i].lgl);
confs -= lglgetconfs (workers[i].lgl);
props -= lglgetprops (workers[i].lgl);
}
decs += workers[i].cloned.decs;
confs += workers[i].cloned.confs;
props += workers[i].cloned.props;
cloned += workers[i].cloned.count;
if (pthread_mutex_unlock (&workers[i].cloned.lock))
warn ("worker failed to lock 'cloned' mutex");
}
fprintf (file, "c\n");
fprintf (file, "c ---------[global-stats]-------------------------\n");
fprintf (file, "c\n");
statsps (file, "scheduled jobs", queue, wct);
fprintf (file, "c %d failed assumptions %.0f%% out of %d\n",
redassumptions,
sumassumptions ? (100.0*redassumptions)/sumassumptions : 0,
sumassumptions);
fprintf (file, "c\n");
fprintf (file, "c %d cloned\n", cloned);
fprintf (file, "c\n");
statsps (file, "conflicts", confs, wct);
statsps (file, "decisions", decs, wct);
statsps (file, "propagations", props, wct);
fprintf (file, "c wall clock time %.1f seconds\n", wct);
fprintf (file, "c process time %.1f seconds\n", prt);
fprintf (file, "c utilization %.0f%%\n",
wct > 0 ? 100.0 * (prt / wct / nworkers) : 0.0);
fflush (file);
n = 0;
sum = 0;
max = min = -1;
for (i = 0; i < nassumptions; i++) {
if ((t = times[i]) < 0) continue;
sum += t;
times[n++] = t;
if (min < 0 || (t < min)) min = t;
if (max < 0 || (t > max)) max = t;
}
if (n) {
fprintf (file, "c\n");
avg = sum/n;
fprintf (file, "c %d finished jobs in average time %.3f\n", n, avg);
fprintf (file, "c time: sum %.3f, min %.3f, max %.3f\n", sum, min, max);
std = 0;
for (i = 0; i < n; i++) {
t = times[i] - avg;
std += t*t;
}
std = sqrt (std);
qsort (times, n, sizeof times, cmpdblptr);
fprintf (file, "c time: median %.3f, std dve %.3f\n", times[n/2], std);
}
fflush (file);
}
static void hist (void) {
FILE * file = histfile ? histfile : stdout;
int i;
for (i = 0; i < nassumptions; i++)
fprintf (file, "%.3f\n", times[i]);
fflush (file);
}
static int catchedsig;
static void (*sig_int_handler)(int);
static void (*sig_segv_handler)(int);
static void (*sig_abrt_handler)(int);
static void (*sig_term_handler)(int);
static void resetsighandlers (void) {
(void) signal (SIGINT, sig_int_handler);
(void) signal (SIGSEGV, sig_segv_handler);
(void) signal (SIGABRT, sig_abrt_handler);
(void) signal (SIGTERM, sig_term_handler);
}
static void caughtsigmsg (int sig) {
if (!verbose) return;
printf ("c\nc CAUGHT SIGNAL %d\nc\n", sig);
fflush (stdout);
}
static void catchsig (int sig) {
if (!catchedsig) {
fputs ("s UNKNOWN\n", stdout);
fflush (stdout);
catchedsig = 1;
caughtsigmsg (sig);
if (statsfile) stats ();
if (histfile) hist ();
if (statsfile || histfile) caughtsigmsg (sig);
}
resetsighandlers ();
if (!getenv ("LGLNABORT")) raise (sig); else exit (1);
}
static void setsighandlers (void) {
sig_int_handler = signal (SIGINT, catchsig);
sig_segv_handler = signal (SIGSEGV, catchsig);
sig_abrt_handler = signal (SIGABRT, catchsig);
sig_term_handler = signal (SIGTERM, catchsig);
}
int main (int argc, char ** argv) {
const char * statsfilename = 0, * histfilename = 0;
int i, closeinputfile, res = 0;
Worker * winner, * w;
startime = currentime ();
for (i = 1; i < argc; i++) { if (!strcmp (argv[i], "-h")) {
printf (
"usage: ilingeling [<option> ...][<inccnf>][<nworkers>]\n"
"\n"
"where <option> is one of the following:\n"
"\n"
" -h print this command line option summary\n"
"\n"
" -v increase verbose level\n"
" -q do not print 'c job ...' lines (requires verbosity < 2)\n"
" -b progress bar (implies '-q')\n"
"\n"
" --version\n"
"\n"
" -s <stats> output statistics to separate file\n"
" -t <hist> output job run time histogram to separate file\n"
"\n"
" --clone use cloning for hard cubes\n"
" --reduce reduce learned clause cache after each job\n"
" --no-melt do not melt unused assumption variables\n"
" --no-flush do not flush learned clause cache before every job\n"
" --no-reverse do not reverse assumptions\n"
"\n"
" --deterministic | --det\n"
"\n"
" jobs are mapped deterministically to workers\n"
"\n"
" --no-add do not add failed assumptions as don't care\n"
" -A add all assumptions as don't care\n"
"\n"
" <inccnf> 'p inccnf' + '<lit*> 0' clauses + 'a <lit>* 0' assumptions\n"
" <nworkers> number of workers defaults to 1\n"
"\n"
" -d|--drup <path-prefix-for-traces>\n");
exit (0);
} else if (!strcmp (argv[i], "--version")) {
printf ("%s\n", lglversion ());
exit (0);
} else if (!strcmp (argv[i], "-v")) verbose++;
else if (!strcmp (argv[i], "-b")) bar = 1;
else if (!strcmp (argv[i], "-n")) nowitness = 1;
else if (!strcmp (argv[i], "--no-reverse")) noreverse = 1;
else if (!strcmp (argv[i], "--no-add")) addassumptions = 0;
else if (!strcmp (argv[i], "--no-melt")) nomelt = 1;
else if (!strcmp (argv[i], "--reduce")) reduce = 1;
else if (!strcmp (argv[i], "--deterministic") ||
!strcmp (argv[i], "--det"))
deterministic = 1;
else if (!strcmp (argv[i], "-A")) addassumptions = 2;
else if (!strcmp (argv[i], "-p")) plain = 1;
else if (!strcmp (argv[i], "-s")) {
if (statsfilename) die ("two '-s' options");
if (++i == argc) die ("argument to '-s' missing");
statsfilename = argv[i];
} else if (!strcmp (argv[i], "-t")) {
if (histfilename) die ("two '-t' options");
if (++i == argc) die ("argument to '-t' missing");
histfilename = argv[i];
} else if (!strcmp (argv[i], "--clone")) doclone = 1;
else if (!strcmp (argv[i], "--no-flush")) noflush = 1;
else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--drup")) {
if (++i == argc) die ("argument to '%s' missing", argv[i]);
if (druptraceprefix) die ("DRUP path prefix set twice");
druptraceprefix = argv[i];
}
else if (argv[i][0] == '-') die ("invalid option '%s'", argv[i]);
else if (isnum (argv[i])) {
if (nworkers) die ("number of workers specified twice: '%d' and '%s'",
nworkers, argv[i]);
if ((nworkers = atoi (argv[i])) <= 0)
die ("invalid number of workers argument: '%s'", argv[i]);
} else if (inputname)
die ("two files given: '%s' and '%s'", inputname, argv[i]);
else inputname = argv[i];
}
if (bar && !isatty (1))
die ("progress bar requested but <stdout> not connected to terminal");
if (verbose >= 2 && bar) die ("verbosity %d > 1 with '-b'", verbose);
if (statsfilename && !(statsfile = fopen (statsfilename, "w")))
die ("can not write to stats file '%s'", statsfilename);
if (histfilename && !(histfile = fopen (histfilename, "w")))
die ("can not write to job run time histogram file '%s'", histfilename);
if (verbose && !statsfile) statsfile = stdout;
if (verbose)
lglbnr ("iLingeling Incremental Parallel Lingeling", "c ", stdout),
printf ("c\n"), fflush (stdout);
if (!nworkers) nworkers = 1;
msg (0, 1, "using %d workers", nworkers);
if (inputname) {
if (!(inputfile = fopen (inputname, "r")))
die ("can not read '%s'", inputname);
closeinputfile = 1;
} else inputname = "<stdin>", inputfile = stdin, closeinputfile = 0;
init ();
setsighandlers ();
msg (0, 1, "parsing %s", inputname);
parse ();
if (closeinputfile) fclose (inputfile);
msg (0, 1, "%d variables out of %d used in assumptions which is %.0f%%",
nused, nvars, nvars ? 100.0 * (nused /(double)nvars) : 0.0);
freeze ();
start ();
stop ();
winner = 0;
for (w = workers; w < workers + nworkers; w++)
if (w->res) { winner = w; if (w->res == 10) break; }
if (winner && (res = winner->res) == 10 && !nowitness) {
NEW (vals, nvars);
for (i = 1; i < nvars; i++)
vals[i] = lglderef (winner->lgl, i);
}
assert (winner || !nassumptions);
resetsighandlers ();
if (statsfile) stats ();
if (statsfilename) fclose (statsfile);
if (histfile) hist ();
if (histfile) fclose (histfile);
if (res == 10) printf ("s SATISFIABLE\n");
else if (res == 20) printf ("s UNSATISFIABLE\n");
else printf ("s UNKNOWN\n");
fflush (stdout);
if (vals) {
for (i = 1; i < nvars; i++) {
fputs ("v ", stdout);
if (vals[i] < 0) fputc ('-', stdout);
printf ("%d\n", i);
}
fputs ("v 0\n", stdout);
fflush (stdout);
}
reset ();
return res;
}