Support nested quantifier elimination for get-qe command (#5490)

Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.

Fixes CVC4/cvc4-wishues#26

Fixes #5484.

6 files changed, 48 insertions, 6 deletions

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 59e9dfc9e..e5ecafd4a 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/subs.h"
 #include "smt/smt_solver.h"
+#include "theory/quantifiers/cegqi/nested_qe.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -40,6 +41,10 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     throw ModalException(
         "Expecting a quantified formula as argument to get-qe.");
   }
+  // do nested quantifier elimination if necessary
+  q = quantifiers::NestedQe::doNestedQe(q, true);
+  Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
+                  << q << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   // tag the quantified formula with the quant-elim attribute
   TypeNode t = nm->booleanType();
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
index 7f77a1daf..72e7ef66f 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.cpp
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -69,6 +69,14 @@ bool NestedQe::hasNestedQuantification(Node q)
 
 Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  Node qOrig = q;
+  bool inputExists = false;
+  if (q.getKind() == kind::EXISTS)
+  {
+    q = nm->mkNode(kind::FORALL, q[0], q[1].negate());
+    inputExists = true;
+  }
   Assert(q.getKind() == kind::FORALL);
   std::unordered_set<Node, NodeHashFunction> nqs;
   if (!getNestedQuantification(q, nqs))
@@ -77,7 +85,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
         << "...no nested quantification" << std::endl;
     if (keepTopLevel)
     {
-      return q;
+      return qOrig;
     }
     // just do ordinary quantifier elimination
     Node qqe = doQe(q);
@@ -114,13 +122,12 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
   // reconstruct the body
   std::vector<Node> qargs;
   qargs.push_back(q[0]);
-  qargs.push_back(qeBody);
+  qargs.push_back(inputExists ? qeBody.negate() : qeBody);
   if (q.getNumChildren() == 3)
   {
     qargs.push_back(q[2]);
   }
-  NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::FORALL, qargs);
+  return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs);
 }
 
 Node NestedQe::doQe(Node q)
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 034226474..6d7275fac 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1865,8 +1865,9 @@ bool QuantifiersRewriter::doOperation(Node q,
   }
   else if (computeOption == COMPUTE_PROCESS_TERMS)
   {
-    return options::elimExtArithQuant()
-           || options::iteLiftQuant() != options::IteLiftQuantMode::NONE;
+    return is_std
+           && (options::elimExtArithQuant()
+               || options::iteLiftQuant() != options::IteLiftQuantMode::NONE);
   }
   else if (computeOption == COMPUTE_COND_SPLIT)
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7e87c337a..cb37b428e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1616,6 +1616,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5469-aext.smt2
   regress1/quantifiers/issue5470-aext.smt2
   regress1/quantifiers/issue5471-aext.smt2
+  regress1/quantifiers/issue5484-qe.smt2
+  regress1/quantifiers/issue5484b-qe.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2
new file mode 100644
index 000000000..c2499ed16
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun v9 () Bool)
+(declare-fun v18 () Bool)
+(declare-fun i2 () Int)
+(declare-fun v31 () Bool)
+(get-qe (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (xor (=> (not (not (distinct 83 407))) (> (- i2 31 722) 319)) (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (not (not (not v9)))) v31 (> 665 (+ (mod 83 923) (div i2 850)) 319 (- 939 878)) v18)))
diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2
new file mode 100644
index 000000000..86f999504
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2
@@ -0,0 +1,18 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v4 () Bool)
+(declare-fun v7 () Bool)
+(declare-fun v8 () Bool)
+(declare-fun i6 () Int)
+(declare-fun i9 () Int)
+(declare-fun i11 () Int)
+(declare-fun i13 () Int)
+(declare-fun v9 () Bool)
+(declare-fun i16 () Int)
+(get-qe (forall ((q75 Bool)) (xor (< i9 52) (forall ((q75 Bool)) (not (and (< i16 37) q75 q75 v1))) v2 (and (distinct v4 v3 v4) v9 v9 (and v7 v0 (>= 24 56 i11 i6 7) v0 v8)) (= (+ (div i13 340) 268 i9) i13))))