[LRA proof] Recording & Printing LRA Proofs (#2758)

* [LRA proof] Recording & Printing LRA Proofs

Now we use the ArithProofRecorder to record and later print arithmetic
proofs.

If an LRA lemma can be proven by a single farkas proof, then that is
done. Otherwise, we `trust` the lemma.

I haven't **really** enabled LRA proofs yet, so `--check-proofs` still
is a no-op for LRA.

To test, do
```
lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2)
```

where `lfsccvc4` is an alias invoking `lfscc` with all the necessary
signatures. On my machine that is:

```
alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \
/home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf"

```

* Added guards to proof recording

Also reverted some small, unintentional changes.

Also had to add printing for STRING_SUBSTR??

* Responding to Yoni's review

* SimpleFarkasProof examples

* Respond to Aina's comments

* Reorder Constraint declarations

* fix build

* Moved friend declaration in Constraint

* Trichotomy example

* Lift getNumChildren invocation in PLUS case

Credits to aina for spotting it.

* Clang-format

1 files changed, 1 insertions, 0 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6fa7eadeb..e6ff02f10 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -917,6 +917,7 @@ void CvcPrinter::toStream(
     case kind::STRING_LENGTH:
       out << "LENGTH";
       break;
+    case kind::STRING_SUBSTR: out << "SUBSTR"; break;
 
     default:
       Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;