Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Kshitij Bansal, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Skolem manager utility.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__EXPR__SKOLEM_MANAGER_H
19 : : #define CVC5__EXPR__SKOLEM_MANAGER_H
20 : :
21 : : #include <cvc5/cvc5_skolem_id.h>
22 : :
23 : : #include <string>
24 : :
25 : : #include "expr/internal_skolem_id.h"
26 : : #include "expr/node.h"
27 : :
28 : : namespace cvc5::internal {
29 : :
30 : : class ProofGenerator;
31 : :
32 : : /**
33 : : * A manager for skolems that can be used in proofs. This is designed to be
34 : : * a trusted interface for constructing variables of SKOLEM type, where one
35 : : * must provide information that characterizes the skolem. This information
36 : : * may either be:
37 : : * (1) the term that the skolem purifies (`mkPurifySkolem`)
38 : : * (2) an identifier (`mkSkolemFunction`) and a set of "cache values", which
39 : : * can be seen as arguments to the skolem function. These are typically used for
40 : : * implementing theory-specific inferences that introduce symbols that
41 : : * are not interpreted by the theory (see SkolemId enum).
42 : : *
43 : : * Note that (1) is a special instance of (2), where the purification skolem
44 : : * for t is equivalent to calling mkSkolemFunction on SkolemId::PURIFY
45 : : * and t.
46 : : *
47 : : * If a variable cannot be associated with any of the above information,
48 : : * the method `mkDummySkolem` may be used, which always constructs a fresh
49 : : * skolem variable.
50 : : *
51 : : * It is implemented by mapping terms to an attribute corresponding to their
52 : : * "original form" as described below. Hence, this class does not impact the
53 : : * reference counting of skolem variables which may be deleted if they are not
54 : : * used.
55 : : *
56 : : * To handle purification of witness terms, notice that the purification
57 : : * skolem for (witness ((x T)) P) is equivalent to the skolem function:
58 : : * (QUANTIFIERS_SKOLEMIZE (exists ((x T)) P) 0)
59 : : * In other words, the purification for witness terms are equivalent to
60 : : * the skolemization of their corresponding existential. This is currently only
61 : : * used for eliminating witness terms coming from algorithms that introduce
62 : : * them, e.g. BV/set instantiation. Unifying these two skolems is required
63 : : * for ensuring proof checking succeeds for term formula removal on witness
64 : : * terms.
65 : : *
66 : : * The use of purification skolems and skolem functions avoid having to reason
67 : : * about witness terms. This avoids several complications. In particular,
68 : : * witness terms in most contexts should be seen as black boxes, converting
69 : : * something to a witness term may have unintended consequences e.g. variable
70 : : * shadowing. In contrast, converting to original form does not have these
71 : : * complications. Furthermore, having original form greatly simplifies
72 : : * reasoning in the proof in certain external proof formats, in particular, it
73 : : * avoids the need to reason about identifiers for introduced variables for
74 : : * the binders of witness terms.
75 : : */
76 : : class SkolemManager
77 : : {
78 : : public:
79 : : SkolemManager(NodeManager* nm);
80 : 72382 : ~SkolemManager() {}
81 : : /**
82 : : * Make purification skolem. This skolem is unique for each t, which we
83 : : * implement via an attribute on t. This attribute is used to ensure to
84 : : * associate a unique skolem for each t.
85 : : *
86 : : * Notice that a purification skolem is trivial to justify (via
87 : : * SKOLEM_INTRO), and hence it does not require a proof generator.
88 : : *
89 : : * Notice that we do not convert t to original form in this call. Thus,
90 : : * in very rare cases, two Skolems may be introduced that have the same
91 : : * original form. For example, let k be the skolem introduced to eliminate
92 : : * (ite A B C). Then, asking for the purify skolem for:
93 : : * (ite (ite A B C) D E) and (ite k D E)
94 : : * will return two different Skolems.
95 : : *
96 : : * @param t The term to purify
97 : : * @return The purification skolem for t
98 : : */
99 : : static Node mkPurifySkolem(Node t);
100 : : /**
101 : : * Make skolem function. This method should be used for creating fixed
102 : : * skolem functions of the forms described in SkolemId. The user of this
103 : : * method is responsible for providing a proper type for the identifier that
104 : : * matches the description of id.
105 : : * This can be done from the function
106 : : * `SkolemManager::getTypeFor`.
107 : : * Skolem functions are useful for modelling
108 : : * the behavior of partial functions, or for theory-specific inferences that
109 : : * introduce fresh variables.
110 : : *
111 : : * A skolem function is not given a formal semantics in terms of a witness
112 : : * term, nor is it a purification skolem, thus it does not fall into the two
113 : : * categories of skolems above. This method is motivated by convenience, as
114 : : * the user of this method does not require constructing canonical variables
115 : : * for witness terms.
116 : : *
117 : : * The returned skolem is an ordinary skolem variable that can be used
118 : : * e.g. in APPLY_UF terms when tn is a function type.
119 : : *
120 : : * Notice that we do not insist that tn is a function type. A user of this
121 : : * method may construct a canonical (first-order) skolem using this method
122 : : * as well.
123 : : *
124 : : * @param id The identifier of the skolem function
125 : : * @param cacheVal A cache value. The returned skolem function will be
126 : : * unique to the pair (id, cacheVal). This value is required, for instance,
127 : : * for skolem functions that are in fact families of skolem functions,
128 : : * e.g. the wrongly applied case of selectors.
129 : : * @return The skolem function.
130 : : */
131 : : Node mkSkolemFunction(SkolemId id, Node cacheVal = Node::null());
132 : : /**
133 : : * Same as above, with multiple cache values.
134 : : * @param id The identifier of the skolem function
135 : : * @param cacheVals A vector of cache values.
136 : : * @return The skolem function.
137 : : */
138 : : Node mkSkolemFunction(SkolemId id,
139 : : const std::vector<Node>& cacheVals);
140 : : /**
141 : : * Same as above, with multiple cache values and an internal skolem id.
142 : : * This will call mkSkolemFunction where the (external) id is
143 : : * SkolemId::INTERNAL. The type is provided explicitly.
144 : : */
145 : : Node mkInternalSkolemFunction(InternalSkolemId id,
146 : : TypeNode tn,
147 : : const std::vector<Node>& cacheVals = {});
148 : : /**
149 : : * Is k a skolem function? Returns true if k was generated by the above
150 : : * call.
151 : : */
152 : : static bool isSkolemFunction(TNode k);
153 : : /**
154 : : * Is k a skolem function? Returns true if k was generated by the above
155 : : * call. Updates the arguments to the values used when constructing it.
156 : : */
157 : : static bool isSkolemFunction(TNode k, SkolemId& id, Node& cacheVal);
158 : : /**
159 : : * @param k The skolem.
160 : : * @return skolem function id for k.
161 : : */
162 : : SkolemId getId(TNode k) const;
163 : : /**
164 : : * @param k The skolem.
165 : : * @return The list of skolem indices for k.
166 : : */
167 : : std::vector<Node> getIndices(TNode k) const;
168 : : /**
169 : : * @param k The skolem.
170 : : * @return the internal skolem function id, for skolem k whose id is
171 : : * SkolemId::INTERNAL.
172 : : */
173 : : InternalSkolemId getInternalId(TNode k) const;
174 : : /**
175 : : * Create a skolem constant with the given name, type, and comment. This
176 : : * should only be used if the definition of the skolem does not matter.
177 : : * The definition of a skolem matters e.g. when the skolem is used in a
178 : : * proof.
179 : : *
180 : : * @param prefix the name of the new skolem variable is the prefix
181 : : * appended with a unique ID. This way a family of skolem variables
182 : : * can be made with unique identifiers, used in dump, tracing, and
183 : : * debugging output. Use SKOLEM_EXACT_NAME flag if you don't want
184 : : * a unique ID appended and use prefix as the name.
185 : : * @param type the type of the skolem variable to create
186 : : * @param flags an optional mask of bits from SkolemFlags to control
187 : : * skolem behavior
188 : : */
189 : : Node mkDummySkolem(const std::string& prefix,
190 : : const TypeNode& type,
191 : : SkolemFlags flags = SkolemFlags::SKOLEM_DEFAULT);
192 : : /** Returns true if n is a skolem that stands for an abstract value */
193 : : bool isAbstractValue(TNode n) const;
194 : : /**
195 : : * Convert to original form, which recursively replaces all skolems terms in
196 : : * n by the term they purify.
197 : : *
198 : : * @param n The term or formula to convert to original form described above
199 : : * @return n in original form.
200 : : */
201 : : static Node getOriginalForm(Node n);
202 : : /**
203 : : * Convert to unpurified form, which returns the term that k purifies. This
204 : : * is literally the term that was passed as an argument to mkPurify on the
205 : : * call that created k. In contrast to getOriginalForm, this is not
206 : : * recursive w.r.t. skolems, so that the term purified by k may itself
207 : : * contain purification skolems that are not expanded.
208 : : *
209 : : * @param k The skolem to convert to unpurified form
210 : : * @return the unpurified form of k.
211 : : */
212 : : static Node getUnpurifiedForm(Node k);
213 : : /**
214 : : * Get the number of indices for a skolem id.
215 : : * @param id The skolem id.
216 : : * @return The number of indices for the skolem id.
217 : : */
218 : : size_t getNumIndicesForSkolemId(SkolemId id) const;
219 : : /**
220 : : * Is the given skolem identifier commutative, in the sense that its
221 : : * arguments can be reordered? If this method returns true, then
222 : : * we sort the arguments to the skolem upon construction via the API.
223 : : */
224 : : static bool isCommutativeSkolemId(SkolemId id);
225 : : private:
226 : : /** The associated node manager. */
227 : : NodeManager* d_nm;
228 : : /** Cache of skolem functions for mkSkolemFunction above. */
229 : : std::map<std::tuple<SkolemId, TypeNode, Node>, Node> d_skolemFuns;
230 : : /** Backwards mapping of above */
231 : : std::map<Node, std::tuple<SkolemId, TypeNode, Node>> d_skolemFunMap;
232 : :
233 : : /**
234 : : * A counter used to produce unique skolem names.
235 : : *
236 : : * Note that it is NOT incremented when skolems are created using
237 : : * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
238 : : * by this node manager.
239 : : */
240 : : size_t d_skolemCounter;
241 : : /** Same as mkSkolemFunction, with explicit type */
242 : : Node mkSkolemFunctionTyped(SkolemId id,
243 : : TypeNode tn,
244 : : Node cacheVal = Node::null());
245 : : /** Same as above, with multiple cache values and explicit Type */
246 : : Node mkSkolemFunctionTyped(SkolemId id,
247 : : TypeNode tn,
248 : : const std::vector<Node>& cacheVals);
249 : : /**
250 : : * Create a skolem constant with the given name, type, and comment.
251 : : *
252 : : * This method is intentionally private. To create skolems, one should
253 : : * call a public method from SkolemManager for allocating a skolem in a
254 : : * proper way, or otherwise use SkolemManager::mkDummySkolem.
255 : : */
256 : : Node mkSkolemNode(Kind k,
257 : : const std::string& prefix,
258 : : const TypeNode& type,
259 : : SkolemFlags flags = SkolemFlags::SKOLEM_DEFAULT);
260 : : /** Get type for skolem */
261 : : TypeNode getTypeFor(SkolemId id, const std::vector<Node>& cacheVals);
262 : : };
263 : :
264 : : } // namespace cvc5::internal
265 : :
266 : : #endif /* CVC5__EXPR__PROOF_SKOLEM_CACHE_H */
|
