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, 8 deletions

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 8a641743b..32a8005d1 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -63,14 +63,14 @@ class Rewriter {
   static void clearCaches();
 
   /**
-   * Registers a theory rewriter with this rewriter. This transfers the
-   * ownership of the theory rewriter to the rewriter.
+   * Registers a theory rewriter with this rewriter. The rewriter does not own
+   * the theory rewriters.
    *
    * @param tid The theory that the theory rewriter should be associated with.
    * @param trew The theory rewriter to register.
    */
   static void registerTheoryRewriter(theory::TheoryId tid,
-                                     std::unique_ptr<TheoryRewriter> trew);
+                                     TheoryRewriter* trew);
 
   /**
    * Register a prerewrite for a given kind.
@@ -112,11 +112,12 @@ class Rewriter {
 
  private:
   /**
-   * Get the (singleton) instance of the rewriter.
+   * Get the rewriter associated with the SmtEngine in scope.
    *
-   * TODO(#3468): Get rid of this singleton
+   * TODO(#3468): Get rid of this function (it relies on there being an
+   * singleton with the current SmtEngine in scope)
    */
-  static Rewriter& getInstance();
+  static Rewriter* getInstance();
 
   /** Returns the appropriate cache for a node */
   Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
@@ -148,8 +149,8 @@ class Rewriter {
 
   void clearCachesInternal();
 
-  /** Theory rewriters managed by this rewriter instance */
-  std::unique_ptr<TheoryRewriter> d_theoryRewriters[theory::THEORY_LAST];
+  /** Theory rewriters used by this rewriter instance */
+  TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 
   unsigned long d_iterationCount = 0;