diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 25 |
1 files changed, 12 insertions, 13 deletions
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; |