Normalize grammars - 2 (#1420)

This is another step towards addressing #1304 and #1344. This pull request:

- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback

This lays the basis for more general linearizations.

7 files changed, 760 insertions, 208 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 4a7a9e8a7..f997a8923 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -272,8 +272,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false
   aggressively minimize sygus grammars
 option sygusAddConstGrammar --sygus-add-const-grammar bool :default true
   statically add constants appearing in conjecture to grammars
-option sygusNormalizeGrammar --sygus-norm-grammar bool :default false
-  statically normalize sygus grammars based on flattening
+option sygusGrammarNorm --sygus-grammar-norm bool :default false
+  statically normalize sygus grammars based on flattening (linearization)
 option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false
   embed sygus templates into grammars
   
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index c5287e469..77f68e097 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -208,5 +208,7 @@ void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
   }
 }
 
+std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr;
+
 } /* CVC4::printer namespace */
 } /* CVC4 namespace */
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index 84da0f86c..e0c220e00 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -154,6 +154,19 @@ class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
   virtual void toStreamSygus(const Printer* p,
                              std::ostream& out,
                              Expr e) const override;
+  /* Retrieves empty callback pointer */
+  static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC()
+  {
+    if (!d_empty_pc)
+    {
+      d_empty_pc = std::make_shared<SygusEmptyPrintCallback>();
+    }
+    return d_empty_pc;
+  }
+
+ private:
+  /* empty callback object */
+  static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc;
 };
 
 } /* CVC4::printer namespace */
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index 05aa599b1..ee1b50842 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -119,11 +119,8 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
           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);
-    }
+    SygusGrammarNorm sygus_norm(d_qe);
+    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
index 9037566b7..67c40d6aa 100644
--- a/src/theory/quantifiers/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus_grammar_norm.cpp
@@ -17,162 +17,435 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
+#include <numeric>  // for std::iota
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TypeObject::TypeObject(std::string type_name) : d_dt(Datatype(type_name))
+bool OpPosTrie::getOrMakeType(TypeNode tn,
+                              TypeNode& unres_tn,
+                              std::vector<unsigned> op_pos,
+                              unsigned ind)
 {
-  d_tn = TypeNode::null();
-  /* Create an unresolved type */
-  d_unres_t = NodeManager::currentNM()
-                  ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
-                  .toType();
+  if (ind == op_pos.size())
+  {
+    /* Found type */
+    if (!d_unres_tn.isNull())
+    {
+      Trace("sygus-grammar-normalize-trie")
+          << "\tFound type " << d_unres_tn << "\n";
+      unres_tn = d_unres_tn;
+      return true;
+    }
+    /* Creating unresolved type */
+    std::stringstream ss;
+    ss << tn << "_";
+    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+    {
+      ss << "_" << std::to_string(op_pos[i]);
+    }
+    d_unres_tn = NodeManager::currentNM()->mkSort(
+        ss.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
+    Trace("sygus-grammar-normalize-trie")
+        << "\tCreating type " << d_unres_tn << "\n";
+    unres_tn = d_unres_tn;
+    return false;
+  }
+  /* Go to next node */
+  return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
 }
 
-TypeObject::TypeObject(TypeNode src_tn, std::string type_name)
-    : d_dt(Datatype(type_name))
+void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
+                                               const DatatypeConstructor& cons)
 {
-  d_tn = src_tn;
-  d_t = src_tn.toType();
-  /* Create an unresolved type */
-  d_unres_t = NodeManager::currentNM()
-                  ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
-                  .toType();
+  Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
+  /* Recover the sygus operator to not lose reference to the original
+   * operator (NOT, ITE, etc) */
+  Node exp_sop_n = Node::fromExpr(
+      smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp()));
+  d_ops.push_back(Rewriter::rewrite(exp_sop_n));
+  Trace("sygus-grammar-normalize-defs")
+      << "\tOriginal op: " << cons.getSygusOp()
+      << "\n\tExpanded one: " << exp_sop_n
+      << "\n\tRewritten one: " << d_ops.back() << "\n\n";
+  d_cons_names.push_back(cons.getName());
+  d_pc.push_back(cons.getSygusPrintCallback());
+  d_weight.push_back(cons.getWeight());
+  d_cons_args_t.push_back(std::vector<Type>());
+  for (const DatatypeConstructorArg& arg : cons)
+  {
+    /* Collect unresolved type nodes corresponding to the typenode of the
+     * arguments */
+    d_cons_args_t.back().push_back(
+        sygus_norm
+            ->normalizeSygusRec(TypeNode::fromType(
+                static_cast<SelectorType>(arg.getType()).getRangeType()))
+            .toType());
+  }
+}
+
+void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
+                                                 const Datatype& dt)
+{
+  /* Use the sygus type to not lose reference to the original types (Bool,
+   * Int, etc) */
+  d_dt.setSygus(dt.getSygusType(),
+                sygus_norm->d_sygus_vars.toExpr(),
+                dt.getSygusAllowConst(),
+                dt.getSygusAllowAll());
+  for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+  {
+    d_dt.addSygusConstructor(d_ops[i].toExpr(),
+                             d_cons_names[i],
+                             d_cons_args_t[i],
+                             d_pc[i],
+                             d_weight[i]);
+  }
+  Trace("sygus-grammar-normalize") << "...built datatype " << d_dt << " ";
+  /* Add to global accumulators */
+  sygus_norm->d_dt_all.push_back(d_dt);
+  sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
+  Trace("sygus-grammar-normalize") << "---------------------------------\n";
+}
+
+/* TODO #1304: have more operators and types. Moreover, have more general ways
+   of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
+   function should realize that it is chainable for integers */
+bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op)
+{
+  /* Checks whether operator occurs chainable for its type */
+  if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS)
+  {
+    return true;
+  }
+  return false;
 }
 
-SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p)
-    : d_qe(qe), d_parent(p), d_tds(d_qe->getTermDatabaseSygus())
+/* TODO #1304: have more operators and types. Moreover, have more general ways
+   of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
+   function should realize that it is chainable for integers */
+bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n)
 {
+  if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS
+      && n == TermUtil::mkTypeValue(tn, 0))
+  {
+    return true;
+  }
+  return false;
 }
 
-/* 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)
+void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
+                                              TypeObject& to,
+                                              const Datatype& dt,
+                                              std::vector<unsigned>& op_pos)
 {
-  if (visited.find(tn) != visited.end())
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<unsigned> claimed(d_elem_pos);
+  claimed.push_back(d_chain_op_pos);
+  unsigned nb_op_pos = op_pos.size();
+  /* TODO do this properly */
+  /* Remove from op_pos the positions claimed by the transformation */
+  std::sort(op_pos.begin(), op_pos.end());
+  std::sort(claimed.begin(), claimed.end());
+  std::vector<unsigned> difference;
+  std::set_difference(op_pos.begin(),
+                      op_pos.end(),
+                      claimed.begin(),
+                      claimed.end(),
+                      std::back_inserter(difference));
+  op_pos = difference;
+  if (Trace.isOn("sygus-grammar-normalize-chain"))
+  {
+    Trace("sygus-grammar-normalize-chain")
+        << "OP at " << d_chain_op_pos << "\n"
+        << d_elem_pos.size() << " d_elem_pos: ";
+    for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize-chain") << d_elem_pos[i] << " ";
+    }
+    Trace("sygus-grammar-normalize-chain")
+        << "\n"
+        << op_pos.size() << " remaining op_pos: ";
+    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize-chain") << op_pos[i] << " ";
+    }
+    Trace("sygus-grammar-normalize-chain") << "\n";
+  }
+  /* Build identity operator and empty callback */
+  Node iden_op =
+      SygusGrammarNorm::getIdOp(TypeNode::fromType(dt.getSygusType()));
+  /* If all operators are claimed, create a monomial */
+  if (nb_op_pos == d_elem_pos.size() + 1)
+  {
+    Trace("sygus-grammar-normalize-chain")
+        << "\tCreating id type for " << d_elem_pos.back() << "\n";
+    /* creates type for element */
+    std::vector<unsigned> tmp;
+    tmp.push_back(d_elem_pos.back());
+    Type t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp).toType();
+    /* consumes element */
+    d_elem_pos.pop_back();
+    /* adds to Root: "type" */
+    to.d_ops.push_back(iden_op);
+    to.d_cons_names.push_back("id");
+    to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
+    /* Identity operators should not increase the size of terms */
+    to.d_weight.push_back(0);
+    to.d_cons_args_t.push_back(std::vector<Type>());
+    to.d_cons_args_t.back().push_back(t);
+    Trace("sygus-grammar-normalize-chain")
+        << "\tAdding  " << t << " to " << to.d_unres_tn << "\n";
+    /* adds to Root: "type + Root" */
+    to.d_ops.push_back(nm->operatorOf(PLUS));
+    to.d_cons_names.push_back(kindToString(PLUS));
+    to.d_pc.push_back(nullptr);
+    to.d_weight.push_back(-1);
+    to.d_cons_args_t.push_back(std::vector<Type>());
+    to.d_cons_args_t.back().push_back(t);
+    to.d_cons_args_t.back().push_back(to.d_unres_tn.toType());
+    Trace("sygus-grammar-normalize-chain")
+        << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
+        << to.d_unres_tn << " and " << t << "\n";
+  }
+  /* In the initial case if not all operators claimed always creates a next */
+  Assert(nb_op_pos != d_elem_pos.size() + 1 || d_elem_pos.size() > 1);
+  /* TODO #1304: consider case in which CHAIN op has different types than
+     to.d_tn */
+  /* If no more elements to chain, finish */
+  if (d_elem_pos.size() == 0)
   {
     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>(tos.back().d_t).getDatatype();
-  tn_to_unres[tn] = tos.back().d_unres_t;
-  /* Visit types of constructor arguments */
-  for (const DatatypeConstructor& cons : dt)
+  /* Creates a type do be added to root representing next step in the chain */
+  /* Add + to elems */
+  d_elem_pos.push_back(d_chain_op_pos);
+  if (Trace.isOn("sygus-grammar-normalize-chain"))
   {
-    for (const DatatypeConstructorArg& arg : cons)
+    Trace("sygus-grammar-normalize-chain")
+        << "\tCreating type for next entry with sygus_ops ";
+    for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
     {
-      collectInfoFor(
-          TypeNode::fromType(
-              static_cast<SelectorType>(arg.getType()).getRangeType()),
-          tos,
-          tn_to_unres,
-          visited);
+      Trace("sygus-grammar-normalize-chain")
+          << dt[d_elem_pos[i]].getSygusOp() << " ";
     }
+    Trace("sygus-grammar-normalize-chain") << "\n";
   }
+  /* adds to Root: (\lambda x. x ) Next */
+  to.d_ops.push_back(iden_op);
+  to.d_cons_names.push_back("id_next");
+  to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
+  to.d_weight.push_back(0);
+  to.d_cons_args_t.push_back(std::vector<Type>());
+  to.d_cons_args_t.back().push_back(
+      sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType());
 }
 
-void SygusGrammarNorm::normalizeSygusInt(unsigned ind,
-                                         std::vector<TypeObject>& tos,
-                                         std::map<TypeNode, Type>& tn_to_unres,
-                                         Node sygus_vars)
+std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
+
+/* Traverse the constructors of dt according to the positions in op_pos. Collect
+ * those that fit the kinds established by to_collect. Remove collected operator
+ * positions from op_pos. Accumulate collected positions in collected
+ *
+ * returns true if collected anything
+ */
+SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
+    TypeNode tn, const Datatype& dt, const std::vector<unsigned>& op_pos)
 {
-  const Datatype& dt =
-      static_cast<DatatypeType>(tos[ind].d_t).getDatatype();
-  Trace("sygus-grammar-normalize")
-      << "Normalizing integer type " << tos[ind].d_tn << " from datatype\n"
-      << dt << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+  /* TODO #1304: step 0: look for redundant constructors to drop */
+  /* TODO #1304: step 1: look for singleton */
+  /* step 2: look for chain */
+  unsigned chain_op_pos = dt.getNumConstructors();
+  std::vector<unsigned> elem_pos;
+  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+  {
+    Assert(op_pos[i] < dt.getNumConstructors());
+    Expr sop = dt[op_pos[i]].getSygusOp();
+    /* Collects a chainable operator such as PLUS */
+    if (sop.getKind() == BUILTIN
+        && TransfChain::isChainable(sygus_tn, Node::fromExpr(sop)))
+    {
+      Assert(nm->operatorToKind(Node::fromExpr(sop)) == PLUS);
+      /* TODO #1304: be robust for this case */
+      /* For now only transforms applications whose arguments have the same type
+       * as the root */
+      bool same_type_plus = true;
+      for (const DatatypeConstructorArg& arg : dt[op_pos[i]])
+      {
+        if (TypeNode::fromType(
+                static_cast<SelectorType>(arg.getType()).getRangeType())
+            != tn)
+        {
+          same_type_plus = false;
+          break;
+        }
+      }
+      if (!same_type_plus)
+      {
+        Trace("sygus-grammar-normalize-infer")
+            << "\tFor OP " << PLUS << " did not collecting sop " << sop
+            << " in position " << op_pos[i] << "\n";
+        continue;
+      }
+      Assert(chain_op_pos == dt.getNumConstructors());
+      Trace("sygus-grammar-normalize-infer")
+          << "\tCollecting chainable OP " << sop << " in position " << op_pos[i]
+          << "\n";
+      chain_op_pos = op_pos[i];
+      continue;
+    }
+    /* TODO #1304: check this for each operator */
+    /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
+    if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), Node::fromExpr(sop)))
+    {
+      Trace("sygus-grammar-normalize-infer")
+          << "\tCollecting for NON_ID_ELEMS the sop " << sop
+          << " in position " << op_pos[i] << "\n";
+      elem_pos.push_back(op_pos[i]);
+    }
+  }
+  /* Typenode admits a chain transformation for normalization */
+  if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
+  {
+    Trace("sygus-grammar-normalize-infer")
+        << "\tInfering chain transformation\n";
+    return new TransfChain(chain_op_pos, elem_pos);
+  }
+  return nullptr;
 }
 
-TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
+                                             const Datatype& dt,
+                                             std::vector<unsigned>& op_pos)
 {
-  /* 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_t).getDatatype();
-    Trace("sygus-grammar-normalize")
-        << "Rebuild " << tos[i].d_tn << " from " << dt << std::endl;
-    /* Collect information to rebuild constructors */
-    for (const DatatypeConstructor& cons : dt)
+  /* Corresponding type node to tn with the given operator positions. To be
+   * retrieved (if cached) or defined (otherwise) */
+  TypeNode unres_tn;
+  if (Trace.isOn("sygus-grammar-normalize-trie"))
+  {
+    Trace("sygus-grammar-normalize-trie")
+        << "\tRecursing on " << tn << " with op_positions ";
+    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
+    }
+    Trace("sygus-grammar-normalize-trie") << "\n";
+  }
+  /* Checks if unresolved type already created (and returns) or creates it
+   * (and then proceeds to definition) */
+  std::sort(op_pos.begin(), op_pos.end());
+  if (d_tries[tn].getOrMakeType(tn, unres_tn, op_pos))
+  {
+    if (Trace.isOn("sygus-grammar-normalize-trie"))
     {
-      Trace("sygus-grammar-normalize")
-          << "...for " << cons.getName() << std::endl;
-      /* Recover the sygus operator to not lose reference to the original
-       * operator (NOT, ITE, etc) */
-      Node exp_sop_n = Node::fromExpr(
-          smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp()));
-      tos[i].d_ops.push_back(Rewriter::rewrite(exp_sop_n));
-      Trace("sygus-grammar-normalize")
-          << "\tOriginal op: " << cons.getSygusOp()
-          << "\n\tExpanded one: " << exp_sop_n
-          << "\n\tRewritten one: " << tos[i].d_ops.back() << std::endl;
-      tos[i].d_cons_names.push_back(cons.getName());
-      tos[i].d_pcb.push_back(cons.getSygusPrintCallback());
-      tos[i].d_cons_args_t.push_back(std::vector<Type>());
-      for (const DatatypeConstructorArg& arg : cons)
+      Trace("sygus-grammar-normalize-trie")
+          << "\tTypenode " << tn << " has already been normalized with op_pos ";
+      for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
       {
-        /* 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())]);
+        Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
       }
+      Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn << "\n";
+    }
+    return unres_tn;
+  }
+  if (Trace.isOn("sygus-grammar-normalize-trie"))
+  {
+    Trace("sygus-grammar-normalize-trie")
+        << "\tTypenode " << tn << " not yet normalized with op_pos ";
+    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
     }
-    /* 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)
+    Trace("sygus-grammar-normalize-trie") << "\n";
+  }
+  /* Creates type object for normalization */
+  TypeObject to(tn, unres_tn);
+  /* If normalization option enabled, infer transformations to be applied in the
+   * type */
+  if (options::sygusGrammarNorm())
+  {
+    /* Determine normalization transformation based on sygus type and given
+     * operators */
+    Transf* transformation = inferTransf(tn, dt, op_pos);
+    /* If a transformation was selected, apply it */
+    if (transformation != nullptr)
     {
-      tos[i].d_dt.addSygusConstructor(tos[i].d_ops[j].toExpr(),
-                                      tos[i].d_cons_names[j],
-                                      tos[i].d_cons_args_t[j],
-                                      tos[i].d_pcb[j]);
+      transformation->buildType(this, to, dt, op_pos);
     }
-    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)
+  /* Remaining operators are rebuilt as they are */
+  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
   {
-    dts.push_back(to.d_dt);
-    unres_all.insert(to.d_unres_t);
+    Assert(op_pos[i] < dt.getNumConstructors());
+    to.addConsInfo(this, dt[op_pos[i]]);
+  }
+  /* Build normalize datatype */
+  if (Trace.isOn("sygus-grammar-normalize"))
+  {
+    Trace("sygus-grammar-normalize") << "\nFor positions ";
+    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize") << op_pos[i] << " ";
+    }
+    Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
+  }
+  to.buildDatatype(this, dt);
+  return to.d_unres_tn;
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
+{
+  /* Collect all operators for normalization */
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  std::vector<unsigned> op_pos(dt.getNumConstructors());
+  std::iota(op_pos.begin(), op_pos.end(), 0);
+  return normalizeSygusRec(tn, dt, op_pos);
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+{
+  /* Normalize all types in tn */
+  d_sygus_vars = sygus_vars;
+  normalizeSygusRec(tn);
+  /* Resolve created types */
+  Assert(!d_dt_all.empty() && !d_unres_t_all.empty());
+  if (Trace.isOn("sygus-grammar-normalize-build"))
+  {
+    Trace("sygus-grammar-normalize-build")
+        << "making mutual datatyes with datatypes \n";
+    for (unsigned i = 0, size = d_dt_all.size(); i < size; ++i)
+    {
+      Trace("sygus-grammar-normalize-build") << d_dt_all[i];
+    }
+    Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
+    for (const Type& unres_t : d_unres_t_all)
+    {
+      Trace("sygus-grammar-normalize-build") << unres_t << " ";
+    }
+    Trace("sygus-grammar-normalize-build") << "\n";
   }
+  Assert(d_dt_all.size() == d_unres_t_all.size());
   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]);
+      NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
+          d_dt_all, d_unres_t_all);
+  Assert(types.size() == d_dt_all.size());
+  /* Clear accumulators */
+  d_dt_all.clear();
+  d_unres_t_all.clear();
+  /* By construction the normalized type node will be the last one considered */
+  return TypeNode::fromType(types.back());
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h
index 15b4502d3..38e3f168e 100644
--- a/src/theory/quantifiers/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus_grammar_norm.h
@@ -14,137 +14,407 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
 
+#include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class CegConjecture;
+class SygusGrammarNorm;
 
-/** Keeps the necessary information about a sygus type:
+/** Operator position trie class
  *
- * the original typenode, from which the datatype representation can be
- * extracted
+ * This data structure stores an unresolved type corresponding to the
+ * normalization of a type. This unresolved type is indexed by the positions of
+ * the construtors of the datatype associated with the original type. The list
+ * of positions represent the operators, associated with the respective
+ * considered constructors, that were used for building the unresolved type.
  *
- * the operators, names and argument types for each constructor
+ * Example:
  *
- * the unresolved type used as placeholder for references of the yet to be built
- * type
+ * Let A be a type defined by the grammar "A -> x | 0 | 1 | A + A". In its
+ * datatype representation the operator for "x" is in position 0, for "0" in
+ * position "1" and so on. Consider entries (T, [op_1, ..., op_n]) -> T' to
+ * represent that a type T is normalized with operators [op_1, ..., op_n] into
+ * the type T'. For entries
  *
- * a datatype to represent the structure of the typenode for the new type */
-struct TypeObject
+ * (A, [x, 0, 1, +]) -> A1
+ * (A, [x, 1, +]) -> A2
+ * (A, [1, +]) -> A3
+ * (A, [0]) -> AZ
+ * (A, [x]) -> AX
+ * (A, [1]) -> AO
+ *
+ * the OpPosTrie T we build for this type is :
+ *
+ * T[A] :
+ *      T[A].d_children[0] : AX
+ *        T[A].d_children[0].d_children[1] :
+ *          T[A].d_children[0].d_children[1].d_children[2] :
+ *            T[A].d_children[0].d_children[1].d_children[2].d_children[3] : A1
+ *        T[A].d_children[0].d_children[2] :
+ *          T[A].d_children[0].d_children[2].d_children[3] : A2
+ *      T[A].d_children[1] : AZ
+ *      T[A].d_children[2] : AO
+ *        T[A].d_children[2].d_children[4] : A3
+ *
+ * Nodes store the types built for the path of positions up to that point, if
+ * any.
+ */
+class OpPosTrie
 {
-  /* 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;
-  /* The type represented by d_tn */
-  Type d_t;
-  /* Operators for each constructor. */
-  std::vector<Node> d_ops;
-  /* Names for each constructor. */
-  std::vector<std::string> d_cons_names;
-  /* Print callbacks for each constructor */
-  std::vector<std::shared_ptr<SygusPrintCallback>> d_pcb;
-  /* 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
+ public:
+  /** type retrieval/addition
+   *
+   * if type indexed by the given operator positions is already in the trie then
+   * unres_t becomes the indexed type and true is returned. Otherwise a new type
+   * is created, indexed by the given positions, and assigned to unres_t, with
+   * false being returned.
+   */
+  bool getOrMakeType(TypeNode tn,
+                     TypeNode& unres_tn,
+                     std::vector<unsigned> op_pos,
+                     unsigned ind = 0);
+  /** clear all data from this trie */
+  void clear() { d_children.clear(); }
+
+ private:
+  /** the data (only set for the final node of an inserted path) */
+  TypeNode d_unres_tn;
+  /* the children of the trie node */
+  std::map<unsigned, OpPosTrie> d_children;
+}; /* class OpPosTrie */
+
+/** Utility for normalizing SyGuS grammars to avoid spurious enumerations
  *
  * 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).
+ * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
  *
  * 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 */
+ * Int0 -> IntZ | Int1
+ * IntZ -> 0
+ * Int1 -> IntX | IntX + Int1 | Int2
+ * IntX -> x
+ * Int2 -> IntY | IntY + Int2 | Int3
+ * IntY -> y
+ * Int3 -> IntO | IntO + Int3 | Int4
+ * IntO -> 1
+ * Int4 -> IntITE | IntITE + Int4
+ * IntITE -> ite(Bool, Int0, Int0)
+ *
+ * TODO: #1304 normalize more complex grammars
+ *
+ * This class also performs more straightforward normalizations, such as
+ * expanding definitions of functions declared with a "define-fun" command.
+ * These lighweight transformations are always applied, independently of the
+ * normalization option being enabled.
+ */
 class SygusGrammarNorm
 {
  public:
-  SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p);
+  SygusGrammarNorm(QuantifiersEngine* qe)
+      : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
+  {
+  }
   ~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.
+   * In a normalized typenode all typenodes it contains are normalized.
+   * Normalized typenodes can be structurally identicial to their original
+   * counterparts.
    *
    * sygus_vars are the input variables for the function to be synthesized,
-   * which are used as input for the built datatypes. */
+   * which are used as input for the built datatypes.
+   *
+   * This is the function that will resolve all types and datatypes built during
+   * normalization. This operation can only be performed after all types
+   * contained in "tn" have been normalized, since the resolution of datatypes
+   * depends on all types involved being defined.
+   */
   TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars);
 
+  /* Retrives, or, if none, creates, stores and returns, the node for the
+   * identity operator (\lambda x. x) for the given type node */
+  static inline Node getIdOp(TypeNode tn)
+  {
+    auto it = d_tn_to_id.find(tn);
+    if (it == d_tn_to_id.end())
+    {
+      std::vector<Node> vars = {NodeManager::currentNM()->mkBoundVar(tn)};
+      Node n = NodeManager::currentNM()->mkNode(
+          kind::LAMBDA,
+          NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars),
+          vars.back());
+      d_tn_to_id[tn] = n;
+      return n;
+    }
+    return it->second;
+  }
+
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
-  /** parent conjecture
+  /** Keeps the necessary information for bulding a normalized type:
+   *
+   * the original typenode, from which the datatype representation can be
+   * extracted
+   *
+   * the operators, names, print callbacks and list of argument types for each
+   * constructor
    *
-   * This contains global information about the synthesis conjecture. */
-  CegConjecture* d_parent;
+   * the unresolved type node used as placeholder for references of the yet to
+   * be built normalized type
+   *
+   * a datatype to represent the structure of the type node for the normalized
+   * type
+   */
+  class TypeObject
+  {
+   public:
+    /* Stores the original type node and the unresolved placeholder. The
+     * datatype for the latter is created with the respective name. */
+    TypeObject(TypeNode src_tn, TypeNode unres_tn)
+        : d_tn(src_tn),
+          d_unres_tn(unres_tn),
+          d_dt(Datatype(unres_tn.getAttribute(expr::VarNameAttr())))
+    {
+    }
+    ~TypeObject() {}
+
+    /** adds information in "cons" (operator, name, print callback, argument
+     * types) as it is into "to"
+     *
+     * A side effect of this procedure is to expand the definitions in the sygus
+     * operator of "cons"
+     *
+     * The types of the arguments of "cons" are recursively normalized
+     */
+    void addConsInfo(SygusGrammarNorm* sygus_norm,
+                     const DatatypeConstructor& cons);
+
+    /** builds a datatype with the information in the type object
+     *
+     * "dt" is the datatype of the original typenode. It is necessary for
+     * retrieving ancillary information during the datatype building, such as
+     * its sygus type (e.g. Int)
+     *
+     * The built datatype and its unresolved type are saved in the global
+     * accumulators of "sygus_norm"
+     */
+    void buildDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
+
+    //---------- information stored from original type node
+
+    /* The original typenode this TypeObject is built from */
+    TypeNode d_tn;
 
+    //---------- information to build normalized type node
+
+    /* Operators for each constructor. */
+    std::vector<Node> d_ops;
+    /* Names for each constructor. */
+    std::vector<std::string> d_cons_names;
+    /* Print callbacks for each constructor */
+    std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
+    /* Weights for each constructor */
+    std::vector<int> d_weight;
+    /* List of argument types for each constructor */
+    std::vector<std::vector<Type>> d_cons_args_t;
+    /* Unresolved type node placeholder */
+    TypeNode d_unres_tn;
+    /* Datatype to represent type's structure */
+    Datatype d_dt;
+  }; /* class TypeObject */
+
+  /** Transformation abstract class
+   *
+   * Classes extending this one will define specif transformationst for building
+   * normalized types based on applications of specific operators
+   */
+  class Transf
+  {
+   public:
+    /** abstract function for building normalized types
+     *
+     * Builds normalized types for the operators specifed by the positions in
+     * op_pos of constructors from dt. The built types are associated with the
+     * given type object and accumulated in the sygus_norm object, whose
+     * utilities for any extra necessary normalization.
+     */
+    virtual void buildType(SygusGrammarNorm* sygus_norm,
+                           TypeObject& to,
+                           const Datatype& dt,
+                           std::vector<unsigned>& op_pos) = 0;
+  }; /* class Transf */
+
+  /** Chain transformation class
+   *
+   * Determines how to build normalized types by chaining the application of one
+   * of its operators. The resulting type should admit the same terms as the
+   * previous one modulo commutativity, associativity and identity of the
+   * neutral element.
+   *
+   * TODO: #1304:
+   * - define this transformation for more than just PLUS for Int.
+   * - improve the building such that elements that should not be entitled a
+   * "link in the chain" (such as 5 in opposition to variables and 1) do not get
+   * one
+   * - consider the case when operator is applied to different types, e.g.:
+   *   A -> B + B | x; B -> 0 | 1
+   * - consider the case in which in which the operator occurs nested in an
+   *   argument type of itself, e.g.:
+   *   A -> (B + B) + B | x; B -> 0 | 1
+   */
+  class TransfChain : public Transf
+  {
+   public:
+    TransfChain(unsigned chain_op_pos, std::vector<unsigned> elem_pos)
+        : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
+
+    /** builds types encoding a chain in which each link contains a repetition
+     * of the application of the chain operator over a non-identity element
+     *
+     * Example: when considering, over the integers, the operator "+" and the
+     * elemenst "1", "x" and "y", the built chain is e.g.
+     *
+     * x + ... + x + y + ... + y + 1 + ...+ 1
+     *
+     * whose encoding in types would be e.g.
+     *
+     * A  -> AX | AX + A | B
+     * AX -> x
+     * B  -> BY | BY + B | C
+     * BY -> y
+     * C  -> C1 | C1 + C
+     * C1 -> 1
+     *
+     * ++++++++
+     *
+     * The types composing links in the chain are built recursively by invoking
+     * sygus_norm, which caches results and handles the global normalization, on
+     * the operators not used in a given link, which will lead to recalling this
+     * transformation and so on until all operators originally given are
+     * considered.
+     */
+    virtual void buildType(SygusGrammarNorm* sygus_norm,
+                           TypeObject& to,
+                           const Datatype& dt,
+                           std::vector<unsigned>& op_pos) override;
+
+    /** Whether operator is chainable for the type (e.g. PLUS for Int)
+     *
+     *  Since the map this function depends on cannot be built statically, this
+     *  function first build maps the first time a type is checked. As a
+     *  consequence the list of chainabel operators is hardcoded in the map
+     *  building.
+     *
+     * TODO: #1304: Cover more types and operators, make this robust to more
+     * complex grammars
+     */
+    static bool isChainable(TypeNode tn, Node op);
+    /* Whether n is the identity for the chain operator of the type (e.g. 1 is
+     * not the identity 0 for PLUS for Int)
+     *
+     * TODO: #1304: Cover more types, make this robust to more complex grammars
+     */
+    static bool isId(TypeNode tn, Node op, Node n);
+
+   private:
+    /* TODO #1304: this should admit more than one, as well as which elements
+     * are associated with which operator */
+    /* Position of chain operator */
+    unsigned d_chain_op_pos;
+    /* Positions (of constructors in the datatype whose type is being
+     * normalized) of elements the chain operator is applied to */
+    std::vector<unsigned> d_elem_pos;
+    /** Specifies for each type node which are its chainable operators
+     *
+     * For example, for Int the map is {OP -> [+]}
+     *
+     * TODO #1304: consider more operators
+     */
+    static std::map<TypeNode, std::vector<Kind>> d_chain_ops;
+    /** Specifies for each type node and chainable operator its identity
+     *
+     * For example, for Int and PLUS the map is {Int -> {+ -> 0}}
+     *
+     * TODO #1304: consider more operators
+     */
+    static std::map<TypeNode, std::map<Kind, Node>> d_chain_op_id;
+
+  }; /* class TransfChain */
+
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
   /** sygus term database associated with this utility */
   TermDbSygus* d_tds;
+  /** List of variable inputs of function-to-synthesize.
+   *
+   * This information is needed in the construction of each datatype
+   * representation of type nodes contained in the type node being normalized
+   */
+  TNode d_sygus_vars;
+  /* Datatypes to be resolved */
+  std::vector<Datatype> d_dt_all;
+  /* Types to be resolved */
+  std::set<Type> d_unres_t_all;
+  /* Associates type nodes with OpPosTries */
+  std::map<TypeNode, OpPosTrie> d_tries;
+  /* Map of type nodes into their identity operators (\lambda x. x) */
+  static std::map<TypeNode, Node> d_tn_to_id;
 
-  /** normalize integer type
+  /** recursively traverses a typenode normalizing all of its elements
    *
-   * TODO actually perform the normalization #1304
+   * "tn" is the typenode to be normalized
+   * "dt" is its datatype representation
+   * "op_pos" is the list of positions of construtors of dt that are being
+   * considered for the normalization
    *
-   * ind is the index of the analyzed typeobject in tos
+   * The result of normalizing tn with the respective constructors is cached
+   * with an OpPosTrie. New types and datatypes created during normalization are
+   * accumulated grobally to be later resolved.
    *
-   * New types created during normalization will be added to tos and
-   * tn_to_unres
+   * The normalization occurs following some inferred transformation based on
+   * the sygus type (e.g. Int) of tn, and the operators being considered.
    *
-   * 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
+   * Example: Let A be the type node encoding the grammar
    *
-   * 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.
+   * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
    *
-   * tn_to_unres maps the sygus types that the typenodes stand for into
-   * the unresolved type to be built for the typenodes normalizations.
+   * and assume all its datatype constructors are being used for
+   * normalization. The inferred normalization transformation will consider the
+   * non-zero elements {x, y, 1, ite(...)} and the operator {+} to build a chain
+   * of monomials, as seen above. The operator for "0" is rebuilt as is (the
+   * default behaviour of operators not selected for transformations).
+   *
+   * recursion depth is limited by the height of the types, which is small
+   */
+  TypeNode normalizeSygusRec(TypeNode tn,
+                             const Datatype& dt,
+                             std::vector<unsigned>& op_pos);
+
+  /** wrapper for the above function
+   *
+   * invoked when all operators of "tn" are to be considered for normalization
+   */
+  TypeNode normalizeSygusRec(TypeNode tn);
+
+  /** infers a transformation for normalizing dt when allowed to use the
+   * operators in the positions op_pos.
    *
-   * visited caches visited nodes
+   * TODO: #1304: Infer more complex transformations
    */
-  void collectInfoFor(TypeNode src_tn,
-                      std::vector<TypeObject>& tos,
-                      std::map<TypeNode, Type>& tn_to_unres,
-                      std::map<TypeNode, bool>& visited);
-};
+  Transf* inferTransf(TypeNode tn,
+                      const Datatype& dt,
+                      const std::vector<unsigned>& op_pos);
+}; /* class SygusGrammarNorm */
 
 }  // namespace quantifiers
 }  // namespace theory
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 8625d9089..295d7fb52 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -237,8 +237,6 @@ Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) {
     Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl;
     Node gr = Rewriter::rewrite( g );
     Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl;
-    gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) );
-    Trace("sygus-db-debug") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl;
     d_generic_base[tn][c] = gr;
     return gr;
   }else{
@@ -411,8 +409,7 @@ Node TermDbSygus::getNormalized(TypeNode t, Node prog)
 {
   std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
   if( itn==d_normalized[t].end() ){
-    Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
-    progr = Rewriter::rewrite( progr );
+    Node progr = Rewriter::rewrite( prog );
     Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
     d_normalized[t][prog] = progr;
     return progr;