Imported SAT competition 2020 Version

.gitignore

@@ -0,0 +1,14 @@
+lglbnr.o
+lglcfg.h
+lglcflags.h
+lgldimacs.o
+lglib.o
+lglmain.o
+lglmbt
+lglmbt.o
+lglopts.o
+liblgl.a
+lingeling
+makefile
+plingeling
+plingeling.o

VERSION

@@ -1 +1 @@
-bcj
+bcp

blimc.c

@@ -147,26 +147,26 @@ static int prepilit (unsigned ulit) {
 }
 
 static unsigned aiginput (unsigned idx) {
-  assert (0 <= idx && idx < model->num_inputs);
+  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 (0 <= idx && idx < model->num_latches);
+  assert (idx < model->num_latches);
   return model->latches[idx].lit;
 }
 
 static unsigned aigreset (unsigned idx) {
-  assert (0 <= idx && idx < model->num_latches);
+  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 (0 <= idx && idx < model->num_latches);
+  assert (idx < model->num_latches);
   return model->latches[idx].next;
 }
 
@@ -180,17 +180,17 @@ static unsigned aigbad (unsigned idx) {
 static int prepbad (unsigned idx) { return prepilit (aigbad (idx)); }
 
 static int preplhs (unsigned idx) {
-  assert (0 <= idx && idx < model->num_ands);
+  assert (idx < model->num_ands);
   return prepilit (model->ands[idx].lhs);
 }
 
 static int prepleft (unsigned idx) {
-  assert (0 <= idx && idx < model->num_ands);
+  assert (idx < model->num_ands);
   return prepilit (model->ands[idx].rhs0);
 }
 
 static int prepright (unsigned idx) {
-  assert (0 <= idx && idx < model->num_ands);
+  assert (idx < model->num_ands);
   return prepilit (model->ands[idx].rhs1);
 }
 
@@ -362,7 +362,7 @@ static void extract (void * dummy, int lit) {
 
 static int mapuntimedlit (int lit) {
   int idx = abs (lit), res;
-  assert (1 <= idx && idx <= model->maxvar + 1);
+  assert (1 <= idx && idx <= (int) model->maxvar + 1);
   if (!(res = litmap[idx])) litmap[idx] = res = ++maxvar;
   if (lit < 0) res = -res;
   return res;
@@ -378,7 +378,7 @@ static void mapcnf (void) {
 
 static int mainilit (unsigned ulit) {
   int tmp = prepilit (ulit), idx = abs (tmp), res;
-  assert (1 <= idx && idx <= model->maxvar+1);
+  assert (1 <= idx && idx <= (int) model->maxvar+1);
   res = litmap[idx];
   if (tmp < 0) res = -res;
   return res;
@@ -629,7 +629,7 @@ int main (int argc, char ** argv) {
     if (res == 10) {
       fprintf (outfile, "1\nb0\n");
       if (!nowitness) {
-	for (i = 0; i < model->num_latches; i++) {
+	for (i = 0; i < (int) model->num_latches; i++) {
 	  if (ulitincoi (aiglatch (i))) {
 	    lit = shift (mainilit (aiglatch (i)), 0);
 	    val = lglderef (lgl, lit);

configure.sh

@@ -183,10 +183,10 @@ fi
 
 [ x"$CC" = x ] && CC=gcc
 
-CFLAGS="-Wall"
+CFLAGS="-W -Wall"
 if [ $debug = yes ]
 then
-  CFLAGS="$CFLAGS -g3"
+  CFLAGS="$CFLAGS -ggdb3"
   [ $olevel = none ] || CFLAGS="$CFLAGS $olevel"
 else
   [ $olevel = none ] && olevel=-O3

getgitid

@@ -0,0 +1,2 @@
+#!/bin/sh
+git show|awk '{print $2;exit}'

ilingeling.c

@@ -109,7 +109,7 @@ static signed char * vals;
 static int nlits, szlits;
 static int * lits;
 
-static int verbose, bar, nowitness, plain, clone, deterministic;
+static int verbose, bar, nowitness, plain, doclone, deterministic;
 static int noreverse, addassumptions = 1, noflush, reduce, nomelt;
 
 static const char * druptraceprefix;
@@ -202,7 +202,7 @@ static int term (void * voidptr) {
 
 static void progress (int pmille, int total, int max, double avg, int nl) {
   int ch, i, lim, eta;
-  char fmt[10];
+  char fmt[16];
   double rem;
   msglock (0);
   if (isatty (1)) fputc ('\r', stdout);
@@ -290,13 +290,13 @@ static int sat (Worker * w) {
   int res;
   char name[100];
   LGL * cloned;
-  if (!druptraceprefix && clone) lglsetopt (w->lgl, "clim", CLONELIMIT);
+  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 || !clone || res);
+  assert (!druptraceprefix || !doclone || res);
   if (!res && !justreturn (w)) {
     msg (w, 1, "cloning after %d conflicts", CLONELIMIT);
     cloned = lglclone (w->lgl);
@@ -890,7 +890,7 @@ int main (int argc, char ** argv) {
       if (histfilename) die ("two '-t' options");
       if (++i == argc) die ("argument to '-t' missing");
       histfilename = argv[i];
-    } else if (!strcmp (argv[i], "--clone")) clone = 1;
+    } 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]);

lglddtrace.c

@@ -406,6 +406,7 @@ static void prt (int final) {
     fputc ('\r', stdout);
   }
   msg ("written %s with %d events", oname, prevents);
+  (void) final;
 }
 
 static void dd (void) {
@@ -771,7 +772,7 @@ int main (int argc, char ** argv) {
   if (ch == EOF) goto DONE;
   if (ch == '\r') goto NEXT;
   if (ch != '\n') {
-    if (len + 1 >= sizeof (buffer)) perr ("line buffer exceeded");
+    if (len + 1 >= (int) sizeof (buffer)) perr ("line buffer exceeded");
     buffer[len++] = ch;
     buffer[len] = 0;
     goto NEXT;

lgldimacs.c

@@ -54,6 +54,7 @@ LDR * ldrminit (void * state,
   res->mem.state = state;
   res->mem.alloc = alloc;
   res->mem.dealloc = dealloc;
+  (void) realloc;
   return res;
 }