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 e0bc8d44644b06a6d873a906a287e4de37de21d8..a7c2538a58a02314e43e77fdb99909be22571026 100644 (file)
--- 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 ea03a9e2032d061a1f698366239e0a7e7eec787b..6c2c5e2e8a48c66d14d3475d8d002301b054ba08 100644 (file)
--- 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);