1 /********************* */
2 /*! \file quantifiers_attributes.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Paul Meng, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief Attributes for the theory quantifiers
14 ** Attributes for the theory quantifiers.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
20 #define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
22 #include "expr/attribute.h"
23 #include "expr/node.h"
28 class QuantifiersEngine
;
30 /** Attribute true for quantifiers that are axioms */
31 struct AxiomAttributeId
{};
32 typedef expr::Attribute
< AxiomAttributeId
, bool > AxiomAttribute
;
34 /** Attribute true for quantifiers that are conjecture */
35 struct ConjectureAttributeId
{};
36 typedef expr::Attribute
< ConjectureAttributeId
, bool > ConjectureAttribute
;
38 /** Attribute true for function definition quantifiers */
39 struct FunDefAttributeId
{};
40 typedef expr::Attribute
< FunDefAttributeId
, bool > FunDefAttribute
;
42 /** Attribute true for quantifiers that we are doing quantifier elimination on */
43 struct QuantElimAttributeId
{};
44 typedef expr::Attribute
< QuantElimAttributeId
, bool > QuantElimAttribute
;
46 /** Attribute true for quantifiers that we are doing partial quantifier elimination on */
47 struct QuantElimPartialAttributeId
{};
48 typedef expr::Attribute
< QuantElimPartialAttributeId
, bool > QuantElimPartialAttribute
;
50 /** Attribute true for quantifiers that are SyGus conjectures */
51 struct SygusAttributeId
{};
52 typedef expr::Attribute
< SygusAttributeId
, bool > SygusAttribute
;
54 /** Attribute true for quantifiers that are synthesis conjectures */
55 struct SynthesisAttributeId
{};
56 typedef expr::Attribute
< SynthesisAttributeId
, bool > SynthesisAttribute
;
58 /** Attribute for setting printing information for sygus variables
60 * For variable d of sygus datatype type, if
61 * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
63 struct SygusPrintProxyAttributeId
66 typedef expr::Attribute
<SygusPrintProxyAttributeId
, Node
>
67 SygusPrintProxyAttribute
;
69 namespace quantifiers
{
71 /** Attribute priority for rewrite rules */
72 //struct RrPriorityAttributeId {};
73 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
75 /** This struct stores attributes for a single quantified formula */
79 QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
80 d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
82 /** does the quantified formula have a pattern? */
84 /** if non-null, this is the rewrite rule representation of the quantified
87 /** is this formula marked a conjecture? */
89 /** is this formula marked an axiom? */
91 /** if non-null, this quantified formula is a function definition for function
94 /** is this formula marked as a sygus conjecture? */
96 /** is this formula marked as a synthesis (non-sygus) conjecture? */
98 /** if a rewrite rule, then this is the priority value for the rewrite rule */
100 /** stores the maximum instantiation level allowed for this quantified formula
101 * (-1 means allow any) */
103 /** is this formula marked for quantifier elimination? */
105 /** is this formula marked for partial quantifier elimination? */
106 bool d_quant_elim_partial
;
107 /** the instantiation pattern list for this quantified formula (its 3rd child)
110 /** the quantifier id associated with this formula */
112 /** is this quantified formula a rewrite rule? */
113 bool isRewriteRule() { return !d_rr
.isNull(); }
114 /** is this quantified formula a function definition? */
115 bool isFunDef() { return !d_fundef_f
.isNull(); }
118 /** This class caches information about attributes of quantified formulas
120 * It also has static utility functions used for determining attributes and
122 * quantified formulas.
124 class QuantAttributes
127 QuantAttributes( QuantifiersEngine
* qe
);
129 /** set user attribute
130 * This function applies an attribute
131 * This can be called when we mark expressions with attributes, e.g. (! q
132 * :attribute attr [node_values, str_value...]),
133 * It can also be called internally in various ways (for SyGus, quantifier
136 static void setUserAttribute(const std::string
& attr
,
138 std::vector
<Node
>& node_values
,
139 std::string str_value
);
141 /** compute quantifier attributes */
142 static void computeQuantAttributes(Node q
, QAttributes
& qa
);
143 /** compute the attributes for q */
144 void computeAttributes(Node q
);
146 /** is quantifier treated as a rewrite rule? */
147 static bool checkRewriteRule( Node q
);
148 /** get the rewrite rule associated with the quanfied formula */
149 static Node
getRewriteRule( Node q
);
151 static bool checkFunDef( Node q
);
153 static bool checkFunDefAnnotation( Node ipl
);
154 /** is sygus conjecture */
155 static bool checkSygusConjecture( Node q
);
156 /** is sygus conjecture */
157 static bool checkSygusConjectureAnnotation( Node ipl
);
158 /** get fun def body */
159 static Node
getFunDefHead( Node q
);
160 /** get fun def body */
161 static Node
getFunDefBody( Node q
);
162 /** is quant elim annotation */
163 static bool checkQuantElimAnnotation( Node ipl
);
166 bool isConjecture( Node q
);
168 bool isAxiom( Node q
);
169 /** is function definition */
170 bool isFunDef( Node q
);
171 /** is sygus conjecture */
172 bool isSygus( Node q
);
173 /** is synthesis conjecture */
174 bool isSynthesis( Node q
);
175 /** get instantiation level */
176 int getQuantInstLevel( Node q
);
177 /** get rewrite rule priority */
178 int getRewriteRulePriority( Node q
);
180 bool isQuantElim( Node q
);
181 /** is quant elim partial */
182 bool isQuantElimPartial( Node q
);
183 /** get quant id num */
184 int getQuantIdNum( Node q
);
185 /** get quant id num */
186 Node
getQuantIdNumNode( Node q
);
189 /** pointer to quantifiers engine */
190 QuantifiersEngine
* d_quantEngine
;
191 /** cache of attributes */
192 std::map
< Node
, QAttributes
> d_qattr
;
193 /** function definitions */
194 std::map
< Node
, bool > d_fun_defs
;