diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-10 23:55:34 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-10 23:55:34 +0000 |
commit | ed555a82d64772dcbac7772e0770c9015b11a8e8 (patch) | |
tree | c214c44390af57f14fe8f71e3eaa4ad3147e9819 /src/theory/quantifiers | |
parent | 5ab69fcdf91fb3034bf9e25f515b551124d4e747 (diff) |
Fix to quantifier rewritting not being idempotent. See bug 441.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 063875235..d25e516fe 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -224,8 +224,12 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { InstConstantAttribute ica; n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); } + + // This is required if substitute in computePrenex() is used. + return RewriteResponse(REWRITE_AGAIN_FULL, n ); + }else{ + return RewriteResponse(REWRITE_DONE, n ); } - return RewriteResponse(REWRITE_DONE, n ); } return RewriteResponse(REWRITE_DONE, in); } @@ -493,6 +497,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl; return newBody; }else{ return body; |