Ensure standard miniscoping is applied before aggressive miniscoping (#3974)

Fixes #3947.

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1607dc0dc5811e87c606f0ccb3c30c61f3a49af0..6a54e83932e4faa96fd30ac6cbe1cbe718937da7 100644 (file)
--- 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);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0edbd094db1e13b4a9025bc6a976284cd85e2ec6..046b073ff4a12c4f492a22909ff2d1ac16a3402c 100644 (file)
--- 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 (file)
index 0000000..c8e2db9
--- /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)