cmake: Add module finder for ABC.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 81e9a0e3061fab4c9a44b3908f043bade27c0447..9a2f8ed8a52618aedf41954f0c8d5ac4b4328a24 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -146,16 +146,18 @@ cvc4_option(ENABLE_TRACING       "Enable tracing")
 cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 cvc4_option(ENABLE_SHARED        "Build as shared library")
+
 # >> 2-valued: ON OFF, for options where we don't need to detect if set by user
-option(ENABLE_COVERAGE           "Enable support for gcov coverage testing" OFF)
-option(ENABLE_PROFILING          "Enable support for gprof profiling" OFF)
+option(ENABLE_COVERAGE           "Enable support for gcov coverage testing")
+option(ENABLE_PROFILING          "Enable support for gprof profiling")
 
 # Optional dependencies
+option(USE_ABC                   "Use ABC for AIG bit-blasting")
 option(USE_CADICAL               "Use CaDiCaL SAT solver")
 option(USE_CLN                   "Use CLN instead of GMP")
 option(USE_CRYPTOMINISAT         "Use CryptoMiniSat SAT solver")
 option(USE_LFSC                  "Use LFSC proof checker")
-option(USE_READLINE              "Use readline for better interactive support" OFF)
+option(USE_READLINE              "Use readline for better interactive support")
 option(USE_SYMFPU                "Use SymFPU for floating point support")
 
 # Supported language bindings
@@ -338,6 +340,13 @@ if(ENABLE_VALGRIND)
   add_definitions(-DCVC4_VALGRIND)
 endif()
 
+if(USE_ABC)
+  find_package(ABC REQUIRED)
+  cvc4_link_library(${ABC_LIBRARIES})
+  include_directories(${ABC_INCLUDE_DIR})
+  add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
+endif()
+
 if(USE_CADICAL)
   find_package(CaDiCaL REQUIRED)
   cvc4_link_library(${CaDiCaL_LIBRARIES})
@@ -576,7 +585,7 @@ endif()
 #message("Multithreaded: ${support_multithreaded}")
 message("Portfolio         : ${ENABLE_PORTFOLIO}")
 message("")
-#message("ABC          : ${{with_abc}")
+message("ABC               : ${USE_ABC}")
 message("CaDiCaL           : ${USE_CADICAL}")
 message("Cryptominisat     : ${USE_CRYPTOMINISAT}")
 #message("GLPK              : ${USE_GLPK}")

diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake
new file mode 100644 (file)
index 0000000..406471c
--- /dev/null
+++ b/cmake/FindABC.cmake
@@ -0,0 +1,29 @@
+# Find ABC
+# ABC_FOUND - system has ABC lib
+# ABC_INCLUDE_DIR - the ABC include directory
+# ABC_LIBRARIES - Libraries needed to use ABC
+# ABC_ARCH_FLAGS - Platform specific compile flags
+
+set(ABC_DEFAULT_HOME "${PROJECT_SOURCE_DIR}/abc/alanmi-abc-53f39c11b58d")
+
+find_path(ABC_INCLUDE_DIR
+          NAMES base/abc/abc.h
+          PATHS ${ABC_DEFAULT_HOME}/src)
+find_library(ABC_LIBRARIES
+             NAMES abc
+             PATHS ${ABC_DEFAULT_HOME})
+find_program(ABC_ARCH_FLAGS_PROG
+             NAMES arch_flags
+             PATHS ${ABC_DEFAULT_HOME})
+
+if(ABC_ARCH_FLAGS_PROG)
+  execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG}
+                  OUTPUT_VARIABLE ABC_ARCH_FLAGS)
+endif()
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(ABC
+  DEFAULT_MSG
+  ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
+
+mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)