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

1 files changed, 12 insertions, 3 deletions

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);