1 /********************* */ 2 /*! \file skolem_cache.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Andres Noetzli 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief A cache of skolems for theory of strings. 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H 18 #define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H 19 20 #include <map> 21 #include <tuple> 22 #include <unordered_set> 23 24 #include "expr/node.h" 25 26 namespace CVC4 { 27 namespace theory { 28 namespace strings { 29 30 /** 31 * A cache of all string skolems generated by the TheoryStrings class. This 32 * cache is used to ensure that duplicate skolems are not generated when 33 * possible, and helps identify what skolems were allocated in the current run. 34 */ 35 class SkolemCache 36 { 37 public: 38 SkolemCache(); 39 /** Identifiers for skolem types 40 * 41 * The comments below document the properties of each skolem introduced by 42 * inference in the strings solver, where by skolem we mean the fresh 43 * string variable that witnesses each of "exists k". 44 * 45 * The skolems with _REV suffixes are used for the reverse version of the 46 * preconditions below, e.g. where we are considering a' ++ a = b' ++ b. 47 * 48 * All skolems assume a and b are strings unless otherwise stated. 49 */ 50 enum SkolemId 51 { 52 // exists k. k = a 53 SK_PURIFY, 54 // a != "" ^ b = "ccccd" ^ a ++ "d" ++ a' = b ++ b' => 55 // exists k. a = "cccc" + k 56 SK_ID_C_SPT, 57 SK_ID_C_SPT_REV, 58 // a != "" ^ b = "c" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' => 59 // exists k. a = "c" ++ k 60 SK_ID_VC_SPT, 61 SK_ID_VC_SPT_REV, 62 // a != "" ^ b = "cccccccc" ^ len(a)!=len(b) a ++ a' = b = b' => 63 // exists k. a = "cccc" ++ k OR ( len(k) > 0 ^ "cccc" = a ++ k ) 64 SK_ID_VC_BIN_SPT, 65 SK_ID_VC_BIN_SPT_REV, 66 // a != "" ^ b != "" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' => 67 // exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k ) 68 SK_ID_V_SPT, 69 SK_ID_V_SPT_REV, 70 // a != "" ^ b = "c" ^ a ++ a' != b ++ b' => 71 // exists k, k_rem. 72 // len( k ) = 1 ^ 73 // ( ( a = k ++ k_rem ^ k != "c" ) OR ( a = "c" ++ k_rem ) ) 74 SK_ID_DC_SPT, 75 SK_ID_DC_SPT_REM, 76 // a != "" ^ b != "" ^ len( a ) != len( b ) ^ a ++ a' != b ++ b' => 77 // exists k_x k_y k_z. 78 // ( len( k_y ) = len( a ) ^ len( k_x ) = len( b ) ^ len( k_z) > 0 79 // ( a = k_x ++ k_z OR b = k_y ++ k_z ) ) 80 SK_ID_DEQ_X, 81 SK_ID_DEQ_Y, 82 SK_ID_DEQ_Z, 83 // contains( a, b ) => 84 // exists k_pre, k_post. a = k_pre ++ b ++ k_post ^ 85 // ~contains(k_pre ++ substr( b, 0, len(b)-1 ), b) 86 // 87 // As an optimization, these skolems are reused for positive occurrences of 88 // contains, where they have the semantics: 89 // 90 // contains( a, b ) => 91 // exists k_pre, k_post. a = k_pre ++ b ++ k_post 92 // 93 // We reuse them since it is sound to consider w.l.o.g. the first occurrence 94 // of b in a as the witness for contains( a, b ). 95 SK_FIRST_CTN_PRE, 96 SK_FIRST_CTN_POST, 97 // For integer b, 98 // len( a ) > b => 99 // exists k. a = k ++ a' ^ len( k ) = b 100 SK_PREFIX, 101 // For integer b, 102 // b > 0 => 103 // exists k. a = a' ++ k ^ len( k ) = ite( len(a)>b, len(a)-b, 0 ) 104 SK_SUFFIX_REM, 105 // --------------- integer skolems 106 // exists k. ( b occurs k times in a ) 107 SK_NUM_OCCUR, 108 // --------------- function skolems 109 // For function k: Int -> Int 110 // exists k. 111 // forall 0 <= x <= n, 112 // k(x) is the end index of the x^th occurrence of b in a 113 // where n is the number of occurrences of b in a, and k(0)=0. 114 SK_OCCUR_INDEX, 115 }; 116 /** 117 * Returns a skolem of type string that is cached for (a,b,id) and has 118 * name c. 119 */ 120 Node mkSkolemCached(Node a, Node b, SkolemId id, const char* c); 121 /** 122 * Returns a skolem of type string that is cached for (a,[null],id) and has 123 * name c. 124 */ 125 Node mkSkolemCached(Node a, SkolemId id, const char* c); 126 /** Same as above, but the skolem to construct has a custom type tn */ 127 Node mkTypedSkolemCached( 128 TypeNode tn, Node a, Node b, SkolemId id, const char* c); 129 /** Same as mkTypedSkolemCached above for (a,[null],id) */ 130 Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); 131 /** Returns a (uncached) skolem of type string with name c */ 132 Node mkSkolem(const char* c); 133 /** Same as above, but for custom type tn */ 134 Node mkTypedSkolem(TypeNode tn, const char* c); 135 /** Returns true if n is a skolem allocated by this class */ 136 bool isSkolem(Node n) const; 137 138 private: 139 /** 140 * Simplifies the arguments for a string skolem used for indexing into the 141 * cache. In certain cases, we can share skolems with similar arguments e.g. 142 * SK_FIRST_CTN(a, c) can be used instead of SK_FIRST_CTN((str.substr a 0 n), 143 * c) because the first occurrence of "c" in "(str.substr a 0 n)" is also the 144 * first occurrence of "c" in "a" (assuming that "c" appears in both and 145 * otherwise the value of SK_FIRST_CTN does not matter). 146 * 147 * @param id The type of skolem 148 * @param a The first argument used for indexing 149 * @param b The second argument used for indexing 150 * @return A tuple with the new skolem id, the new first, and the new second 151 * argument 152 */ 153 std::tuple<SkolemId, Node, Node> normalizeStringSkolem(SkolemId id, 154 Node a, 155 Node b); 156 157 /** string type */ 158 TypeNode d_strType; 159 /** Constant node zero */ 160 Node d_zero; 161 /** map from node pairs and identifiers to skolems */ 162 std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; 163 /** the set of all skolems we have generated */ 164 std::unordered_set<Node, NodeHashFunction> d_allSkolems; 165 }; 166 167 } // namespace strings 168 } // namespace theory 169 } // namespace CVC4 170 171 #endif /* __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ 172