From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Oct 2018 16:19:52 +0000 (-0500)
Subject:  Fix partial operator elimination in sygus grammar normalization (#2620)
X-Git-Tag: cvc5-1.0.0~4433
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82ddf4c77bf234d08feaa884d9ead245abcead81;p=cvc5.git

 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 b5dea4c38..8e41b6b07 100644
--- 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;