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.

2 files changed, 14 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2e1716543..03d9409be 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -802,6 +802,7 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_theoryEngine(nullptr),
       d_propEngine(nullptr),
       d_proofManager(nullptr),
+      d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_fmfRecFunctionsDefined(nullptr),
       d_assertionList(nullptr),
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 37b89cfb7..3f24c8bab 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -108,6 +108,7 @@ namespace smt {
 
 namespace theory {
   class TheoryModel;
+  class Rewriter;
 }/* CVC4::theory namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -134,6 +135,7 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::Model;  // to access d_modelCommands
   friend class ::CVC4::theory::TheoryModel;
+  friend class ::CVC4::theory::Rewriter;
 
   /* .......................................................................  */
  public:
@@ -876,6 +878,9 @@ class CVC4_PUBLIC SmtEngine
   /** Get a pointer to the ProofManager owned by this SmtEngine. */
   ProofManager* getProofManager() { return d_proofManager.get(); };
 
+  /** Get a pointer to the Rewriter owned by this SmtEngine. */
+  theory::Rewriter* getRewriter() { return d_rewriter.get(); }
+
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
   StatisticsRegistry* getStatisticsRegistry()
   {
@@ -1085,6 +1090,14 @@ class CVC4_PUBLIC SmtEngine
   /** The proof manager */
   std::unique_ptr<ProofManager> d_proofManager;
 
+  /**
+   * The rewriter associated with this SmtEngine. We have a different instance
+   * of the rewriter for each SmtEngine instance. This is because rewriters may
+   * hold references to objects that belong to theory solvers, which are
+   * specific to an SmtEngine/TheoryEngine instance.
+   */
+  std::unique_ptr<theory::Rewriter> d_rewriter;
+
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;