diff options
| -rw-r--r-- | INSTALL | 21 | ||||
| -rw-r--r-- | config/glpk.m4 | 6 |
2 files changed, 16 insertions, 11 deletions
@@ -96,7 +96,7 @@ None of these is required, but can improve CVC4 as described below: Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator) Optional: CLN v1.3 or newer (Class Library for Numbers) - Optional: GLPK (GNU Linear Programming Kit) + Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit) Optional: GNU Readline library (for an improved interactive experience) Optional: The Boost C++ threading library (libboost_thread) Optional: CxxTest unit testing framework @@ -114,14 +114,19 @@ CVC4 with CLN support, you are licensing CVC4 under that same license. (Usually CVC4's license is more permissive than GPL is; see the file COPYING in the CVC4 source distribution for details.) Please visit http://www.ginac.de/CLN/ for more details about CLN. - -GLPK is the GNU Linear Programming Kit, and can be used to speed up -the arithmetic implementation in CVC4. GLPK is covered by the GNU -General Public License, version 3; so if you choose to use CVC4 with -GLPK support, you are licensing CVC4 under that same license. +a fork of GLPK (the GNU Linear Programming Kit). +glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit). +This can be used to speed up certain classes of problems for the arithmetic +implementation in CVC4. (This is not recommended for most users.) The source +code for glpk-cut-log is available at: +https://github.com/timothy-king/glpk-cut-log/ +The only option for installation of glpk-cut-log i downloading the library, +compiling and installing it manually. CVC4 is no longer compatible with the +main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public +License, version 3; so if you choose to use CVC4 with GLPK support, you are +licensing CVC4 under that same license. (Usually CVC4's license is more permissive; see above discussion.) -Please visit http://www.gnu.org/software/glpk/ for more details about -GLPK. +Please visit http://www.gnu.org/software/glpk/ for more details about GLPK. The GNU Readline library is optionally used to provide command editing, tab completion, and history functionality at the CVC prompt diff --git a/config/glpk.m4 b/config/glpk.m4 index 932b053e0..ecb91abdd 100644 --- a/config/glpk.m4 +++ b/config/glpk.m4 @@ -35,7 +35,7 @@ elif test "$with_glpk" = yes; then CVC4_TRY_GLPK_WITH([-lgmp -lz -lltdl]) CVC4_TRY_GLPK_WITH([-lgmp -lz -lltdl -ldl]) if test -z "$GLPK_LIBS"; then - AC_MSG_FAILURE([cannot link against libglpk! (or it's too old, or can't get it to work)]) + AC_MSG_FAILURE([cannot link against libglpk! (perhaps you have not switched to glpk-cut-log? see /README)]) else AC_MSG_RESULT([$GLPK_LIBS]) # make sure it works in static builds, too @@ -95,7 +95,7 @@ if test -z "$GLPK_LIBS"; then [#else] [#include <glpk.h>] [#endif], - [int i = glp_get_it_cnt(NULL)])], + [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])], [GLPK_LIBS="-lglpk $1"], []) LIBS="$cvc4_save_LIBS" @@ -118,7 +118,7 @@ if test -z "$GLPK_LIBS"; then [#else] [#include <glpk.h>] [#endif], - [int i = glp_get_it_cnt(NULL)])], + [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])], [GLPK_LIBS="-lglpk $1"], []) LIBS="$cvc4_save_LIBS" |