diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 28 |
1 files changed, 22 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ab14904ff..bcb5c58b4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2814,13 +2814,29 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node } // otherwise expand it - bool doExpand = k == kind::APPLY; - if( !doExpand ){ - // options that assign substitutions to APPLY_UF - if (options::macrosQuant() || options::sygusInference()) + bool doExpand = false; + if (k == kind::APPLY) + { + doExpand = true; + } + else if (k == kind::APPLY_UF) + { + // Always do beta-reduction here. The reason is that there may be + // operators such as INTS_MODULUS in the body of the lambda that would + // otherwise be introduced by beta-reduction via the rewriter, but are + // not expanded here since the traversal in this function does not + // traverse the operators of nodes. Hence, we beta-reduce here to + // ensure terms in the body of the lambda are expanded during this + // call. + if (n.getOperator().getKind() == kind::LAMBDA) + { + doExpand = true; + } + else if (options::macrosQuant() || options::sygusInference()) { - //expand if we have inferred an operator corresponds to a defined function - doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() ); + // The above options assign substitutions to APPLY_UF, thus we check + // here and expand if this operator corresponds to a defined function. + doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); } } if (doExpand) { |