[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)

Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.

This is in preparation for the new unsat cores based on proofs.

34 files changed, 190 insertions, 103 deletions

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 3f663726c..fbb21034a 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -65,7 +65,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
   {
     theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
   }
-
+  // Add the proof checkers for each theory
+  if (d_pnm)
+  {
+    d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
+  }
   Trace("smt-debug") << "Making prop engine..." << std::endl;
   /* force destruction of referenced PropEngine to enforce that statistics
    * are unregistered by the obsolete PropEngine object before registered
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 577aa0e6c..834a3d52d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/theory_arith.h"
 
+#include "expr/proof_checker.h"
 #include "expr/proof_rule.h"
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -65,6 +66,11 @@ TheoryArith::~TheoryArith(){
 
 TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryArith::getProofChecker()
+{
+  return d_internal->getProofChecker();
+}
+
 bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
 {
   return d_internal->needsEqualityEngine(esi);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 40abe21e0..0c1320b03 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -61,6 +61,8 @@ class TheoryArith : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if this theory needs an equality engine, which is assigned
    * to it (d_equalityEngine) by the equality engine manager during
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b11bff768..d38dd881b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -172,11 +172,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_previousStatus(Result::SAT_UNKNOWN),
       d_statistics()
 {
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    d_checker.registerTo(pc);
-  }
 }
 
 TheoryArithPrivate::~TheoryArithPrivate(){
@@ -5507,6 +5502,11 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
   }
 }
 
+ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
+{
+  return &d_checker;
+}
+
 // InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const
 // inferbounds::InferBoundAlgorithm& param){
 //   Assert(param.findUpperBound());
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 929f40b56..ca2df4bd8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -335,7 +335,7 @@ private:
   // inline void raiseConflict(const ConstraintCPVec& cv){
   //   d_conflicts.push_back(cv);
   // }
-  
+
   // void raiseConflict(ConstraintCP a, ConstraintCP b);
   // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
 
@@ -508,6 +508,9 @@ private:
    */
   bool foundNonlinear() const;
 
+  /** get the proof checker of this theory */
+  ArithProofRuleChecker* getProofChecker();
+
  private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
@@ -759,7 +762,7 @@ private:
 
   static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict);
   static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict);
-  
+
   // Returns true if the node contains a literal
   // that is an arithmetic literal and is not a sat literal
   // No caching is done so this should likely only
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 543d9833c..c51f4b98a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -131,11 +131,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
   d_ppEqualityEngine.addFunctionKind(kind::SELECT);
   d_ppEqualityEngine.addFunctionKind(kind::STORE);
 
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    d_pchecker.registerTo(pc);
-  }
   // indicate we are using the default theory state object, and the arrays
   // inference manager
   d_theoryState = &d_state;
@@ -167,6 +162,8 @@ TheoryArrays::~TheoryArrays() {
 
 TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; }
+
 bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index e61c76089..24772a5f0 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -145,6 +145,8 @@ class TheoryArrays : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -349,7 +351,7 @@ class TheoryArrays : public Theory {
   NotifyClass d_notify;
 
   /** The proof checker */
-  ArraysProofRuleChecker d_pchecker;
+  ArraysProofRuleChecker d_checker;
 
   /** Conflict when merging constants */
   void conflict(TNode a, TNode b);
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index bea83ce40..933f1b1a1 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/bags/theory_bags.h"
 
+#include "expr/proof_checker.h"
 #include "smt/logic_exception.h"
 #include "theory/bags/normal_form.h"
 #include "theory/rewriter.h"
@@ -50,6 +51,8 @@ TheoryBags::~TheoryBags() {}
 
 TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
+
 bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 7bb6111bd..7505f43bf 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -46,6 +46,8 @@ class TheoryBags : public Theory
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 74279f43c..04d6e77f6 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -29,8 +29,6 @@
 #include "theory/valuation.h"
 #include "util/hash.h"
 
-using namespace std;
-
 namespace cvc5 {
 namespace theory {
 namespace booleans {
@@ -43,12 +41,6 @@ TheoryBool::TheoryBool(context::Context* c,
                        ProofNodeManager* pnm)
     : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
 {
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    // add checkers
-    d_bProofChecker.registerTo(pc);
-  }
 }
 
 Theory::PPAssertStatus TheoryBool::ppAssert(
@@ -80,6 +72,12 @@ Theory::PPAssertStatus TheoryBool::ppAssert(
   return Theory::ppAssert(tin, outSubstitutions);
 }
 
+TheoryRewriter* TheoryBool::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryBool::getProofChecker() { return &d_checker; }
+
+std::string TheoryBool::identify() const { return std::string("TheoryBool"); }
+
 }  // namespace booleans
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 05b169c24..042e487d6 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -37,18 +37,21 @@ class TheoryBool : public Theory {
              const LogicInfo& logicInfo,
              ProofNodeManager* pnm = nullptr);
 
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
 
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
 
-  std::string identify() const override { return std::string("TheoryBool"); }
+  std::string identify() const override;
 
  private:
   /** The theory rewriter for this theory. */
   TheoryBoolRewriter d_rewriter;
   /** Proof rule checker */
-  BoolProofRuleChecker d_bProofChecker;
+  BoolProofRuleChecker d_checker;
 };/* class TheoryBool */
 
 }  // namespace booleans
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index bd0374675..c2d9520d5 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -22,8 +22,6 @@
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
-using namespace std;
-
 namespace cvc5 {
 namespace theory {
 namespace builtin {
@@ -36,14 +34,12 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c,
                              ProofNodeManager* pnm)
     : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm)
 {
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    // add checkers
-    d_bProofChecker.registerTo(pc);
-  }
 }
 
+TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; }
+
 std::string TheoryBuiltin::identify() const
 {
   return std::string("TheoryBuiltin");
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index b4de83c02..fca05d7ff 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -37,7 +37,10 @@ class TheoryBuiltin : public Theory
                 const LogicInfo& logicInfo,
                 ProofNodeManager* pnm = nullptr);
 
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
 
   std::string identify() const override;
 
@@ -48,7 +51,7 @@ class TheoryBuiltin : public Theory
   /** The theory rewriter for this theory. */
   TheoryBuiltinRewriter d_rewriter;
   /** Proof rule checker */
-  BuiltinProofRuleChecker d_bProofChecker;
+  BuiltinProofRuleChecker d_checker;
 }; /* class TheoryBuiltin */
 
 }  // namespace builtin
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index c96e8d0bc..7049044d4 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -74,10 +74,6 @@ BVSolverSimple::BVSolverSimple(TheoryState* s,
       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
                 : nullptr)
 {
-  if (pnm != nullptr)
-  {
-    d_bvProofChecker.registerTo(pnm->getChecker());
-  }
 }
 
 void BVSolverSimple::addBBLemma(TNode fact)
@@ -149,6 +145,8 @@ bool BVSolverSimple::collectModelValues(TheoryModel* m,
   return d_bitblaster->collectModelValues(m, termSet);
 }
 
+BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; }
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 8983bddb2..843032bef 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -25,7 +25,6 @@
 #include "theory/eager_proof_generator.h"
 
 namespace cvc5 {
-
 namespace theory {
 namespace bv {
 
@@ -63,6 +62,9 @@ class BVSolverSimple : public BVSolver
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
+  /** get the proof checker of this theory */
+  BVProofRuleChecker* getProofChecker();
+
  private:
   /**
    * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
@@ -75,8 +77,8 @@ class BVSolverSimple : public BVSolver
 
   /** Proof generator that manages proofs for lemmas generated by this class. */
   std::unique_ptr<EagerProofGenerator> d_epg;
-
-  BVProofRuleChecker d_bvProofChecker;
+  /** Proof rule checker */
+  BVProofRuleChecker d_checker;
 };
 
 }  // namespace bv
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8f9f88ea2..0587b8da0 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/bv/theory_bv.h"
 
+#include "expr/proof_checker.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "theory/bv/bv_solver_bitblast.h"
@@ -63,6 +64,15 @@ TheoryBV::~TheoryBV() {}
 
 TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryBV::getProofChecker()
+{
+  if (options::bvSolver() == options::BVSolver::SIMPLE)
+  {
+    return static_cast<BVSolverSimple*>(d_internal.get())->getProofChecker();
+  }
+  return nullptr;
+}
+
 bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
 {
   bool need_ee = d_internal->needsEqualityEngine(esi);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c9ddaad11..c959aa5c1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,6 +25,9 @@
 #include "theory/theory_state.h"
 
 namespace cvc5 {
+
+class ProofRuleChecker;
+
 namespace theory {
 namespace bv {
 
@@ -49,6 +52,8 @@ class TheoryBV : public Theory
 
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
 
   /**
    * Returns true if we need an equality engine. If so, we initialize the
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9d231f07d..3646c47b6 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -75,13 +75,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
   d_inferManager = &d_im;
-
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    // add checkers
-    d_pchecker.registerTo(pc);
-  }
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -95,6 +88,8 @@ TheoryDatatypes::~TheoryDatatypes() {
 
 TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryDatatypes::getProofChecker() { return &d_checker; }
+
 bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
@@ -141,10 +136,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak
       if( n.getKind()==APPLY_CONSTRUCTOR ){
         ei->d_constructor = n;
       }
-      
+
       //add to selectors
       d_selector_apps[n] = 0;
-      
+
       return ei;
     }else{
       return NULL;
@@ -1018,7 +1013,7 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact
     }else{
       d_selector_apps_data[n].push_back( s );
     }
-  
+
     eqc->d_selectors = true;
   }
   if( assertFacts && !eqc->d_constructor.get().isNull() ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 34e865a50..e6df13348 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -199,6 +199,8 @@ private:
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -309,7 +311,7 @@ private:
   /** The notify class */
   NotifyClass d_notify;
   /** Proof checker for datatypes */
-  DatatypesProofRuleChecker d_pchecker;
+  DatatypesProofRuleChecker d_checker;
 };/* class TheoryDatatypes */
 
 }  // namespace datatypes
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 38444c7af..f647450c0 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -132,6 +132,8 @@ TheoryFp::TheoryFp(context::Context* c,
 
 TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; }
+
 bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notification;
@@ -940,12 +942,11 @@ void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2)
   d_im.conflictEqConstantMerge(t1, t2);
 }
 
-
-bool TheoryFp::needsCheckLastEffort() 
-{ 
+bool TheoryFp::needsCheckLastEffort()
+{
   // only need to check if we have added to the abstraction map, otherwise
   // postCheck below is a no-op.
-  return !d_abstractionMap.empty(); 
+  return !d_abstractionMap.empty();
 }
 
 void TheoryFp::postCheck(Effort level)
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 87c63a231..6ed026567 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -51,6 +51,8 @@ class TheoryFp : public Theory
   //--------------------------------- initialization
   /** Get the official theory rewriter of this theory. */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index c3c3fe7b6..31b4f8c24 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -48,13 +48,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   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);
-  }
-
   // Finish initializing the term registry by hooking it up to the inference
   // manager. This is required due to a cyclic dependency between the term
   // database and the instantiate module. Term database needs inference manager
@@ -82,6 +75,9 @@ TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
 TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryQuantifiers::getProofChecker() { return &d_checker; }
+
 void TheoryQuantifiers::finishInit()
 {
   // quantifiers are not evaluated in getModelValue
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 21c30390c..716e8cdbd 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -47,6 +47,8 @@ class TheoryQuantifiers : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /** finish initialization */
   void finishInit() override;
   /** needs equality engine */
@@ -83,7 +85,7 @@ class TheoryQuantifiers : public Theory {
   /** The theory rewriter for this theory. */
   QuantifiersRewriter d_rewriter;
   /** The proof rule checker */
-  QuantifiersProofRuleChecker d_qChecker;
+  QuantifiersProofRuleChecker d_checker;
   /** The quantifiers state */
   QuantifiersState d_qstate;
   /** The quantifiers registry */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index ab9b1b08d..6085c034d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -87,6 +87,8 @@ void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
 
 TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; }
+
 bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
@@ -174,7 +176,7 @@ void TheorySep::computeCareGraph() {
 
 void TheorySep::postProcessModel( TheoryModel* m ){
   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
-  
+
   std::vector< Node > sep_children;
   Node m_neq;
   Node m_heap;
@@ -963,9 +965,15 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) {
 }
 
 //return cardinality
-int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, 
-                                 std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
-                                 bool pol, bool hasPol, bool underSpatial ) {
+int TheorySep::processAssertion(
+    Node n,
+    std::map<int, std::map<Node, int> >& visited,
+    std::map<int, std::map<Node, std::vector<Node> > >& references,
+    std::map<int, std::map<Node, bool> >& references_strict,
+    bool pol,
+    bool hasPol,
+    bool underSpatial)
+{
   int index = hasPol ? ( pol ? 1 : -1 ) : 0;
   int card = 0;
   std::map< Node, int >::iterator it = visited[index].find( n );
@@ -975,7 +983,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
       registerRefDataTypesAtom(n);
       if( hasPol && pol ){
         references[index][n].clear();
-        references_strict[index][n] = true; 
+        references_strict[index][n] = true;
       }else{
         card = 1;
       }
@@ -993,7 +1001,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
         references[index][n].push_back( n[0] );
       }
       if( hasPol && pol ){
-        references_strict[index][n] = true; 
+        references_strict[index][n] = true;
       }else{
         card = 1;
       }
@@ -1055,7 +1063,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
   }else{
     card = it->second;
   }
-  
+
   if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
     TypeNode tn = getReferenceType( n );
     Assert(!tn.isNull());
@@ -1157,7 +1165,7 @@ void TheorySep::initializeBounds() {
       Trace("sep-bound")  << "Initialize bounds for " << tn << "..." << std::endl;
       unsigned n_emp = 0;
       if( d_bound_kind[tn] != bound_invalid ){
-        n_emp = d_card_max[tn];  
+        n_emp = d_card_max[tn];
       }else if( d_type_references[tn].empty() ){
         //must include at least one constant TODO: remove?
         n_emp = 1;
@@ -1213,12 +1221,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
       }
     }else{
       //break symmetries TODO
-    
+
       d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
     }
     //Assert( !d_type_references_all[tn].empty() );
-    
-    if( d_bound_kind[tn]!=bound_invalid ){      
+
+    if (d_bound_kind[tn] != bound_invalid)
+    {
       //construct bound
       d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
       Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
@@ -1247,7 +1256,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
         }
       }
     }
-    
+
     //assert that nil ref is not in base label
     Node nr = getNilRef( tn );
     Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate();
@@ -1344,8 +1353,16 @@ Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited )
   }
 }
 
-Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, 
-                                  TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
+Node TheorySep::instantiateLabel(Node n,
+                                 Node o_lbl,
+                                 Node lbl,
+                                 Node lbl_v,
+                                 std::map<Node, Node>& visited,
+                                 std::map<Node, Node>& pto_model,
+                                 TypeNode rtn,
+                                 std::map<Node, bool>& active_lbl,
+                                 unsigned ind)
+{
   Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
   if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
     Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
@@ -1420,7 +1437,8 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             for( unsigned i=0; i<children.size(); i++ ){
               std::vector< Node > tchildren;
               Node mval = mvals[i];
-              tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );            
+              tchildren.push_back(
+                  NodeManager::currentNM()->mkNode(kind::SUBSET, mval, lbl));
               tchildren.push_back( children[i] );
               std::vector< Node > rem_children;
               for( unsigned j=0; j<children.size(); j++ ){
@@ -1442,7 +1460,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
           Node sub_lbl_0 = d_label_map[n][lbl][0];
           Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
           wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() );
-          
+
           //return the lemma
           wchildren.push_back( children[0].negate() );
           wchildren.push_back( children[1] );
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index d52a3bca5..7d658352d 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -56,7 +56,7 @@ class TheorySep : public Theory {
 
   /** True node for predicates = false */
   Node d_false;
-  
+
   //whether bounds have been initialized
   bool d_bounds_init;
 
@@ -68,9 +68,14 @@ class TheorySep : public Theory {
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
-  int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, 
-                        std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
-                        bool pol, bool hasPol, bool underSpatial );
+  int processAssertion(
+      Node n,
+      std::map<int, std::map<Node, int> >& visited,
+      std::map<int, std::map<Node, std::vector<Node> > >& references,
+      std::map<int, std::map<Node, bool> >& references_strict,
+      bool pol,
+      bool hasPol,
+      bool underSpatial);
 
  public:
   TheorySep(context::Context* c,
@@ -93,6 +98,8 @@ class TheorySep : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -258,7 +265,7 @@ class TheorySep : public Theory {
     bound_invalid,
   };
   std::map< TypeNode, unsigned > d_bound_kind;
-  
+
   std::map< TypeNode, std::vector< Node > > d_type_references_card;
   std::map< Node, unsigned > d_type_ref_card_id;
   std::map< TypeNode, std::vector< Node > > d_type_references_all;
@@ -328,8 +335,15 @@ class TheorySep : public Theory {
   void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
   void mergePto( Node p1, Node p2 );
   void computeLabelModel( Node lbl );
-  Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, 
-                         TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
+  Node instantiateLabel(Node n,
+                        Node o_lbl,
+                        Node lbl,
+                        Node lbl_v,
+                        std::map<Node, Node>& visited,
+                        std::map<Node, Node>& pto_model,
+                        TypeNode rtn,
+                        std::map<Node, bool>& active_lbl,
+                        unsigned ind = 0);
   void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
 
   Node mkUnion( TypeNode tn, std::vector< Node >& locs );
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index bd682ca57..eb2363eb7 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -55,6 +55,8 @@ TheoryRewriter* TheorySets::getTheoryRewriter()
   return d_internal->getTheoryRewriter();
 }
 
+ProofRuleChecker* TheorySets::getProofChecker() { return nullptr; }
+
 bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 16829bc6d..14f4b5699 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -53,6 +53,8 @@ class TheorySets : public Theory
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -102,7 +104,7 @@ class TheorySets : public Theory
     void eqNotifyNewClass(TNode t) override;
     void eqNotifyMerge(TNode t1, TNode t2) override;
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
-    
+
    private:
     TheorySetsPrivate& d_theory;
   };
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2f584da7..2ce8adf95 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -84,12 +84,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
   // set up the extended function callback
   d_extTheoryCb.d_esolver = &d_esolver;
 
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    // add checkers
-    d_sProofChecker.registerTo(pc);
-  }
   // use the state object as the official theory state
   d_theoryState = &d_state;
   // use the inference manager as the official inference manager
@@ -102,6 +96,8 @@ TheoryStrings::~TheoryStrings() {
 
 TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryStrings::getProofChecker() { return &d_checker; }
+
 bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index e1fc20d29..99a3f2c04 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -74,6 +74,8 @@ class TheoryStrings : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -273,7 +275,7 @@ class TheoryStrings : public Theory {
   /** The theory rewriter for this theory. */
   StringsRewriter d_rewriter;
   /** The proof rule checker */
-  StringProofRuleChecker d_sProofChecker;
+  StringProofRuleChecker d_checker;
   /**
    * The base solver, responsible for reasoning about congruent terms and
    * inferring constants for equivalence classes.
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4b06a5fa8..050fd51f7 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -43,6 +43,7 @@ namespace cvc5 {
 
 class ProofNodeManager;
 class TheoryEngine;
+class ProofRuleChecker;
 
 namespace theory {
 
@@ -317,6 +318,10 @@ class Theory {
    */
   virtual TheoryRewriter* getTheoryRewriter() = 0;
   /**
+   * @return The proof checker associated with this theory.
+   */
+  virtual ProofRuleChecker* getProofChecker() = 0;
+  /**
    * Returns true if this theory needs an equality engine for checking
    * satisfiability.
    *
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6271f0afb..1482259e1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -24,6 +24,7 @@
 #include "expr/lazy_proof.h"
 #include "expr/node_builder.h"
 #include "expr/node_visitor.h"
+#include "expr/proof_checker.h"
 #include "expr/proof_ensure_closed.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -1894,4 +1895,17 @@ void TheoryEngine::spendResource(ResourceManager::Resource r)
   d_resourceManager->spendResource(r);
 }
 
+void TheoryEngine::initializeProofChecker(ProofChecker* pc)
+{
+  for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
+       ++id)
+  {
+    ProofRuleChecker* prc = d_theoryTable[id]->getProofChecker();
+    if (prc)
+    {
+      prc->registerTo(pc);
+    }
+  }
+}
+
 }  // namespace cvc5
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7b91191f9..03c733451 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -46,6 +46,7 @@ namespace cvc5 {
 class ResourceManager;
 class OutputManager;
 class TheoryEngineProofGenerator;
+class ProofChecker;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -322,6 +323,9 @@ class TheoryEngine {
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
 
+  /** Register theory proof rule checkers to the given proof checker */
+  void initializeProofChecker(ProofChecker* pc);
+
   void setPropEngine(prop::PropEngine* propEngine)
   {
     d_propEngine = propEngine;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f3c0a0ba0..e8ce7660a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -57,12 +57,6 @@ TheoryUF::TheoryUF(context::Context* c,
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
-
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
-  {
-    d_ufProofChecker.registerTo(pc);
-  }
   // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;
   d_inferManager = &d_im;
@@ -73,6 +67,8 @@ TheoryUF::~TheoryUF() {
 
 TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; }
+
 bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f6f4b3ee9..bae2a2544 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -111,6 +111,8 @@ private:
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -170,7 +172,7 @@ private:
   bool isHigherOrderType(TypeNode tn);
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
-  UfProofRuleChecker d_ufProofChecker;
+  UfProofRuleChecker d_checker;
   /** A (default) theory state object */
   TheoryState d_state;
   /** A (default) inference manager */