Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS

3 files changed, 24 insertions, 15 deletions

diff --git a/src/main/options b/src/main/options
index ba36e43ab..faac6b8f1 100644
--- a/src/main/options
+++ b/src/main/options
@@ -7,6 +7,7 @@ module DRIVER "main/options.h" Driver
 
 common-option version -V --version/ bool
  identify this CVC4 binary
+alias --license = --version
 
 common-option help -h --help/ bool
  full command line reference
diff --git a/src/util/configuration.h b/src/util/configuration.h
index be49e3dcf..696b67715 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -83,12 +83,16 @@ public:
 
   static std::string about();
 
+  static bool licenseIsGpl();
+
   static bool isBuiltWithGmp();
 
   static bool isBuiltWithCln();
 
   static bool isBuiltWithGlpk();
 
+  static bool isBuiltWithReadline();
+
   static bool isBuiltWithCudd();
 
   static bool isBuiltWithTlsSupport();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e33c5fa36..5d078b5ef 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -107,6 +107,18 @@ namespace CVC4 {
 #  define IS_GLPK_BUILD false
 #endif /* CVC4_USE_GLPK */
 
+#ifdef HAVE_LIBREADLINE
+#  define IS_READLINE_BUILD true
+#else /* HAVE_LIBREADLINE */
+#  define IS_READLINE_BUILD false
+#endif /* HAVE_LIBREADLINE */
+
+#if CVC4_GPL_DEPS
+#  define IS_GPL_BUILD true
+#else /* CVC4_GPL_DEPS */
+#  define IS_GPL_BUILD false
+#endif /* CVC4_GPL_DEPS */
+
 #ifdef TLS
 #  define USING_TLS true
 #else /* TLS */
@@ -126,24 +138,16 @@ compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
   New York University and The University of Iowa\n\n" + \
-    ( IS_CLN_BUILD ? "\
-This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without CLN if you want to license CVC4 under the (modified) BSD license.\n\n\
-" : ( IS_GLPK_BUILD ? "\
-This CVC4 library uses GLPK in its arithmetic solver.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, GLPK, the GNU Linear Programming Kit, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+GLPK, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without GLPK if you want to license CVC4 under the (modified) BSD license.\n\n\
+    ( IS_GPL_BUILD ? "\
+This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\
+General Public License (GPL) version 3.  Versions of CVC4 are available\n\
+that are covered by the (modified) BSD license.  If you want to license\n\
+CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\
+before building from sources.\n\
 " : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\n\
-" ) ) + "\
+" ) + "\
 THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\
 See the file COPYING (distributed with the source code, and with all binaries)\n\
 for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" )