edits
authorbdemsky <bdemsky@uci.edu>
Wed, 31 Dec 2014 14:14:13 +0000 (23:14 +0900)
committerbdemsky <bdemsky@uci.edu>
Wed, 31 Dec 2014 14:14:13 +0000 (23:14 +0900)
lingeling/build.sh
lingeling/code/lglincremental.c
lingeling/code/makefile.in

index fa09dd5..f78a510 100755 (executable)
@@ -3,5 +3,6 @@ rm -rf binary
 mkdir binary
 cd code
 ./configure.sh || exit 1
 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 lingeling ../binary
+install -m 755 -s incling ../binary
index 6c73a7b..8beb544 100644 (file)
@@ -33,6 +33,12 @@ static void resetsighandlers (void) {
   (void) signal (SIGBUS, sig_bus_handler);
 }
 
   (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);
 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;
 }
 
   outbuffer[outoffset++]=value;
 }
 
+#define bool int
+#define false 0
+#define true 1
+
 void readClauses(LGL *solver) {
   bool haveClause = false;
   while(true) {
 void readClauses(LGL *solver) {
   bool haveClause = false;
   while(true) {
@@ -226,9 +236,9 @@ void processSAT(LGL *solver) {
 
 
 int main (int argc, char ** argv) {
 
 
 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;
   FILE * pfile;
   char * tmp;
   LGL * lgl;
index 6119322..5626f86 100644 (file)
@@ -28,7 +28,7 @@ liblgl.a: lglib.o lglbnr.o lgldimacs.o makefile
        ranlib $@
 
 incling: lglincremental.o liblgl.a makefile $(LDEPS)
        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)
 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) -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
 lglmain.o: lglmain.c lglib.h makefile
        $(CC) $(CFLAGS) -c lglmain.c
 plingeling.o: plingeling.c lglib.h makefile