(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.

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 99c80dd4a..2f882e257 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
 
 #include "context/context.h"
+#include "theory/booleans/proof_checker.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/theory.h"
 
@@ -33,19 +34,20 @@ class TheoryBool : public Theory {
              context::UserContext* u,
              OutputChannel& out,
              Valuation valuation,
-             const LogicInfo& logicInfo);
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm = nullptr);
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
-  //void check(Effort);
-
   std::string identify() const override { return std::string("TheoryBool"); }
 
  private:
   /** The theory rewriter for this theory. */
   TheoryBoolRewriter d_rewriter;
+  /** Proof rule checker */
+  BoolProofRuleChecker d_bProofChecker;
 };/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */