GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_attributes.h Lines: 7 7 100.0 %
Date: 2021-03-23 Branches: 4 8 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_attributes.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Attributes for the theory quantifiers
13
 **
14
 ** Attributes for the theory quantifiers.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
20
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
21
22
#include "expr/attribute.h"
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
/** Attribute true for function definition quantifiers */
29
struct FunDefAttributeId {};
30
typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
31
32
/** Attribute true for quantifiers that we are doing quantifier elimination on */
33
struct QuantElimAttributeId {};
34
typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
35
36
/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
37
struct QuantElimPartialAttributeId {};
38
typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
39
40
/** Attribute true for quantifiers that are SyGus conjectures */
41
struct SygusAttributeId {};
42
typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
43
44
/**Attribute to give names to quantified formulas */
45
struct QuantNameAttributeId
46
{
47
};
48
typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
49
50
struct InstLevelAttributeId
51
{
52
};
53
typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
54
55
/** Attribute for setting printing information for sygus variables
56
 *
57
 * For variable d of sygus datatype type, if
58
 * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
59
 */
60
struct SygusPrintProxyAttributeId
61
{
62
};
63
typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
64
    SygusPrintProxyAttribute;
65
66
/** Attribute for specifying a "side condition" for a sygus conjecture
67
 *
68
 * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
69
 * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
70
 */
71
struct SygusSideConditionAttributeId
72
{
73
};
74
typedef expr::Attribute<SygusSideConditionAttributeId, Node>
75
    SygusSideConditionAttribute;
76
77
/** Attribute for indicating that a sygus variable encodes a term
78
 *
79
 * This is used, e.g., for abduction where the formal argument list of the
80
 * abduct-to-synthesize corresponds to the free variables of the sygus
81
 * problem.
82
 */
83
struct SygusVarToTermAttributeId
84
{
85
};
86
typedef expr::Attribute<SygusVarToTermAttributeId, Node>
87
    SygusVarToTermAttribute;
88
89
/**
90
 * Attribute marked true for types that are used as abstraction types in
91
 * the finite model finding for function definitions algorithm.
92
 */
93
struct AbsTypeFunDefAttributeId
94
{
95
};
96
typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
97
98
/**
99
 * Attribute true for quantifiers that have been internally generated, e.g.
100
 * for reductions of string operators.
101
 *
102
 * Currently, this attribute is used for indicating that E-matching should
103
 * not be applied, as E-matching should not be applied to quantifiers
104
 * generated for strings reductions.
105
 *
106
 * This attribute can potentially be generalized to an identifier indicating
107
 * the internal source of the quantified formula (of which strings reduction
108
 * is one possibility).
109
 */
110
struct InternalQuantAttributeId
111
{
112
};
113
typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute;
114
115
namespace quantifiers {
116
117
/** This struct stores attributes for a single quantified formula */
118
struct QAttributes
119
{
120
 public:
121
186438
  QAttributes()
122
186438
      : d_hasPattern(false),
123
        d_sygus(false),
124
        d_qinstLevel(-1),
125
        d_quant_elim(false),
126
        d_quant_elim_partial(false),
127
186438
        d_isInternal(false)
128
  {
129
186438
  }
130
186438
  ~QAttributes(){}
131
  /** does the quantified formula have a pattern? */
132
  bool d_hasPattern;
133
  /** if non-null, this quantified formula is a function definition for function
134
   * d_fundef_f */
135
  Node d_fundef_f;
136
  /** is this formula marked as a sygus conjecture? */
137
  bool d_sygus;
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
  /** is this formula marked for quantifier elimination? */
144
  bool d_quant_elim;
145
  /** is this formula marked for partial quantifier elimination? */
146
  bool d_quant_elim_partial;
147
  /** Is this formula internally generated? */
148
  bool d_isInternal;
149
  /** the instantiation pattern list for this quantified formula (its 3rd child)
150
   */
151
  Node d_ipl;
152
  /** The name of this quantified formula, used for :qid */
153
  Node d_name;
154
  /** The (internal) quantifier id associated with this formula */
155
  Node d_qid_num;
156
  /** is this quantified formula a function definition? */
157
1038262
  bool isFunDef() const { return !d_fundef_f.isNull(); }
158
  /**
159
   * Is this a standard quantifier? A standard quantifier is one that we can
160
   * perform destructive updates (variable elimination, miniscoping, etc).
161
   *
162
   * A quantified formula is not standard if it is sygus, one for which
163
   * we are performing quantifier elimination, is a function definition, or
164
   * has a name.
165
   */
166
  bool isStandard() const;
167
};
168
169
/** This class caches information about attributes of quantified formulas
170
*
171
* It also has static utility functions used for determining attributes and
172
* information about
173
* quantified formulas.
174
*/
175
class QuantAttributes
176
{
177
 public:
178
  QuantAttributes();
179
8994
  ~QuantAttributes(){}
180
  /** set user attribute
181
  * This function applies an attribute
182
  * This can be called when we mark expressions with attributes, e.g. (! q
183
  * :attribute attr [node_values, str_value...]),
184
  * It can also be called internally in various ways (for SyGus, quantifier
185
  * elimination, etc.)
186
  */
187
  static void setUserAttribute(const std::string& attr,
188
                               Node q,
189
                               std::vector<Node>& node_values,
190
                               std::string str_value);
191
192
  /** compute quantifier attributes */
193
  static void computeQuantAttributes(Node q, QAttributes& qa);
194
  /** compute the attributes for q */
195
  void computeAttributes(Node q);
196
197
  /** is fun def */
198
  static bool checkFunDef( Node q );
199
  /** is fun def */
200
  static bool checkFunDefAnnotation( Node ipl );
201
  /** is sygus conjecture */
202
  static bool checkSygusConjecture( Node q );
203
  /** is sygus conjecture */
204
  static bool checkSygusConjectureAnnotation( Node ipl );
205
  /** get fun def body */
206
  static Node getFunDefHead( Node q );
207
  /** get fun def body */
208
  static Node getFunDefBody( Node q );
209
  /** is quant elim annotation */
210
  static bool checkQuantElimAnnotation( Node ipl );
211
212
  /** is function definition */
213
  bool isFunDef( Node q );
214
  /** is sygus conjecture */
215
  bool isSygus( Node q );
216
  /** get instantiation level */
217
  int64_t getQuantInstLevel(Node q);
218
  /** is quant elim */
219
  bool isQuantElim( Node q );
220
  /** is quant elim partial */
221
  bool isQuantElimPartial( Node q );
222
  /** is internal quantifier */
223
  bool isInternal(Node q) const;
224
  /** get quant name, which is used for :qid */
225
  Node getQuantName(Node q) const;
226
  /** Print quantified formula q, possibly using its name, if it has one */
227
  std::string quantToString(Node q) const;
228
  /** get (internal) quant id num */
229
  int getQuantIdNum( Node q );
230
  /** get (internal)quant id num */
231
  Node getQuantIdNumNode( Node q );
232
233
  /** set instantiation level attr */
234
  static void setInstantiationLevelAttr(Node n, uint64_t level);
235
  /** set instantiation level attr */
236
  static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
237
238
 private:
239
  /** cache of attributes */
240
  std::map< Node, QAttributes > d_qattr;
241
  /** function definitions */
242
  std::map< Node, bool > d_fun_defs;
243
};
244
245
}
246
}
247
}
248
249
#endif