#include "lglib.h"
#include "aiger.h"
#include <assert.h>
#include <ctype.h>
#include <limits.h>
#include <signal.h>
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
typedef struct Clause { int * lits; } Clause;
static aiger * model;
static unsigned num_bad;
static aiger_symbol * badsyms;
static FILE *outfile, *msgfile, *errfile, *apitrace;
static int verbose, xstim, plain, nowitness, noclone;
static LGL * lgl, * clone;
static int * coi, opt = 3;
static int cloned;
static Clause * clauses;
static int nclauses, szclauses;
static int * lits;
static int nlits, szlits;
static int maxvar;
static int * litmap;
static int k;
static size_t maxbytes, curbytes;
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 msg (int level, const char * fmt, ...) {
va_list ap;
if (verbose < level) return;
fprintf (msgfile, "c [blimc] %.2f ", lglprocesstime ());
va_start (ap, fmt);
vfprintf (msgfile, fmt, ap);
va_end (ap);
fputc ('\n', msgfile);
fflush (msgfile);
}
static void caughtsigmsg (int sig) {
if (!verbose) return;
fprintf (errfile, "c [blimc]\nc [blimc] CAUGHT SIGNAL %d\nc [blimc]\n", sig);
fflush (errfile);
}
static void stats (void) {
if (verbose) {
if (clone) lglstats (clone);
if (lgl) lglstats (lgl);
}
msg (1, "reached k = %d", k);
msg (1, "cloned %d solvers", cloned);
msg (1, "max %.1f MB", maxbytes/(double)(1<<20));
}
static void catchsig (int sig) {
if (!catchedsig) {
fputs ("s UNKNOWN\n", errfile);
fflush (errfile);
catchedsig = 1;
caughtsigmsg (sig);
if (verbose) stats (), 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);
}
static void die (const char * fmt, ...) {
va_list ap;
fputs ("*** blimc: ", errfile);
va_start (ap, fmt);
vfprintf (errfile, fmt, ap);
va_end (ap);
fputc ('\n', errfile);
fflush (errfile);
exit (1);
}
static void * new (void * state, size_t bytes) {
char * res;
(void) state;
res = malloc (bytes);
if (!res) die ("out of memory");
curbytes += bytes;
if (curbytes > maxbytes) maxbytes = curbytes;
return res;
}
static void del (void * state, void * ptr, size_t bytes) {
(void) state;
assert (curbytes >= bytes);
curbytes -= bytes;
free (ptr);
}
static void * rsz (void * state, void * ptr, size_t o, size_t n) {
char * res;
(void) state;
assert (curbytes >= o);
curbytes -= o;
res = realloc (ptr, n);
if (!res) die ("out of memory");
curbytes += n;
if (curbytes > maxbytes) maxbytes = curbytes;
return res;
}
static int prepilit (unsigned ulit) {
int res;
assert (aiger_lit2var (ulit) <= model->maxvar);
assert (coi[aiger_lit2var (ulit)]);
assert (ulit <= 2*model->maxvar + 1);
res = (ulit>>1) + 1;
if (ulit & 1) res = -res;
return res;
}
static unsigned aiginput (unsigned idx) {
assert (idx < model->num_inputs);
return model->inputs[idx].lit;
}
static int prepinput (unsigned idx) { return prepilit (aiginput (idx)); }
static unsigned aiglatch (unsigned idx) {
assert (idx < model->num_latches);
return model->latches[idx].lit;
}
static unsigned aigreset (unsigned idx) {
assert (idx < model->num_latches);
return model->latches[idx].reset;
}
static int preplatch (unsigned idx) { return prepilit (aiglatch (idx)); }
static unsigned aignext (unsigned idx) {
assert (idx < model->num_latches);
return model->latches[idx].next;
}
static int prepnext (unsigned idx) { return prepilit (aignext (idx)); }
static unsigned aigbad (unsigned idx) {
assert (idx < num_bad);
return badsyms[idx].lit;
}
static int prepbad (unsigned idx) { return prepilit (aigbad (idx)); }
static int preplhs (unsigned idx) {
assert (idx < model->num_ands);
return prepilit (model->ands[idx].lhs);
}
static int prepleft (unsigned idx) {
assert (idx < model->num_ands);
return prepilit (model->ands[idx].rhs0);
}
static int prepright (unsigned idx) {
assert (idx < model->num_ands);
return prepilit (model->ands[idx].rhs1);
}
static void unit (int ilit) { lgladd (lgl, ilit); lgladd (lgl, 0); }
static void binary (int a, int b) {
lgladd (lgl, a);
lgladd (lgl, b);
lgladd (lgl, 0);
}
static void ternary (int a, int b, int c) {
lgladd (lgl, a);
lgladd (lgl, b);
lgladd (lgl, c);
lgladd (lgl, 0);
}
static int ulitincoi (unsigned ulit) {
unsigned idx;
assert (ulit <= 2*model->maxvar + 1);
idx = aiger_lit2var (ulit);
assert (idx <= model->maxvar);
return coi[idx];
}
static void prepfreeze (void) {
unsigned i;
msg (2, "freeze");
for (i = 0; i < model->num_inputs; i++)
if (!nowitness && ulitincoi (aiginput (i)))
lglfreeze (lgl, prepinput (i));
for (i = 0; i < model->num_latches; i++) {
if (!ulitincoi (aiglatch (i))) continue;
lglfreeze (lgl, preplatch (i));
lglfreeze (lgl, prepnext (i));
}
for (i = 0; i < num_bad; i++) {
assert (ulitincoi (badsyms[i].lit));
lglfreeze (lgl, prepbad (i));
}
if (ulitincoi (0)) lglfreeze (lgl, 1);
}
static void and (int lhs, int rhs0, int rhs1) {
binary (-lhs, rhs0);
binary (-lhs, rhs1);
ternary (-rhs0, -rhs1, lhs);
}
static void logic (void) {
unsigned i;
msg (2, "logic");
if (ulitincoi (0)) unit (-1);
for (i = 0; i < model->num_ands; i++)
if (ulitincoi (model->ands[i].lhs))
and (preplhs (i), prepleft (i), prepright (i));
}
static const char * usage =
"usage: blimc [-h][-v][-x][-n][-p][-O[0123]][--no-clone][<maxk>][<aiger>]\n"
;
static int isnumstr (const char * str) {
const char * p = str;
int ch;
if (!isdigit (*p++)) return 0;
while (isdigit ((ch = *p))) p++;
return !ch;
}
static double percent (double a, double b) {
return b ? 100.0 * (a / b) : 0.0;
}
static void coimsg (const char * name, unsigned remaining, unsigned all) {
msg (1, "%-9s in COI: %10u = %3.0f%% out of %u",
name, remaining, percent (remaining, all), all);
}
static void travcoi (void) {
unsigned next, top, size, latches, inputs, ands, constants;
unsigned lit, * stack, idx, stripped;
aiger_symbol * s;
aiger_and * a;
size = model->maxvar + 1;
stack = new (0, size * sizeof *stack);
latches = inputs = ands = constants = 0;
assert (num_bad == 1);
lit = badsyms[0].lit;
idx = aiger_lit2var (lit);
coi[idx] = top = next = 1;
for (;;) {
assert (idx <= model->maxvar);
assert (coi[idx]);
stripped = aiger_strip (lit);
if (aiger_is_input (model, stripped)) inputs++;
else if ((s = aiger_is_latch (model, stripped))) {
latches++;
lit = s->next;
idx = aiger_lit2var (lit);
assert (idx <= model->maxvar);
if (!coi[idx]) stack[top++] = lit, coi[idx] = top;
} else if ((a = aiger_is_and (model, stripped))) {
ands++;
lit = a->rhs0;
idx = aiger_lit2var (lit);
assert (idx <= model->maxvar);
if (!coi[idx]) stack[top++] = lit, coi[idx] = top;
lit = a->rhs1;
idx = aiger_lit2var (lit);
assert (idx <= model->maxvar);
if (!coi[idx]) stack[top++] = lit, coi[idx] = top;
} else assert (!stripped), constants++;
if (next == top) break;
lit = stack[next++];
}
del (0, stack, size * sizeof * stack);
coimsg ("literals", top, model->maxvar);
coimsg ("inputs", inputs, model->num_inputs);
coimsg ("latches", latches, model->num_latches);
coimsg ("constants", constants, 1);
coimsg ("ands", ands, model->num_ands);
}
static void newlgl (int setapitrace) {
const char * apitracename = getenv ("BLIMCLGLAPITRACE");
lgl = lglminit (0,new,rsz,del);
if (setapitrace && apitracename) {
assert (!apitrace);
apitrace = fopen (apitracename, "w");
if (!apitrace)
die ("can write to API trace file '%s'", apitracename);
lglwtrapi (lgl, apitrace);
}
lglsetout (lgl, msgfile);
if (verbose >= 2) lglsetopt (lgl, "verbose", verbose - 1);
if (plain) lglsetopt (lgl, "plain", 1);
}
static void extract (void * dummy, int lit) {
size_t oldbytes, newbytes;
Clause * c;
int i;
(void) dummy;
if (lit) {
if (nlits == szlits) {
oldbytes = szlits * sizeof *lits;
szlits = szlits ? 2*szlits : 1;
newbytes = szlits * sizeof *lits;
lits = rsz (0, lits, oldbytes, newbytes);
}
lits[nlits++] = lit;
} else {
if (nclauses == szclauses) {
oldbytes = szclauses * sizeof *clauses;
szclauses = szclauses ? 2*szclauses : 1;
newbytes = szclauses * sizeof *clauses;
clauses = rsz (0, clauses, oldbytes, newbytes);
}
c = clauses + nclauses++;
newbytes = (nlits + 1) * sizeof *c->lits;
c->lits = new (0, newbytes);
for (i = 0; i < nlits; i++) c->lits[i] = lits[i];
c->lits[i] = 0;
nlits = 0;
}
}
static int mapuntimedlit (int lit) {
int idx = abs (lit), res;
assert (1 <= idx && idx <= (int) model->maxvar + 1);
if (!(res = litmap[idx])) litmap[idx] = res = ++maxvar;
if (lit < 0) res = -res;
return res;
}
static void mapcnf (void) {
int * p, lit;
Clause * c;
for (c = clauses; c < clauses + nclauses; c++)
for (p = c->lits; (lit = *p); p++)
*p = mapuntimedlit (lit);
}
static int mainilit (unsigned ulit) {
int tmp = prepilit (ulit), idx = abs (tmp), res;
assert (1 <= idx && idx <= (int) model->maxvar+1);
res = litmap[idx];
if (tmp < 0) res = -res;
return res;
}
static int shift (int ilit, int time) {
int idx = abs (ilit), res;
assert (1 <= idx && idx <= maxvar);
res = idx + time * maxvar;
if (ilit < 0) res = -res;
return res;
}
static void equiv (int a, int b) { binary (-a, b); binary (a, -b); }
static void shiftcnf (int time) {
int * p, lit, prev;
unsigned i;
Clause * c;
assert (0 <= time);
if (time > 0) {
for (i = 0; i < model->num_latches; i++) {
if (!ulitincoi (aiglatch (i))) continue;
prev = shift (mainilit (aignext (i)), time-1);
lit = shift (mainilit (aiglatch (i)), time);
equiv (prev, lit);
lglmelt (lgl, prev);
}
}
for (c = clauses; c < clauses + nclauses; c++) {
for (p = c->lits; (lit = *p); p++) lgladd (lgl, shift (lit, time));
lgladd (lgl, 0);
}
for (i = 0; i < model->num_latches; i++)
if (ulitincoi (aiglatch (i)))
lglfreeze (lgl, shift (mainilit (aignext (i)), time));
}
static void bad (LGL * whichlgl, int time) {
lglassume (whichlgl, shift (mainilit (aigbad (0)), time));
}
static void init (void) {
size_t bytes;
unsigned i;
int lit;
bytes = (model->maxvar + 2) * sizeof *litmap;
litmap = new (0, bytes);
memset (litmap, 0, bytes);
assert (!maxvar);
maxvar = 0; for (i = 0; i < model->num_latches; i++) {
if (!ulitincoi (aiglatch (i))) continue;
lit = ++maxvar;
litmap[preplatch (i)] = lit;
}
for (i = 0; i < model->num_inputs; i++) {
if (!ulitincoi (aiginput (i))) continue;
lit = ++maxvar;
litmap[prepinput (i)] = lit;
}
mapcnf ();
for (i = 0; i < model->num_latches; i++)
if (ulitincoi (aiglatch (i)))
(void) mapuntimedlit (prepnext (i));
msg (1, "mapped %d variables", maxvar);
#ifndef NDEBUG
for (i = 0; i < num_bad; i++)
if (ulitincoi (aigbad (i)))
assert (litmap[abs (prepbad (i))]);
#endif
for (i = 0; i < model->num_latches; i++) {
if (!ulitincoi (aiglatch (i))) continue;
if (aiglatch (i) == aigreset (i)) continue;
if (aiger_false == aigreset (i)) unit (-mainilit (aiglatch (i)));
if (aiger_true == aigreset (i)) unit (mainilit (aiglatch (i)));
}
}
static int length (const int * p) {
const int * q;
for (q = p; *q; q++)
;
return q - p;
}
int main (int argc, char ** argv) {
int res, i, lit, maxk, val;
unsigned j, init0, init1, initx;
const char * iname, * err;
size_t coibytes;
char prefix[80];
#ifndef NDEBUG
int fres;
#endif
LGL * tmp;
char vch;
outfile = stdout, msgfile = errfile = stderr;
iname = 0;
maxk = 0;
for (i = 1; i < argc; i++) {
if (!strcmp (argv[i], "-h")) { fputs (usage, outfile); exit (0);}
else if (!strcmp (argv[i], "-v")) verbose++;
else if (!strcmp (argv[i], "-x")) xstim = 1;
else if (!strcmp (argv[i], "-n")) nowitness = 1;
else if (!strcmp (argv[i], "-p")) plain = 1;
else if (!strcmp (argv[i], "-O")) opt = 1;
else if (!strcmp (argv[i], "-O0")) opt = 0;
else if (!strcmp (argv[i], "-O1")) opt = 1;
else if (!strcmp (argv[i], "-O2")) opt = 2;
else if (!strcmp (argv[i], "-O3")) opt = 3;
else if (!strcmp (argv[i], "--no-clone")) noclone = 1;
else if (argv[i][0] == '-')
die ("invalid command line option '%s'", argv[i]);
else if (isnumstr (argv[i])) maxk = atoi (argv[i]);
else if (iname)
die ("two files specified '%s' and '%s'", iname, argv[i]);
else iname = argv[i];
}
if (verbose)
lglbnr ("BLIMC Bounded Lingeling Model Checker",
"c [blimc] ", msgfile);
setsighandlers ();
msg (1, "reading %s", iname ? iname : "<stdin>");
model = aiger_init ();
if (iname) err = aiger_open_and_read_from_file (model, iname);
else err = aiger_read_from_file (model, stdin);
if (err) die ("parse error in '%s' at %s",
iname ? iname : "<stdin>", err);
msg (1, "MILOA %u %u %u %u %u",
model->maxvar,
model->num_inputs,
model->num_latches,
model->num_outputs,
model->num_ands);
msg (1, "BCJK %u %u %u %u %u",
model->num_bad,
model->num_constraints,
model->num_justice,
model->num_fairness);
if (!model->num_outputs && !model->num_bad)
die ("model contains no output nor bad state property");
if (model->num_bad > 1)
die ("can not handle multiple bad state properties");
if (!model->num_bad && model->num_outputs > 1)
die ("can not handle multiple outputs (without bad state property)");
if (model->num_constraints > 0)
die ("can not handle environment constraints");
if (model->num_justice)
msg (1, "ignoring %d justice properties", model->num_justice);
if (model->num_fairness)
msg (1, "ignoring %d fairness constraints", model->num_fairness);
if (model->num_bad) num_bad = model->num_bad, badsyms = model->bad;
else num_bad = model->num_outputs, badsyms = model->outputs;
assert (num_bad == 1);
init0 = init1 = initx = 0;
for (j = 0; j < model->num_latches; j++) {
unsigned rst = aigreset (j);
if (rst == aiger_false) init0++;
if (rst == aiger_true) init1++;
if (rst == aiglatch (j)) initx++;
}
if (model->num_latches) {
msg (1, "%u latches initialized to 0", init0);
msg (1, "%u latches initialized to 1", init1);
msg (1, "%u latches uninitialized", initx);
} else msg (1, "no latches, so purely combinational");
coibytes = (model->maxvar+1) * sizeof *coi;
coi = new (0, coibytes);
memset (coi, 0, coibytes);
travcoi ();
newlgl (0);
lglsetprefix (lgl, "c [lglopt] ");
logic ();
prepfreeze ();
msg (1, "encoded");
(void) lglsimp (lgl, opt);
msg (1, "simplified");
if (lglfixed (lgl, prepbad (0)) < 0) {
res = 20;
fprintf (outfile, "0\nb0\n.\n");
} else {
res = 0;
lgltravall (lgl, 0, extract);
msg (1, "extracted");
if (verbose >= 1) lglstats (lgl);
tmp = lgl, lgl = 0;
lglrelease (tmp);
newlgl (1);
lglsetopt (lgl, "flipping", 0);
lglsetopt (lgl, "boost", 0);
lglsetopt (lgl, "simpdelay", 100);
lglsetprefix (lgl, "c [lgl0] ");
init ();
msg (1, "maxk %d", maxk);
for (k = 0; k <= maxk; k++) {
msg (1, "bound %d", k);
sprintf (prefix, "c [lgl%d] ", k);
lglsetprefix (lgl, prefix);
shiftcnf (k);
bad (lgl, k);
if (!noclone) lglsetopt (lgl, "clim", 1000);
res = lglsat (lgl);
if (!res) {
assert (!clone);
assert (!noclone);
clone = lglclone (lgl);
sprintf (prefix, "c [lgl%dclone%d] ", k, cloned++);
lglsetprefix (clone, prefix);
lglfixate (clone);
lglmeltall (clone);
#if 0#endif
res = lglsimp (clone, 1);
if (!res) {
lglsetopt (clone, "clim", -1);
res = lglsat (clone);
assert (res == 10 || res == 20);
}
if (verbose >= 3) lglstats (clone);
tmp = clone, clone = 0;
#ifndef NDEBUG
fres =
#endif
lglunclone (lgl, tmp);
assert (fres == res);
lglrelease (tmp);
}
assert (res);
if (res == 10) break;
assert (res == 20);
printf ("u%d\n", k);
fflush (stdout);
if (!model->num_latches) break;
if (k < maxk && !((k + 1) & k)) (void) lglsimp (lgl, 0);
}
if (res == 10) {
fprintf (outfile, "1\nb0\n");
if (!nowitness) {
for (i = 0; i < (int) model->num_latches; i++) {
if (ulitincoi (aiglatch (i))) {
lit = shift (mainilit (aiglatch (i)), 0);
val = lglderef (lgl, lit);
} else val = 0;
if (val > 0) vch = '1';
else if (!val && xstim) vch = 'x';
else vch = '0';
fputc (vch, stdout);
}
fputc ('\n', stdout);
for (i = 0; i <= k; i++) {
for (j = 0; j < model->num_inputs; j++) {
if (ulitincoi (aiginput (j))) {
lit = shift (mainilit (aiginput (j)), i);
val = lglderef (lgl, lit);
} else val = 0;
if (val > 0) vch = '1';
else if (!val && xstim) vch = 'x';
else vch = '0';
fputc (vch, stdout);
}
fputc ('\n', stdout);
}
}
printf (".\n");
} else if (res == 20 && !model->num_latches)
fprintf (outfile, "0\nb0\n.\n");
else fprintf (outfile, "2\nb0\n.\n");
del (0, litmap, (model->maxvar + 2) * sizeof *litmap);
}
fflush (outfile);
del (0, coi, (model->maxvar+1) * sizeof *coi);
aiger_reset (model);
for (i = 0; i < nclauses; i++)
del (0, clauses[i].lits,
(length (clauses[i].lits) + 1) * sizeof *clauses[i].lits);
del (0, clauses, szclauses * sizeof *clauses);
del (0, lits, szlits * sizeof *lits);
resetsighandlers ();
stats ();
lglrelease (lgl);
if (apitrace) fflush (apitrace), fclose (apitrace);
msg (1, "exit %d", res);
return res;
}