GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/skolem_cache.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
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-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.\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
8992
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 */