Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/enum_stream_substitution.h	Lines:	6	6	100.0 %
Date:	2021-09-12	Branches:	2	4	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, 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.
 * ****************************************************************************
 *
 * Class for streaming concrete values (through substitutions) from
 * enumerated abstract ones.
 */
#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H

#include "expr/node.h"
#include "theory/quantifiers/sygus/enum_val_generator.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class TermDbSygus;

/** Streamer of different values according to variable permutations
 *
 * Generates a new value (modulo rewriting) when queried in which its variables
 * are permuted (see EnumStreamSubstitution for more details).
 */
class EnumStreamPermutation
{
 public:
  EnumStreamPermutation(TermDbSygus* tds);
  ~EnumStreamPermutation() {}
  /** resets utility
   *
   * for each subset of the variables in value (according to their
   * subclasses_classes), a permutation utility is initialized
   */
  void reset(Node value);
  /** computes next permutation, if any, of value
   *
   * a "next" permutation is determined by having at least one new permutation
   * in one of the variable subclasses in the value.
   *
   * For example, if the variables of value (OP x1 x2 x3 x4) are partioned into
   * {{x1, x4}, {x2, x3}} then the sequence of getNext() is
   *
   * (OP x4 x2 x3 x1)
   * (OP x1 x3 x2 x4)
   * (OP x4 x3 x2 x1)
   *
   * Moreover, new values are only considered if they are unique modulo
   * rewriting. If for example OP were "+", then no next value would exist,
   * while if OP were "-" the only next value would be: (- x4 x2 x3 x1)
   *
   * Since the same variable can occur in different subfield types (and
   * therefore their datatype equivalents would have different types) a map from
   * variables to sets of constructors (see var_cons) is used to build
   * substitutions in a proper way when generating different combinations.
   */
  Node getNext();
  /** retrieve variables in class with given id */
  const std::vector<Node>& getVarsClass(unsigned id) const;
  /** retrieve number of variables being permuted from subclass with given id */
  unsigned getVarClassSize(unsigned id) const;

 private:
  /** sygus term database of current quantifiers engine */
  TermDbSygus* d_tds;
  /** maps subclass ids to subset of d_vars with that subclass id */
  std::map<unsigned, std::vector<Node>> d_var_classes;
  /** maps variables to subfield types with constructors for
   * the that variable, which are themselves associated with the respective
   * constructors */
  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
  /** whether first query */
  bool d_first;
  /** value to which we are generating permutations */
  Node d_value;
  /** generated permutations (modulo rewriting) */
  std::unordered_set<Node> d_perm_values;
  /** retrieves variables occurring in value */
  void collectVars(Node n,
                   std::vector<Node>& vars,
                   std::unordered_set<Node>& visited);
  /** Utility for stepwise application of Heap's algorithm for permutation
   *
   * see https://en.wikipedia.org/wiki/Heap%27s_algorithm
   */
  class PermutationState
  {
   public:
    PermutationState(const std::vector<Node>& vars);
    /** computes next permutation, i.e. execute one step of Heap's algorithm
     *
     * returns true if one exists, false otherwise
     *
     * when a new permutation is generated the the new variable arrangement is
     * stored in d_last_perm (in terms of d_vars' indices)
     */
    bool getNextPermutation();
    /** resets permutation state to initial variable ordering */
    void reset();
    /** retrieves last variable permutation
     *
     * vars is populated with the new variable arrangement
     */
    void getLastPerm(std::vector<Node>& vars);
    /** retrieve variables being permuted */
    const std::vector<Node>& getVars() const;

   private:
    /** variables being permuted */
    std::vector<Node> d_vars;
    /** last computed permutation of variables */
    std::vector<unsigned> d_last_perm;
    /** auxiliary position list for generating permutations */
    std::vector<unsigned> d_seq;
    /** current index being permuted */
    unsigned d_curr_ind;
  };
  /** permutation state of each variable subclass */
  std::vector<PermutationState> d_perm_state_class;
  /** current variable subclass being permuted */
  unsigned d_curr_ind;
};

/** Streamer of concrete values for enumerator
 *
 * When a given enumerator is "variable agnostic", only values in which
 * variables are ordered are chosen for it (see
 * TermDbSygus::registerEnumerator). If such values are seen as "abstract", in
 * the sense that each represent a set of values, this class can be used to
 * stream all the concrete values that correspond to them.
 *
 * For example a variable agnostic enumerator that contains three variables, x1,
 * x2, x3, in which x1 < x2 < x3, for which an "abstract" value (OP x1 x2) is
 * derived, will lead to the stream of "concrete" values
 *
 * (OP x1 x2)
 * (OP x1 x3)
 * (OP x2 x3)
 *
 * (OP x2 x1)
 * (OP x3 x1)
 * (OP x3 x2)
 *
 * in which for each permutation of the variables in the abstract value ([x1,
 * x2] and [x2, x1] in the above) we generate all the substitutions through
 * ordered combinations of the variables of the enumerator ([x1, x2], [x1, x3],
 * and [x2, x3] in the above).
 *
 * Moreover the permutations are generated modulo rewriting, s.t. if two
 * permutations are equivalent, only one is used.
 *
 * It should be noted that the variables of a variable agnostic enumerator are
 * kept in independent "subclasses" (see TermDbSygus::getSubclassForVar).
 * Therefore when streaming concrete values, permutations and combinations are
 * generated by the product of the permutations and combinations of each class.
 */
class EnumStreamSubstitution
{
 public:
  EnumStreamSubstitution(TermDbSygus* tds);
  ~EnumStreamSubstitution() {}
  /** initializes utility
   *
   * the combinations are generated from a initial set of variables (for now all
   * variables in given type).
   */
  void initialize(TypeNode tn);
  /** resets value for which substitutions will be generated through
   * combinations
   *
   * For each variable subclass in this utility, a subset is chosen with as
   * many variables as in the same variable subclass of value's variables.
   *
   * The combinations are performed modulo subclasses. For each subclass of the
   * given variables, a combination utility is initialized.
   *
   * For example, if the initial variable set is partioned into
   *
   * {1 -> {x1, x4}, 2 -> {x2, x3, x6}, 3 -> {x5}}
   *
   * and value's variables into
   *
   * {1 -> {x1, x4}, 2 -> {x2}, 3 -> {}}
   *
   * then the combination utilities are initialized such that for class 1 all
   * ordered subsets with two variables are chosen; for class 2 all ordered
   * subsets with one variable; and for class 3 no combination can be chosen.
   */
  void resetValue(Node value);
  /** computes next combination, if any, of value
   *
   * a "next" combination is determined by having at least one new combination
   * in one of the variable subclasses in the initial set of variables. If no
   * new combination exists, the cycle restarts with a new base value generated
   * by EnumStreamPermutation::getNext() (see above).
   *
   * This layered approach (of deriving all combinations for each permutation)
   * allows to consider only ordered combinations to generate all possible
   * variations of the base value. See the example in EnumStreamSubstitution for
   * further details.
   */
  Node getNext();

 private:
  /** sygus term database of current quantifiers engine */
  TermDbSygus* d_tds;
  /** type this utility has been initialized for */
  TypeNode d_tn;
  /** current value */
  Node d_value;
  /** maps subclass ids to d_tn's variables with that subclass id */
  std::map<unsigned, std::vector<Node>> d_var_classes;
  /** maps variables to subfield types with constructors for
   * the that variable, which are themselves associated with the respective
   * constructors */
  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
  /** last value generated after a combination
   *
   * If getNext() has been called, this is the return value of the most recent
   * call to getNext(). Otherwise, this value is null.
   */
  Node d_last;
  /** generated combinations */
  std::unordered_set<Node> d_comb_values;
  /** permutation utility */
  EnumStreamPermutation d_stream_permutations;
  /** Utility for stepwise generation of ordered subsets of size k from n
   * variables */
  class CombinationState
  {
   public:
    CombinationState(unsigned n,
                     unsigned k,
                     unsigned subclass_id,
                     const std::vector<Node>& vars);
    /** computes next combination
     *
     * returns true if one exists, false otherwise
     */
    bool getNextCombination();
    /** resets combination state to first k variables in vars */
    void reset();
    /** retrieves last variable combination
     *
     * variables in new combination are stored in argument vars
     */
    void getLastComb(std::vector<Node>& vars);
    /** retrieve subclass id */
    const unsigned getSubclassId() const;

   private:
    /** subclass id of variables being combined */
    unsigned d_subclass_id;
    /** number of variables */
    unsigned d_n;
    /** size of subset */
    unsigned d_k;
    /** last combination state */
    std::vector<unsigned> d_last_comb;
    /** variables from which combination is extracted */
    std::vector<Node> d_vars;
  };
  /** combination state for each variable subclass */
  std::vector<CombinationState> d_comb_state_class;
  /** current class being combined */
  unsigned d_curr_ind;
};

/**
 * An enumerated value generator based on the above class. This is
 * SynthConjecture's interface to using the above utility.
 */
class EnumStreamConcrete : public EnumValGenerator
{
 public:
  EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {}
  /** initialize this class with enumerator e */
  void initialize(Node e) override;
  /** get that value v was enumerated */
  void addValue(Node v) override;
  /** increment */
  bool increment() override;
  /** get the current value enumerated by this class */
  Node getCurrent() override;

 private:
  /** stream substitution utility */
  EnumStreamSubstitution d_ess;
  /** the current term generated by this class */
  Node d_currTerm;
};

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

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, 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		* Class for streaming concrete values (through substitutions) from
14		* enumerated abstract ones.
15		*/
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
20
21		#include "expr/node.h"
22		#include "theory/quantifiers/sygus/enum_val_generator.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28		class TermDbSygus;
29
30		/** Streamer of different values according to variable permutations
31		*
32		* Generates a new value (modulo rewriting) when queried in which its variables
33		* are permuted (see EnumStreamSubstitution for more details).
34		*/
35		class EnumStreamPermutation
36		{
37		public:
38		EnumStreamPermutation(TermDbSygus* tds);
39	1	~EnumStreamPermutation() {}
40		/** resets utility
41		*
42		* for each subset of the variables in value (according to their
43		* subclasses_classes), a permutation utility is initialized
44		*/
45		void reset(Node value);
46		/** computes next permutation, if any, of value
47		*
48		* a "next" permutation is determined by having at least one new permutation
49		* in one of the variable subclasses in the value.
50		*
51		* For example, if the variables of value (OP x1 x2 x3 x4) are partioned into
52		* {{x1, x4}, {x2, x3}} then the sequence of getNext() is
53		*
54		* (OP x4 x2 x3 x1)
55		* (OP x1 x3 x2 x4)
56		* (OP x4 x3 x2 x1)
57		*
58		* Moreover, new values are only considered if they are unique modulo
59		* rewriting. If for example OP were "+", then no next value would exist,
60		* while if OP were "-" the only next value would be: (- x4 x2 x3 x1)
61		*
62		* Since the same variable can occur in different subfield types (and
63		* therefore their datatype equivalents would have different types) a map from
64		* variables to sets of constructors (see var_cons) is used to build
65		* substitutions in a proper way when generating different combinations.
66		*/
67		Node getNext();
68		/** retrieve variables in class with given id */
69		const std::vector<Node>& getVarsClass(unsigned id) const;
70		/** retrieve number of variables being permuted from subclass with given id */
71		unsigned getVarClassSize(unsigned id) const;
72
73		private:
74		/** sygus term database of current quantifiers engine */
75		TermDbSygus* d_tds;
76		/** maps subclass ids to subset of d_vars with that subclass id */
77		std::map<unsigned, std::vector<Node>> d_var_classes;
78		/** maps variables to subfield types with constructors for
79		* the that variable, which are themselves associated with the respective
80		* constructors */
81		std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
82		/** whether first query */
83		bool d_first;
84		/** value to which we are generating permutations */
85		Node d_value;
86		/** generated permutations (modulo rewriting) */
87		std::unordered_set<Node> d_perm_values;
88		/** retrieves variables occurring in value */
89		void collectVars(Node n,
90		std::vector<Node>& vars,
91		std::unordered_set<Node>& visited);
92		/** Utility for stepwise application of Heap's algorithm for permutation
93		*
94		* see https://en.wikipedia.org/wiki/Heap%27s_algorithm
95		*/
96	3	class PermutationState
97		{
98		public:
99		PermutationState(const std::vector<Node>& vars);
100		/** computes next permutation, i.e. execute one step of Heap's algorithm
101		*
102		* returns true if one exists, false otherwise
103		*
104		* when a new permutation is generated the the new variable arrangement is
105		* stored in d_last_perm (in terms of d_vars' indices)
106		*/
107		bool getNextPermutation();
108		/** resets permutation state to initial variable ordering */
109		void reset();
110		/** retrieves last variable permutation
111		*
112		* vars is populated with the new variable arrangement
113		*/
114		void getLastPerm(std::vector<Node>& vars);
115		/** retrieve variables being permuted */
116		const std::vector<Node>& getVars() const;
117
118		private:
119		/** variables being permuted */
120		std::vector<Node> d_vars;
121		/** last computed permutation of variables */
122		std::vector<unsigned> d_last_perm;
123		/** auxiliary position list for generating permutations */
124		std::vector<unsigned> d_seq;
125		/** current index being permuted */
126		unsigned d_curr_ind;
127		};
128		/** permutation state of each variable subclass */
129		std::vector<PermutationState> d_perm_state_class;
130		/** current variable subclass being permuted */
131		unsigned d_curr_ind;
132		};
133
134		/** Streamer of concrete values for enumerator
135		*
136		* When a given enumerator is "variable agnostic", only values in which
137		* variables are ordered are chosen for it (see
138		* TermDbSygus::registerEnumerator). If such values are seen as "abstract", in
139		* the sense that each represent a set of values, this class can be used to
140		* stream all the concrete values that correspond to them.
141		*
142		* For example a variable agnostic enumerator that contains three variables, x1,
143		* x2, x3, in which x1 < x2 < x3, for which an "abstract" value (OP x1 x2) is
144		* derived, will lead to the stream of "concrete" values
145		*
146		* (OP x1 x2)
147		* (OP x1 x3)
148		* (OP x2 x3)
149		*
150		* (OP x2 x1)
151		* (OP x3 x1)
152		* (OP x3 x2)
153		*
154		* in which for each permutation of the variables in the abstract value ([x1,
155		* x2] and [x2, x1] in the above) we generate all the substitutions through
156		* ordered combinations of the variables of the enumerator ([x1, x2], [x1, x3],
157		* and [x2, x3] in the above).
158		*
159		* Moreover the permutations are generated modulo rewriting, s.t. if two
160		* permutations are equivalent, only one is used.
161		*
162		* It should be noted that the variables of a variable agnostic enumerator are
163		* kept in independent "subclasses" (see TermDbSygus::getSubclassForVar).
164		* Therefore when streaming concrete values, permutations and combinations are
165		* generated by the product of the permutations and combinations of each class.
166		*/
167		class EnumStreamSubstitution
168		{
169		public:
170		EnumStreamSubstitution(TermDbSygus* tds);
171	1	~EnumStreamSubstitution() {}
172		/** initializes utility
173		*
174		* the combinations are generated from a initial set of variables (for now all
175		* variables in given type).
176		*/
177		void initialize(TypeNode tn);
178		/** resets value for which substitutions will be generated through
179		* combinations
180		*
181		* For each variable subclass in this utility, a subset is chosen with as
182		* many variables as in the same variable subclass of value's variables.
183		*
184		* The combinations are performed modulo subclasses. For each subclass of the
185		* given variables, a combination utility is initialized.
186		*
187		* For example, if the initial variable set is partioned into
188		*
189		* {1 -> {x1, x4}, 2 -> {x2, x3, x6}, 3 -> {x5}}
190		*
191		* and value's variables into
192		*
193		* {1 -> {x1, x4}, 2 -> {x2}, 3 -> {}}
194		*
195		* then the combination utilities are initialized such that for class 1 all
196		* ordered subsets with two variables are chosen; for class 2 all ordered
197		* subsets with one variable; and for class 3 no combination can be chosen.
198		*/
199		void resetValue(Node value);
200		/** computes next combination, if any, of value
201		*
202		* a "next" combination is determined by having at least one new combination
203		* in one of the variable subclasses in the initial set of variables. If no
204		* new combination exists, the cycle restarts with a new base value generated
205		* by EnumStreamPermutation::getNext() (see above).
206		*
207		* This layered approach (of deriving all combinations for each permutation)
208		* allows to consider only ordered combinations to generate all possible
209		* variations of the base value. See the example in EnumStreamSubstitution for
210		* further details.
211		*/
212		Node getNext();
213
214		private:
215		/** sygus term database of current quantifiers engine */
216		TermDbSygus* d_tds;
217		/** type this utility has been initialized for */
218		TypeNode d_tn;
219		/** current value */
220		Node d_value;
221		/** maps subclass ids to d_tn's variables with that subclass id */
222		std::map<unsigned, std::vector<Node>> d_var_classes;
223		/** maps variables to subfield types with constructors for
224		* the that variable, which are themselves associated with the respective
225		* constructors */
226		std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
227		/** last value generated after a combination
228		*
229		* If getNext() has been called, this is the return value of the most recent
230		* call to getNext(). Otherwise, this value is null.
231		*/
232		Node d_last;
233		/** generated combinations */
234		std::unordered_set<Node> d_comb_values;
235		/** permutation utility */
236		EnumStreamPermutation d_stream_permutations;
237		/** Utility for stepwise generation of ordered subsets of size k from n
238		* variables */
239	3	class CombinationState
240		{
241		public:
242		CombinationState(unsigned n,
243		unsigned k,
244		unsigned subclass_id,
245		const std::vector<Node>& vars);
246		/** computes next combination
247		*
248		* returns true if one exists, false otherwise
249		*/
250		bool getNextCombination();
251		/** resets combination state to first k variables in vars */
252		void reset();
253		/** retrieves last variable combination
254		*
255		* variables in new combination are stored in argument vars
256		*/
257		void getLastComb(std::vector<Node>& vars);
258		/** retrieve subclass id */
259		const unsigned getSubclassId() const;
260
261		private:
262		/** subclass id of variables being combined */
263		unsigned d_subclass_id;
264		/** number of variables */
265		unsigned d_n;
266		/** size of subset */
267		unsigned d_k;
268		/** last combination state */
269		std::vector<unsigned> d_last_comb;
270		/** variables from which combination is extracted */
271		std::vector<Node> d_vars;
272		};
273		/** combination state for each variable subclass */
274		std::vector<CombinationState> d_comb_state_class;
275		/** current class being combined */
276		unsigned d_curr_ind;
277		};
278
279		/**
280		* An enumerated value generator based on the above class. This is
281		* SynthConjecture's interface to using the above utility.
282		*/
283	2	class EnumStreamConcrete : public EnumValGenerator
284		{
285		public:
286	1	EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {}
287		/** initialize this class with enumerator e */
288		void initialize(Node e) override;
289		/** get that value v was enumerated */
290		void addValue(Node v) override;
291		/** increment */
292		bool increment() override;
293		/** get the current value enumerated by this class */
294		Node getCurrent() override;
295
296		private:
297		/** stream substitution utility */
298		EnumStreamSubstitution d_ess;
299		/** the current term generated by this class */
300		Node d_currTerm;
301		};
302
303		} // namespace quantifiers
304		} // namespace theory
305		} // namespace cvc5
306
307		#endif