[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, 71 insertions, 1 deletions

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a58294998..640d2db8d 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -64,7 +64,7 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
 
   /**
-   * @brief Where farkas proofs of lemmas are stored.
+   * Where farkas proofs of lemmas are stored.
    */
   proof::ArithProofRecorder d_recorder;
 
@@ -86,6 +86,76 @@ public:
                       std::ostream& os,
                       const ProofLetMap& map) override;
   void printOwnedSort(Type type, std::ostream& os) override;
+
+  /**
+   * Print a rational number in LFSC format.
+   *        e.g. 5/8 or (~ 1/1)
+   *
+   * @param o ostream to print to.
+   * @param r the rational to print
+   */
+  static void printRational(std::ostream& o, const Rational& r);
+
+  /**
+   * Print a value of type poly_formula_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be of the form [linear polynomial >= constant])
+   */
+  static void printLinearPolynomialPredicateNormalizer(std::ostream& o,
+                                                       const Node& n);
+
+  /**
+   * Print a value of type poly_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a linear polynomial)
+   */
+  static void printLinearPolynomialNormalizer(std::ostream& o, const Node& n);
+
+  /**
+   * Print a value of type poly_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a linear monomial)
+   */
+  static void printLinearMonomialNormalizer(std::ostream& o, const Node& n);
+
+  /**
+   * Print a LFSC rational
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a const rational)
+   */
+  static void printConstRational(std::ostream& o, const Node& n);
+
+  /**
+   * print the pn_var normalizer for n (type poly_norm)
+   *
+   * @param o the ostream to print to
+   * @param n the node to print (asserted to be a variable)
+   */
+  static void printVariableNormalizer(std::ostream& o, const Node& n);
+  /**
+   * print a proof of the lemma
+   *
+   * First, we print linearity witnesses, i.e. witnesses  that each literal has
+   * the form:
+   *   [linear polynomial] >= 0 OR
+   *   [linear polynomial] >  0
+   *
+   * Then we use those witnesses to prove that the above linearized constraints
+   * hold.
+   *
+   * Then we use the farkas coefficients to combine the literals into a
+   * variable-free contradiction. The literals may be a mix of strict and
+   * relaxed inequalities.
+   *
+   * @param lemma the set of literals disjoined in the lemma
+   * @param os stream to print the proof to
+   * @param paren global closing stream (unused)
+   * @param map let map (unused)
+   */
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
                              std::ostream& os,
                              std::ostream& paren,