Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_attributes.h	Lines:	7	7	100.0 %
Date:	2021-08-06	Branches:	4	8	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Attributes for the theory quantifiers.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H

#include "expr/attribute.h"
#include "expr/node.h"

namespace cvc5 {
namespace theory {

/** Attribute true for function definition quantifiers */
struct FunDefAttributeId {};
typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;

/** Attribute true for quantifiers that we are doing quantifier elimination on */
struct QuantElimAttributeId {};
typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;

/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
struct QuantElimPartialAttributeId {};
typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;

/** Attribute true for quantifiers that are SyGus conjectures */
struct SygusAttributeId {};
typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;

/**Attribute to give names to quantified formulas */
struct QuantNameAttributeId
{
};
typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;

struct InstLevelAttributeId
{
};
typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;

/** Attribute for setting printing information for sygus variables
 *
 * For variable d of sygus datatype type, if
 * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
 */
struct SygusPrintProxyAttributeId
{
};
typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
    SygusPrintProxyAttribute;

/** Attribute for specifying a "side condition" for a sygus conjecture
 *
 * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
 * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
 */
struct SygusSideConditionAttributeId
{
};
typedef expr::Attribute<SygusSideConditionAttributeId, Node>
    SygusSideConditionAttribute;

/** Attribute for indicating that a sygus variable encodes a term
 *
 * This is used, e.g., for abduction where the formal argument list of the
 * abduct-to-synthesize corresponds to the free variables of the sygus
 * problem.
 */
struct SygusVarToTermAttributeId
{
};
typedef expr::Attribute<SygusVarToTermAttributeId, Node>
    SygusVarToTermAttribute;

/**
 * Attribute marked true for types that are used as abstraction types in
 * the finite model finding for function definitions algorithm.
 */
struct AbsTypeFunDefAttributeId
{
};
typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;

/**
 * Attribute true for quantifiers that have been internally generated, e.g.
 * for reductions of string operators.
 *
 * Currently, this attribute is used for indicating that E-matching should
 * not be applied, as E-matching should not be applied to quantifiers
 * generated for strings reductions.
 *
 * This attribute can potentially be generalized to an identifier indicating
 * the internal source of the quantified formula (of which strings reduction
 * is one possibility).
 */
struct InternalQuantAttributeId
{
};
typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute;

namespace quantifiers {

/** This struct stores attributes for a single quantified formula */
struct QAttributes
{
 public:
  QAttributes()
      : d_hasPattern(false),
        d_hasPool(false),
        d_sygus(false),
        d_qinstLevel(-1),
        d_quant_elim(false),
        d_quant_elim_partial(false),
        d_isInternal(false)
  {
  }
  ~QAttributes(){}
  /** does the quantified formula have a pattern? */
  bool d_hasPattern;
  /** does the quantified formula have a pool? */
  bool d_hasPool;
  /** if non-null, this quantified formula is a function definition for function
   * d_fundef_f */
  Node d_fundef_f;
  /** is this formula marked as a sygus conjecture? */
  bool d_sygus;
  /** side condition for sygus conjectures */
  Node d_sygusSideCondition;
  /** stores the maximum instantiation level allowed for this quantified formula
   * (-1 means allow any) */
  int64_t d_qinstLevel;
  /** is this formula marked for quantifier elimination? */
  bool d_quant_elim;
  /** is this formula marked for partial quantifier elimination? */
  bool d_quant_elim_partial;
  /** Is this formula internally generated? */
  bool d_isInternal;
  /** the instantiation pattern list for this quantified formula (its 3rd child)
   */
  Node d_ipl;
  /** The name of this quantified formula, used for :qid */
  Node d_name;
  /** The (internal) quantifier id associated with this formula */
  Node d_qid_num;
  /** is this quantified formula a function definition? */
  bool isFunDef() const { return !d_fundef_f.isNull(); }
  /**
   * Is this a standard quantifier? A standard quantifier is one that we can
   * perform destructive updates (variable elimination, miniscoping, etc).
   *
   * A quantified formula is not standard if it is sygus, one for which
   * we are performing quantifier elimination, is a function definition, or
   * has a name.
   */
  bool isStandard() const;
};

/** This class caches information about attributes of quantified formulas
*
* It also has static utility functions used for determining attributes and
* information about
* quantified formulas.
*/
class QuantAttributes
{
 public:
  QuantAttributes();
  ~QuantAttributes(){}
  /** set user attribute
  * This function applies an attribute
  * This can be called when we mark expressions with attributes, e.g. (! q
  * :attribute attr [node_values, str_value...]),
  * It can also be called internally in various ways (for SyGus, quantifier
  * elimination, etc.)
  */
  static void setUserAttribute(const std::string& attr,
                               Node q,
                               std::vector<Node>& node_values,
                               std::string str_value);

  /** compute quantifier attributes */
  static void computeQuantAttributes(Node q, QAttributes& qa);
  /** compute the attributes for q */
  void computeAttributes(Node q);

  /** is fun def */
  static bool checkFunDef( Node q );
  /** is fun def */
  static bool checkFunDefAnnotation( Node ipl );
  /** is sygus conjecture */
  static bool checkSygusConjecture( Node q );
  /** is sygus conjecture */
  static bool checkSygusConjectureAnnotation( Node ipl );
  /** get fun def body */
  static Node getFunDefHead( Node q );
  /** get fun def body */
  static Node getFunDefBody( Node q );
  /** is quant elim annotation */
  static bool checkQuantElimAnnotation( Node ipl );

  /** is function definition */
  bool isFunDef( Node q );
  /** is sygus conjecture */
  bool isSygus( Node q );
  /** get instantiation level */
  int64_t getQuantInstLevel(Node q);
  /** is quant elim */
  bool isQuantElim( Node q );
  /** is quant elim partial */
  bool isQuantElimPartial( Node q );
  /** is internal quantifier */
  bool isInternal(Node q) const;
  /** get quant name, which is used for :qid */
  Node getQuantName(Node q) const;
  /** Print quantified formula q, possibly using its name, if it has one */
  std::string quantToString(Node q) const;
  /** get (internal) quant id num */
  int getQuantIdNum( Node q );
  /** get (internal)quant id num */
  Node getQuantIdNumNode( Node q );

  /** set instantiation level attr */
  static void setInstantiationLevelAttr(Node n, uint64_t level);
  /** set instantiation level attr */
  static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);

 private:
  /** cache of attributes */
  std::map< Node, QAttributes > d_qattr;
  /** function definitions */
  std::map< Node, bool > d_fun_defs;
};

}
}
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

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