[LRA Proof] Storage for LRA proofs (#2747)

* [LRA Proof] Storage for LRA proofs

During LRA solving the `ConstraintDatabase` contains the reasoning
behind different constraints. Combinations of constraints are
periodically used to justify lemmas (conflict clauses, propegations, ...
?). `ConstraintDatabase` is SAT context-dependent.

ArithProofRecorder will be used to store concise representations of the
proof for each lemma raised by the (LR)A theory. The (LR)A theory will
write to it, and the ArithProof class will read from it to produce LFSC
proofs.

Right now, it's pretty simplistic -- it allows for only Farkas proofs.

In future PRs I'll:
   1. add logic that stores proofs therein
   2. add logic that retrieves and prints proofs
   3. enable LRA proof production, checking, and testing

* Document ArithProofRecorder use-sites

* Update src/proof/arith_proof_recorder.cpp

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Yoni's review

* clang-format

* Response to Mathias' review.

2 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d7113b17d..9902121d0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -36,6 +36,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
     , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
+    , d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
   if (options::nlExt()) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 195cb1883..e4b1c5b26 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -19,6 +19,7 @@
 
 #include "theory/theory.h"
 #include "expr/node.h"
+#include "proof/arith_proof_recorder.h"
 #include "theory/arith/theory_arith_private_forward.h"
 
 
@@ -40,6 +41,11 @@ private:
 
   TimerStat d_ppRewriteTimer;
 
+  /**
+   * @brief Where to store Farkas proofs of lemmas
+   */
+  proof::ArithProofRecorder * d_proofRecorder;
+
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
               Valuation valuation, const LogicInfo& logicInfo);
@@ -90,6 +96,11 @@ public:
       const EntailmentCheckParameters* params,
       EntailmentCheckSideEffects* out) override;
 
+  void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
+  {
+    d_proofRecorder = proofRecorder;
+  }
+
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */