cmake: Add more documentation, some fixes and cleanup.

7 files changed, 72 insertions, 55 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 54bbc6e12..36d88c12f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,9 +1,5 @@
 cmake_minimum_required(VERSION 3.1)
 
-if(POLICY CMP0075)
-  cmake_policy(SET CMP0075 NEW)
-endif()
-
 #-----------------------------------------------------------------------------#
 # Project configuration
 
@@ -43,7 +39,7 @@ option(ENABLE_GPL "Enable GPL dependencies")
 
 # General build options
 #
-# >> 3-valued: INGORE ON OFF
+# >> 3-valued: IGNORE ON OFF
 #    > allows to detect if set by user (default: IGNORE)
 #    > only necessary for options set for build types
 cvc4_option(ENABLE_ASAN          "Enable ASAN build")
@@ -69,7 +65,7 @@ option(ENABLE_PROFILING        "Enable support for gprof profiling")
 
 # Optional dependencies
 #
-# >> 3-valued: INGORE ON OFF
+# >> 3-valued: IGNORE ON OFF
 #    > allows to detect if set by user (default: IGNORE)
 #    > only necessary for options set for ENABLE_BEST
 cvc4_option(USE_ABC      "Use ABC for AIG bit-blasting")
@@ -160,7 +156,9 @@ cvc4_set_option(ENABLE_SHARED ON)
 
 if(ENABLE_BEST)
   cvc4_set_option(USE_ABC ON)
+  cvc4_set_option(USE_CADICAL ON)
   cvc4_set_option(USE_CLN ON)
+  cvc4_set_option(USE_CRYPTOMINISAT ON)
   cvc4_set_option(USE_GLPK ON)
   cvc4_set_option(USE_READLINE ON)
 endif()
@@ -199,9 +197,11 @@ libcvc4_link_libraries(${GMP_LIBRARIES})
 libcvc4_include_directories(${GMP_INCLUDE_DIR})
 
 if(ENABLE_ASAN)
-  set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
+  # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
+  # otherwise the -fsanitize=address check will fail while linking.
+  set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
   add_required_c_cxx_flag("-fsanitize=address")
-  unset(CMAKE_REQUIRED_LIBRARIES)
+  unset(CMAKE_REQUIRED_FLAGS)
   add_required_c_cxx_flag("-fno-omit-frame-pointer")
   add_check_c_cxx_flag("-fsanitize-recover=address")
 endif()
@@ -282,7 +282,7 @@ if(ENABLE_TRACING)
 endif()
 
 if(ENABLE_UNIT_TESTING)
-	find_package(CxxTest REQUIRED)
+  find_package(CxxTest REQUIRED)
   # Force shared libs for unit tests, static libs with unit tests are not
   # working right now.
   set(ENABLE_SHARED ON)
@@ -363,6 +363,7 @@ if(USE_LFSC)
 endif()
 
 if(USE_READLINE)
+  set(GPL_LIBS "${GPL_LIBS} readline")
   find_package(Readline REQUIRED)
   set(HAVE_LIBREADLINE 1)
   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
@@ -517,7 +518,7 @@ if(GPL_LIBS)
   "\n"
   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
   "\n"
-  "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
+  "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
   )
 else()
   message(
diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake
index 2448f73cb..16dd72236 100644
--- a/cmake/FindReadline.cmake
+++ b/cmake/FindReadline.cmake
@@ -2,6 +2,8 @@
 # Readline_FOUND - system has Readline lib
 # Readline_INCLUDE_DIR - the Readline include directory
 # Readline_LIBRARIES - Libraries needed to use Readline
+# Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function
+#                                           returns a (char *)
 
 find_path(Readline_INCLUDE_DIR NAMES readline/readline.h)
 find_library(Readline_LIBRARIES NAMES readline)
@@ -19,6 +21,8 @@ if(Readline_INCLUDE_DIR)
      int main() { rl_completion_entry_function = foo; return 0; }"
      Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
   )
+  unset(CMAKE_REQUIRED_QUIET)
+  unset(CMAKE_REQUIRED_LIBRARIES)
 endif()
 
 include(FindPackageHandleStandardArgs)
diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake
index 86008e0d2..ec7216452 100644
--- a/cmake/Helpers.cmake
+++ b/cmake/Helpers.cmake
@@ -1,6 +1,7 @@
 include(CheckCCompilerFlag)
 include(CheckCXXCompilerFlag)
 
+# Add a C flag to the global list of C flags.
 macro(add_c_flag flag)
   if(CMAKE_C_FLAGS)
     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
@@ -10,6 +11,7 @@ macro(add_c_flag flag)
   message(STATUS "Configuring with C flag '${flag}'")
 endmacro()
 
+# Add a CXX flag to the global list of CXX flags.
 macro(add_cxx_flag flag)
   if(CMAKE_CXX_FLAGS)
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
@@ -19,11 +21,13 @@ macro(add_cxx_flag flag)
   message(STATUS "Configuring with CXX flag '${flag}'")
 endmacro()
 
+# Add a C and CXX flag to the global list of C/CXX flags.
 macro(add_c_cxx_flag flag)
   add_c_flag(${flag})
   add_cxx_flag(${flag})
 endmacro()
 
+# Check if C flag is supported and add to global list of C flags.
 macro(add_check_c_flag flag)
   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
@@ -32,6 +36,7 @@ macro(add_check_c_flag flag)
   endif()
 endmacro()
 
+# Check if CXX flag is supported and add to global list of CXX flags.
 macro(add_check_cxx_flag flag)
   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
@@ -40,11 +45,14 @@ macro(add_check_cxx_flag flag)
   endif()
 endmacro()
 
+# Check if C/CXX flag is supported and add to global list of C/CXX flags.
 macro(add_check_c_cxx_flag flag)
   add_check_c_flag(${flag})
   add_check_cxx_flag(${flag})
 endmacro()
 
+# Add required CXX flag. Configuration fails if the CXX flag is not supported
+# by the compiler.
 macro(add_required_cxx_flag flag)
   string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
@@ -54,6 +62,8 @@ macro(add_required_cxx_flag flag)
   add_cxx_flag(${flag})
 endmacro()
 
+# Add required C flag. Configuration fails if the C flag is not supported by
+# the compiler.
 macro(add_required_c_flag flag)
   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
@@ -63,6 +73,8 @@ macro(add_required_c_flag flag)
   add_c_flag(${flag})
 endmacro()
 
+# Add requied C/CXX flag. Configuration fails if the C/CXX flag is not
+# supported by the compiler.
 macro(add_required_c_cxx_flag flag)
   add_required_c_flag(${flag})
   add_required_cxx_flag(${flag})
diff --git a/configure.sh b/configure.sh
index e5bf0de4a..f3ba57c82 100755
--- a/configure.sh
+++ b/configure.sh
@@ -16,8 +16,8 @@ General options;
   -h, --help               display this help and exit
   --prefix=STR             install directory
   --name=STR               use custom build directory name (optionally: +path)
-  --best                   turn on dependences known to give best performance
-  --gpl                    permit GPL dependences, if available
+  --best                   turn on dependencies known to give best performance
+  --gpl                    permit GPL dependencies, if available
   --win64                  cross-compile for Windows 64 bit
 
 
@@ -29,11 +29,11 @@ The following flags enable optional features (disable with --no-<option name>).
   --debug-symbols          include debug symbols
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
-  --statistics             do not include statistics
-  --replay                 turn off the replay feature
-  --assertions             turn off assertions
-  --tracing                remove all tracing code
-  --dumping                remove all dumping code
+  --statistics             include statistics
+  --replay                 turn on the replay feature
+  --assertions             turn on assertions
+  --tracing                include tracing code
+  --dumping                include dumping code
   --muzzle                 complete silence (no non-result output)
   --coverage               support for gcov coverage testing
   --profiling              support for gprof profiling
@@ -52,23 +52,23 @@ The following flags enable optional packages (disable with --no-<option name>).
   --glpk                   use GLPK simplex solver
   --abc                    use the ABC AIG library
   --cadical                use the CaDiCaL SAT solver
-  --cryptominisat          use the CRYPTOMINISAT sat solver
+  --cryptominisat          use the CryptoMiniSat sat solver
   --lfsc                   use the LFSC proof checker
-  --symfpu                 use symfpu for floating point solver
+  --symfpu                 use SymFPU for floating point solver
   --portfolio              build the multithreaded portfolio version of CVC4
                            (pcvc4)
   --readline               support the readline library
 
 Optional Path to Optional Packages:
-  --abc-dir=PATH           path to top level of abc source tree
+  --abc-dir=PATH           path to top level of ABC source tree
   --antlr-dir=PATH         path to ANTLR C headers and libraries
   --cadical-dir=PATH       path to top level of CaDiCaL source tree
-  --cryptominisat-dir=PATH path to top level of cryptominisat source tree
+  --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
   --cxxtest-dir=DIR        path to CxxTest installation
-  --glpk-dir=PATH          path to top level of glpk installation
+  --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
-  --lfsc-dir=PATH          path to top level of lfsc source tree
-  --symfpu-dir=PATH        path to top level of symfpu source tree
+  --lfsc-dir=PATH          path to top level of LFSC source tree
+  --symfpu-dir=PATH        path to top level of SymFPU source tree
 
 Report bugs to <cvc4-bugs@cs.stanford.edu>.
 EOF
diff --git a/cvc4autoconfig.new.h.in b/cvc4autoconfig.new.h.in
index 8fafd62e3..ce8aeb5da 100644
--- a/cvc4autoconfig.new.h.in
+++ b/cvc4autoconfig.new.h.in
@@ -19,7 +19,7 @@
 /* Full name of this package. */
 #define PACKAGE_NAME "@PACKAGE_NAME@"
 
-/* Define to 1 if CVC4 is built with (optional) GPLed library dependences. */
+/* Define to 1 if CVC4 is built with (optional) GPLed library dependencies. */
 #cmakedefine01 CVC4_GPL_DEPS
 
 /* Define to use the CLN multi-precision arithmetic library. */
@@ -31,7 +31,7 @@
 /* Define to 1 if Boost threading library has support for thread attributes. */
 #cmakedefine01 BOOST_HAS_THREAD_ATTR
 
-/* Define to 1 if `clock_gettime' is supported by the platform. */
+/* Define if `clock_gettime' is supported by the platform. */
 #cmakedefine HAVE_CLOCK_GETTIME
 
 /* Define to 1 if the declaration of `optreset' is available. */
@@ -40,19 +40,19 @@
 /* Define to 1 if the <ext/stdio_filebuf.h> header file is available. */
 #cmakedefine01 HAVE_EXT_STDIO_FILEBUF_H
 
-/* Define to 1 if `ffs' is supported by the platform. */
+/* Define if `ffs' is supported by the platform. */
 #cmakedefine HAVE_FFS
 
 /* Define to 1 to use libreadline. */
 #cmakedefine01 HAVE_LIBREADLINE
 
-/* Define to 1 if `sigaltstack' is supported by the platform. */
+/* Define if `sigaltstack' is supported by the platform. */
 #cmakedefine HAVE_SIGALTSTACK
 
 /* Define to 1 if `strerror_r' is supported by the platform. */
 #cmakedefine01 HAVE_STRERROR_R
 
-/* Define to 1 if `strtok_r' is supported by the platform. */
+/* Define if `strtok_r' is supported by the platform. */
 #cmakedefine HAVE_STRTOK_R
 
 /* Define to 1 if the <unistd.h> header file is available. */
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index a37cb9276..33d341ac8 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -30,8 +30,8 @@ add_custom_target(runexamples
 #           - a list variable: set(<list name> <libs1> <libs2> ...) and pass
 #                              as "${<list name>}"
 #           - a string: pass as "lib1 lib2 ..." (alternative: "lib1;lib2;...")
-# > ouput_dir: Determines the examples subdirectory and is empty (passed as
-#              empty string) for the examples root director (this)
+# > output_dir: Determines the examples subdirectory and is empty (passed as
+#               empty string) for the examples root directory (this)
 # > ARGN: Any additional arguments passed to the macro are interpreted as
 #         as arguments to the test executable.
 macro(cvc4_add_example name src_files libs output_dir)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4ba64c11a..3e32ab7bf 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -788,29 +788,29 @@ install(FILES
         DESTINATION
           include/theory)
 install(FILES
-        util/abstract_value.h
-        util/bitvector.h
-        util/bool.h
-        util/cardinality.h
-        util/channel.h
-        util/divisible.h
-        util/gmp_util.h
-        util/hash.h
-        util/integer_cln_imp.h
-        util/integer_gmp_imp.h
-        util/maybe.h
-        util/proof.h
-        util/rational_cln_imp.h
-        util/rational_gmp_imp.h
-        util/regexp.h
-        util/resource_manager.h
-        util/result.h
-        util/sexpr.h
-        util/statistics.h
-        util/tuple.h
-        util/unsafe_interrupt_exception.h
-        ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
-        ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
-        ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
+          util/abstract_value.h
+          util/bitvector.h
+          util/bool.h
+          util/cardinality.h
+          util/channel.h
+          util/divisible.h
+          util/gmp_util.h
+          util/hash.h
+          util/integer_cln_imp.h
+          util/integer_gmp_imp.h
+          util/maybe.h
+          util/proof.h
+          util/rational_cln_imp.h
+          util/rational_gmp_imp.h
+          util/regexp.h
+          util/resource_manager.h
+          util/result.h
+          util/sexpr.h
+          util/statistics.h
+          util/tuple.h
+          util/unsafe_interrupt_exception.h
+          ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
+          ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
+          ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
         DESTINATION
           include/util)