Towards safe initialization of rewriter

src/theory/bags/theory_bags.cpp

@@ -52,7 +52,14 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
 
 TheoryBags::~TheoryBags() {}
 
-TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheoryBags::getTheoryRewriter()
+{
+  if (!options().bags.bagsExp)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
 

src/theory/rewriter.cpp

@@ -141,7 +141,15 @@ Node Rewriter::rewriteEqualityExt(TNode node)
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
                                       TheoryRewriter* trew)
 {
-  d_theoryRewriters[tid] = trew;
+  if (trew == nullptr)
+  {
+    // if nullptr, use the default (null) theory rewriter.
+    d_theoryRewriters[tid] = &d_nullTr;
+  }
+  else
+  {
+    d_theoryRewriters[tid] = trew;
+  }
 }
 
 TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)

src/theory/rewriter.h

@@ -176,6 +176,8 @@ class Rewriter {
 
   /** Theory rewriters used by this rewriter instance */
   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
+  /** Null theory rewriter, used when theory does not provide a rewriter */
+  NullTheoryRewriter d_nullTr;
 
   /** The proof generator */
   std::unique_ptr<TConvProofGenerator> d_tpg;

src/theory/rewriter_tables_template.h

@@ -81,7 +81,7 @@ void Rewriter::setPostRewriteCache(theory::TheoryId theoryId,
 }
 
 Rewriter::Rewriter(NodeManager* nm)
-    : d_nm(nm), d_resourceManager(nullptr), d_tpg(nullptr)
+    : d_nm(nm), d_resourceManager(nullptr), d_nullTr(nm), d_tpg(nullptr)
 {
 }
 

src/theory/sep/theory_sep.cpp

@@ -90,7 +90,14 @@ void TheorySep::initializeHeapTypes()
   }
 }
 
-TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheorySep::getTheoryRewriter()
+{
+  if (!options().sep.sepExp)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; }
 

src/theory/theory_rewriter.h

@@ -118,21 +118,21 @@ class TheoryRewriter
   virtual void registerRewrites(Rewriter* rewriter) {}
 
   /**
-   * Performs a pre-rewrite step.
+   * Performs a post-rewrite step.
    *
    * @param node The node to rewrite
    */
   virtual RewriteResponse postRewrite(TNode node) = 0;
 
   /**
-   * Performs a pre-rewrite step, with proofs.
+   * Performs a post-rewrite step, with proofs.
    *
    * @param node The node to rewrite
    */
   virtual TrustRewriteResponse postRewriteWithProof(TNode node);
 
   /**
-   * Performs a post-rewrite step.
+   * Performs a pre-rewrite step.
    *
    * @param node The node to rewrite
    */
@@ -235,6 +235,26 @@ class TheoryRewriter
   NodeManager* nodeManager() const;
 };
 
+/**
+ * The null theory rewriter, which does not perform any rewrites. This is used
+ * if a theory does not have an (active) rewriter.
+ */
+class NullTheoryRewriter : public TheoryRewriter
+{
+ public:
+  NullTheoryRewriter(NodeManager* nm) : TheoryRewriter(nm) {}
+  /** Performs a post-rewrite step. */
+  RewriteResponse postRewrite(TNode node) override
+  {
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+  /** Performs a pre-rewrite step. */
+  RewriteResponse preRewrite(TNode node) override
+  {
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+};
+
 }  // namespace theory
 }  // namespace cvc5::internal