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.

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 6cb3bf3ff2668b7b89707c8e0212eaaab12c2e3f..361d90dcd974401b219d33581445c5e99abcc4ba 100644 (file)
--- 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 f96062b6154057b3a28297130aaf3001332c905c..d90af4a31ef062709e009e0857019d7ffb272001 100644 (file)
--- 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 */