Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_unif_strat.h	Lines:	18	18	100.0 %
Date:	2021-05-22	Branches:	3	6	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, 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.
 * ****************************************************************************
 *
 * sygus_unif_strat
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H

#include <map>
#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class TermDbSygus;

/** roles for enumerators
 *
 * This indicates the role of an enumerator that is allocated by approaches
 * for synthesis-by-unification (see details below).
 *   io : the enumerator should enumerate values that are overall solutions
 *        for the function-to-synthesize,
 *   ite_condition : the enumerator should enumerate values that are useful
 *                   in ite conditions in the ITE strategy,
 *   concat_term : the enumerator should enumerate values that are used as
 *                 components of string concatenation solutions.
 */
enum EnumRole
{
  enum_invalid,
  enum_io,
  enum_ite_condition,
  enum_concat_term,
};
std::ostream& operator<<(std::ostream& os, EnumRole r);

/** roles for strategy nodes
 *
 * This indicates the role of a strategy node, which is a subprocedure of
 * SygusUnif::constructSolution (see details below).
 *   equal : the node constructed must be equal to the overall solution for
 *           the function-to-synthesize,
 *   string_prefix/suffix : the node constructed must be a prefix/suffix
 *                          of the function-to-synthesize,
 *   ite_condition : the node constructed must be a condition that makes some
 *                   active input examples true and some input examples false.
 */
enum NodeRole
{
  role_invalid,
  role_equal,
  role_string_prefix,
  role_string_suffix,
  role_ite_condition,
};
std::ostream& operator<<(std::ostream& os, NodeRole r);

/** enumerator role for node role */
EnumRole getEnumeratorRoleForNodeRole(NodeRole r);

/** strategy types
 *
 * This indicates a strategy for synthesis-by-unification (see details below).
 *   ITE : strategy for constructing if-then-else solutions via decision
 *         tree learning techniques,
 *   CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
 *         solutions via a divide and conquer approach,
 *   ID : identity strategy used for calling strategies on child type through
 *        an identity function.
 */
enum StrategyType
{
  strat_INVALID,
  strat_ITE,
  strat_CONCAT_PREFIX,
  strat_CONCAT_SUFFIX,
  strat_ID,
};
std::ostream& operator<<(std::ostream& os, StrategyType st);

/** virtual base class for context in synthesis-by-unification approaches */
class UnifContext
{
 public:
  virtual ~UnifContext() {}

  /** Get the current role
   *
   * In a particular context when constructing solutions in synthesis by
   * unification, we may be solving based on a modified role. For example,
   * if we are currently synthesizing x in a solution ("a" ++ x), we are
   * synthesizing the string suffix of the overall solution. In this case, this
   * function returns role_string_suffix.
   */
  virtual NodeRole getCurrentRole() = 0;
  /** is return value modified?
   *
   * This returns true if we are currently in a state where the return value
   * of the solution has been modified, e.g. by a previous node that solved
   * for a string prefix.
   */
  bool isReturnValueModified() { return getCurrentRole() != role_equal; }
};

/**
* This class stores information regarding an enumerator, including
* information regarding the role of this enumerator (see EnumRole), its
* parent, whether it is templated, its slave enumerators, and so on.
*
* We say an enumerator is a master enumerator if it is the variable that
* we use to enumerate values for its sort. Master enumerators may have
* (possibly multiple) slave enumerators, stored in d_enum_slave. When
* constructing a sygus unifciation strategy, we make the first enumerator for
* each type a master enumerator, and any additional ones slaves of it.
*/
class EnumInfo
{
 public:
  EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
  /** initialize this class
  *
  * role is the "role" the enumerator plays in the high-level strategy,
  *   which is one of enum_* above.
  */
  void initialize(EnumRole role);
  /** is this enumerator associated with a template? */
  bool isTemplated() { return !d_template.isNull(); }
  /** set conditional
    *
    * This flag is set to true if this enumerator may not apply to all
    * input/output examples. For example, if this enumerator is used
    * as an output value beneath a conditional in an instance of strat_ITE,
    * then this enumerator is conditional.
    */
  void setConditional() { d_is_conditional = true; }
  /** returns if this enumerator is conditional */
  bool isConditional() { return d_is_conditional; }
  /** get the role of this enumerator */
  EnumRole getRole() { return d_role; }
  /** enumerator template
  *
  * If d_template non-null, enumerated values V are immediately transformed to
  * d_template { d_template_arg -> V }.
  */
  Node d_template;
  Node d_template_arg;
  /**
  * Slave enumerators of this enumerator. These are other enumerators that
  * have the same type, but a different role in the strategy tree. We
  * generally
  * only use one enumerator per type, and hence these slaves are notified when
  * values are enumerated for this enumerator.
  */
  std::vector<Node> d_enum_slave;

 private:
  /** the role of this enumerator (one of enum_* above). */
  EnumRole d_role;
  /** is this enumerator conditional */
  bool d_is_conditional;
};

class EnumTypeInfoStrat;

/** represents a node in the strategy graph
 *
 * It contains a list of possible strategies which are tried during calls
 * to constructSolution.
 */
class StrategyNode
{
 public:
  StrategyNode() {}
  ~StrategyNode();
  /** the set of strategies to try at this node in the strategy graph */
  std::vector<EnumTypeInfoStrat*> d_strats;
};

/**
 * Stores all enumerators and strategies for a SyGuS datatype type.
 */
class EnumTypeInfo
{
 public:
  EnumTypeInfo() {}
  /** the type that this information is for */
  TypeNode d_this_type;
  /** map from enum roles to enumerators for this type */
  std::map<EnumRole, Node> d_enum;
  /** map from node roles to strategy nodes */
  std::map<NodeRole, StrategyNode> d_snodes;
  /** get strategy node for node role */
  StrategyNode& getStrategyNode(NodeRole nrole);
};

/** represents a strategy for a SyGuS datatype type
  *
  * This represents a possible strategy to apply when processing a strategy
  * node in constructSolution. When applying the strategy represented by this
  * class, we may make recursive calls to the children of the strategy,
  * given in d_cenum. If all recursive calls to constructSolution for these
  * children are successful, say:
  *   constructSolution( d_cenum[1], ... ) = t1,
  *    ...,
  *   constructSolution( d_cenum[n], ... ) = tn,
  * Then, the solution returned by this strategy is
  *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
  * where * is application of substitution.
  */
class EnumTypeInfoStrat
{
 public:
  /** the type of strategy this represents */
  StrategyType d_this;
  /** the sygus datatype constructor that induced this strategy
    *
    * For example, this may be a sygus datatype whose sygus operator is ITE,
    * if the strategy type above is strat_ITE.
    */
  Node d_cons;
  /** children of this strategy */
  std::vector<std::pair<Node, NodeRole> > d_cenum;
  /** the arguments for the (templated) solution */
  std::vector<Node> d_sol_templ_args;
  /** the template for the solution */
  Node d_sol_templ;
  /** Returns true if argument is valid strategy in unification context x */
  bool isValid(UnifContext& x);
};

/**
 * flags for extra restrictions to be inferred during redundant operators
 * learning
 */
struct StrategyRestrictions
{
  StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true)
  {
  }
  /**
   * if this flag is true then staticLearnRedundantOps will also try to make
   * the return value of boolean ITEs to be restricted to constants
   */
  bool d_iteReturnBoolConst;
  /**
   * if this flag is true then staticLearnRedundantOps will also try to make
   * the condition values of ITEs to be restricted to atoms
   */
  bool d_iteCondOnlyAtoms;
  /**
   * A list of unused strategies. This maps strategy points to the indices
   * in StrategyNode::d_strats that are not used by the caller of
   * staticLearnRedundantOps, and hence should not be taken into account
   * when doing redundant operator learning.
   */
  std::map<Node, std::unordered_set<unsigned>> d_unused_strategies;
};

/**
 * Stores strategy and enumeration information for a function-to-synthesize.
 *
 * When this class is initialized, we construct a "strategy tree" based on
 * the grammar of the function to synthesize f. This tree is represented by
 * the above classes.
 */
class SygusUnifStrategy
{
 public:
  SygusUnifStrategy() : d_tds(nullptr) {}
  /** initialize
   *
   * This initializes this class with function-to-synthesize f. We also call
   * f the candidate variable.
   *
   * This call constructs a set of enumerators for the relevant subfields of
   * the grammar of f and adds them to enums.
   */
  void initialize(TermDbSygus* tds, Node f, std::vector<Node>& enums);
  /** Get the root enumerator for this class */
  Node getRootEnumerator() const;
  /**
   * Get the enumerator info for enumerator e, where e must be an enumerator
   * initialized by this class (in enums after a call to initialize).
   */
  EnumInfo& getEnumInfo(Node e);
  /**
   * Get the enumerator type info for sygus type t, where t must be the type
   * of some enumerator initialized by this class
   */
  EnumTypeInfo& getEnumTypeInfo(TypeNode tn);

  /** static learn redundant operators
   *
   * This learns static lemmas for pruning enumerative space based on the
   * strategy for the function-to-synthesize of this class, and stores these
   * into strategy_lemmas.
   *
   * These may correspond to static symmetry breaking predicates (for example,
   * those that exclude ITE from enumerators whose role is enum_io when the
   * strategy is ITE_strat).
   *
   * then the module may also try to apply the given pruning restrictions (see
   * StrategyRestrictions for more details)
   */
  void staticLearnRedundantOps(
      std::map<Node, std::vector<Node>>& strategy_lemmas,
      StrategyRestrictions& restrictions);
  /**
   * creates the default restrictions when they are not given and calls the
   * above function
   */
  void staticLearnRedundantOps(
      std::map<Node, std::vector<Node>>& strategy_lemmas);

  /** debug print this strategy on Trace c */
  void debugPrint(const char* c);

 private:
  /** pointer to the term database sygus */
  TermDbSygus* d_tds;
  /** The candidate variable this strategy is for */
  Node d_candidate;
  /** maps enumerators to relevant information */
  std::map<Node, EnumInfo> d_einfo;
  /** list of all enumerators for the function-to-synthesize */
  std::vector<Node> d_esym_list;
  /** Info for sygus datatype type occurring in a field of d_root */
  std::map<TypeNode, EnumTypeInfo> d_tinfo;
  /**
    * The root sygus datatype for the function-to-synthesize,
    * which encodes the overall syntactic restrictions on the space
    * of solutions.
    */
  TypeNode d_root;
  /**
    * Maps sygus datatypes to their master enumerator. This is the (single)
    * enumerator of that type that we enumerate values for.
    */
  std::map<TypeNode, Node> d_master_enum;
  /** Initialize necessary information for (sygus) type tn */
  void initializeType(TypeNode tn);

  //-----------------------debug printing
  /** print ind indentations on trace c */
  static void indent(const char* c, int ind);
  //-----------------------end debug printing

  //------------------------------ strategy registration
  /** build strategy graph
   *
   * This builds the strategy for enumerated values of type tn for the given
   * role of nrole, for solutions to function-to-synthesize of this class.
   */
  void buildStrategyGraph(TypeNode tn, NodeRole nrole);
  /** register enumerator
   *
   * This registers that et is an enumerator of type tn, having enumerator
   * role enum_role.
   *
   * inSearch is whether we will enumerate values based on this enumerator.
   * A strategy node is represented by a (enumerator, node role) pair. Hence,
   * we may use enumerators for which this flag is false to represent strategy
   * nodes that have child strategies.
   */
  void registerStrategyPoint(Node et,
                          TypeNode tn,
                          EnumRole enum_role,
                          bool inSearch);
  /** infer template */
  bool inferTemplate(unsigned k,
                     Node n,
                     std::map<Node, unsigned>& templ_var_index,
                     std::map<unsigned, unsigned>& templ_injection);
  /** helper for static learn redundant operators
   *
   * (e, nrole) specify the strategy node in the graph we are currently
   * analyzing, visited stores the nodes we have already visited.
   *
   * This method builds the mapping needs_cons, which maps (master) enumerators
   * to a map from the constructors that it needs.
   */
  void staticLearnRedundantOps(
      Node e,
      NodeRole nrole,
      std::map<Node, std::map<NodeRole, bool>>& visited,
      std::map<Node, std::map<unsigned, bool>>& needs_cons,
      StrategyRestrictions& restrictions);
  /** finish initialization of the strategy tree
   *
   * (e, nrole) specify the strategy node in the graph we are currently
   * analyzing, visited stores the nodes we have already visited.
   *
   * isCond is whether the current enumerator is conditional (beneath a
   * conditional of an strat_ITE strategy).
   */
  void finishInit(Node e,
                  NodeRole nrole,
                  std::map<Node, std::map<NodeRole, bool> >& visited,
                  bool isCond);
  /** helper for debug print
   *
   * Prints the node e with role nrole on Trace(c).
   *
   * (e, nrole) specify the strategy node in the graph we are currently
   * analyzing, visited stores the nodes we have already visited.
   *
   * ind is the current level of indentation (for debugging)
   */
  void debugPrint(const char* c,
                  Node e,
                  NodeRole nrole,
                  std::map<Node, std::map<NodeRole, bool> >& visited,
                  int ind);
  //------------------------------ end strategy registration
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, 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		* sygus_unif_strat
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
20
21		#include <map>
22		#include "expr/node.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28		class TermDbSygus;
29
30		/** roles for enumerators
31		*
32		* This indicates the role of an enumerator that is allocated by approaches
33		* for synthesis-by-unification (see details below).
34		* io : the enumerator should enumerate values that are overall solutions
35		* for the function-to-synthesize,
36		* ite_condition : the enumerator should enumerate values that are useful
37		* in ite conditions in the ITE strategy,
38		* concat_term : the enumerator should enumerate values that are used as
39		* components of string concatenation solutions.
40		*/
41		enum EnumRole
42		{
43		enum_invalid,
44		enum_io,
45		enum_ite_condition,
46		enum_concat_term,
47		};
48		std::ostream& operator<<(std::ostream& os, EnumRole r);
49
50		/** roles for strategy nodes
51		*
52		* This indicates the role of a strategy node, which is a subprocedure of
53		* SygusUnif::constructSolution (see details below).
54		* equal : the node constructed must be equal to the overall solution for
55		* the function-to-synthesize,
56		* string_prefix/suffix : the node constructed must be a prefix/suffix
57		* of the function-to-synthesize,
58		* ite_condition : the node constructed must be a condition that makes some
59		* active input examples true and some input examples false.
60		*/
61		enum NodeRole
62		{
63		role_invalid,
64		role_equal,
65		role_string_prefix,
66		role_string_suffix,
67		role_ite_condition,
68		};
69		std::ostream& operator<<(std::ostream& os, NodeRole r);
70
71		/** enumerator role for node role */
72		EnumRole getEnumeratorRoleForNodeRole(NodeRole r);
73
74		/** strategy types
75		*
76		* This indicates a strategy for synthesis-by-unification (see details below).
77		* ITE : strategy for constructing if-then-else solutions via decision
78		* tree learning techniques,
79		* CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
80		* solutions via a divide and conquer approach,
81		* ID : identity strategy used for calling strategies on child type through
82		* an identity function.
83		*/
84		enum StrategyType
85		{
86		strat_INVALID,
87		strat_ITE,
88		strat_CONCAT_PREFIX,
89		strat_CONCAT_SUFFIX,
90		strat_ID,
91		};
92		std::ostream& operator<<(std::ostream& os, StrategyType st);
93
94		/** virtual base class for context in synthesis-by-unification approaches */
95	47	class UnifContext
96		{
97		public:
98	47	virtual ~UnifContext() {}
99
100		/** Get the current role
101		*
102		* In a particular context when constructing solutions in synthesis by
103		* unification, we may be solving based on a modified role. For example,
104		* if we are currently synthesizing x in a solution ("a" ++ x), we are
105		* synthesizing the string suffix of the overall solution. In this case, this
106		* function returns role_string_suffix.
107		*/
108		virtual NodeRole getCurrentRole() = 0;
109		/** is return value modified?
110		*
111		* This returns true if we are currently in a state where the return value
112		* of the solution has been modified, e.g. by a previous node that solved
113		* for a string prefix.
114		*/
115	3578	bool isReturnValueModified() { return getCurrentRole() != role_equal; }
116		};
117
118		/**
119		* This class stores information regarding an enumerator, including
120		* information regarding the role of this enumerator (see EnumRole), its
121		* parent, whether it is templated, its slave enumerators, and so on.
122		*
123		* We say an enumerator is a master enumerator if it is the variable that
124		* we use to enumerate values for its sort. Master enumerators may have
125		* (possibly multiple) slave enumerators, stored in d_enum_slave. When
126		* constructing a sygus unifciation strategy, we make the first enumerator for
127		* each type a master enumerator, and any additional ones slaves of it.
128		*/
129	146	class EnumInfo
130		{
131		public:
132	146	EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
133		/** initialize this class
134		*
135		* role is the "role" the enumerator plays in the high-level strategy,
136		* which is one of enum_* above.
137		*/
138		void initialize(EnumRole role);
139		/** is this enumerator associated with a template? */
140	2501	bool isTemplated() { return !d_template.isNull(); }
141		/** set conditional
142		*
143		* This flag is set to true if this enumerator may not apply to all
144		* input/output examples. For example, if this enumerator is used
145		* as an output value beneath a conditional in an instance of strat_ITE,
146		* then this enumerator is conditional.
147		*/
148	69	void setConditional() { d_is_conditional = true; }
149		/** returns if this enumerator is conditional */
150	227	bool isConditional() { return d_is_conditional; }
151		/** get the role of this enumerator */
152	18005	EnumRole getRole() { return d_role; }
153		/** enumerator template
154		*
155		* If d_template non-null, enumerated values V are immediately transformed to
156		* d_template { d_template_arg -> V }.
157		*/
158		Node d_template;
159		Node d_template_arg;
160		/**
161		* Slave enumerators of this enumerator. These are other enumerators that
162		* have the same type, but a different role in the strategy tree. We
163		* generally
164		* only use one enumerator per type, and hence these slaves are notified when
165		* values are enumerated for this enumerator.
166		*/
167		std::vector<Node> d_enum_slave;
168
169		private:
170		/** the role of this enumerator (one of enum_* above). */
171		EnumRole d_role;
172		/** is this enumerator conditional */
173		bool d_is_conditional;
174		};
175
176		class EnumTypeInfoStrat;
177
178		/** represents a node in the strategy graph
179		*
180		* It contains a list of possible strategies which are tried during calls
181		* to constructSolution.
182		*/
183		class StrategyNode
184		{
185		public:
186	134	StrategyNode() {}
187		~StrategyNode();
188		/** the set of strategies to try at this node in the strategy graph */
189		std::vector<EnumTypeInfoStrat*> d_strats;
190		};
191
192		/**
193		* Stores all enumerators and strategies for a SyGuS datatype type.
194		*/
195	84	class EnumTypeInfo
196		{
197		public:
198	84	EnumTypeInfo() {}
199		/** the type that this information is for */
200		TypeNode d_this_type;
201		/** map from enum roles to enumerators for this type */
202		std::map<EnumRole, Node> d_enum;
203		/** map from node roles to strategy nodes */
204		std::map<NodeRole, StrategyNode> d_snodes;
205		/** get strategy node for node role */
206		StrategyNode& getStrategyNode(NodeRole nrole);
207		};
208
209		/** represents a strategy for a SyGuS datatype type
210		*
211		* This represents a possible strategy to apply when processing a strategy
212		* node in constructSolution. When applying the strategy represented by this
213		* class, we may make recursive calls to the children of the strategy,
214		* given in d_cenum. If all recursive calls to constructSolution for these
215		* children are successful, say:
216		* constructSolution( d_cenum[1], ... ) = t1,
217		* ...,
218		* constructSolution( d_cenum[n], ... ) = tn,
219		* Then, the solution returned by this strategy is
220		* d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
221		* where * is application of substitution.
222		*/
223	186	class EnumTypeInfoStrat
224		{
225		public:
226		/** the type of strategy this represents */
227		StrategyType d_this;
228		/** the sygus datatype constructor that induced this strategy
229		*
230		* For example, this may be a sygus datatype whose sygus operator is ITE,
231		* if the strategy type above is strat_ITE.
232		*/
233		Node d_cons;
234		/** children of this strategy */
235		std::vector<std::pair<Node, NodeRole> > d_cenum;
236		/** the arguments for the (templated) solution */
237		std::vector<Node> d_sol_templ_args;
238		/** the template for the solution */
239		Node d_sol_templ;
240		/** Returns true if argument is valid strategy in unification context x */
241		bool isValid(UnifContext& x);
242		};
243
244		/**
245		* flags for extra restrictions to be inferred during redundant operators
246		* learning
247		*/
248	59	struct StrategyRestrictions
249		{
250	59	StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true)
251		{
252	59	}
253		/**
254		* if this flag is true then staticLearnRedundantOps will also try to make
255		* the return value of boolean ITEs to be restricted to constants
256		*/
257		bool d_iteReturnBoolConst;
258		/**
259		* if this flag is true then staticLearnRedundantOps will also try to make
260		* the condition values of ITEs to be restricted to atoms
261		*/
262		bool d_iteCondOnlyAtoms;
263		/**
264		* A list of unused strategies. This maps strategy points to the indices
265		* in StrategyNode::d_strats that are not used by the caller of
266		* staticLearnRedundantOps, and hence should not be taken into account
267		* when doing redundant operator learning.
268		*/
269		std::map<Node, std::unordered_set<unsigned>> d_unused_strategies;
270		};
271
272		/**
273		* Stores strategy and enumeration information for a function-to-synthesize.
274		*
275		* When this class is initialized, we construct a "strategy tree" based on
276		* the grammar of the function to synthesize f. This tree is represented by
277		* the above classes.
278		*/
279	59	class SygusUnifStrategy
280		{
281		public:
282	59	SygusUnifStrategy() : d_tds(nullptr) {}
283		/** initialize
284		*
285		* This initializes this class with function-to-synthesize f. We also call
286		* f the candidate variable.
287		*
288		* This call constructs a set of enumerators for the relevant subfields of
289		* the grammar of f and adds them to enums.
290		*/
291		void initialize(TermDbSygus* tds, Node f, std::vector<Node>& enums);
292		/** Get the root enumerator for this class */
293		Node getRootEnumerator() const;
294		/**
295		* Get the enumerator info for enumerator e, where e must be an enumerator
296		* initialized by this class (in enums after a call to initialize).
297		*/
298		EnumInfo& getEnumInfo(Node e);
299		/**
300		* Get the enumerator type info for sygus type t, where t must be the type
301		* of some enumerator initialized by this class
302		*/
303		EnumTypeInfo& getEnumTypeInfo(TypeNode tn);
304
305		/** static learn redundant operators
306		*
307		* This learns static lemmas for pruning enumerative space based on the
308		* strategy for the function-to-synthesize of this class, and stores these
309		* into strategy_lemmas.
310		*
311		* These may correspond to static symmetry breaking predicates (for example,
312		* those that exclude ITE from enumerators whose role is enum_io when the
313		* strategy is ITE_strat).
314		*
315		* then the module may also try to apply the given pruning restrictions (see
316		* StrategyRestrictions for more details)
317		*/
318		void staticLearnRedundantOps(
319		std::map<Node, std::vector<Node>>& strategy_lemmas,
320		StrategyRestrictions& restrictions);
321		/**
322		* creates the default restrictions when they are not given and calls the
323		* above function
324		*/
325		void staticLearnRedundantOps(
326		std::map<Node, std::vector<Node>>& strategy_lemmas);
327
328		/** debug print this strategy on Trace c */
329		void debugPrint(const char* c);
330
331		private:
332		/** pointer to the term database sygus */
333		TermDbSygus* d_tds;
334		/** The candidate variable this strategy is for */
335		Node d_candidate;
336		/** maps enumerators to relevant information */
337		std::map<Node, EnumInfo> d_einfo;
338		/** list of all enumerators for the function-to-synthesize */
339		std::vector<Node> d_esym_list;
340		/** Info for sygus datatype type occurring in a field of d_root */
341		std::map<TypeNode, EnumTypeInfo> d_tinfo;
342		/**
343		* The root sygus datatype for the function-to-synthesize,
344		* which encodes the overall syntactic restrictions on the space
345		* of solutions.
346		*/
347		TypeNode d_root;
348		/**
349		* Maps sygus datatypes to their master enumerator. This is the (single)
350		* enumerator of that type that we enumerate values for.
351		*/
352		std::map<TypeNode, Node> d_master_enum;
353		/** Initialize necessary information for (sygus) type tn */
354		void initializeType(TypeNode tn);
355
356		//-----------------------debug printing
357		/** print ind indentations on trace c */
358		static void indent(const char* c, int ind);
359		//-----------------------end debug printing
360
361		//------------------------------ strategy registration
362		/** build strategy graph
363		*
364		* This builds the strategy for enumerated values of type tn for the given
365		* role of nrole, for solutions to function-to-synthesize of this class.
366		*/
367		void buildStrategyGraph(TypeNode tn, NodeRole nrole);
368		/** register enumerator
369		*
370		* This registers that et is an enumerator of type tn, having enumerator
371		* role enum_role.
372		*
373		* inSearch is whether we will enumerate values based on this enumerator.
374		* A strategy node is represented by a (enumerator, node role) pair. Hence,
375		* we may use enumerators for which this flag is false to represent strategy
376		* nodes that have child strategies.
377		*/
378		void registerStrategyPoint(Node et,
379		TypeNode tn,
380		EnumRole enum_role,
381		bool inSearch);
382		/** infer template */
383		bool inferTemplate(unsigned k,
384		Node n,
385		std::map<Node, unsigned>& templ_var_index,
386		std::map<unsigned, unsigned>& templ_injection);
387		/** helper for static learn redundant operators
388		*
389		* (e, nrole) specify the strategy node in the graph we are currently
390		* analyzing, visited stores the nodes we have already visited.
391		*
392		* This method builds the mapping needs_cons, which maps (master) enumerators
393		* to a map from the constructors that it needs.
394		*/
395		void staticLearnRedundantOps(
396		Node e,
397		NodeRole nrole,
398		std::map<Node, std::map<NodeRole, bool>>& visited,
399		std::map<Node, std::map<unsigned, bool>>& needs_cons,
400		StrategyRestrictions& restrictions);
401		/** finish initialization of the strategy tree
402		*
403		* (e, nrole) specify the strategy node in the graph we are currently
404		* analyzing, visited stores the nodes we have already visited.
405		*
406		* isCond is whether the current enumerator is conditional (beneath a
407		* conditional of an strat_ITE strategy).
408		*/
409		void finishInit(Node e,
410		NodeRole nrole,
411		std::map<Node, std::map<NodeRole, bool> >& visited,
412		bool isCond);
413		/** helper for debug print
414		*
415		* Prints the node e with role nrole on Trace(c).
416		*
417		* (e, nrole) specify the strategy node in the graph we are currently
418		* analyzing, visited stores the nodes we have already visited.
419		*
420		* ind is the current level of indentation (for debugging)
421		*/
422		void debugPrint(const char* c,
423		Node e,
424		NodeRole nrole,
425		std::map<Node, std::map<NodeRole, bool> >& visited,
426		int ind);
427		//------------------------------ end strategy registration
428		};
429
430		} // namespace quantifiers
431		} // namespace theory
432		} // namespace cvc5
433
434		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */