Updates to interface for Sygus grammar construction. (#1323)

* Updates to interface for grammar construction.

* Minor

* Format

3 files changed, 121 insertions, 40 deletions

diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 3af623f13..5af8eafc8 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -50,7 +50,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
   d_ceg_si = new CegConjectureSingleInv(qe, this);
   d_ceg_pbe = new CegConjecturePbe(qe, this);
   d_ceg_proc = new CegConjectureProcess(qe);
-  d_ceg_gc = new CegGrammarConstructor(qe);
+  d_ceg_gc = new CegGrammarConstructor(qe, this);
 }
 
 CegConjecture::~CegConjecture() {
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index 6152417a5..f6b2ab07a 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -28,10 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-
-CegGrammarConstructor::CegGrammarConstructor( QuantifiersEngine * qe ) : 
-d_qe( qe ), d_is_syntax_restricted(false), d_has_ite(true){
-
+CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
+                                             CegConjecture* p)
+    : d_qe(qe), d_parent(p), d_is_syntax_restricted(false), d_has_ite(true)
+{
 }
 
 void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){
@@ -91,14 +92,30 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
     Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
     // sfvl may be null for constant synthesis functions
     Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+
     TypeNode tn;
     std::stringstream ss;
     ss << sf;
     if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
       tn = v.getType();
     }else{
+      // check which arguments are irrelevant
+      std::unordered_set<unsigned> arg_irrelevant;
+      // TODO (#1210) : get arg irrelevant based on conjecture-specific analysis
+      std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+      // convert to term
+      for (std::unordered_set<unsigned>::iterator ita = arg_irrelevant.begin();
+           ita != arg_irrelevant.end();
+           ++ita)
+      {
+        unsigned arg = *ita;
+        Assert(arg < sfvl.getNumChildren());
+        term_irrelevant.insert(sfvl[arg]);
+      }
+
       // make the default grammar
-      tn = mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
+      tn = mkSygusDefaultType(
+          v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant);
     }
     // check if there is a template
     std::map< Node, Node >::iterator itt = templates.find( sf );
@@ -283,13 +300,31 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::ve
   }
 }
 
-void CegGrammarConstructor::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 ) {
+void CegGrammarConstructor::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)
+{
+  Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
+                             << range << std::endl;
   // collect the variables
   std::vector<Node> sygus_vars;
   if( !bvl.isNull() ){
     for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
-      sygus_vars.push_back( bvl[i] );
+      if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
+      {
+        sygus_vars.push_back(bvl[i]);
+      }
+      else
+      {
+        Trace("sygus-grammar-def") << "...synth var " << bvl[i]
+                                   << " has been marked irrelevant."
+                                   << std::endl;
+      }
     }
   }
   //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
@@ -297,7 +332,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, con
   //}
   std::vector< std::vector< Expr > > ops;
   int startIndex = -1;
-  Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl;
   std::map< Type, Type > sygus_to_builtin;
 
   std::vector< TypeNode > types;
@@ -529,16 +563,21 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, con
   }
 }
 
-
-TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, 
-                                          std::map< TypeNode, std::vector< Node > >& extra_cons ) {
+TypeNode CegGrammarConstructor::mkSygusDefaultType(
+    TypeNode range,
+    Node bvl,
+    const std::string& fun,
+    std::map<TypeNode, std::vector<Node> >& extra_cons,
+    std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
+{
   Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
   for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){
     Trace("sygus-grammar-def") << "    ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
   }
   std::set<Type> unres;
   std::vector< CVC4::Datatype > datatypes;
-  mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres );
+  mkSygusDefaultGrammar(
+      range, bvl, fun, extra_cons, term_irrelevant, datatypes, unres);
   Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
   Assert( !datatypes.empty() );
   std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
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 );