Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_grammar_cons.h	Lines:	4	4	100.0 %
Date:	2021-08-01	Branches:	2	4	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Yoni Zohar, Haniel Barbosa
 *
 * 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 constructing inductive datatypes that correspond to
 * grammars that encode syntactic restrictions for SyGuS.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H

#include <map>
#include <vector>

#include "expr/attribute.h"
#include "expr/node.h"
#include "expr/sygus_datatype.h"

namespace cvc5 {
namespace theory {

/**
 * Attribute for associating a function-to-synthesize with a first order
 * variable whose type is a sygus datatype type that encodes its grammar.
 */
struct SygusSynthGrammarAttributeId
{
};
typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
    SygusSynthGrammarAttribute;

/**
 * Attribute for associating a function-to-synthesize with its formal argument
 * list.
 */
struct SygusSynthFunVarListAttributeId
{
};
typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
    SygusSynthFunVarListAttribute;

namespace quantifiers {

class SynthConjecture;
class TermDbSygus;

/**
 * Utility for constructing datatypes that correspond to syntactic restrictions,
 * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
 */
class CegGrammarConstructor
{
public:
 CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
 ~CegGrammarConstructor() {}
 /** process
  *
  * This converts node q based on its deep embedding
  * (Section 4 of Reynolds et al CAV 2015).
  * The syntactic restrictions are associated with
  * the functions-to-synthesize using the attribute
  * SygusSynthGrammarAttribute.
  * The arguments templates and template_args
  * indicate templates for the function to synthesize,
  * in particular the solution for the i^th function
  * to synthesis must be of the form
  *   templates[i]{ templates_arg[i] -> t }
  * for some t if !templates[i].isNull().
  */
 Node process(Node q,
              const std::map<Node, Node>& templates,
              const std::map<Node, Node>& templates_arg);
 /**
  * Same as above, but we have already determined that the set of first-order
  * datatype variables that will quantify the deep embedding conjecture are
  * the vector ebvl.
  */
 Node process(Node q,
              const std::map<Node, Node>& templates,
              const std::map<Node, Node>& templates_arg,
              const std::vector<Node>& ebvl);

 /** Is the syntax restricted? */
 bool isSyntaxRestricted() { return d_is_syntax_restricted; }

 /**
  * Make the default sygus datatype type corresponding to builtin type range
  * arguments:
  *   - bvl: the set of free variables to include in the grammar
  *   - fun: used for naming
  *   - extra_cons: a set of extra constant symbols to include in the grammar,
  *     regardless of their inclusion in the default grammar.
  *   - exclude_cons: used to exclude operators from the grammar,
  *   - term_irrelevant: a set of terms that should not be included in the
  *      grammar.
  *   - include_cons: a set of operators such that if this set is not empty,
  *     its elements that are in the default grammar (and only them)
  *     will be included.
  */
 static TypeNode mkSygusDefaultType(
     TypeNode range,
     Node bvl,
     const std::string& fun,
     std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
     std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
     std::map<TypeNode, std::unordered_set<Node>>& include_cons,
     std::unordered_set<Node>& term_irrelevant);

 /**
  * Make the default sygus datatype type corresponding to builtin type range.
  */
 static TypeNode mkSygusDefaultType(TypeNode range,
                                    Node bvl,
                                    const std::string& fun)
 {
   std::map<TypeNode, std::unordered_set<Node>> extra_cons;
   std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
   std::map<TypeNode, std::unordered_set<Node>> include_cons;
   std::unordered_set<Node> term_irrelevant;
   return mkSygusDefaultType(range,
                             bvl,
                             fun,
                             extra_cons,
                             exclude_cons,
                             include_cons,
                             term_irrelevant);
  }

  /** make the sygus datatype type that encodes the solution space (lambda
  * templ_arg. templ[templ_arg]) where templ_arg
  * has syntactic restrictions encoded by sygus type templ_arg_sygus_type
  *   bvl is the set of free variables to include in the grammar
  *   fun is for naming
  */
  static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
  /**
   * Returns true iff there are syntax restrictions on the
   * functions-to-synthesize of sygus conjecture q.
   */
  static bool hasSyntaxRestrictions(Node q);
  /**
   * Make the builtin constants for type "type" that should be included in a
   * sygus grammar, add them to vector ops.
   */
  static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
  /** Is it possible to construct a default grammar for type t? */
  static bool isHandledType(TypeNode t);
  /**
   * Convert node n based on deep embedding, see Section 4 of Reynolds et al
   * CAV 2015.
   *
   * This returns the result of converting n to its deep embedding based on
   * the mapping from functions to datatype variables, stored in
   * d_synth_fun_vars. This method should be called only after calling process
   * above.
   */
  Node convertToEmbedding(Node n);

 private:
  /** The sygus term database we are using */
  TermDbSygus* d_tds;
  /** parent conjecture
  * This contains global information about the synthesis conjecture.
  */
  SynthConjecture* d_parent;
  /**
   * Maps each synthesis function to its corresponding (first-order) sygus
   * datatype variable. This map is initialized by the process methods.
   */
  std::map<Node, Node> d_synth_fun_vars;
  /** is the syntax restricted? */
  bool d_is_syntax_restricted;
  /** collect terms */
  void collectTerms(Node n,
                    std::map<TypeNode, std::unordered_set<Node>>& consts);
  //---------------- grammar construction
  /** A class for generating sygus datatypes */
  class SygusDatatypeGenerator
  {
   public:
    SygusDatatypeGenerator(const std::string& name);
    ~SygusDatatypeGenerator() {}
    /**
     * Possibly add a constructor to d_sdt, based on the criteria mentioned
     * in this class below. For details see expr/sygus_datatype.h.
     */
    void addConstructor(Node op,
                        const std::string& name,
                        const std::vector<TypeNode>& consTypes,
                        int weight = -1);
    /**
     * Possibly add a constructor to d_sdt, based on the criteria mentioned
     * in this class below.
     */
    void addConstructor(Kind k,
                        const std::vector<TypeNode>& consTypes,
                        int weight = -1);
    /** Should we include constructor with operator op? */
    bool shouldInclude(Node op) const;
    /** The constructors that should be excluded. */
    std::unordered_set<Node> d_exclude_cons;
    /**
     * If this set is non-empty, then only include variables and constructors
     * from it.
     */
    std::unordered_set<Node> d_include_cons;
    /** The sygus datatype we are generating. */
    SygusDatatype d_sdt;
  };

  // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
  static TypeNode mkUnresolvedType(const std::string& name,
                                   std::set<TypeNode>& unres);
  // collect the list of types that depend on type range
  static void collectSygusGrammarTypesFor(TypeNode range,
                                          std::vector<TypeNode>& types);
  /** helper function for function mkSygusDefaultType
  * Collects a set of mutually recursive datatypes "datatypes" corresponding to
  * encoding type "range" to SyGuS.
  *   unres is used for the resulting call to mkMutualDatatypeTypes
  */
  static void mkSygusDefaultGrammar(
      TypeNode range,
      Node bvl,
      const std::string& fun,
      std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
      std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
      const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
      std::unordered_set<Node>& term_irrelevant,
      std::vector<SygusDatatypeGenerator>& sdts,
      std::set<TypeNode>& unres);

  // helper function for mkSygusTemplateType
  static TypeNode mkSygusTemplateTypeRec(Node templ,
                                         Node templ_arg,
                                         TypeNode templ_arg_sygus_type,
                                         Node bvl,
                                         const std::string& fun,
                                         unsigned& tcount);

  /**
   * Given a kind k, create a lambda operator with the given builtin input type
   * and an extra zero argument of that same type.  For example, for k = LEQ and
   * bArgType = Int, the operator will be lambda x : Int. x + 0.  Currently the
   * supported input types are Real (thus also Int) and BitVector.
   */
  static Node createLambdaWithZeroArg(Kind k,
                                      TypeNode bArgType);
  //---------------- end grammar construction
};

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

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Yoni Zohar, Haniel Barbosa
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 constructing inductive datatypes that correspond to
14		* grammars that encode syntactic restrictions for SyGuS.
15		*/
16
17		#include "cvc5_private.h"
18
19		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
20		#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
21
22		#include <map>
23		#include <vector>
24
25		#include "expr/attribute.h"
26		#include "expr/node.h"
27		#include "expr/sygus_datatype.h"
28
29		namespace cvc5 {
30		namespace theory {
31
32		/**
33		* Attribute for associating a function-to-synthesize with a first order
34		* variable whose type is a sygus datatype type that encodes its grammar.
35		*/
36		struct SygusSynthGrammarAttributeId
37		{
38		};
39		typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
40		SygusSynthGrammarAttribute;
41
42		/**
43		* Attribute for associating a function-to-synthesize with its formal argument
44		* list.
45		*/
46		struct SygusSynthFunVarListAttributeId
47		{
48		};
49		typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
50		SygusSynthFunVarListAttribute;
51
52		namespace quantifiers {
53
54		class SynthConjecture;
55		class TermDbSygus;
56
57		/**
58		* Utility for constructing datatypes that correspond to syntactic restrictions,
59		* and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
60		*/
61		class CegGrammarConstructor
62		{
63		public:
64		CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
65	1151	~CegGrammarConstructor() {}
66		/** process
67		*
68		* This converts node q based on its deep embedding
69		* (Section 4 of Reynolds et al CAV 2015).
70		* The syntactic restrictions are associated with
71		* the functions-to-synthesize using the attribute
72		* SygusSynthGrammarAttribute.
73		* The arguments templates and template_args
74		* indicate templates for the function to synthesize,
75		* in particular the solution for the i^th function
76		* to synthesis must be of the form
77		* templates[i]{ templates_arg[i] -> t }
78		* for some t if !templates[i].isNull().
79		*/
80		Node process(Node q,
81		const std::map<Node, Node>& templates,
82		const std::map<Node, Node>& templates_arg);
83		/**
84		* Same as above, but we have already determined that the set of first-order
85		* datatype variables that will quantify the deep embedding conjecture are
86		* the vector ebvl.
87		*/
88		Node process(Node q,
89		const std::map<Node, Node>& templates,
90		const std::map<Node, Node>& templates_arg,
91		const std::vector<Node>& ebvl);
92
93		/** Is the syntax restricted? */
94	331	bool isSyntaxRestricted() { return d_is_syntax_restricted; }
95
96		/**
97		* Make the default sygus datatype type corresponding to builtin type range
98		* arguments:
99		* - bvl: the set of free variables to include in the grammar
100		* - fun: used for naming
101		* - extra_cons: a set of extra constant symbols to include in the grammar,
102		* regardless of their inclusion in the default grammar.
103		* - exclude_cons: used to exclude operators from the grammar,
104		* - term_irrelevant: a set of terms that should not be included in the
105		* grammar.
106		* - include_cons: a set of operators such that if this set is not empty,
107		* its elements that are in the default grammar (and only them)
108		* will be included.
109		*/
110		static TypeNode mkSygusDefaultType(
111		TypeNode range,
112		Node bvl,
113		const std::string& fun,
114		std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
115		std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
116		std::map<TypeNode, std::unordered_set<Node>>& include_cons,
117		std::unordered_set<Node>& term_irrelevant);
118
119		/**
120		* Make the default sygus datatype type corresponding to builtin type range.
121		*/
122		static TypeNode mkSygusDefaultType(TypeNode range,
123		Node bvl,
124		const std::string& fun)
125		{
126		std::map<TypeNode, std::unordered_set<Node>> extra_cons;
127		std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
128		std::map<TypeNode, std::unordered_set<Node>> include_cons;
129		std::unordered_set<Node> term_irrelevant;
130		return mkSygusDefaultType(range,
131		bvl,
132		fun,
133		extra_cons,
134		exclude_cons,
135		include_cons,
136		term_irrelevant);
137		}
138
139		/** make the sygus datatype type that encodes the solution space (lambda
140		* templ_arg. templ[templ_arg]) where templ_arg
141		* has syntactic restrictions encoded by sygus type templ_arg_sygus_type
142		* bvl is the set of free variables to include in the grammar
143		* fun is for naming
144		*/
145		static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
146		/**
147		* Returns true iff there are syntax restrictions on the
148		* functions-to-synthesize of sygus conjecture q.
149		*/
150		static bool hasSyntaxRestrictions(Node q);
151		/**
152		* Make the builtin constants for type "type" that should be included in a
153		* sygus grammar, add them to vector ops.
154		*/
155		static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
156		/** Is it possible to construct a default grammar for type t? */
157		static bool isHandledType(TypeNode t);
158		/**
159		* Convert node n based on deep embedding, see Section 4 of Reynolds et al
160		* CAV 2015.
161		*
162		* This returns the result of converting n to its deep embedding based on
163		* the mapping from functions to datatype variables, stored in
164		* d_synth_fun_vars. This method should be called only after calling process
165		* above.
166		*/
167		Node convertToEmbedding(Node n);
168
169		private:
170		/** The sygus term database we are using */
171		TermDbSygus* d_tds;
172		/** parent conjecture
173		* This contains global information about the synthesis conjecture.
174		*/
175		SynthConjecture* d_parent;
176		/**
177		* Maps each synthesis function to its corresponding (first-order) sygus
178		* datatype variable. This map is initialized by the process methods.
179		*/
180		std::map<Node, Node> d_synth_fun_vars;
181		/** is the syntax restricted? */
182		bool d_is_syntax_restricted;
183		/** collect terms */
184		void collectTerms(Node n,
185		std::map<TypeNode, std::unordered_set<Node>>& consts);
186		//---------------- grammar construction
187		/** A class for generating sygus datatypes */
188	1735	class SygusDatatypeGenerator
189		{
190		public:
191		SygusDatatypeGenerator(const std::string& name);
192	2500	~SygusDatatypeGenerator() {}
193		/**
194		* Possibly add a constructor to d_sdt, based on the criteria mentioned
195		* in this class below. For details see expr/sygus_datatype.h.
196		*/
197		void addConstructor(Node op,
198		const std::string& name,
199		const std::vector<TypeNode>& consTypes,
200		int weight = -1);
201		/**
202		* Possibly add a constructor to d_sdt, based on the criteria mentioned
203		* in this class below.
204		*/
205		void addConstructor(Kind k,
206		const std::vector<TypeNode>& consTypes,
207		int weight = -1);
208		/** Should we include constructor with operator op? */
209		bool shouldInclude(Node op) const;
210		/** The constructors that should be excluded. */
211		std::unordered_set<Node> d_exclude_cons;
212		/**
213		* If this set is non-empty, then only include variables and constructors
214		* from it.
215		*/
216		std::unordered_set<Node> d_include_cons;
217		/** The sygus datatype we are generating. */
218		SygusDatatype d_sdt;
219		};
220
221		// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
222		static TypeNode mkUnresolvedType(const std::string& name,
223		std::set<TypeNode>& unres);
224		// collect the list of types that depend on type range
225		static void collectSygusGrammarTypesFor(TypeNode range,
226		std::vector<TypeNode>& types);
227		/** helper function for function mkSygusDefaultType
228		* Collects a set of mutually recursive datatypes "datatypes" corresponding to
229		* encoding type "range" to SyGuS.
230		* unres is used for the resulting call to mkMutualDatatypeTypes
231		*/
232		static void mkSygusDefaultGrammar(
233		TypeNode range,
234		Node bvl,
235		const std::string& fun,
236		std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
237		std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
238		const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
239		std::unordered_set<Node>& term_irrelevant,
240		std::vector<SygusDatatypeGenerator>& sdts,
241		std::set<TypeNode>& unres);
242
243		// helper function for mkSygusTemplateType
244		static TypeNode mkSygusTemplateTypeRec(Node templ,
245		Node templ_arg,
246		TypeNode templ_arg_sygus_type,
247		Node bvl,
248		const std::string& fun,
249		unsigned& tcount);
250
251		/**
252		* Given a kind k, create a lambda operator with the given builtin input type
253		* and an extra zero argument of that same type. For example, for k = LEQ and
254		* bArgType = Int, the operator will be lambda x : Int. x + 0. Currently the
255		* supported input types are Real (thus also Int) and BitVector.
256		*/
257		static Node createLambdaWithZeroArg(Kind k,
258		TypeNode bArgType);
259		//---------------- end grammar construction
260		};
261
262		} // namespace quantifiers
263		} // namespace theory
264		} // namespace cvc5
265
266		#endif