From aac70d0b7e1784f1c34be7df9e22f3fba1cb1522 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 14 Jul 2018 00:30:04 +0200
Subject: Fix and improve grammar normalization for any constant. (#2101)

---
 .../quantifiers/sygus/sygus_grammar_norm.cpp       | 65 ++++++++++++----------
 1 file changed, 35 insertions(+), 30 deletions(-)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index f4cdc22c5..8a415cc10 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -106,36 +106,6 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
                 sygus_norm->d_sygus_vars.toExpr(),
                 dt.getSygusAllowConst(),
                 dt.getSygusAllowAll());
-  if (dt.getSygusAllowConst())
-  {
-    TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
-    // must be handled by counterexample-guided instantiation
-    // don't do it for Boolean (not worth the trouble, since it has only
-    // minimal gain (1 any constant vs 2 constructors for true/false), and
-    // we need to do a lot of special symmetry breaking, e.g. for ensuring
-    // any constant constructors are not the 1st children of ITEs.
-    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
-        && !sygus_type.isBoolean())
-    {
-      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
-      // add an "any constant" proxy variable
-      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
-      // mark that it represents any constant
-      SygusAnyConstAttribute saca;
-      av.setAttribute(saca, true);
-      std::stringstream ss;
-      ss << d_unres_tn << "_any_constant";
-      std::string cname(ss.str());
-      std::vector<Type> builtin_arg;
-      builtin_arg.push_back(dt.getSygusType());
-      // we add this constructor first since we use left associative chains
-      // and our symmetry breaking should group any constants together
-      // beneath the same application
-      // we set its weight to zero since it should be considered at the
-      // same level as constants.
-      d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0);
-    }
-  }
   for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
   {
     d_dt.addSygusConstructor(d_ops[i].toExpr(),
@@ -462,6 +432,41 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
     Assert(op_pos[i] < dt.getNumConstructors());
     to.addConsInfo(this, dt[op_pos[i]]);
   }
+  if (dt.getSygusAllowConst())
+  {
+    TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
+    // must be handled by counterexample-guided instantiation
+    // don't do it for Boolean (not worth the trouble, since it has only
+    // minimal gain (1 any constant vs 2 constructors for true/false), and
+    // we need to do a lot of special symmetry breaking, e.g. for ensuring
+    // any constant constructors are not the 1st children of ITEs.
+    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
+        && !sygus_type.isBoolean())
+    {
+      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
+      // add an "any constant" proxy variable
+      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
+      // mark that it represents any constant
+      SygusAnyConstAttribute saca;
+      av.setAttribute(saca, true);
+      std::stringstream ss;
+      ss << to.d_unres_tn << "_any_constant";
+      std::string cname(ss.str());
+      std::vector<Type> builtin_arg;
+      builtin_arg.push_back(dt.getSygusType());
+      // we add this constructor first since we use left associative chains
+      // and our symmetry breaking should group any constants together
+      // beneath the same application
+      // we set its weight to zero since it should be considered at the
+      // same level as constants.
+      to.d_ops.insert(to.d_ops.begin(), av.toExpr());
+      to.d_cons_names.insert(to.d_cons_names.begin(), cname);
+      to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg);
+      to.d_pc.insert(to.d_pc.begin(),
+                     printer::SygusEmptyPrintCallback::getEmptyPC());
+      to.d_weight.insert(to.d_weight.begin(), 0);
+    }
+  }
   /* Build normalize datatype */
   if (Trace.isOn("sygus-grammar-normalize"))
   {
-- 
cgit v1.2.3