[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

3 files changed, 532 insertions, 131 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 1d51f99e1..0d2bb5be0 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -19,10 +19,14 @@
 #include <memory>
 #include <stack>
 
+#include "expr/node.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
+#include "theory/arith/constraint_forward.h"
 #include "theory/arith/theory_arith.h"
 
+#define CVC4_ARITH_VAR_TERM_PREFIX "term."
+
 namespace CVC4 {
 
 inline static Node eqNode(TNode n1, TNode n2) {
@@ -674,151 +678,169 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
   // !d_realMode <--> term.getType().isInteger()
 
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
-  switch (term.getKind()) {
+  switch (term.getKind())
+  {
+    case kind::CONST_RATIONAL:
+    {
+      Assert(term.getNumChildren() == 0);
+      Assert(term.getType().isInteger() || term.getType().isReal());
 
-  case kind::CONST_RATIONAL: {
-    Assert (term.getNumChildren() == 0);
-    Assert (term.getType().isInteger() || term.getType().isReal());
+      const Rational& r = term.getConst<Rational>();
+      bool neg = (r < 0);
 
-    const Rational& r = term.getConst<Rational>();
-    bool neg = (r < 0);
+      os << (!d_realMode ? "(a_int " : "(a_real ");
 
-    os << (!d_realMode ? "(a_int " : "(a_real ");
+      if (neg)
+      {
+        os << "(~ ";
+      }
 
-    if (neg) {
-      os << "(~ ";
-    }
+      if (!d_realMode)
+      {
+        os << r.abs();
+      }
+      else
+      {
+        printRational(os, r.abs());
+      }
 
-    if (!d_realMode) {
-      os << r.abs();
-    } else {
-      os << r.abs().getNumerator();
-      os << "/";
-      os << r.getDenominator();
+      if (neg)
+      {
+        os << ") ";
+      }
+
+      os << ") ";
+      return;
     }
 
-    if (neg) {
+    case kind::UMINUS:
+    {
+      Assert(term.getNumChildren() == 1);
+      Assert(term.getType().isInteger() || term.getType().isReal());
+      os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
       os << ") ";
+      return;
     }
 
-    os << ") ";
-    return;
-  }
+    case kind::PLUS:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::UMINUS: {
-    Assert (term.getNumChildren() == 1);
-    Assert (term.getType().isInteger() || term.getType().isReal());
-    os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << ") ";
-    return;
-  }
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(+_Int " : "(+_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-  case kind::PLUS: {
-    Assert (term.getNumChildren() >= 2);
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
+    }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(+_Int " : "(+_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+    case kind::MINUS:
+    {
+      Assert(term.getNumChildren() >= 2);
+
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(-_Int " : "(-_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
+
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::MULT:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::MINUS: {
-    Assert (term.getNumChildren() >= 2);
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(*_Int " : "(*_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(-_Int " : "(-_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::DIVISION:
+    case kind::DIVISION_TOTAL:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::MULT: {
-    Assert (term.getNumChildren() >= 2);
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(/_Int " : "(/_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(*_Int " : "(*_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::GT:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(>_Int " : "(>_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-  case kind::DIVISION:
-  case kind::DIVISION_TOTAL: {
-    Assert (term.getNumChildren() >= 2);
+    case kind::GEQ:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(/_Int " : "(/_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
+    case kind::LT:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(<_Int " : "(<_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
       os << " ";
-      paren << ") ";
-    }
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::LEQ:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-  case kind::GT:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(>_Int " : "(>_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::GEQ:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::LT:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(<_Int " : "(<_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::LEQ:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
+    case kind::VARIABLE:
+    case kind::SKOLEM:
+      os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term);
+      return;
 
-  default:
-    Debug("pf::arith") << "Default printing of term: " << term << std::endl;
-    os << term;
-    return;
+    default:
+      Debug("pf::arith") << "Default printing of term: " << term << std::endl;
+      os << term;
+      return;
   }
 }
 
@@ -833,26 +855,327 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
   }
 }
 
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
-  os << " ;; Arith Theory Lemma \n;;";
-  for (unsigned i = 0; i < lemma.size(); ++i) {
-    os << lemma[i] <<" ";
+void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
+{
+  if (r.sgn() < 0)
+  {
+    o << "(~ " << r.getNumerator().abs() << "/" << r.getDenominator().abs()
+      << ")";
+  }
+  else
+  {
+    o << r.getNumerator() << "/" << r.getDenominator();
+  }
+}
+
+void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
+                                                     const Node& n)
+{
+  switch (n.getKind())
+  {
+    case kind::PLUS:
+    {
+      // Since our axioms are binary, but n may be n-ary, we rig up
+      // a right-associative tree.
+      size_t nchildren = n.getNumChildren();
+      for (size_t i = 0; i < nchildren; ++i)
+      {
+        if (i < nchildren - 1)
+        {
+          o << "\n      (pn_+ _ _ _ _ _ ";
+        }
+        printLinearMonomialNormalizer(o, n[i]);
+      }
+      std::fill_n(std::ostream_iterator<char>(o), nchildren - 1, ')');
+      break;
+    }
+    case kind::MULT:
+    case kind::VARIABLE:
+    case kind::CONST_RATIONAL:
+    case kind::SKOLEM:
+    {
+      printLinearMonomialNormalizer(o, n);
+      break;
+    }
+    default:
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream msg;
+      msg << "Invalid operation " << n.getKind() << " in linear polynomial";
+      Unreachable(msg.str().c_str());
+#endif  // CVC4_ASSERTIONS
+      break;
+  }
+}
+
+void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
+                                                   const Node& n)
+{
+  switch (n.getKind())
+  {
+    case kind::MULT: {
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream s;
+      s << "node " << n << " is not a linear monomial";
+      s << " " << n[0].getKind() << " " << n[1].getKind();
+      Assert((n[0].getKind() == kind::CONST_RATIONAL
+              && (n[1].getKind() == kind::VARIABLE
+                  || n[1].getKind() == kind::SKOLEM)),
+             s.str().c_str());
+#endif  // CVC4_ASSERTIONS
+
+      o << "\n        (pn_mul_c_L _ _ _ ";
+      printConstRational(o, n[0]);
+      o << " ";
+      printVariableNormalizer(o, n[1]);
+      o << ")";
+      break;
+    }
+    case kind::CONST_RATIONAL:
+    {
+      o << "\n        (pn_const ";
+      printConstRational(o, n);
+      o << ")";
+      break;
+    }
+    case kind::VARIABLE:
+    case kind::SKOLEM:
+    {
+      o << "\n        ";
+      printVariableNormalizer(o, n);
+      break;
+    }
+    default:
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream msg;
+      msg << "Invalid operation " << n.getKind() << " in linear monomial";
+      Unreachable(msg.str().c_str());
+#endif  // CVC4_ASSERTIONS
+      break;
+  }
+}
+
+void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
+{
+  Assert(n.getKind() == kind::CONST_RATIONAL);
+  const Rational value = n.getConst<Rational>();
+  printRational(o, value);
+}
+
+void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
+{
+  std::ostringstream msg;
+  msg << "Invalid variable kind " << n.getKind() << " in linear monomial";
+  Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM,
+         msg.str().c_str());
+  o << "(pn_var " << n << ")";
+}
+
+void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
+                                                              const Node& n)
+{
+  Assert(n.getKind() == kind::GEQ,
+         "can only print normalization witnesses for (>=) nodes");
+  Assert(n[1].getKind() == kind::CONST_RATIONAL);
+  o << "(poly_formula_norm_>= _ _ _ ";
+  o << "\n    (pn_- _ _ _ _ _ ";
+  printLinearPolynomialNormalizer(o, n[0]);
+  o << "\n      (pn_const ";
+  printConstRational(o, n[1]);
+  o << ")))";
+}
+
+void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                           std::ostream& os,
+                                           std::ostream& paren,
+                                           const ProofLetMap& map)
+{
+  Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl;
+  // Prefixes for the names of linearity witnesses
+  const char* linearityWitnessPrefix = "lp";
+  const char* linearizedProofPrefix = "pf_lp";
+  std::ostringstream lemmaParen;
+
+  // Construct the set of conflicting literals
+  std::set<Node> conflictSet;
+  std::transform(lemma.begin(),
+                 lemma.end(),
+                 std::inserter(conflictSet, conflictSet.begin()),
+                 [](const Expr& e) {
+                   return NodeManager::currentNM()->fromExpr(e).negate();
+                 });
+
+  // If we have Farkas coefficients stored for this lemma, use them to write a
+  // proof. Otherwise, just `trust` the lemma.
+  if (d_recorder.hasFarkasCoefficients(conflictSet))
+  {
+    // Get farkas coefficients & literal order
+    const auto& farkasInfo = d_recorder.getFarkasCoefficients(conflictSet);
+    const Node& conflict = farkasInfo.first;
+    theory::arith::RationalVectorCP farkasCoefficients = farkasInfo.second;
+    Assert(farkasCoefficients != theory::arith::RationalVectorCPSentinel);
+    Assert(conflict.getNumChildren() == farkasCoefficients->size());
+    const size_t nAntecedents = conflict.getNumChildren();
+
+    // Print proof
+    os << "\n;; Farkas Proof" << std::endl;
+
+    // Construct witness that the literals are linear polynomials
+    os << ";  Linear Polynomial Normalization Witnesses" << std::endl;
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& antecedent = conflict[i];
+      const Rational farkasC = (*farkasCoefficients)[i];
+      os << "\n; " << antecedent << " w/ farkas c = " << farkasC << std::endl;
+      os << "  (@ "
+         << ProofManager::getLitName(antecedent.negate(),
+                                     linearityWitnessPrefix)
+         << " ";
+      const Node& nonneg =
+          antecedent.getKind() == kind::NOT ? antecedent[0] : antecedent;
+      printLinearPolynomialPredicateNormalizer(os, nonneg);
+      lemmaParen << ")";
+    }
+
+    // Prove linear polynomial constraints
+    os << "\n;  Linear Polynomial Proof Conversions";
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& antecedent = conflict[i];
+      os << "\n  (@ "
+         << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix)
+         << " ";
+      lemmaParen << ")";
+      switch (conflict[i].getKind())
+      {
+        case kind::NOT:
+        {
+          Assert(conflict[i][0].getKind() == kind::GEQ);
+          os << "(poly_flip_not_>= _ _ "
+             << "(poly_form_not _ _ "
+             << ProofManager::getLitName(antecedent.negate(),
+                                         linearityWitnessPrefix)
+             << " " << ProofManager::getLitName(antecedent.negate(), "")
+             << "))";
+          break;
+        }
+        case kind::GEQ:
+        {
+          os << "(poly_form _ _ "
+             << ProofManager::getLitName(antecedent.negate(),
+                                         linearityWitnessPrefix)
+             << " " << ProofManager::getLitName(antecedent.negate(), "") << ")";
+          break;
+        }
+        default: Unreachable();
+      }
+    }
+
+    /* Combine linear polynomial constraints to derive a contradiction.
+     *
+     * The linear polynomial constraints are refered to as **antecedents**,
+     * since they are antecedents to the contradiction.
+     *
+     * The structure of the combination is a tree
+     *
+     *   (=> <=)
+     *      |
+     *      +                   0
+     *     / \
+     *    *   +                 1
+     *       / \
+     *      *   +               2
+     *         / \
+     *        *  ...            i
+     *             \
+     *              +           n-1
+     *             / \
+     *            *   (0 >= 0)
+     *
+     * Where each * is a linearized antecedant being scaled by a farkas
+     * coefficient and each + is the sum of inequalities. The tricky bit is that
+     * each antecedent can be strict (>) or relaxed (>=) and the axiom used for
+     * each * and + depends on this... The axiom for * depends on the
+     * strictness of its linear polynomial input, and the axiom for + depends
+     * on the strictness of **both** its inputs. The contradiction axiom is
+     * also a function of the strictness of its input.
+     *
+     * There are n *s and +s and we precompute
+     *    1. The strictness of the ith antecedant  (`ith_antecedent_is_strict`)
+     *    2. The strictness of the right argument of the ith sum
+     * (`ith_acc_is_strict`)
+     *    3. The strictness of the final result (`strict_contradiction`)
+     *
+     * Precomupation is helpful since
+     *    the computation is post-order,
+     *    but printing is pre-order.
+     */
+    std::vector<bool> ith_antecedent_is_strict(nAntecedents, false);
+    std::vector<bool> ith_acc_is_strict(nAntecedents, false);
+    for (int i = nAntecedents - 1; i >= 0; --i)
+    {
+      ith_antecedent_is_strict[i] = conflict[i].getKind() == kind::NOT;
+      if (i == (int)nAntecedents - 1)
+      {
+        ith_acc_is_strict[i] = false;
+      }
+      else
+      {
+        ith_acc_is_strict[i] =
+            ith_acc_is_strict[i + 1] || ith_antecedent_is_strict[i + 1];
+      }
+    }
+    bool strict_contradiction =
+        ith_acc_is_strict[0] || ith_antecedent_is_strict[0];
+
+    // Now, print the proof
+    os << "\n;  Farkas Combination";
+    // Choose the appropriate contradiction axiom
+    os << "\n  (lra_contra_" << (strict_contradiction ? ">" : ">=") << " _ ";
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& lit = conflict[i];
+      const char* ante_op = ith_antecedent_is_strict[i] ? ">" : ">=";
+      const char* acc_op = ith_acc_is_strict[i] ? ">" : ">=";
+      os << "\n    (lra_add_" << ante_op << "_" << acc_op << " _ _ _ ";
+      os << "\n       (lra_mul_c_" << ante_op << " _ _ ";
+      printRational(os, (*farkasCoefficients)[i].abs());
+      os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix)
+         << ")"
+         << " ; " << lit;
+    }
+
+    // The basis, at least, is always the same...
+    os << "\n    (lra_axiom_>= 0/1)";
+    std::fill_n(std::ostream_iterator<char>(os),
+                nAntecedents,
+                ')');  // close lra_add_*_*
+    os << ")";         // close lra_contra_*
+
+    os << lemmaParen.str();  // close normalizers and proof-normalizers
+  }
+  else
+  {
+    os << "\n; Arithmetic proofs which use reasoning more complex than Farkas "
+          "proofs are currently unsupported\n(clausify_false trust)\n";
   }
-  os <<"\n";
-  //os << " (clausify_false trust)";
-  ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
 }
 
 void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
-  for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
+  for (ExprSet::const_iterator it = d_declarations.begin();
+       it != d_declarations.end();
+       ++it)
+  {
     Expr term = *it;
     Assert(term.isVariable());
-    os << "(% " << ProofManager::sanitize(term) << " ";
-    os << "(term ";
-    os << term.getType() << ")\n";
+    os << "(% " << ProofManager::sanitize(term) << " var_real\n";
+    os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term)
+       << " ";
+    os << "(a_var_real " << ProofManager::sanitize(term) << ")\n";
+    paren << ")";
     paren << ")";
   }
 }
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,
diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp
index d654ea073..097fdb51e 100644
--- a/src/proof/arith_proof_recorder.cpp
+++ b/src/proof/arith_proof_recorder.cpp
@@ -30,17 +30,25 @@ ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients()
 void ArithProofRecorder::saveFarkasCoefficients(
     Node conflict, theory::arith::RationalVectorCP farkasCoefficients)
 {
+  // Verify that the conflict is a conjuction of (possibly negated) real bounds
+  // Verify that the conflict is a conjunciton ...
   Assert(conflict.getKind() == kind::AND);
   Assert(conflict.getNumChildren() == farkasCoefficients->size());
-  for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+  for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; ++i)
   {
     const Node& child = conflict[i];
-    Assert(child.getType().isBoolean() && child[0].getType().isReal());
+    // ... of possibly negated ...
+    const Node& nonNegativeChild =
+        child.getKind() == kind::NOT ? child[0] : child;
+    // ... real bounds
+    Assert(nonNegativeChild.getType().isBoolean()
+           && nonNegativeChild[0].getType().isReal());
   }
   Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl;
   if (Debug.isOn("pf::arith"))
   {
-    for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+    for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
+         ++i)
     {
       const Node& child = conflict[i];
       const Rational& r = (*farkasCoefficients)[i];