diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 19:23:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 19:23:05 -0500 |
commit | 7d3df3b642aa1b346c11066be69a46f2edd1a9d9 (patch) | |
tree | acf6e3887b16534283646b604595270d2083d3af /src/theory/quantifiers | |
parent | 7ccbc8647811439112951e20d0ec9e4b8448d1de (diff) |
Ensure standard miniscoping is applied before aggressive miniscoping (#3974)
Fixes #3947.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 1607dc0dc..6a54e8393 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1672,8 +1672,11 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } return mkForAll( newArgs, body[1], qa ); }else if( body.getKind()==AND ){ - if( options::miniscopeQuant() ){ - //break apart + // aggressive miniscoping implies that structural miniscoping should + // be applied first + if (options::miniscopeQuant() || options::aggressiveMiniscopeQuant()) + { + // break apart NodeBuilder<> t(kind::AND); for( unsigned i=0; i<body.getNumChildren(); i++ ){ t << computeMiniscoping( args, body[i], qa ); @@ -1685,7 +1688,12 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo if( options::quantSplit() ){ //splitting subsumes free variable miniscoping, apply it with higher priority return computeSplit( args, body, qa ); - }else if( options::miniscopeQuantFreeVar() ){ + } + else if (options::miniscopeQuantFreeVar() + || options::aggressiveMiniscopeQuant()) + { + // aggressive miniscoping implies that free variable miniscoping should + // be applied first Node newBody = body; NodeBuilder<> body_split(kind::OR); NodeBuilder<> tb(kind::OR); |