From 6660ab05c399d309208251263faeff3be2964f7b Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 17 Dec 2018 15:01:23 -0800 Subject: 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. --- cmake/FindDrat2Er.cmake | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 cmake/FindDrat2Er.cmake (limited to 'cmake') 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() -- cgit v1.2.3