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

2 files changed, 12 insertions, 11 deletions

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