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, 4 insertions, 6 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 63ca46b41..a6751e1ec 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -56,6 +56,7 @@ class QuantifiersEngine;
 class TheoryModel;
 class SubstitutionMap;
 class ExtTheory;
+class TheoryRewriter;
 
 class EntailmentCheckParameters;
 class EntailmentCheckSideEffects;
@@ -79,9 +80,7 @@ namespace eq {
  * all calls to them.)
  */
 class Theory {
-
-private:
-
+ private:
   friend class ::CVC4::TheoryEngine;
 
   // Disallow default construction, copy, assignment.
@@ -140,7 +139,6 @@ private:
 
  protected:
 
-
   // === STATISTICS ===
   /** time spent in check calls */
   TimerStat d_checkTime;
@@ -318,9 +316,9 @@ public:
   virtual ~Theory();
 
   /**
-   * Creates a new theory rewriter for the theory.
+   * @return The theory rewriter associated with this theory.
    */
-  virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0;
+  virtual TheoryRewriter* getTheoryRewriter() = 0;
 
   /**
    * Subclasses of Theory may add additional efforts.  DO NOT CHECK