(proof-new) Add proof managers and eager gens to arith (#5159)

This commit threads ProofNodeManager, EagerProofGenerator, etc
throughout the arith theory into the appropriate locations. These
objects are currently unused, but will be used in future commits.

Crediting Andy, since he set up some of this.

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com

1 files changed, 13 insertions, 7 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index eb2d89de7..0afc0bc2f 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -85,6 +85,7 @@
 #include "context/cdqueue.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
 #include "theory/arith/congruence_manager.h"
@@ -1086,6 +1087,10 @@ private:
   ArithCongruenceManager& d_congruenceManager;
 
   const context::Context * const d_satContext;
+  /** Owned by the TheoryArithPrivate, used here. */
+  EagerProofGenerator* d_pfGen;
+  /** Owned by the TheoryArithPrivate, used here. */
+  ProofNodeManager* d_pnm;
 
   RaiseConflict d_raiseConflict;
 
@@ -1095,13 +1100,14 @@ private:
 
   friend class Constraint;
 
-public:
-
-  ConstraintDatabase( context::Context* satContext,
-                      context::Context* userContext,
-                      const ArithVariables& variables,
-                      ArithCongruenceManager& dm,
-                      RaiseConflict conflictCallBack);
+ public:
+  ConstraintDatabase(context::Context* satContext,
+                     context::Context* userContext,
+                     const ArithVariables& variables,
+                     ArithCongruenceManager& dm,
+                     RaiseConflict conflictCallBack,
+                     EagerProofGenerator* pfGen,
+                     ProofNodeManager* pnm);
 
   ~ConstraintDatabase();