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 : : * Attributes for the theory quantifiers.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
16 : : #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
17 : :
18 : : #include "context/cdhashset.h"
19 : : #include "expr/attribute.h"
20 : : #include "expr/node.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : :
25 : : /** Attribute true for function definition quantifiers */
26 : : struct FunDefAttributeId
27 : : {
28 : : };
29 : : typedef expr::Attribute<FunDefAttributeId, bool> FunDefAttribute;
30 : :
31 : : /** Attribute true for quantifiers that we are doing partial quantifier
32 : : * elimination on */
33 : : struct QuantElimPartialAttributeId
34 : : {
35 : : };
36 : : typedef expr::Attribute<QuantElimPartialAttributeId, bool>
37 : : QuantElimPartialAttribute;
38 : :
39 : : /** Attribute true for quantifiers that are SyGus conjectures */
40 : : struct SygusAttributeId
41 : : {
42 : : };
43 : : typedef expr::Attribute<SygusAttributeId, bool> SygusAttribute;
44 : :
45 : : /**
46 : : * Attribute set to the name of the binary for quantifiers that are oracle
47 : : * interfaces. In detail, an oracle interface is a quantified formula of the
48 : : * form:
49 : : * (FORALL
50 : : * (BOUND_VAR_LIST i1 ... in o1 ... om)
51 : : * (ORACLE_FORMULA_GEN A C)
52 : : * (INST_PATTERN_LIST k))
53 : : * where i1 ... in are the inputs to the interface, o1 ... om are the outputs
54 : : * of the interface, A is the "assumption" formula, C is the "constraint"
55 : : * formula, and k is a dummy skolem that has been marked with this attribute.
56 : : * The string value of this attribute specifies a binary whose I/O behavior
57 : : * should match the types of inputs and outputs specified by i1 ... in and
58 : : * o1 ... om respectively.
59 : : */
60 : : struct OracleInterfaceAttributeId
61 : : {
62 : : };
63 : : typedef expr::Attribute<OracleInterfaceAttributeId, Node>
64 : : OracleInterfaceAttribute;
65 : :
66 : : /**Attribute to give names to quantified formulas */
67 : : struct QuantNameAttributeId
68 : : {
69 : : };
70 : : typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
71 : :
72 : : /** Attribute for setting printing information for sygus variables
73 : : *
74 : : * For variable d of sygus datatype type, if
75 : : * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
76 : : */
77 : : struct SygusPrintProxyAttributeId
78 : : {
79 : : };
80 : : typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
81 : : SygusPrintProxyAttribute;
82 : :
83 : : /** Attribute for specifying a "side condition" for a sygus conjecture
84 : : *
85 : : * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
86 : : * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
87 : : */
88 : : struct SygusSideConditionAttributeId
89 : : {
90 : : };
91 : : typedef expr::Attribute<SygusSideConditionAttributeId, Node>
92 : : SygusSideConditionAttribute;
93 : :
94 : : /** Attribute for indicating that a sygus variable encodes a term
95 : : *
96 : : * This is used, e.g., for abduction where the formal argument list of the
97 : : * abduct-to-synthesize corresponds to the free variables of the sygus
98 : : * problem.
99 : : */
100 : : struct SygusVarToTermAttributeId
101 : : {
102 : : };
103 : : typedef expr::Attribute<SygusVarToTermAttributeId, Node>
104 : : SygusVarToTermAttribute;
105 : :
106 : : /**
107 : : * Attribute marked true for types that are used as abstraction types in
108 : : * the finite model finding for function definitions algorithm.
109 : : */
110 : : struct AbsTypeFunDefAttributeId
111 : : {
112 : : };
113 : : typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
114 : :
115 : : namespace quantifiers {
116 : :
117 : : /** This struct stores attributes for a single quantified formula */
118 : : struct QAttributes
119 : : {
120 : : public:
121 : 647611 : QAttributes()
122 : 647611 : : d_hasPattern(false),
123 : 647611 : d_hasPool(false),
124 : 647611 : d_sygus(false),
125 : 647611 : d_qinstLevel(-1),
126 : 647611 : d_preserveStructure(false),
127 : 647611 : d_quant_elim(false),
128 : 647611 : d_quant_elim_partial(false),
129 : 647611 : d_isQuantBounded(false)
130 : : {
131 : 647611 : }
132 : 647611 : ~QAttributes() {}
133 : : /** does the quantified formula have a pattern? */
134 : : bool d_hasPattern;
135 : : /** does the quantified formula have a pool? */
136 : : bool d_hasPool;
137 : : /** if non-null, this quantified formula is a function definition for function
138 : : * d_fundef_f */
139 : : Node d_fundef_f;
140 : : /** is this formula marked as a sygus conjecture? */
141 : : bool d_sygus;
142 : : /** the oracle, which stores an implementation */
143 : : Node d_oracle;
144 : : /** side condition for sygus conjectures */
145 : : Node d_sygusSideCondition;
146 : : /** stores the maximum instantiation level allowed for this quantified formula
147 : : * (-1 means allow any) */
148 : : int64_t d_qinstLevel;
149 : : /**
150 : : * Is this formula marked as preserving structure?
151 : : * For example, this attribute is marked when computing (partial) quantifier
152 : : * elimination on a quantified formula, but does not impact the solving method
153 : : * for it.
154 : : */
155 : : bool d_preserveStructure;
156 : : /**
157 : : * Is this formula marked for quantifier elimination? This impacts the
158 : : * strategy used for instantiating it, e.g. we always use CEGQI.
159 : : */
160 : : bool d_quant_elim;
161 : : /**
162 : : * Is this formula marked for partial quantifier elimination? This impacts the
163 : : * strategy used for instantiating it, e.g. we only invoke a single
164 : : * instantiation for it.
165 : : */
166 : : bool d_quant_elim_partial;
167 : : /** Is this formula internally generated and belonging to bounded integers? */
168 : : bool d_isQuantBounded;
169 : : /** the instantiation pattern list for this quantified formula (its 3rd child)
170 : : */
171 : : Node d_ipl;
172 : : /** The name of this quantified formula, used for :qid */
173 : : Node d_name;
174 : : /** The (internal) quantifier id associated with this formula */
175 : : Node d_qid_num;
176 : : /** is this quantified formula a function definition? */
177 : 5194339 : bool isFunDef() const { return !d_fundef_f.isNull(); }
178 : : /** is this quantified formula an oracle interface quantifier? */
179 : 5116762 : bool isOracleInterface() const { return !d_oracle.isNull(); }
180 : : /**
181 : : * Is this a standard quantifier? A standard quantifier is one that we can
182 : : * perform destructive updates (variable elimination, miniscoping, etc).
183 : : *
184 : : * A quantified formula is not standard if it is sygus, one for which
185 : : * we are performing quantifier elimination, or is a function definition.
186 : : */
187 : : bool isStandard() const;
188 : : };
189 : :
190 : : /** This class caches information about attributes of quantified formulas
191 : : *
192 : : * It also has static utility functions used for determining attributes and
193 : : * information about
194 : : * quantified formulas.
195 : : */
196 : : class QuantAttributes
197 : : {
198 : : public:
199 : : QuantAttributes(context::Context* userContext);
200 : 28686 : ~QuantAttributes() {}
201 : : /** set user attribute
202 : : * This function applies an attribute
203 : : * This can be called when we mark expressions with attributes, e.g. (! q
204 : : * :attribute attr [nodeValues]),
205 : : * It can also be called internally in various ways (for SyGus, quantifier
206 : : * elimination, etc.)
207 : : */
208 : : static void setUserAttribute(const std::string& attr,
209 : : TNode q,
210 : : const std::vector<Node>& nodeValues);
211 : :
212 : : /** compute quantifier attributes */
213 : : static void computeQuantAttributes(Node q, QAttributes& qa);
214 : : /** compute the attributes for q */
215 : : void computeAttributes(Node q);
216 : :
217 : : /** is sygus conjecture */
218 : : static bool checkSygusConjecture(Node q);
219 : : /** is sygus conjecture */
220 : : static bool checkSygusConjectureAnnotation(Node ipl);
221 : : /** get fun def body */
222 : : static Node getFunDefHead(Node q);
223 : : /** get fun def body */
224 : : static Node getFunDefBody(Node q);
225 : : /** does q have a user-provided pattern? */
226 : : static bool hasPattern(Node q);
227 : :
228 : : /** is function definition */
229 : : bool isFunDef(Node q);
230 : : /** is sygus conjecture */
231 : : bool isSygus(Node q);
232 : : /** is oracle interface */
233 : : bool isOracleInterface(Node q);
234 : : /** get instantiation level */
235 : : int64_t getQuantInstLevel(Node q);
236 : : /**
237 : : * Is q a quantified formula we are performing quantifier elimination for?
238 : : * This also true if we are performing partial quantifier elimination on q.
239 : : */
240 : : bool isQuantElim(Node q) const;
241 : : /** is quant elim partial */
242 : : bool isQuantElimPartial(Node q) const;
243 : : /** is internal quantifier */
244 : : bool isQuantBounded(Node q) const;
245 : : /** get quant name, which is used for :qid */
246 : : Node getQuantName(Node q) const;
247 : : /** Print quantified formula q, possibly using its name, if it has one */
248 : : std::string quantToString(Node q) const;
249 : : /** get (internal) quant id num */
250 : : int getQuantIdNum(Node q);
251 : : /** get (internal)quant id num */
252 : : Node getQuantIdNumNode(Node q);
253 : :
254 : : /** Make the instantiation attribute that marks "quantifier elimination" */
255 : : static Node mkAttrQuantifierElimination(NodeManager* nm);
256 : : /** Make the instantiation attribute that marks to perserve its structure */
257 : : static Node mkAttrPreserveStructure(NodeManager* nm);
258 : : /**
259 : : * Set instantiation level attribute for all subterms without an instantiation
260 : : * level in n to level.
261 : : */
262 : : static void setInstantiationLevelAttr(Node n, uint64_t level);
263 : : /**
264 : : * Get "instantiation level" for term n, if applicable. If n has an
265 : : * instantiation level, we return true and set level to its instantiation
266 : : * level.
267 : : *
268 : : * The instantiation level is an approximate measure of how many
269 : : * instantiations were required for generating term n. In particular,
270 : : * all new terms generated by an instantiation { x1 -> t1 ... xn -> tn } are
271 : : * assigned an instantiation level that is 1 + max(level(t1)...level(tn)),
272 : : * where all terms in the input formula have level 0.
273 : : */
274 : : static bool getInstantiationLevel(const Node& n, uint64_t& level);
275 : :
276 : : private:
277 : : /** An identifier for the method below */
278 : : enum class AttrType
279 : : {
280 : : ATTR_PRESERVE_STRUCTURE,
281 : : ATTR_QUANT_ELIM
282 : : };
283 : : /** Make attribute internal, helper for mkAttrX methods above. */
284 : : static Node mkAttrInternal(NodeManager* nm, AttrType at);
285 : : /** cache of attributes */
286 : : std::map<Node, QAttributes> d_qattr;
287 : : /** Function definitions active in the current user context. */
288 : : context::CDHashSet<Node> d_fun_defs;
289 : : };
290 : :
291 : : /**
292 : : * Make a named quantified formula. This is a quantified formula that will
293 : : * print like:
294 : : * (<k> <bvl> (! <body> :qid name))
295 : : */
296 : : Node mkNamedQuant(Kind k, Node bvl, Node body, const std::string& name);
297 : : } // namespace quantifiers
298 : : } // namespace theory
299 : : } // namespace cvc5::internal
300 : :
301 : : #endif
|
