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

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index a1c04848a..0c46881e7 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -32,18 +32,20 @@ ExtfSolver::ExtfSolver(context::Context* c,
                        SolverState& s,
                        InferenceManager& im,
                        SkolemCache& skc,
+                       StringsRewriter& rewriter,
                        BaseSolver& bs,
                        CoreSolver& cs,
                        ExtTheory* et,
-                       SequencesStatistics& stats)
+                       SequencesStatistics& statistics)
     : d_state(s),
       d_im(im),
       d_skCache(skc),
+      d_rewriter(rewriter),
       d_bsolver(bs),
       d_csolver(cs),
       d_extt(et),
-      d_statistics(stats),
-      d_preproc(&skc, u, stats),
+      d_statistics(statistics),
+      d_preproc(&skc, u, statistics),
       d_hasExtf(c, false),
       d_extfInferCache(c)
 {
@@ -620,7 +622,7 @@ void ExtfSolver::checkExtfInference(Node n,
   if (inferEqr.getKind() == EQUAL)
   {
     // try to use the extended rewriter for equalities
-    inferEqrr = SequencesRewriter::rewriteEqualityExt(inferEqr);
+    inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
   }
   if (inferEqrr != inferEqr)
   {