From 82ddf4c77bf234d08feaa884d9ead245abcead81 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Oct 2018 11:19:52 -0500 Subject: [PATCH] Fix partial operator elimination in sygus grammar normalization (#2620) --- .../quantifiers/sygus/sygus_grammar_norm.cpp | 25 +++++++++---------- 1 file 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; -- 2.30.2