src/theory/strings/skolem_cache.h

   1 /*********************                                                        */
   2 /*! \file skolem_cache.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 <unordered_set>
  22 #include "expr/node.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace strings {
  27
  28 /**
  29  * A cache of all string skolems generated by the TheoryStrings class. This
  30  * cache is used to ensure that duplicate skolems are not generated when
  31  * possible, and helps identify what skolems were allocated in the current run.
  32  */
  33 class SkolemCache
  34 {
  35  public:
  36   SkolemCache();
  37   /** Identifiers for skolem types
  38    *
  39    * The comments below document the properties of each skolem introduced by
  40    * inference in the strings solver, where by skolem we mean the fresh
  41    * string variable that witnesses each of "exists k".
  42    *
  43    * The skolems with _REV suffixes are used for the reverse version of the
  44    * preconditions below, e.g. where we are considering a' ++ a = b' ++ b.
  45    */
  46   enum SkolemId
  47   {
  48     // a != "" ^ b = "ccccd" ^ a ++ "d" ++ a' = b ++ b' =>
  49     //    exists k. a = "cccc" + k
  50     SK_ID_C_SPT,
  51     SK_ID_C_SPT_REV,
  52     // a != "" ^ b = "c" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' =>
  53     //    exists k. a = "c" ++ k
  54     SK_ID_VC_SPT,
  55     SK_ID_VC_SPT_REV,
  56     // a != "" ^ b = "cccccccc" ^ len(a)!=len(b) a ++ a' = b = b' =>
  57     //    exists k. a = "cccc" ++ k OR ( len(k) > 0 ^ "cccc" = a ++ k )
  58     SK_ID_VC_BIN_SPT,
  59     SK_ID_VC_BIN_SPT_REV,
  60     // a != "" ^ b != "" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' =>
  61     //    exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k )
  62     SK_ID_V_SPT,
  63     SK_ID_V_SPT_REV,
  64     // contains( a, b ) =>
  65     //    exists k_pre, k_post. a = k_pre ++ b ++ k_post
  66     SK_ID_CTN_PRE,
  67     SK_ID_CTN_POST,
  68     // a != ""  ^ b = "c" ^ a ++ a' != b ++ b' =>
  69     //    exists k, k_rem.
  70     //         len( k ) = 1 ^
  71     //         ( ( a = k ++ k_rem ^ k != "c" ) OR ( a = "c" ++ k_rem ) )
  72     SK_ID_DC_SPT,
  73     SK_ID_DC_SPT_REM,
  74     // a != ""  ^ b != "" ^ len( a ) != len( b ) ^ a ++ a' != b ++ b' =>
  75     //    exists k_x k_y k_z.
  76     //         ( len( k_y ) = len( a ) ^ len( k_x ) = len( b ) ^ len( k_z) > 0
  77     //           ( a = k_x ++ k_z OR b = k_y ++ k_z ) )
  78     SK_ID_DEQ_X,
  79     SK_ID_DEQ_Y,
  80     SK_ID_DEQ_Z,
  81   };
  82   /**
  83    * Returns a skolem of type string that is cached for (a,b,id) and has
  84    * name c.
  85    */
  86   Node mkSkolemCached(Node a, Node b, SkolemId id, const char* c);
  87   /** Returns a (uncached) skolem of type string with name c */
  88   Node mkSkolem(const char* c);
  89   /** Returns true if n is a skolem allocated by this class */
  90   bool isSkolem(Node n) const;
  91
  92  private:
  93   /** map from node pairs and identifiers to skolems */
  94   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
  95   /** the set of all skolems we have generated */
  96   std::unordered_set<Node, NodeHashFunction> d_allSkolems;
  97 };
  98
  99 }  // namespace strings
 100 }  // namespace theory
 101 }  // namespace CVC4
 102
 103 #endif /* __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */