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

4 files changed, 198 insertions, 2 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 3b57be1f2..1d51f99e1 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -640,8 +640,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
 }
 
 ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
-  : TheoryProof(arith, pe), d_realMode(false)
-{}
+  : TheoryProof(arith, pe), d_recorder(), d_realMode(false)
+{
+  arith->setProofRecorder(&d_recorder);
+}
 
 theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; }
 void ArithProof::registerTerm(Expr term) {
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 27012184a..a58294998 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "expr/expr.h"
+#include "proof/arith_proof_recorder.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "theory/uf/equality_engine.h"
@@ -62,6 +63,11 @@ protected:
   //   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
   ExprSet d_declarations; // all the variable/function declarations
 
+  /**
+   * @brief Where farkas proofs of lemmas are stored.
+   */
+  proof::ArithProofRecorder d_recorder;
+
   bool d_realMode;
   theory::TheoryId getTheoryId() override;
 
diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp
new file mode 100644
index 000000000..d654ea073
--- /dev/null
+++ b/src/proof/arith_proof_recorder.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file arith_proof_recorder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for recording the skeletons of arithmetic proofs at solve
+ ** time so they can later be used during proof-production time.
+ **/
+
+#include "proof/arith_proof_recorder.h"
+
+#include <algorithm>
+#include <vector>
+
+#include "base/map_util.h"
+
+namespace CVC4 {
+namespace proof {
+
+ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients()
+{
+  // Nothing else
+}
+void ArithProofRecorder::saveFarkasCoefficients(
+    Node conflict, theory::arith::RationalVectorCP farkasCoefficients)
+{
+  Assert(conflict.getKind() == kind::AND);
+  Assert(conflict.getNumChildren() == farkasCoefficients->size());
+  for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+  {
+    const Node& child = conflict[i];
+    Assert(child.getType().isBoolean() && child[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)
+    {
+      const Node& child = conflict[i];
+      const Rational& r = (*farkasCoefficients)[i];
+      Debug("pf::arith") << "  " << std::setw(8) << r;
+      Debug("pf::arith") << "  " << child << std::endl;
+    }
+  }
+
+  std::set<Node> lits;
+  std::copy(
+      conflict.begin(), conflict.end(), std::inserter(lits, lits.begin()));
+
+  d_lemmasToFarkasCoefficients[lits] =
+      std::make_pair(std::move(conflict), *farkasCoefficients);
+}
+
+bool ArithProofRecorder::hasFarkasCoefficients(
+    const std::set<Node>& conflict) const
+{
+  return d_lemmasToFarkasCoefficients.find(conflict)
+         != d_lemmasToFarkasCoefficients.end();
+}
+
+std::pair<Node, theory::arith::RationalVectorCP>
+ArithProofRecorder::getFarkasCoefficients(const std::set<Node>& conflict) const
+{
+  if (auto *p = FindOrNull(d_lemmasToFarkasCoefficients, conflict))
+  {
+    return std::make_pair(p->first, &p->second);
+  }
+  else
+  {
+    return std::make_pair(Node(), theory::arith::RationalVectorCPSentinel);
+  }
+}
+
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h
new file mode 100644
index 000000000..2d0501332
--- /dev/null
+++ b/src/proof/arith_proof_recorder.h
@@ -0,0 +1,107 @@
+/*********************                                                        */
+/*! \file arith_proof_recorder.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for recording the skeletons of arithmetic proofs at solve
+ ** time so they can later be used during proof-production time.
+ **
+ ** In particular, we're interested in proving bottom from a conjunction of
+ ** theory literals.
+ **
+ ** For now, we assume that this can be done using a Farkas combination, and if
+ ** that doesn't work for some reason, then we give up and "trust" the lemma.
+ ** In the future we'll build support for more sophisticated reasoning.
+ **
+ ** Given this scope, our task is to...
+ **   for each lemma (a set of literals)
+ **   save the Farkas coefficients for those literals
+ **      which requires we save an ordering of the literals
+ **      and a parallel ordering of Farkas coefficients.
+ **
+ ** Farkas proofs have the following core structure:
+ **    For a list of affine bounds: c[i] dot x >= b[i]
+ **      (x is a vector of variables)
+ **      (c[i] is a vector of coefficients)
+ **    and a list of non-negative coefficients: f[i],
+ **    compute
+ **
+ **             sum_i{ (c[i] dot x) * f[i] }     and   sum_i{b[i]*f[i]}
+ **
+ **    and then verify that the left is actually < the right, a contradiction
+ **
+ **    To be clear: this code does not check Farkas proofs, it just stores the
+ **    information needed to write them.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H
+
+#include <map>
+#include <set>
+
+#include "expr/node.h"
+#include "theory/arith/constraint_forward.h"
+
+namespace CVC4 {
+namespace proof {
+
+class ArithProofRecorder
+{
+ public:
+  ArithProofRecorder();
+
+  /**
+   * @brief For a set of incompatible literals, save the Farkas coefficients
+   * demonstrating their incompatibility
+   *
+   * @param conflict a conjunction of conflicting literals
+   * @param farkasCoefficients a list of rational coefficients which the literals
+   *       should be multiplied by (pairwise) to produce a contradiction.
+   *
+   * The orders of the two vectors must agree!
+   */
+  void saveFarkasCoefficients(
+      Node conflict, theory::arith::RationalVectorCP farkasCoefficients);
+
+  /**
+   * @brief Determine whether some literals have a Farkas proof of their
+   * incompatibility
+   *
+   * @param conflict a conjunction of (putatively) conflicting literals
+   *
+   * @return whether or not there is actually a proof for them.
+   */
+  bool hasFarkasCoefficients(const std::set<Node>& conflict) const;
+
+  /**
+   * @brief Get the Farkas Coefficients object
+   *
+   * @param conflict a conjunction of conflicting literals
+   * @return theory::arith::RationalVectorCP -- the Farkas coefficients
+   *         Node -- a conjunction of the problem literals in coefficient order
+   *
+   *         theory::arith::RationalVectorCPSentinel if there is no entry for
+   * these lits
+   */
+  std::pair<Node, theory::arith::RationalVectorCP> getFarkasCoefficients(
+      const std::set<Node>& conflict) const;
+
+ protected:
+  // For each lemma, save the Farkas coefficients of that lemma
+  std::map<std::set<Node>, std::pair<Node, theory::arith::RationalVector>>
+      d_lemmasToFarkasCoefficients;
+};
+
+}  // namespace proof
+}  // namespace CVC4
+
+#endif