Infrastructure for variable agnostic sygus enumerators (#2511)

2 files changed, 245 insertions, 28 deletions

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 1f4e34c1f..a10ecc566 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -343,6 +343,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
           }
         }else{
           // no arguments to synthesis functions
+          d_var_list[tn].clear();
         }
         // register connected types
         for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
@@ -421,11 +422,51 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
   }
 }
 
+/** A trie indexed by types that assigns unique identifiers to nodes. */
+class TypeNodeIdTrie
+{
+ public:
+  /** children of this node */
+  std::map<TypeNode, TypeNodeIdTrie> d_children;
+  /** the data stored at this node */
+  std::vector<Node> d_data;
+  /** add v to this trie, indexed by types */
+  void add(Node v, std::vector<TypeNode>& types)
+  {
+    TypeNodeIdTrie* tnt = this;
+    for (unsigned i = 0, size = types.size(); i < size; i++)
+    {
+      tnt = &tnt->d_children[types[i]];
+    }
+    tnt->d_data.push_back(v);
+  }
+  /**
+   * Assign each node in this trie an identifier such that
+   * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
+   */
+  void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount)
+  {
+    if (!d_data.empty())
+    {
+      for (const Node& v : d_data)
+      {
+        assign[v] = idCount;
+      }
+      idCount++;
+    }
+    for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
+    {
+      c.second.assignIds(assign, idCount);
+    }
+  }
+};
+
 void TermDbSygus::registerEnumerator(Node e,
                                      Node f,
                                      SynthConjecture* conj,
                                      bool mkActiveGuard,
-                                     bool useSymbolicCons)
+                                     bool useSymbolicCons,
+                                     bool isVarAgnostic)
 {
   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
   {
@@ -441,15 +482,7 @@ void TermDbSygus::registerEnumerator(Node e,
   NodeManager* nm = NodeManager::currentNM();
   if( mkActiveGuard ){
     // make the guard
-    Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType()));
-    eg = d_quantEngine->getValuation().ensureLiteral( eg );
-    AlwaysAssert( !eg.isNull() );
-    d_quantEngine->getOutputChannel().requirePhase( eg, true );
-    //add immediate lemma
-    Node lem = nm->mkNode(OR, eg, eg.negate());
-    Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
-    d_quantEngine->getOutputChannel().lemma( lem );
-    d_enum_to_active_guard[e] = eg;
+    d_enum_to_active_guard[e] = nm->mkSkolem("eG", nm->booleanType());
   }
 
   Trace("sygus-db") << "  registering symmetry breaking clauses..."
@@ -459,35 +492,47 @@ void TermDbSygus::registerEnumerator(Node e,
   // breaking lemma templates for each relevant subtype of the grammar
   std::vector<TypeNode> sf_types;
   getSubfieldTypes(et, sf_types);
+  // maps variables to the list of subfield types they occur in
+  std::map<Node, std::vector<TypeNode> > type_occurs;
+  std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et);
+  Assert(itv != d_var_list.end());
+  for (const Node& v : itv->second)
+  {
+    type_occurs[v].clear();
+  }
   // for each type of subfield type of this enumerator
   for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
   {
     std::vector<unsigned> rm_indices;
     TypeNode stn = sf_types[i];
     Assert(stn.isDatatype());
-    const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype();
-    std::map<TypeNode, unsigned>::iterator itsa =
-        d_sym_cons_any_constant.find(stn);
-    if (itsa != d_sym_cons_any_constant.end())
+    const Datatype& dt = stn.getDatatype();
+    int anyC = getAnyConstantConsNum(stn);
+    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
-      if (!useSymbolicCons)
+      Expr sop = dt[i].getSygusOp();
+      Assert(!sop.isNull());
+      bool isAnyC = static_cast<int>(i) == anyC;
+      Node sopn = Node::fromExpr(sop);
+      if (type_occurs.find(sopn) != type_occurs.end())
+      {
+        // if it is a variable, store that it occurs in stn
+        type_occurs[sopn].push_back(stn);
+      }
+      else if (isAnyC && !useSymbolicCons)
       {
+        // if we are not using the any constant constructor
         // do not use the symbolic constructor
-        rm_indices.push_back(itsa->second);
+        rm_indices.push_back(i);
       }
-      else
+      else if (anyC != -1 && !isAnyC && useSymbolicCons)
       {
-        // can remove all other concrete constant constructors
-        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+        // if we are using the any constant constructor, do not use any
+        // concrete constant
+        Node c_op = getConsNumConst(stn, i);
+        if (!c_op.isNull())
         {
-          if (i != itsa->second)
-          {
-            Node c_op = getConsNumConst(stn, i);
-            if (!c_op.isNull())
-            {
-              rm_indices.push_back(i);
-            }
-          }
+          rm_indices.push_back(i);
         }
       }
     }
@@ -515,6 +560,33 @@ void TermDbSygus::registerEnumerator(Node e,
     }
   }
   Trace("sygus-db") << "  ...finished" << std::endl;
+
+  d_enum_var_agnostic[e] = isVarAgnostic;
+  if (isVarAgnostic)
+  {
+    // if not done so already, compute type class identifiers for each variable
+    if (d_var_subclass_id.find(et) == d_var_subclass_id.end())
+    {
+      d_var_subclass_id[et].clear();
+      TypeNodeIdTrie tnit;
+      for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+      {
+        tnit.add(to.first, to.second);
+      }
+      // 0 is reserved for "no type class id"
+      unsigned typeIdCount = 1;
+      tnit.assignIds(d_var_subclass_id[et], typeIdCount);
+      // assign the list and reverse map to index
+      for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+      {
+        Node v = to.first;
+        unsigned sc = d_var_subclass_id[et][v];
+        Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
+        d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size();
+        d_var_subclass_list[et][sc].push_back(v);
+      }
+    }
+  }
 }
 
 bool TermDbSygus::isEnumerator(Node e) const
@@ -561,6 +633,16 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
   return false;
 }
 
+bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
+{
+  std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e);
+  if (itus != d_enum_var_agnostic.end())
+  {
+    return itus->second;
+  }
+  return false;
+}
+
 void TermDbSygus::getEnumerators(std::vector<Node>& mts)
 {
   for (std::map<Node, SynthConjecture*>::iterator itm =
@@ -881,6 +963,82 @@ bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
   return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
 }
 
+unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const
+{
+  std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc =
+      d_var_subclass_id.find(tn);
+  if (itc == d_var_subclass_id.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n);
+  if (itcc == itc->second.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  return itcc->second;
+}
+
+unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const
+{
+  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
+      itv = d_var_subclass_list.find(tn);
+  if (itv == d_var_subclass_list.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+      itv->second.find(sc);
+  if (itvv == itv->second.end())
+  {
+    Assert(false);
+    return 0;
+  }
+  return itvv->second.size();
+}
+Node TermDbSygus::getVarSubclassIndex(TypeNode tn,
+                                      unsigned sc,
+                                      unsigned i) const
+{
+  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
+      itv = d_var_subclass_list.find(tn);
+  if (itv == d_var_subclass_list.end())
+  {
+    Assert(false);
+    return Node::null();
+  }
+  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+      itv->second.find(sc);
+  if (itvv == itv->second.end() || i >= itvv->second.size())
+  {
+    Assert(false);
+    return Node::null();
+  }
+  return itvv->second[i];
+}
+
+bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn,
+                                           Node v,
+                                           unsigned& index) const
+{
+  std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv =
+      d_var_subclass_list_index.find(tn);
+  if (itv == d_var_subclass_list_index.end())
+  {
+    return false;
+  }
+  std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v);
+  if (itvv == itv->second.end())
+  {
+    return false;
+  }
+  index = itvv->second;
+  return true;
+}
+
 bool TermDbSygus::isSymbolicConsApp(Node n) const
 {
   if (n.getKind() != APPLY_CONSTRUCTOR)
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index b7bdba3ab..361c6bae0 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -69,6 +69,10 @@ class TermDbSygus {
    * (see d_enum_to_active_guard),
    * useSymbolicCons : whether we want model values for e to include symbolic
    * constructors like the "any constant" variable.
+   * isVarAgnostic : if this flag is true, the enumerator will only generate
+   * values whose variables are in canonical order (for example, only x1-x2
+   * and not x2-x1 will be generated, assuming x1 and x2 are in the same
+   * "subclass", see getSubclassForVar).
    *
    * Notice that enumerator e may not be one-to-one with f in
    * synthesis-through-unification approaches (e.g. decision tree construction
@@ -78,7 +82,8 @@ class TermDbSygus {
                           Node f,
                           SynthConjecture* conj,
                           bool mkActiveGuard = false,
-                          bool useSymbolicCons = false);
+                          bool useSymbolicCons = false,
+                          bool isVarAgnostic = false);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
@@ -89,6 +94,8 @@ class TermDbSygus {
   Node getActiveGuardForEnumerator(Node e) const;
   /** are we using symbolic constructors for enumerator e? */
   bool usingSymbolicConsForEnumerator(Node e) const;
+  /** is this enumerator agnostic to variables? */
+  bool isVariableAgnosticEnumerator(Node e) const;
   /** get all registered enumerators */
   void getEnumerators(std::vector<Node>& mts);
   /** Register symmetry breaking lemma
@@ -273,6 +280,8 @@ class TermDbSygus {
   std::map<Node, TypeNode> d_sb_lemma_to_type;
   /** mapping from symmetry breaking lemmas to size */
   std::map<Node, unsigned> d_sb_lemma_to_size;
+  /** enumerators to whether they are variable agnostic */
+  std::map<Node, bool> d_enum_var_agnostic;
   //------------------------------end enumerators
 
   //-----------------------------conversion from sygus to builtin
@@ -345,6 +354,17 @@ class TermDbSygus {
    * for this type.
    */
   std::map<TypeNode, bool> d_has_subterm_sym_cons;
+  /**
+   * Map from sygus types and bound variables to their type subclass id. Note
+   * type class identifiers are computed for each type of registered sygus
+   * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
+   */
+  std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_id;
+  /** the list of variables with given subclass */
+  std::map<TypeNode, std::map<unsigned, std::vector<Node> > >
+      d_var_subclass_list;
+  /** the index of each variable in the above list */
+  std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_list_index;
 
  public:  // general sygus utilities
   bool isRegistered(TypeNode tn) const;
@@ -390,6 +410,45 @@ class TermDbSygus {
    * Returns true if any subterm of type tn can be a symbolic constructor.
    */
   bool hasSubtermSymbolicCons(TypeNode tn) const;
+  //--------------------------------- variable subclasses
+  /** Get subclass id for variable
+   *
+   * This returns the "subclass" identifier for variable v in sygus
+   * type tn. A subclass identifier groups variables based on the sygus
+   * types they occur in:
+   *   A -> A + B | C + C | x | y | z | w | u
+   *   B -> y | z
+   *   C -> u
+   * The variables in this grammar can be grouped according to the sygus types
+   * they appear in:
+   *   { x,w } occur in A
+   *   { y,z } occur in A,B
+   *   { u } occurs in A,C
+   * We say that e.g. x, w are in the same subclass.
+   *
+   * If this method returns 0, then v is not a variable in sygus type tn.
+   * Otherwise, this method returns a positive value n, such that
+   * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
+   * same subclass.
+   *
+   * The type tn should be the type of an enumerator registered to this
+   * database, where notice that we do not compute this information for the
+   * subfield types of the enumerator.
+   */
+  unsigned getSubclassForVar(TypeNode tn, Node v) const;
+  /**
+   * Get the number of variable in the subclass with identifier sc for type tn.
+   */
+  unsigned getNumSubclassVars(TypeNode tn, unsigned sc) const;
+  /** Get the i^th variable in the subclass with identifier sc for type tn */
+  Node getVarSubclassIndex(TypeNode tn, unsigned sc, unsigned i) const;
+  /**
+   * Get the a variable's index in its subclass list. This method returns true
+   * iff variable v has been assigned a subclass in tn. It updates index to
+   * be v's index iff the method returns true.
+   */
+  bool getIndexInSubclassForVar(TypeNode tn, Node v, unsigned& index) const;
+  //--------------------------------- end variable subclasses
   /** return whether n is an application of a symbolic constructor */
   bool isSymbolicConsApp(Node n) const;
   /** can construct kind