Update theory rewriter ownership, add stats to strings (#4202)

This commit adds statistics for string rewrites. This is work towards proof     
support in the string solver. At a high level, this commit adds a pointer to a  
`SequenceStatistics` in the rewriters and modifies                              
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,   
to make this work requires a couple of changes, some of them temporary:         
                                                                                
- We can't have a single `Rewriter` instance shared between different           
  `SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the        
  `SmtEngine` and calling the rewriter retrieves the rewriter associated with   
  the current `SmtEngine`. This is a temporary workaround before we get rid of  
  singletons.                                                                   
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made         
  non-`static` because they need access to the statistics instance.             
- `StringsEntail` now has non-`static` methods because it needs a reference to  
  the sequences rewriter that it can call.                                      
- The interaction between the `StringsRewriter` and the `SequencesRewriter`     
  changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits 
  from `SequencesRewriter` and calls its `postRewrite()` before applying its    
  own rewrites (this is essentially a reversal of roles from before: the        
  `SequencesRewriter` used to call `static` methods in the `StringsRewriter`).  
- The theory rewriters are now owned by the individual theories. This design    
  mirrors the `EqualityEngine`s owned by the individual theories.

1 files changed, 9 insertions, 9 deletions

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 54b9f319d..ca552de66 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -18,6 +18,7 @@
 #include "theory/rewriter.h"
 
 #include "options/theory_options.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter_tables.h"
@@ -93,13 +94,13 @@ Node Rewriter::rewrite(TNode node) {
     // eagerly for the sake of efficiency here.
     return node;
   }
-  return getInstance().rewriteTo(theoryOf(node), node);
+  return getInstance()->rewriteTo(theoryOf(node), node);
 }
 
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
-                                      std::unique_ptr<TheoryRewriter> trew)
+                                      TheoryRewriter* trew)
 {
-  getInstance().d_theoryRewriters[tid] = std::move(trew);
+  getInstance()->d_theoryRewriters[tid] = trew;
 }
 
 void Rewriter::registerPreRewrite(
@@ -130,10 +131,9 @@ void Rewriter::registerPostRewriteEqual(
   d_postRewritersEqual[tid] = fn;
 }
 
-Rewriter& Rewriter::getInstance()
+Rewriter* Rewriter::getInstance()
 {
-  thread_local static Rewriter rewriter;
-  return rewriter;
+  return smt::currentSmtEngine()->getRewriter();
 }
 
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
@@ -351,13 +351,13 @@ RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n)
 }
 
 void Rewriter::clearCaches() {
-  Rewriter& rewriter = getInstance();
+  Rewriter* rewriter = getInstance();
 
 #ifdef CVC4_ASSERTIONS
-  rewriter.d_rewriteStack.reset(nullptr);
+  rewriter->d_rewriteStack.reset(nullptr);
 #endif
 
-  rewriter.clearCachesInternal();
+  rewriter->clearCachesInternal();
 }
 
 }/* CVC4::theory namespace */