fix bug 33 (statically link the "cvc4" binary); also main driver cleanup

diff --git a/Makefile.builds.in b/Makefile.builds.in
index 650d7be6df1afb3a23a193bb023d0744e7da2772..f26111c4feab55ea92491dc48e58f3419ca05723 100644 (file)
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -57,9 +57,8 @@ ifeq ($(BUILDING_SHARED),1)
        progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
                eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
                eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
-endif
-ifeq ($(BUILDING_STATIC),1)
-#      if we're building static libs, just install them directly
+else
+#      if we're building static libs only, just install the driver binary directly
        $(install_sh) \
                $(CURRENT_BUILD)/src/main/cvc4 \
                "$(abs_builddir)$(bindir)"
@@ -78,9 +77,8 @@ ifeq ($(BUILDING_SHARED),1)
        thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
                eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
                eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
-endif
-ifeq ($(BUILDING_STATIC),1)
-#      if we're building static libs, just install them directly
+else
+#      if we're building static libs only, just install the driver binary directly
        $(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
 endif
 #      set up builds/bin and builds/lib

diff --git a/configure.ac b/configure.ac
index c67da8ba20f2260f8a453fb3529b499ea87e87fd..36f6d6c169d369a1605bd8594c959d8c78caae22 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -407,6 +407,7 @@ if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
 if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
 AC_SUBST(BUILDING_SHARED)
 AC_SUBST(BUILDING_STATIC)
+AM_CONDITIONAL([STATIC_BINARY], [test "$enable_shared" != yes -a "$enable_static" = yes])
 
 AC_SUBST(CVC4_LIBRARY_VERSION)
 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 04d717294b1bacdcb2b2e75de082abd31e2bc916..79eb8c74ea21f825945c3f14a09b5f26e53366e3 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -15,4 +15,8 @@ cvc4_LDADD = \
        ../parser/libcvc4parser.la \
        ../libcvc4.la
 
+if STATIC_BINARY
+cvc4_LINK = $(CXXLINK) -all-static
+else
 cvc4_LINK = $(CXXLINK)
+endif

diff --git a/src/main/main.cpp b/src/main/main.cpp
index e54bbb5f65cca6b582a9219e52360490cbc9f47f..6ebe895a5fff64b9ab52deb114f6e87bf211be69 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -68,16 +68,16 @@ int main(int argc, char *argv[]) {
     SmtEngine smt(&exprMgr, &options);
 
     // If no file supplied we read from standard input
-    bool inputFromStdin = firstArgIndex >= argc;
+    bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 
     // Auto-detect input language by filename extension
     if(!inputFromStdin && options.lang == Parser::LANG_AUTO) {
-      if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4)) {
+      const char* filename = argv[firstArgIndex];
+      unsigned len = strlen(filename);
+      if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         options.lang = Parser::LANG_SMTLIB;
-      } else if(!strcmp(".cvc", argv[firstArgIndex]
-          + strlen(argv[firstArgIndex]) - 4)
-          || !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex])
-              - 5)) {
+      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
         options.lang = Parser::LANG_CVC4;
       }
     }