Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

8 files changed, 126 insertions, 201 deletions

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 758a337ba..f5f8a1a10 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include "theory/arith/callbacks.h"
+
+#include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 
 namespace CVC4 {
@@ -87,17 +89,17 @@ void FarkasConflictBuilder::reset(){
   d_consequent = NullConstraint;
   d_constraints.clear();
   d_consequentSet = false;
-  PROOF(d_farkas.clear());
+  ARITH_PROOF(d_farkas.clear());
   Assert(!underConstruction());
 }
 
 /* Adds a constraint to the constraint under construction. */
 void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
   Assert(
-      !PROOF_ON()
+      !ARITH_PROOF_ON()
       || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
       || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
-  Assert(PROOF_ON() || d_farkas.empty());
+  Assert(ARITH_PROOF_ON() || d_farkas.empty());
   Assert(c->isTrue());
 
   if(d_consequent == NullConstraint){
@@ -105,17 +107,20 @@ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
   } else {
     d_constraints.push_back(c);
   }
-  PROOF(d_farkas.push_back(fc););
-  Assert(!PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
-  Assert(PROOF_ON() || d_farkas.empty());
+  ARITH_PROOF(d_farkas.push_back(fc));
+  Assert(!ARITH_PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
+  Assert(ARITH_PROOF_ON() || d_farkas.empty());
 }
 
 void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
   Assert(!mult.isZero());
-  if(PROOF_ON() && !mult.isOne()){
+  if (ARITH_PROOF_ON() && !mult.isOne())
+  {
     Rational prod = fc * mult;
     addConstraint(c, prod);
-  }else{
+  }
+  else
+  {
     addConstraint(c, fc);
   }
 }
@@ -132,7 +137,7 @@ void FarkasConflictBuilder::makeLastConsequent(){
     ConstraintCP last = d_constraints.back();
     d_constraints.back() = d_consequent;
     d_consequent = last;
-    PROOF( std::swap( d_farkas.front(), d_farkas.back() ) );
+    ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back()));
     d_consequentSet = true;
   }
 
@@ -145,14 +150,14 @@ ConstraintCP FarkasConflictBuilder::commitConflict(){
   Assert(underConstruction());
   Assert(!d_constraints.empty());
   Assert(
-      !PROOF_ON()
+      !ARITH_PROOF_ON()
       || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
       || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
-  Assert(PROOF_ON() || d_farkas.empty());
+  Assert(ARITH_PROOF_ON() || d_farkas.empty());
   Assert(d_consequentSet);
 
   ConstraintP not_c = d_consequent->getNegation();
-  RationalVectorCP coeffs = NULLPROOF(&d_farkas);
+  RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas);
   not_c->impliedByFarkas(d_constraints, coeffs, true );
 
   reset();
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 6a04e70d1..081bc08a7 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -21,7 +21,6 @@
 #include <unordered_set>
 
 #include "base/output.h"
-#include "proof/proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
@@ -551,46 +550,49 @@ bool Constraint::hasTrichotomyProof() const {
 
 void Constraint::printProofTree(std::ostream& out, size_t depth) const
 {
-#if IS_PROOFS_BUILD
-  const ConstraintRule& rule = getConstraintRule();
-  out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
-  if (hasLiteral())
+  if (ARITH_PROOF_ON())
   {
-    out << getLiteral();
-  }
-  else
-  {
-    out << "NOLIT";
-  };
-  out << "]" << ' ' << getType() << ' ' << getValue() << " (" << getProofType()
-      << ")";
-  if (getProofType() == FarkasAP)
-  {
-    out << " [";
-    bool first = true;
-    for (const auto& coeff : *rule.d_farkasCoefficients)
+    const ConstraintRule& rule = getConstraintRule();
+    out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
+    if (hasLiteral())
     {
-      if (not first)
+      out << getLiteral();
+    }
+    else
+    {
+      out << "NOLIT";
+    };
+    out << "]" << ' ' << getType() << ' ' << getValue() << " ("
+        << getProofType() << ")";
+    if (getProofType() == FarkasAP)
+    {
+      out << " [";
+      bool first = true;
+      for (const auto& coeff : *rule.d_farkasCoefficients)
       {
-        out << ", ";
+        if (not first)
+        {
+          out << ", ";
+        }
+        first = false;
+        out << coeff;
       }
-      first = false;
-      out << coeff;
+      out << "]";
     }
-    out << "]";
-  }
-  out << endl;
+    out << endl;
 
-  for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i) {
-    ConstraintCP antecdent = d_database->getAntecedent(i);
-    if (antecdent == NullConstraint) {
-      break;
+    for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i)
+    {
+      ConstraintCP antecdent = d_database->getAntecedent(i);
+      if (antecdent == NullConstraint)
+      {
+        break;
+      }
+      antecdent->printProofTree(out, depth + 1);
     }
-    antecdent->printProofTree(out, depth + 1);
+    return;
   }
-#else  /* IS_PROOFS_BUILD */
   out << "Cannot print proof. This is not a proof build." << endl;
-#endif /* IS_PROOFS_BUILD */
 }
 
 bool Constraint::sanityChecking(Node n) const {
@@ -648,8 +650,7 @@ ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
 
 
 void ConstraintRule::print(std::ostream& out) const {
-  
-  RationalVectorCP coeffs = NULLPROOF(d_farkasCoefficients);
+  RationalVectorCP coeffs = ARITH_NULLPROOF(d_farkasCoefficients);
   out << "{ConstraintRule, ";
   out << d_constraint << std::endl;
   out << "d_proofType= " << d_proofType << ", " << std::endl;
@@ -658,7 +659,7 @@ void ConstraintRule::print(std::ostream& out) const {
   if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
   {
     const ConstraintDatabase& database = d_constraint->getDatabase();
-    
+
     size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
     AntecedentId p = d_antecedentEnd;
     // must have at least one antecedent
@@ -700,9 +701,11 @@ bool Constraint::wellFormedFarkasProof() const {
   ConstraintCP antecedent = d_database->d_antecedents[p];
   if(antecedent  == NullConstraint) { return false; }
 
-#if IS_PROOFS_BUILD
-  if(!PROOF_ON()){ return cr.d_farkasCoefficients == RationalVectorCPSentinel; }
-  Assert(PROOF_ON());
+  if (!ARITH_PROOF_ON())
+  {
+    return cr.d_farkasCoefficients == RationalVectorCPSentinel;
+  }
+  Assert(ARITH_PROOF_ON());
 
   if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
   if(cr.d_farkasCoefficients->size() < 2){ return false; }
@@ -755,7 +758,7 @@ bool Constraint::wellFormedFarkasProof() const {
     default:
       return false;
     }
-    
+
     if(coeffIterator == coeffBegin){ return false; }
     --coeffIterator;
     --p;
@@ -800,10 +803,6 @@ bool Constraint::wellFormedFarkasProof() const {
   // 0 = lhs <= rhs < 0
   return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
          && rhs.sgn() < 0;
-
-#else  /* IS_PROOFS_BUILD */
-  return true;
-#endif /* IS_PROOFS_BUILD */
 }
 
 ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
@@ -860,7 +859,6 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
   , d_one(1)
   , d_negOne(-1)
 {
-  
 }
 
 SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
@@ -1109,7 +1107,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
     return isNot ? hit->getNegation(): hit;
   }else{
     Comparison negCmp = Comparison::parseNormalForm(negationNode);
-    
+
     ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
     DeltaRational negDR = negCmp.normalizedDeltaRational();
 
@@ -1213,7 +1211,8 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
   AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
 
   RationalVectorP coeffs;
-  if(PROOF_ON()){
+  if (ARITH_PROOF_ON())
+  {
     std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
 
     Rational first(sgns.first);
@@ -1222,10 +1221,11 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
     coeffs = new RationalVector();
     coeffs->push_back(first);
     coeffs->push_back(second);
-  } else {
+  }
+  else
+  {
     coeffs = RationalVectorPSentinel;
   }
-
   // no need to delete coeffs the memory is owned by ConstraintRule
   d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
 
@@ -1233,7 +1233,7 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
   if(Debug.isOn("constraint::conflictCommit") && inConflict()){
     Debug("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
   }
-  
+
   if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
     getConstraintRule().print(Debug("constraints::wffp"));
   }
@@ -1343,7 +1343,7 @@ void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
  *   coeffs != RationalVectorSentinal,
  *   coeffs->size() = a.size() + 1,
  *   for i in [0,a.size) : coeff[i] corresponds to a[i], and
- *   coeff.back() corresponds to the current constraint. 
+ *   coeff.back() corresponds to the current constraint.
  */
 void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
   Debug("constraints::pf") << "impliedByFarkas(" << this;
@@ -1359,10 +1359,9 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
   Assert(negationHasProof() == nowInConflict);
   Assert(allHaveProof(a));
 
-  Assert(PROOF_ON() == (coeffs != RationalVectorCPSentinel));
-  // !PROOF_ON() => coeffs == RationalVectorCPSentinel
-  //  PROOF_ON() => coeffs->size() == a.size() + 1
-  Assert(!PROOF_ON() || coeffs->size() == a.size() + 1);
+  Assert(ARITH_PROOF_ON() == (coeffs != RationalVectorCPSentinel));
+  Assert(!ARITH_PROOF_ON() || coeffs->size() == a.size() + 1);
+
   Assert(a.size() >= 1);
 
   d_database->d_antecedents.push_back(NullConstraint);
@@ -1374,10 +1373,13 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
   AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
 
   RationalVectorCP coeffsCopy;
-  if(PROOF_ON()){
+  if (ARITH_PROOF_ON())
+  {
     Assert(coeffs != RationalVectorCPSentinel);
     coeffsCopy = new RationalVector(*coeffs);
-  } else {
+  }
+  else
+  {
     coeffsCopy = RationalVectorCPSentinel;
   }
   d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index b32616a04..3caccdebd 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -75,9 +75,9 @@
 #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
 #define CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <unordered_map>
 #include <list>
 #include <set>
+#include <unordered_map>
 #include <vector>
 
 #include "base/configuration_private.h"
@@ -85,12 +85,12 @@
 #include "context/cdqueue.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "proof/proof.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
+#include "theory/arith/proof_macros.h"
 
 namespace CVC4 {
 namespace theory {
@@ -252,11 +252,11 @@ struct PerVariableDatabase{
   }
 };
 
-
 /**
  * If proofs are on, there is a vector of rationals for farkas coefficients.
- * This is the owner of the memory for the vector, and calls delete upon cleanup.
- * 
+ * This is the owner of the memory for the vector, and calls delete upon
+ * cleanup.
+ *
  */
 struct ConstraintRule {
   ConstraintP d_constraint;
@@ -302,17 +302,13 @@ struct ConstraintRule {
    * We do however use all of the constraints by requiring non-zero
    * coefficients.
    */
-#if IS_PROOFS_BUILD
   RationalVectorCP d_farkasCoefficients;
-#endif /* IS_PROOFS_BUILD */
   ConstraintRule()
     : d_constraint(NullConstraint)
     , d_proofType(NoAP)
     , d_antecedentEnd(AntecedentIdSentinel)
   {
-#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif /* IS_PROOFS_BUILD */
   }
 
   ConstraintRule(ConstraintP con, ArithProofType pt)
@@ -320,18 +316,14 @@ struct ConstraintRule {
     , d_proofType(pt)
     , d_antecedentEnd(AntecedentIdSentinel)
   {
-#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif /* IS_PROOFS_BUILD */
   }
   ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
     : d_constraint(con)
     , d_proofType(pt)
     , d_antecedentEnd(antecedentEnd)
   {
-#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif /* IS_PROOFS_BUILD */
   }
 
   ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
@@ -339,10 +331,8 @@ struct ConstraintRule {
     , d_proofType(pt)
     , d_antecedentEnd(antecedentEnd)
   {
-    Assert(PROOF_ON() || coeffs == RationalVectorCPSentinel);
-#if IS_PROOFS_BUILD
+    Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel);
     d_farkasCoefficients = coeffs;
-#endif /* IS_PROOFS_BUILD */
   }
 
   void print(std::ostream& out) const;
@@ -750,7 +740,7 @@ class Constraint {
 
   /**
    * If the constraint
-   *   canBePropagated() and 
+   *   canBePropagated() and
    *   !assertedToTheTheory(),
    * the constraint is added to the database's propagation queue.
    *
@@ -789,9 +779,11 @@ class Constraint {
       ConstraintP constraint = crp->d_constraint;
       Assert(constraint->d_crid != ConstraintRuleIdSentinel);
       constraint->d_crid = ConstraintRuleIdSentinel;
-
-      PROOF(if (crp->d_farkasCoefficients != RationalVectorCPSentinel) {
-        delete crp->d_farkasCoefficients;
+      ARITH_PROOF({
+        if (crp->d_farkasCoefficients != RationalVectorCPSentinel)
+        {
+          delete crp->d_farkasCoefficients;
+        }
       });
     }
   };
@@ -876,10 +868,11 @@ class Constraint {
     return getConstraintRule().d_antecedentEnd;
   }
 
-  inline RationalVectorCP getFarkasCoefficients() const {
-    return NULLPROOF(getConstraintRule().d_farkasCoefficients);
+  inline RationalVectorCP getFarkasCoefficients() const
+  {
+    return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients);
   }
-  
+
   void debugPrint() const;
 
   /**
@@ -1051,8 +1044,7 @@ private:
      * The index in this list is the proper ordering of the proofs.
      */
     ConstraintRuleList d_constraintProofs;
-    
-    
+
     /**
      * Contains the exact list of constraints that can be used for propagation.
      */
@@ -1100,9 +1092,9 @@ private:
 
   const Rational d_one;
   const Rational d_negOne;
-  
+
   friend class Constraint;
-  
+
 public:
 
   ConstraintDatabase( context::Context* satContext,
@@ -1209,7 +1201,7 @@ public:
 
   /** AntecendentID must be in range. */
   ConstraintCP getAntecedent(AntecedentId p) const;
-  
+
 private:
   /** returns true if cons is now in conflict. */
   bool handleUnateProp(ConstraintP ant, ConstraintP cons);
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 7eb2f3f9e..3c4f678a2 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -510,11 +510,11 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
   RowIndex ridx = d_tableau.basicToRowIndex(basic);
 
   ConstraintCPVec bounds;
-  RationalVectorP coeffs = NULLPROOF(new RationalVector());
+  RationalVectorP coeffs = ARITH_NULLPROOF(new RationalVector());
   propagateRow(bounds, ridx, upperBound, c, coeffs);
   c->impliedByFarkas(bounds, coeffs, false);
   c->tryToPropagate();
-  
+
   if(coeffs != RationalVectorPSentinel) { delete coeffs; }
 }
 
@@ -524,9 +524,9 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
  * The proof is in terms of the other constraints and the negation of c, ~c.
  *
  * A row has the form:
- *   sum a_i * x_i  = 0 
+ *   sum a_i * x_i  = 0
  * or
- *   sx + sum r y + sum q z = 0 
+ *   sx + sum r y + sum q z = 0
  * where r > 0 and q < 0.
  *
  * If rowUp, we are proving c
@@ -555,7 +555,7 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo
     Assert(farkas->empty());
     farkas->push_back(Rational(0));
   }
-  
+
   ArithVar v = c->getVariable();
   Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
                                    << ridx << ", " << rowUp << ", " << v << ") start" << endl;
@@ -563,7 +563,7 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo
   const Rational& multiple = rowUp ? d_one : d_negOne;
 
   Debug("arith::propagateRow") << "multiple: " << multiple << endl;
-  
+
   Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
   for(; !iter.atEnd(); ++iter){
     const Tableau::Entry& entry = *iter;
@@ -595,8 +595,8 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo
       if(farkas != RationalVectorPSentinel){
         Assert(farkas->front().isZero());
         Rational multAij = multiple * a_ij;
-        Debug("arith::propagateRow") << "("<<multAij<<") ";        
-        farkas->front() = multAij;      
+        Debug("arith::propagateRow") << "(" << multAij << ") ";
+        farkas->front() = multAij;
       }
 
       Debug("arith::propagateRow") << c << endl;
@@ -605,10 +605,10 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo
       ConstraintCP bound = selectUb
         ? d_variables.getUpperBoundConstraint(nonbasic)
         : d_variables.getLowerBoundConstraint(nonbasic);
-      
+
       if(farkas != RationalVectorPSentinel){
         Rational multAij = multiple * a_ij;
-        Debug("arith::propagateRow") << "("<<multAij<<") ";        
+        Debug("arith::propagateRow") << "(" << multAij << ") ";
         farkas->push_back(multAij);
       }
       Assert(bound != NullConstraint);
@@ -678,7 +678,7 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
  * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
  *
  * A row has the form:
- *   -x_b sum a_i * x_i  = 0 
+ *   -x_b sum a_i * x_i  = 0
  * or
  *   -x_b + sum r y + sum q z = 0,
  *    x_b = sum r y + sum q z
@@ -724,7 +724,7 @@ ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithV
     Assert(assignment < d_variables.getLowerBound(basicVar));
     surplus = d_variables.getLowerBound(basicVar) - assignment;
   }
-  
+
   bool anyWeakenings = false;
   for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
     const Tableau::Entry& entry = *i;
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index cc10d6659..cfa153a56 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
+#include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ea751ca74..762634ce7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -41,7 +41,6 @@ TheoryArith::TheoryArith(context::Context* c,
       d_internal(
           new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
-      d_proofRecorder(nullptr),
       d_astate(*d_internal, c, u, valuation)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index bfe30db61..6adf8f66a 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -18,7 +18,6 @@
 #pragma once
 
 #include "expr/node.h"
-#include "proof/arith_proof_recorder.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/theory_arith_private_forward.h"
 #include "theory/theory.h"
@@ -41,11 +40,6 @@ class TheoryArith : public Theory {
 
   TimerStat d_ppRewriteTimer;
 
-  /**
-   * @brief Where to store Farkas proofs of lemmas
-   */
-  proof::ArithProofRecorder * d_proofRecorder;
-
  public:
   TheoryArith(context::Context* c,
               context::UserContext* u,
@@ -110,11 +104,6 @@ class TheoryArith : public Theory {
 
   std::pair<bool, Node> entailmentCheck(TNode lit) override;
 
-  void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
-  {
-    d_proofRecorder = proofRecorder;
-  }
-
  private:
   /** The state object wrapping TheoryArithPrivate  */
   ArithState d_astate;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7f521e2f9..8a780116c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -624,7 +624,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
     ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
     ConstraintP negation = constraint->getNegation();
     negation->impliedByUnate(ubc, true);
-    
+
     raiseConflict(constraint);
 
     ++(d_statistics.d_statAssertLowerConflicts);
@@ -757,7 +757,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
   if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
     return false; //sat
   }
-  
+
   // cmpToLb =  \lowerbound(x_i).cmp(c_i)
   int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
   if( cmpToLB < 0 ){ //  \upperbound(x_i) < \lowerbound(x_i)
@@ -802,7 +802,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
         ++(d_statistics.d_statDisequalityConflicts);
         raiseConflict(eq);
         return true;
-      }      
+      }
     }
   }else if(cmpToLB > 0){
     // l <= x <= u and l < u
@@ -1291,8 +1291,10 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
   }else{
     if (d_nonlinearExtension == nullptr)
     {
-      if( vlNode.getKind()==kind::EXPONENTIAL || vlNode.getKind()==kind::SINE || 
-          vlNode.getKind()==kind::COSINE || vlNode.getKind()==kind::TANGENT ){
+      if (vlNode.getKind() == kind::EXPONENTIAL
+          || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
+          || vlNode.getKind() == kind::TANGENT)
+      {
         d_nlIncomplete = true;
       }
     }
@@ -1737,7 +1739,6 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
   } else {
     Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
   }
-  
 
   if(Debug.isOn("arith::negatedassumption") && inConflict){
     ConstraintP negation = constraint->getNegation();
@@ -1905,7 +1906,7 @@ void TheoryArithPrivate::outputConflicts(){
   Debug("arith::conflict") << "outputting conflicts" << std::endl;
   Assert(anyConflict());
   static unsigned int conflicts = 0;
-  
+
   if(!conflictQueueEmpty()){
     Assert(!d_conflicts.empty());
     for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
@@ -1923,35 +1924,6 @@ void TheoryArithPrivate::outputConflicts(){
       ++conflicts;
       Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
                                << " has proof: " << hasProof << endl;
-      PROOF(if (d_containing.d_proofRecorder && confConstraint->hasFarkasProof()
-                && pf.d_farkasCoefficients->size()
-                       == conflict.getNumChildren()) {
-        // The Farkas coefficients and the children of `conflict` seem to be in
-        // opposite orders... There is some relevant documentation in the
-        // comment for the d_farkasCoefficients field  in "constraint.h"
-        //
-        // Anyways, we reverse the children in `conflict` here.
-        NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
-        for (size_t j = 0, nchildren = conflict.getNumChildren(); j < nchildren;
-             ++j)
-        {
-          conflictInFarkasCoefficientOrder
-              << conflict[conflict.getNumChildren() - j - 1];
-        }
-
-        if (Debug.isOn("arith::pf::tree")) {
-          confConstraint->printProofTree(Debug("arith::pf::tree"));
-          confConstraint->getNegation()->printProofTree(Debug("arith::pf::tree"));
-        }
-
-        Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
-        if (confConstraint->hasSimpleFarkasProof()
-            && confConstraint->getNegation()->isPossiblyTightenedAssumption())
-        {
-          d_containing.d_proofRecorder->saveFarkasCoefficients(
-              conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);
-        }
-      })
       if(Debug.isOn("arith::normalize::external")){
         conflict = flattenAndSort(conflict);
         Debug("arith::conflict") << "(normalized to) " << conflict << endl;
@@ -2190,7 +2162,6 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D
       return make_pair(imp, added);
     }
   }
-  
 
   ConstraintP newc = d_constraintDatabase.getConstraint(v, t, dr);
   d_replayConstraints.push_back(newc);
@@ -2337,7 +2308,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
       // ConstraintCPVec& back = conflicts.back();
       // back.push_back(conflicting);
       // back.push_back(negConflicting);
-      
+
       // // remove the floor/ceiling contraint implied by bcneg
       // Constraint::assertionFringe(back);
     }
@@ -2375,14 +2346,15 @@ void TheoryArithPrivate::replayAssert(ConstraintP c) {
     }else{
       Debug("approx::replayAssert") << "replayAssert " << c << " has explanation" << endl;
     }
-    Debug("approx::replayAssert") << "replayAssertion " << c << endl;    
+    Debug("approx::replayAssert") << "replayAssertion " << c << endl;
     if(inConflict){
       raiseConflict(c);
     }else{
       assertionCases(c);
     }
   }else{
-    Debug("approx::replayAssert") << "replayAssert " << c << " already asserted" << endl;    
+    Debug("approx::replayAssert")
+        << "replayAssert " << c << " already asserted" << endl;
   }
 }
 
@@ -2551,7 +2523,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
         SimplexDecisionProcedure& simplex = selectSimplex(true);
         simplex.findModel(false);
-	// can change d_qflraStatus
+        // can change d_qflraStatus
 
         d_linEq.stopTrackingBoundCounts();
         d_partialModel.startQueueingBoundCounts();
@@ -3101,13 +3073,13 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
     << " " << useApprox
     << " " << safeToCallApprox()
     << endl;
-  
+
   bool noPivotLimitPass1 = noPivotLimit && !useApprox;
   d_qflraStatus = simplex.findModel(noPivotLimitPass1);
 
   Debug("TheoryArithPrivate::solveRealRelaxation")
     << "solveRealRelaxation()" << " pass1 " << d_qflraStatus << endl;
-  
+
   if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
     // pass2: fancy-final
     static const int32_t relaxationLimit = 10000;
@@ -3275,7 +3247,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //   if(!useFancyFinal){
 //     d_qflraStatus = simplex.findModel(noPivotLimit);
 //   }else{
-    
 
 //     if(d_qflraStatus == Result::SAT_UNKNOWN){
 //       //Message() << "got sat unknown" << endl;
@@ -3711,7 +3682,7 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
     Integer ceil_d = d.ceiling();
     Rational f = r - floor_d;
     // Multiply by -1 to get abs value.
-    Rational c = (r - ceil_d) * (-1); 
+    Rational c = (r - ceil_d) * (-1);
     Integer nearest = (c > f) ? floor_d : ceil_d;
 
     // Prioritize trying a simple rounding of the real solution first,
@@ -4651,7 +4622,6 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
 
     ConstraintP implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
     if(implied != NullConstraint){
-      
       return rowImplicationCanBeApplied(ridx, rowUp, implied);
     }
   }
@@ -4699,9 +4669,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
 
   if( !assertedToTheTheory && canBePropagated && !hasProof ){
     ConstraintCPVec explain;
-
-    PROOF(d_farkasBuffer.clear());
-    RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer);
+    ARITH_PROOF(d_farkasBuffer.clear());
+    RationalVectorP coeffs = ARITH_NULLPROOF(&d_farkasBuffer);
 
     // After invoking `propegateRow`:
     //   * coeffs[0] is for implied
@@ -4716,38 +4685,6 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
       }
       Node implication = implied->externalImplication(explain);
       Node clause = flattenImplication(implication);
-      PROOF(if (d_containing.d_proofRecorder
-                && coeffs != RationalVectorCPSentinel
-                && coeffs->size() == clause.getNumChildren()) {
-        Debug("arith::prop") << "implied    : " << implied << std::endl;
-        Debug("arith::prop") << "implication: " << implication << std::endl;
-        Debug("arith::prop") << "coeff len: " << coeffs->size() << std::endl;
-        Debug("arith::prop") << "exp    : " << explain << std::endl;
-        Debug("arith::prop") << "clause : " << clause << std::endl;
-        Debug("arith::prop")
-            << "clause len: " << clause.getNumChildren() << std::endl;
-        Debug("arith::prop") << "exp len: " << explain.size() << std::endl;
-        // Using the information from the above comment we assemble a conflict
-        // AND in coefficient order
-        NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
-        conflictInFarkasCoefficientOrder << implication[1].negate();
-        for (const Node& antecedent : implication[0])
-        {
-          Debug("arith::prop") << "  ante: " << antecedent << std::endl;
-          conflictInFarkasCoefficientOrder << antecedent;
-        }
-
-        Assert(coeffs != RationalVectorPSentinel);
-        Assert(conflictInFarkasCoefficientOrder.getNumChildren()
-               == coeffs->size());
-        if (std::all_of(explain.begin(), explain.end(), [](ConstraintCP c) {
-              return c->isAssumption() || c->hasIntTightenProof();
-            }))
-        {
-          d_containing.d_proofRecorder->saveFarkasCoefficients(
-              conflictInFarkasCoefficientOrder, coeffs);
-        }
-      })
       outputLemma(clause);
     }else{
       Assert(!implied->negationHasProof());