Improve skolem caching by normalizing skolem args (#2723)

In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index d0eabd4c2..a6e91a246 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -18,7 +18,9 @@
 #define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
 
 #include <map>
+#include <tuple>
 #include <unordered_set>
+
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -134,8 +136,28 @@ class SkolemCache
   bool isSkolem(Node n) const;
 
  private:
+  /**
+   * Simplifies the arguments for a string skolem used for indexing into the
+   * cache. In certain cases, we can share skolems with similar arguments e.g.
+   * SK_FIRST_CTN(a, c) can be used instead of SK_FIRST_CTN((str.substr a 0 n),
+   * c) because the first occurrence of "c" in "(str.substr a 0 n)" is also the
+   * first occurrence of "c" in "a" (assuming that "c" appears in both and
+   * otherwise the value of SK_FIRST_CTN does not matter).
+   *
+   * @param id The type of skolem
+   * @param a The first argument used for indexing
+   * @param b The second argument used for indexing
+   * @return A tuple with the new skolem id, the new first, and the new second
+   * argument
+   */
+  std::tuple<SkolemId, Node, Node> normalizeStringSkolem(SkolemId id,
+                                                         Node a,
+                                                         Node b);
+
   /** string type */
   TypeNode d_strType;
+  /** Constant node zero */
+  Node d_zero;
   /** map from node pairs and identifiers to skolems */
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */