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.

3 files changed, 10 insertions, 8 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 8df5a8535..b9d05b833 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -36,11 +36,6 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c,
 {
 }
 
-std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter()
-{
-  return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter());
-}
-
 std::string TheoryBuiltin::identify() const
 {
   return std::string("TheoryBuiltin");
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index d240f4f63..bf99003ec 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -19,6 +19,7 @@
 #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
 #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
 
+#include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
@@ -34,12 +35,16 @@ class TheoryBuiltin : public Theory
                 Valuation valuation,
                 const LogicInfo& logicInfo);
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   std::string identify() const override;
 
   /** finish initialization */
   void finishInit() override;
+
+ private:
+  /** The theory rewriter for this theory. */
+  TheoryBuiltinRewriter d_rewriter;
 }; /* class TheoryBuiltin */
 
 }  // namespace builtin
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index a39d4231b..dd6d434ca 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -84,8 +84,10 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
         Assert(retNode.getType() == node.getType());
         Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
         return RewriteResponse(REWRITE_DONE, retNode);
-      } 
-    }else{
+      }
+    }
+    else
+    {
       Trace("builtin-rewrite-debug") << "...failed to get array representation." << std::endl;
     }
     return RewriteResponse(REWRITE_DONE, node);