(proof-new) Update Theory interface for proof-new (#4648)

This includes 4 changes:

Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.

This PR is also contingent on the performance tests for proof-new on SMT-LIB.

2 files changed, 24 insertions, 7 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5a8cde21e..e7d5d36a3 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -18,6 +18,7 @@
 
 #include "base/check.h"
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/fmf/model_engine.h"
@@ -35,8 +36,13 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
+TheoryQuantifiers::TheoryQuantifiers(Context* c,
+                                     context::UserContext* u,
+                                     OutputChannel& out,
+                                     Valuation valuation,
+                                     const LogicInfo& logicInfo,
+                                     ProofNodeManager* pnm)
+    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm)
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
@@ -46,6 +52,13 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "quant-elim", this );
   out.handleUserAttribute( "quant-elim-partial", this );
+
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    // add the proof rules
+    d_qChecker.registerTo(pc);
+  }
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 0dab150ed..3168af195 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,13 +19,12 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
-#include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/output_channel.h"
+#include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/theory.h"
-#include "theory/theory_engine.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
@@ -35,9 +34,12 @@ namespace quantifiers {
 
 class TheoryQuantifiers : public Theory {
  public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u,
-                    OutputChannel& out, Valuation valuation,
-                    const LogicInfo& logicInfo);
+  TheoryQuantifiers(context::Context* c,
+                    context::UserContext* u,
+                    OutputChannel& out,
+                    Valuation valuation,
+                    const LogicInfo& logicInfo,
+                    ProofNodeManager* pnm = nullptr);
   ~TheoryQuantifiers();
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
@@ -62,6 +64,8 @@ class TheoryQuantifiers : public Theory {
  private:
   /** The theory rewriter for this theory. */
   QuantifiersRewriter d_rewriter;
+  /** The proof rule checker */
+  QuantifiersProofRuleChecker d_qChecker;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */