From f047038b1bec31a1ebb89e9d35e3aebb3301eddc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Oct 2021 19:35:14 -0500
Subject: [PATCH] Make proofs of rewrites robust to use in internal subsolvers
 (#7411)

We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance.

This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique.
---
 src/theory/rewriter.cpp | 22 ++++++++++------------
 src/theory/rewriter.h   | 11 +++++++++++
 2 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 6cb3bf3ff..361d90dcd 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -32,13 +32,6 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
-/** Attribute true for nodes that have been rewritten with proofs enabled */
-struct RewriteWithProofsAttributeId
-{
-};
-typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
-    RewriteWithProofsAttribute;
-
 // Note that this function is a simplified version of Theory::theoryOf for
 // (type-based) theoryOfMode. We expand and simplify it here for the sake of
 // efficiency.
@@ -173,7 +166,6 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                          Node node,
                          TConvProofGenerator* tcpg)
 {
-  RewriteWithProofsAttribute rpfa;
 #ifdef CVC5_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
@@ -187,7 +179,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
 
   // Check if it's been cached already
   Node cached = getPostRewriteCache(theoryId, node);
-  if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa)))
+  if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
   {
     return cached;
   }
@@ -217,7 +209,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
                                   rewriteStackTop.d_node);
       if (cached.isNull()
-          || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
+          || (tcpg != nullptr
+              && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
       {
         // Rewrite until fix-point is reached
         for(;;) {
@@ -256,7 +249,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                                  rewriteStackTop.d_node);
     // If not, go through the children
     if (cached.isNull()
-        || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
+        || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
     {
       // The child we need to rewrite
       unsigned child = rewriteStackTop.d_nextChild++;
@@ -343,7 +336,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       if (tcpg != nullptr)
       {
         // if proofs are enabled, mark that we've rewritten with proofs
-        rewriteStackTop.d_original.setAttribute(rpfa, true);
+        d_tpgNodes.insert(rewriteStackTop.d_original);
         if (!cached.isNull())
         {
           // We may have gotten a different node, due to non-determinism in
@@ -474,5 +467,10 @@ void Rewriter::clearCaches()
   clearCachesInternal();
 }
 
+bool Rewriter::hasRewrittenWithProofs(TNode n) const
+{
+  return d_tpgNodes.find(n) != d_tpgNodes.end();
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f96062b61..d90af4a31 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -159,6 +159,11 @@ class Rewriter {
 
   void clearCachesInternal();
 
+  /**
+   * Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
+   */
+  bool hasRewrittenWithProofs(TNode n) const;
+
   /** The resource manager, for tracking resource usage */
   ResourceManager* d_resourceManager;
 
@@ -167,6 +172,12 @@ class Rewriter {
 
   /** The proof generator */
   std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * Nodes rewritten with proofs. Since d_tpg contains a reference to all
+   * nodes that have been rewritten with proofs, we can keep only a TNode
+   * here.
+   */
+  std::unordered_set<TNode> d_tpgNodes;
 #ifdef CVC5_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
 #endif /* CVC5_ASSERTIONS */
-- 
2.30.2