(proof-new) Theory engine proof producing (#5195)

This completes proof support in TheoryEngine.

The main addition in this PR is to make its getExplanation method proof producing.

1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e410bddd5..fd6d1af27 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -42,6 +42,7 @@
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
+#include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
@@ -111,7 +112,6 @@ class TheoryEngine {
 
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
-  friend class theory::CombinationEngine;
   friend class theory::EngineOutputChannel;
   friend class theory::CombinationEngine;
   friend class theory::SharedSolver;
@@ -175,9 +175,6 @@ class TheoryEngine {
   /** are we in eager model building mode? (see setEagerModelBuilding). */
   bool d_eager_model_building;
 
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
   /**
    * Output channels for individual theories.
    */
@@ -315,7 +312,8 @@ class TheoryEngine {
                ResourceManager* rm,
                RemoveTermFormulas& iteRemover,
                const LogicInfo& logic,
-               OutputManager& outMgr);
+               OutputManager& outMgr,
+               ProofNodeManager* pnm);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -339,7 +337,7 @@ class TheoryEngine {
                                               *d_theoryOut[theoryId],
                                               theory::Valuation(this),
                                               d_logicInfo,
-                                              nullptr);
+                                              d_pnm);
     theory::Rewriter::registerTheoryRewriter(
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
@@ -365,6 +363,9 @@ class TheoryEngine {
     return d_propEngine;
   }
 
+  /** Get the proof node manager */
+  ProofNodeManager* getProofNodeManager() const;
+
   /**
    * Get a pointer to the underlying sat context.
    */
@@ -740,7 +741,6 @@ private:
 
  private:
   IntStat d_arithSubstitutionsAdded;
-
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */