1 /********************* */
2 /*! \file skolem_cache.h
4 ** Top contributors (to current version):
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
12 ** \brief A cache of skolems for theory of sets.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H
18 #define CVC4__THEORY__SETS__SKOLEM_CACHE_H
21 #include <unordered_set>
23 #include "expr/node.h"
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.
38 /** Identifiers for skolem types
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".
48 // a != b => exists k. ( k in a != k in b )
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) )
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).
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.
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;
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
;
83 #endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */