1 files changed, 20 insertions, 28 deletions

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);