diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-11 12:48:13 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-11 12:48:13 -0800 |
| commit | 7635ca090c5866b0cc4eeb5beb279032f93bd654 (patch) | |
| tree | 9ab0ac62ea78965c235c3be13b6ddeb507c806df | |
| parent | 87f38648fe82b69b527a387bec9836455290cdba (diff) | |
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
| -rw-r--r-- | cmake/FindDrat2Er.cmake | 12 | ||||
| -rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 15 |
2 files changed, 22 insertions, 5 deletions
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); |