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