1 files changed, 68 insertions, 26 deletions
diff --git a/src/theory/quantifiers/sygus_grammar_cons.h b/src/theory/quantifiers/sygus_grammar_cons.h
index e8b09293c..4e486f88f 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus_grammar_cons.h
@@ -24,38 +24,72 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class CegConjecture;
+
 /** 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( QuantifiersEngine * qe );
-  ~CegGrammarConstructor(){}
-  /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
-  Node process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg );
-  /** is the syntax restricted? */
-  bool isSyntaxRestricted() { return d_is_syntax_restricted; }
-  /** does the syntax allow ITE expressions? */
-  bool hasSyntaxITE() { return d_has_ite; }
-  // make the default sygus datatype type corresponding to builtin type range
-  //   bvl is the set of free variables to include in the grammar
-  //   fun is for naming
-  //   extra_cons is a set of extra constant symbols to include in the grammar
-  static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons );
-  // 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::vector< Node > > extra_cons;
-    return mkSygusDefaultType( range, bvl, fun, extra_cons );
+ CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* 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,
+              std::map<Node, Node>& templates,
+              std::map<Node, Node>& templates_arg);
+ /** is the syntax restricted? */
+ bool isSyntaxRestricted() { return d_is_syntax_restricted; }
+ /** does the syntax allow ITE expressions? */
+ bool hasSyntaxITE() { return d_has_ite; }
+ /** make the default sygus datatype type corresponding to builtin type range
+ *   bvl is the set of free variables to include in the grammar
+ *   fun is for naming
+ *   extra_cons is a set of extra constant symbols to include in the grammar
+ *   term_irrelevant is a set of terms that should not be included in the
+ *      grammar.
+ */
+ static TypeNode mkSygusDefaultType(
+     TypeNode range,
+     Node bvl,
+     const std::string& fun,
+     std::map<TypeNode, std::vector<Node> >& extra_cons,
+     std::unordered_set<Node, NodeHashFunction>& 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::vector<Node> > extra_cons;
+   std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+   return mkSygusDefaultType(range, bvl, fun, extra_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 frammar
-  //   fun is for naming
+  /** 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 );
 private:
   /** reference to quantifier engine */
   QuantifiersEngine * d_qe;
+  /** parent conjecture
+  * This contains global information about the synthesis conjecture.
+  */
+  CegConjecture* d_parent;
   /** is the syntax restricted? */
   bool d_is_syntax_restricted;
   /** does the syntax allow ITE expressions? */
@@ -71,11 +105,19 @@ private:
   static void mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops );
   // collect the list of types that depend on type range
   static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
-  // helper function for function mkSygusDefaultGrammar
-  //   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::vector< Node > >& extra_cons, 
-                                     std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres );
+  /** 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::vector<Node> >& extra_cons,
+      std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
+      std::vector<CVC4::Datatype>& datatypes,
+      std::set<Type>& 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 );