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