From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 22 Jul 2021 07:22:02 +0000 (-0500)
Subject: Preparation for carry the rewrite rule database in the proof checker (#6915)
X-Git-Tag: cvc5-1.0.0~1466
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b839049634d97025ac57ba9a342fd8ab70737a33;p=cvc5.git

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 96f5197e3..6a9979f75 100644
--- 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 ac5531bf4..f1f10eedb 100644
--- 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