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

 [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.