(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, 16 insertions, 12 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 513ed6bc0..c98de0f18 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -65,10 +65,13 @@ class TheoryBV : public Theory {
   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
-public:
-
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
+ public:
+  TheoryBV(context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
+           ProofNodeManager* pnm = nullptr,
            std::string name = "");
 
   ~TheoryBV();
@@ -79,7 +82,7 @@ public:
 
   void finishInit() override;
 
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode n) override;
 
@@ -89,7 +92,7 @@ public:
 
   void propagate(Effort e) override;
 
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
@@ -100,27 +103,28 @@ public:
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node> >& exp) override;
+                              std::map<Node, std::vector<Node>>& exp) override;
   int getReduction(int effort, Node n, Node& nr) override;
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   void enableCoreTheorySlicer();
 
-  Node ppRewrite(TNode t) override;
+  TrustNode ppRewrite(TNode t) override;
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
   void presolve() override;
 
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+  bool applyAbstraction(const std::vector<Node>& assertions,
+                        std::vector<Node>& new_assertions);
 
   void setProofLog(proof::BitVectorProof* bvp);
 
  private:
-
-  class Statistics {
-  public:
+  class Statistics
+  {
+   public:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;