src/theory/sets/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-2020 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 sets.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H
  18 #define CVC4__THEORY__SETS__SKOLEM_CACHE_H
  19
  20 #include <map>
  21 #include <unordered_set>
  22
  23 #include "expr/node.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace sets {
  28
  29 /**
  30  * A cache of all set skolems generated by the TheorySets class. This
  31  * cache is used to ensure that duplicate skolems are not generated when
  32  * possible, and helps identify what skolems were allocated in the current run.
  33  */
  34 class SkolemCache
  35 {
  36  public:
  37   SkolemCache();
  38   /** Identifiers for skolem types
  39    *
  40    * The comments below document the properties of each skolem introduced by
  41    * inference in the sets solver, where by skolem we mean the fresh
  42    * set variable that witnesses each of "exists k".
  43    */
  44   enum SkolemId
  45   {
  46     // exists k. k = a
  47     SK_PURIFY,
  48     // a != b => exists k. ( k in a != k in b )
  49     SK_DISEQUAL,
  50     // a in tclosure(b) => exists k1 k2. ( a.1, k1 ) in b ^ ( k2, a.2 ) in b ^
  51     //                                   ( k1 = k2 V ( k1, k2 ) in tclosure(b) )
  52     SK_TCLOSURE_DOWN1,
  53     SK_TCLOSURE_DOWN2,
  54     // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B
  55     // This is cached by the nodes corresponding to (a,b) and join(A,B).
  56     SK_JOIN,
  57   };
  58
  59   /**
  60    * Makes a skolem of type tn that is cached based on the key (a,b,id).
  61    * Argument c is the variable name of the skolem.
  62    */
  63   Node mkTypedSkolemCached(
  64       TypeNode tn, Node a, Node b, SkolemId id, const char* c);
  65   /** same as above, cached based on key (a,null,id) */
  66   Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
  67   /** Same as above, but without caching. */
  68   Node mkTypedSkolem(TypeNode tn, const char* c);
  69   /** Returns true if n is a skolem allocated by this class */
  70   bool isSkolem(Node n) const;
  71
  72  private:
  73   /** map from node pairs and identifiers to skolems */
  74   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
  75   /** the set of all skolems we have generated */
  76   std::unordered_set<Node, NodeHashFunction> d_allSkolems;
  77 };
  78
  79 }  // namespace sets
  80 }  // namespace theory
  81 }  // namespace CVC4
  82
  83 #endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */