Adding infrastructure for normalizing SyGuS grammars (#1397)

* minor

Using string previously computed

* adding option

* starting module for simplifying grammars

* more

* more

* fix

* fix

* fix

* fix

* fix

* removing unused command

* removing unused command

* removing unnecessary quantifier engine

* adding lambda support

* transient

* reverting changes

* starting normalization of integers

* removing unnecessary objects

* using for_each

* rebuilding given datatypes

* recrating types as given

* bug fixing

* minor

* reverting space changes

* addressing review

* addressing review

3 files changed, 324 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index 68926eb34..05aa599b1 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -20,11 +20,11 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus_process_conj.h"
+#include "theory/quantifiers/sygus_grammar_norm.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
-using namespace std;
 
 namespace CVC4 {
 namespace theory {
@@ -118,6 +118,12 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
       tn = mkSygusDefaultType(
           v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant);
     }
+    // normalize type
+    if (options::sygusNormalizeGrammar())
+    {
+      SygusGrammarNorm sygus_norm(d_qe, d_parent);
+      tn = sygus_norm.normalizeSygusType(tn, sfvl);
+    }
     // check if there is a template
     std::map< Node, Node >::iterator itt = templates.find( sf );
     if( itt!=templates.end() ){
diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp
new file mode 100644
index 000000000..ea7722df0
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_norm.cpp
@@ -0,0 +1,168 @@
+/*********************                                                        */
+/*! \file sygus_grammar_norm.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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.\endverbatim
+ **
+ ** \brief implementation of class for for simplifying SyGuS grammars after they
+ ** are encoded into datatypes.
+ **/
+
+#include "theory/quantifiers/sygus_grammar_norm.h"
+
+#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"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TypeObject::TypeObject(std::string type_name) : d_dt(Datatype(type_name))
+{
+  d_tn = TypeNode::null();
+  /* Create an unresolved type */
+  d_unres_t = NodeManager::currentNM()
+                  ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
+                  .toType();
+}
+
+TypeObject::TypeObject(TypeNode src_tn, std::string type_name)
+    : d_dt(Datatype(type_name))
+{
+  d_tn = src_tn;
+  /* Create an unresolved type */
+  d_unres_t = NodeManager::currentNM()
+                  ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
+                  .toType();
+}
+
+SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p)
+    : d_qe(qe), d_parent(p), d_tds(d_qe->getTermDatabaseSygus())
+{
+}
+
+/* recursion depth is limited by the height of the types, which is small  */
+void SygusGrammarNorm::collectInfoFor(TypeNode tn,
+                                      std::vector<TypeObject>& tos,
+                                      std::map<TypeNode, Type>& tn_to_unres,
+                                      std::map<TypeNode, bool>& visited)
+{
+  if (visited.find(tn) != visited.end())
+  {
+    return;
+  }
+  visited[tn] = true;
+  Assert(tn.isDatatype());
+  /* Create new type name */
+  std::stringstream ss;
+  ss << tn << "_norm";
+  std::string type_name = ss.str();
+  /* Add to global accumulators */
+  tos.push_back(TypeObject(tn, type_name));
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  tn_to_unres[tn] = tos.back().d_unres_t;
+  /* Visit types of constructor arguments */
+  for (const DatatypeConstructor& cons : dt)
+  {
+    for (const DatatypeConstructorArg& arg : cons)
+    {
+      collectInfoFor(
+          TypeNode::fromType(
+              static_cast<SelectorType>(arg.getType()).getRangeType()),
+          tos,
+          tn_to_unres,
+          visited);
+    }
+  }
+}
+
+void SygusGrammarNorm::normalizeSygusInt(unsigned ind,
+                                         std::vector<TypeObject>& tos,
+                                         std::map<TypeNode, Type>& tn_to_unres,
+                                         Node sygus_vars)
+{
+  const Datatype& dt =
+      static_cast<DatatypeType>(tos[ind].d_tn.toType()).getDatatype();
+  Trace("sygus-grammar-normalize")
+      << "Normalizing integer type " << tos[ind].d_tn << " from datatype\n"
+      << dt << std::endl;
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+{
+  /* Make int_type and zero */
+  NodeManager* nm = NodeManager::currentNM();
+  /* Accumulates all typing information for normalization and reconstruction */
+  std::vector<TypeObject> tos;
+  /* Allows retrieving respective unresolved types for the sygus types of the
+   * original type nodes */
+  std::map<TypeNode, Type> tn_to_unres;
+  std::map<TypeNode, bool> visited;
+  collectInfoFor(tn, tos, tn_to_unres, visited);
+  /* Build datatypes TODO and normalize accordingly #1304 */
+  for (unsigned i = 0, size = tos.size(); i < size; ++i)
+  {
+    const Datatype& dt =
+        static_cast<DatatypeType>(tos[i].d_tn.toType()).getDatatype();
+    Trace("sygus-grammar-normalize")
+        << "Rebuild " << tos[i].d_tn << " from " << dt << std::endl;
+    /* Collect information to rebuild constructors */
+    for (const DatatypeConstructor& cons : dt)
+    {
+      Trace("sygus-grammar-normalize")
+          << "...for " << cons.getName() << std::endl;
+      /* Recover the sygus operator to not lose reference to the original
+       * operator (NOT, ITE, etc) */
+      tos[i].d_ops.push_back(cons.getSygusOp());
+      tos[i].d_cons_names.push_back(cons.getName());
+      tos[i].d_cons_args_t.push_back(std::vector<Type>());
+      for (const DatatypeConstructorArg& arg : cons)
+      {
+        /* Collect unresolved types corresponding to the typenode of the
+         * arguments */
+        tos[i].d_cons_args_t.back().push_back(tn_to_unres[TypeNode::fromType(
+            static_cast<SelectorType>(arg.getType()).getRangeType())]);
+      }
+    }
+    /* Use the sygus type to not lose reference to the original types (Bool,
+     * Int, etc) */
+    tos[i].d_dt.setSygus(dt.getSygusType(),
+                         sygus_vars.toExpr(),
+                         dt.getSygusAllowConst(),
+                         dt.getSygusAllowAll());
+    for (unsigned j = 0, size_d_ops = tos[i].d_ops.size(); j < size_d_ops; ++j)
+    {
+      tos[i].d_dt.addSygusConstructor(
+          tos[i].d_ops[j], tos[i].d_cons_names[j], tos[i].d_cons_args_t[j]);
+    }
+    Trace("sygus-grammar-normalize")
+        << "...built datatype " << tos[i].d_dt << std::endl;
+  }
+  /* Resolve types */
+  std::vector<Datatype> dts;
+  std::set<Type> unres_all;
+  for (TypeObject& to : tos)
+  {
+    dts.push_back(to.d_dt);
+    unres_all.insert(to.d_unres_t);
+  }
+  std::vector<DatatypeType> types =
+      nm->toExprManager()->mkMutualDatatypeTypes(dts, unres_all);
+  Assert(types.size() == dts.size());
+  /* By construction the normalized type node will be first one considered */
+  return TypeNode::fromType(types[0]);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h
new file mode 100644
index 000000000..bd63f5fdb
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_norm.h
@@ -0,0 +1,149 @@
+/*********************                                                        */
+/*! \file sygus_grammar_norm.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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.\endverbatim
+ **
+ ** \brief class for simplifying SyGuS grammars after they are encoded into
+ ** datatypes.
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** Keeps the necessary information about a sygus type:
+ *
+ * the original typenode, from which the datatype representation can be
+ * extracted
+ *
+ * the operators, names and argument types for each constructor
+ *
+ * the unresolved type used as placeholder for references of the yet to be built
+ * type
+ *
+ * a datatype to represent the structure of the typenode for the new type */
+struct TypeObject
+{
+  /* Both constructors create an unresolved type and datatype with the given
+   * name. An original typenode is optional, since normalized types can be
+   * created from scratch during normalization */
+  TypeObject(TypeNode src_tn, std::string type_name);
+  TypeObject(std::string type_name);
+  ~TypeObject() {}
+
+  /* The original typenode this TypeObject is built from */
+  TypeNode d_tn;
+  /* Operators for each constructor. */
+  std::vector<Expr> d_ops;
+  /* Names for each constructor. */
+  std::vector<std::string> d_cons_names;
+  /* List of argument types for each constructor */
+  std::vector<std::vector<Type>> d_cons_args_t;
+  /* Unresolved type placeholder */
+  Type d_unres_t;
+  /* Datatype to represent type's structure */
+  Datatype d_dt;
+};
+
+/** Utility for normalizing SyGuS grammars and avoid spurious enumarations
+ *
+ * Uses the datatype representation of a SyGuS grammar to identify entries that
+ * can normalized in order to have less possible enumerations. An example is
+ * with integer types, e.g.:
+ *
+ * Int -> x | y | Int + Int | Int - Int | 0 | 1 | ite( Bool, Int, Int ) |
+ *        c1...cn
+ *
+ * where c1...cn are additional constants (in the case of large constants
+ * appearing in the conjecture).
+ *
+ * becomes
+ *
+ * Int -> ite( Bool, Int, Int ) | IntN
+ * IntN -> IntX | Int0 - IntX
+ * Int0 -> 0
+ * IntX -> IntXX + IntX | IntY
+ * IntXX -> x
+ * IntY -> IntYY + IntY | IntC
+ * IntYY -> y
+ * IntC -> IntCC + IntC | IntV
+ * IntCC -> 1
+ * IntV -> 0 | c1...cn */
+class SygusGrammarNorm
+{
+ public:
+  SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p);
+  ~SygusGrammarNorm() {}
+  /** creates a normalized typenode from a given one.
+   *
+   * In a normalized typenode all of its types that can be normalized (e.g. Int)
+   * are so and its other types are structurally identical to the original
+   * typenode it normalizes.
+   *
+   * sygus_vars are the input variables for the function to be synthesized,
+   * which are used as input for the built datatypes. */
+  TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars);
+
+ private:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** parent conjecture
+   *
+   * This contains global information about the synthesis conjecture. */
+  CegConjecture* d_parent;
+
+  /** sygus term database associated with this utility */
+  TermDbSygus* d_tds;
+
+  /** normalize integer type
+   *
+   * TODO actually perform the normalization #1304
+   *
+   * ind is the index of the analyzed typeobject in tos
+   *
+   * New types created during normalization will be added to tos and
+   * tn_to_unres
+   *
+   * sygus_vars is used as above for datatype construction */
+  void normalizeSygusInt(unsigned ind,
+                         std::vector<TypeObject>& tos,
+                         std::map<TypeNode, Type>& tn_to_unres,
+                         Node sygus_vars);
+
+  /** Traverses the datatype representation of src_tn and collects the types it
+   * contains
+   *
+   * For each new typenode a TypeObject is created, with an unresolved type and
+   * a datatype to be later resolved and constructed, respectively. These are
+   * accumulated in tos.
+   *
+   * tn_to_unres maps the sygus types that the typenodes stand for into
+   * the unresolved type to be built for the typenodes normalizations.
+   *
+   * visited caches visited nodes
+   */
+  void collectInfoFor(TypeNode src_tn,
+                      std::vector<TypeObject>& tos,
+                      std::map<TypeNode, Type>& tn_to_unres,
+                      std::map<TypeNode, bool>& visited);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif