diff --git a/COPYING b/COPYING new file mode 100644 index 0000000..9e299be --- /dev/null +++ b/COPYING @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2010-2018 Armin Biere, Johannes Kepler University Linz, Austria + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README b/README new file mode 100644 index 0000000..66f861c --- /dev/null +++ b/README @@ -0,0 +1,33 @@ +These are the sources of the SAT solver Lingeling. +The file VERSION contains the current version number. + +To build everything issue + + ./configure.sh && make + +This will build the library 'liblgl.o', the sequential solver 'lingeling', +its parallel version 'plingeling', and the cube & conquer solvers +'treengeling' and 'ilingeling'. + +If you have a compiled copy of the AIGER library in '../aiger/', which +can be obtained from 'http://fmv.jku.at/aiger' then the bounded +model checker 'blimc' will also be build. + +If you need proof support add and compile the 'druplig' library in +'../druplig/' from 'http://fmv.jku.at/druplig'. + +If you want to add local search (particularly useful for 'treengeling') add +and compile 'yalsat' in '../yalsat/' from 'http://fmv.jku.at/yalsat'. + +Copyright, authors and license are described in COPYING. + +With release 'bcj', which in essence is the version submitted +to the SAT Competition 2018, we moved to an MIT style license. + +A more recent version of Lingeling might be found at + + http://fmv.jku.at/lingeling + +and this site might also contain more documentation. + +Thu May 17 11:45:27 CEST 2018 diff --git a/VERSION b/VERSION new file mode 100644 index 0000000..a9014c1 --- /dev/null +++ b/VERSION @@ -0,0 +1 @@ +bcj diff --git a/blimc.c b/blimc.c new file mode 100644 index 0000000..8ef38b7 --- /dev/null +++ b/blimc.c @@ -0,0 +1,677 @@ +/*-------------------------------------------------------------------------*/ +/* Copyright 2010-2018 Armin Biere Johannes Kepler University Linz Austria */ +/*-------------------------------------------------------------------------*/ + +#include "lglib.h" +#include "aiger.h" + +#include +#include +#include +#include +#include +#include +#include +#include + +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 (0 <= idx && idx < model->num_inputs); + return model->inputs[idx].lit; +} + +static int prepinput (unsigned idx) { return prepilit (aiginput (idx)); } + +static unsigned aiglatch (unsigned idx) { + assert (0 <= idx && idx < model->num_latches); + return model->latches[idx].lit; +} + +static unsigned aigreset (unsigned idx) { + assert (0 <= idx && idx < model->num_latches); + return model->latches[idx].reset; +} + +static int preplatch (unsigned idx) { return prepilit (aiglatch (idx)); } + +static unsigned aignext (unsigned idx) { + assert (0 <= idx && 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 (0 <= idx && idx < model->num_ands); + return prepilit (model->ands[idx].lhs); +} + +static int prepleft (unsigned idx) { + assert (0 <= idx && idx < model->num_ands); + return prepilit (model->ands[idx].rhs0); +} + +static int prepright (unsigned idx) { + assert (0 <= idx && 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][][]\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 <= 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 <= 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; // true lit + 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 : ""); + 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 : "", 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 + if (cloned & (cloned-1)) res = 0; + else +#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 < 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; +} diff --git a/configure.sh b/configure.sh new file mode 100755 index 0000000..097f446 --- /dev/null +++ b/configure.sh @@ -0,0 +1,281 @@ +#!/bin/sh + +dema=no +check=undefined +chksol=undefined +coverage=undefined +debug=no +log=undefined +lto=no +olevel=none +other=none +druplig=undefined +profile=undefined +static=no +classify=no +aiger=undefined +yalsat=undefined +files=no + +########################################################################## + +die () { + echo "*** configure.sh: $*" 1>&2 + exit 1 +} + +########################################################################## + +while [ $# -gt 0 ] +do + case $1 in + -h|--help) + echo "usage: configure.sh [