diff options
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
-rw-r--r-- | src/theory/strings/skolem_cache.h | 22 |
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 */ |