From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 00:23:05 +0000 (-0500)
Subject: Ensure standard miniscoping is applied before aggressive miniscoping (#3974)
X-Git-Tag: cvc5-1.0.0~3540
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d3df3b642aa1b346c11066be69a46f2edd1a9d9;p=cvc5.git

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 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);
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)