Preparation for carry the rewrite rule database in the proof checker (#6915)

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 96f5197e3280070388bf4989575fa7238584730a..6a9979f750f6e7e0c1fdf5bb03859b9387a51bac 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -85,6 +85,11 @@ ProofCheckerStatistics::ProofCheckerStatistics()
 {
 }
 
+ProofChecker::ProofChecker(uint32_t pclevel, theory::RewriteDb* rdb)
+    : d_pclevel(pclevel), d_rdb(rdb)
+{
+}
+
 Node ProofChecker::check(ProofNode* pn, Node expected)
 {
   return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
@@ -303,6 +308,8 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
   return it->second;
 }
 
+theory::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; }
+
 uint32_t ProofChecker::getPedanticLevel(PfRule id) const
 {
   std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);

diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
index ac5531bf492d04a5234f18871c0309f47956d91b..f1f10eedb96a8951bbe6cfc044811af698bd9159 100644 (file)
--- a/src/proof/proof_checker.h
+++ b/src/proof/proof_checker.h
@@ -29,6 +29,10 @@ namespace cvc5 {
 class ProofChecker;
 class ProofNode;
 
+namespace theory {
+class RewriteDb;
+}
+
 /** A virtual base class for checking a proof rule */
 class ProofRuleChecker
 {
@@ -101,7 +105,7 @@ class ProofCheckerStatistics
 class ProofChecker
 {
  public:
-  ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {}
+  ProofChecker(uint32_t pclevel = 0, theory::RewriteDb* rdb = nullptr);
   ~ProofChecker() {}
   /**
    * Return the formula that is proven by proof node pn, or null if pn is not
@@ -162,7 +166,8 @@ class ProofChecker
                               uint32_t plevel = 10);
   /** get checker for */
   ProofRuleChecker* getCheckerFor(PfRule id);
-
+  /** get the rewrite database */
+  theory::RewriteDb* getRewriteDatabase();
   /**
    * Get the pedantic level for id if it has been assigned a pedantic
    * level via registerTrustedChecker above, or zero otherwise.
@@ -186,6 +191,8 @@ class ProofChecker
   std::map<PfRule, uint32_t> d_plevel;
   /** The pedantic level of this checker */
   uint32_t d_pclevel;
+  /** Pointer to the rewrite database */
+  theory::RewriteDb* d_rdb;
   /**
    * Check internal. This is used by check and checkDebug above. It writes
    * checking errors on out when enableOutput is true. We treat trusted checkers