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