Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/type_info.h	Lines:	1	1	100.0 %
Date:	2021-05-22	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Sygus type info data structure.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H

#include <map>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class TermDbSygus;

/**
 * This data structure stores statically computed information regarding a sygus
 * datatype type.
 *
 * To use an instance of this class x, call x.initialize(tn); where tn is a
 * sygus datatype type. Then, most of the query methods on x can be called.
 * As an exception, the variable subclass queries require that additionally
 * x.initializeVarSubclasses() is called.
 *
 */
class SygusTypeInfo
{
 public:
  SygusTypeInfo();
  //-------------------------------------------- initialize
  /** initialize this information for sygus datatype type tn */
  void initialize(TermDbSygus* tds, TypeNode tn);
  /**
   * Initialize the variable subclass information for this class. Must have
   * called initialize(...) prior to calling this method.
   */
  void initializeVarSubclasses();
  //-------------------------------------------- end initialize
  /** Get the builtin type that this sygus type encodes */
  TypeNode getBuiltinType() const;
  /** Get the variable list (formal argument list) for the sygus type */
  const std::vector<Node>& getVarList() const;
  /**
   * Return the index of the constructor of this sygus type that encodes
   * application of the builtin Kind k, or -1 if one does not exist.
   */
  int getKindConsNum(Kind k) const;
  /**
   * Return the index of the constructor of this sygus type that encodes
   * constant c, or -1 if one does not exist.
   */
  int getConstConsNum(Node c) const;
  /**
   * Return the index of the constructor of this sygus type whose builtin
   * operator is n, or -1 if one does not exist.
   */
  int getOpConsNum(Node n) const;
  /** Is there a constructor that encodes application of builtin Kind k? */
  bool hasKind(Kind k) const;
  /** Is there a constructor that encodes constant c? */
  bool hasConst(Node c) const;
  /** Is there a constructor whose builtin operator is n? */
  bool hasOp(Node n) const;
  /**
   * Returns true if this sygus type has a constructor whose sygus operator is
   * ITE, or is a lambda whose body is ITE.
   */
  bool hasIte() const;
  /**
   * Returns true if this sygus type has a constructor whose sygus operator is
   * a Boolean connective.
   */
  bool hasBoolConnective() const;
  /**
   * Get the builtin kind for the i^th constructor of this sygus type. If the
   * i^th constructor does not encode an application of a builtin kind, this
   * method returns UNDEFINED_KIND.
   */
  Kind getConsNumKind(unsigned i) const;
  /**
   * Get the construct for the i^th constructor of this sygus type. If the
   * i^th constructor does not encode a builtin constant, this method returns
   * the null node.
   */
  Node getConsNumConst(unsigned i) const;
  /** Get the builtin operator of the i^th constructor of this sygus type */
  Node getConsNumOp(unsigned i) const;
  /**
   * Returns true if the i^th constructor encodes application of a builtin Kind.
   */
  bool isKindArg(unsigned i) const;
  /**
   * Returns true if the i^th constructor encodes a builtin constant.
   */
  bool isConstArg(unsigned i) const;
  /**
   * Get the index of the "any constant" constructor of type tn if it has one,
   * or returns -1 otherwise.
   */
  int getAnyConstantConsNum() const;
  /** has subterm symbolic constructor
   *
   * Returns true if any subterm of type tn can be a symbolic constructor.
   */
  bool hasSubtermSymbolicCons() const;
  /** get subfield types
   *
   * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
   * type tnc, where x has type tn. In other words, tnc is the type of some
   * subfield of terms of type tn, at any depth.
   */
  void getSubfieldTypes(std::vector<TypeNode>& sf_types) const;
  //--------------------------------- variable subclasses
  /** Get subclass id for variable
   *
   * This returns the "subclass" identifier for variable v in sygus
   * type tn. A subclass identifier groups variables based on the sygus
   * types they occur in:
   *   A -> A + B | C + C | x | y | z | w | u
   *   B -> y | z
   *   C -> u
   * The variables in this grammar can be grouped according to the sygus types
   * they appear in:
   *   { x,w } occur in A
   *   { y,z } occur in A,B
   *   { u } occurs in A,C
   * We say that e.g. x, w are in the same subclass.
   *
   * If this method returns 0, then v is not a variable in sygus type tn.
   * Otherwise, this method returns a positive value n, such that
   * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
   * same subclass.
   *
   * The type tn should be the type of an enumerator registered to this
   * database, where notice that we do not compute this information for the
   * subfield types of the enumerator.
   */
  unsigned getSubclassForVar(Node v) const;
  /**
   * Get the number of variable in the subclass with identifier sc for type tn.
   */
  unsigned getNumSubclassVars(unsigned sc) const;
  /** Get the i^th variable in the subclass with identifier sc for type tn */
  Node getVarSubclassIndex(unsigned sc, unsigned i) const;
  /**
   * Get the a variable's index in its subclass list. This method returns true
   * iff variable v has been assigned a subclass in tn. It updates index to
   * be v's index iff the method returns true.
   */
  bool getIndexInSubclassForVar(Node v, unsigned& index) const;
  /**
   * Are the variable subclasses a trivial partition (each variable subclass
   * has a single variable)?
   */
  bool isSubclassVarTrivial() const;
  //--------------------------------- end variable subclasses
  /**
   * Get the minimum depth of type in this grammar
   *
   */
  unsigned getMinTypeDepth(TypeNode tn) const;
  /** Get the minimum size for a term of this sygus type */
  unsigned getMinTermSize() const;
  /**
   * Get the minimum size for a term that is an application of a constructor of
   * this type.
   */
  unsigned getMinConsTermSize(unsigned cindex);

 private:
  /** The sygus type that this class is for */
  TypeNode d_this;
  /** The builtin type that this sygus type encodes */
  TypeNode d_btype;
  /** The variable list of the sygus type */
  std::vector<Node> d_var_list;
  /**
   * Maps constructor indices to the (builtin) Kind that they encode, if any.
   */
  std::map<unsigned, Kind> d_arg_kind;
  /** Reverse of the above map */
  std::map<Kind, unsigned> d_kinds;
  /**
   * Whether this sygus type has a constructors whose sygus operator is ITE,
   * or is a lambda whose body is ITE.
   */
  bool d_hasIte;
  /**
   * Whether this sygus type has a constructor whose sygus operator is a
   * Boolean connective.
   */
  bool d_hasBoolConnective;
  /**
   * Maps constructor indices to the constant that they encode, if any.
   */
  std::map<unsigned, Node> d_arg_const;
  /** Reverse of the above map */
  std::map<Node, unsigned> d_consts;
  /**
   * Maps constructor indices to the operator they encode.
   */
  std::map<unsigned, Node> d_arg_ops;
  /** Reverse of the above map */
  std::map<Node, unsigned> d_ops;
  /**
   * This maps the subfield datatype types T to the smallest size of a term of
   * this sygus type that includes T as a subterm. For example, for type A with
   * grammar:
   *   A -> B+B | 0 | B-D
   *   B -> C+C
   *   ...
   * we have that d_min_type_depth = { A -> 0, B -> 1, C -> 2, D -> 1 }.
   */
  std::map<TypeNode, unsigned> d_min_type_depth;
  /** The minimimum size term of this type */
  unsigned d_min_term_size;
  /**
   * Maps constructors to the minimum size term that is an application of that
   * constructor.
   */
  std::map<unsigned, unsigned> d_min_cons_term_size;
  /** a cache for getSelectorWeight */
  std::map<Node, unsigned> d_sel_weight;
  /**
   * For each sygus type, the index of the "any constant" constructor, if it
   * has one, or -1 otherwise.
   */
  int d_sym_cons_any_constant;
  /**
   * Whether any subterm of this type contains a symbolic constructor. This
   * corresponds to whether sygus repair techniques will ever have any effect
   * for this type.
   */
  bool d_has_subterm_sym_cons;
  /**
   * Map from sygus types and bound variables to their type subclass id. Note
   * type class identifiers are computed for each type of registered sygus
   * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
   */
  std::map<Node, unsigned> d_var_subclass_id;
  /** the list of variables with given subclass */
  std::map<unsigned, std::vector<Node> > d_var_subclass_list;
  /** the index of each variable in the above list */
  std::map<Node, unsigned> d_var_subclass_list_index;
  /** computes the map d_min_type_depth */
  void computeMinTypeDepthInternal(TypeNode root_tn, unsigned type_depth);
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Sygus type info data structure.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
20
21		#include <map>
22
23		#include "expr/node.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29		class TermDbSygus;
30
31		/**
32		* This data structure stores statically computed information regarding a sygus
33		* datatype type.
34		*
35		* To use an instance of this class x, call x.initialize(tn); where tn is a
36		* sygus datatype type. Then, most of the query methods on x can be called.
37		* As an exception, the variable subclass queries require that additionally
38		* x.initializeVarSubclasses() is called.
39		*
40		*/
41	1807	class SygusTypeInfo
42		{
43		public:
44		SygusTypeInfo();
45		//-------------------------------------------- initialize
46		/** initialize this information for sygus datatype type tn */
47		void initialize(TermDbSygus* tds, TypeNode tn);
48		/**
49		* Initialize the variable subclass information for this class. Must have
50		* called initialize(...) prior to calling this method.
51		*/
52		void initializeVarSubclasses();
53		//-------------------------------------------- end initialize
54		/** Get the builtin type that this sygus type encodes */
55		TypeNode getBuiltinType() const;
56		/** Get the variable list (formal argument list) for the sygus type */
57		const std::vector<Node>& getVarList() const;
58		/**
59		* Return the index of the constructor of this sygus type that encodes
60		* application of the builtin Kind k, or -1 if one does not exist.
61		*/
62		int getKindConsNum(Kind k) const;
63		/**
64		* Return the index of the constructor of this sygus type that encodes
65		* constant c, or -1 if one does not exist.
66		*/
67		int getConstConsNum(Node c) const;
68		/**
69		* Return the index of the constructor of this sygus type whose builtin
70		* operator is n, or -1 if one does not exist.
71		*/
72		int getOpConsNum(Node n) const;
73		/** Is there a constructor that encodes application of builtin Kind k? */
74		bool hasKind(Kind k) const;
75		/** Is there a constructor that encodes constant c? */
76		bool hasConst(Node c) const;
77		/** Is there a constructor whose builtin operator is n? */
78		bool hasOp(Node n) const;
79		/**
80		* Returns true if this sygus type has a constructor whose sygus operator is
81		* ITE, or is a lambda whose body is ITE.
82		*/
83		bool hasIte() const;
84		/**
85		* Returns true if this sygus type has a constructor whose sygus operator is
86		* a Boolean connective.
87		*/
88		bool hasBoolConnective() const;
89		/**
90		* Get the builtin kind for the i^th constructor of this sygus type. If the
91		* i^th constructor does not encode an application of a builtin kind, this
92		* method returns UNDEFINED_KIND.
93		*/
94		Kind getConsNumKind(unsigned i) const;
95		/**
96		* Get the construct for the i^th constructor of this sygus type. If the
97		* i^th constructor does not encode a builtin constant, this method returns
98		* the null node.
99		*/
100		Node getConsNumConst(unsigned i) const;
101		/** Get the builtin operator of the i^th constructor of this sygus type */
102		Node getConsNumOp(unsigned i) const;
103		/**
104		* Returns true if the i^th constructor encodes application of a builtin Kind.
105		*/
106		bool isKindArg(unsigned i) const;
107		/**
108		* Returns true if the i^th constructor encodes a builtin constant.
109		*/
110		bool isConstArg(unsigned i) const;
111		/**
112		* Get the index of the "any constant" constructor of type tn if it has one,
113		* or returns -1 otherwise.
114		*/
115		int getAnyConstantConsNum() const;
116		/** has subterm symbolic constructor
117		*
118		* Returns true if any subterm of type tn can be a symbolic constructor.
119		*/
120		bool hasSubtermSymbolicCons() const;
121		/** get subfield types
122		*
123		* This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
124		* type of tn if there exists a selector chain S1( ... Sn( x )...) that has
125		* type tnc, where x has type tn. In other words, tnc is the type of some
126		* subfield of terms of type tn, at any depth.
127		*/
128		void getSubfieldTypes(std::vector<TypeNode>& sf_types) const;
129		//--------------------------------- variable subclasses
130		/** Get subclass id for variable
131		*
132		* This returns the "subclass" identifier for variable v in sygus
133		* type tn. A subclass identifier groups variables based on the sygus
134		* types they occur in:
135		* A -> A + B \| C + C \| x \| y \| z \| w \| u
136		* B -> y \| z
137		* C -> u
138		* The variables in this grammar can be grouped according to the sygus types
139		* they appear in:
140		* { x,w } occur in A
141		* { y,z } occur in A,B
142		* { u } occurs in A,C
143		* We say that e.g. x, w are in the same subclass.
144		*
145		* If this method returns 0, then v is not a variable in sygus type tn.
146		* Otherwise, this method returns a positive value n, such that
147		* getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
148		* same subclass.
149		*
150		* The type tn should be the type of an enumerator registered to this
151		* database, where notice that we do not compute this information for the
152		* subfield types of the enumerator.
153		*/
154		unsigned getSubclassForVar(Node v) const;
155		/**
156		* Get the number of variable in the subclass with identifier sc for type tn.
157		*/
158		unsigned getNumSubclassVars(unsigned sc) const;
159		/** Get the i^th variable in the subclass with identifier sc for type tn */
160		Node getVarSubclassIndex(unsigned sc, unsigned i) const;
161		/**
162		* Get the a variable's index in its subclass list. This method returns true
163		* iff variable v has been assigned a subclass in tn. It updates index to
164		* be v's index iff the method returns true.
165		*/
166		bool getIndexInSubclassForVar(Node v, unsigned& index) const;
167		/**
168		* Are the variable subclasses a trivial partition (each variable subclass
169		* has a single variable)?
170		*/
171		bool isSubclassVarTrivial() const;
172		//--------------------------------- end variable subclasses
173		/**
174		* Get the minimum depth of type in this grammar
175		*
176		*/
177		unsigned getMinTypeDepth(TypeNode tn) const;
178		/** Get the minimum size for a term of this sygus type */
179		unsigned getMinTermSize() const;
180		/**
181		* Get the minimum size for a term that is an application of a constructor of
182		* this type.
183		*/
184		unsigned getMinConsTermSize(unsigned cindex);
185
186		private:
187		/** The sygus type that this class is for */
188		TypeNode d_this;
189		/** The builtin type that this sygus type encodes */
190		TypeNode d_btype;
191		/** The variable list of the sygus type */
192		std::vector<Node> d_var_list;
193		/**
194		* Maps constructor indices to the (builtin) Kind that they encode, if any.
195		*/
196		std::map<unsigned, Kind> d_arg_kind;
197		/** Reverse of the above map */
198		std::map<Kind, unsigned> d_kinds;
199		/**
200		* Whether this sygus type has a constructors whose sygus operator is ITE,
201		* or is a lambda whose body is ITE.
202		*/
203		bool d_hasIte;
204		/**
205		* Whether this sygus type has a constructor whose sygus operator is a
206		* Boolean connective.
207		*/
208		bool d_hasBoolConnective;
209		/**
210		* Maps constructor indices to the constant that they encode, if any.
211		*/
212		std::map<unsigned, Node> d_arg_const;
213		/** Reverse of the above map */
214		std::map<Node, unsigned> d_consts;
215		/**
216		* Maps constructor indices to the operator they encode.
217		*/
218		std::map<unsigned, Node> d_arg_ops;
219		/** Reverse of the above map */
220		std::map<Node, unsigned> d_ops;
221		/**
222		* This maps the subfield datatype types T to the smallest size of a term of
223		* this sygus type that includes T as a subterm. For example, for type A with
224		* grammar:
225		* A -> B+B \| 0 \| B-D
226		* B -> C+C
227		* ...
228		* we have that d_min_type_depth = { A -> 0, B -> 1, C -> 2, D -> 1 }.
229		*/
230		std::map<TypeNode, unsigned> d_min_type_depth;
231		/** The minimimum size term of this type */
232		unsigned d_min_term_size;
233		/**
234		* Maps constructors to the minimum size term that is an application of that
235		* constructor.
236		*/
237		std::map<unsigned, unsigned> d_min_cons_term_size;
238		/** a cache for getSelectorWeight */
239		std::map<Node, unsigned> d_sel_weight;
240		/**
241		* For each sygus type, the index of the "any constant" constructor, if it
242		* has one, or -1 otherwise.
243		*/
244		int d_sym_cons_any_constant;
245		/**
246		* Whether any subterm of this type contains a symbolic constructor. This
247		* corresponds to whether sygus repair techniques will ever have any effect
248		* for this type.
249		*/
250		bool d_has_subterm_sym_cons;
251		/**
252		* Map from sygus types and bound variables to their type subclass id. Note
253		* type class identifiers are computed for each type of registered sygus
254		* enumerators, but not all sygus types. For details, see getSubclassIdForVar.
255		*/
256		std::map<Node, unsigned> d_var_subclass_id;
257		/** the list of variables with given subclass */
258		std::map<unsigned, std::vector<Node> > d_var_subclass_list;
259		/** the index of each variable in the above list */
260		std::map<Node, unsigned> d_var_subclass_list_index;
261		/** computes the map d_min_type_depth */
262		void computeMinTypeDepthInternal(TypeNode root_tn, unsigned type_depth);
263		};
264
265		} // namespace quantifiers
266		} // namespace theory
267		} // namespace cvc5
268
269		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */