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