Fix partial operator elimination in sygus grammar normalization (#2620)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index b5dea4c38da69e169b800efc6d2d4f810cfc7d77..8e41b6b0757844340c6b4b73e3fdd07737ea7ba2 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -159,20 +159,13 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
   Trace("sygus-grammar-normalize-debug")
       << ".....operator is " << sygus_op << std::endl;
   Node exp_sop_n = sygus_op;
-  // Only expand definitions if the operator is not constant, since calling
-  // expandDefinitions on them should be a no-op. This check ensures we don't
-  // try to expand e.g. bitvector extract operators, whose type is undefined,
-  // and thus should not be passed to expandDefinitions.
-  if (!sygus_op.isConst())
-  {
-    exp_sop_n = Node::fromExpr(
-        smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
-  }
-  // get the kind for the operator.
-  Kind ok = NodeManager::operatorToKind(exp_sop_n);
-  // if it is a builtin operator, convert to total version if necessary
-  if (ok != UNDEFINED_KIND)
+  if (exp_sop_n.isConst())
   {
+    // If it is a builtin operator, convert to total version if necessary.
+    // First, get the kind for the operator.
+    Kind ok = NodeManager::operatorToKind(exp_sop_n);
+    Trace("sygus-grammar-normalize-debug")
+        << "...builtin kind is " << ok << std::endl;
     Kind nk = getEliminateKind(ok);
     if (nk != ok)
     {
@@ -183,6 +176,12 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
   }
   else
   {
+    // Only expand definitions if the operator is not constant, since calling
+    // expandDefinitions on them should be a no-op. This check ensures we don't
+    // try to expand e.g. bitvector extract operators, whose type is undefined,
+    // and thus should not be passed to expandDefinitions.
+    exp_sop_n = Node::fromExpr(
+        smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
     exp_sop_n = Rewriter::rewrite(exp_sop_n);
     Trace("sygus-grammar-normalize-debug")
         << ".....operator (post-rewrite) is " << exp_sop_n << std::endl;