5 files changed, 46 insertions, 3 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index ff71f6432..352ba0f36 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -602,7 +602,7 @@ void ConstraintRule::print(std::ostream& out) const {
 
 bool Constraint::wellFormedFarkasProof() const {
   Assert(hasProof());
-  
+
   const ConstraintRule& cr = getConstraintRule();
   if(cr.d_constraint != this){ return false; }
   if(cr.d_proofType != FarkasAP){ return false; }
@@ -1071,6 +1071,7 @@ ConstraintP ConstraintDatabase::lookup(TNode literal) const{
 }
 
 void Constraint::setAssumption(bool nowInConflict){
+  Debug("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(hasLiteral());
@@ -1113,6 +1114,7 @@ void Constraint::propagate(){
  *  1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
  */
 void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")" << std::endl;
   Assert(!hasProof());
   Assert(imp->hasProof());
   Assert(negationHasProof() == nowInConflict);
@@ -1152,6 +1154,8 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
 }
 
 void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a << ", ";
+  Debug("constraints::pf") << *b << ")" << std::endl;
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(a->hasProof());
@@ -1180,6 +1184,7 @@ bool Constraint::allHaveProof(const ConstraintCPVec& b){
 }
 
 void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")" << std::endl;
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(a->hasProof());
@@ -1196,6 +1201,15 @@ void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
 }
 
 void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByIntHole(" << this;
+  if (Debug.isOn("constraints::pf")) {
+    for (const ConstraintCP& p : b)
+    {
+      Debug("constraints::pf") << ", " << p;
+    }
+  }
+  Debug("constraints::pf") << ")" << std::endl;
+
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(allHaveProof(b));
@@ -1224,6 +1238,15 @@ void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
  *   coeff.back() corresponds to the current constraint. 
  */
 void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByFarkas(" << this;
+  if (Debug.isOn("constraints::pf")) {
+    for (const ConstraintCP& p : a)
+    {
+      Debug("constraints::pf") << ", " << p;
+    }
+  }
+  Debug("constraints::pf") << ", <coeffs>";
+  Debug("constraints::pf") << ")" << std::endl;
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(allHaveProof(a));
@@ -1263,6 +1286,8 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
 
 
 void Constraint::setInternalAssumption(bool nowInConflict){
+  Debug("constraints::pf") << "setInternalAssumption(" << this;
+  Debug("constraints::pf") << ")" << std::endl;
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(!assertedToTheTheory());
@@ -1277,6 +1302,8 @@ void Constraint::setInternalAssumption(bool nowInConflict){
 
 
 void Constraint::setEqualityEngineProof(){
+  Debug("constraints::pf") << "setEqualityEngineProof(" << this;
+  Debug("constraints::pf") << ")" << std::endl;
   Assert(truthIsUnknown());
   Assert(hasLiteral());
   d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 5eef9663e..d411f2d34 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -928,7 +928,11 @@ private:
   /** Return true if every element in b has a proof. */
   static bool allHaveProof(const ConstraintCPVec& b);
 
-  /** Precondition: hasFarkasProof() */
+  /** Precondition: hasFarkasProof()
+   * Computes the combination implied by the farkas coefficients. Sees if it is
+   * a contradiction.
+   */
+
   bool wellFormedFarkasProof() const;
   
 }; /* class ConstraintValue */
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 6650e6680..5fd585588 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -216,7 +216,7 @@ public:
   int getUpId() const;
 
   /**
-   * Looks up a row id to the appropraite arith variable.
+   * Looks up a row id to the appropriate arith variable.
    * Be careful these are deleted in context during replay!
    * failure returns ARITHVAR_SENTINEL */
   ArithVar lookupRowId(int rowId) const;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d7113b17d..9902121d0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -36,6 +36,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
     , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
+    , d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
   if (options::nlExt()) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 195cb1883..e4b1c5b26 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -19,6 +19,7 @@
 
 #include "theory/theory.h"
 #include "expr/node.h"
+#include "proof/arith_proof_recorder.h"
 #include "theory/arith/theory_arith_private_forward.h"
 
 
@@ -40,6 +41,11 @@ private:
 
   TimerStat d_ppRewriteTimer;
 
+  /**
+   * @brief Where to store Farkas proofs of lemmas
+   */
+  proof::ArithProofRecorder * d_proofRecorder;
+
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
               Valuation valuation, const LogicInfo& logicInfo);
@@ -90,6 +96,11 @@ public:
       const EntailmentCheckParameters* params,
       EntailmentCheckSideEffects* out) override;
 
+  void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
+  {
+    d_proofRecorder = proofRecorder;
+  }
+
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */