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, 25 insertions, 31 deletions

diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index 4cc679ca8..7e45296a9 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -14,6 +14,12 @@
  ** Unit tests for the strings/sequences rewriter.
  **/
 
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine.h"
@@ -23,11 +29,7 @@
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
-
-#include <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
+#include "theory/strings/strings_rewriter.h"
 
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -246,7 +248,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
 
     // (str.substr "A" x x) --> ""
     Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x);
-    Node res = SequencesRewriter::rewriteSubstr(n);
+    Node res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, empty);
 
     // (str.substr "A" (+ x 1) x) -> ""
@@ -254,7 +256,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
                      a,
                      d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))),
                      x);
-    res = SequencesRewriter::rewriteSubstr(n);
+    res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, empty);
 
     // (str.substr "A" (+ x (str.len s2)) x) -> ""
@@ -263,24 +265,24 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
         a,
         d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)),
         x);
-    res = SequencesRewriter::rewriteSubstr(n);
+    res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, empty);
 
     // (str.substr "A" x y) -> (str.substr "A" x y)
     n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y);
-    res = SequencesRewriter::rewriteSubstr(n);
+    res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, n);
 
     // (str.substr "ABCD" (+ x 3) x) -> ""
     n = d_nm->mkNode(
         kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x);
-    res = SequencesRewriter::rewriteSubstr(n);
+    res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, empty);
 
     // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
     n = d_nm->mkNode(
         kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x);
-    res = SequencesRewriter::rewriteSubstr(n);
+    res = StringsRewriter(nullptr).rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, n);
 
     // (str.substr (str.substr s x x) x x) -> ""
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 4a019ac08..992251f16 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -113,18 +113,6 @@ class FakeTheoryRewriter : public TheoryRewriter
 template <TheoryId theoryId>
 class FakeTheory : public Theory
 {
-  /**
-   * This fake theory class is equally useful for bool, uf, arith, etc.  It
-   * keeps an identifier to identify itself.
-   */
-  std::string d_id;
-
-  /**
-   * The expected sequence of rewrite calls.  Filled by FakeTheory::expect() and
-   * consumed by FakeTheory::preRewrite() and FakeTheory::postRewrite().
-   */
-  // static std::deque<RewriteItem> s_expected;
-
  public:
   FakeTheory(context::Context* ctxt,
              context::UserContext* uctxt,
@@ -135,10 +123,7 @@ class FakeTheory : public Theory
   {
   }
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override
-  {
-    return std::unique_ptr<TheoryRewriter>(new FakeTheoryRewriter());
-  }
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   /** Register an expected rewrite call */
   static void expect(RewriteType type,
@@ -176,6 +161,16 @@ class FakeTheory : public Theory
     return Node::null();
   }
   Node getValue(TNode n) { return Node::null(); }
+
+ private:
+  /**
+   * This fake theory class is equally useful for bool, uf, arith, etc.  It
+   * keeps an identifier to identify itself.
+   */
+  std::string d_id;
+
+  /** The theory rewriter for this theory. */
+  FakeTheoryRewriter d_rewriter;
 }; /* class FakeTheory */
 
 /* definition of the s_expected static field in FakeTheory; see above */
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index eb43e00cb..0d5238aa9 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -102,10 +102,7 @@ class DummyTheory : public Theory {
       : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
   {}
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter()
-  {
-    return std::unique_ptr<TheoryRewriter>();
-  }
+  TheoryRewriter* getTheoryRewriter() { return nullptr; }
 
   void registerTerm(TNode n) {
     // check that we registerTerm() a term only once