diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-17 15:01:23 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-17 15:01:23 -0800 |
| commit | 6660ab05c399d309208251263faeff3be2964f7b (patch) | |
| tree | ec7ba5d8c9d1ff90611bfce726acb3044be39d6d /cmake | |
| parent | 332357104e9ab1937049f0ea8e53042d8534f966 (diff) | |
Configured for linking against drat2er (#2754)
drat2er is a C/C++ project which includes support for
* Checking DRAT proofs
* Converting DRAT proofs to LRAT proofs
* Converting DRAT proofs to ER proofs
It does the first 2 by using drat-trim under the hood.
I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/FindDrat2Er.cmake | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake new file mode 100644 index 000000000..e0bc8d446 --- /dev/null +++ b/cmake/FindDrat2Er.cmake @@ -0,0 +1,31 @@ +# Find drat2er +# Drat2Er_FOUND - system has Drat2Er lib +# Drat2Er_INCLUDE_DIR - the Drat2Er include directory +# Drat2Er_LIBRARIES - Libraries needed to use Drat2Er + + +# Check default location of Drat2Er built with contrib/get-drat2er. +# If the user provides a directory we will not search the default paths and +# fail if Drat2Er was not found in the specified directory. +if(NOT Drat2Er_HOME) + set(Drat2Er_HOME ${PROJECT_SOURCE_DIR}/drat2er/build/install) +endif() + +find_path(Drat2Er_INCLUDE_DIR + NAMES drat2er.h + PATHS ${Drat2Er_HOME}/include + NO_DEFAULT_PATH) +find_library(Drat2Er_LIBRARIES + NAMES libdrat2er.a + PATHS ${Drat2Er_HOME}/lib + NO_DEFAULT_PATH) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Drat2Er + DEFAULT_MSG + Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) + +mark_as_advanced(Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) +if(Drat2Er_LIBRARIES) + message(STATUS "Found Drat2Er libs: ${Drat2Er_LIBRARIES}") +endif() |