From 7d3df3b642aa1b346c11066be69a46f2edd1a9d9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Mar 2020 19:23:05 -0500 Subject: [PATCH] Ensure standard miniscoping is applied before aggressive miniscoping (#3974) Fixes #3947. --- src/theory/quantifiers/quantifiers_rewriter.cpp | 14 +++++++++++--- test/regress/CMakeLists.txt | 1 + .../regress1/sygus/issue3947-agg-miniscope.smt2 | 9 +++++++++ 3 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/sygus/issue3947-agg-miniscope.smt2 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& 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); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0edbd094d..046b073ff 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1842,6 +1842,7 @@ set(regress_1_tests regress1/sygus/issue3802-default-consts.sy regress1/sygus/issue3839-cond-rewrite.smt2 regress1/sygus/issue3944-div-rewrite.smt2 + regress1/sygus/issue3947-agg-miniscope.smt2 regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue3947-agg-miniscope.smt2 b/test/regress/regress1/sygus/issue3947-agg-miniscope.smt2 new file mode 100644 index 000000000..c8e2db922 --- /dev/null +++ b/test/regress/regress1/sygus/issue3947-agg-miniscope.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(set-option :ag-miniscope-quant true) +(set-option :sygus-inference true) +(declare-fun a () Real) +(declare-fun b () Real) +(assert (forall ((c Real)) (or (< c a) (< 0 b)))) +(check-sat) -- 2.30.2