edits

diff --git a/lingeling/build.sh b/lingeling/build.sh
index fa09dd5a5991570a61b6cba81fd7ab43af8c653a..f78a510fcd8836048ea4106b55de0d5e7b16e43a 100755 (executable)
--- a/lingeling/build.sh
+++ b/lingeling/build.sh
@@ -3,5 +3,6 @@ rm -rf binary
 mkdir binary
 cd code
 ./configure.sh || exit 1
-make lingeling || exit 1
+make lingeling incling || exit 1
 install -m 755 -s lingeling ../binary
+install -m 755 -s incling ../binary

diff --git a/lingeling/code/lglincremental.c b/lingeling/code/lglincremental.c
index 6c73a7bebb7ff6148755a4364c773d59effda064..8beb5447c9e3298d1315b7209809766614ebd291 100644 (file)
--- a/lingeling/code/lglincremental.c
+++ b/lingeling/code/lglincremental.c
@@ -33,6 +33,12 @@ static void resetsighandlers (void) {
   (void) signal (SIGBUS, sig_bus_handler);
 }
 
+static inline double cpuTime(void) {
+  struct rusage ru;
+  getrusage(RUSAGE_SELF, &ru);
+  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+}
+
 static void caughtsigmsg (int sig) {
   if (verbose < 0) return;
   printf ("c\nc CAUGHT SIGNAL %d", sig);
@@ -154,6 +160,10 @@ void putInt(int value) {
   outbuffer[outoffset++]=value;
 }
 
+#define bool int
+#define false 0
+#define true 1
+
 void readClauses(LGL *solver) {
   bool haveClause = false;
   while(true) {
@@ -226,9 +236,9 @@ void processSAT(LGL *solver) {
 
 
 int main (int argc, char ** argv) {
-  int res, i, j, val, len, lineno, simponly, count;
-  const char * pname, * match, * p, * err, * thanks;
-  int maxvar, lit, nopts, simplevel;
+  int res, i, j, val, len, lineno, simponly;
+  const char * pname, * match, * p, * thanks;
+  int nopts, simplevel;
   FILE * pfile;
   char * tmp;
   LGL * lgl;

diff --git a/lingeling/code/makefile.in b/lingeling/code/makefile.in
index 611932273d4c507ca5b4964869d771b053d1a29a..5626f86431b10ad7dd4d88b53ca129604e011e0b 100644 (file)
--- a/lingeling/code/makefile.in
+++ b/lingeling/code/makefile.in
@@ -28,7 +28,7 @@ liblgl.a: lglib.o lglbnr.o lgldimacs.o makefile
        ranlib $@
 
 incling: lglincremental.o liblgl.a makefile $(LDEPS)
-       $(CC) $(CFLAGS) -I../.. -o $@ lglincremetal.o -L. -llgl $(LIBS)
+       $(CC) $(CFLAGS) -o $@ lglincremental.o -L. -llgl $(LIBS)
 lingeling: lglmain.o liblgl.a makefile $(LDEPS)
        $(CC) $(CFLAGS) -o $@ lglmain.o -L. -llgl $(LIBS)
 plingeling: plingeling.o liblgl.a makefile $(LDEPS)
@@ -47,7 +47,7 @@ lglddtrace: lglddtrace.o liblgl.a makefile $(LDEPS)
        $(CC) $(CFLAGS) -o $@ lglddtrace.o -L. -llgl $(LIBS)
 
 lglincremental.o: lglincremental.c lglib.h makefile
-       $(CC) $(CFLAGS) -c lglincremental.c
+       $(CC) $(CFLAGS) -I../.. -c lglincremental.c
 lglmain.o: lglmain.c lglib.h makefile
        $(CC) $(CFLAGS) -c lglmain.c
 plingeling.o: plingeling.c lglib.h makefile