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