diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-08 12:08:20 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-08-08 12:08:20 -0500 |
commit | c90efa1b1a5dbf1d7c1188787adcfc889640b61e (patch) | |
tree | c074f3ed64ed30a651a4f7f3c0ed30b675acf8c3 | |
parent | 047e75b485ad16a729083c210ba4064943d2e7c5 (diff) |
Do beta-reduction in expandDefinitions (#2286)
-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) { |