BUILD: Use CUDD 3.0.0 !

tulip-control · Jan 24, 2016 · 052a6fb · 052a6fb · johnyf · Jan 24, 2016
1 parent 707924f
commit 052a6fb
Show file tree

Hide file tree

Showing 6 changed files with 52 additions and 55 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -7,7 +7,7 @@ compiler:
 
 install:
   - ./get-deps.sh
-  - make -e cudd
+  - ./build-deps.sh
 script:
   - make -e all
   - make -e check

diff --git a/Makefile b/Makefile
@@ -10,16 +10,13 @@ AUX_PROGRAMS = autman
 prefix = /usr/local
 exec_prefix = $(prefix)
 bindir = $(exec_prefix)/bin
+export deps_prefix = extern
 
 # Possibly change to `cp' when `install' is unavailable
 INSTALL = install
 
 SRCDIR = src
 EXPDIR = exp
-export CUDD_ROOT = extern/cudd-2.5.1
-CUDD_LIB = $(CUDD_ROOT)/cudd/libcudd.a $(CUDD_ROOT)/mtr/libmtr.a $(CUDD_ROOT)/st/libst.a $(CUDD_ROOT)/util/libutil.a $(CUDD_ROOT)/epd/libepd.a
-export CUDD_XCFLAGS = -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
-CUDD_INC = -I$(CUDD_ROOT)/include
 
 LEX = flex -X
 LFLAGS = 
@@ -29,9 +26,9 @@ YFLAGS = -d
 CC = gcc
 LD = ld -r
 
-CFLAGS = -g -Wall -pedantic -ansi
-ALL_CFLAGS = $(CFLAGS) $(CUDD_XCFLAGS) $(CUDD_INC) -Isrc
-LDFLAGS = $(CUDD_LIB) -lm $(CUDD_XCFLAGS)
+CFLAGS = -g -Wall -pedantic -ansi -I$(deps_prefix)/include
+export CFLAGS += -Isrc
+export LDFLAGS = -L$(deps_prefix)/lib -lm -lcudd
 
 # To use and statically link with GNU Readline
 #CFLAGS += -DUSE_READLINE
@@ -62,55 +59,55 @@ grjit: grjit.o sim.o util.o logging.o interactive.o solve_metric.o solve_support
 	$(CC) -o $@ $^ $(LDFLAGS)
 
 autman.o: aux/autman.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 
 grpatch.o: $(EXPDIR)/grpatch.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 grjit.o: $(EXPDIR)/grjit.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 
 main.o: $(SRCDIR)/main.c $(SRCDIR)/common.h
-	$(CC) $(ALL_CFLAGS) -c $<
+	$(CC) $(CFLAGS) -c $<
 rg_main.o: $(SRCDIR)/rg_main.c $(SRCDIR)/common.h
-	$(CC) $(ALL_CFLAGS) -c $<
+	$(CC) $(CFLAGS) -c $<
 sim.o: $(SRCDIR)/sim.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 util.o: $(SRCDIR)/util.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 ptree.o: $(SRCDIR)/ptree.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 logging.o: $(SRCDIR)/logging.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 automaton.o: $(SRCDIR)/automaton.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 automaton_io.o: $(SRCDIR)/automaton_io.c $(SRCDIR)/common.h
-	$(CC) $(ALL_CFLAGS) -c $<
+	$(CC) $(CFLAGS) -c $<
 interactive.o: $(SRCDIR)/interactive.c $(SRCDIR)/common.h
-	$(CC) $(ALL_CFLAGS) -c $<
+	$(CC) $(CFLAGS) -c $<
 solve_metric.o: $(SRCDIR)/solve_metric.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 solve_support.o: $(SRCDIR)/solve_support.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 solve_operators.o: $(SRCDIR)/solve_operators.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 solve.o: $(SRCDIR)/solve.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 patching.o: $(SRCDIR)/patching.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 patching_support.o: $(SRCDIR)/patching_support.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 patching_hotswap.o: $(SRCDIR)/patching_hotswap.c
-	$(CC) $(ALL_CFLAGS) -c $^
+	$(CC) $(CFLAGS) -c $^
 
 gr1c_parse.o: $(SRCDIR)/gr1c_scan.l $(SRCDIR)/gr1c_parse.y
 	$(YACC) $(YFLAGS) $(SRCDIR)/gr1c_parse.y
 	$(LEX) $<
-	$(CC) $(ALL_CFLAGS) -c lex.yy.c y.tab.c
+	$(CC) $(CFLAGS) -c lex.yy.c y.tab.c
 	$(LD) lex.yy.o y.tab.o -o $@
 rg_parse.o: $(SRCDIR)/gr1c_scan.l $(SRCDIR)/rg_parse.y gr1c_parse.o
 	$(YACC) $(YFLAGS) $(SRCDIR)/rg_parse.y
 	$(LEX) $<
-	$(CC) $(ALL_CFLAGS) -c lex.yy.c y.tab.c
+	$(CC) $(CFLAGS) -c lex.yy.c y.tab.c
 	$(LD) lex.yy.o y.tab.o -o $@
 
 install:
@@ -126,10 +123,6 @@ uninstall:
 check: $(CORE_PROGRAMS) $(EXP_PROGRAMS)
 	$(MAKE) -C tests CC=$(CC)
 
-.PHONY: cudd
-cudd:
-	$(MAKE) -C $(CUDD_ROOT) XCFLAGS='$(CUDD_XCFLAGS)' CC=$(CC)
-
 .PHONY: doc
 doc:
 	@(cd doc; doxygen; cd ..)

diff --git a/build-deps.sh b/build-deps.sh
@@ -0,0 +1,10 @@
+#!/bin/sh -e
+#
+# Build dependencies locally under extern/
+
+CUDDVER=3.0.0
+
+cd extern/src/cudd-$CUDDVER
+./configure --prefix=`pwd`/../..
+make
+make install
diff --git a/get-deps.sh b/get-deps.sh
@@ -1,12 +1,12 @@
 #!/bin/sh -e
 #
-# Fetch dependencies, and place them in location that Makefile expects
+# Fetch dependencies, and place them in location that build-deps.sh expects
 
-CUDDVER=2.5.1
-SHA256SUM=4b19c34328d8738a839b994c6b9395f3895ff981d2f3495ce62e7ba576ead88b
+CUDDVER=3.0.0
+SHA256SUM=b8e966b4562c96a03e7fbea239729587d7b395d53cadcc39a7203b49cf7eeb69
 URI=ftp://vlsi.colorado.edu/pub/cudd-$CUDDVER.tar.gz
 
-mkdir -p extern
+mkdir -p extern/src
 curl -sS $URI > extern/cudd-$CUDDVER.tar.gz
 
 if hash sha256sum >/dev/null 2>&1; then
@@ -21,11 +21,10 @@ fi
 
 if [ "$SHA256SUM" = "$FILECHECKSUM" ]
 then
-    cd extern
-    tar -xzf cudd-$CUDDVER.tar.gz
+    cd extern/src
+    tar -xzf ../cudd-$CUDDVER.tar.gz
 else
     echo "Fetched file ($URI) has unexpected SHA checksum."
     false
 fi
-echo "Successfully fetched CUDD; ready to build!"
-
+echo "Successfully fetched CUDD; next run build-deps.sh"
diff --git a/src/common.h b/src/common.h
@@ -28,7 +28,6 @@ typedef char bool;
 typedef unsigned char byte;
 
 
-#include "util.h"
 #include "cudd.h"
 
 #endif
diff --git a/tests/Makefile b/tests/Makefile
@@ -2,13 +2,9 @@
 #
 # SCL; 2012, 2013.
 
+CFLAGS += -I../$(deps_prefix)/include -I../src
+LDFLAGS += -L../$(deps_prefix)/lib
 
-CUDD_LIB = ../$(CUDD_ROOT)/cudd/libcudd.a ../$(CUDD_ROOT)/mtr/libmtr.a ../$(CUDD_ROOT)/st/libst.a ../$(CUDD_ROOT)/util/libutil.a ../$(CUDD_ROOT)/epd/libepd.a
-CUDD_INC = -I../$(CUDD_ROOT)/include
-
-CFLAGS = -g -Wall -pedantic -ansi
-ALL_CFLAGS = $(CFLAGS) $(CUDD_XCFLAGS) $(CUDD_INC) -I../src
-LDFLAGS = $(CUDD_LIB) -lm $(CUDD_XCFLAGS)
 PROGRAMS = test_logging test_automaton test_automaton_io test_ptree test_ptree_to_BDD test_solve_support test_patching
 
 all: $(PROGRAMS)
@@ -27,25 +23,25 @@ all: $(PROGRAMS)
 COMMON_BINS = ../util.o ../automaton.o ../automaton_io.o ../ptree.o ../solve_support.o ../logging.o
 
 test_logging: test_logging.c
-	$(CC) $(ALL_CFLAGS) $^ ../logging.o -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ ../logging.o -o $@ $(LDFLAGS)
 
 test_ptree: test_ptree.c
-	$(CC) $(ALL_CFLAGS) $^ ../ptree.o -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ ../ptree.o -o $@ $(LDFLAGS)
 
 test_ptree_to_BDD: test_ptree_to_BDD.c
-	$(CC) $(ALL_CFLAGS) $^ ../ptree.o -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ ../ptree.o -o $@ $(LDFLAGS)
 
 test_automaton: test_automaton.c
-	$(CC) $(ALL_CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
 
 test_automaton_io: test_automaton_io.c
-	$(CC) $(ALL_CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
 
 test_solve_support: test_solve_support.c
-	$(CC) $(ALL_CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ $(COMMON_BINS) -o $@ $(LDFLAGS)
 
 test_patching: test_patching.c
-	$(CC) $(ALL_CFLAGS) $^ $(COMMON_BINS) ../patching.o ../patching_support.o -o $@ $(LDFLAGS)
+	$(CC) $(CFLAGS) $^ $(COMMON_BINS) ../patching.o ../patching_support.o -o $@ $(LDFLAGS)
 
 clean:
 	-rm -f *~ *.o $(PROGRAMS) temp_*_dump*