Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_attributes.h	Lines:	7	7	100.0 %
Date:	2021-08-20	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, or is a function definition.
   */
  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	192689	QAttributes()
121	192689	: 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	192689	d_isInternal(false)
128		{
129	192689	}
130	192689	~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	1092880	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, or is a function definition.
166		*/
167		bool isStandard() const;
168		};
169
170		/** This class caches information about attributes of quantified formulas
171		*
172		* It also has static utility functions used for determining attributes and
173		* information about
174		* quantified formulas.
175		*/
176		class QuantAttributes
177		{
178		public:
179		QuantAttributes();
180	9856	~QuantAttributes(){}
181		/** set user attribute
182		* This function applies an attribute
183		* This can be called when we mark expressions with attributes, e.g. (! q
184		* :attribute attr [node_values, str_value...]),
185		* It can also be called internally in various ways (for SyGus, quantifier
186		* elimination, etc.)
187		*/
188		static void setUserAttribute(const std::string& attr,
189		Node q,
190		std::vector<Node>& node_values,
191		std::string str_value);
192
193		/** compute quantifier attributes */
194		static void computeQuantAttributes(Node q, QAttributes& qa);
195		/** compute the attributes for q */
196		void computeAttributes(Node q);
197
198		/** is fun def */
199		static bool checkFunDef( Node q );
200		/** is fun def */
201		static bool checkFunDefAnnotation( Node ipl );
202		/** is sygus conjecture */
203		static bool checkSygusConjecture( Node q );
204		/** is sygus conjecture */
205		static bool checkSygusConjectureAnnotation( Node ipl );
206		/** get fun def body */
207		static Node getFunDefHead( Node q );
208		/** get fun def body */
209		static Node getFunDefBody( Node q );
210		/** is quant elim annotation */
211		static bool checkQuantElimAnnotation( Node ipl );
212
213		/** is function definition */
214		bool isFunDef( Node q );
215		/** is sygus conjecture */
216		bool isSygus( Node q );
217		/** get instantiation level */
218		int64_t getQuantInstLevel(Node q);
219		/** is quant elim */
220		bool isQuantElim( Node q );
221		/** is quant elim partial */
222		bool isQuantElimPartial( Node q );
223		/** is internal quantifier */
224		bool isInternal(Node q) const;
225		/** get quant name, which is used for :qid */
226		Node getQuantName(Node q) const;
227		/** Print quantified formula q, possibly using its name, if it has one */
228		std::string quantToString(Node q) const;
229		/** get (internal) quant id num */
230		int getQuantIdNum( Node q );
231		/** get (internal)quant id num */
232		Node getQuantIdNumNode( Node q );
233
234		/** set instantiation level attr */
235		static void setInstantiationLevelAttr(Node n, uint64_t level);
236		/** set instantiation level attr */
237		static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
238
239		private:
240		/** cache of attributes */
241		std::map< Node, QAttributes > d_qattr;
242		/** function definitions */
243		std::map< Node, bool > d_fun_defs;
244		};
245
246		}
247		}
248		} // namespace cvc5
249
250		#endif