From: Alex Ozdemir Date: Fri, 11 Jan 2019 20:48:13 +0000 (-0800) Subject: Fixed linking against drat2er, and use drat2er (#2785) X-Git-Tag: cvc5-1.0.0~4292 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7635ca090c5866b0cc4eeb5beb279032f93bd654;p=cvc5.git Fixed linking against drat2er, and use drat2er (#2785) * Fixed linking against drat2er/drat-trim We have machinery for linking against drat2er. However, this machinery didn't quite work because libdrat2er.a contains an (undefined) reference to `run_drat_trim` from libdrat-trim.a. Thus, when linking against libdrat2er.a, we also need to link against libdrat-trim.a. I made this change, and then tested it by actually calling a function from the drat2er library (CheckAndConvertToLRAT) which relies on `run_drat_trim`. Since this invocation compiles, we know that the linking is working properly now. * Combined the two libs, per Mathias * drat2er configured gaurds --- diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake index e0bc8d446..a7c2538a5 100644 --- a/cmake/FindDrat2Er.cmake +++ b/cmake/FindDrat2Er.cmake @@ -19,13 +19,21 @@ find_library(Drat2Er_LIBRARIES NAMES libdrat2er.a PATHS ${Drat2Er_HOME}/lib NO_DEFAULT_PATH) +find_library(DratTrim_LIBRARIES + NAMES libdrat-trim.a + PATHS ${Drat2Er_HOME}/lib + NO_DEFAULT_PATH) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(Drat2Er DEFAULT_MSG - Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) + Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES DratTrim_LIBRARIES) -mark_as_advanced(Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) +mark_as_advanced(Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES DratTrim_LIBRARIES) if(Drat2Er_LIBRARIES) message(STATUS "Found Drat2Er libs: ${Drat2Er_LIBRARIES}") endif() +if(DratTrim_LIBRARIES) + message(STATUS "Found DratTrim libs: ${DratTrim_LIBRARIES}") + list(APPEND Drat2Er_LIBRARIES ${DratTrim_LIBRARIES}) +endif() diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index ea03a9e20..6c2c5e2e8 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -25,6 +25,11 @@ #include "base/cvc4_assert.h" #include "base/output.h" +#if CVC4_USE_DRAT2ER +#include "drat2er_options.h" +#include "drat_trim_interface.h" +#endif + namespace CVC4 { namespace proof { namespace lrat { @@ -221,9 +226,13 @@ LratProof LratProof::fromDratProof( dratStream << dratBinary; dratStream.close(); - // TODO(aozdemir) Add invocation of DRAT trim, once I get CMake to bundle it - // into CVC4 correctly. - Unimplemented(); +#if CVC4_USE_DRAT2ER + drat2er::drat_trim::CheckAndConvertToLRAT( + formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); +#else + Unimplemented("LRAT proof production requires drat2er.\n" + "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); +#endif std::ifstream lratStream(lratFilename); LratProof lrat(lratStream);