src/theory/strings/skolem_cache.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Yoni Zohar
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Implementation of a cache of skolems for theory of strings.
  14  */
  15
  16 #include "theory/strings/skolem_cache.h"
  17
  18 #include "expr/attribute.h"
  19 #include "expr/bound_var_manager.h"
  20 #include "expr/skolem_manager.h"
  21 #include "theory/rewriter.h"
  22 #include "theory/strings/arith_entail.h"
  23 #include "theory/strings/theory_strings_utils.h"
  24 #include "theory/strings/word.h"
  25 #include "util/rational.h"
  26
  27 using namespace cvc5::kind;
  28
  29 namespace cvc5 {
  30 namespace theory {
  31 namespace strings {
  32
  33 /**
  34  * A bound variable corresponding to the universally quantified integer
  35  * variable used to range over the valid positions in a string, used
  36  * for axiomatizing the behavior of some term.
  37  */
  38 struct IndexVarAttributeId
  39 {
  40 };
  41 typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute;
  42
  43 /**
  44  * A bound variable corresponding to the universally quantified integer
  45  * variable used to range over the valid lengths of a string, used for
  46  * axiomatizing the behavior of some term.
  47  */
  48 struct LengthVarAttributeId
  49 {
  50 };
  51 typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute;
  52
  53 SkolemCache::SkolemCache(bool useOpts) : d_useOpts(useOpts)
  54 {
  55   NodeManager* nm = NodeManager::currentNM();
  56   d_strType = nm->stringType();
  57   d_zero = nm->mkConst(Rational(0));
  58 }
  59
  60 Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
  61 {
  62   return mkTypedSkolemCached(d_strType, a, b, id, c);
  63 }
  64
  65 Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
  66 {
  67   return mkSkolemCached(a, Node::null(), id, c);
  68 }
  69
  70 Node SkolemCache::mkTypedSkolemCached(
  71     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
  72 {
  73   Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
  74                         << ", " << b << ")" << std::endl;
  75   SkolemId idOrig = id;
  76   // do not rewrite beforehand if we are not using optimizations, this is so
  77   // that the proof checker does not depend on the rewriter.
  78   if (d_useOpts)
  79   {
  80     a = a.isNull() ? a : Rewriter::rewrite(a);
  81     b = b.isNull() ? b : Rewriter::rewrite(b);
  82   }
  83   std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
  84
  85   // optimization: if we aren't asking for the purification skolem for constant
  86   // a, and the skolem is equivalent to a, then we just return a.
  87   if (d_useOpts && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
  88   {
  89     Trace("skolem-cache") << "...optimization: return constant " << a
  90                           << std::endl;
  91     return a;
  92   }
  93
  94   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
  95   if (it != d_skolemCache[a][b].end())
  96   {
  97     Trace("skolem-cache") << "...return existing " << it->second << std::endl;
  98     // already cached
  99     return it->second;
 100   }
 101
 102   NodeManager* nm = NodeManager::currentNM();
 103   SkolemManager* sm = nm->getSkolemManager();
 104   Node sk;
 105   switch (id)
 106   {
 107     // exists k. k = a
 108     case SK_PURIFY:
 109     {
 110       // for sequences of Booleans, we may purify Boolean terms, in which case
 111       // they must be Boolean term variables.
 112       int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR
 113                                           : NodeManager::SKOLEM_DEFAULT;
 114       sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
 115     }
 116     break;
 117     // these are eliminated by normalizeStringSkolem
 118     case SK_ID_V_SPT:
 119     case SK_ID_V_SPT_REV:
 120     case SK_ID_VC_SPT:
 121     case SK_ID_VC_SPT_REV:
 122     case SK_FIRST_CTN_POST:
 123     case SK_ID_C_SPT:
 124     case SK_ID_C_SPT_REV:
 125     case SK_ID_DC_SPT:
 126     case SK_ID_DC_SPT_REM:
 127     case SK_ID_DEQ_X:
 128     case SK_ID_DEQ_Y:
 129     case SK_FIRST_CTN_PRE:
 130     case SK_PREFIX:
 131     case SK_SUFFIX_REM:
 132       Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
 133       break;
 134     case SK_NUM_OCCUR:
 135     case SK_OCCUR_INDEX:
 136     default:
 137     {
 138       Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
 139       Node v = nm->mkBoundVar(tn);
 140       Node cond = nm->mkConst(true);
 141       sk = sm->mkSkolem(v, cond, c, "string skolem");
 142     }
 143     break;
 144   }
 145   Trace("skolem-cache") << "...returned " << sk << std::endl;
 146   d_allSkolems.insert(sk);
 147   d_skolemCache[a][b][id] = sk;
 148   return sk;
 149 }
 150 Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 151                                       Node a,
 152                                       SkolemId id,
 153                                       const char* c)
 154 {
 155   return mkTypedSkolemCached(tn, a, Node::null(), id, c);
 156 }
 157
 158 Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
 159 {
 160   // Note this method is static and does not rely on any local caching.
 161   // It is used by expand definitions and by (dynamic) reductions, thus
 162   // it is centrally located here.
 163   Assert(seqType.isSequence());
 164   NodeManager* nm = NodeManager::currentNM();
 165   SkolemManager* sm = nm->getSkolemManager();
 166   std::vector<TypeNode> argTypes;
 167   argTypes.push_back(seqType);
 168   argTypes.push_back(nm->integerType());
 169   TypeNode elemType = seqType.getSequenceElementType();
 170   TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
 171   return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
 172 }
 173
 174 Node SkolemCache::mkSkolem(const char* c)
 175 {
 176   // TODO: eliminate this
 177   SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
 178   Node n = sm->mkDummySkolem(c, d_strType, "string skolem");
 179   d_allSkolems.insert(n);
 180   return n;
 181 }
 182
 183 bool SkolemCache::isSkolem(Node n) const
 184 {
 185   return d_allSkolems.find(n) != d_allSkolems.end();
 186 }
 187
 188 std::tuple<SkolemCache::SkolemId, Node, Node>
 189 SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 190 {
 191
 192   NodeManager* nm = NodeManager::currentNM();
 193
 194   // eliminate in terms of prefix/suffix_rem
 195   if (id == SK_FIRST_CTN_POST)
 196   {
 197     // SK_FIRST_CTN_POST(x, y) --->
 198     //   SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
 199     id = SK_SUFFIX_REM;
 200     Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
 201     b = nm->mkNode(
 202         PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
 203   }
 204   else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
 205   {
 206     // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
 207     id = SK_SUFFIX_REM;
 208     b = nm->mkNode(STRING_LENGTH, b);
 209   }
 210   else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
 211   {
 212     // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
 213     id = SK_PREFIX;
 214     b = nm->mkNode(
 215         MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
 216   }
 217   else if (id == SK_ID_VC_SPT)
 218   {
 219     // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
 220     id = SK_SUFFIX_REM;
 221     b = nm->mkConst(Rational(1));
 222   }
 223   else if (id == SK_ID_VC_SPT_REV)
 224   {
 225     // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
 226     id = SK_PREFIX;
 227     b = nm->mkNode(
 228         MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
 229   }
 230   else if (id == SK_ID_DC_SPT)
 231   {
 232     // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
 233     id = SK_PREFIX;
 234     b = nm->mkConst(Rational(1));
 235   }
 236   else if (id == SK_ID_DC_SPT_REM)
 237   {
 238     // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
 239     id = SK_SUFFIX_REM;
 240     b = nm->mkConst(Rational(1));
 241   }
 242   else if (id == SK_ID_DEQ_X)
 243   {
 244     // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
 245     id = SK_PREFIX;
 246     Node aOld = a;
 247     a = b;
 248     b = nm->mkNode(STRING_LENGTH, aOld);
 249   }
 250   else if (id == SK_ID_DEQ_Y)
 251   {
 252     // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
 253     id = SK_PREFIX;
 254     b = nm->mkNode(STRING_LENGTH, b);
 255   }
 256   else if (id == SK_FIRST_CTN_PRE)
 257   {
 258     // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
 259     id = SK_PREFIX;
 260     b = nm->mkNode(STRING_INDEXOF, a, b, d_zero);
 261   }
 262
 263   if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
 264   {
 265     bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
 266     Node la = nm->mkNode(STRING_LENGTH, a);
 267     Node lb = nm->mkNode(STRING_LENGTH, b);
 268     Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
 269                     : utils::mkSuffix(a, lb);
 270     Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
 271                     : utils::mkSuffix(b, la);
 272     id = SK_PURIFY;
 273     // SK_ID_V_UNIFIED_SPT(x,y) --->
 274     //   ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
 275     a = nm->mkNode(ITE, nm->mkNode(GEQ, la, lb), ta, tb);
 276     b = Node::null();
 277   }
 278
 279   // now, eliminate prefix/suffix_rem in terms of purify
 280   if (id == SK_PREFIX)
 281   {
 282     // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
 283     id = SK_PURIFY;
 284     a = utils::mkPrefix(a, b);
 285     b = Node::null();
 286   }
 287   else if (id == SK_SUFFIX_REM)
 288   {
 289     // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
 290     id = SK_PURIFY;
 291     a = utils::mkSuffix(a, b);
 292     b = Node::null();
 293   }
 294
 295   if (d_useOpts)
 296   {
 297     a = a.isNull() ? a : Rewriter::rewrite(a);
 298     b = b.isNull() ? b : Rewriter::rewrite(b);
 299   }
 300   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
 301                         << ", " << b << ")" << std::endl;
 302   return std::make_tuple(id, a, b);
 303 }
 304
 305 Node SkolemCache::mkIndexVar(Node t)
 306 {
 307   NodeManager* nm = NodeManager::currentNM();
 308   TypeNode intType = nm->integerType();
 309   BoundVarManager* bvm = nm->getBoundVarManager();
 310   return bvm->mkBoundVar<IndexVarAttribute>(t, intType);
 311 }
 312
 313 Node SkolemCache::mkLengthVar(Node t)
 314 {
 315   NodeManager* nm = NodeManager::currentNM();
 316   TypeNode intType = nm->integerType();
 317   BoundVarManager* bvm = nm->getBoundVarManager();
 318   return bvm->mkBoundVar<LengthVarAttribute>(t, intType);
 319 }
 320
 321 }  // namespace strings
 322 }  // namespace theory
 323 }  // namespace cvc5